1open HolKernel Parse boolLib bossLib finite_mapTheory; 2open recursivefnsTheory; 3open prnlistTheory; 4open primrecfnsTheory; 5open listTheory; 6open arithmeticTheory; 7open numpairTheory; 8open nlistTheory; 9open pred_setTheory; 10open turing_machineTheory; 11open whileTheory 12open logrootTheory; 13 14val _ = new_theory "turing_machine_primeq"; 15 16val DISJ_IMP_EQ = prove( 17 ���((x = y) ��� P ��� (x ��� y ��� P)) ��� 18 (P ��� (x = y) ��� (x ��� y ��� P)) ��� 19 (x ��� y ��� P ��� ((x = y) ��� P)) ��� 20 (P ��� x ��� y ��� ((x = y) ��� P))���, 21 METIS_TAC []); 22val _ = augment_srw_ss [rewrites [DISJ_IMP_EQ]] 23 24val updn_def = Define ` 25 (updn [] = 0) ��� 26 (updn [x] = tri x) ��� 27 (updn [x;y] = if y = 0 then tri x 28 else if y = 1 then tri (x + 2) + 2 29 else if y = 2 then tri x 30 else nB (y = 3) * tri x) ��� 31 (updn [s;actn;tmn] = 32 let tape = (nsnd tmn) in 33 let tl = (nfst tape) in 34 let th = ((nsnd tape) MOD 2) in 35 let tr = ((nsnd tape) DIV 2) in 36 if actn = 0 then (* Write 0 *) 37 s *, (tl *, ((2 * tr))) 38 else if actn = 1 then (* Write 1 *) 39 s *, (tl *, ((2 * tr) + 1 )) 40 else if actn = 2 then (* Move left *) 41 if tl MOD 2 = 1 then 42 s *, (((tl-1) DIV 2) *, ((2 * (th + (2 * tr))) + 1)) 43 else 44 s *, ((tl DIV 2) *, (2 * (( th + (2 * tr))))) 45 else if actn = 3 then (* Move right *) 46 if tr MOD 2 = 1 then 47 s *, ((th + (2 * tl)) *, ((2 * ((tr-1) DIV 2)) + 1)) 48 else 49 s *, ((th + (2 * tl)) *, (2 * (tr DIV 2))) 50 else tmn) ��� 51 (updn (s::actn::tmn::a::b) = updn [s;actn;tmn]) 52`; 53 54val UPDATE_TM_NUM_act0_lem = Q.store_thm ("UPDATE_TM_NUM_act0_lem", 55 `��� s tmn actn. 56 (actn = 0) ==> 57 (updn [s;actn;tmn] = 58 ���UPDATE_ACT_S_TM s (NUM_TO_ACT actn) (FULL_DECODE_TM tmn)���)`, 59 REWRITE_TAC [updn_def] >> rpt strip_tac >> 60 (* actn = 0*) 61 simp[NUM_TO_ACT_def] >> rw[FULL_DECODE_TM_def,FULL_ENCODE_TM_def] 62 >- (rw[UPDATE_ACT_S_TM_def] >> EVAL_TAC) >> 63 rw[ENCODE_TM_TAPE_def] 64 >- (rw[UPDATE_ACT_S_TM_def] >> rw[DECODE_TM_TAPE_def] >> 65 simp[ENCODE_DECODE_thm]) 66 >- (rw[UPDATE_ACT_S_TM_def] >> rw[DECODE_TM_TAPE_def] >> 67 simp[ENCODE_DECODE_thm ] >> 68 `ODD (nsnd (nsnd tmn))` by metis_tac[EVEN_OR_ODD] >> 69 fs[ODD_DIV_2_lem]) >> 70 `(UPDATE_ACT_S_TM s Wr0 71 <|state := nfst tmn; 72 tape_l := FST (DECODE_TM_TAPE (nsnd tmn)); 73 tape_h := FST (SND (DECODE_TM_TAPE (nsnd tmn))); 74 tape_r := SND (SND (DECODE_TM_TAPE (nsnd tmn)))|>).tape_h = Z` 75 by fs[WRITE_0_HEAD_lem] >> 76 rfs[]); 77 78 79val UPDATE_TM_NUM_act1_lem = Q.store_thm ("UPDATE_TM_NUM_act1_lem", 80 `��� s tmn actn. 81 (actn = 1) ==> 82 (updn [s;actn;tmn] = 83 ���UPDATE_ACT_S_TM s (NUM_TO_ACT actn) (FULL_DECODE_TM tmn)���)`, 84 REWRITE_TAC [updn_def] >> rpt strip_tac >> 85 simp[NUM_TO_ACT_def] >> 86 rw[FULL_DECODE_TM_def] >> rw[FULL_ENCODE_TM_def] 87 >- (rw[UPDATE_ACT_S_TM_def] >> EVAL_TAC) >> 88 rw[ENCODE_TM_TAPE_def] 89 >- (rw[UPDATE_ACT_S_TM_def] >> rw[DECODE_TM_TAPE_def] >> 90 simp[ENCODE_DECODE_thm]) 91 >- (`(UPDATE_ACT_S_TM s Wr1 92 <|state := nfst tmn; 93 tape_l := FST (DECODE_TM_TAPE (nsnd tmn)); 94 tape_h := FST (SND (DECODE_TM_TAPE (nsnd tmn))); 95 tape_r := SND (SND (DECODE_TM_TAPE (nsnd tmn)))|>).tape_h = O` 96 by fs[WRITE_1_HEAD_lem] >> `O=Z` by fs[] >> fs[]) 97 >- (rw[UPDATE_ACT_S_TM_def] >> rw[DECODE_TM_TAPE_def] >> 98 simp[ENCODE_DECODE_thm ]) >> 99 rw[UPDATE_ACT_S_TM_def] >> rw[DECODE_TM_TAPE_def] >> 100 simp[ENCODE_DECODE_thm]); 101 102val UPDATE_TM_NUM_act2_lem = Q.store_thm ("UPDATE_TM_NUM_act2_lem", 103 `��� s tmn actn. 104 (actn = 2) ==> 105 (updn [s;actn;tmn] = 106 ���UPDATE_ACT_S_TM s (NUM_TO_ACT actn) (FULL_DECODE_TM tmn)���)`, 107 REWRITE_TAC [updn_def] >> rpt strip_tac >> 108 simp[NUM_TO_ACT_def, FULL_DECODE_TM_def, FULL_ENCODE_TM_def, 109 UPDATE_ACT_S_TM_def] >> 110 rw[] 111 >- (fs[]) 112 >- (`~EVEN (nfst (nsnd tmn))` by metis_tac[MOD_2, DECIDE ``0n <> 1``] >> 113 `ODD (nfst (nsnd tmn))` by metis_tac[EVEN_OR_ODD] >> 114 simp[ENCODE_TM_TAPE_def, ODD_TL_DECODE_lem, ENCODE_DECODE_thm] >> 115 rw[ENCODE_def, ENCODE_DECODE_thm,DECODE_TM_TAPE_def] >> rfs[ODD_HD_DECODE] 116 >- metis_tac[MOD_2] 117 >- (rw[MOD_2] >> metis_tac[ODD_DIV_2_lem, EVEN_OR_ODD])) 118 >- (simp[ENCODE_TM_TAPE_def, ODD_TL_DECODE_lem, ENCODE_DECODE_thm] >> 119 rw[ENCODE_def,DECODE_TM_TAPE_def,ENCODE_DECODE_thm,MOD_2] >> 120 metis_tac[ODD_DIV_2_lem, EVEN_OR_ODD]) 121 >- (`EVEN (nfst (nsnd tmn))` by metis_tac[MOD_2, DECIDE ``0n <> 1``] >> 122 `~ODD (nfst (nsnd tmn))` by metis_tac[EVEN_AND_ODD] >> 123 simp[ENCODE_TM_TAPE_def, EVEN_TL_DECODE_lem, ENCODE_DECODE_thm] >> 124 rw[ENCODE_def,DECODE_TM_TAPE_def, ENCODE_DECODE_thm] >> 125 rfs[EVEN_HD_DECODE] 126 >- simp[MOD_2] 127 >- (rw[MOD_2] >> metis_tac[ODD_DIV_2_lem, EVEN_OR_ODD])) 128 ); 129 130val UPDATE_TM_NUM_act3_lem = Q.store_thm ("UPDATE_TM_NUM_act3_lem", 131 `��� s tmn actn. 132 (actn = 3) ==> 133 (updn [s;actn;tmn] = 134 ���UPDATE_ACT_S_TM s (NUM_TO_ACT actn) (FULL_DECODE_TM tmn)���)`, 135 REWRITE_TAC [updn_def] >> rpt strip_tac >> 136 simp[NUM_TO_ACT_def, FULL_DECODE_TM_def, FULL_ENCODE_TM_def, 137 UPDATE_ACT_S_TM_def] >> 138 rw[] 139 >- (fs[SND_SND_DECODE_TM_TAPE]) 140 >- (simp[ENCODE_TM_TAPE_def, ENCODE_DECODE_thm] >> 141 `~EVEN (nsnd (nsnd tmn) DIV 2)` by metis_tac[MOD_2, DECIDE ``0n <> 1``] >> 142 `ODD (nsnd (nsnd tmn) DIV 2)` by metis_tac[EVEN_OR_ODD] >> 143 rfs[SND_SND_DECODE_TM_TAPE] >> simp[ENCODE_def] >> 144 fs[ODD_TL_DECODE_lem,ENCODE_DECODE_thm] >> 145 `HD (DECODE (nsnd (nsnd tmn) DIV 2)) = O` by fs[ODD_HD_DECODE] >> 146 simp[] >> rw[ENCODE_def,DECODE_TM_TAPE_def,ENCODE_DECODE_thm,MOD_2]) 147 >- (simp[ENCODE_TM_TAPE_def, ENCODE_DECODE_thm] >> 148 `EVEN (nsnd (nsnd tmn) DIV 2)` by metis_tac[MOD_2, DECIDE ``0n <> 1``] >> 149 `~ODD (nsnd (nsnd tmn) DIV 2)` by metis_tac[EVEN_AND_ODD] >> 150 rfs[SND_SND_DECODE_TM_TAPE] >> 151 rw[ENCODE_def,DECODE_TM_TAPE_def, ENCODE_DECODE_thm,MOD_2] ) 152 >- (simp[ENCODE_TM_TAPE_def, ENCODE_DECODE_thm] >> 153 `EVEN (nsnd (nsnd tmn) DIV 2)` by metis_tac[MOD_2, DECIDE ``0n <> 1``] >> 154 fs[SND_SND_DECODE_TM_TAPE,EVEN_HD_DECODE] >> 155 rw[ENCODE_def,DECODE_TM_TAPE_def, ENCODE_DECODE_thm,MOD_2] >> 156 fs[EVEN_TL_DECODE_lem,ENCODE_DECODE_thm]) 157 ); 158 159val UPDATE_TM_NUM_thm = Q.store_thm ("UPDATE_TM_NUM_thm", 160 `��� s tmn actn. 161 actn < 4 ==> 162 (updn [s;actn;tmn] = 163 ���UPDATE_ACT_S_TM s (NUM_TO_ACT actn) (FULL_DECODE_TM tmn)���)`, 164 rpt strip_tac >> 165 `(actn = 0) ��� (actn = 1) ��� (actn = 2) ��� (actn = 3)` by simp[] 166 >- (* actn = 0*) 167 fs[UPDATE_TM_NUM_act0_lem] 168 >- (* actn = 1*) 169 fs[UPDATE_TM_NUM_act1_lem] 170 >- (* actn = 2*) 171 fs[UPDATE_TM_NUM_act2_lem] 172 >- (* actn = 3*) 173 fs[UPDATE_TM_NUM_act3_lem]); 174 175val pr3_def = Define` 176 (pr3 f [] = f 0 0 0 : num) ��� 177 (pr3 f [x:num] = f x 0 0) ��� 178 (pr3 f [x;y] = f x y 0) ��� 179 (pr3 f (x::y::z::t) = f x y z) 180`; 181 182val GENLIST1 = prove(``GENLIST f 1 = [f 0]``, 183 SIMP_TAC bool_ss [ONE, GENLIST, SNOC]); 184 185val GENLIST2 = prove( 186``GENLIST f 2 = [f 0; f 1]``, 187SIMP_TAC bool_ss [TWO, ONE, GENLIST, SNOC]); 188 189val GENLIST3 = prove( 190``GENLIST f 3 = [f 0; f 1; f 2]``, 191EVAL_TAC ); 192 193val ternary_primrec_eq = store_thm("ternary_primrec_eq", 194 ``primrec f 3 ��� (���n m p. f [n; m; p] = g n m p) ��� (f = pr3 g)``, 195 SRW_TAC [][] >> SIMP_TAC (srw_ss()) [FUN_EQ_THM] >> 196 Q.X_GEN_TAC `l` >> 197 `(l = []) ��� ���n ns. l = n :: ns` by (Cases_on `l` >> SRW_TAC [][]) THENL [ 198 SRW_TAC [][] >> 199 `f [] = f (GENLIST (K 0) 3)` by METIS_TAC [primrec_nil] >> 200 SRW_TAC [][GENLIST3,pr3_def], 201 202 `(ns = []) ��� ���m ms. ns = m::ms` by (Cases_on `ns` THEN SRW_TAC [][]) >> 203 SRW_TAC [][] THENL [ 204 IMP_RES_THEN (Q.SPEC_THEN `[n]` MP_TAC) primrec_short >> 205 SRW_TAC [][GENLIST1] >> EVAL_TAC, 206 `(ms = []) ��� ���p ps. ms = p::ps` by (Cases_on `ms` THEN SRW_TAC [][]) >| [ 207 fs[pr3_def] >> 208 `f [n;m] = f ([n;m] ++ GENLIST (K 0) (3 - LENGTH [n;m]))` 209 by fs[primrec_short] >> 210 `GENLIST (K 0) (3 - LENGTH [n;m]) = [0]` by EVAL_TAC >> rfs[], 211 IMP_RES_THEN (Q.SPEC_THEN `(n::m::p::ps)` MP_TAC) 212 primrec_arg_too_long >> 213 SRW_TAC [ARITH_ss][] >> fs[pr3_def] 214 ] 215 ] 216 ]); 217 218val primrec_pr3 = store_thm( 219 "primrec_pr3", 220``(���g. primrec g 3 ��� (���m n p. g [m; n; p] = f m n p)) ��� primrec (pr3 f) 3``, 221METIS_TAC [ternary_primrec_eq]); 222 223val MULT2_def = Define `MULT2 x = 2*x`; 224 225val pr_pr_up_case1_def = Define` 226 pr_pr_up_case1 = 227 Cn (pr2 $*,) [ proj 0;Cn (pr2 $*,) [proj 2;Cn (pr1 MULT2) [proj 4]] ] 228`; 229 230val pr_up_case1_thm = Q.store_thm("pr_up_case1_thm", 231 `��� x. 232 (proj 0 x) *, (proj 2 x) *, (2 * (proj 4 x)) = 233 Cn (pr2 $*,) [ proj 0;Cn (pr2 $*,) [proj 2;Cn (pr1 MULT2) [proj 4]] ] x`, 234 strip_tac >> rfs[MULT2_def] ); 235 236val pr_pr_up_case2_def = Define` 237 pr_pr_up_case2 = 238 Cn (pr2 $*,) [ proj 0; 239 Cn (pr2 $*,) [proj 2;Cn (succ) [Cn (pr1 MULT2) [proj 4]] ] ] 240`; 241 242val pr_pr_up_case3_def = Define`pr_pr_up_case3 = 243 Cn (pr2 $*,) [ proj 0;Cn (pr2 $*,) [Cn (pr1 DIV2) [Cn (pr1 PRE) [proj 2]]; 244 Cn (succ) [Cn (pr1 MULT2) [Cn (pr2 (+)) [proj 3; Cn (pr1 MULT2) [proj 4]]]] ] ] `; 245 246val pr_pr_up_case4_def = Define`pr_pr_up_case4 = 247 Cn (pr2 $*,) [ proj 0;Cn (pr2 $*,) [Cn (pr1 DIV2) [proj 2]; 248 Cn (pr1 MULT2) [Cn (pr2 (+)) [proj 3; Cn (pr1 MULT2) [proj 4]]] ] ] `; 249 250val pr_pr_up_case5_def = Define`pr_pr_up_case5 = 251 Cn (pr2 $*,) [ proj 0;Cn (pr2 $*,) [Cn (pr2 (+)) [proj 3;Cn (pr1 MULT2) [proj 2]]; 252 Cn (succ) [Cn (pr1 MULT2) [Cn (pr1 DIV2) [Cn (pr1 PRE) [proj 4]]]] ] ] `; 253 254val pr_pr_up_case6_def = Define`pr_pr_up_case6 = 255 Cn (pr2 $*,) [ proj 0;Cn (pr2 $*,) [Cn (pr2 (+)) [proj 3;Cn (pr1 MULT2) [proj 2]]; 256 Cn (pr1 MULT2) [Cn (pr1 DIV2) [proj 4]]] ] `; 257 258val pr_pr_up_case7_def = Define`pr_pr_up_case7 = 259 proj 5 `; 260 261 262val _ = overload_on ("onef", ``K 1 : num list -> num``) 263 264val _ = overload_on ("twof", ``K 2 : num list -> num``) 265 266val _ = overload_on ("threef", ``K 3 : num list -> num``) 267 268val _ = overload_on ("fourf", ``K 4 : num list -> num``) 269 270val nB_cond_elim = prove( 271``nB p * x + nB (~p) * y = if p then x else y``, 272Cases_on `p` >> simp[]); 273 274 275val updn_zero_thm = Q.store_thm ("updn_zero_thm", 276`��� x. updn [x;0] = updn [x]`, 277strip_tac >> fs[updn_def]) 278 279val updn_two_lem_1 = Q.store_thm("updn_two_lem_1", 280`��� x. ((x <> []) ��� (LENGTH x <= 2)) ==> ( ��� h. (x = [h])) ��� (��� h t. (x = [h;t]))`, 281rpt strip_tac >> Cases_on `x` >- fs[] >> Cases_on `t` >- fs[] >> Cases_on `t'` >- fs[] >> rfs[] ); 282 283val updn_two_lem_2 = Q.store_thm("updn_two_lem_2", 284`���x. (LENGTH x = 2) ==> (���h t. (x = [h;t]))`, 285rpt strip_tac >> Cases_on `x` >> fs[] >> Cases_on `t` >> fs[]) 286 287val updn_three_lem_1 = Q.store_thm("updn_three_lem_1", 288 `��� x. ��(LENGTH x <= 2) ==> 289 (��� a b c. (x = [a;b;c]) ) ��� (��� a b c d e. x = a::b::c::d::e)`, 290 rpt strip_tac >> Cases_on `x` >- fs[] >> 291 rename [���LENGTH (h::t)���] >> Cases_on ���t��� >> fs[] >> 292 rename [���SUC (LENGTH l)���] >> Cases_on ���l��� >> fs[] >> 293 metis_tac[list_CASES]); 294 295Theorem prim_pr_rec_updn: 296 updn = 297 Cn 298 (pr_cond (Cn pr_eq [proj 1;zerof]) (pr_pr_up_case1) ( 299 pr_cond (Cn pr_eq [proj 1; onef]) (pr_pr_up_case2) ( 300 pr_cond (Cn pr_eq [proj 1; twof]) ( 301 pr_cond (Cn pr_eq [Cn (pr_mod) [proj 2;twof];onef]) 302 (pr_pr_up_case3) 303 (pr_pr_up_case4) 304 ) ( 305 pr_cond (Cn pr_eq [proj 1;threef]) ( 306 pr_cond (Cn pr_eq [Cn (pr_mod) [proj 4;twof];onef]) 307 (pr_pr_up_case5) 308 (pr_pr_up_case6) 309 ) ( 310 pr_cond (Cn pr_eq [proj 1;fourf]) 311 (pr_pr_up_case7) 312 (pr_pr_up_case7) 313 ) 314 ) 315 ) 316 ) 317 ) 318 [proj 0;proj 1; Cn (pr1 nfst) [Cn (pr1 nsnd) [proj 2]] ; 319 Cn (pr_mod) [Cn (pr1 nsnd) [ Cn (pr1 nsnd) [proj 2]];twof]; 320 Cn (pr1 DIV2) [Cn (pr1 nsnd) [ Cn (pr1 nsnd) [proj 2]]]; proj 2 ] 321Proof 322 rw[Cn_def,FUN_EQ_THM] 323 >> fs[pr_pr_up_case1_def,pr_pr_up_case2_def,pr_pr_up_case3_def, 324 pr_pr_up_case4_def,pr_pr_up_case5_def,pr_pr_up_case6_def] >> rw[] 325 >- (rw[proj_def,updn_def,updn_zero_thm,updn_three_lem_1] >> fs[] 326 >- EVAL_TAC 327 >- (`(���h. x = [h]) ��� (���h t. x = [h;t])` by simp[updn_two_lem_1] 328 >- (rw[updn_def] >> simp[MULT2_def] >> simp[npair_def]) 329 >- (fs[updn_def,updn_zero_thm] >> simp[MULT2_def] >> 330 simp[npair_def])) 331 >- (`(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))` 332 by simp[updn_three_lem_1] >> 333 fs[updn_def,MULT2_def,DIV2_def]) 334 ) 335 >- (fs[proj_def,updn_def,updn_zero_thm,pr_pr_up_case2_def] >> rw[] >> fs[] 336 >- (`(���h. x = [h]) ��� (���h t. x = [h;t])` by simp[updn_two_lem_1] >> 337 fs[updn_def,updn_zero_thm] >> simp[MULT2_def, npair_def] >> 338 EVAL_TAC >> simp[]) 339 >- (`(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))` 340 by simp[updn_three_lem_1] >> fs[updn_def,MULT2_def,DIV2_def]) 341 ) 342 >- (fs[proj_def,updn_def,updn_zero_thm,pr_pr_up_case3_def] >> rw[] >> fs[] >> 343 `(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))` 344 by simp[updn_three_lem_1] >> fs[updn_def,MULT2_def,DIV2_def]) 345 >- (fs[proj_def,updn_def,updn_zero_thm,pr_pr_up_case4_def] >> rw[] >> fs[] 346 >- (`(���h. x = [h]) ��� (���h t. x = [h;t])` by simp[updn_two_lem_1] >> 347 fs[updn_def,updn_zero_thm] >> simp[MULT2_def] >> simp[npair_def]) 348 >- (`(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))` 349 by simp[updn_three_lem_1] >> fs[updn_def,MULT2_def,DIV2_def]) 350 ) 351 >- (fs[proj_def,updn_def,updn_zero_thm,pr_pr_up_case5_def] >> rw[] >> fs[] >> 352 `(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))` 353 by simp[updn_three_lem_1] >> fs[updn_def,MULT2_def,DIV2_def]) 354 >- (fs[proj_def,updn_def,updn_zero_thm,pr_pr_up_case6_def] >> rw[] >> fs[] 355 >- (`(���h. x = [h]) ��� (���h t. x = [h;t])` by simp[updn_two_lem_1] >> 356 fs[updn_def] >> simp[MULT2_def] >> simp[npair_def]) 357 >- (`(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))` 358 by simp[updn_three_lem_1] >> fs[updn_def,MULT2_def,DIV2_def]) 359 ) 360 >- (fs[proj_def,updn_def,updn_zero_thm,pr_pr_up_case7_def] >> rw[] >> fs[] 361 362 >- (Cases_on ���x = []��� >> fs[] >> 363 `(���h. x = [h]) ��� (���h t. x = [h;t])` by simp[updn_two_lem_1] >> 364 fs[updn_def]) 365 >- (`(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))` 366 by simp[updn_three_lem_1] >> fs[updn_def]) 367 ) 368QED 369 370val primrec_cn = List.nth(CONJUNCTS primrec_rules, 3); 371 372val primrec_pr = List.nth(CONJUNCTS primrec_rules, 4); 373 374val primrec_mult2 = Q.store_thm("primrec_mult2", 375`primrec (pr1 MULT2) 1`, 376MATCH_MP_TAC primrec_pr1 >> 377Q.EXISTS_TAC `Cn (pr2 $*) [proj 0; twof]` >> conj_tac >- 378 SRW_TAC [][primrec_rules, alt_Pr_rule,Pr_thm,Pr_def ] >> 379 SRW_TAC [][primrec_rules, alt_Pr_rule,Pr_thm,Pr_def ] >> rw[MULT2_def]); 380 381val primrec_div2 = Q.store_thm("primrec_div2", 382`primrec (pr1 DIV2) 1`, 383MATCH_MP_TAC primrec_pr1 >> 384Q.EXISTS_TAC `Cn (pr_div) [proj 0; twof]` >> conj_tac >- 385SRW_TAC [][primrec_rules, alt_Pr_rule,Pr_thm,Pr_def,primrec_pr_div ] >> 386SRW_TAC [][primrec_rules, alt_Pr_rule,Pr_thm,Pr_def,primrec_pr_div ] >> rw[DIV2_def]); 387 388val primrec_pr_case1 = Q.store_thm("primrec_pr_case1", 389`primrec pr_pr_up_case1 6`, 390SRW_TAC [][pr_pr_up_case1_def] >> 391rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> rw[primrec_mult2] 392 ); 393 394val primrec_pr_case2 = Q.store_thm("primrec_pr_case2", 395`primrec pr_pr_up_case2 6`, 396SRW_TAC [][pr_pr_up_case2_def] >> 397 rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> rw[primrec_mult2] 398 ); 399 400val primrec_pr_case3 = Q.store_thm("primrec_pr_case3", 401`primrec pr_pr_up_case3 6`, 402SRW_TAC [][pr_pr_up_case3_def] >> 403 rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> 404 rw[primrec_mult2,primrec_div2] ); 405 406val primrec_pr_case4 = Q.store_thm("primrec_pr_case4", 407`primrec pr_pr_up_case4 6`, 408SRW_TAC [][pr_pr_up_case4_def] >> 409 rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> rw[primrec_mult2,primrec_div2] 410 ); 411 412val primrec_pr_case5 = Q.store_thm("primrec_pr_case5", 413`primrec pr_pr_up_case5 6`, 414SRW_TAC [][pr_pr_up_case5_def] >> 415 rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> rw[primrec_mult2,primrec_div2] 416 ); 417 418val primrec_pr_case6 = Q.store_thm("primrec_pr_case6", 419`primrec pr_pr_up_case6 6`, 420SRW_TAC [][pr_pr_up_case6_def] >> 421 rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> rw[primrec_mult2,primrec_div2] 422 ); 423 424val primrec_proj = List.nth(CONJUNCTS primrec_rules, 2); 425 426val primrec_pr_case7 = Q.store_thm("primrec_pr_case7", 427`primrec pr_pr_up_case7 6`, 428SRW_TAC [][pr_pr_up_case7_def] >> 429 `5<6` by fs[] >> SRW_TAC [][primrec_proj] 430 ); 431 432val UPDATE_TM_NUM_PRIMREC = Q.store_thm("UPDATE_TM_NUM_PRIMREC", 433`primrec updn 3`, 434SRW_TAC [][updn_def,primrec_rules,prim_pr_rec_updn] >> SRW_TAC [][pr_cond_def] >> 435 rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) 436 >> fs[primrec_pr_case1,primrec_pr_case2,primrec_pr_case3,primrec_pr_case4, 437 primrec_pr_case5,primrec_pr_case6,primrec_pr_case7,primrec_div2] 438 ); 439 440 441val tmstepf_def = tDefine "tmstepf" ` 442 tmstepf p tmn = 443 case OLEAST n. (nfst n, CELL_NUM (nsnd n)) ��� FDOM p ��� nfst n<>0 of 444 NONE => 0 *, nsnd tmn 445 | SOME n => let s = nfst n ; 446 sym = CELL_NUM (nsnd n) ; 447 (s',actn) = p ' (s,sym) 448 in 449 if nfst n = 0 then tmn 450 else if (nfst tmn = s) ��� 451 ((nsnd (nsnd tmn)) MOD 2 = NUM_CELL sym) 452 then updn [s'; ACT_TO_NUM actn; tmn] 453 else tmstepf (p \\ (s,sym)) tmn 454` 455 (WF_REL_TAC `measure (CARD o FDOM o FST)` >> simp[OLEAST_EQ_SOME] >> 456 metis_tac[MEMBER_CARD]); 457 458val HEAD_DECODE_ENCDOE_EQ = Q.store_thm("HEAD_DECODE_ENCDOE_EQ[simp]", 459`(HD (DECODE (ENCODE t)) = Z) ==> (HD t = Z)`, 460Cases_on `t` 461 >- (EVAL_TAC) 462 >- (fs[ENCODE_def,DECODE_def] >> Cases_on `h` >> fs[] >> `2* ENCODE t' +1 = SUC (2* ENCODE t')` by fs[] >> rw[DECODE_def] >> rfs[ODD_DOUBLE] ) ) 463 464val ENCODE_ONE_TL_ZERO = Q.store_thm("ENCODE_ONE_TL_ZERO", 465`(ENCODE t = 1) ==> (ENCODE (TL t) = 0)`, 466Cases_on ` t` >> fs[] >- (EVAL_TAC) >- (fs[ENCODE_def] >> Cases_on `h` >> fs[]) ) 467 468 469val HD_DECODE_DOUBLED = Q.store_thm("HD_DECODE_DOUBLED[simp]", 470`(x <> 0) ==> (HD (DECODE (2 * x)) = Z)`, 471Cases_on `x` >> fs[] >> `2*(SUC n) =SUC (SUC (2* n))` by simp[] >> simp[DECODE_def,ODD,ODD_MULT] ) 472 473 474val TL_DECODE_DOUBLED = Q.store_thm("TL_DECODE_DOUBLED[simp]", 475`(x <> 0) ==> (TL (DECODE (2 * x)) = DECODE x)`, 476Cases_on `x` >> fs[] >> `2 * (SUC n) =SUC (SUC (2* n))` by simp[] >> 477 simp[DECODE_def,SimpLHS,ODD,ODD_MULT] >> pop_assum(SUBST1_TAC o SYM) >> fs[TWO_TIMES_DIV_TWO_thm] ) 478 479val HD_DECODE_DOUBLED = Q.store_thm("HD_DECODE_DOUBLED[simp]", 480`(HD (DECODE (2 * x + 1)) = O)`, 481simp[GSYM(ADD1),DECODE_def,ODD,ODD_MULT] ) 482 483 484val TL_DECODE_DOUBLED = Q.store_thm("TL_DECODE_DOUBLED[simp]", 485`(TL (DECODE (2 * x + 1)) = DECODE x)`, 486simp[GSYM(ADD1),DECODE_def,ODD,ODD_MULT] ) 487 488 489 490val ENCODED_DECODED_ENCODED_UPDATE_TM_thm = Q.store_thm( 491 "ENCODED_DECODED_ENCODED_UPDATE_TM_thm", 492 `���UPDATE_ACT_S_TM (FST (p ' (tm.state,tm.tape_h))) 493 (SND (p ' (tm.state,tm.tape_h))) (FULL_DECODE_TM ���tm���) ��� = 494 ���(UPDATE_ACT_S_TM (FST (p ' (tm.state,tm.tape_h))) 495 (SND (p ' (tm.state,tm.tape_h))) (tm) )���`, 496 fs[FULL_DECODE_TM_def,FULL_ENCODE_TM_def] >> rw[] 497 >- (fs[ENCODE_TM_TAPE_def] >> Cases_on `tm.tape_h` 498 >- (fs[SND_SND_DECODE_TM_TAPE_FULL] >> 499 `EVEN (2 * ENCODE tm.tape_r)` by fs[EVEN_DOUBLE] >> 500 fs[FST_SND_DECODE_TM_TAPE_FULL] >> fs[UPDATE_ACT_S_TM_def] >> 501 Cases_on `SND (p ' (tm.state,Z))` >> fs[] 502 >- (Cases_on `tm.tape_l = []` >> fs[ENCODE_def] >> 503 Cases_on `ENCODE tm.tape_l = 0` >> fs[] ) 504 >- (Cases_on `tm.tape_r = []` >> fs[ENCODE_def] >> 505 Cases_on `2* ENCODE tm.tape_r DIV 2 = 0` >> fs[])) 506 >- (fs[SND_SND_DECODE_TM_TAPE_FULL] >> 507 fs[UPDATE_ACT_S_TM_def] >> 508 Cases_on `SND (p ' (tm.state,O))` >> fs[] 509 >- (Cases_on `tm.tape_l = []` >> fs[ENCODE_def] >> 510 Cases_on `ENCODE tm.tape_l = 0` >> fs[]) 511 >- (Cases_on `tm.tape_r = []` >> fs[ENCODE_def] >> 512 Cases_on `(2 * ENCODE tm.tape_r + 1) DIV 2 = 0` >> fs[]))) 513 >- (fs[UPDATE_ACT_S_TM_def] >> 514 Cases_on `SND (p ' (tm.state,tm.tape_h))` >> fs[] 515 >- (simp[ENCODE_TM_TAPE_def,ENCODE_DECODE_thm] >> rw[] ) 516 >- (simp[ENCODE_TM_TAPE_def,ENCODE_DECODE_thm] >> rw[]) 517 >- (Cases_on `tm.tape_l` >> fs[ENCODE_def] 518 >- (simp[ENCODE_TM_TAPE_def,ENCODE_DECODE_thm]) 519 >- (Cases_on `h` >> simp[] 520 >- (rw[] 521 >- (simp[ENCODE_TM_TAPE_def,ENCODE_def]) 522 >- (simp[ENCODE_TM_TAPE_def,ENCODE_def] >> 523 simp[ENCODE_DECODE_thm] )) 524 >- (simp[ENCODE_TM_TAPE_def,ENCODE_DECODE_thm] ) ) ) 525 >- (Cases_on `tm.tape_r` >> fs[ENCODE_def] 526 >- (simp[ENCODE_TM_TAPE_def,ENCODE_DECODE_thm]) 527 >- (Cases_on `h` >> simp[] 528 >- (rw[] 529 >- (simp[ENCODE_TM_TAPE_def,ENCODE_def]) 530 >- (simp[ENCODE_TM_TAPE_def,ENCODE_def] >> 531 simp[ENCODE_DECODE_thm] )) 532 >- (simp[ENCODE_TM_TAPE_def,ENCODE_DECODE_thm] ) ) )) 533); 534 535 536val UPDATE_TM_NUM_corol = Q.store_thm("UPDATE_TM_NUM_corol", 537`���s' tmn actn'. (updn [s'; ACT_TO_NUM actn'; tmn] = 538 ���UPDATE_ACT_S_TM s' actn' (FULL_DECODE_TM tmn)���)`, 539fs[ACT_TO_NUM_LESS_4,UPDATE_TM_NUM_thm]) 540 541val lemma_11 = 542 UPDATE_TM_ARB_Q |> Q.INST[`q` |-> `tm.prog` ] 543 |> SIMP_RULE(srw_ss())[tm_with_prog] 544 545val updn_UPDATE_TAPE = Q.store_thm("updn_UPDATE_TAPE", 546 `(tm.state, tm.tape_h) ��� FDOM p ��� tm.state <> 0 ==> 547 ((��(s',actn). updn [s'; ACT_TO_NUM actn; ���tm���]) (p ' (tm.state,tm.tape_h)) = 548 ���UPDATE_TAPE (tm with prog := p)���)`, 549 rw[] >> `ACT_TO_NUM actn < 4` by fs[ACT_TO_NUM_LESS_4] >> 550 qabbrev_tac `ptm = tm with prog := p` >> 551 `(tm.state,tm.tape_h) ��� FDOM ptm.prog` by fs[Abbr`ptm`] >> 552 `(ptm.state,ptm.tape_h) ��� FDOM ptm.prog` by fs[Abbr`ptm`] >> 553 `ptm.state <> 0` by simp[Abbr`ptm`] >> 554 `(UPDATE_ACT_S_TM 555 (FST (ptm.prog ' (ptm.state, ptm.tape_h))) 556 (SND (ptm.prog ' (ptm.state,ptm.tape_h))) 557 ptm = 558 UPDATE_TAPE ptm)` 559 by fs[UPDATE_TAPE_ACT_STATE_TM_thm] >> rfs[] >> 560 `ACT_TO_NUM (SND (ptm.prog ' (tm.state,tm.tape_h))) < 4` 561 by fs[ACT_TO_NUM_LESS_4] >> 562 `(updn [FST (ptm.prog ' (tm.state,tm.tape_h)); 563 ACT_TO_NUM (SND (p ' (tm.state,tm.tape_h))); 564 ���tm���] = 565 ���UPDATE_ACT_S_TM (FST (ptm.prog ' (tm.state,tm.tape_h))) 566 (SND (p ' (tm.state,tm.tape_h))) 567 (FULL_DECODE_TM ���tm���)���)` 568 by fs[UPDATE_TM_NUM_corol] >> 569 simp[pairTheory.UNCURRY] >> fs[Abbr`ptm`] >> 570 simp[ENCODED_DECODED_ENCODED_UPDATE_TM_thm,lemma_11]); 571 572val CELL_NUM_NUM_CELL = Q.store_thm("CELL_NUM_NUM_CELL[simp]", 573`CELL_NUM (NUM_CELL x) = x`, 574Cases_on `x` >> fs[CELL_NUM_def]) 575 576val CELL_NUM_NUM_CELL_RW = Q.store_thm("CELL_NUM_NUM_CELL_RW", 577 `(NUM_CELL (CELL_NUM c) = c) ==> (NUM_CELL h <> c) ==> (h <> CELL_NUM c)`, 578 strip_tac >> strip_tac >> metis_tac[] ) 579 580val NUM_STATE_CELL_NUM_LEM = Q.store_thm("NUM_STATE_CELL_NUM_LEM", 581 `(NUM_CELL (CELL_NUM c) = c) ��� ((tm.state = n) ��� NUM_CELL tm.tape_h ��� c) ��� 582 (tm.state = n) ��� tm.tape_h ��� CELL_NUM c`, 583 strip_tac >> strip_tac >> strip_tac >> 584 fs[CELL_NUM_NUM_CELL_RW]); 585 586val EQ_SND_P_LESS = Q.store_thm("EQ_SND_P_LESS", 587 `a <> b ==> ((p \\ a) ' b = p ' b)`, 588 simp[DOMSUB_FAPPLY_THM]); 589 590val UPDATE_W_PROG_NIN_TM = Q.store_thm("UPDATE_W_PROG_NIN_TM", 591 `((NUM_CELL (CELL_NUM c) = c) ��� ((n,CELL_NUM c) ��� FDOM p) ��� 592 n <> 0 ��� ((tm.state = n) ��� NUM_CELL tm.tape_h ��� c)) 593 ��� 594 (���UPDATE_TAPE (tm with prog := p \\ (n,CELL_NUM c)) ��� = 595 ���UPDATE_TAPE (tm with prog := p)���)`, 596 simp[FULL_ENCODE_TM_def] >> rw[] >> 597 `(tm.state = n) ��� tm.tape_h ��� CELL_NUM c` 598 by metis_tac[NUM_STATE_CELL_NUM_LEM] >> 599 `(tm.state,tm.tape_h) <> (n,CELL_NUM c)` 600 by (simp[] >> metis_tac[]) >> 601 rw[] >> 602 Cases_on `(tm.state,tm.tape_h) ��� FDOM p` >> 603 rw[UPDATE_TAPE_def] >> fs[EQ_SND_P_LESS] >> 604 Cases_on `SND (p ' (tm.state,tm.tape_h))` >> fs[] >> 605 Cases_on `tm.tape_l = []` >> fs[] >> 606 Cases_on `tm.tape_r = []` >> fs[ENCODE_TM_TAPE_def]); 607 608val tm_eq_tm_with_state = Q.store_thm("tm_eq_tm_with_state", 609 `(tm.state = a) ==> (tm = tm with state := a)`, 610 strip_tac >> `(tm with state := a).state = a` by fs[] >> 611 rfs[TM_component_equality]) 612 613val effempty_def = Define` 614 effempty p <=> FDOM p ��� {(a,b) | (a,b) | a = 0} 615`; 616 617val containment_lem_nzero = Q.store_thm("containment_lem_nzero", 618 `((OLEAST n. (nfst n,CELL_NUM (nsnd n)) ��� FDOM p ��� nfst n <>0) = NONE) 619 ��� 620 effempty p`, 621 rw[effempty_def] >> eq_tac >> simp[] >> csimp[fmap_EXT] >> 622 simp[pairTheory.FORALL_PROD] >> strip_tac 623 >- (rw[SUBSET_DEF] >> rename[`sc ��� FDOM p`] >> 624 `���s c. sc = (s,c)` by simp[pairTheory.pair_CASES]>> 625 rw[] >> first_x_assum (qspec_then `s *, (NUM_CELL c)` mp_tac) >>simp[]) 626 >- (rpt strip_tac >> fs[SUBSET_DEF] >> res_tac >> fs[])); 627 628val effempty_no_update = Q.store_thm("effempty_no_update", 629 `effempty tm.prog ==> (UPDATE_TAPE tm = tm with state := 0)`, 630 rw[effempty_def]>> simp[UPDATE_TAPE_def]>> 631 Cases_on `(tm.state,tm.tape_h) ��� FDOM tm.prog`>> simp[]>> 632 fs[SUBSET_DEF] >> res_tac >> fs[]); 633 634val CELL_NUM_LEM1 = Q.store_thm("CELL_NUM_LEM1", 635 `(���n'. n' < n ��� c ��� nfst n' ��� 0 ��� 636 (nfst n',CELL_NUM (nsnd n')) ��� FDOM p) ��� 637 (n,CELL_NUM c) ��� FDOM p ��� n<>0 638 ==> 639 (c=0) ��� (c=1)`, 640 spose_not_then strip_assume_tac >> Cases_on `CELL_NUM c` 641 >- (`0<c` by simp[] >> 642 metis_tac[nfst_npair,nsnd_npair,npair2_lt,CELL_NUM_def]) 643 >- (`1<c` by simp[] >> 644 metis_tac[nfst_npair,nsnd_npair,npair2_lt,CELL_NUM_def])); 645 646val FULL_ENCODE_IGNORES_PROGS' = 647 FULL_ENCODE_IGNORES_PROGS |> SYM |> Q.INST[`p`|->`ARB` ] 648 649val tmstepf_update_equiv = Q.store_thm("tmstepf_update_equiv", 650 `���p n tm. 651 (n = ���tm���) ==> 652 (tmstepf p n = FULL_ENCODE_TM (UPDATE_TAPE (tm with prog := p) ))`, 653 ho_match_mp_tac (theorem"tmstepf_ind") >> simp[OLEAST_EQ_SOME] >> rw[] >> 654 pop_assum (assume_tac o CONV_RULE (HO_REWR_CONV npair_lem)) >> fs[] >> 655 simp[Once tmstepf_def] >> 656 Cases_on ` 657 OLEAST n. (nfst n,CELL_NUM (nsnd n)) ��� FDOM p ��� nfst n ��� 0 658 ` 659 >- (simp[] >> fs[containment_lem_nzero,effempty_no_update] >> 660 simp[UPDATE_TAPE_def,FULL_ENCODE_TM_def, ENCODE_TM_TAPE_def]) >> 661 fs[OLEAST_EQ_SOME] >> rename [`nfst nc ��� 0`] >> simp[] >> 662 `���n c. nc = n *, c` by metis_tac[npair_cases] >> 663 fs[UPDATE_TAPE_ACT_STATE_TM_thm,NUM_TO_CELL_TO_NUM, 664 FULL_ENCODE_TM_STATE] >> 665 `NUM_CELL (CELL_NUM c) = c` 666 by metis_tac[CELL_NUM_LEM1,NUM_TO_CELL_TO_NUM] >> simp[] >> fs[] >> 667 rfs[NUM_CELL_INJ] >> 668 Cases_on `(tm.state = n) ��� (NUM_CELL tm.tape_h = c)` >> rw[] 669 >- (fs[updn_UPDATE_TAPE]) >> 670 `��� a s. p ' (n,CELL_NUM c) = (s,a)` by metis_tac[pairTheory.pair_CASES] >> 671 first_x_assum(qspecl_then[`n`,`c`,`s`,`a`] mp_tac) >> simp[] >> 672 rw[CELL_NUM_NUM_CELL_RW] >> simp[UPDATE_TAPE_def] >> 673 Cases_on `(tm.state,tm.tape_h) ��� FDOM p` >> simp[] 674 >- (Cases_on `tm.state = 0` >>simp[] 675 >- simp_tac bool_ss [FULL_ENCODE_IGNORES_PROGS, GSYM TM_fupdcanon] >> 676 reverse COND_CASES_TAC >- fs[] >> 677 simp[DOMSUB_FAPPLY_THM ] >> 678 `��((n = tm.state) ��� (CELL_NUM c = tm.tape_h))` 679 by fs[CELL_NUM_def,NUM_CELL_def] >> simp[] >> 680 Cases_on `SND (p ' (tm.state,tm.tape_h))` >> rw[] >> 681 ONCE_REWRITE_TAC [FULL_ENCODE_IGNORES_PROGS'] >> 682 CONV_TAC (BINOP_CONV (RAND_CONV (SIMP_CONV (srw_ss()) []))) >> 683 simp[]) >> 684 ONCE_REWRITE_TAC [FULL_ENCODE_IGNORES_PROGS'] >> 685 CONV_TAC (BINOP_CONV (RAND_CONV (SIMP_CONV (srw_ss()) []))) >> 686 simp[]); 687 688val primrec_tmstepf_form = Q.store_thm("primrec_tmstepf_form", 689 `���n. 690 (Cn (proj 0) [ 691 pr_cond (Cn (pr2 $* ) [Cn pr_eq [Cn (pr1 nfst) [proj 0] ; 692 Cn (pr1 nfst) [K k] ]; 693 Cn pr_eq [Cn pr_mod [ 694 Cn (pr1 nsnd) [ 695 Cn (pr1 nsnd) [proj 0] 696 ]; 697 twof 698 ]; 699 Cn (pr1 nsnd) [K k] ] ] ) 700 (Cn updn [K snum; K anum ; proj 0] ) 701 (Cn (pr1 (tmstepf q)) [proj 0] ) 702 ]) [n] 703 = 704 (��tmn. if (nfst tmn = nfst k) ��� (nsnd (nsnd tmn) MOD 2 = nsnd k) then 705 updn [snum; anum; tmn] 706 else tmstepf q tmn) n`, 707 rw[Cn_def,FUN_EQ_THM] >> rw[pr_cond_def]); 708 709 710val primrec_of_tmstepf = Q.store_thm("primrec_of_tmstepf", 711 `primrec (pr1 (tmstepf q)) 1 ==> 712 primrec (Cn (proj 0) [ 713 pr_cond (Cn (pr2 $* ) [ 714 Cn pr_eq [Cn (pr1 nfst) [proj 0] ; Cn (pr1 nfst) [K k] ]; 715 Cn pr_eq [ 716 Cn pr_mod [Cn (pr1 nsnd) [Cn (pr1 nsnd) [proj 0]] ;twof]; 717 Cn (pr1 nsnd) [K k] ] ] ) 718 (Cn updn [K snum; K anum ; proj 0] ) 719 (Cn (pr1 (tmstepf q)) [proj 0] ) 720 ]) 1`, 721 strip_tac >> SRW_TAC [][primrec_rules] >> SRW_TAC [][pr_cond_def] >> 722 rpt (MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> 723 fs[UPDATE_TM_NUM_PRIMREC]); 724 725val primrec_tmstepf = Q.store_thm ("primrec_tmstepf", 726 `primrec (pr1 (tmstepf p)) 1`, 727 Induct_on `CARD (FDOM p)` 728 >- (rpt strip_tac >> 729 `FDOM p = {}` by metis_tac[FDOM_FINITE,CARD_EQ_0] >> fs[FDOM_EQ_EMPTY] >> 730 rw[Once tmstepf_def] >> qmatch_abbrev_tac`primrec f 1` >> 731 `f = Cn (pr2 npair) [zerof; Cn (pr1 nsnd) [proj 0]]` suffices_by 732 simp[primrec_rules,primrec_npair,primrec_nsnd] >> 733 simp[Abbr`f`,FUN_EQ_THM] >> Cases >> 734 simp[proj_def,nsnd_def] >> rw[Once tmstepf_def] >> simp[nsnd_def] ) 735 >- (rpt strip_tac >> MATCH_MP_TAC primrec_pr1 >> rw[Once tmstepf_def] >> 736 `(OLEAST n. (nfst n,CELL_NUM (nsnd n)) ��� FDOM p) <> NONE` 737 by (simp[] >> `FDOM p <> {}` by (strip_tac >> fs[]) >> 738 `���a b. (a,b) IN FDOM p` 739 by metis_tac[SET_CASES,pairTheory.pair_CASES,IN_INSERT] >> 740 qexists_tac`a *, NUM_CELL b` >> simp[]) >> 741 Cases_on ` 742 (OLEAST n. (nfst n,CELL_NUM (nsnd n)) ��� FDOM p ��� nfst n ��� 0)` >> 743 fs[] 744 >- (qexists_tac `Cn (pr2 npair) [zerof; Cn (pr1 nsnd) [proj 0]]` >> 745 conj_tac 746 >- simp[primrec_rules,primrec_npair,primrec_nsnd] 747 >- simp[proj_def,nsnd_def]) >> 748 fs[OLEAST_EQ_SOME] >> rename [���nfst k <> 0���] >> 749 `��� s a. (p ' (nfst k,CELL_NUM (nsnd k))) = (s,a)` 750 by metis_tac[pairTheory.pair_CASES] >> simp[] >> 751 `CARD (FDOM (p \\ (nfst k,CELL_NUM (nsnd k)))) = v` by fs[] >> 752 qabbrev_tac`q = p \\ (nfst k,CELL_NUM (nsnd k))` >> 753 `primrec (pr1 (tmstepf q)) 1` by fs[] >> 754 `NUM_CELL (CELL_NUM (nsnd k)) = nsnd k` 755 by metis_tac[npair_11,npair,CELL_NUM_LEM1,NUM_TO_CELL_TO_NUM] >> 756 fs[] >> 757 qabbrev_tac`anum = ACT_TO_NUM a` >> 758 qexists_tac` 759 Cn (proj 0) [ 760 pr_cond 761 (Cn (pr2 $* ) [ 762 Cn pr_eq [Cn (pr1 nfst) [proj 0] ; Cn (pr1 nfst) [K k] ]; 763 Cn pr_eq [Cn pr_mod [Cn (pr1 nsnd) [Cn (pr1 nsnd) [proj 0]]; 764 twof]; 765 Cn (pr1 nsnd) [K k]] 766 ]) 767 (Cn updn [K s; K anum ; proj 0] ) 768 (Cn (pr1 (tmstepf q)) [proj 0] ) 769 ]` >> fs[primrec_of_tmstepf,primrec_tmstepf_form])); 770 771val tm_return_def = tDefine"tm_return"` 772 tm_return tm = 773 if tm.tape_h = Z then 0 774 else 775 case tm.tape_r of 776 [] => 0 777 | h::t => 1 + tm_return (tm with <| tape_h := h;tape_r:=t|>) 778` 779 (WF_REL_TAC`measure (LENGTH o (��tm. tm.tape_r))` >> simp[]); 780 781val tm_fn_def = Define` 782 tm_fn p args = 783 let tm0 = INITIAL_TM p args 784 in 785 OPTION_MAP (��k. (RUN k tm0)) (OLEAST n. HALTED (RUN n tm0)) 786`; 787 788val _ = temp_overload_on ("un_nlist", ���listOfN���) 789 790val INITIAL_TM_NUM_def = Define` 791 INITIAL_TM_NUM = (��l. ���INITIAL_TM FEMPTY (un_nlist (proj 0 l))���) 792`; 793 794val RUN_NUM_def = Define` 795 RUN_NUM p targs = Pr (INITIAL_TM_NUM) (Cn (pr1 (tmstepf p)) [proj 1]) targs 796`; 797 798val INITIAL_TAPE_PROG = Q.store_thm("INITIAL_TAPE_PROG", 799`(INITIAL_TAPE_TM tm l) with prog := p = INITIAL_TAPE_TM (tm with prog := p) l`, 800Cases_on `l` >> simp[INITIAL_TAPE_TM_def]) 801 802val UPDATE_TAPE_PROG = Q.store_thm("UPDATE_TAPE_PROG", 803`(tm.prog = p) ==> ((UPDATE_TAPE tm) with prog := p = UPDATE_TAPE tm)`, 804strip_tac >>simp[UPDATE_TAPE_def] >> rw[] >> 805Cases_on `SND (tm.prog ' (tm.state,tm.tape_h))` >>simp[TM_component_equality]); 806 807val UPDATE_PROG_CONSERVE = Q.store_thm("UPDATE_PROG_CONSERVE[simp]", 808`(UPDATE_TAPE tm).prog = tm.prog`, 809simp[UPDATE_TAPE_def] >> rw[] >> 810Cases_on `SND (tm.prog ' (tm.state,tm.tape_h))` >>simp[TM_component_equality]); 811 812val RUN_PROG_CONSERVE = Q.store_thm("RUN_PROG_CONSERVE[simp]", 813`(RUN n tm).prog = tm.prog`, 814Induct_on `n` >> simp[FUNPOW_SUC]) 815 816val RUN_PROG = Q.store_thm("RUN_PROG", 817`(tm.prog = p) ==> ((RUN n tm) with prog := p = RUN n tm)`, 818 simp[TM_component_equality] ) 819 820val INITIAL_TAPE_TM_PROG = Q.store_thm("INITIAL_TAPE_TM_PROG[simp]", 821`(INITIAL_TAPE_TM tm args).prog = tm.prog`, 822Cases_on `args` >> simp[INITIAL_TAPE_TM_def] ) 823 824val INITIAL_TM_PROG = Q.store_thm("INITIAL_TM_PROG[simp]", 825`(INITIAL_TM p args).prog = p`, 826 simp[INITIAL_TM_def]) 827 828val RUN_NUM_corr = Q.store_thm("RUN_NUM_corr", 829 `RUN_NUM p [t;args] = ���FUNPOW UPDATE_TAPE t (INITIAL_TM p (un_nlist args))���`, 830 simp[RUN_NUM_def] >> Induct_on `t` >> fs[] 831 >- (simp[INITIAL_TM_NUM_def,INITIAL_TM_def] >> 832 ONCE_REWRITE_TAC[FULL_ENCODE_IGNORES_PROGS 833 |> Q.INST [`p`|-> `ARB` ] |> SYM] >> 834 simp_tac bool_ss[INITIAL_TAPE_PROG] >>simp[]) 835 >- (simp[FUNPOW_SUC] >> rw[SIMP_RULE bool_ss[] tmstepf_update_equiv] >> 836 fs[RUN_PROG])); 837 838val tm_return_num_def = Define` 839 tm_return_num = 840 Pr (Cn (pr1 nsnd) [Cn (pr1 nsnd) [proj 0]]) 841 (pr_cond (Cn pr_eq [Cn pr_mod [Cn pr_div [proj 2;proj 0]; twof]; zerof]) 842 (proj 1) 843 (Cn (pr2 $+) [proj 1;onef])) 844`; 845 846val _ = temp_set_fixity "*." (Infixl 600) 847val _ = temp_overload_on ("*.", ``��n m. Cn (pr2 $*) [n; m]``) 848 849 850val pr_exp_def = Define` 851pr_exp = Cn (Pr onef ( proj 1 *. ( proj 2))) [proj 1;proj 0]` 852 853val primrec_pr_exp = Q.store_thm( 854"primrec_pr_exp[simp]", 855`primrec pr_exp 2`, 856 rw[pr_exp_def] >> SRW_TAC [][primrec_rules] >> SRW_TAC [][pr_cond_def] >> 857 rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) ); 858 859 860val tm_log_num_def = Define` 861 tm_log_num = 862 minimise (SOME ��� 863 Cn pr_eq [ 864 Cn pr_mod [ 865 Cn pr_div [proj 1; Cn pr_exp [twof;Cn succ [proj 0] ] ]; 866 twof 867 ]; 868 zerof 869 ]) 870`; 871 872val primrec_tm_log_num = Q.store_thm("primrec_tm_log_num", 873 `primrec (Cn pr_eq [Cn pr_mod [Cn pr_div [proj 1; 874 Cn pr_exp [twof;Cn succ [proj 0]]]; 875 twof]; 876 zerof ]) 2`, 877 SRW_TAC [][primrec_rules] >> SRW_TAC [][pr_cond_def] >> 878 rpt (MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> 879 simp[primrec_pr_exp]); 880 881val recfn_rulesl = CONJUNCTS recfn_rules 882val recfnMin = save_thm("recfnMin", List.nth(recfn_rulesl, 5)) 883 884val recfn_tm_log_num = Q.store_thm("recfn_tm_log_num", 885 `recfn tm_log_num 1`, 886 `recfn (SOME o 887 Cn pr_eq [Cn pr_mod [Cn pr_div [proj 1; 888 Cn pr_exp [twof;Cn succ [proj 0]]]; 889 twof] ; 890 zerof]) 2` 891 by simp[primrec_recfn,primrec_tm_log_num] >> 892 rw[tm_log_num_def] >> rfs[recfnMin]); 893 894val primrec_tm_ret_run = Q.store_thm("primrec_tm_ret_run", 895 `primrec tm_return_num 2`, 896 `primrec (Cn (pr1 nsnd) [Cn (pr1 nsnd) [proj 0]]) 1` 897 by (SRW_TAC [][primrec_rules] >> 898 SRW_TAC [][pr_cond_def] >> 899 rpt (MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules])) >> 900 `primrec (pr_cond (Cn pr_eq [Cn pr_mod [Cn pr_div [proj 2;proj 0]; twof]; 901 zerof]) 902 (proj 1) 903 (Cn (pr2 $+) [proj 1;onef] )) 3` 904 by (SRW_TAC [][primrec_rules] >> 905 SRW_TAC [][pr_cond_def] >> 906 rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules])) >> 907 rw[tm_return_num_def,primrec_pr]); 908 909 910val INITIAL_TAPE_PRES_STATE = Q.store_thm("INITIAL_TAPE_PRES_STATE[simp]", 911 `(INITIAL_TAPE_TM tm k).state = tm.state`, 912 Cases_on `k` >> rw[INITIAL_TAPE_TM_def]) 913 914val pr_neq_def = Define` 915 pr_neq = Cn (pr2 $+) [Cn (pr2 $-) [pr_le; cflip pr_le]; 916 Cn (pr2 $-) [cflip pr_le; pr_le]] 917`; 918 919val pr_neq_thm = Q.store_thm( 920 "pr_neq_thm", 921 `pr_neq [n; m] = nB (n <> m)`, 922 SRW_TAC [ARITH_ss][pr_neq_def] >> Cases_on `n<=m` >> Cases_on `m<=n` >> fs[]); 923 924val primrec_pr_neq = Q.store_thm( 925"primrec_pr_neq[simp]", 926`primrec pr_neq 2`, 927SRW_TAC [][pr_neq_def, primrec_rules]); 928 929val el_zero_def = Define` 930 (el_zero 0 = 1) ��� 931 (el_zero (SUC n) = 932 let t = ntl (SUC n) 933 in 934 napp (el_zero n) (ncons (nel t (el_zero n) + 1) 0)) 935`; 936 937Theorem ntl_nlist_unnlist: 938 ntl (SUC n) = nlist_of (TL (un_nlist (SUC n))) 939Proof 940 ������n. 0 < n ��� ntl n = nlist_of (TL (listOfN n))��� suffices_by simp[] >> 941 ho_match_mp_tac nlist_ind >> simp[] 942QED 943 944val length_unnlist = Q.store_thm("length_unnlist", 945`0 < LENGTH (un_nlist (SUC n))`, 946fs[DECIDE ���0 < n ��� n ��� 0���]) 947 948val ntl_suc_less = Q.store_thm("ntl_suc_less", 949`���n. ntl (SUC n) <= n`, 950strip_tac >> rw[ntl_def,nsnd_le]) 951 952Theorem nel_nlist_of: 953 i < nlen l ��� nel i l = EL i (listOfN l) 954Proof 955 simp[GSYM nel_correct] 956QED 957 958Theorem el_zero_corr: 959 el_zero n = nlist_of (GENLIST (LENGTH o un_nlist) (n+1)) 960Proof 961 Induct_on `n` >> fs[el_zero_def] >- EVAL_TAC >> 962 `ntl (SUC n) <= n` by simp[ntl_suc_less] >> 963 simp[ADD_CLAUSES,GENLIST,SNOC_APPEND,nel_nlist_of] >> 964 qspec_then ���n + 1��� strip_assume_tac nlist_cases >> fs[ADD1] 965QED 966 967val nleng_def = Define `nleng n = nel n (el_zero n)` 968 969(* add_persistent_funs ["numpair.nlistrec_def"] *) 970 971val nlen_reduc = Q.store_thm("nlen_reduc", 972 `���n. nlen (SUC n) = nlen (ntl (SUC n)) + 1`, 973 strip_tac >> `SUC n <> 0` by fs[] >> 974 `���h t. SUC n = ncons h t ` by metis_tac[nlist_cases] >> rw[]); 975 976val pr_el_zero_def = Define` 977 pr_el_zero = 978 Cn (Pr (onef) 979 (Cn (pr2 napp) [ proj 1 ; 980 Cn (pr2 ncons) [ 981 Cn succ [ 982 Cn (pr2 nel) [ 983 Cn (pr1 ntl) [ 984 Cn succ [proj 0] 985 ]; 986 proj 1 987 ] 988 ]; 989 zerof 990 ] 991 ])) 992 [proj 0;onef] 993`; 994 995val primrec_pr_el_zero = Q.store_thm("primrec_pr_el_zero", 996 `primrec pr_el_zero 1`, 997 fs[pr_el_zero_def] >> rpt (irule primrec_cn >> rw[primrec_rules]) >> 998 irule alt_Pr_rule >> 999 fs[primrec_rules] >> rpt (irule primrec_cn >> rw[primrec_rules])) 1000 1001val primrec_el_zero = Q.store_thm("primrec_el_zero", 1002`primrec (pr1 el_zero) 1`, 1003`(���g. primrec g 1 ��� ���n. g [n] = el_zero n)` suffices_by fs[primrec_pr1] >> 1004 qexists_tac `pr_el_zero` >> fs[primrec_pr_el_zero] >> strip_tac >> Induct_on `n` >- EVAL_TAC >> 1005 rw[el_zero_def,pr_el_zero_def] >> `Pr onef (Cn (pr2 napp) [proj 1; 1006 Cn (pr2 ncons) [Cn succ [Cn (pr2 nel) [Cn (pr1 ntl) [Cn succ [proj 0]]; proj 1]]; zerof]]) [n; 1]= pr_el_zero [n]` by 1007 fs[pr_el_zero_def] >> rfs[] >> rw[] >> fs[ADD1] ) 1008 1009val primrec_nleng = Q.store_thm("primrec_nleng", 1010`primrec (pr1 nleng) 1`, 1011`(���g. primrec g 1 ��� ���n. g [n] = nleng n)` suffices_by fs[primrec_pr1] >> 1012 qexists_tac`Cn (pr2 nel) [proj 0;Cn (pr1 el_zero) [proj 0]]` >> conj_tac 1013 >- (rpt (irule primrec_cn >> rw[primrec_rules]) >> fs[primrec_el_zero]) 1014 >- (strip_tac >> fs[nleng_def] ) ) 1015 1016val Pr_eval = prove( 1017``0 < m ==> (Pr b r (m :: t) = r (m - 1 :: Pr b r (m - 1 :: t) :: t))``, 1018STRIP_TAC THEN SIMP_TAC (srw_ss()) [Once Pr_def, SimpLHS] THEN 1019 Cases_on `m` THEN SRW_TAC [ARITH_ss][]); 1020 1021 1022(* Pr defs, probs use *) 1023val pr_log_def = Define` 1024pr_log = Cn (pr2 $- ) [Cn (Pr (zerof) (Cn (pr2 $+) [proj 1; Cn pr_neq [zerof;Cn pr_div [Cn (pr1 nfst) [proj 2]; 1025 Cn pr_exp [Cn (pr1 nsnd) [proj 2];proj 0 ]]]])) 1026 [proj 0;Cn (pr2 npair) [proj 0;proj 1]];onef]` 1027 1028val pr_tl_en_con_fun2_def = Define` 1029pr_tl_en_con_fun2 = 1030 Cn (pr2 $+) [Cn (pr2 $* ) 1031 [Cn (pr2 $-) [ Cn pr_exp [twof;Cn (pr2 nel) 1032 [proj 0;proj 2 ]];onef ]; 1033 Cn pr_exp [twof;Cn pr_log [proj 1;twof] ] ]; 1034 proj 1] `; 1035 1036val order_flip_def = Define` 1037order_flip = Cn (Pr (zerof ) 1038 (Cn (pr2 ncons) [Cn (pr2 nel) [proj 0;proj 2] ;proj 1] )) 1039 [Cn (pr1 nleng) [proj 0];proj 0]`; 1040 1041val pr_tl_en_con_fun4_def = Define` 1042pr_tl_en_con_fun4 = Cn (pr2 $+) [Cn (pr2 $-) 1043 [Cn pr_exp [twof;Cn (pr2 nel) [proj 0;Cn order_flip [proj 2] ]];onef ]; 1044 Cn (pr2 $* ) [proj 1;Cn pr_exp [twof;Cn succ 1045 [ Cn pr_log [Cn pr_exp [twof;Cn (pr2 nel) [proj 0;Cn order_flip [proj 2]]] ; twof]] ]]] `; 1046 1047val pr_tl_en_con_def = Define` 1048pr_tl_en_con = Cn (pr1 DIV2) [Cn (Pr (zerof) (pr_tl_en_con_fun4)) [Cn (pr1 nleng) [proj 0];proj 0]]`; 1049 1050val primrec_order_flip = Q.store_thm("primrec_order_flip", 1051`primrec order_flip 1`, 1052rw[order_flip_def] >> rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >>fs[primrec_nleng] ) 1053 1054val primrec_pr_log = Q.store_thm("primrec_pr_log", 1055`primrec pr_log 2`, 1056rw[pr_log_def] >> rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> irule alt_Pr_rule >> rw[primrec_rules] >> rpt (irule primrec_cn >> rw[primrec_rules])); 1057 1058 1059val primrec_pr_tl_en_con_fun4 = Q.store_thm("primrec_pr_tl_en_con_fun4", 1060`primrec pr_tl_en_con_fun4 3`, 1061rw[pr_tl_en_con_fun4_def] >> rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> rw[primrec_rules,primrec_pr_exp,primrec_order_flip,primrec_pr_log] >> fs[primrec_nleng] ); 1062 1063val primrec_pr_tl_en_con = Q.store_thm("primrec_pr_tl_en_con", 1064`primrec pr_tl_en_con 1`, 1065SRW_TAC [][pr_tl_en_con_def,primrec_rules] >> 1066 rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules,primrec_div2,primrec_nleng]) >> 1067 fs[primrec_nleng] >> irule alt_Pr_rule >> rw[primrec_pr_tl_en_con_fun4] ); 1068 1069 1070val invtri_zero = Q.store_thm("invtri_zero[simp]", 1071`invtri 0 = 0`, 1072EVAL_TAC) 1073 1074val ntl_zero = Q.store_thm("ntl_zero[simp]", 1075`ntl 0 = 0`, 1076EVAL_TAC) 1077 1078val invtri_nzero = Q.store_thm("invtri_nzero[simp]", 1079`(invtri n = 0) <=> (n = 0)`, 1080eq_tac >> fs[] >> 1081 SRW_TAC [][invtri_def] >> 1082 Q.SPECL_THEN [`n`, `0`] MP_TAC invtri0_thm >> 1083 SRW_TAC [ARITH_ss][tri_def] >> `n < SUC 0` by metis_tac[SND_invtri0] >> rw[] 1084) 1085 1086val nsnd_fun_thm = Q.store_thm("nsnd_fun_thm[simp]", 1087`(nsnd n = n) <=> (n = 0)`, 1088eq_tac >> rw[nsnd_def] >> Cases_on `n` >> fs[] >> 1089`tri (invtri (SUC n')) = 0` by fs[SUB_EQ_EQ_0] >> `tri 0 = 0` by fs[tri_def] >> 1090`invtri (SUC n') = 0` by rfs[tri_11] >> fs[]) 1091 1092val nsnd_lthen = Q.store_thm("nsnd_lthen[simp]", 1093`���n. (nsnd n < n)<=> (n<> 0)`, 1094strip_tac >> eq_tac >> fs[] >> strip_tac >> `nsnd n <= n` by fs[nsnd_le] >> `nsnd n <> n` by fs[] >> rw[]) 1095 1096val FUNPOW_mono = Q.store_thm("FUNPOW_mono", 1097`(���n m. m <= n ==> f m <= f n) ==> (���n m k. m <= n ==> FUNPOW f k m <= FUNPOW f k n)`, 1098rpt strip_tac >> Induct_on `k` >> fs[] >> fs[FUNPOW_SUC] ) 1099 1100val ENCODE_TL_DIV2 = Q.store_thm("ENCODE_TL_DIV2", 1101`ENCODE (TL (h::t)) = DIV2 (ENCODE (h::t))`, 1102Cases_on `h` >> fs[ENCODE_def,DIV2_def,TWO_TIMES_DIV_TWO_thm]) 1103 1104val el_zero_exp = Q.store_thm("el_zero_exp", 1105`el_zero n = nlist_of ((GENLIST (LENGTH ��� un_nlist) n) ++ [(LENGTH ��� un_nlist) n])`, 1106`n+1 = SUC n` by fs[ADD1] >> rw[GENLIST,SNOC_APPEND,el_zero_corr] ) 1107 1108val el_zero_napp = Q.store_thm("el_zero_napp", 1109`el_zero n = napp (nlist_of (GENLIST (LENGTH ��� un_nlist) n)) (nlist_of [(LENGTH ��� un_nlist) n])`, 1110fs[el_zero_exp] ) 1111 1112val r_zero_def = Define` 1113 (r_zero 0 = ncons 0 0) ��� 1114 (r_zero (SUC n) = 1115 let t = ntl (SUC n); r0n = r_zero n; revt = nel t r0n; 1116 res = napp revt (ncons (nhd (SUC n)) 0) 1117 in 1118 napp r0n (ncons res 0)) 1119`; 1120 1121val r_zero_corr = Q.store_thm("r_zero_corr", 1122 `r_zero n = nlist_of (GENLIST (nlist_of o REVERSE o un_nlist) ( n+1))`, 1123 Induct_on `n` >> fs[r_zero_def,ADD_CLAUSES] >> 1124 `ntl (SUC n)<= n` by fs[ntl_suc_less]>> 1125 rw[GENLIST, SNOC_APPEND,nel_nlist_of] >> 1126 `���l. n+1 = nlist_of l` by metis_tac[nlist_of_SURJ] >> rw[ADD1] >> 1127 Cases_on `l` >> fs[]) 1128 1129val _ = overload_on ("order_flip" ,``pr1 (��n. nel n (r_zero n))``) 1130 1131val order_flip_corr = Q.store_thm("order_flip_corr", 1132`order_flip [n] = nlist_of (REVERSE (un_nlist n))`, 1133fs[r_zero_corr,nel_nlist_of]) 1134 1135Theorem order_flip_ncons[simp]: 1136 order_flip [ncons h t] = napp (order_flip [t]) (ncons h 0) 1137Proof fs[order_flip_corr] 1138QED 1139 1140Definition list_rec_comb_def: 1141 list_rec_comb c n 0 = ncons n 0 ��� 1142 list_rec_comb c n (SUC k) = 1143 let t = ntl (SUC k); h=nhd (SUC k); rl = list_rec_comb c n k; 1144 r = nel t rl 1145 in napp rl (ncons (c [h; t; r]) 0) 1146End 1147 1148val LIST_REC_def = Define`(LIST_REC c (n:num) [] = n) ��� 1149 (LIST_REC c n (h::t) = c [h;nlist_of t;LIST_REC c n t])` 1150 1151Theorem list_rec_comb_corr: 1152 list_rec_comb c n k = nlist_of (GENLIST (LIST_REC c n o un_nlist) (k+1)) 1153Proof 1154 Induct_on `k` >> fs[list_rec_comb_def,LIST_REC_def,ADD_CLAUSES]>> 1155 `ntl (SUC k)<= k` by fs[ntl_suc_less]>> 1156 rw[GENLIST, SNOC_APPEND,nel_nlist_of] >> rw[] >> rw[ADD1] >> 1157 `���l. k+1 = nlist_of l` by metis_tac[nlist_of_SURJ]>> rw[] >> 1158 Cases_on `l` >> fs[] >> rw[LIST_REC_def] 1159QED 1160 1161Theorem primrec_list_rec_comb: 1162 primrec c 3 ==> primrec (pr1 (list_rec_comb c n)) 1 1163Proof 1164 strip_tac >> irule primrec_pr1 >> 1165 qexists_tac` 1166 Pr1 (ncons n 0) ( 1167 Cn (pr2 napp) [ 1168 proj 1; 1169 Cn (pr2 ncons) [ 1170 Cn c [ 1171 Cn (pr1 nhd) [Cn succ [proj 0]]; 1172 Cn (pr1 ntl) [Cn succ [proj 0]]; 1173 Cn (pr2 nel) [Cn (pr1 ntl) [Cn succ [proj 0]];proj 1 ] 1174 ]; 1175 zerof 1176 ] 1177 ] 1178 ) 1179 ` >> conj_tac 1180 >- (irule primrec_Pr1 >> 1181 rpt (irule primrec_cn >> rw[primrec_rules,primrec_napp,primrec_ncons])) >> 1182 Induct >> fs[list_rec_comb_def] 1183QED 1184 1185val list_num_rec_thm = Q.store_thm("list_num_rec_thm", 1186`���n c.(primrec c 3)==> ���f.(primrec f 1) ��� (f [0] = n) ��� (���h t. f [ncons h t] = c [h; t; (f [t])])`, 1187rpt strip_tac >> qexists_tac`Cn (pr2 nel) [proj 0;Cn (pr1 (list_rec_comb c n)) [proj 0]] ` >> 1188rpt conj_tac >- (rpt (irule primrec_cn >> rw[primrec_rules,primrec_nel,primrec_list_rec_comb]))>> 1189 simp[list_rec_comb_def] >> simp[list_rec_comb_corr,nel_nlist_of,LIST_REC_def] ) 1190 1191val nleng_thm = new_specification("nleng_def", ["nleng"], 1192list_num_rec_thm |> SPECL[``0n``,``Cn succ [proj 2]``] 1193 |> SIMP_RULE (srw_ss())[primrec_cn, primrec_rules]) 1194 1195val nrev_thm = new_specification("nrev_def", ["nrev"], 1196list_num_rec_thm |> SPECL[``0n``,``Cn (pr2 napp) [proj 2;Cn (pr2 ncons) [proj 0;zerof] ]``] 1197 |> SIMP_RULE (srw_ss())[primrec_cn, primrec_rules]) 1198 1199val concatWith_Z_thm = new_specification("concatWith_Z_def", ["concatWith_Z"], 1200 list_num_rec_thm |> SPECL[``0n``,``pr_cond (Cn pr_eq [proj 1;zerof]) 1201 (proj 0) (Cn (pr2 napp) [proj 0; Cn (pr2 napp) [onef;proj 2]])``] 1202 |> SIMP_RULE (srw_ss())[primrec_cn, primrec_rules]) 1203 1204Theorem concatWith_Z_corr: 1205 concatWith_Z [x] = nlist_of (concatWith [0] (MAP un_nlist (un_nlist x))) 1206Proof 1207 completeInduct_on `x` >> 1208 `(x = 0) ��� ���h t. x = ncons h t` by metis_tac[nlist_cases] >> 1209 simp[concatWith_Z_thm,concatWith_def] >> rw[] >> 1210 simp[concatWith_Z_thm,concatWith_def] >> 1211 `t < ncons h t` 1212 by (simp[ncons_def] >> 1213 `t = nsnd (h *, t)` by simp[] >> 1214 `nsnd (h *, t) <= h *, t` by simp[nsnd_le] >> simp[] ) >> 1215 RES_TAC >> simp[concatWith_def] >> 1216 `���h' t'. t = ncons h' t'` by metis_tac[nlist_cases] >> 1217 simp[concatWith_def] >> 1218 ���ncons 0 0 = 1��� suffices_by (disch_then (SUBST1_TAC o SYM) >> simp[]) >> 1219 EVAL_TAC 1220QED 1221 1222val INITIAL_TAPE_PRES_L = Q.store_thm("INITIAL_TAPE_PRES_L[simp]", 1223`(INITIAL_TAPE_TM tm (h::t)).tape_l = []`, 1224fs[INITIAL_TAPE_TM_def]) 1225 1226val tape_encode_def = Define `tape_encode = pr_cond (Cn pr_eq [proj 1;zerof]) 1227 (Cn (pr2 npair) [proj 0;Cn (pr2 $*) [twof;proj 2]]) 1228 (Cn (pr2 npair) [proj 0;Cn succ [Cn (pr2 $* ) [twof;proj 2]]])` 1229 1230val primrec_tape_encode = Q.store_thm("primrec_tape_encode[simp]", 1231`primrec tape_encode 3`, 1232fs[tape_encode_def] >> irule primrec_pr_cond >> rpt conj_tac >> 1233rpt (irule primrec_cn >> 1234 rw[primrec_rules,primrec_pr_cond,primrec_pr_eq,primrec_pr_mult])); 1235 1236val tape_encode_corr = Q.store_thm("tape_encode_corr", 1237`tape_encode [ENCODE tm.tape_l;NUM_CELL tm.tape_h;ENCODE tm.tape_r] = ENCODE_TM_TAPE tm`, 1238fs[tape_encode_def,ENCODE_TM_TAPE_def] >> `CELL_NUM (NUM_CELL tm.tape_h) = tm.tape_h` by 1239 fs[CELL_NUM_NUM_CELL]>> `CELL_NUM 0 = Z` by fs[CELL_NUM_def]>>`NUM_CELL Z = 0` by fs[NUM_CELL_def] 1240>>`(NUM_CELL tm.tape_h = 0) ��� (tm.tape_h = Z)` by metis_tac[NUM_CELL_INJ] >>rw[] ) 1241 1242val tape_encode_corr_sym = Q.store_thm("tape_encode_corr_sym", 1243`ENCODE_TM_TAPE tm = tape_encode [ENCODE tm.tape_l;NUM_CELL tm.tape_h;ENCODE tm.tape_r]`, 1244fs[tape_encode_corr]) 1245 1246 1247(* Define correctly so it matches what it should *) 1248val pr_INITIAL_TAPE_TM_NUM_def = Define` 1249pr_INITIAL_TAPE_TM_NUM = pr_cond (Cn pr_eq [proj 1;zerof]) (proj 0) (Cn (pr2 npair) 1250[Cn (pr1 nfst) [proj 0];Cn (pr2 npair) [Cn (pr1 nhd) [proj 1];Cn (pr1 ntl) [proj 1]] ])`; 1251 1252val primrec_pr_INITIAL_TAPE_TM_NUM = Q.store_thm( 1253 "primrec_pr_INITIAL_TAPE_TM_NUM[simp]", 1254 `primrec pr_INITIAL_TAPE_TM_NUM 2`, 1255 fs[pr_INITIAL_TAPE_TM_NUM_def] >> `0<2` by fs[] >> 1256 irule primrec_pr_cond >> rpt conj_tac >> 1257 rpt (irule primrec_cn >> 1258 rw[primrec_rules,primrec_pr_eq,primrec_nsnd,primrec_nfst]) >> 1259 fs[primrec_proj]); 1260 1261val pr_INITIAL_TM_NUM_def = Define` 1262pr_INITIAL_TM_NUM = Cn (pr2 npair) [zerof;Cn tape_encode 1263 [Cn (pr1 nfst) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]]; 1264 Cn (pr1 nfst) [Cn (pr1 nsnd) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]]]; 1265 Cn (pr1 nsnd) [Cn (pr1 nsnd) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]]]]]`; 1266 1267val pr_ODD_def = Define`pr_ODD = pr_cond (Cn pr_eq [Cn pr_mod [proj 0;twof];onef]) onef zerof` 1268 1269val pr_ODD_corr = Q.store_thm("pr_ODD_corr", 1270`pr_ODD [x] = if ODD x then 1 else 0`, 1271fs[pr_ODD_def] >> Cases_on `ODD x` >- metis_tac[ODD_MOD_TWO_lem] >> 1272`EVEN x` by metis_tac[EVEN_OR_ODD] >> fs[EVEN_MOD2]); 1273 1274val GENLIST_ZERO = Q.store_thm("GENLIST_ZERO", 1275`(GENLIST a b = []) <=> (b=0)`, 1276eq_tac >> fs[GENLIST] >> strip_tac >> Cases_on `b` >> fs[GENLIST] ); 1277 1278val concatWith_Z_empty = Q.store_thm("concatWith_Z_empty", 1279`(concatWith [Z] (MAP (GENLIST (K O)) args) = []) <=> ((args = []) ��� (args = [0]))`, 1280eq_tac >- (strip_tac >> Cases_on `MAP (GENLIST (K O)) args` >> rfs[concatWith_def] >> 1281 Cases_on `t` >> rfs[concatWith_def] >> `GENLIST (K O) x0 = []` by fs[] >> fs[GENLIST_ZERO]) 1282 >- (strip_tac >> rw[concatWith_def])); 1283 1284val head_concatWith = Q.store_thm("head_concatWith", 1285`((l<> []) ��� (HD l <> [])) ==> (HD (concatWith a l) = HD (HD l))`, 1286strip_tac >> Cases_on `l` >> fs[concatWith_def] >> Cases_on `t` >> fs[concatWith_def,HD] >> 1287 Cases_on `h` >> fs[]) 1288 1289val head_nil_concatWith = Q.store_thm("head_nil_concatWith[simp]", 1290`HD (concatWith [a] ([]::b::c)) = a`, 1291rw[concatWith_def]) 1292 1293val odd_encode_hd_concat = Q.store_thm("odd_encode_hd_concat", 1294`(concatWith [Z] (MAP (GENLIST (K O)) args) <> []) ==> (NUM_CELL (HD (concatWith [Z] (MAP (GENLIST (K O)) args))) = 1 - pr_eq [proj 0 args;0])`, 1295strip_tac >> fs[concatWith_Z_empty] 1296 >> Cases_on `args` >- rw[concatWith_def] >> Cases_on `h = 0` >> simp[proj_def]>> 1297 Cases_on `MAP (GENLIST (K O)) t`>> simp[] 1298 >- (`t = []` by fs[MAP_EQ_NIL] >> rw[]) >> simp[concatWith_def] 1299 >- (`���h'. h = SUC h'` by metis_tac[num_CASES] >> rw[] >> fs[HD_GENLIST]) 1300 >- (`���h'. h = SUC h'` by metis_tac[num_CASES] >> rw[] >> fs[GENLIST_CONS]) ) 1301 1302val nfst_zero = Q.store_thm("nfst_zero[simp]", `nfst 0 = 0`, EVAL_TAC) 1303val nsnd_zero = Q.store_thm("nsnd_zero[simp]", `nsnd 0 = 0`, EVAL_TAC) 1304val nhd_zero = Q.store_thm("nhd_zero[simp]", `nhd 0 = 0`, EVAL_TAC) 1305val ntl_zero = Q.store_thm("nstl_zero[simp]", `ntl 0 = 0`, EVAL_TAC) 1306 1307val num_cell_encode_hd_concat = Q.store_thm("num_cell_encode_hd_concat", 1308`(concatWith [Z] (MAP (GENLIST (K O)) args) <> []) ==> (NUM_CELL (HD (concatWith [Z] (MAP (GENLIST (K O)) args))) = 1 - pr_eq [ nhd (nlist_of args);0])`, 1309rw[odd_encode_hd_concat] >> Cases_on `args` >> simp[nhd_thm] ) 1310 1311val encode_concat_def = tDefine "encode_concat" ` 1312 (encode_concat 0 = 0) ��� 1313 (encode_concat args = ((2** (nhd args)) - 1) + 1314 (2* ((2** (nhd args))) * (encode_concat (ntl args))))` 1315(qexists_tac `$<` >> conj_tac >- simp[prim_recTheory.WF_LESS] >> strip_tac >> 1316`ntl (SUC v) <= v` by simp[ntl_suc_less] >> `v < SUC v` by simp[prim_recTheory.LESS_SUC_REFL]>> 1317rw[]) 1318 1319val encode_tl_concat_def = Define`encode_tl_concat args = DIV2 (encode_concat args)` 1320 1321val ENCODE_GENLIST_p_Z = Q.store_thm("ENCODE_GENLIST_p_Z", 1322`ENCODE (GENLIST (K O) h ++ [Z] ++ b) = ((2**h) - 1) + (2*((2**h))*(ENCODE b))`, 1323Induct_on `h` >> simp[ENCODE_def] >> simp[GENLIST_CONS] >> simp[ENCODE_def] >>rw[EXP] >> 1324`2 * (2 ** h ��� 1 + 2 * (ENCODE b * 2 ** h)) = 2*2 ** h ��� 2*1 + 4 * (ENCODE b * 2 ** h)` by fs[]>> 1325rw[] >> `2<=2*2**h` by (rpt (pop_assum kall_tac) >> Induct_on `h` >> simp[]) >> simp[]) 1326 1327val ENCODE_GENLIST_O = Q.store_thm("ENCODE_GENLIST_O", 1328`ENCODE (GENLIST (K O) h) = 2 ** h ��� 1`, 1329Induct_on `h` >> simp[ENCODE_def,GENLIST_CONS,EXP] >> `1<=2**h` suffices_by simp[] >> 1330 `0<2**h` suffices_by decide_tac >> simp[]) 1331 1332val encode_concat_corr = Q.store_thm("encode_concat_corr", 1333`ENCODE (concatWith [Z] (MAP (GENLIST (K O)) args)) = encode_concat (nlist_of args)`, 1334Induct_on `args` >> fs[concatWith_def,ENCODE_def,encode_concat_def] >> strip_tac >> 1335`nhd (ncons h (nlist_of args)) = h` by simp[nhd_thm] >> `ntl (ncons h (nlist_of args)) = 1336nlist_of args` by simp[ntl_thm] >> `ncons h (nlist_of args) <> 0` by simp[ncons_not_nnil] >> 1337`��� n0. ncons h (nlist_of args) = SUC n0 ` by metis_tac[num_CASES] >>rw[encode_concat_def] >> 1338full_simp_tac bool_ss[] >> 1339Cases_on `args` >> simp[concatWith_def] >- simp[encode_concat_def,ENCODE_GENLIST_O] >> 1340simp[ENCODE_GENLIST_p_Z] >> fs[]) 1341 1342val pr_INITIAL_TM_NUM_def = Define` 1343pr_INITIAL_TM_NUM = Cn (pr2 npair) [zerof;Cn tape_encode 1344 [zerof; 1345 Cn (pr2 $-) [onef ;Cn pr_eq [Cn (pr1 nhd) [proj 0];zerof]]; 1346 Cn (pr1 encode_tl_concat) [proj 0]]]` 1347 1348Theorem encode_concat_list_rec: 1349 encode_concat n = 1350 nel n ( 1351 list_rec_comb ( 1352 Cn (pr2 $+) [ 1353 Cn (pr1 PRE) [Cn (pr2 $EXP) [twof;proj 0]]; 1354 Cn (pr2 $*) [twof;Cn (pr2 $*) [proj 2;Cn (pr2 $EXP) [twof;proj 0]]] 1355 ] 1356 ) 0 n 1357 ) 1358Proof 1359 rw[list_rec_comb_corr] >> 1360 `���l. n = nlist_of l` by metis_tac[nlist_of_SURJ] >> rw[] >> 1361 Induct_on `l` >> simp[LIST_REC_def,encode_concat_def] >> strip_tac >> 1362 `ncons h (nlist_of l) <> 0` by simp[ncons_not_nnil] >> 1363 `��� n0. ncons h (nlist_of l) = SUC n0 ` by metis_tac[num_CASES] >> 1364 rw[encode_concat_def] >> 1365 full_simp_tac bool_ss[] >> pop_assum (SUBST_ALL_TAC o SYM) >> 1366 simp[nel_nlist_of,LIST_REC_def] 1367QED 1368 1369val pr_encode_concat_def = Define` 1370 pr_encode_concat = 1371 Cn (pr2 nel) [ 1372 proj 0; 1373 Cn (pr1 (list_rec_comb (Cn (pr2 $+) [ 1374 Cn (pr1 PRE) [Cn (pr2 $EXP) [twof;proj 0]]; 1375 Cn (pr2 $*) [twof;Cn (pr2 $*) [proj 2;Cn (pr2 $EXP) [twof;proj 0]]] 1376 ]) 0)) [proj 0] 1377 ]`; 1378 1379val pr_encode_tl_concat_def = Define`pr_encode_tl_concat = Cn (pr1 DIV2) [Cn (pr2 nel) [proj 0; 1380 Cn (pr1 (list_rec_comb (Cn (pr2 $+) [Cn (pr1 PRE) [Cn (pr2 $EXP) [twof;proj 0]]; 1381 Cn (pr2 $*) [twof;Cn (pr2 $*) [proj 2;Cn (pr2 $EXP) [twof;proj 0]]]]) 0)) [proj 0]]]` 1382 1383 1384val primrec_exp = Q.store_thm("primrec_exp", 1385`primrec (pr2 $**) 2`, 1386 irule primrec_pr2 >>qexists_tac `pr_exp` >> conj_tac >-simp[primrec_pr_exp] >> simp[pr_exp_def]>> 1387Induct >> Induct >> simp[] >> rw[EXP]) 1388 1389val primrec_pr_INITIAL_TM_NUM = Q.store_thm("primrec_pr_INITIAL_TM_NUM[simp]", 1390`primrec pr_INITIAL_TM_NUM 1`, 1391SRW_TAC [][pr_INITIAL_TM_NUM_def,primrec_rules] >> 1392 rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules,concatWith_Z_thm,primrec_pr_INITIAL_TAPE_TM_NUM,primrec_tape_encode,primrec_npair,primrec_ntl,primrec_nhd]) >> 1393 irule primrec_pr1 >> qexists_tac `pr_encode_tl_concat` >> conj_tac 1394 >- (rw[pr_encode_tl_concat_def] >>rpt (irule primrec_cn >> rw[primrec_rules,primrec_nel] )>- 1395(`primrec (Cn (pr2 $+) 1396 [Cn (pr1 PRE) [Cn (pr2 $** ) [twof; proj 0]]; 1397 twof *. (proj 2 *. Cn (pr2 $** ) [twof; proj 0])]) 3` suffices_by 1398 rw[primrec_list_rec_comb] >> rpt (irule primrec_cn >> rw[primrec_rules,primrec_nel] ) >> 1399 simp[primrec_exp,primrec_div2]) >> simp[primrec_div2] ) 1400 >- (strip_tac >> simp[encode_concat_list_rec] >> `���l. n = nlist_of l` by metis_tac[nlist_of_SURJ] >> rw[] >> Induct_on `l` >> simp[list_rec_comb_def,encode_tl_concat_def,encode_concat_def,nlist_of_def,pr_encode_concat_def] >- simp[pr_encode_concat_def,pr_encode_tl_concat_def,list_rec_comb_def] >> strip_tac >> simp[pr_encode_tl_concat_def,encode_concat_list_rec] ) ) 1401 1402 1403 1404val tape_encode_thm = Q.store_thm("tape_encode_thm", 1405`tape_encode [a;b;c] = if b=0 then a *, (2* c) else a *, (SUC (2*c))`, 1406fs[tape_encode_def]) 1407 1408val tape_encode_eq = Q.store_thm("tape_encode_eq", 1409`(((b=0) ��� (b=1)) ��� ((e=0) ��� (e=1))) ==> 1410 ( (tape_encode [a;b;c] = tape_encode [d;e;f]) <=> ((a=d) ��� (b=e) ���(c=f)))`, 1411strip_tac >> eq_tac >> rw[tape_encode_thm] 1412 >- (CCONTR_TAC >> rfs[] >> `ODD (SUC (2* f))` by fs[ODD_DOUBLE] >> `EVEN (2*c)` by 1413 fs[EVEN_DOUBLE] >> rfs[EVEN_AND_ODD] >> fs[EVEN,EVEN_DOUBLE] ) 1414 >- (CCONTR_TAC >> rfs[] >> `ODD (SUC (2* c))` by fs[ODD_DOUBLE] >> `EVEN (2*f)` by 1415 fs[EVEN_DOUBLE] >> rfs[EVEN_AND_ODD] >> metis_tac[EVEN_AND_ODD]) ) 1416 1417val ENCODE_TL_concatWith = Q.store_thm("ENCODE_TL_concatWith", 1418`(concatWith [Z] (MAP (GENLIST (K O)) args) = h::t) ==> (ENCODE t = encode_tl_concat (nlist_of args))`, 1419rw[] >> simp[encode_tl_concat_def] >> `ENCODE t = ENCODE (TL (concatWith [Z] (MAP (GENLIST (K O)) args)))` 1420by simp[] >> metis_tac[encode_concat_corr,ENCODE_TL_DIV2]) 1421 1422Theorem primrec_INITIAL_TM_NUM: 1423 primrec INITIAL_TM_NUM 1 1424Proof 1425 `INITIAL_TM_NUM = pr_INITIAL_TM_NUM` 1426 suffices_by fs[primrec_pr_INITIAL_TM_NUM] >> 1427 fs[FUN_EQ_THM] >> strip_tac >> 1428 fs[INITIAL_TM_NUM_def,INITIAL_TM_def,INITIAL_TAPE_TM_def, 1429 FULL_ENCODE_TM_def,pr_INITIAL_TM_NUM_def,tape_encode_corr_sym] >> 1430 Cases_on `(concatWith [Z] (MAP (GENLIST (K O)) (un_nlist (proj 0 x))))` >> 1431 fs[INITIAL_TAPE_TM_def] >> 1432 fs[pr_INITIAL_TM_NUM_def,pr_INITIAL_TAPE_TM_NUM_def,tape_encode_corr, 1433 concatWith_Z_corr] 1434 >- (`���l. proj 0 x = nlist_of l` by metis_tac[nlist_of_SURJ] >>fs[]>> 1435 `(l = []) ��� (l = [0])` by rfs[concatWith_Z_empty] >> 1436 fs[encode_tl_concat_def,encode_concat_def,ENCODE_def,DIV2_def, 1437 ncons_def] >>EVAL_TAC) >> 1438 simp[ENCODE_def] >> 1439 `ENCODE t = encode_tl_concat (proj 0 x)` 1440 by metis_tac[ENCODE_TL_concatWith,listOfN_nlist, nlist_listOfN] >> 1441 simp[ENCODE_TL_concatWith] >> 1442 `NUM_CELL h = 1443 NUM_CELL 1444 (HD (concatWith [Z] (MAP (GENLIST (K O)) (un_nlist (proj 0 x)))))` 1445 by simp[] >> 1446 simp[odd_encode_hd_concat] >> 1447 `nB (proj 0 (un_nlist (proj 0 x)) ��� 0) = nB (nhd (proj 0 x) ��� 0)` 1448 suffices_by simp[] >> rw[] >> 1449 Cases_on `x` >> simp[] >> 1450 `���l. h' = nlist_of l` by metis_tac[nlist_of_SURJ] >> rw[]>> 1451 Cases_on `l` >> simp[] 1452QED 1453 1454val RUN_NUM_p = Q.store_thm("RUN_NUM_p", 1455 `RUN_NUM p = Pr INITIAL_TM_NUM (Cn (pr1 (tmstepf p)) [proj 1]) `, 1456 simp[FUN_EQ_THM,RUN_NUM_def]); 1457 1458val primrec_RUN_NUM = Q.store_thm("primrec_RUN_NUM", 1459 `primrec (RUN_NUM p) 2`, 1460 fs[RUN_NUM_p] >> irule alt_Pr_rule >> rpt conj_tac 1461 >- fs[primrec_INITIAL_TM_NUM] >> 1462 irule primrec_cn >> rpt conj_tac >- fs[primrec_rules] >> fs[primrec_tmstepf]); 1463 1464val Pr_thm_one = Q.store_thm("Pr_thm_one", 1465`(Pr b r (1::t) = r (0::Pr b r (0::t)::t))`, 1466rw[Pr_thm] >> `Pr b r (1::t) = Pr b r ((SUC 0)::t)` by metis_tac[ONE] >> rw[]) 1467 1468val zero_less_nB = Q.store_thm("zero_less_nB[simp]", 1469`(0 < nB A) <=> A`, 1470Cases_on `A` >> fs[]) 1471 1472 1473val recfn_rulesl = CONJUNCTS recfn_rules 1474val recfnCn = save_thm("recfnCn", List.nth(recfn_rulesl, 3)) 1475val recfnPr = save_thm("recfnPr", List.nth(recfn_rulesl, 4)) 1476val recfnMin = save_thm("recfnMin", List.nth(recfn_rulesl, 5)) 1477 1478(* Probably need to include a 'tape reset' type function, ie tm_return_num *) 1479val recfn_tm_def = Define` 1480 recfn_tm p = recCn (SOME o (RUN_NUM p)) [ 1481 minimise (SOME o (Cn (pr1 nfst) [RUN_NUM p] ) ) ; 1482 SOME o proj 0] ` 1483 1484val recfn_tm_recfn = Q.store_thm("recfn_tm_recfn", 1485 `recfn (recfn_tm p) 1`, 1486 rw[recfn_tm_def] >> fs[primrec_RUN_NUM,primrec_recfn] >> irule recfnCn >> 1487 rw[recfn_rules] 1488 >- (irule recfnMin >> fs[] >> irule primrec_recfn >> 1489 rpt (irule primrec_cn >> 1490 rw[primrec_rules,primrec_pr_eq,primrec_RUN_NUM,primrec_pr_add])) 1491 >- (fs[primrec_RUN_NUM,primrec_recfn])); 1492 1493val UPDATE_TAPE_HALTED = Q.store_thm("UPDATE_TAPE_HALTED[simp]", 1494`(HALTED tm) ==> (UPDATE_TAPE tm = tm)`, 1495rw[] >> fs[UPDATE_TAPE_def,HALTED_def] >> simp[TM_component_equality]); 1496 1497val run_num_halted = Q.store_thm("run_num_halted", 1498 `���n. HALTED (RUN n (INITIAL_TM p args)) ��� n<=m ==> 1499 (RUN_NUM p [m; nlist_of args] = RUN_NUM p [SUC m; nlist_of args])`, 1500 rpt strip_tac >> `���k. m=n+k` by metis_tac[LESS_EQ_EXISTS] >> 1501 rw[RUN_NUM_corr,FUNPOW_SUC] >> qmatch_abbrev_tac `���tm��� = ���UPDATE_TAPE tm���` >> 1502 `HALTED tm` suffices_by simp[] >> 1503 qunabbrev_tac `tm` >> fs[] >> Induct_on `k` >> 1504 simp[] >> rw[] >> simp[FUNPOW_SUC,ADD_CLAUSES]); 1505 1506val main_eq_thm = Q.store_thm("main_eq_thm", 1507 `���p. ���f. recfn f 1 ��� 1508 ���args. 1509 OPTION_MAP FULL_ENCODE_TM (tm_fn p args) = f [nlist_of args]`, 1510 strip_tac >> qexists_tac`recfn_tm p` >> conj_tac 1511 >- fs[recfn_tm_recfn] >> 1512 strip_tac >> fs[tm_fn_def,recfn_tm_def] >> 1513 Cases_on `(OLEAST n. HALTED (RUN n (INITIAL_TM p args)))` >> 1514 fs[optionTheory.OPTION_MAP_DEF] >> rw[RUN_NUM_corr] >> fs[recCn_def] 1515 >- (fs[] >>fs[minimise_def] >> rpt strip_tac >> rfs[RUN_NUM_corr] >> 1516 first_x_assum (qspec_then `n` mp_tac) >> simp[HALTED_def] >> 1517 fs[]) 1518 >- (fs[OLEAST_EQ_SOME,minimise_def] >> rw[] 1519 >- (rename[`RUN n (INITIAL_TM p args)`] >> qexists_tac `n` >> 1520 fs[HALTED_def,RUN_NUM_corr] >> metis_tac[]) 1521 >- (fs[RUN_NUM_corr] >> qmatch_abbrev_tac `���RUN i tm��� = ���RUN j tm���`>> 1522 `i=j` suffices_by simp[] >> qunabbrev_tac `i` >> SELECT_ELIM_TAC >> 1523 rw[] 1524 >- (fs[HALTED_def] >> metis_tac[]) 1525 >- (fs[HALTED_def] >> 1526 qmatch_abbrev_tac `a=b` >>`��(a<b)�����(b<a)` suffices_by simp[] >> 1527 rpt strip_tac >> metis_tac[NOT_ZERO_LT_ZERO])) 1528 >- (fs[RUN_NUM_corr] >> first_x_assum (qspec_then `x` mp_tac)>> 1529 rpt strip_tac >> fs[HALTED_def] >> 1530 `���i. i < x ��� ((RUN i (INITIAL_TM p args)).state = 0)` by fs[] >> 1531 metis_tac[]))); 1532 1533(* as final step, should show that we can extract number under head *) 1534 1535val _ = export_theory(); 1536