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