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