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