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