oneScript.sml
1(* ===================================================================== *)
2(* FILE : oneScript.sml *)
3(* DESCRIPTION : Creates the theory "one" containing the logical *)
4(* definition of the type :one, the type with only one *)
5(* value. The type :one is defined and the following *)
6(* `axiomatization` is proven from the definition of the *)
7(* type: *)
8(* *)
9(* one_axiom: |- !f g. f = (g:'a->one) *)
10(* *)
11(* an alternative axiom is also proved: *)
12(* *)
13(* one_Axiom: |- !e:'a. ?!fn. fn one = e *)
14(* *)
15(* Translated from hol88. *)
16(* *)
17(* AUTHORS : (c) Tom Melham, University of Cambridge *)
18(* DATE : 87.03.03 *)
19(* TRANSLATOR : Konrad Slind, University of Calgary *)
20(* DATE : September 15, 1991 *)
21(* ===================================================================== *)
22Theory one[bare]
23Ancestors[qualified]
24 sat
25Libs
26 Lib HolKernel Parse boolLib BasicProvers
27
28
29
30local open OpenTheoryMap in
31val ns = ["Data","Unit"]
32val _ = OpenTheory_tyop_name{tyop={Thy="one",Tyop="one"},name=(ns,"unit")}
33val _ = OpenTheory_const_name{const={Thy="one",Name="one"},name=(ns,"()")}
34val _ = OpenTheory_const_name
35 {const={Thy="one",Name="one_CASE"},name=(ns,"case")}
36end
37
38(* ---------------------------------------------------------------------*)
39(* Introduce the new type. *)
40(* The type :one will be represented by the subset {T} of :bool. *)
41(* The predicate defining this subset will be `\b.b`. We must first *)
42(* prove the (trivial) theorem: ?b.(\b.b)b. *)
43(*----------------------------------------------------------------------*)
44
45Theorem EXISTS_ONE_REP[local]:
46 ?b:bool. (\b.b) b
47Proof
48 EXISTS_TAC “T” THEN CONV_TAC BETA_CONV THEN ACCEPT_TAC TRUTH
49QED
50
51(*---------------------------------------------------------------------------*)
52(* Use the type definition mechanism to introduce the new type. *)
53(* The theorem returned is: |- ?rep. TYPE_DEFINITION (\b.b) rep *)
54(*---------------------------------------------------------------------------*)
55
56val one_TY_DEF =
57 REWRITE_RULE [boolTheory.TYPE_DEFINITION_THM]
58 (new_type_definition("one", EXISTS_ONE_REP));
59
60(* ---------------------------------------------------------------------*)
61(* The proof of the `axiom` for type :one follows. *)
62(* ---------------------------------------------------------------------*)
63
64Theorem one_axiom:
65 !f g:'a -> one. f = g
66Proof
67 CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN
68 REPEAT GEN_TAC THEN
69 STRIP_ASSUME_TAC (CONV_RULE (DEPTH_CONV BETA_CONV) one_TY_DEF) THEN
70 FIRST_ASSUM MATCH_MP_TAC THEN
71 EQ_TAC THEN DISCH_THEN (K ALL_TAC) THEN
72 POP_ASSUM (CONV_TAC o REWR_CONV) THENL
73 [EXISTS_TAC (Term`g (x:'a):one`), EXISTS_TAC (Term`f (x:'a):one`)]
74 THEN REFL_TAC
75QED
76
77(*---------------------------------------------------------------------------
78 Define the constant `one` of type one.
79 ---------------------------------------------------------------------------*)
80
81val one_DEF = new_definition ("one_DEF", “one = @x:one.T”);
82
83(*---------------------------------------------------------------------------
84 The following theorem shows that there is only one value of type :one
85 ---------------------------------------------------------------------------*)
86
87Theorem one[simp]:
88 !v:one. v = one
89Proof
90 GEN_TAC THEN
91 ACCEPT_TAC (CONV_RULE (DEPTH_CONV BETA_CONV)
92 (AP_THM
93 (SPECL [Term`\x:'a.(v:one)`,
94 Term`\x:'a.one`] one_axiom) (Term`x:'a`)))
95QED
96
97(*---------------------------------------------------------------------------
98 Prove also the following theorem:
99 ---------------------------------------------------------------------------*)
100
101Theorem one_Axiom:
102 !e:'a. ?!fn. fn one = e
103Proof
104 STRIP_TAC THEN
105 CONV_TAC EXISTS_UNIQUE_CONV THEN
106 STRIP_TAC THENL
107 [EXISTS_TAC “\(x:one).(e:'a)” THEN
108 BETA_TAC THEN REFL_TAC,
109 REPEAT STRIP_TAC THEN
110 CONV_TAC FUN_EQ_CONV THEN
111 ONCE_REWRITE_TAC [one] THEN
112 ASM_REWRITE_TAC[]]
113QED
114
115Theorem one_prim_rec:
116 !e:'a. ?fn. fn one = e
117Proof
118 ACCEPT_TAC
119 (GEN_ALL (CONJUNCT1 (SPEC_ALL
120 (CONV_RULE (DEPTH_CONV EXISTS_UNIQUE_CONV) one_Axiom))))
121QED
122
123(* ----------------------------------------------------------------------
124 Set up the one value to print as (), by analogy with SML's unit
125 ---------------------------------------------------------------------- *)
126
127val _ = add_rule {block_style = (AroundEachPhrase, (PP.CONSISTENT,0)),
128 fixity = Closefix,
129 paren_style = OnlyIfNecessary,
130 pp_elements = [TOK "(", TOK ")"],
131 term_name = "one"};
132
133(*---------------------------------------------------------------------------
134 Doing the above does not affect the pretty-printer because the
135 printer works under the assumption that the only things with
136 pretty-printer rules are applications ("comb"s). In order to get
137 ``one`` to print as ``()``, we overload it to that string. This is
138 solely for its effect on the printing ("outward") direction; the
139 concrete syntax is such that Absyn parsing will never generate the
140 string "()" for later stages of the parsing process to see, and it
141 wouldn't matter if it did.
142 ---------------------------------------------------------------------------*)
143
144Overload "()" = “one”
145Type unit[pp] = ``:one``
146
147Theorem one_induction:
148 !P:one->bool. P one ==> !x. P x
149Proof
150 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC [one] THEN ASM_REWRITE_TAC[]
151QED
152
153Theorem FORALL_ONE[simp]:
154 (!x:unit. P x) <=> P ()
155Proof
156 simpLib.SIMP_TAC boolSimps.bool_ss [EQ_IMP_THM, one_induction]
157QED
158
159(* This (and the next) was in examples/lambda/basics/termSceipt.sml, etc. *)
160Theorem FORALL_ONE_FN :
161 (!uf : one -> 'a. P uf) = !a. P (\u. a)
162Proof
163 SRW_TAC [][EQ_IMP_THM] THEN
164 POP_ASSUM (Q.SPEC_THEN `uf ()` MP_TAC) THEN
165 Q_TAC SUFF_TAC `(\y. uf()) = uf` THEN1 SRW_TAC [][] THEN
166 SRW_TAC [][FUN_EQ_THM, one]
167QED
168
169Theorem EXISTS_ONE_FN :
170 (?f : 'a -> one -> 'b. P f) = (?f : 'a -> 'b. P (\x u. f x))
171Proof
172 SRW_TAC [][EQ_IMP_THM] THENL [
173 Q.EXISTS_TAC `\a. f a ()` THEN SRW_TAC [][] THEN
174 Q_TAC SUFF_TAC `(\x u. f x ()) = f` THEN1 SRW_TAC [][] THEN
175 SRW_TAC [][FUN_EQ_THM, one],
176 Q.EXISTS_TAC `\a u. f a` THEN SRW_TAC [][]
177 ]
178QED
179
180(*---------------------------------------------------------------------------
181 Define the case constant
182 ---------------------------------------------------------------------------*)
183
184val one_case_def = new_definition (
185 "one_case_def",
186 “one_CASE (u:unit) (x:'a) = x”);
187
188Theorem one_case_thm:
189 !x:'a. one_CASE () x = x
190Proof
191 ONCE_REWRITE_TAC [GSYM one] THEN REWRITE_TAC [one_case_def]
192QED
193
194
195val _ = TypeBase.export (
196 TypeBasePure.gen_datatype_info {
197 ax=one_prim_rec, ind=one_induction,
198 case_defs = [one_case_thm]
199 }
200 )
201
202val _ = computeLib.add_persistent_funs ["one_case_def"]