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