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