1open HolKernel boolLib bossLib Parse binderLib
2
3open chap3Theory
4open pred_setTheory
5open termTheory
6open boolSimps
7open normal_orderTheory
8open churchboolTheory
9open churchpairTheory
10open reductionEval
11open stepsTheory
12
13fun Store_thm(n,t,tac) = store_thm(n,t,tac) before export_rewrites [n]
14
15val _ = new_theory "churchnum"
16
17val _ = set_trace "Unicode" 1
18
19val church_def = Define`
20  church n = LAM "z" (LAM "s" (FUNPOW (APP (VAR "s")) n (VAR "z")))
21`
22
23val FUNPOW_SUC = arithmeticTheory.FUNPOW_SUC
24
25val size_funpow = store_thm(
26  "size_funpow",
27  ``size (FUNPOW (APP f) n x) = (size f + 1) * n + size x``,
28  Induct_on `n` THEN
29  SRW_TAC [ARITH_ss][FUNPOW_SUC, arithmeticTheory.LEFT_ADD_DISTRIB,
30                     arithmeticTheory.MULT_CLAUSES]);
31
32val church_11 = store_thm(
33  "church_11",
34  ``(church m = church n) ��� (m = n)``,
35  SRW_TAC [][church_def, EQ_IMP_THM] THEN
36  POP_ASSUM (MP_TAC o Q.AP_TERM `size`) THEN
37  SRW_TAC [ARITH_ss][size_funpow, arithmeticTheory.LEFT_ADD_DISTRIB]);
38val _ = export_rewrites ["church_11"]
39
40val bnf_church = store_thm(
41  "bnf_church",
42  ``���n. bnf (church n)``,
43  SRW_TAC [][church_def] THEN
44  Induct_on `n` THEN SRW_TAC [][] THEN
45  SRW_TAC [][FUNPOW_SUC]);
46val _ = export_rewrites ["bnf_church"]
47
48val is_abs_church = Store_thm(
49  "is_abs_church",
50  ``is_abs (church n)``,
51  SRW_TAC [][church_def]);
52
53val church_lameq_11 = Store_thm(
54  "church_lameq_11",
55  ``(church m == church n) ��� (m = n)``,
56  SRW_TAC [][EQ_IMP_THM, chap2Theory.lameq_rules] THEN
57  `���Z. church m -��->* Z ��� church n -��->* Z`
58     by METIS_TAC [beta_CR, theorem3_13, prop3_18] THEN
59  `church m = church n`
60     by METIS_TAC [corollary3_2_1, beta_normal_form_bnf, bnf_church] THEN
61  FULL_SIMP_TAC (srw_ss()) []);
62
63val FV_church = store_thm(
64  "FV_church",
65  ``FV (church n) = {}``,
66  SRW_TAC [][church_def] THEN
67  `(n = 0) ��� (���m. n = SUC m)`
68    by METIS_TAC [TypeBase.nchotomy_of ``:num``] THEN
69  SRW_TAC [][] THENL [
70    SRW_TAC [CONJ_ss] [EXTENSION],
71    Q_TAC SUFF_TAC
72          `FV (FUNPOW (APP (VAR "s")) (SUC m) (VAR "z")) = {"s"; "z"}`
73          THEN1 SRW_TAC [CONJ_ss][pred_setTheory.EXTENSION] THEN
74    Induct_on `m` THEN SRW_TAC [][] THENL [
75      SRW_TAC [][EXTENSION],
76      SRW_TAC [][Once FUNPOW_SUC] THEN
77      SRW_TAC [][EXTENSION] THEN METIS_TAC []
78    ]
79  ]);
80val _ = export_rewrites ["FV_church"]
81
82val is_church_def = Define`
83  is_church t =
84    ���f z n. f ��� z ��� (t = LAM z (LAM f (FUNPOW (APP (VAR f)) n (VAR z))))
85`;
86
87
88val church_is_church = Store_thm(
89  "church_is_church",
90  ``is_church (church n)``,
91  SRW_TAC [][is_church_def, church_def] THEN
92  `"z" ��� "s"` by SRW_TAC [][] THEN METIS_TAC []);
93
94val force_num_def = Define`
95  force_num t = if is_church t then (@n. t = church n) else 0
96`;
97
98val force_num_church = Store_thm(
99  "force_num_church",
100  ``force_num (church n) = n``,
101  SRW_TAC [][force_num_def]);
102
103val force_num_church_composed = Store_thm(
104  "force_num_church_composed",
105  ``(force_num o church o f = f) ���
106    (force_num o church = I)``,
107  SRW_TAC [][FUN_EQ_THM]);
108
109val tpm_funpow_app = store_thm(
110  "tpm_funpow_app",
111  ``tpm pi (FUNPOW (APP f) n x) = FUNPOW (APP (tpm pi f)) n (tpm pi x)``,
112  Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC]);
113val _  = export_rewrites ["tpm_funpow_app"]
114
115val FV_funpow_app = store_thm(
116  "FV_funpow_app",
117  ``FV (FUNPOW (APP f) n x) ��� FV f ��� FV x``,
118  Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC]);
119
120val FV_funpow_app_I = store_thm(
121  "FV_funpow_app_I",
122  ``v ��� FV x ��� v ��� FV (FUNPOW (APP f) n x)``,
123  Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC]);
124
125val FV_funpow_app_E = store_thm(
126  "FV_funpow_app_E",
127  ``v ��� FV (FUNPOW (APP f) n x) ��� v ��� FV f ��� v ��� FV x``,
128  MATCH_ACCEPT_TAC (REWRITE_RULE [IN_UNION, SUBSET_DEF] FV_funpow_app));
129
130val fresh_funpow_app_I = store_thm(
131  "fresh_funpow_app_I",
132  ``v ��� FV f ��� v ��� FV x ��� v ��� FV (FUNPOW (APP f) n x)``,
133  METIS_TAC [FV_funpow_app_E]);
134val _ = export_rewrites ["fresh_funpow_app_I"]
135
136val is_church_church = store_thm(
137  "is_church_church",
138  ``is_church t ��� ���n. t = church n``,
139  SRW_TAC [][is_church_def, church_def] THEN
140  Q.EXISTS_TAC `n` THEN SRW_TAC [CONJ_ss][LAM_eq_thm] THEN
141  Cases_on `z = "z"` THEN SRW_TAC [CONJ_ss][] THEN
142  Cases_on `z = "s"` THEN SRW_TAC [CONJ_ss][]);
143
144val force_num_size = store_thm(
145  "force_num_size",
146  ``is_church t ��� (force_num t = size t DIV 2 - 1)``,
147  SRW_TAC [][force_num_def] THEN
148  `���n. t = church n` by METIS_TAC [is_church_church] THEN
149  SRW_TAC [ARITH_ss][church_def, size_funpow] THEN
150  Q_TAC SUFF_TAC `(2 * n + 3) DIV 2 = n + 1` THEN1 DECIDE_TAC THEN
151  MATCH_MP_TAC arithmeticTheory.DIV_UNIQUE THEN Q.EXISTS_TAC `1` THEN
152  DECIDE_TAC);
153
154
155
156
157val SUB_funpow_app = store_thm(
158  "SUB_funpow_app",
159  ``[M:term/v] (FUNPOW (APP f) n x) = FUNPOW (APP ([M/v]f)) n ([M/v]x)``,
160  Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC]);
161val _ = export_rewrites ["SUB_funpow_app"]
162
163val church_thm = bstore_thm(
164  "church_thm",
165  ``church 0 @@ x @@ f == x ���
166    church (SUC n) @@ x @@ f == f @@ (church n @@ x @@ f)``,
167  CONJ_TAC THENL [
168    SIMP_TAC (bsrw_ss()) [church_def] THEN FRESH_TAC THEN
169    ASM_SIMP_TAC (bsrw_ss()) [],
170
171    SIMP_TAC (bsrw_ss()) [church_def] THEN FRESH_TAC THEN
172    ASM_SIMP_TAC (bsrw_ss()) [FUNPOW_SUC]
173  ]);
174
175val csuc_def = Define`
176  csuc = LAM "n" (LAM "z" (LAM "s"
177            (VAR "s" @@ (VAR "n" @@ VAR "z" @@ VAR "s"))))
178`;
179val FV_csuc = Store_thm(
180  "FV_csuc",
181  ``FV csuc = {}``,
182  SRW_TAC [][csuc_def, EXTENSION] THEN METIS_TAC []);
183val bnf_csuc = Store_thm(
184  "bnf_csuc",
185  ``bnf csuc``,
186  SRW_TAC [][csuc_def]);
187
188val csuc_behaviour = bstore_thm(
189  "csuc_behaviour",
190  ``���n. (csuc @@ (church n)) -n->* church (SUC n)``,
191  SIMP_TAC (bsrw_ss()) [csuc_def, church_def, FUNPOW_SUC]);
192
193val church_eq = store_thm(
194  "church_eq",
195  ``(���s. church n ��� VAR s) ��� (���M N. church n ��� M @@ N)``,
196  SRW_TAC [][church_def]);
197val _ = export_rewrites ["church_eq"]
198
199val natrec_def = Define`
200  natrec = LAM "z" (LAM "f" (LAM "n" (
201             csnd @@ (VAR "n"
202                          @@ (cpair @@ church 0 @@ VAR "z")
203                          @@ (LAM "r" (cpair
204                                         @@ (csuc @@ (cfst @@ VAR "r"))
205                                         @@ (VAR "f" @@ (cfst @@ VAR "r")
206                                                     @@ (csnd @@ VAR "r"))))))))
207`;
208
209val FV_natrec = Store_thm(
210  "FV_natrec",
211  ``FV natrec = {}``,
212  SRW_TAC [][natrec_def, EXTENSION] THEN METIS_TAC []);
213infix |> fun x |> f = f x
214val lameq_sub = chap2Theory.lemma2_12 |> CONJUNCTS
215                                      |> hd
216                                      |> UNDISCH
217                                      |> GEN_ALL
218                                      |> DISCH_ALL
219                                      |> GEN_ALL
220
221val natrec_behaviour = bstore_thm(
222  "natrec_behaviour",
223  ``natrec @@ z @@ f @@ church 0 == z ���
224    natrec @@ z @@ f @@ church (SUC n) ==
225       f @@ church n @@ (natrec @@ z @@ f @@ church n)``,
226  CONJ_TAC THENL [
227    SIMP_TAC (srw_ss()) [natrec_def] THEN FRESH_TAC THEN
228    SRW_TAC [][tpm_fresh, lemma14b] THEN
229    ASM_SIMP_TAC (bsrw_ss()) [],
230
231    SIMP_TAC (srw_ss()) [natrec_def] THEN unvarify_tac lameq_sub THEN
232    ASM_SIMP_TAC (bsrw_ss()) [] THEN
233    Q.MATCH_ABBREV_TAC
234      `VAR fs @@ NN0 @@ YY == VAR fs @@ NN1 @@ YY` THEN
235    Q_TAC SUFF_TAC `NN0 == NN1` THEN1 SIMP_TAC (bsrw_ss()) [] THEN
236    markerLib.UNABBREV_ALL_TAC THEN
237    Q.ID_SPEC_TAC `n` THEN Induct THEN ASM_SIMP_TAC (bsrw_ss()) []
238  ]);
239
240val cplus_def = Define`
241  cplus = LAM "m" (LAM "n" (VAR "m" @@ VAR "n" @@ csuc))
242`;
243
244val FV_cplus = Store_thm(
245  "FV_cplus",
246  ``FV cplus = {}``,
247  SRW_TAC [][cplus_def, EXTENSION] THEN METIS_TAC []);
248val is_abs_cplus = Store_thm(
249  "is_abs_cplus",
250  ``is_abs cplus``,
251  SRW_TAC [][cplus_def]);
252
253val cplus_behaviour = bstore_thm(
254  "cplus_behaviour",
255  ``cplus @@ church m @@ church n -n->* church (m + n)``,
256  SIMP_TAC (bsrw_ss()) [cplus_def] THEN Induct_on `m` THEN
257  ASM_SIMP_TAC (bsrw_ss()) [arithmeticTheory.ADD_CLAUSES]);
258
259val cpred_def = Define`
260  cpred = LAM "n" (natrec @@ church 0
261                          @@ (LAM "n0" (LAM "r" (VAR "n0")))
262                          @@ (VAR "n"))
263`;
264val FV_cpred = store_thm(
265  "FV_cpred",
266  ``FV cpred = {}``,
267  SRW_TAC [][cpred_def, EXTENSION] THEN
268  METIS_TAC []);
269val _ = export_rewrites ["FV_cpred"]
270
271val cpred_0 = store_thm(
272  "cpred_0",
273  ``cpred @@ church 0 -n->* church 0``,
274  SIMP_TAC (bsrw_ss()) [cpred_def]);
275
276val cpred_SUC = store_thm(
277  "cpred_SUC",
278  ``cpred @@ church (SUC n) -n->* church n``,
279  SIMP_TAC (bsrw_ss()) [cpred_def]);
280
281val cpred_behaviour = bstore_thm(
282  "cpred_behaviour",
283  ``cpred @@ church n -n->* church (PRE n)``,
284  Cases_on `n` THEN SRW_TAC [][cpred_SUC, cpred_0]);
285
286val cminus_def = Define`
287  cminus = LAM "m" (LAM "n" (VAR "n" @@ VAR "m" @@ cpred))
288`;
289val FV_cminus = Store_thm(
290  "FV_cminus",
291  ``FV cminus = {}``,
292  SRW_TAC [][cminus_def, EXTENSION] THEN METIS_TAC []);
293val is_abs_cminus = Store_thm(
294  "is_abs_cminus",
295  ``is_abs cminus``,
296  SRW_TAC [][cminus_def]);
297
298val cminus_behaviour = bstore_thm(
299  "cminus_behaviour",
300  ``cminus @@ church m @@ church n -n->* church (m - n)``,
301  SIMP_TAC (bsrw_ss()) [cminus_def] THEN
302  Q.ID_SPEC_TAC `m` THEN Induct_on `n` THEN
303  ASM_SIMP_TAC (bsrw_ss()) [DECIDE ``m - SUC n = PRE (m - n)``]);
304
305val cmult_def = Define`
306  cmult = LAM "m" (LAM "n" (VAR "m" @@ church 0 @@ (cplus @@ VAR "n")))
307`;
308val FV_cmult = Store_thm(
309  "FV_cmult",
310  ``FV cmult = {}``,
311  SRW_TAC [][cmult_def, EXTENSION] THEN METIS_TAC []);
312
313val cmult_behaviour = bstore_thm(
314  "cmult_behaviour",
315  ``cmult @@ church m @@ church n -n->* church (m * n)``,
316  SIMP_TAC (bsrw_ss()) [cmult_def] THEN Induct_on `m` THEN
317  ASM_SIMP_TAC (bsrw_ss() ++ ARITH_ss) [arithmeticTheory.MULT_CLAUSES]);
318
319(* predicates/relations *)
320val cis_zero_def = Define`
321  cis_zero = LAM "n" (VAR "n" @@ cB T @@ (LAM "x" (cB F)))
322`;
323val FV_cis_zero = Store_thm(
324  "FV_cis_zero",
325  ``FV cis_zero = {}``,
326  SRW_TAC [][cis_zero_def, EXTENSION]);
327val bnf_cis_zero = Store_thm(
328  "bnf_cis_zero",
329  ``bnf cis_zero``,
330  SRW_TAC [][cis_zero_def]);
331
332val cis_zero_behaviour = bstore_thm(
333  "cis_zero_behaviour",
334  ``cis_zero @@ church n -n->* cB (n = 0)``,
335  Cases_on `n` THEN
336  ASM_SIMP_TAC (bsrw_ss()) [cis_zero_def]);
337
338val wh_cis_zero = store_thm(
339  "wh_cis_zero",
340  ``cis_zero @@ church n -w->* cB (n = 0)``,
341  SRW_TAC [][cis_zero_def, church_def] THEN
342  ASM_SIMP_TAC (whfy(srw_ss())) [] THEN
343  Cases_on `n` THEN SRW_TAC [][FUNPOW_SUC] THEN
344  ASM_SIMP_TAC (whfy(srw_ss())) []);
345
346val ceqnat_def = Define`
347  ceqnat =
348  LAM "n"
349    (VAR "n"
350       @@ cis_zero
351       @@ (LAM "r" (LAM "m"
352            (cand @@ (cnot @@ (cis_zero @@ (VAR "m")))
353                  @@ (VAR "r" @@ (cpred @@ (VAR "m")))))))
354`;
355val FV_ceqnat = Store_thm(
356  "FV_ceqnat",
357  ``FV ceqnat = {}``,
358  SRW_TAC [][ceqnat_def, EXTENSION] THEN METIS_TAC []);
359
360val ceqnat_behaviour = bstore_thm(
361  "ceqnat_behaviour",
362  ``ceqnat @@ church n @@ church m -n->* cB (n = m)``,
363  SIMP_TAC (bsrw_ss()) [ceqnat_def] THEN
364  Q.ID_SPEC_TAC `m` THEN Induct_on `n` THEN1
365    SIMP_TAC (bsrw_ss()) [EQ_SYM_EQ] THEN
366  ASM_SIMP_TAC (bsrw_ss()) [] THEN
367  Cases_on `m` THEN SRW_TAC [][])
368
369(* $< 0 = ��n. not (is_zero n)
370   $< (SUC m) = ��n. not (is_zero n) ��� $< m (PRE n)
371*)
372val cless_def = Define`
373  cless = LAM "m"
374            (VAR "m" @@ (LAM "n" (cnot @@ (cis_zero @@ VAR "n")))
375                     @@ (LAM "r"
376                         (LAM "n" (cand
377                                     @@ (cnot @@ (cis_zero @@ VAR "n"))
378                                     @@ (VAR "r" @@ (cpred @@ VAR "n"))))))
379`;
380val FV_cless = Store_thm(
381  "FV_cless",
382  ``FV cless = {}``,
383  SRW_TAC [][cless_def, EXTENSION] THEN METIS_TAC []);
384val is_abs_cless = Store_thm(
385  "is_abs_cless",
386  ``is_abs cless``,
387  SRW_TAC [][cless_def]);
388
389val cless_behaviour = bstore_thm(
390  "cless_behaviour",
391  ``cless @@ church m @@ church n -n->* cB (m < n)``,
392  SIMP_TAC (bsrw_ss()) [cless_def] THEN
393  Q.ID_SPEC_TAC `n` THEN Induct_on `m` THENL [
394    SIMP_TAC (bsrw_ss()) [arithmeticTheory.NOT_ZERO_LT_ZERO],
395    ASM_SIMP_TAC (bsrw_ss()) [] THEN
396    Cases_on `n` THEN SRW_TAC [][]
397  ]);
398
399(* ----------------------------------------------------------------------
400    divmod
401
402    Functional presentation would be
403
404     divmod (a,p,q) = if q = 0 then (0,0) else
405                      if p < q then (a,p)
406                      else divmod (a+1,p-q,q)
407
408    But this is not primitive recursive.  We make it so by passing in
409    an extra argument which is the "target" value for the next recursive
410    step.  The primitive recursion does nothing until it hits a target
411    value, which it then can set up appropriately for the next bit.
412
413    In this setting the "target" is parameter p, which is where the
414    recursion is happening.
415
416     divmod 0 (a,p,q) = if p < q then (a,p) else (0,0)
417     divmod (SUC n) (a,p,q) =
418       if SUC n = p then
419         if p < q then (a,p)
420         else divmod n (a+1,p-q,q)
421       else divmod n (a,p,q)
422
423     We can optimise a little by having q be lifted past the recursion.
424
425   ---------------------------------------------------------------------- *)
426
427val cdivmodt_def = Define`
428  cdivmodt = LAM "q"
429   (LAM "n"
430    (natrec
431      @@ cpair
432      @@ (LAM "n0" (LAM "r" (LAM "a" (LAM "p"
433              (ceqnat @@ (csuc @@ VAR "n0") @@ VAR "p"
434                      @@ (cless @@ VAR "p" @@ VAR "q"
435                           @@ (cpair @@ VAR "a" @@ VAR "p")
436                           @@ (VAR "r" @@
437                                 (csuc @@ VAR "a") @@
438                                 (cminus @@ VAR "p" @@ VAR "q")))
439                      @@ (VAR "r" @@ VAR "a" @@ VAR "p"))))))
440      @@ VAR "n"))
441`;
442
443val FV_cdivmodt = Store_thm(
444  "FV_cdivmodt",
445  ``FV cdivmodt = {}``,
446  SRW_TAC [][cdivmodt_def, EXTENSION] THEN METIS_TAC []);
447
448val cdivmodt_behaviour = store_thm(
449  "cdivmodt_behaviour",
450  ``���p a.
451       0 < q ��� p ��� n ���
452       cdivmodt @@ church q @@ church n @@ church a @@ church p -n->*
453       cvpr (church (a + p DIV q)) (church (p MOD q))``,
454  SIMP_TAC (bsrw_ss()) [cdivmodt_def, cpair_behaviour] THEN
455  Induct_on `n` THENL [
456    SIMP_TAC (bsrw_ss()) [arithmeticTheory.ZERO_DIV, cpair_behaviour],
457
458    ASM_SIMP_TAC (bsrw_ss()) [] THEN
459    REPEAT STRIP_TAC THEN
460    Cases_on `p = SUC n` THEN ASM_SIMP_TAC (bsrw_ss()) [] THENL [
461      Cases_on `SUC n < q` THEN ASM_SIMP_TAC (bsrw_ss()) [] THENL [
462        ASM_SIMP_TAC (bsrw_ss()) [arithmeticTheory.LESS_DIV_EQ_ZERO],
463        ASM_SIMP_TAC (bsrw_ss() ++ ARITH_ss) [] THEN
464        `(SUC n - q) DIV q = SUC n DIV q - 1`
465           by (MP_TAC (Q.INST [`n` |-> `q`, `q` |-> `1`,
466                                    `m` |-> `SUC n`]
467                                   arithmeticTheory.DIV_SUB) THEN
468               SRW_TAC [ARITH_ss][]) THEN
469        `(SUC n - q) MOD q = SUC n MOD q`
470           by (MP_TAC (Q.INST [`n` |-> `q`, `q` |-> `1`, `m` |-> `SUC n`]
471                              arithmeticTheory.MOD_SUB) THEN
472               SRW_TAC [ARITH_ss][]) THEN
473        SRW_TAC [ARITH_ss][] THEN
474        `���x y. (x = y) ��� x == y` by SRW_TAC [][] THEN
475        POP_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN
476        Q_TAC SUFF_TAC `0 < SUC n DIV q` THEN1 DECIDE_TAC THEN
477        SRW_TAC [ARITH_ss][arithmeticTheory.X_LT_DIV]
478      ],
479      SRW_TAC [ARITH_ss][]
480    ]
481  ]);
482
483val cdiv_def = Define`
484  cdiv =
485  LAM "p" (LAM "q"
486    (cfst @@ (cdivmodt @@ VAR "q" @@ VAR "p" @@ church 0 @@ VAR "p")))
487`
488val FV_cdiv = Store_thm(
489  "FV_cdiv",
490  ``FV cdiv = {}``,
491  SIMP_TAC bool_ss [cdiv_def, EXTENSION, NOT_IN_EMPTY] THEN
492  SRW_TAC [][FRESH_APP, FRESH_LAM]);
493
494val cdiv_behaviour = bstore_thm(
495  "cdiv_behaviour",
496  ``0 < q ���
497      cdiv @@ church p @@ church q -n->* church (p DIV q)``,
498  SIMP_TAC (bsrw_ss()) [cdivmodt_behaviour, cdiv_def]);
499
500val cmod_def = Define`
501  cmod = LAM "p" (LAM "q"
502           (csnd @@ (cdivmodt @@ VAR "q" @@ VAR "p" @@ church 0 @@ VAR "p")))
503`;
504val FV_cmod = Store_thm(
505  "FV_cmod",
506  ``FV cmod = {}``,
507  SRW_TAC [][cmod_def, EXTENSION] THEN METIS_TAC [])
508
509val cmod_behaviour = bstore_thm(
510  "cmod_behaviour",
511  ``0 < q ���
512     cmod @@ church p @@ church q -n->* church (p MOD q)``,
513  SIMP_TAC (bsrw_ss()) [cdivmodt_behaviour, cmod_def]);
514
515(* ----------------------------------------------------------------------
516    Pairs of numbers
517   ---------------------------------------------------------------------- *)
518
519val cnvpr_def = Define`
520  cnvpr (n,m) = cvpr (church n) (church m)
521`;
522
523val bnf_cnvpr = Store_thm(
524  "bnf_cnvpr",
525  ``bnf (cnvpr p)``,
526  Cases_on `p` THEN SRW_TAC [][cnvpr_def]);
527
528val FV_cnvpr = Store_thm(
529  "FV_cnvpr",
530  ``FV (cnvpr p) = {}``,
531  Cases_on `p` THEN SRW_TAC [][cnvpr_def]);
532
533val cfst_cnvpr = bstore_thm(
534  "cfst_cnvpr",
535  ``cfst @@ cnvpr p -n->* church (FST p)``,
536  Cases_on `p` THEN SIMP_TAC (bsrw_ss())[cnvpr_def]);
537val csnd_cnvpr = bstore_thm(
538  "csnd_cnvpr",
539  ``csnd @@ cnvpr p -n->* church (SND p)``,
540  Cases_on `p` THEN SIMP_TAC (bsrw_ss())[cnvpr_def]);
541
542
543(* ----------------------------------------------------------------------
544    Numeric pairing
545   ---------------------------------------------------------------------- *)
546
547open numpairTheory
548
549(* triangular numbers and the tri����� function *)
550val ctri_def = Define`
551  ctri = LAM "n" (natrec @@ church 0
552                         @@ (LAM "n0" (cplus @@ (csuc @@ VAR "n0")))
553                         @@ VAR "n")
554`;
555
556val FV_ctri = Store_thm(
557  "FV_ctri",
558  ``FV ctri = {}``,
559  SRW_TAC [][ctri_def, EXTENSION] THEN METIS_TAC []);
560
561val ctri_behaviour = bstore_thm(
562  "ctri_behaviour",
563  ``ctri @@ church n -n->* church (tri n)``,
564  SIMP_TAC (bsrw_ss()) [ctri_def] THEN
565  Induct_on `n` THEN
566  ASM_SIMP_TAC (bsrw_ss()) [tri_def]);
567
568(* invtri0
569    |- ���n a.
570         invtri0 n a =
571         if n < a + 1 then (n,a) else invtri0 (n ��� (a + 1)) (a + 1) : thm
572   make it prim. rec. by using a target parameter, as with divmod
573*)
574
575val cinvtri0_def = Define`
576  cinvtri0 =
577  natrec
578    @@ (LAM "n" (LAM "a" (cvpr (VAR "n") (VAR "a"))))
579    @@ (LAM "t0" (LAM "r" (LAM "n" (LAM "a"
580          (ceqnat @@ (csuc @@ (VAR "t0")) @@ VAR "n"
581                  @@ (cless @@ VAR "n" @@ (csuc @@ VAR "a")
582                            @@ cvpr (VAR "n") (VAR "a")
583                            @@ (VAR "r"
584                                    @@ (cminus @@ VAR "n"
585                                               @@ (csuc @@ VAR "a"))
586                                    @@ (csuc @@ VAR "a")))
587                  @@ (VAR "r" @@ VAR "n" @@ VAR "a"))))))
588`;
589(* have messed my naming up here in order to keep the "n" and "a" of the
590   original definition.  "t" is the parameter that is being recursed on,
591   and "n" is the target parameter that causes things to happen when t reaches
592   it. *)
593
594val FV_cinvtri0 = Store_thm(
595  "FV_cinvtri0",
596  ``FV cinvtri0 = {}``,
597  SRW_TAC [][cinvtri0_def, EXTENSION] THEN METIS_TAC []);
598
599val cinvtri0_behaviour = store_thm(
600  "cinvtri0_behaviour",
601  ``n ��� t ���
602    cinvtri0 @@ church t @@ church n @@ church a -n->*
603    cnvpr (invtri0 n a)``,
604  SIMP_TAC (bsrw_ss()) [cinvtri0_def] THEN
605  Q.ID_SPEC_TAC `n` THEN Q.ID_SPEC_TAC `a` THEN
606  Induct_on `t` THENL [
607    SIMP_TAC (bsrw_ss()) [] THEN
608    ONCE_REWRITE_TAC [invtri0_def] THEN
609    SIMP_TAC (srw_ss() ++ ARITH_ss) [cnvpr_def],
610
611    SIMP_TAC (bsrw_ss()) [] THEN
612    REPEAT STRIP_TAC THEN Cases_on `n = SUC t` THEN
613    ASM_SIMP_TAC (bsrw_ss()) [] THENL [
614      Cases_on `t < a` THENL [
615        ASM_SIMP_TAC (bsrw_ss()) [] THEN
616        ONCE_REWRITE_TAC [invtri0_def] THEN
617        SRW_TAC [ARITH_ss][cnvpr_def],
618
619        ASM_SIMP_TAC (bsrw_ss()) [] THEN
620        CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [invtri0_def])) THEN
621        SRW_TAC [ARITH_ss][] THEN
622        `SUC t - (a + 1) = t - a` by DECIDE_TAC THEN
623        SRW_TAC [][arithmeticTheory.ADD1]
624      ],
625
626      `n ��� t` by DECIDE_TAC THEN
627      ASM_SIMP_TAC (bsrw_ss()) []
628    ]
629  ]);
630
631val cinvtri_def = Define`
632  cinvtri =
633  LAM "n" (csnd @@ (cinvtri0 @@ VAR "n" @@ VAR "n" @@ church 0))
634`;
635
636val FV_cinvtri = Store_thm(
637  "FV_cinvtri",
638  ``FV cinvtri = {}``,
639  SRW_TAC [][cinvtri_def, EXTENSION] THEN METIS_TAC []);
640
641val cinvtri_behaviour = bstore_thm(
642  "cinvtri_behaviour",
643  ``cinvtri @@ church n -n->* church (tri����� n)``,
644  SIMP_TAC (bsrw_ss()) [cinvtri_def, cinvtri0_behaviour, invtri_def]);
645
646(* -- The pairing function and fst and snd *)
647
648val cnpair_def = Define`
649  cnpair =
650  LAM "n" (LAM "m"
651    (cplus @@ (ctri @@ (cplus @@ VAR "n" @@ VAR "m")) @@ VAR "m"))
652`;
653
654val FV_cnpair = Store_thm(
655  "FV_cnpair",
656  ``FV cnpair = {}``,
657  SRW_TAC [][cnpair_def, EXTENSION] THEN METIS_TAC []);
658
659val cnpair_behaviour = bstore_thm(
660  "cnpair_behaviour",
661  ``cnpair @@ church n @@ church m -n->* church (n ��� m)``,
662  SIMP_TAC (bsrw_ss()) [cnpair_def, npair_def]);
663
664(* cnfst *)
665val cnfst_def = Define`
666  cnfst = LAM "n" (cminus
667                     @@ (cplus @@ (ctri @@ (cinvtri @@ VAR "n"))
668                               @@ (cinvtri @@ VAR "n"))
669                     @@ VAR "n")
670`;
671
672val FV_cnfst = Store_thm(
673  "FV_cnfst",
674  ``FV cnfst = {}``,
675  SRW_TAC [][cnfst_def, EXTENSION] THEN METIS_TAC []);
676
677val cnfst_behaviour = bstore_thm(
678  "cnfst_behaviour",
679  ``cnfst @@ church p -n->* church (nfst p)``,
680  SIMP_TAC (bsrw_ss()) [cnfst_def, nfst_def]);
681
682(* cnsnd *)
683val cnsnd_def = Define`
684  cnsnd = LAM "n" (cminus @@ VAR "n"
685                          @@ (ctri @@ (cinvtri @@ VAR "n")))
686`;
687
688val FV_cnsnd = Store_thm(
689  "FV_cnsnd",
690  ``FV cnsnd = {}``,
691  SRW_TAC [][cnsnd_def, EXTENSION] THEN METIS_TAC []);
692
693val cnsnd_behaviour = bstore_thm(
694  "cnsnd_behaviour",
695  ``cnsnd @@ church p -n->* church (nsnd p)``,
696  SIMP_TAC (bsrw_ss()) [cnsnd_def, nsnd_def]);
697
698(* ----------------------------------------------------------------------
699    cfindleast
700   ---------------------------------------------------------------------- *)
701
702val cfindbody_def = Define`
703  cfindbody P N k =
704    let lp = NEW (FV P ��� FV k) in
705    let nv = NEW (FV P ��� FV k ��� {lp})
706    in
707        Yf (LAM lp (LAM nv (P @@ VAR nv
708                              @@ (k @@ VAR nv)
709                              @@ (VAR lp @@ (csuc @@ VAR nv))))) @@ N
710`;
711
712val fresh_cfindbody = store_thm(
713  "fresh_cfindbody",
714  ``lp ��� FV P ��� lp ��� FV k ��� nv ��� lp ��� nv ��� FV P ��� nv ��� FV k ���
715    (cfindbody P N k =
716     Yf (LAM lp (LAM nv (P @@ VAR nv @@ (k @@ VAR nv)
717                           @@ (VAR lp @@ (csuc @@ VAR nv))))) @@
718     N)``,
719  SRW_TAC [][LET_THM, cfindbody_def] THEN
720  binderLib.NEW_ELIM_TAC THEN REPEAT STRIP_TAC THEN
721  binderLib.NEW_ELIM_TAC THEN REPEAT STRIP_TAC THEN
722  SRW_TAC [][termTheory.LAM_eq_thm, termTheory.tpm_fresh] THEN
723  Cases_on `nv = v` THEN SRW_TAC [][termTheory.tpm_fresh] THEN
724  Cases_on `lp = v'` THEN SRW_TAC [][termTheory.tpm_fresh] THEN
725  METIS_TAC []);
726
727val cfindbody_SUB = Store_thm(
728  "cfindbody_SUB",
729  ``[Q/v] (cfindbody P N k) = cfindbody ([Q/v]P) ([Q/v]N) ([Q/v]k)``,
730  Q_TAC (NEW_TAC "lp") `FV P ��� FV k ��� FV Q ��� {v}` THEN
731  Q_TAC (NEW_TAC "nv") `FV P ��� FV k ��� FV Q ��� {v;lp}` THEN
732  `cfindbody P N k = Yf (LAM lp (LAM nv (P @@ VAR nv @@ (k @@ VAR nv)
733                                           @@ (VAR lp @@ (csuc @@ VAR nv))))) @@
734                     N`
735    by SRW_TAC [][fresh_cfindbody] THEN
736  `cfindbody ([Q/v]P) ([Q/v]N) ([Q/v]k) =
737   Yf (LAM lp (LAM nv ([Q/v]P @@ VAR nv @@ ([Q/v]k @@ VAR nv)
738                            @@ (VAR lp @@ (csuc @@ VAR nv))))) @@ [Q/v]N`
739    by (MATCH_MP_TAC (GEN_ALL fresh_cfindbody) THEN
740        SRW_TAC [][chap2Theory.NOT_IN_FV_SUB]) THEN
741  SRW_TAC [][termTheory.lemma14b]);
742
743val cfindbody_thm = store_thm(
744  "cfindbody_thm",
745  ``cfindbody P N k -w->* P @@ N @@ (k @@ N) @@ cfindbody P (csuc @@ N) k``,
746  unvarify_tac head_reductionTheory.whstar_substitutive THEN
747  SRW_TAC [][termTheory.lemma14b] THEN
748  Q_TAC (NEW_TAC "z") `{Ps; ks}` THEN
749  Q_TAC (NEW_TAC "nv") `{Ps; z; ks}` THEN
750  `���N. cfindbody (VAR Ps) N (VAR ks) =
751       Yf (LAM z (LAM nv (VAR Ps @@ VAR nv @@ (VAR ks @@ VAR nv)
752                              @@ (VAR z @@ (csuc @@ VAR nv)))))
753       @@ N`
754     by SRW_TAC [][fresh_cfindbody] THEN
755  ASM_SIMP_TAC (whfy (srw_ss())) [MATCH_MP relationTheory.RTC_SUBSET
756                                           head_reductionTheory.whY2]);
757
758val cfindbody_cong = store_thm(
759  "cfindbody_cong",
760  ``P == P' ��� N == N' ��� k == k' ��� cfindbody P N k == cfindbody P' N' k'``,
761  Q_TAC (NEW_TAC "lp") `FV P ��� FV P' ��� FV k ��� FV k'` THEN
762  Q_TAC (NEW_TAC "nv") `FV P ��� FV P' ��� FV k ��� FV k' ��� {lp}` THEN
763  REPEAT STRIP_TAC THEN
764  `(cfindbody P N k = Yf (LAM lp (LAM nv (P @@ VAR nv @@ (k @@ VAR nv)
765                                         @@ (VAR lp @@ (csuc @@ VAR nv))))) @@
766                   N) ���
767   (cfindbody P' N' k' =
768      Yf (LAM lp (LAM nv (P' @@ VAR nv @@ (k' @@ VAR nv)
769                             @@ (VAR lp @@ (csuc @@ VAR nv))))) @@
770      N')`
771    by SRW_TAC [][fresh_cfindbody] THEN
772  ASM_SIMP_TAC (bsrw_ss()) []);
773
774val bnf_cfindbody = Store_thm(
775  "bnf_cfindbody",
776  ``��bnf (cfindbody P N k)``,
777  SRW_TAC [][cfindbody_def, LET_THM]);
778
779val FV_cfindbody = Store_thm(
780  "FV_cfindbody",
781  ``FV (cfindbody P N k) = FV P ��� FV N ��� FV k``,
782  SRW_TAC [][cfindbody_def, EXTENSION, LET_THM] THEN
783  NEW_ELIM_TAC THEN SRW_TAC [][] THEN
784  NEW_ELIM_TAC THEN SRW_TAC [][] THEN METIS_TAC []);
785
786val cfindleast_def = Define`
787  cfindleast = LAM "P" (LAM "k" (cfindbody (VAR "P") (church 0) (VAR "k")))
788`;
789
790val FV_cfindleast = Store_thm(
791  "FV_cfindleast",
792  ``FV cfindleast = {}``,
793  SRW_TAC [][cfindleast_def, pred_setTheory.EXTENSION] THEN METIS_TAC []);
794
795val cfindleast_behaviour = store_thm(
796  "cfindleast_behaviour",
797  ``cfindleast @@ P @@ k == cfindbody P (church 0) k``,
798  SIMP_TAC (bsrw_ss()) [cfindleast_def] THEN
799  Q_TAC (NEW_TAC "kk") `FV P ��� {"P"; "k"}` THEN
800  `LAM "k" (cfindbody (VAR "P") (church 0) (VAR "k")) =
801   LAM kk (cfindbody (VAR "P") (church 0) (VAR kk))`
802     by (`cfindbody (VAR "P") (church 0) (VAR kk) =
803           [VAR kk/"k"] (cfindbody (VAR "P") (church 0) (VAR "k"))`
804           by SRW_TAC [][termTheory.lemma14b] THEN
805         POP_ASSUM SUBST1_TAC THEN
806         MATCH_MP_TAC termTheory.SIMPLE_ALPHA THEN SRW_TAC [][]) THEN
807  POP_ASSUM SUBST_ALL_TAC THEN
808  ASM_SIMP_TAC (bsrw_ss()) []);
809
810val cfindleast_termI = store_thm(
811  "cfindleast_termI",
812  ``(���n. ���b. P @@ church n == cB b) ��� P @@ church n == cB T ���
813    cfindleast @@ P @@ k == k @@ church (LEAST n. P @@ church n == cB T)``,
814  STRIP_TAC THEN numLib.LEAST_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN
815  POP_ASSUM (K ALL_TAC) THEN
816  SIMP_TAC (bsrw_ss()) [cfindleast_behaviour] THEN
817  Q_TAC SUFF_TAC
818    `���p n. p ��� n ���
819           (���m. m < n ��� ��(P @@ church m == cB T)) ���
820           P @@ church n == cB T ���
821           cfindbody P (church p) k == k @@ church n`
822    THEN1 METIS_TAC [DECIDE ``0 ��� n``] THEN
823  Induct_on `n - p` THEN REPEAT STRIP_TAC THENL [
824    `p = n` by DECIDE_TAC THEN
825    ASM_SIMP_TAC (bsrw_ss()) [Once cfindbody_thm],
826
827    `p < n` by DECIDE_TAC THEN
828    `���r. P @@ church p == cB r` by METIS_TAC [] THEN
829    `r = F` by (Cases_on `r` THEN METIS_TAC []) THEN
830    ASM_SIMP_TAC (bsrw_ss()) [Once cfindbody_thm, Cong cfindbody_cong] THEN
831    FIRST_X_ASSUM (fn th => MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] th)) THEN
832    ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) []
833  ]);
834
835val cfindbody_11 = Store_thm(
836  "cfindbody_11",
837  ``(cfindbody P1 N1 k1 = cfindbody P2 N2 k2) ���
838      (P1 = P2) ��� (N1 = N2) ��� (k1 = k2)``,
839  Q_TAC (NEW_TAC "lp") `FV P1 ��� FV P2 ��� FV k1 ��� FV k2` THEN
840  Q_TAC (NEW_TAC "nv") `FV P1 ��� FV P2 ��� FV k1 ��� FV k2 ��� {lp}` THEN
841  `(cfindbody P1 N1 k1 = Yf (LAM lp (LAM nv (P1 @@ VAR nv @@ (k1 @@ VAR nv)
842                                            @@ (VAR lp @@ (csuc @@ VAR nv)))))
843                            @@ N1) ���
844   (cfindbody P2 N2 k2 = Yf (LAM lp (LAM nv (P2 @@ VAR nv @@ (k2 @@ VAR nv)
845                                            @@ (VAR lp @@ (csuc @@ VAR nv)))))
846                            @@ N2)`
847      by SRW_TAC [][fresh_cfindbody] THEN
848  SRW_TAC [][AC CONJ_ASSOC CONJ_COMM]);
849
850val lameq_triangle = store_thm(
851  "lameq_triangle",
852  ``M == N ��� M == P ��� bnf N ��� bnf P ��� (N = P)``,
853  METIS_TAC [chap3Theory.betastar_lameq_bnf, chap2Theory.lameq_rules,
854             chap3Theory.bnf_reduction_to_self]);
855
856val cfindleast_bnfE = store_thm(
857  "cfindleast_bnfE",
858  ``(���n. ���b. P @@ church n == cB b) ���
859    cfindleast @@ P @@ k == r ��� bnf r ���
860    ���m. (r == k @@ church m) ��� P @@ church m == cB T ���
861        ���m���. m��� < m ��� P @@ church m��� == cB F``,
862  SIMP_TAC (bsrw_ss()) [cfindleast_behaviour] THEN
863  REPEAT STRIP_TAC THEN
864  `���N. steps N (cfindbody P (church 0) k) = r`
865    by METIS_TAC [nstar_steps, nstar_betastar_bnf,
866                  chap3Theory.betastar_lameq_bnf] THEN
867  Q_TAC SUFF_TAC
868    `���N cn ct. (steps N (cfindbody P ct k) = r) ���
869               (���c0. c0 < cn ��� P @@ church c0 == cB F) ���
870               (ct == church cn) ���
871               ���m. (r == k @@ church m) ��� P @@ church m == cB T ���
872                   ���m���. m��� < m ��� P @@ church m��� == cB F`
873    THEN1 METIS_TAC [DECIDE ``��(x < 0)``, chap2Theory.lameq_refl] THEN
874  REPEAT (FIRST_X_ASSUM (fn th => if free_in ``cfindbody`` (concl th) then
875                                    ALL_TAC
876                                  else NO_TAC)) THEN
877  completeInduct_on `N` THEN
878  MAP_EVERY Q.X_GEN_TAC [`cn`,`ct`] THEN REPEAT STRIP_TAC THEN
879  `cfindbody P ct k -n->* P @@ ct @@ (k @@ ct) @@ (cfindbody P (csuc @@ ct) k)`
880     by METIS_TAC [cfindbody_thm, whstar_nstar] THEN
881  `���b. P @@ church cn == cB b` by METIS_TAC [] THEN
882  Cases_on `b` THENL [
883    `cfindbody P ct k == k @@ church cn`
884      by ASM_SIMP_TAC (bsrw_ss()) [] THEN
885    `cfindbody P ct k -n->* r` by METIS_TAC [steps_nstar] THEN
886    METIS_TAC [nstar_lameq, chap2Theory.lameq_rules],
887
888    `P @@ ct == cB F` by ASM_SIMP_TAC (bsrw_ss()) [] THEN
889    POP_ASSUM (STRIP_ASSUME_TAC o
890               MATCH_MP (GEN_ALL (CONJUNCT2 whead_tests))) THEN
891    `cfindbody P ct k -n->* cfindbody P (csuc @@ ct) k`
892      by METIS_TAC [whstar_nstar, relationTheory.RTC_CASES_RTC_TWICE] THEN
893    `���n1. cfindbody P (csuc @@ ct) k = steps n1 (cfindbody P ct k)`
894      by METIS_TAC [nstar_steps] THEN
895    `��bnf (cfindbody P (csuc @@ ct) k)` by SRW_TAC [][] THEN
896    `n1 < N` by METIS_TAC [DECIDE ``n:num < m ��� (n = m) ��� m < n``,
897                           bnf_steps_upwards_closed] THEN
898    `���rest. N = rest + n1` by (Q.EXISTS_TAC `N - n1` THEN DECIDE_TAC) THEN
899    FULL_SIMP_TAC (srw_ss()) [steps_plus] THEN
900    `n1 ��� 0` by (STRIP_TAC THEN
901                 FULL_SIMP_TAC (srw_ss()) [termTheory.APP_acyclic]) THEN
902    `rest < rest + n1` by DECIDE_TAC THEN
903    POP_ASSUM (fn th1 => FIRST_X_ASSUM (MP_TAC o C MATCH_MP th1)) THEN
904    DISCH_THEN (Q.SPECL_THEN [`SUC cn`, `csuc @@ ct`] MP_TAC) THEN
905    ASM_SIMP_TAC (bsrw_ss()) [] THEN
906    DISCH_THEN MATCH_MP_TAC THEN
907    REPEAT STRIP_TAC THEN
908    `(c0 = cn) ��� c0 < cn` by DECIDE_TAC THEN SRW_TAC [][]
909  ]);
910
911val _ = export_theory()
912
913