1open HolKernel Parse boolLib bossLib 2 3open arithmeticTheory whileTheory logrootTheory pred_setTheory listTheory; 4open recursivefnsTheory; 5open prnlistTheory; 6open primrecfnsTheory; 7open prtermTheory; 8open nlistTheory; 9 10open recfunsTheory; 11open recsetsTheory; 12 13open reductionEval; 14open churchDBTheory; 15 16val _ = new_theory "recdegrees"; 17 18val _ = Datatype`form = BASE num num | EXISTS num form | ALL num form` 19 20Definition MKEA_0[simp]: 21 (MKEA0 0 m R = BASE R (m+1)) ��� 22 (MKEA0 (SUC n) m R = EXISTS (SUC n) (MKAE0 n m R)) ��� 23 (MKAE0 0 m R = BASE R (m+1)) ��� 24 (MKAE0 (SUC n) m R = ALL (SUC n) (MKEA0 n m R)) 25End 26 27Definition MKEA[simp]: 28 MKEA n R = MKEA0 n n R 29End 30 31Definition MKAE[simp]: 32 MKAE n R = MKAE0 n n R 33End 34 35Definition interpret[simp]: 36 (interpret �� (BASE Ri n) <=> 37 Phi Ri (fold (MAP �� (GENLIST I (n)))) = SOME 1) ��� 38 (interpret �� (EXISTS v f) <=> ���n. interpret �����v���n��� f) ��� 39 (interpret �� (ALL v f) <=> ���n. interpret �����v���n��� f) 40End 41 42Definition rec_sigma: 43 rec_sigma n = { 44 A | ���Ri. (���m. (Phi Ri m = SOME 0) ��� (Phi Ri m = SOME 1)) ��� 45 ���x. x���A <=> interpret I���0���x��� (MKEA n Ri) 46 } 47End 48 49Theorem rec_sigma0_corr: 50 A ��� rec_sigma 0 <=> recursive A 51Proof 52 simp[rec_sigma,recursive_def] >> eq_tac >> rw[] >> 53 fs[combinTheory.APPLY_UPDATE_THM] 54 >- (qexists_tac ���Ri��� >> rw[] >> metis_tac[]) 55 >- (qexists_tac ���M��� >> rw[]) 56QED 57 58Theorem rec_cn = List.nth (CONJUNCTS recfn_rules,3) 59 60Theorem recfn_K_2: 61 ���n. recfn (SOME o (K n)) 2 62Proof 63 rw[] >> `primrec (K n) 2` by fs[primrec_K] >> 64 `recfn (SOME ��� (K n)) 2` by fs[primrec_recfn] >> fs[] 65QED 66 67Theorem recfn_proj: 68 ���i n. i<n ==> recfn (SOME o (proj i)) n 69Proof 70 rw[] >> `primrec (proj i) n` by fs[primrec_rules] >> fs[primrec_recfn] 71QED 72 73Theorem recfn_sub: 74 recfn (SOME o (pr2 $-)) 2 75Proof 76 fs[primrec_pr_sub,primrec_recfn] 77QED 78 79Overload not_Phi_npair[local] = ��� 80 ��R. recCn (SOME o (pr2 $-)) [ 81 SOME o (K 1); 82 recCn recPhi [ 83 SOME o (K R); 84 recCn (SOME o (pr2 npair)) [ 85 SOME o (proj 1); 86 SOME o (proj 0) 87 ] 88 ] 89 ]��� 90 91Theorem recfn_recCnminimise_r_npair: 92 ���R. recfn (minimise (not_Phi_npair R)) 1 93Proof 94 strip_tac >> 95 ���recfn (not_Phi_npair R) 2��� suffices_by fs[recfn_rules] >> 96 irule rec_cn >> rw[] 97 >- (`recfn (SOME o (K 1)) 2` by fs[recfn_K_2] >> fs[]) 98 >- (irule rec_cn >> rw[] 99 >- (`recfn (SOME o (K R)) 2` by fs[recfn_K_2] >> fs[]) 100 >- (irule rec_cn >> rw[] 101 >- (fs[recfn_proj]) 102 >- (fs[recfn_proj]) 103 >- (irule primrec_recfn >> simp[primrec_npair]) ) 104 >- (metis_tac[recfn_recPhi,recPhi_rec2Phi]) ) 105 >- (fs[recfn_sub]) 106QED 107 108Theorem recCnminimise_r_npair_corr: 109 not_Phi_npair R [n;e] = 110 if IS_SOME (Phi R (e *, n)) then SOME (1 - THE (Phi R (e *, n))) 111 else NONE 112Proof 113 rw[recCn_def] >> fs[quantHeuristicsTheory.IS_SOME_EQ_NOT_NONE] 114QED 115 116Theorem recCnminimise_r_npair_corr2: 117 IS_SOME (Phi R (e *, n)) ==> 118 not_Phi_npair R [n;e] = SOME (1 - THE (Phi R (e *, n))) 119Proof 120 fs[recCnminimise_r_npair_corr] 121QED 122 123Theorem minimise_useful: 124 minimise f l = SOME n <=> f (n::l) = SOME 0 ��� 125 ���i. i<n ==> ���m. f (i::l) = SOME m ��� 0 < m 126Proof 127 fs[minimise_thm] >> DEEP_INTRO_TAC optionTheory.some_intro >> rw[EQ_IMP_THM] 128 >- simp[] 129 >- metis_tac[] 130 >- (rename[`n1=n2`] >> 131 �����(n1<n2) ��� ��(n2<n1)��� suffices_by simp[] >> 132 rpt strip_tac >> metis_tac[prim_recTheory.LESS_REFL,optionTheory.SOME_11]) 133 >- metis_tac[] 134QED 135 136Definition step_n_def: 137 step_n N = 138 LAM "xn" 139 (cbnf 140 @@ (csteps 141 @@ (cnsnd @@ VAR"xn") 142 @@ (cdAPP 143 @@ (cnumdB @@ church N) 144 @@ (cchurch @@ (cnfst @@ VAR"xn") ) ) ) 145 @@ church 1 146 @@ church 0 ) 147End 148 149val step_n_eqn = brackabs.brackabs_equiv [] (SPEC_ALL step_n_def) 150 151Theorem step_n_behaviour: 152 step_n N @@ church M == 153 church (if (bnf (steps (nsnd M) (toTerm (numdB N) @@ church (nfst M)) ) ) 154 then 1 else 0) 155Proof 156 simp_tac (bsrw_ss()) [step_n_eqn, csteps_behaviour, 157 cbnf_behaviour] >> rw[] >> 158 simp_tac (bsrw_ss()) [churchboolTheory.cB_behaviour] 159QED 160 161Theorem FV_steps_n[simp]: FV (step_n N) = {} 162Proof simp[EXTENSION,step_n_def] 163QED 164 165Theorem cB_true_K: 166 cB T = K 167Proof 168 simp_tac (bsrw_ss()) [churchboolTheory.cB_def] >> 169 fs[chap2Theory.K_def] 170QED 171 172 173 174Theorem cB_false_I: 175 cB F = LAM "x" I 176Proof 177 simp_tac (bsrw_ss()) [brackabsTheory.I_I,churchboolTheory.cB_def] 178QED 179 180 181Theorem cB_church: 182 is_church (cB p) ==> (���n. cB p = church n) 183Proof 184 rw[] >> `���n. cB p = church n` by fs[churchnumTheory.is_church_church] >> 185 metis_tac[] 186QED 187 188Theorem cB_is_church_T: 189 is_church (cB T) 190Proof 191 fs[churchnumTheory.is_church_def,churchboolTheory.cB_def] >> qexists_tac`"y" ` >> 192 qexists_tac`"x"` >> qexists_tac`0` >> rw[] 193QED 194 195Theorem cB_is_church_F: 196 ��is_church (cB F) 197Proof 198 strip_tac >> fs[churchnumTheory.is_church_def,churchboolTheory.cB_def] >> 199 fs[termTheory.LAM_eq_thm] >> Cases_on`n` >> fs[FUNPOW_SUC] 200QED 201 202Theorem force_num_cB_F: 203 force_num (cB F) = 0 204Proof 205 metis_tac[cB_is_church_F,churchnumTheory.force_num_def] 206QED 207 208Theorem force_num_cB_T: 209 force_num (cB T) = 0 210Proof 211 fs[cB_is_church_T,churchnumTheory.force_num_def] >> 212 SELECT_ELIM_TAC >> rw[cB_church,cB_is_church_T] >> 213 fs[churchboolTheory.cB_def,churchnumTheory.church_def, 214 termTheory.LAM_eq_thm] 215 >- (qexists_tac ���0��� >> simp[]) >> 216 Cases_on`x` >> fs[FUNPOW_SUC] 217QED 218 219Theorem force_num_cB: 220 force_num (cB x) = 0 221Proof 222 Cases_on`x` >> fs[force_num_cB_F,force_num_cB_T] 223QED 224 225Theorem bnf_of_church[simp]: 226 bnf_of (church x) = SOME (church x) 227Proof 228 simp[normal_orderTheory.bnf_bnf_of] 229QED 230 231Theorem rec_sigma1_corr: 232 A ��� rec_sigma 1 <=> re A 233Proof 234 simp[rec_sigma,re_semidp] >> eq_tac >> rw[] >> 235 fs[combinTheory.APPLY_UPDATE_THM,theorem "MKEA_0_compute"] 236 >- (qabbrev_tac ���M = not_Phi_npair Ri��� >> 237 ���recfn (minimise M) 1��� by fs[Abbr���M���, recfn_recCnminimise_r_npair] >> 238 drule_then (qx_choose_then ���i��� assume_tac) recfns_in_Phi >> 239 qexists_tac���i��� >> rw[] >> 240 first_x_assum $ qspec_then ���[e]��� mp_tac >> simp[] >> strip_tac >> 241 simp[minimise_useful] >> 242 ������x. IS_SOME (Phi Ri x)��� 243 by metis_tac[optionTheory.IS_SOME_DEF] >> 244 ������x y. M [x;y] = SOME (1 - THE (Phi Ri (y *, x)))��� 245 by (rw[Abbr���M���, recCnminimise_r_npair_corr2] >> fs[]) >> 246 eq_tac >> rw[] 247 >- (qabbrev_tac���mu = LEAST x. Phi Ri (e *, x) = SOME 1��� >> 248 qexists_tac���mu��� >> 249 qunabbrev_tac ���mu��� >> numLib.LEAST_ELIM_TAC >> conj_tac 250 >- metis_tac[] >> simp[] >> rw[] >> 251 rename [���THE (Phi Ri (e *, j))���] >> 252 ���Phi Ri (e *, j) = SOME 0��� suffices_by simp[] >> metis_tac[]) 253 >- (qexists_tac���m��� >> CCONTR_TAC >> 254 ���Phi Ri (e *, m) = SOME 0��� by metis_tac[] >> fs[])) 255 >- (qexists_tac���dBnum (fromTerm (step_n N) )��� >> rw[Phi_def] >> 256 simp_tac (bsrw_ss()) [step_n_behaviour] 257 >- (full_simp_tac (bsrw_ss()) [step_n_behaviour,AllCaseEqs()]) 258 >- (rw[stepsTheory.bnf_steps,AllCaseEqs()])) 259QED 260 261Definition co_re: 262 co_re s = re (COMPL s) 263End 264 265Definition rec_pi: 266 rec_pi n = { 267 A | ���Ri. 268 (���m. (Phi Ri m = SOME 0) ��� (Phi Ri m = SOME 1)) ��� 269 ���x. x ��� A ��� interpret I���0 ��� x��� (MKAE n Ri) 270 } 271End 272 273Theorem rec_pi_0_recursive: 274 A ��� rec_pi 0 <=> recursive A 275Proof 276 ���A ��� rec_pi 0 <=> A ��� rec_sigma 0��� suffices_by metis_tac[rec_sigma0_corr] >> 277 simp[rec_pi,rec_sigma] 278QED 279 280 281Definition co_re_machine: 282 co_re_machine Ri = 283 LAM "e" 284 (cfindleast 285 @@ (LAM "NN" 286 (ceqnat @@ 287 church 0 @@ 288 (cforce_num @@ 289 (cbnf_ofk 290 @@ I 291 @@ (cdAPP @@ (cnumdB @@ church Ri) 292 @@ (cchurch 293 @@ (cnpair @@ VAR "e" @@ VAR "NN"))))))) 294 @@ I) 295End 296 297Theorem FV_co_re_machine[simp]: 298 FV (co_re_machine n) = {} 299Proof 300 simp[co_re_machine,EXTENSION,DISJ_IMP_EQ] >> rw[EQ_IMP_THM] 301QED 302 303val co_re_machine_eqn = brackabs.brackabs_equiv [] (SPEC_ALL co_re_machine) 304 305Theorem rec_pi_1_co_re: 306 A ��� rec_pi 1 <=> co_re A 307Proof 308 simp[rec_pi,re_semidp,co_re] >> eq_tac >> rw[] >> 309 fs[combinTheory.APPLY_UPDATE_THM,theorem "MKEA_0_compute"] 310 >- (qexists_tac���dBnum (fromTerm (co_re_machine Ri))��� >> rw[] >> 311 simp_tac (bsrw_ss()) [co_re_machine_eqn,Phi_def] >> 312 qmatch_abbrev_tac���_ <=> ���z. bnf_of (cfindleast @@ P @@ I) = SOME z��� >> 313 ������n. P @@ church n == cB (Phi Ri (e *, n) = SOME 0)��� 314 by (simp_tac (bsrw_ss()) [Abbr���P���, cdBnum_behaviour] >> 315 qx_gen_tac ���n��� >> 316 last_x_assum (qspec_then ���e ��� n��� mp_tac) >> simp[] >> 317 Cases_on ���Phi Ri (e ��� n) = SOME 1��� >> simp[] >> 318 rpt strip_tac >> pop_assum mp_tac >> simp[Phi_def] >> strip_tac >> 319 drule (GEN_ALL cbnf_of_works1) >> simp[] >> 320 simp_tac (bsrw_ss()) [] >> simp[]) >> 321 ���(���n. ���b. P @@ church n == cB b)��� by metis_tac[] >> 322 eq_tac >> rw[] 323 >- (last_x_assum (qspec_then ���e ��� n��� mp_tac)>> 324 Cases_on ���Phi Ri (e ��� n) = SOME 1��� >> simp[] 325 >- (fs[Phi_def] >> metis_tac[]) >> 326 strip_tac >> 327 ���P @@ church n == cB T��� 328 by (asm_simp_tac (bsrw_ss()) [] >> metis_tac[]) >> 329 drule_all churchnumTheory.cfindleast_termI >> 330 simp_tac (bsrw_ss()) []) 331 >- (���(cfindleast @@ P @@ I) -n->* z ��� bnf z��� 332 by metis_tac[normal_orderTheory.bnf_of_SOME]>> 333 ���(cfindleast @@ P @@ I) == z��� by fs[normal_orderTheory.nstar_lameq] >> 334 drule_all churchnumTheory.cfindleast_bnfE >> rw[] >> 335 qexists_tac���m��� >> qpat_x_assum ���_ @@ _ == cB T��� mp_tac >> 336 asm_simp_tac (bsrw_ss()) [] >> simp[Phi_def] >> rw[] >> fs[] >> 337 metis_tac[DECIDE���0 ��� 1���])) 338 >- (qexists_tac���dBnum (fromTerm (B @@ (cminus @@ church 1) @@ step_n N))��� >> 339 simp[Phi_def] >> 340 simp_tac (bsrw_ss()) [step_n_behaviour,churchnumTheory.cminus_behaviour]>> 341 rw[] >> 342 ONCE_REWRITE_TAC[(DECIDE���(P <=> Q) <=> (��P <=> ��Q)���)] >> 343 PURE_ASM_REWRITE_TAC [] >> 344 simp[Phi_def] >> simp_tac (srw_ss()++boolSimps.COND_elim_ss) [] >> 345 simp[stepsTheory.bnf_steps] ) 346QED 347Definition rec_delta: 348 rec_delta n = rec_sigma n ��� rec_pi n 349End 350 351Definition lnot: 352 lnot M = dBnum (fromTerm (B @@ (cbnf_ofk @@ (B @@ (cminus @@ church 1) 353 @@ cforce_num) ) 354 @@ (B @@ (cdAPP @@ (cnumdB @@ church M)) 355 @@ cchurch ))) 356End 357 358 359Theorem lnot_thm[simp]: 360 Phi (lnot m) n = OPTION_MAP ((-) 1) (Phi m n) 361Proof 362 fs[lnot,Phi_def] >> simp_tac (bsrw_ss()) [] >> 363 Cases_on���bnf_of (toTerm (numdB m) @@ church n)��� >> simp[] 364 >- (drule bnfNONE_cbnf_ofk_fails >> simp[] >> 365 rw[normal_orderTheory.bnf_of_NONE]) >> 366 drule cbnf_of_works1 >> simp[] >> simp_tac (bsrw_ss()) [] 367QED 368 369Theorem lnot_lnot_I: 370 (���m. (Phi n m = SOME 0) ��� (Phi n m = SOME 1)) ==> 371 (Phi (lnot (lnot n)) k = Phi n k) 372Proof 373 rw[] >> Cases_on���Phi n k = SOME 0��� >> simp[] >> 374 ���Phi n k = SOME 1��� by metis_tac[] >> simp[] 375QED 376 377Theorem lnot_01: 378 (���m. (Phi n m = SOME 0) ��� (Phi n m = SOME 1)) ==> 379 ���m. (Phi (lnot n) m = SOME 0) ��� (Phi (lnot n) m = SOME 1) 380Proof 381 rw[] >> Cases_on���(���z. (Phi n m = SOME z) ��� 1 ��� z)��� >> rw[] >> 382 qexists_tac���0��� >> fs[] >> 383 ���Phi n m ��� SOME 1 ��� ��(1 ��� 1)��� by fs[] >- metis_tac[] >- fs[] 384QED 385 386 387Theorem MKAE0_lnot_lnot[simp]: 388 (���m. (Phi R m = SOME 0) ��� (Phi R m = SOME 1)) ==> 389 ���f. (interpret f (MKAE0 n k (lnot (lnot R))) = interpret f (MKAE0 n k R)) ��� 390 (interpret f (MKEA0 n k (lnot (lnot R))) = interpret f (MKEA0 n k R)) 391Proof 392 strip_tac >> Induct_on���n��� >> 393 simp[combinTheory.APPLY_UPDATE_THM,theorem "MKEA_0_compute"] >> 394 rw[EQ_IMP_THM] >> rename [���1 - (1 - u) = 1���] >> 395 Cases_on���u = 1��� >> fs[] >> ���u ��� 0��� by simp[] >> 396 metis_tac[TypeBase.one_one_of ���:�� option���] 397QED 398 399Theorem lnot_interpret: 400 ���k f R. (���m. (Phi R m = SOME 0) ��� (Phi R m = SOME 1)) ==> 401 ((��interpret f (MKEA0 n k R)) ��� interpret f (MKAE0 n k (lnot R))) ��� 402 ((��interpret f (MKAE0 n k R)) ��� interpret f (MKEA0 n k (lnot R))) 403Proof 404 Induct_on���n��� >> simp[combinTheory.APPLY_UPDATE_THM,theorem "MKEA_0_compute"]>> 405 rw[] >> fs[combinTheory.APPLY_UPDATE_THM,theorem "MKEA_0_compute"] >> rw[] >> 406 eq_tac >> rw[] 407 >- (qexists_tac���0��� >> fs[] >>metis_tac[]) 408 >- (���z=0��� by fs[] >> fs[] ) 409QED 410 411Theorem thm1_3_i: 412 COMPL A ��� rec_pi n <=> A ��� rec_sigma n 413Proof 414 simp[rec_pi,rec_sigma] >> eq_tac >> rw[] >> 415 fs[combinTheory.APPLY_UPDATE_THM,lnot_interpret] >> 416 metis_tac[lnot_interpret,lnot_01] 417QED 418 419(* Up to here *) 420 421(* 422Theorem interpret_MKEA0_LT: 423 ���m1 n1 n2 f g m2. (n1<m1 ��� n2<m2 ��� interpret f (MKEA0 n1 n2 Ri)) ==> 424 (interpret g (MKAE0 m1 m2 Ri) ��� interpret g (MKEA0 m1 m2 Ri)) 425Proof 426 Induct_on���m1��� >> fs[] >> rw[] >> Cases_on ���n1 = m1��� >> rw[] 427 >- () 428 >- (���n1 < m1��� by fs[] >> metis_tac[]) 429 >- () 430 >- (qexists_tac���SUC m1��� >> ���n1 < m1��� by fs[] >> metis_tac[]) 431QED 432 433 434Theorem rec_sigma_step: 435 A ��� rec_sigma n ��� A ��� rec_pi n ==> A ��� rec_sigma (SUC n) ��� A ��� rec_pi (SUC n) 436Proof 437 rw[rec_pi,rec_sigma] >> qexists_tac���Ri��� >> rw[] 438QED 439 440 441 442Theorem thm1_3_ii1: 443 ���m n. A ��� rec_sigma n ==> n<m ==> A ��� rec_sigma m ��� rec_pi m 444Proof 445 Induct_on���m��� >> simp[] >> rw[] >> fs[rec_sigma,rec_pi] 446 >- (qexists_tac���Ri��� >> rw[] >> eq_tac >> rw[]) 447 448 >- (Cases_on���A ��� rec_sigma m��� >- (fs[]) >- (fs[] >> �����(n<m)��� by fs[] >> Cases_on���n=m��� >> fs[]) ) 449QED 450 451 452Theorem thm1_3_ii2: 453 rec_pi A n ==> (���m. m>n ==> (rec_sigma A m ��� rec_pi A m) ) 454Proof 455 rw[rec_pi,rec_sigma] 456QED 457 458 459Theorem thm1_3_iii1: 460 rec_sigma A n ��� rec_sigma B n ==> (rec_sigma (A ��� B) n ��� rec_sigma (A ��� B) n) 461Proof 462 463QED 464 465Theorem thm1_3_iii2: 466 rec_pi A n ��� rec_pi B n ==> (rec_pi (A ��� B) n ��� rec_pi (A ��� B) n) 467Proof 468 469QED 470 471Theorem thm1_3_iv: 472 rec_sigma R n ��� n>0 ��� A = {x | ���y. R (x,y)} ==> rec_sigma A n 473Proof 474 475QED 476 477 478*) 479val _ = export_theory() 480