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(* ===================================================================== *)
22
23
24open Lib HolKernel Parse boolLib BasicProvers
25
26local open satTheory in end
27
28val _ = new_theory "one";
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{const={Thy="one",Name="one_CASE"},name=(ns,"case")}
35end
36
37(* ---------------------------------------------------------------------*)
38(* Introduce the new type.                                              *)
39(* The type :one will be represented by the subset {T} of :bool.        *)
40(* The predicate defining this subset will be `\b.b`.  We must first    *)
41(* prove the (trivial) theorem: ?b.(\b.b)b.                             *)
42(*----------------------------------------------------------------------*)
43
44val EXISTS_ONE_REP = prove
45(���?b:bool. (\b.b) b���,
46 EXISTS_TAC ���T��� THEN CONV_TAC BETA_CONV THEN ACCEPT_TAC TRUTH);
47
48(*---------------------------------------------------------------------------*)
49(* Use the type definition mechanism to introduce the new type.              *)
50(* The theorem returned is:   |- ?rep. TYPE_DEFINITION (\b.b) rep            *)
51(*---------------------------------------------------------------------------*)
52
53val one_TY_DEF =
54 REWRITE_RULE [boolTheory.TYPE_DEFINITION_THM]
55    (new_type_definition("one", EXISTS_ONE_REP));
56
57(* ---------------------------------------------------------------------*)
58(* The proof of the `axiom` for type :one follows.                      *)
59(* ---------------------------------------------------------------------*)
60
61val one_axiom = store_thm("one_axiom",
62  Term`!f g:'a -> one. f = g`,
63    CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN
64    REPEAT GEN_TAC THEN
65    STRIP_ASSUME_TAC (CONV_RULE (DEPTH_CONV BETA_CONV) one_TY_DEF) THEN
66    FIRST_ASSUM MATCH_MP_TAC THEN
67    EQ_TAC THEN DISCH_THEN (K ALL_TAC) THEN
68    POP_ASSUM (CONV_TAC o REWR_CONV) THENL
69    [EXISTS_TAC (Term`g (x:'a):one`), EXISTS_TAC (Term`f (x:'a):one`)]
70    THEN REFL_TAC);
71
72(*---------------------------------------------------------------------------
73    Define the constant `one` of type one.
74 ---------------------------------------------------------------------------*)
75
76val one_DEF = new_definition ("one_DEF", Term`one = @x:one.T`);
77
78(*---------------------------------------------------------------------------
79  The following theorem shows that there is only one value of type :one
80 ---------------------------------------------------------------------------*)
81
82val one = store_thm("one[simp]",
83 Term`!v:one. v = one`,
84 GEN_TAC THEN
85 ACCEPT_TAC (CONV_RULE (DEPTH_CONV BETA_CONV)
86   (AP_THM
87     (SPECL [Term`\x:'a.(v:one)`,
88             Term`\x:'a.one`] one_axiom) (Term`x:'a`))));
89
90(*---------------------------------------------------------------------------
91    Prove also the following theorem:
92 ---------------------------------------------------------------------------*)
93
94val one_Axiom = store_thm("one_Axiom",
95    ���!e:'a. ?!fn. fn one = e���,
96    STRIP_TAC THEN
97    CONV_TAC EXISTS_UNIQUE_CONV THEN
98    STRIP_TAC THENL
99    [EXISTS_TAC ���\(x:one).(e:'a)��� THEN
100     BETA_TAC THEN REFL_TAC,
101     REPEAT STRIP_TAC THEN
102     CONV_TAC FUN_EQ_CONV THEN
103     ONCE_REWRITE_TAC [one] THEN
104     ASM_REWRITE_TAC[]]);
105
106val one_prim_rec = store_thm
107 ("one_prim_rec",
108  Term`!e:'a. ?fn. fn one = e`,
109  ACCEPT_TAC
110    (GEN_ALL (CONJUNCT1 (SPEC_ALL
111      (CONV_RULE (DEPTH_CONV EXISTS_UNIQUE_CONV) one_Axiom)))));
112
113(* ----------------------------------------------------------------------
114    Set up the one value to print as (), by analogy with SML's unit
115   ---------------------------------------------------------------------- *)
116
117val _ = add_rule {block_style = (AroundEachPhrase, (PP.CONSISTENT,0)),
118                  fixity = Closefix,
119                  paren_style = OnlyIfNecessary,
120                  pp_elements = [TOK "(", TOK ")"],
121                  term_name = "one"};
122
123(*---------------------------------------------------------------------------
124     Doing the above does not affect the pretty-printer because the
125     printer works under the assumption that the only things with
126     pretty-printer rules are applications ("comb"s).  In order to get
127     ``one`` to print as ``()``, we overload it to that string.  This is
128     solely for its effect on the printing ("outward") direction; the
129     concrete syntax is such that Absyn parsing will never generate the
130     string "()" for later stages of the parsing process to see, and it
131     wouldn't matter if it did.
132 ---------------------------------------------------------------------------*)
133
134val _ = overload_on ("()", ``one``);
135val _ = type_abbrev_pp("unit",``:one``);
136
137val one_induction = Q.store_thm
138("one_induction",
139 `!P:one->bool. P one ==> !x. P x`,
140 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC [one] THEN ASM_REWRITE_TAC[]);
141
142val FORALL_ONE = store_thm(
143  "FORALL_ONE[simp]",
144  ``(!x:unit. P x) <=> P ()``,
145  simpLib.SIMP_TAC boolSimps.bool_ss [EQ_IMP_THM, one_induction]);
146
147(*---------------------------------------------------------------------------
148    Define the case constant
149 ---------------------------------------------------------------------------*)
150
151val one_case_def = new_definition (
152  "one_case_def",
153  Term`one_CASE (u:unit) (x:'a) = x`);
154
155val one_case_thm = Q.store_thm
156 ("one_case_thm",
157  `!x:'a. one_CASE () x = x`,
158  ONCE_REWRITE_TAC [GSYM one] THEN REWRITE_TAC [one_case_def]);
159
160
161val _ = TypeBase.export (
162      TypeBasePure.gen_datatype_info {
163        ax=one_prim_rec, ind=one_induction,
164        case_defs = [one_case_thm]
165      }
166    )
167
168val _ = computeLib.add_persistent_funs ["one_case_def"]
169
170
171
172val _ = export_theory();
173