1open HolKernel Parse boolLib bossLib; 2 3open arithmeticTheory whileTheory logrootTheory pred_setTheory listTheory 4open reductionEval; 5open churchoptionTheory churchlistTheory recfunsTheory 6 kolmogorov_complexityTheory invarianceResultsTheory boolListsTheory 7open churchDBTheory 8open recursivefnsTheory primrecfnsTheory prtermTheory 9open unary_recfnsTheory 10 11val _ = new_theory "pfreefns"; 12 13val _ = intLib.deprecate_int() 14 15Theorem bnf_of_SOME_lameq: 16 bnf_of M = SOME N ��� M == N ��� bnf N 17Proof 18 eq_tac 19 >- (strip_tac >> drule normal_orderTheory.bnf_of_SOME >> 20 simp_tac (bsrw_ss())[]) >> 21 ACCEPT_TAC normal_orderTheory.lameq_bnf_of_SOME_I 22QED 23 24Definition calc_fn_alist_def : 25 calc_fn_alist = 26 LAM "M" ( 27 LAM "s" ( 28 LAM "l" ( 29 cmap @@ ( 30 LAM "it" (cpair @@ (cfst @@ VAR "it") 31 @@ (cforce_num @@ (csnd @@ VAR "it"))) 32 ) @@ ( 33 cfilter @@ (LAM "it" (cbnf @@ (csnd @@ VAR "it"))) @@ VAR "l" 34 ) 35 ) @@ ( (* generate list of all step-results *) 36 ctabulate @@ 37 VAR "s" @@ 38 LAM "i" ( 39 cpair @@ VAR "i" @@ ( 40 csteps @@ VAR "s" @@ ( 41 cdAPP @@ (cnumdB @@ VAR "M") 42 @@ (cchurch @@ VAR "i") 43 ) 44 ) 45 ) 46 ) 47 ) 48 ) 49End 50 51Theorem FV_calc_fn_alist[simp]: 52 FV calc_fn_alist = ��� 53Proof 54 simp[EXTENSION, calc_fn_alist_def, DISJ_IMP_EQ] 55QED 56 57Theorem calc_fn_alist_eqn = brackabs.brackabs_equiv [] calc_fn_alist_def; 58 59Theorem bnf_of_cnil[simp]: 60 bnf_of cnil = SOME cnil 61Proof 62 simp[normal_orderTheory.bnf_bnf_of, cnil_def] 63QED 64 65Theorem steps_LAM[simp]: 66 ���n M. steps n (LAM v M) = LAM v (steps n M) 67Proof 68 Induct >> simp[normal_orderTheory.noreduct_thm] >> rw[] >> 69 Cases_on ���noreduct M��� >> 70 fs[normal_orderTheory.noreduct_bnf] 71QED 72 73Theorem steps_VARAPP[simp]: 74 ���n M s. steps n (VAR s @@ M) = VAR s @@ steps n M 75Proof 76 Induct >> simp[normal_orderTheory.noreduct_thm] >> rw[] >> 77 Cases_on ���noreduct M��� >> fs[normal_orderTheory.noreduct_bnf] 78QED 79 80Theorem bnf_of_LAM: 81 bnf_of (LAM v M0) = do M <- bnf_of M0 ; SOME (LAM v M) od 82Proof 83 Cases_on ���bnf_of M0��� >> simp[] 84 >- fs[numsAsCompStatesTheory.bnf_of_EQ_NONE_steps] >> 85 fs[stepsTheory.bnf_steps] >> metis_tac[] 86QED 87 88Theorem bnf_of_VAR[simp]: 89 bnf_of (VAR s) = SOME (VAR s) 90Proof 91 simp[normal_orderTheory.bnf_bnf_of] 92QED 93 94Theorem bnf_of_VARAPP: 95 bnf_of (VAR s @@ M0) = do M <- bnf_of M0 ; SOME (VAR s @@ M) od 96Proof 97 Cases_on ���bnf_of M0��� >> simp[] 98 >- fs[numsAsCompStatesTheory.bnf_of_EQ_NONE_steps] >> 99 fs[stepsTheory.bnf_steps] >> metis_tac[] 100QED 101 102Theorem steps_VARAPP2a: 103 ���m n M0. 104 bnf (steps n M0) ��� m ��� n ��� (���i. i < n ��� ��bnf (steps i M0)) ��� 105 steps m (VAR s @@ M0 @@ N0) = VAR s @@ steps m M0 @@ N0 106Proof 107 Induct >> rw[] >> fs[] 108 >- (first_x_assum (qspec_then ���0��� mp_tac) >> simp[]) >> 109 simp[normal_orderTheory.noreduct_thm] >> Cases_on ���noreduct M0��� >> simp[] 110 >- fs[normal_orderTheory.noreduct_bnf] >> 111 first_x_assum irule >> qexists_tac ���n - 1��� >> simp[] >> 112 Cases_on ���n��� >> fs[] >> rfs[] >> qx_gen_tac ���i��� >> 113 first_x_assum (qspec_then ���SUC i��� mp_tac) >> simp[] 114QED 115 116Theorem steps_VARAPP2b: 117 ���m n M0 N0. 118 bnf (steps n M0) ��� n < m ��� (���i. i < n ��� ��bnf (steps i M0)) ��� 119 steps m (VAR s @@ M0 @@ N0) = VAR s @@ steps n M0 @@ steps (m - n) N0 120Proof 121 Induct >> rw[] >> fs[] 122 >- (Cases_on ���n��� >> simp[]) 123 >- (Cases_on ���SUC m - n��� >> simp[]) 124 >- (Cases_on ���n��� >> fs[] >> rfs[] >> 125 rename [���bnf (steps n0 (THE (noreduct M0)))���] >> 126 simp[normal_orderTheory.noreduct_thm] >> 127 Cases_on ���noreduct M0��� >> simp[] >- fs[normal_orderTheory.noreduct_bnf] >> 128 first_x_assum irule >> fs[] >> qx_gen_tac ���j��� >> 129 first_x_assum (qspec_then ���SUC j��� mp_tac) >> simp[]) >> 130 Cases_on ���n��� >> fs[] >> rfs[] 131 >- (simp[normal_orderTheory.noreduct_thm] >> 132 Cases_on ���noreduct N0��� >> simp[] 133 >- fs[normal_orderTheory.noreduct_bnf] >> 134 Cases_on ���m = 0��� >> rw[] >> 135 first_x_assum (qspec_then ���0��� (irule o SIMP_RULE (srw_ss()) [])) >> 136 simp[]) >> 137 rename [���n < m���] >> 138 �����bnf M0��� 139 by (first_x_assum (qspec_then ���0��� mp_tac) >> simp[]) >> 140 fs[] >> Cases_on ���noreduct M0��� >> simp[] 141 >- fs[normal_orderTheory.noreduct_bnf] >> 142 simp[normal_orderTheory.noreduct_thm] >> first_x_assum irule >> fs[] >> 143 qx_gen_tac ���j��� >> first_x_assum (qspec_then ���SUC j��� mp_tac) >> simp[] 144QED 145 146Theorem bnf_of_VARAPP2: 147 bnf_of (VAR s @@ M0 @@ N0) = 148 do M <- bnf_of M0; N <- bnf_of N0; SOME (VAR s @@ M @@ N) od 149Proof 150 Cases_on ���bnf_of M0��� >> simp[] 151 >- (fs[numsAsCompStatesTheory.bnf_of_EQ_NONE_steps] >> 152 gen_tac >> pop_assum mp_tac >> map_every qid_spec_tac [���M0���, ���n���] >> 153 Induct >> simp[] >- (gen_tac >> disch_then (qspec_then ���0��� mp_tac) >> 154 simp[]) >> 155 gen_tac >> strip_tac >> 156 first_assum (qspec_then ���0��� (mp_tac o SIMP_RULE (srw_ss()) [])) >> 157 simp[] >> strip_tac >> simp[normal_orderTheory.noreduct_thm] >> 158 Cases_on ���noreduct M0��� >> simp[] >> fs[normal_orderTheory.noreduct_bnf]>> 159 first_x_assum match_mp_tac >> gen_tac >> 160 first_x_assum (qspec_then ���SUC n��� mp_tac) >> simp[]) >> 161 Cases_on ���bnf_of N0��� >> simp[] 162 >- (fs[numsAsCompStatesTheory.bnf_of_EQ_NONE_steps, stepsTheory.bnf_steps] >> 163 ������n0. bnf (steps n0 M0) ��� ���i. i < n0 ��� ��bnf (steps i M0)��� 164 by (qspec_then �����j. bnf (steps j M0)��� (irule o BETA_RULE) WOP >> 165 metis_tac[]) >> 166 qx_gen_tac���m��� >> Cases_on ���m ��� n0��� 167 >- (qspecl_then [���m���, ���n0���, ���M0���] mp_tac steps_VARAPP2a >> simp[] >> 168 metis_tac[stepsTheory.steps_def]) >> 169 qspecl_then [���m���, ���n0���, ���M0���] mp_tac steps_VARAPP2b >> simp[]) >> 170 fs[stepsTheory.bnf_steps] >> 171 rename [���VAR s @@ M0 @@ N0���, ���steps n1 M0 = M���, ���steps n2 N0 = N���] >> 172 ������n0. bnf (steps n0 M0) ��� ���i. i < n0 ��� ��bnf (steps i M0)��� 173 by (qspec_then �����j. bnf (steps j M0)��� (irule o BETA_RULE) WOP >> 174 metis_tac[]) >> 175 ���steps n0 M0 = M��� 176 by (Cases_on ���n0 = n1��� >> fs[] >> 177 ���n0 < n1��� by metis_tac[DECIDE ���x < y ��� x = y ��� y < x:num���] >> 178 metis_tac[stepsTheory.bnf_steps_upwards_closed]) >> 179 qexists_tac ���n0 + n2��� >> 180 Cases_on ���n2 = 0��� 181 >- (qspecl_then [���n0���, ���n0���, ���M0���] mp_tac steps_VARAPP2a >> simp[] >> fs[]) >> 182 qspecl_then [���n0 + n2���, ���n0���, ���M0���] mp_tac steps_VARAPP2b >> simp[] 183QED 184 185Theorem S_eq_K: 186 ��(S == K) 187Proof 188 simp[chap3Theory.lameq_betaconversion] >> strip_tac>> 189 `���Z. reduction beta S Z /\ reduction beta K Z` 190 by PROVE_TAC [chap3Theory.theorem3_13, chap3Theory.beta_CR] THEN 191 ���normal_form beta S ��� normal_form beta K��� 192 by PROVE_TAC [chap2Theory.S_beta_normal, chap2Theory.K_beta_normal, 193 chap3Theory.beta_normal_form_bnf] THEN 194 `S = K` by PROVE_TAC [chap3Theory.corollary3_2_1] THEN 195 fs[chap2Theory.S_def, chap2Theory.K_def] 196QED 197 198Theorem cnil_cvcons: 199 ��(cnil == cvcons h t) 200Proof 201 strip_tac >> 202 ���cnil @@ S @@ (K @@ (K @@ K)) == cvcons h t @@ S @@ (K @@ (K @@ K))��� 203 by metis_tac[chap2Theory.lameq_rules] >> 204 pop_assum mp_tac >> 205 simp_tac (bsrw_ss()) [cnil_def, wh_cvcons, S_eq_K] 206QED 207 208Definition ctl0_def: 209 ctl0 = 210 LAM "l" ( 211 VAR "l" @@ (cpair @@ cnil @@ cnil) 212 @@ LAM "h" ( 213 LAM "r" ( 214 cpair @@ (csnd @@ VAR "r") 215 @@ (ccons @@ VAR "h" @@ (csnd @@ VAR "r")) 216 ) 217 ) 218 ) 219End 220 221Theorem FV_ctl0[simp]: 222 FV ctl0 = ��� 223Proof 224 simp[ctl0_def, EXTENSION, DISJ_IMP_EQ] 225QED 226 227Triviality ctl0_eqn = brackabs.brackabs_equiv [] ctl0_def 228 229Theorem ctl0_behaviour: 230 ctl0 @@ cnil == cvpr cnil cnil ��� 231 ctl0 @@ (ccons @@ h @@ t) == cpair @@ (csnd @@ (ctl0 @@ t)) @@ 232 (ccons @@ h @@ (csnd @@ (ctl0 @@ t))) ��� 233 ctl0 @@ cvcons h t == cpair @@ (csnd @@ (ctl0 @@ t)) @@ 234 (ccons @@ h @@ (csnd @@ (ctl0 @@ t))) 235Proof 236 simp_tac (bsrw_ss()) [ctl0_eqn, cnil_def, wh_ccons, wh_cvcons ] >> 237 simp_tac (bsrw_ss()) [churchpairTheory.cpair_behaviour] 238QED 239 240Theorem ctl0_thm: 241 ���t. ctl0 @@ cvlist t == cvpr (cvlist (TL t)) (cvlist t) 242Proof 243 Induct_on ���t��� >> 244 asm_simp_tac (bsrw_ss()) [ctl0_behaviour, wh_ccons, 245 churchpairTheory.cpair_behaviour] 246QED 247 248Definition ctl_def: 249 ctl = B @@ cfst @@ ctl0 250End 251 252Theorem FV_ctl[simp]: 253 FV ctl = ��� 254Proof 255 simp[ctl_def] 256QED 257 258Theorem ctl_thm: 259 ctl @@ cvlist ts == cvlist (TL ts) ��� 260 ctl @@ cvcons h (cvlist ts) == cvlist ts 261Proof 262 simp_tac (bsrw_ss()) [ctl_def, ctl0_thm] >> 263 ���cvcons h (cvlist ts) = cvlist (h::ts)��� by simp[] >> pop_assum SUBST1_TAC >> 264 simp_tac (bsrw_ss()) [ctl0_thm, Excl "cvlist_thm"] 265QED 266 267Triviality cvlist_LIST_REL: 268 ���l1 l2. cvlist l1 == cvlist l2 <=> LIST_REL $== l1 l2 269Proof 270 simp[EQ_IMP_THM, cvlist_LIST_REL_cong] >> 271 Induct >> simp[] 272 >- (Cases >> simp[] >> strip_tac >> 273 drule normal_orderTheory.lameq_bnf_of_cong >> 274 fs[cnil_cvcons]) >> 275 rpt gen_tac >> Cases_on ���l2��� >> simp[] 276 >- metis_tac[chap2Theory.lameq_rules, cnil_cvcons] >> 277 strip_tac >> 278 rename [���cvcons h1 (cvlist t1) == cvcons h2 (cvlist t2)���] >> 279 ���cvcons h1 (cvlist t1) @@ S @@ K == cvcons h2 (cvlist t2) @@ S @@ K��� 280 by metis_tac[chap2Theory.lameq_rules] >> 281 full_simp_tac (bsrw_ss()) [wh_cvcons] >> first_x_assum irule >> 282 ���ctl @@ cvcons h1 (cvlist t1) == ctl @@ cvcons h2 (cvlist t2)��� 283 by asm_simp_tac (bsrw_ss()) [] >> 284 pop_assum mp_tac >> simp_tac(bsrw_ss()) [ctl_thm] 285QED 286 287Theorem calc_fn_alist_behaviour: 288 calc_fn_alist @@ church (dBnum (fromTerm t)) @@ church s == 289 cvlist ( 290 MAP 291 (��(i,t). cvpr (church i) (church (force_num t))) 292 (FILTER (bnf o SND) (GENLIST (��i. (i, steps s (t @@ church i))) s)) 293 ) 294Proof 295 SIMP_TAC (bsrw_ss()) [calc_fn_alist_eqn, ctabulate_cvlist, 296 Cong cvlist_genlist_cong, csteps_behaviour, 297 churchpairTheory.cpair_behaviour, 298 cfilter_cvlist, cbnf_behaviour, PULL_EXISTS, 299 MEM_GENLIST, cmap_cvlist 300 ] >> 301 qmatch_abbrev_tac ��� 302 cvlist (MAP f1 (FILTER P1 (GENLIST g1 s))) == 303 cvlist (MAP f2 (FILTER P2 (GENLIST g2 s))) 304 ��� >> 305 qid_spec_tac ���s��� >> Induct >> 306 simp[GENLIST, rich_listTheory.FILTER_SNOC] >> 307 markerLib.UNABBREV_ALL_TAC >> 308 simp_tac (bsrw_ss()) [churchpairTheory.csnd_cvpr, cbnf_behaviour] >> 309 rw[MAP_SNOC] >> fs[cvlist_LIST_REL, LIST_REL_SNOC] >> 310 simp_tac (bsrw_ss()) [churchpairTheory.cpair_behaviour] 311QED 312 313(* cn2bl0 0 n = 0 /\ 314 cn2bl0 (SUC m) n = if n = SUC m then 315 EVEN n :: cn2bl0 m ((n - 1) DIV 2) 316 else cn2bl0 m n 317*) 318Definition cn2bl0_def: 319 cn2bl0 = 320 natrec 321 @@ (LAM "n" cnil) 322 @@ (LAM "m" (LAM "r" (LAM "n" ( 323 ceqnat @@ VAR "n" @@ (csuc @@ VAR "m") 324 @@ (ccons @@ (cis_zero @@ (cmod @@ VAR "n" @@ church 2)) 325 @@ (VAR "r" @@ 326 (cdiv @@ (cpred @@ VAR "n") @@ church 2))) 327 @@ (VAR "r" @@ VAR "n"))))) 328End 329 330Theorem FV_cn2bl0[simp]: 331 FV cn2bl0 = ��� 332Proof 333 simp[EXTENSION, cn2bl0_def, DISJ_IMP_EQ] 334QED 335 336Triviality cn2bl0_eqn = brackabs.brackabs_equiv [] cn2bl0_def 337 338Theorem cn2bl0_thm: 339 ���t n. 340 n ��� t ��� 341 cn2bl0 @@ church t @@ church n == cvlist (MAP cB (n2bl n)) 342Proof 343 simp_tac (bsrw_ss()) [cn2bl0_eqn] >> 344 Induct >> asm_simp_tac (bsrw_ss()) [churchnumTheory.natrec_behaviour] >> 345 qx_gen_tac ���n��� >> strip_tac >> Cases_on ���n = SUC t��� >> 346 asm_simp_tac (bsrw_ss() ++ ARITH_ss) 347 [churchboolTheory.cB_behaviour, DIV_LESS_EQ] >> 348 simp[Once num_to_bool_list_def, SimpR ���$==���] >> 349 simp[EVEN_MOD2] >> 350 Cases_on ���SUC t MOD 2 = 0��� >> simp[] 351 >- (���(SUC t - 2) DIV 2 = t DIV 2��� by intLib.ARITH_TAC >> simp[] >> 352 simp_tac (bsrw_ss()) [wh_ccons]) >> 353 simp_tac (bsrw_ss()) [wh_ccons] 354QED 355 356Definition cn2bl_def: 357 cn2bl = S @@ cn2bl0 @@ I 358End 359 360Theorem FV_cn2bl[simp]: 361 FV cn2bl = ��� 362Proof 363 simp[cn2bl_def, EXTENSION] 364QED 365 366Theorem cn2bl_thm: 367 cn2bl @@ church n == cvlist (MAP cB (n2bl n)) 368Proof 369 simp_tac (bsrw_ss()) [cn2bl_def, cn2bl0_thm] 370QED 371 372Definition cbeq_def: 373 cbeq = LAM "b1" (LAM "b2" (VAR "b1" @@ VAR "b2" @@ (cnot @@ VAR "b2"))) 374End 375 376Theorem FV_cbeq[simp]: 377 FV cbeq = ��� 378Proof 379 simp[cbeq_def, EXTENSION, DISJ_IMP_EQ] 380QED 381 382Triviality cbeq_eqn = brackabs.brackabs_equiv [] cbeq_def 383 384Theorem cbeq_behaviour: 385 cbeq @@ cB b1 @@ cB b2 == cB (b1 = b2) 386Proof 387 simp_tac (bsrw_ss()) [cbeq_eqn] >> Cases_on ���b1��� >> 388 simp_tac (bsrw_ss()) [] 389QED 390 391val _ = export_betarwt "cbeq_behaviour" 392 393Definition cblprefix_def: 394 cblprefix = 395 LAM "l1" ( 396 VAR "l1" 397 @@ (LAM "l2" (cB T)) (* nil case *) 398 @@ (LAM "h" (LAM "r" (LAM "l2" ( 399 cnull @@ VAR "l2" @@ cB F 400 @@ (cbeq @@ VAR "h" @@ (chd @@ VAR "l2") 401 @@ (VAR "r" @@ (ctl @@ VAR "l2")) 402 @@ cB F))))) 403 ) 404End 405 406Theorem FV_cblprefix[simp]: 407 FV cblprefix = ��� 408Proof 409 simp[cblprefix_def, EXTENSION, DISJ_IMP_EQ] 410QED 411 412Triviality cblprefix_eqn = brackabs.brackabs_equiv [] cblprefix_def 413 414Theorem cblprefix_behaviour: 415 cblprefix @@ cnil @@ t == cB T ��� 416 cblprefix @@ cvcons b1t tt1 @@ cnil == cB F ��� 417 cblprefix @@ cvcons (cB b1) (cvlist t1) @@ cvcons (cB b2) (cvlist t2) == 418 if b1 = b2 then cblprefix @@ cvlist t1 @@ cvlist t2 else cB F 419Proof 420 simp_tac (bsrw_ss()) [cblprefix_eqn, wh_cvcons, cnull_def, cnil_def, 421 ctl_thm, wh_chd] >> rw[] >> 422 simp_tac (bsrw_ss()) [cblprefix_eqn, cnull_def] 423QED 424 425Theorem cblprefix_thm: 426 cblprefix @@ cvlist (MAP cB bs1) @@ cvlist (MAP cB bs2) == cB (bs1 ��� bs2) 427Proof 428 map_every qid_spec_tac [���bs2���, ���bs1���] >> Induct >> 429 simp_tac (bsrw_ss()) [cblprefix_behaviour] >> 430 Cases_on ���bs2��� >> simp_tac (bsrw_ss()) [cblprefix_behaviour] >> rw[] 431QED 432 433Definition cevery_def: 434 cevery = 435 LAM "P" (LAM "l" 436 (VAR "l" @@ cB T 437 @@ (LAM "e" (LAM "r" (VAR "r" @@ (VAR "P" @@ VAR "e") @@ cB F))))) 438End 439 440Theorem FV_cevery[simp]: 441 FV cevery = ��� 442Proof 443 simp[cevery_def, EXTENSION, DISJ_IMP_EQ] 444QED 445 446Triviality cevery_eqn = brackabs.brackabs_equiv [] cevery_def 447 448Theorem cevery_behaviour: 449 cevery @@ P @@ cnil == cB T ��� 450 cevery @@ P @@ cvcons h (cvlist t) == 451 cevery @@ P @@ cvlist t @@ (P @@ h) @@ cB F 452Proof 453 simp_tac (bsrw_ss()) [cevery_eqn, wh_cvcons, cnil_def] 454QED 455 456Theorem cevery_thm: 457 (���e. MEM e l ��� ���b. P @@ e == cB b) ��� 458 cevery @@ P @@ cvlist l == cB (EVERY (��t. P @@ t == cB T) l) 459Proof 460 Induct_on ���l��� >> asm_simp_tac(bsrw_ss()) [cevery_behaviour] >> rw[] >> 461 ������b. P @@ h == cB b��� by metis_tac[] >> Cases_on ���b��� >> 462 asm_simp_tac (bsrw_ss()) [] >> 463 Cases_on ���EVERY (��t. P @@ t == cB T) l��� >> asm_simp_tac (bsrw_ss()) [] 464QED 465 466Definition clength_def: 467 clength = LAM "l" (VAR "l" @@ church 0 @@ (LAM "h" csuc)) 468End 469 470Theorem FV_clength[simp]: 471 FV clength = ��� 472Proof 473 simp[EXTENSION,clength_def] 474QED 475 476val clength_eqn = brackabs.brackabs_equiv [] clength_def 477 478Theorem clength_behaviour: 479 clength @@ cnil == church 0 ��� 480 clength @@ (cvcons h (cvlist t)) == csuc @@ (clength @@ cvlist t) 481Proof 482 simp_tac (bsrw_ss()) [clength_eqn, wh_cvcons, cnil_def] 483QED 484 485Theorem clength_thm: 486 clength @@ cvlist t == church (LENGTH t) 487Proof 488 Induct_on ���t��� >> asm_simp_tac (bsrw_ss()) [clength_behaviour] 489QED 490 491Definition cpfree_check_def: 492 cpfree_check = 493 LAM "bl1" (LAM "bl2" ( 494 cor @@ (ceqnat @@ (clength @@ VAR "bl1") @@ (clength @@ VAR "bl2")) 495 @@ (cand @@ 496 (cnot @@ (cblprefix @@ VAR "bl1" @@ VAR "bl2")) @@ 497 (cnot @@ (cblprefix @@ VAR "bl2" @@ VAR "bl1"))) 498 )) 499End 500 501Theorem FV_cpfree_check[simp]: 502 FV cpfree_check = ��� 503Proof 504 simp[cpfree_check_def, EXTENSION, DISJ_IMP_EQ] 505QED 506 507val cpfree_check_eqn = brackabs.brackabs_equiv [] cpfree_check_def 508 509Theorem cpfree_check_behaviour: 510 cpfree_check @@ cvlist (MAP cB bs1) @@ cvlist (MAP cB bs2) == 511 cB (��(bs1 ��� bs2) ��� ��(bs2 ��� bs1)) 512Proof 513 simp_tac(bsrw_ss()) [cpfree_check_eqn, clength_thm, cblprefix_thm] >> 514 Cases_on ���LENGTH bs1 = LENGTH bs2��� >> simp[] 515 >- (rpt strip_tac >> drule prefix_length_lt >> simp[]) >> 516 rw[prefix_def, EQ_IMP_THM] >> metis_tac[] 517QED 518 519Definition cpfree_list_def: 520 cpfree_list = 521 LAM "l" ( 522 VAR "l" @@ (cpair @@ cnil @@ cB T) @@ ( 523 LAM "h" ( 524 LAM "r" ( 525 cpair @@ (ccons @@ VAR "h" @@ (cfst @@ VAR "r")) @@ 526 (cand @@ (csnd @@ VAR "r") 527 @@ (cevery @@ (cpfree_check @@ VAR "h") @@ (cfst @@ VAR "r"))) 528 ) 529 ) 530 ) 531 ) 532End 533 534Theorem FV_cpfree_list[simp]: 535 FV cpfree_list = ��� 536Proof 537 simp[cpfree_list_def, EXTENSION, DISJ_IMP_EQ] 538QED 539 540val cpfree_list_eqn = brackabs.brackabs_equiv [] cpfree_list_def 541 542val lameq_sym = List.nth(CONJUNCTS chap2Theory.lameq_rules, 2) 543 544val temp = 545 CONV_RULE (SIMP_CONV (bsrw_ss()) []) 546 (cpfree_list_eqn 547 |> MATCH_MP (List.nth(CONJUNCTS chap2Theory.lameq_rules, 4)) 548 |> Q.SPEC ���cvlist bls���) |> MATCH_MP lameq_sym 549 550Theorem cpfree_list_behaviour: 551 cpfree_list @@ cnil == cvpr cnil (cB T) ��� 552 cpfree_list @@ (cvcons bl1 (cvlist bls)) == 553 cvpr (cvcons bl1 (cfst @@ (cpfree_list @@ cvlist bls))) 554 (cand @@ (csnd @@ (cpfree_list @@ cvlist bls)) 555 @@ (cevery @@ (cpfree_check @@ bl1) 556 @@ (cfst @@ (cpfree_list @@ cvlist bls)))) 557Proof 558 conj_tac >- 559 simp_tac (bsrw_ss()) [cpfree_list_eqn, cnil_def, 560 churchpairTheory.cpair_behaviour] >> 561 irule (List.nth(CONJUNCTS chap2Theory.lameq_rules, 3)) >> 562 assume_tac (cpfree_list_eqn 563 |> MATCH_MP (List.nth(CONJUNCTS chap2Theory.lameq_rules, 4)) 564 |> Q.SPEC ���cvcons bl1 (cvlist bls)���) >> 565 goal_assum dxrule >> 566 simp_tac (bsrw_ss()) [wh_cvcons, temp] >> 567 simp_tac (bsrw_ss()) [wh_ccons] >> 568 simp_tac (bsrw_ss()) [churchpairTheory.cpair_behaviour] 569QED 570 571Theorem cpfree_list_thm: 572 cpfree_list @@ cvlist (MAP cvlist (MAP (MAP cB) bls)) == 573 cvpr (cvlist (MAP cvlist (MAP (MAP cB) bls))) (cB (prefix_free (set bls))) 574Proof 575 Induct_on ���bls��� >> 576 asm_simp_tac (bsrw_ss()) [cpfree_list_behaviour, Cong cvpr_cong, 577 Cong cvcons_cong] >> 578 gen_tac >> irule cvpr_cong >> simp[] >> 579 simp_tac (bsrw_ss()) [cevery_thm, cpfree_check_behaviour, MEM_MAP, 580 PULL_EXISTS] >> 581 simp_tac (bsrw_ss()) [EVERY_MAP, cpfree_check_behaviour] >> 582 simp[prefix_free_def, EVERY_MEM] >> eq_tac 583 >- (rw[] >> map_every Cases_on [���a = h���, ���b = h���] >> fs[]) >> 584 metis_tac[] 585QED 586 587Definition pfsearch_def: 588 pfsearch = 589 LAM "M" ( 590 LAM "x" ( 591 LAM "i" ( 592 LAM "dom" ( 593 cand @@ (csnd @@ (cpfree_list @@ (cmap @@ cn2bl @@ VAR "dom"))) 594 @@ (cmem @@ VAR "x" @@ VAR "dom") 595 ) @@ (cmap @@ cfst @@ (calc_fn_alist @@ VAR "M" @@ VAR "i")) 596 ) 597 ) 598 ) 599End 600 601Theorem FV_pfsearch[simp]: 602 FV pfsearch = ��� 603Proof 604 simp[pfsearch_def, EXTENSION, DISJ_IMP_EQ] 605QED 606 607val pfsearch_eqn = brackabs.brackabs_equiv [] pfsearch_def 608 609Theorem cvlist_MAP_cong: 610 (���x. f x == g x) ��� 611 cvlist (MAP f l) == cvlist (MAP g l) 612Proof 613 rw[] >> irule cvlist_LIST_REL_cong >> Induct_on ���l��� >> simp[] 614QED 615 616Theorem cvlist_MAP_cong_UNCURRY: 617 l0 = l1 ��� (���x y. MEM (x,y) l1 ��� f x y == g x y) ��� 618 cvlist (MAP (UNCURRY f) l0) == cvlist (MAP (UNCURRY g) l1) 619Proof 620 rw[] >> irule cvlist_LIST_REL_cong >> Induct_on ���l0��� >> 621 simp[pairTheory.FORALL_PROD] 622QED 623 624Theorem pfsearch_thm: 625 pfsearch @@ church M @@ church x @@ church i == 626 cB (x < i ��� bnf (steps i (toTerm (numdB M) @@ church x)) ��� 627 prefix_free { n2bl j | bnf (steps i (toTerm (numdB M) @@ church j)) ��� 628 j < i }) 629Proof 630 ������db. M = dBnum db��� by metis_tac[enumerationsTheory.dBnumdB] >> 631 rw[] >> 632 ������t. db = fromTerm t��� by metis_tac[pure_dBTheory.fromtoTerm] >> rw[]>> 633 simp_tac (bsrw_ss()) [pfsearch_eqn, calc_fn_alist_behaviour, cmap_cvlist, 634 MAP_MAP_o, pairTheory.o_UNCURRY_R, 635 combinTheory.o_ABS_R] >> 636 ������l. cvlist (MAP (��(i,t). 637 cfst @@ cvpr (church i) (church (force_num t))) l) == 638 cvlist (MAP (��(i,t). church i) l) ��� 639 by (gen_tac >> irule cvlist_MAP_cong >> 640 simp_tac (bsrw_ss()) [pairTheory.FORALL_PROD]) >> 641 ������l. cvlist (MAP (��(i,t). 642 cn2bl @@ (cfst @@ cvpr (church i) (church (force_num t)))) 643 l) == 644 cvlist (MAP (��(i,t). cvlist (MAP cB (n2bl i))) l) ��� 645 by (rpt gen_tac >> irule cvlist_MAP_cong >> 646 simp_tac (bsrw_ss()) [pairTheory.FORALL_PROD, cn2bl_thm]) >> 647 asm_simp_tac (bsrw_ss()) [cmem_cvlist, PULL_EXISTS, MEM_MAP, 648 pairTheory.FORALL_PROD, EXISTS_MAP] >> 649 simp[pairTheory.UNCURRY] >> 650 simp_tac (bsrw_ss()) [churchnumTheory.ceqnat_behaviour, EXISTS_MEM, 651 MEM_FILTER, pairTheory.EXISTS_PROD, MEM_GENLIST] >> 652 rpt (pop_assum (K all_tac)) >> 653 ������l. MAP (��(i,t:term). cvlist (MAP cB (n2bl i))) 654 (l:(num # term) list) = 655 MAP cvlist (MAP (MAP cB) (MAP (n2bl o FST) l))��� 656 by (simp[MAP_MAP_o] >> Induct >> simp[pairTheory.FORALL_PROD]) >> 657 pop_assum (simp o single) >> 658 simp_tac (bsrw_ss())[cpfree_list_thm] >> 659 Cases_on ���x < i��� >> simp[] >> 660 Cases_on ���bnf (steps i (t @@ church x))��� >> simp[] >> 661 simp[prefix_free_def, MEM_MAP, PULL_EXISTS, pairTheory.FORALL_PROD, 662 MEM_FILTER, MEM_GENLIST] 663QED 664 665Definition Upf_def: 666 Upf = LAM "Mi" ( 667 cfindleast 668 @@ (pfsearch @@ (cnfst @@ VAR "Mi") @@ (cnsnd @@ VAR "Mi")) 669 @@ LAM "stepcount" (UM @@ VAR "Mi") 670 ) 671End 672 673Theorem FV_Upf[simp]: 674 FV Upf = ��� 675Proof 676 simp[Upf_def, EXTENSION, DISJ_IMP_EQ] 677QED 678 679val Upf_eqn = brackabs.brackabs_equiv [] Upf_def 680 681Definition pfi_def: 682 pfi i ��� prefix_free { n2bl x | Phi i x <> NONE } 683End 684 685Theorem Phi_SOME_lameq: 686 Phi M x = SOME res ��� 687 ���t. toTerm (numdB M) @@ church x == t ��� bnf t ��� force_num t = res 688Proof 689 simp[PhiSOME_UM] >> simp_tac(bsrw_ss()) [UM_def] >> eq_tac 690 >- (qmatch_abbrev_tac ���CBNF_T == church res ��� _��� >> 691 strip_tac >> ���CBNF_T -n->* church res��� by asm_simp_tac (bsrw_ss()) [] >> 692 qunabbrev_tac ���CBNF_T��� >> ���bnf (church res)��� by simp[] >> 693 drule_all cbnf_ofk_works2 >> 694 simp_tac (bsrw_ss()) [cforce_num_behaviour] >> metis_tac[bnf_of_SOME_lameq])>> 695 strip_tac >> 696 ���bnf_of (toTerm (numdB M) @@ church x) = SOME t��� 697 by metis_tac[bnf_of_SOME_lameq] >> 698 drule cbnf_of_works1 >> asm_simp_tac (bsrw_ss()) [] 699QED 700 701Theorem Phi_EQ_NONE_has_bnf: 702 Phi M x = NONE ��� ��has_bnf (toTerm (numdB M) @@ church x) 703Proof 704 simp[PhiNONE_UM] >> simp[normal_orderTheory.has_bnf_of] >> 705 simp_tac (bsrw_ss()) [UM_def] >> eq_tac >> strip_tac 706 >- (drule normal_orderTheory.bnf_of_SOME >> strip_tac >> 707 drule_all cbnf_ofk_works2 >> simp[PULL_EXISTS]) >> 708 drule_all cbnf_of_works1 >> 709 simp_tac (bsrw_ss()) [normal_orderTheory.bnf_bnf_of] 710QED 711 712Theorem Phi_EQ_NONE_bnf_steps: 713 Phi M x = NONE ��� ���n. ��bnf (steps n (toTerm (numdB M) @@ church x)) 714Proof 715 simp[Phi_EQ_NONE_has_bnf, normal_orderTheory.has_bnf_of] >> 716 ������x. (���N:term. x <> SOME N) ��� x = NONE��� by (Cases >> simp[]) >> simp[] >> 717 fs[numsAsCompStatesTheory.bnf_of_EQ_NONE_steps] 718QED 719 720Theorem Upf_succeeds: 721 pfi M ��� Phi M i = SOME res ��� Upf @@ church (M ��� i) == church res 722Proof 723 simp_tac (bsrw_ss()) [Upf_eqn, churchnumTheory.cnfst_behaviour] >> 724 strip_tac >> 725 drule_then (qx_choose_then ���res_t��� strip_assume_tac) PhiSOME_cbnf_ofk >> 726 first_x_assum (qspec_then ���cforce_num��� strip_assume_tac) >> 727 full_simp_tac (bsrw_ss()) [cforce_num_behaviour] >> 728 fs[GSYM chap3Theory.betastar_lameq_bnf, 729 GSYM normal_orderTheory.nstar_betastar_bnf] >> 730 drule cbnf_ofk_works2 >> simp[] >> 731 disch_then (qx_choose_then ���res_t'��� strip_assume_tac) >> 732 fs[stepsTheory.bnf_steps] >> rename [���steps n _ = toTerm _���] >> 733 ���pfsearch @@ church M @@ church i @@ church (MAX (i+1) n) == cB T��� 734 by (simp_tac (bsrw_ss()) [pfsearch_thm] >> conj_tac 735 >- (���bnf (steps n (toTerm (numdB M) @@ church i))��� by simp[] >> 736 Cases_on ���n = MAX (i + 1) n��� >> simp[] >- metis_tac[] >> 737 ���n < MAX (i + 1) n��� by fs[MAX_DEF] >> 738 drule_all stepsTheory.bnf_steps_upwards_closed >> simp[]) >> 739 fs[pfi_def, prefix_free_def, PULL_EXISTS] >> 740 qx_genl_tac [���a���, ���b���] >> 741 disch_then (REPEAT_TCL CONJUNCTS_THEN assume_tac) >> 742 first_x_assum match_mp_tac >> metis_tac[Phi_EQ_NONE_bnf_steps]) >> 743 ������j. ���b. pfsearch @@ church M @@ church i @@ church j == cB b��� 744 by simp_tac (bsrw_ss()) [pfsearch_thm] >> 745 drule_all_then assume_tac churchnumTheory.cfindleast_termI >> 746 asm_simp_tac (bsrw_ss()) [] >> fs[PhiSOME_UM] >> 747 asm_simp_tac (bsrw_ss()) [] 748QED 749 750Theorem Upf_fails1: 751 Phi M i = NONE ��� ��has_bnf (Upf @@ church (M ��� i)) 752Proof 753 rpt strip_tac >> fs[normal_orderTheory.has_bnf_of, PhiNONE_UM] >> 754 full_simp_tac (bsrw_ss()) [Upf_eqn, bnf_of_SOME_lameq] >> 755 ������j. ���b. pfsearch @@ church M @@ church i @@ church j == cB b��� 756 by simp_tac (bsrw_ss()) [pfsearch_thm] >> 757 drule_all_then (qx_choose_then ���res��� strip_assume_tac) 758 churchnumTheory.cfindleast_bnfE >> 759 full_simp_tac (bsrw_ss()) [] >> 760 metis_tac[lameq_sym] 761QED 762 763Theorem Upf_pfree: 764 prefix_free { n2bl i | has_bnf (Upf @@ church (M ��� i)) } 765Proof 766 simp[prefix_free_def, PULL_EXISTS] >> qx_genl_tac [���a���, ���b���] >> 767 simp[normal_orderTheory.has_bnf_of] >> 768 simp_tac (bsrw_ss()) [Upf_eqn, bnf_of_SOME_lameq] >> 769 disch_then (CONJUNCTS_THEN2 (qx_choose_then ���N1��� strip_assume_tac) mp_tac) >> 770 ������j. ���b. pfsearch @@ church M @@ church a @@ church j == cB b��� 771 by simp_tac (bsrw_ss()) [pfsearch_thm] >> 772 drule_all_then (qx_choose_then ���res1��� strip_assume_tac) 773 churchnumTheory.cfindleast_bnfE >> 774 full_simp_tac(bsrw_ss()) [pfsearch_thm] >> 775 disch_then (qx_choose_then ���N2��� strip_assume_tac) >> 776 ������j. ���bl. pfsearch @@ church M @@ church b @@ church j == cB bl��� 777 by simp_tac (bsrw_ss()) [pfsearch_thm] >> 778 drule_all_then (qx_choose_then ���res2��� strip_assume_tac) 779 churchnumTheory.cfindleast_bnfE >> 780 full_simp_tac(bsrw_ss()) [pfsearch_thm] >> 781 Cases_on ���res1 ��� res2��� 782 >- (qpat_x_assum ���prefix_free { n2bl j | _ ��� j < res2}��� mp_tac >> 783 simp[prefix_free_def, PULL_EXISTS] >> disch_then match_mp_tac >> 784 simp[] >> Cases_on ���res1 = res2��� >- metis_tac[] >> 785 ���res1 < res2��� by simp[] >> 786 metis_tac[stepsTheory.bnf_steps_upwards_closed]) >> 787 ���res2 < res1��� by simp[] >> 788 qpat_x_assum ���prefix_free { n2bl j | _ ��� j < res1}��� mp_tac >> 789 simp[prefix_free_def, PULL_EXISTS] >> disch_then match_mp_tac >> 790 simp[] >> metis_tac[stepsTheory.bnf_steps_upwards_closed] 791QED 792 793(* limitMS M s i = M(i) if i < s and M on i terminates in fewer than s steps 794 o/wise, it loops 795*) 796Definition limitMS_def: 797 limitMS = 798 LAM "M" ( 799 LAM "s" ( 800 LAM "i" ( 801 cless @@ VAR "i" @@ VAR "s" @@ ( 802 LAM "t" ( 803 cbnf @@ VAR "t" @@ (cforce_num @@ VAR "t") @@ �� 804 ) @@ ( 805 csteps @@ VAR "s" 806 @@ (cdAPP @@ (cnumdB @@ VAR "M") @@ (cchurch @@ VAR "i")) 807 ) 808 ) @@ �� 809 ) 810 ) 811 ) 812End 813 814Theorem FV_limitMS[simp]: 815 FV limitMS = ��� 816Proof 817 simp[limitMS_def, EXTENSION, DISJ_IMP_EQ] 818QED 819 820val limitMS_eqn = brackabs.brackabs_equiv [] limitMS_def 821 822Theorem Omega_NEQ_church[simp]: 823 ��(�� == church n) ��� ��(church n == ��) 824Proof 825 metis_tac[normal_orderTheory.bnf_of_Omega, bnf_of_SOME_lameq, 826 optionTheory.NOT_NONE_SOME, lameq_sym, churchnumTheory.bnf_church] 827QED 828 829Theorem limitMS_termination_behaviour_eqn: 830 limitMS @@ church M @@ church s @@ church i == church n ��� 831 ���t. steps s (toTerm (numdB M) @@ church i) = t ��� bnf t ��� force_num t = n ��� i < s 832Proof 833 simp_tac (bsrw_ss())[limitMS_eqn, csteps_behaviour, cbnf_behaviour] >> 834 Cases_on ���i < s��� >> asm_simp_tac (bsrw_ss()) [] >> 835 Cases_on ���bnf (steps s (toTerm (numdB M) @@ church i))��� >> 836 asm_simp_tac (bsrw_ss()) [] 837QED 838 839Theorem limitMS_termination_behaviour_I: 840 (���t. steps s (toTerm (numdB M) @@ church i) = t ��� bnf t ��� force_num t = n ��� 841 i < s) 842 ��� 843 limitMS @@ church M @@ church s @@ church i == church n 844Proof 845 metis_tac[limitMS_termination_behaviour_eqn] 846QED 847 848Theorem limitMS_loop_behaviour1: 849 s ��� i ��� ��has_bnf (limitMS @@ church M @@ church s @@ church i) 850Proof 851 simp_tac (bsrw_ss() ++ ARITH_ss)[normal_orderTheory.has_bnf_of, limitMS_eqn] 852QED 853 854Theorem limitMS_looop_behaviour2: 855 ��bnf (steps s (toTerm (numdB M) @@ church i)) ��� 856 ��has_bnf (limitMS @@ church M @@ church s @@ church i) 857Proof 858 simp_tac (bsrw_ss() ++ ARITH_ss)[normal_orderTheory.has_bnf_of, limitMS_eqn] >> 859 Cases_on ���i < s��� >> 860 asm_simp_tac (bsrw_ss() ++ ARITH_ss)[csteps_behaviour, cbnf_behaviour] 861QED 862 863Theorem limitMS_thm: 864 limitMS @@ church M @@ church s @@ church i == 865 if i < s ��� bnf (steps s (toTerm (numdB M) @@ church i)) then 866 UM @@ church (M ��� i) 867 else �� 868Proof 869 simp_tac (bsrw_ss()) [limitMS_eqn] >> Cases_on ���i < s��� >> 870 asm_simp_tac (bsrw_ss()) [cbnf_behaviour, csteps_behaviour] >> 871 Cases_on ���bnf (steps s (toTerm (numdB M) @@ church i))��� >> 872 asm_simp_tac (bsrw_ss()) [cbnf_behaviour, csteps_behaviour, UM_def] >> 873 qabbrev_tac ���Mi = toTerm (numdB M) @@ church i��� >> 874 ���bnf_of Mi = SOME (steps s Mi)��� by metis_tac[stepsTheory.bnf_steps] >> 875 drule cbnf_of_works1 >> simp_tac (bsrw_ss()) [Abbr���Mi���] 876QED 877 878Theorem exists_steps_bnf: 879 (���n. bnf (steps n t)) ��� has_bnf t 880Proof 881 metis_tac[numsAsCompStatesTheory.bnf_of_EQ_NONE_steps, 882 normal_orderTheory.bnf_of_NONE] 883QED 884 885Theorem Upf_SOME_pfree_exists: 886 Upf @@ church (M ��� i) == t ��� bnf t ��� res = force_num t ��� 887 ���N. pfi N ��� Phi N i = SOME res 888Proof 889 simp_tac (bsrw_ss()) [Upf_eqn] >> 890 ������j. ���b. pfsearch @@ church M @@ church i @@ church j == cB b��� 891 by simp_tac (bsrw_ss()) [pfsearch_thm] >> strip_tac >> 892 drule_all_then (qx_choose_then ���step_count��� strip_assume_tac) 893 churchnumTheory.cfindleast_bnfE >> 894 full_simp_tac (bsrw_ss()) [pfsearch_thm] >> 895 qexists_tac ���dBnum (fromTerm (limitMS @@ church M @@ church step_count))��� >> 896 asm_simp_tac (bsrw_ss())[Phi_SOME_lameq, limitMS_thm] >> reverse conj_tac 897 >- metis_tac[lameq_sym, churchnumTheory.bnf_church, 898 churchnumTheory.force_num_church] >> 899 simp[pfi_def, Phi_EQ_NONE_bnf_steps, exists_steps_bnf, 900 normal_orderTheory.has_bnf_of] >> 901 simp_tac (bsrw_ss()) [limitMS_thm] >> pop_assum (K ALL_TAC) >> 902 fs[prefix_free_def, PULL_EXISTS] >> rw[] 903QED 904 905Definition Upfi_def: 906 Upfi = dBnum (fromTerm Upf) 907End 908 909Theorem Upfi_correct1: 910 pfi M ��� (Phi Upfi (M ��� i) = Phi M i) 911Proof 912 simp[SimpLHS, Phi_def, Upfi_def] >> 913 Cases_on ���Phi M i��� 914 >- (drule Upf_fails1 >> simp[GSYM normal_orderTheory.bnf_of_NONE]) >> 915 strip_tac >> drule_all_then strip_assume_tac Upf_succeeds >> 916 asm_simp_tac (bsrw_ss()) [normal_orderTheory.bnf_bnf_of] 917QED 918 919Theorem Upfi_pfree: 920 prefix_free {n2bl i | Phi Upfi (M ��� i) ��� NONE } 921Proof 922 ������x. Phi Upfi x ��� NONE ��� has_bnf (Upf @@ church x)��� 923 suffices_by simp[Upf_pfree] >> 924 simp[Phi_EQ_NONE_has_bnf, Upfi_def] 925QED 926 927Theorem Upfi_SOME_pfree_exists: 928 Phi Upfi (M ��� i) = SOME x ��� ���N. pfi N ��� Phi Upfi (N ��� i) = SOME x 929Proof 930 strip_tac >> csimp[Upfi_correct1] >> irule Upf_SOME_pfree_exists >> 931 fs[Phi_SOME_lameq, Upfi_def] >> metis_tac[] 932QED 933 934val _ = export_theory(); 935