1open HolKernel Parse boolLib boolTheory; 2 3infix THEN THENL; 4 5val _ = new_theory "num"; 6 7val _ = if !Globals.interactive then () else Feedback.emit_WARNING := false; 8 9(*--------------------------------------------------------------------------- 10 * Define successor `SUC_REP:ind->ind` on ind. 11 *---------------------------------------------------------------------------*) 12 13val SUC_REP_DEF = new_specification 14 ("SUC_REP_DEF",["SUC_REP"], boolTheory.INFINITY_AX); 15 16 17val ZERO_REP_EXISTS = prove( 18 Term`?z. !y. ~(z = SUC_REP y)`, 19 Q.X_CHOOSE_THEN `zrep` ASSUME_TAC ((CONV_RULE NOT_FORALL_CONV o 20 REWRITE_RULE [ONTO_THM] o 21 CONJUNCT2) SUC_REP_DEF) THEN 22 POP_ASSUM (ASSUME_TAC o CONV_RULE NOT_EXISTS_CONV) THEN 23 Q.EXISTS_TAC `zrep` THEN POP_ASSUM ACCEPT_TAC); 24 25(*--------------------------------------------------------------------------- 26 * `ZERO_REP:ind` represents `0:num` 27 *---------------------------------------------------------------------------*) 28 29val ZERO_REP_DEF = new_specification 30 ("ZERO_REP_DEF",["ZERO_REP"], ZERO_REP_EXISTS); 31 32 33(*---------------------------------------------------------------------------*) 34(* `IS_NUM:ind->bool` defines the subset of `:ind` used to represent *) 35(* numbers. It is the smallest subset containing `ZERO_REP` and closed *) 36(* under `SUC_REP`. *) 37(*---------------------------------------------------------------------------*) 38 39val IS_NUM_REP = new_definition("IS_NUM_REP", 40 ���IS_NUM_REP m = 41 !P:ind->bool. (P ZERO_REP /\ (!n. P n ==> P(SUC_REP n))) ==> P m���); 42 43(*--------------------------------------------------------------------------- 44 * Prove that there is a representation in :ind of at least one number. 45 *---------------------------------------------------------------------------*) 46 47val EXISTS_NUM_REP = TAC_PROOF(([],���?n. IS_NUM_REP n���), 48 PURE_REWRITE_TAC [IS_NUM_REP] THEN 49 EXISTS_TAC (���ZERO_REP���) THEN 50 REPEAT STRIP_TAC); 51 52(*--------------------------------------------------------------------------- 53 * Make the type definition. 54 *---------------------------------------------------------------------------*) 55 56val num_TY_DEF = new_type_definition ("num", EXISTS_NUM_REP); 57 58val num_ISO_DEF = define_new_type_bijections 59 {name = "num_ISO_DEF", 60 ABS = "ABS_num", 61 REP = "REP_num", 62 tyax = num_TY_DEF}; 63 64val R_11 = prove_rep_fn_one_one num_ISO_DEF 65and R_ONTO = prove_rep_fn_onto num_ISO_DEF 66and A_11 = prove_abs_fn_one_one num_ISO_DEF 67and A_ONTO = prove_abs_fn_onto num_ISO_DEF; 68 69(*--------------------------------------------------------------------------- 70 * Define ZERO. 71 *---------------------------------------------------------------------------*) 72 73val zero = mk_var("0", mk_thy_type{Tyop="num",Thy="num",Args=[]}); 74 75val ZERO_DEF = new_definition("ZERO_DEF", ���^zero = ABS_num ZERO_REP���); 76 77 78(*--------------------------------------------------------------------------- 79 * Define the successor function on num. 80 *---------------------------------------------------------------------------*) 81 82val SUC_DEF = new_definition("SUC_DEF", 83 ���SUC m = ABS_num(SUC_REP(REP_num m))���); 84 85local open OpenTheoryMap in 86val ns = ["Number","Natural"] 87val _ = OpenTheory_tyop_name{tyop={Thy="num",Tyop="num"},name=(ns,"natural")} 88val _ = OpenTheory_const_name{const={Thy="num",Name="0"},name=(ns,"zero")} 89val _ = OpenTheory_const_name{const={Thy="num",Name="SUC"},name=(ns,"suc")} 90end 91 92(*--------------------------------------------------------------------------- 93 * Prove that IS_NUM_REP ZERO_REP. 94 *---------------------------------------------------------------------------*) 95 96val IS_NUM_REP_ZERO = 97 TAC_PROOF 98 (([], ���IS_NUM_REP ZERO_REP���), 99 REWRITE_TAC [IS_NUM_REP] THEN REPEAT STRIP_TAC); 100 101(*--------------------------------------------------------------------------- 102 * Prove that IS_NUM_REP (SUC_REP x). 103 *---------------------------------------------------------------------------*) 104 105val IS_NUM_SUC_REP = 106 TAC_PROOF 107 (([], ���!i. IS_NUM_REP i ==> IS_NUM_REP (SUC_REP i)���), 108 REWRITE_TAC [IS_NUM_REP] THEN 109 REPEAT STRIP_TAC THEN RES_TAC THEN RES_TAC); 110 111val IS_NUM_REP_SUC_REP = 112 TAC_PROOF 113 (([], ���!n. IS_NUM_REP(SUC_REP(REP_num n))���), 114 GEN_TAC THEN MATCH_MP_TAC IS_NUM_SUC_REP THEN 115 REWRITE_TAC [R_ONTO] THEN 116 EXISTS_TAC (���n:num���) THEN REFL_TAC); 117 118(*--------------------------------------------------------------------------- 119 * |- !x1 x2. (SUC_REP x1 = SUC_REP x2) ==> (x1 = x2) 120 *---------------------------------------------------------------------------*) 121 122val SUC_REP_11 = CONJUNCT1 (REWRITE_RULE [ONE_ONE_THM] SUC_REP_DEF); 123 124(*--------------------------------------------------------------------------- 125 * |- !x. ~(SUC_REP x = ZERO_REP) 126 *---------------------------------------------------------------------------*) 127 128val NOT_SUC_ZERO = GSYM ZERO_REP_DEF; 129 130(*----------------------------------------------------------------------*) 131(* Proof of NOT_SUC : |- !n. ~(SUC n = ZERO) *) 132(* ---------------------------------------------------------------------*) 133 134val NOT_SUC = store_thm("NOT_SUC", 135 ���!n. ~(SUC n = 0)���, 136 PURE_REWRITE_TAC [SUC_DEF,ZERO_DEF] THEN GEN_TAC THEN 137 MP_TAC (SPECL [���SUC_REP(REP_num n)���,���ZERO_REP���] A_11) THEN 138 REWRITE_TAC [IS_NUM_REP_ZERO,IS_NUM_REP_SUC_REP] THEN 139 DISCH_THEN SUBST1_TAC THEN 140 MATCH_ACCEPT_TAC NOT_SUC_ZERO); 141 142(* ---------------------------------------------------------------------*) 143(* Prove that |- !m n. (SUC m = SUC n) ==> (m = n) *) 144(* ---------------------------------------------------------------------*) 145 146val INV_SUC = store_thm("INV_SUC", 147 ���!m n. (SUC m = SUC n) ==> (m = n)���, 148 REPEAT GEN_TAC THEN REWRITE_TAC [SUC_DEF] THEN 149 MP_TAC (SPECL [���SUC_REP(REP_num m)���, 150 ���SUC_REP(REP_num n)���] A_11) THEN 151 REWRITE_TAC [IS_NUM_REP_SUC_REP] THEN DISCH_THEN SUBST1_TAC THEN 152 DISCH_THEN (MP_TAC o MATCH_MP SUC_REP_11) THEN 153 REWRITE_TAC [R_11]); 154 155(* ---------------------------------------------------------------------*) 156(* Prove induction theorem. *) 157(* ---------------------------------------------------------------------*) 158 159val ind_lemma1 = 160 TAC_PROOF 161 (([], ���!P. P ZERO_REP /\ (!i. P i ==> P(SUC_REP i)) 162 ==> 163 !i. IS_NUM_REP i ==> P i���), 164 PURE_ONCE_REWRITE_TAC [IS_NUM_REP] THEN 165 REPEAT STRIP_TAC THEN RES_TAC); 166 167val lemma = 168 TAC_PROOF(([], ���(A ==> (A /\ B)) = (A ==> B)���), 169 ASM_CASES_TAC (���A:bool���) THEN ASM_REWRITE_TAC []); 170 171val ind_lemma2 = TAC_PROOF(([], 172 ���!P. P ZERO_REP /\ (!i. IS_NUM_REP i /\ P i ==> P(SUC_REP i)) 173 ==> 174 !i. IS_NUM_REP i ==> P i���), 175 GEN_TAC THEN STRIP_TAC THEN 176 MP_TAC (SPEC ���\i. IS_NUM_REP i /\ P i��� ind_lemma1) THEN 177 CONV_TAC(DEPTH_CONV BETA_CONV) THEN 178 REWRITE_TAC [lemma] THEN DISCH_THEN MATCH_MP_TAC THEN 179 ASM_REWRITE_TAC [IS_NUM_REP_ZERO] THEN 180 REPEAT STRIP_TAC THEN IMP_RES_TAC IS_NUM_SUC_REP THEN 181 RES_TAC); 182 183val lemma1 = 184 TAC_PROOF 185 (([], ���(!i. IS_NUM_REP i ==> P(ABS_num i)) = (!n. P n)���), 186 EQ_TAC THEN REPEAT STRIP_TAC THENL 187 [STRIP_ASSUME_TAC (SPEC (���n:num���) A_ONTO) THEN 188 RES_TAC THEN ASM_REWRITE_TAC [], 189 POP_ASSUM MP_TAC THEN REWRITE_TAC [R_ONTO] THEN 190 STRIP_GOAL_THEN (STRIP_THM_THEN SUBST1_TAC) THEN 191 ASM_REWRITE_TAC []]); 192 193val INDUCTION = store_thm("INDUCTION", 194 ���!P. P 0 /\ (!n. P n ==> P(SUC n)) ==> !n. P n���, 195 GEN_TAC THEN STRIP_TAC THEN 196 MP_TAC (SPEC ���\i. ((P(ABS_num i)):bool)��� ind_lemma2) THEN 197 CONV_TAC(DEPTH_CONV BETA_CONV) THEN 198 REWRITE_TAC [SYM ZERO_DEF,lemma1] THEN 199 DISCH_THEN MATCH_MP_TAC THEN CONJ_TAC THENL 200 [FIRST_ASSUM ACCEPT_TAC, 201 REWRITE_TAC [R_ONTO] THEN 202 GEN_TAC THEN CONV_TAC ANTE_CONJ_CONV THEN 203 DISCH_THEN (STRIP_THM_THEN SUBST1_TAC) THEN 204 ASM_REWRITE_TAC [num_ISO_DEF,SYM (SPEC_ALL SUC_DEF)]]); 205 206val _ = export_theory(); 207