1open HolKernel Parse boolLib bossLib finite_mapTheory;
2open recursivefnsTheory;
3open prnlistTheory;
4open primrecfnsTheory;
5open listTheory;
6open arithmeticTheory;
7open numpairTheory;
8open nlistTheory;
9open pred_setTheory;
10open turing_machineTheory;
11open whileTheory
12open logrootTheory;
13
14val _ = new_theory "turing_machine_primeq";
15
16val DISJ_IMP_EQ = prove(
17  ���((x = y) ��� P ��� (x ��� y ��� P)) ���
18   (P ��� (x = y) ��� (x ��� y ��� P)) ���
19   (x ��� y ��� P ��� ((x = y) ��� P)) ���
20   (P ��� x ��� y ��� ((x = y) ��� P))���,
21  METIS_TAC []);
22val _ = augment_srw_ss [rewrites [DISJ_IMP_EQ]]
23
24val updn_def = Define `
25  (updn [] = 0) ���
26  (updn [x] = tri x) ���
27  (updn [x;y] =  if y = 0 then tri x
28                 else if y = 1 then tri (x + 2) + 2
29                 else if y = 2 then tri x
30                 else nB (y = 3) * tri x) ���
31  (updn [s;actn;tmn] =
32   let tape = (nsnd tmn) in
33   let tl = (nfst tape) in
34   let th = ((nsnd tape) MOD 2) in
35   let tr = ((nsnd tape) DIV 2) in
36       if actn = 0 then (* Write 0 *)
37           s *, (tl *, ((2 * tr)))
38       else if actn = 1 then (* Write 1 *)
39           s *, (tl *, ((2 * tr) + 1 ))
40       else if actn = 2 then (* Move left *)
41           if tl MOD 2 = 1 then
42               s *, (((tl-1) DIV 2) *, ((2 * (th + (2 * tr))) + 1))
43           else
44               s *, ((tl DIV 2) *, (2 * (( th + (2 * tr)))))
45       else if actn = 3 then  (* Move right *)
46           if tr MOD 2 = 1 then
47               s *, ((th + (2 * tl)) *, ((2 * ((tr-1) DIV 2)) + 1))
48           else
49               s *, ((th + (2 * tl)) *, (2 * (tr DIV 2)))
50       else tmn) ���
51        (updn (s::actn::tmn::a::b) = updn [s;actn;tmn])
52`;
53
54val UPDATE_TM_NUM_act0_lem = Q.store_thm ("UPDATE_TM_NUM_act0_lem",
55  `��� s tmn actn.
56      (actn = 0) ==>
57      (updn [s;actn;tmn] =
58        ���UPDATE_ACT_S_TM s (NUM_TO_ACT actn) (FULL_DECODE_TM tmn)���)`,
59  REWRITE_TAC [updn_def] >> rpt strip_tac >>
60   (* actn = 0*)
61  simp[NUM_TO_ACT_def] >> rw[FULL_DECODE_TM_def,FULL_ENCODE_TM_def]
62  >- (rw[UPDATE_ACT_S_TM_def] >> EVAL_TAC) >>
63  rw[ENCODE_TM_TAPE_def]
64  >- (rw[UPDATE_ACT_S_TM_def] >> rw[DECODE_TM_TAPE_def] >>
65      simp[ENCODE_DECODE_thm])
66  >- (rw[UPDATE_ACT_S_TM_def] >> rw[DECODE_TM_TAPE_def] >>
67      simp[ENCODE_DECODE_thm ] >>
68      `ODD (nsnd (nsnd tmn))` by metis_tac[EVEN_OR_ODD] >>
69      fs[ODD_DIV_2_lem]) >>
70  `(UPDATE_ACT_S_TM s Wr0
71             <|state := nfst tmn;
72               tape_l := FST (DECODE_TM_TAPE (nsnd tmn));
73               tape_h := FST (SND (DECODE_TM_TAPE (nsnd tmn)));
74               tape_r := SND (SND (DECODE_TM_TAPE (nsnd tmn)))|>).tape_h = Z`
75       by fs[WRITE_0_HEAD_lem] >>
76  rfs[]);
77
78
79val UPDATE_TM_NUM_act1_lem = Q.store_thm ("UPDATE_TM_NUM_act1_lem",
80  `��� s tmn actn.
81      (actn = 1) ==>
82      (updn [s;actn;tmn] =
83          ���UPDATE_ACT_S_TM s (NUM_TO_ACT actn) (FULL_DECODE_TM tmn)���)`,
84  REWRITE_TAC [updn_def] >> rpt strip_tac >>
85  simp[NUM_TO_ACT_def] >>
86  rw[FULL_DECODE_TM_def] >> rw[FULL_ENCODE_TM_def]
87  >- (rw[UPDATE_ACT_S_TM_def] >> EVAL_TAC) >>
88  rw[ENCODE_TM_TAPE_def]
89  >- (rw[UPDATE_ACT_S_TM_def] >> rw[DECODE_TM_TAPE_def] >>
90      simp[ENCODE_DECODE_thm])
91  >- (`(UPDATE_ACT_S_TM s Wr1
92             <|state := nfst tmn;
93               tape_l := FST (DECODE_TM_TAPE (nsnd tmn));
94               tape_h := FST (SND (DECODE_TM_TAPE (nsnd tmn)));
95               tape_r := SND (SND (DECODE_TM_TAPE (nsnd tmn)))|>).tape_h = O`
96        by fs[WRITE_1_HEAD_lem] >> `O=Z` by fs[] >> fs[])
97   >- (rw[UPDATE_ACT_S_TM_def] >> rw[DECODE_TM_TAPE_def] >>
98       simp[ENCODE_DECODE_thm ]) >>
99   rw[UPDATE_ACT_S_TM_def] >> rw[DECODE_TM_TAPE_def] >>
100   simp[ENCODE_DECODE_thm]);
101
102val UPDATE_TM_NUM_act2_lem = Q.store_thm ("UPDATE_TM_NUM_act2_lem",
103  `��� s tmn actn.
104      (actn = 2) ==>
105      (updn [s;actn;tmn] =
106         ���UPDATE_ACT_S_TM s (NUM_TO_ACT actn) (FULL_DECODE_TM tmn)���)`,
107  REWRITE_TAC [updn_def] >> rpt strip_tac >>
108  simp[NUM_TO_ACT_def, FULL_DECODE_TM_def, FULL_ENCODE_TM_def,
109       UPDATE_ACT_S_TM_def] >>
110  rw[]
111  >- (fs[])
112  >- (`~EVEN (nfst (nsnd tmn))` by metis_tac[MOD_2, DECIDE ``0n <> 1``] >>
113      `ODD (nfst (nsnd tmn))` by metis_tac[EVEN_OR_ODD] >>
114      simp[ENCODE_TM_TAPE_def, ODD_TL_DECODE_lem, ENCODE_DECODE_thm] >>
115      rw[ENCODE_def, ENCODE_DECODE_thm,DECODE_TM_TAPE_def] >> rfs[ODD_HD_DECODE]
116      >- metis_tac[MOD_2]
117      >- (rw[MOD_2] >> metis_tac[ODD_DIV_2_lem, EVEN_OR_ODD]))
118  >- (simp[ENCODE_TM_TAPE_def, ODD_TL_DECODE_lem, ENCODE_DECODE_thm] >>
119      rw[ENCODE_def,DECODE_TM_TAPE_def,ENCODE_DECODE_thm,MOD_2] >>
120      metis_tac[ODD_DIV_2_lem, EVEN_OR_ODD])
121  >- (`EVEN (nfst (nsnd tmn))` by metis_tac[MOD_2, DECIDE ``0n <> 1``] >>
122      `~ODD (nfst (nsnd tmn))` by metis_tac[EVEN_AND_ODD] >>
123      simp[ENCODE_TM_TAPE_def, EVEN_TL_DECODE_lem, ENCODE_DECODE_thm] >>
124      rw[ENCODE_def,DECODE_TM_TAPE_def, ENCODE_DECODE_thm] >>
125      rfs[EVEN_HD_DECODE]
126      >- simp[MOD_2]
127      >- (rw[MOD_2] >> metis_tac[ODD_DIV_2_lem, EVEN_OR_ODD]))
128 );
129
130val UPDATE_TM_NUM_act3_lem = Q.store_thm ("UPDATE_TM_NUM_act3_lem",
131  `��� s tmn actn.
132      (actn = 3) ==>
133      (updn [s;actn;tmn] =
134         ���UPDATE_ACT_S_TM s (NUM_TO_ACT actn) (FULL_DECODE_TM tmn)���)`,
135  REWRITE_TAC [updn_def] >> rpt strip_tac >>
136  simp[NUM_TO_ACT_def, FULL_DECODE_TM_def, FULL_ENCODE_TM_def,
137       UPDATE_ACT_S_TM_def] >>
138  rw[]
139  >- (fs[SND_SND_DECODE_TM_TAPE])
140  >- (simp[ENCODE_TM_TAPE_def, ENCODE_DECODE_thm] >>
141      `~EVEN (nsnd (nsnd tmn) DIV 2)` by metis_tac[MOD_2, DECIDE ``0n <> 1``] >>
142      `ODD (nsnd (nsnd tmn) DIV 2)` by metis_tac[EVEN_OR_ODD] >>
143      rfs[SND_SND_DECODE_TM_TAPE] >> simp[ENCODE_def] >>
144      fs[ODD_TL_DECODE_lem,ENCODE_DECODE_thm] >>
145      `HD (DECODE (nsnd (nsnd tmn) DIV 2)) = O` by fs[ODD_HD_DECODE] >>
146      simp[] >> rw[ENCODE_def,DECODE_TM_TAPE_def,ENCODE_DECODE_thm,MOD_2])
147  >- (simp[ENCODE_TM_TAPE_def, ENCODE_DECODE_thm] >>
148      `EVEN (nsnd (nsnd tmn) DIV 2)` by metis_tac[MOD_2, DECIDE ``0n <> 1``] >>
149      `~ODD (nsnd (nsnd tmn) DIV 2)` by metis_tac[EVEN_AND_ODD] >>
150      rfs[SND_SND_DECODE_TM_TAPE]  >>
151      rw[ENCODE_def,DECODE_TM_TAPE_def, ENCODE_DECODE_thm,MOD_2] )
152  >- (simp[ENCODE_TM_TAPE_def, ENCODE_DECODE_thm] >>
153      `EVEN (nsnd (nsnd tmn) DIV 2)` by metis_tac[MOD_2, DECIDE ``0n <> 1``] >>
154      fs[SND_SND_DECODE_TM_TAPE,EVEN_HD_DECODE] >>
155      rw[ENCODE_def,DECODE_TM_TAPE_def, ENCODE_DECODE_thm,MOD_2] >>
156      fs[EVEN_TL_DECODE_lem,ENCODE_DECODE_thm])
157 );
158
159val UPDATE_TM_NUM_thm = Q.store_thm ("UPDATE_TM_NUM_thm",
160  `��� s tmn actn.
161      actn < 4 ==>
162      (updn [s;actn;tmn] =
163       ���UPDATE_ACT_S_TM s (NUM_TO_ACT actn) (FULL_DECODE_TM tmn)���)`,
164  rpt strip_tac >>
165  `(actn = 0) ��� (actn = 1) ��� (actn = 2) ��� (actn = 3)` by simp[]
166  >- (* actn = 0*)
167     fs[UPDATE_TM_NUM_act0_lem]
168  >-  (* actn = 1*)
169     fs[UPDATE_TM_NUM_act1_lem]
170  >- (* actn = 2*)
171      fs[UPDATE_TM_NUM_act2_lem]
172  >- (* actn = 3*)
173      fs[UPDATE_TM_NUM_act3_lem]);
174
175val pr3_def = Define`
176  (pr3 f [] = f 0 0 0 : num) ���
177  (pr3 f [x:num] = f x 0 0) ���
178  (pr3 f [x;y] = f x y 0) ���
179  (pr3 f (x::y::z::t) = f x y z)
180`;
181
182val GENLIST1 = prove(``GENLIST f 1 = [f 0]``,
183                     SIMP_TAC bool_ss [ONE, GENLIST, SNOC]);
184
185val GENLIST2 = prove(
186``GENLIST f 2 = [f 0; f 1]``,
187SIMP_TAC bool_ss [TWO, ONE, GENLIST, SNOC]);
188
189val GENLIST3 = prove(
190``GENLIST f 3 = [f 0; f 1; f 2]``,
191EVAL_TAC );
192
193val ternary_primrec_eq = store_thm("ternary_primrec_eq",
194  ``primrec f 3 ��� (���n m p. f [n; m; p] = g n m p) ��� (f = pr3 g)``,
195  SRW_TAC [][] >> SIMP_TAC (srw_ss()) [FUN_EQ_THM] >>
196  Q.X_GEN_TAC `l` >>
197  `(l = []) ��� ���n ns. l = n :: ns` by (Cases_on `l` >> SRW_TAC [][]) THENL [
198    SRW_TAC [][] >>
199    `f [] = f (GENLIST (K 0) 3)` by METIS_TAC [primrec_nil] >>
200    SRW_TAC [][GENLIST3,pr3_def],
201
202    `(ns = []) ��� ���m ms. ns = m::ms` by (Cases_on `ns` THEN SRW_TAC [][]) >>
203    SRW_TAC [][] THENL [
204      IMP_RES_THEN (Q.SPEC_THEN `[n]` MP_TAC) primrec_short >>
205      SRW_TAC [][GENLIST1] >> EVAL_TAC,
206      `(ms = []) ��� ���p ps. ms = p::ps` by (Cases_on `ms` THEN SRW_TAC [][]) >| [
207        fs[pr3_def] >>
208        `f [n;m] = f ([n;m] ++ GENLIST (K 0) (3 - LENGTH [n;m]))`
209          by fs[primrec_short] >>
210        `GENLIST (K 0) (3 - LENGTH [n;m]) = [0]` by EVAL_TAC >> rfs[],
211        IMP_RES_THEN (Q.SPEC_THEN `(n::m::p::ps)` MP_TAC)
212                     primrec_arg_too_long >>
213        SRW_TAC [ARITH_ss][] >> fs[pr3_def]
214      ]
215    ]
216  ]);
217
218val primrec_pr3 = store_thm(
219        "primrec_pr3",
220``(���g. primrec g 3 ��� (���m n p. g [m; n; p] = f m n p)) ��� primrec (pr3 f) 3``,
221METIS_TAC [ternary_primrec_eq]);
222
223val MULT2_def = Define `MULT2 x = 2*x`;
224
225val pr_pr_up_case1_def = Define`
226  pr_pr_up_case1  =
227    Cn (pr2 $*,) [ proj 0;Cn (pr2 $*,) [proj 2;Cn (pr1 MULT2) [proj 4]] ]
228`;
229
230val pr_up_case1_thm = Q.store_thm("pr_up_case1_thm",
231  `��� x.
232     (proj 0 x) *, (proj 2 x) *, (2 * (proj 4 x)) =
233     Cn (pr2 $*,) [ proj 0;Cn (pr2 $*,) [proj 2;Cn (pr1 MULT2) [proj 4]] ] x`,
234  strip_tac >> rfs[MULT2_def] );
235
236val pr_pr_up_case2_def = Define`
237  pr_pr_up_case2  =
238   Cn (pr2 $*,) [ proj 0;
239                  Cn (pr2 $*,) [proj 2;Cn (succ) [Cn (pr1 MULT2) [proj 4]] ] ]
240`;
241
242val pr_pr_up_case3_def = Define`pr_pr_up_case3  =
243        Cn (pr2 $*,) [ proj 0;Cn (pr2 $*,) [Cn (pr1 DIV2) [Cn (pr1 PRE) [proj 2]];
244        Cn (succ) [Cn (pr1 MULT2) [Cn (pr2 (+)) [proj 3; Cn (pr1 MULT2) [proj 4]]]] ] ] `;
245
246val pr_pr_up_case4_def = Define`pr_pr_up_case4  =
247        Cn (pr2 $*,) [ proj 0;Cn (pr2 $*,) [Cn (pr1 DIV2) [proj 2];
248        Cn (pr1 MULT2) [Cn (pr2 (+)) [proj 3; Cn (pr1 MULT2) [proj 4]]] ] ] `;
249
250val pr_pr_up_case5_def = Define`pr_pr_up_case5  =
251        Cn (pr2 $*,) [ proj 0;Cn (pr2 $*,) [Cn (pr2 (+)) [proj 3;Cn (pr1 MULT2) [proj 2]];
252        Cn (succ) [Cn (pr1 MULT2) [Cn (pr1 DIV2) [Cn (pr1 PRE) [proj 4]]]] ] ] `;
253
254val pr_pr_up_case6_def = Define`pr_pr_up_case6  =
255        Cn (pr2 $*,) [ proj 0;Cn (pr2 $*,) [Cn (pr2 (+)) [proj 3;Cn (pr1 MULT2) [proj 2]];
256       Cn (pr1 MULT2) [Cn (pr1 DIV2) [proj 4]]]  ] `;
257
258val pr_pr_up_case7_def = Define`pr_pr_up_case7  =
259  proj 5 `;
260
261
262val _ = overload_on ("onef", ``K 1 : num list -> num``)
263
264val _ = overload_on ("twof", ``K 2 : num list -> num``)
265
266val _ = overload_on ("threef", ``K 3 : num list -> num``)
267
268val _ = overload_on ("fourf", ``K 4 : num list -> num``)
269
270val nB_cond_elim = prove(
271``nB p * x + nB (~p) * y = if p then x else y``,
272Cases_on `p` >> simp[]);
273
274
275val updn_zero_thm = Q.store_thm ("updn_zero_thm",
276`��� x. updn [x;0] = updn [x]`,
277strip_tac >> fs[updn_def])
278
279val updn_two_lem_1 = Q.store_thm("updn_two_lem_1",
280`��� x. ((x <> []) ��� (LENGTH x <= 2)) ==> ( ��� h. (x = [h])) ���  (��� h t. (x = [h;t]))`,
281rpt strip_tac >>  Cases_on `x` >- fs[] >> Cases_on `t` >- fs[] >> Cases_on `t'` >- fs[] >> rfs[] );
282
283val updn_two_lem_2 = Q.store_thm("updn_two_lem_2",
284`���x. (LENGTH x = 2) ==> (���h t. (x = [h;t]))`,
285rpt strip_tac >>  Cases_on `x` >> fs[] >> Cases_on `t` >> fs[])
286
287val updn_three_lem_1 = Q.store_thm("updn_three_lem_1",
288  `��� x. ��(LENGTH x <= 2) ==>
289        (��� a b c. (x = [a;b;c]) ) ��� (��� a b c d e. x = a::b::c::d::e)`,
290  rpt strip_tac >>  Cases_on `x` >- fs[] >>
291  rename [���LENGTH (h::t)���] >> Cases_on ���t��� >> fs[] >>
292  rename [���SUC (LENGTH l)���] >> Cases_on ���l��� >> fs[] >>
293  metis_tac[list_CASES]);
294
295Theorem prim_pr_rec_updn:
296  updn =
297  Cn
298    (pr_cond (Cn pr_eq [proj 1;zerof]) (pr_pr_up_case1) (
299        pr_cond (Cn pr_eq [proj 1; onef]) (pr_pr_up_case2) (
300          pr_cond (Cn pr_eq [proj 1; twof]) (
301            pr_cond (Cn pr_eq [Cn (pr_mod) [proj 2;twof];onef])
302                    (pr_pr_up_case3)
303                    (pr_pr_up_case4)
304          ) (
305            pr_cond (Cn pr_eq [proj 1;threef]) (
306              pr_cond (Cn pr_eq [Cn (pr_mod) [proj 4;twof];onef])
307                      (pr_pr_up_case5)
308                      (pr_pr_up_case6)
309            ) (
310              pr_cond (Cn pr_eq [proj 1;fourf])
311                      (pr_pr_up_case7)
312                      (pr_pr_up_case7)
313            )
314          )
315        )
316      )
317    )
318    [proj 0;proj 1; Cn (pr1 nfst) [Cn (pr1 nsnd) [proj 2]] ;
319     Cn (pr_mod) [Cn (pr1 nsnd) [ Cn (pr1 nsnd) [proj 2]];twof];
320     Cn (pr1 DIV2) [Cn (pr1 nsnd) [ Cn (pr1 nsnd) [proj 2]]]; proj 2 ]
321Proof
322  rw[Cn_def,FUN_EQ_THM]
323  >> fs[pr_pr_up_case1_def,pr_pr_up_case2_def,pr_pr_up_case3_def,
324         pr_pr_up_case4_def,pr_pr_up_case5_def,pr_pr_up_case6_def] >> rw[]
325  >- (rw[proj_def,updn_def,updn_zero_thm,updn_three_lem_1] >> fs[]
326      >- EVAL_TAC
327      >- (`(���h. x = [h]) ��� (���h t. x = [h;t])` by simp[updn_two_lem_1]
328          >- (rw[updn_def] >> simp[MULT2_def] >> simp[npair_def])
329          >- (fs[updn_def,updn_zero_thm] >> simp[MULT2_def] >>
330              simp[npair_def]))
331      >- (`(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))`
332            by simp[updn_three_lem_1] >>
333          fs[updn_def,MULT2_def,DIV2_def])
334     )
335  >- (fs[proj_def,updn_def,updn_zero_thm,pr_pr_up_case2_def] >> rw[] >> fs[]
336      >- (`(���h. x = [h]) ��� (���h t. x = [h;t])` by simp[updn_two_lem_1] >>
337          fs[updn_def,updn_zero_thm] >> simp[MULT2_def, npair_def] >>
338          EVAL_TAC >> simp[])
339      >- (`(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))`
340            by simp[updn_three_lem_1] >> fs[updn_def,MULT2_def,DIV2_def])
341     )
342  >- (fs[proj_def,updn_def,updn_zero_thm,pr_pr_up_case3_def] >> rw[] >> fs[] >>
343      `(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))`
344         by simp[updn_three_lem_1] >> fs[updn_def,MULT2_def,DIV2_def])
345  >- (fs[proj_def,updn_def,updn_zero_thm,pr_pr_up_case4_def] >> rw[] >> fs[]
346      >- (`(���h. x = [h]) ��� (���h t. x = [h;t])` by simp[updn_two_lem_1] >>
347          fs[updn_def,updn_zero_thm] >> simp[MULT2_def] >> simp[npair_def])
348      >- (`(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))`
349            by simp[updn_three_lem_1] >> fs[updn_def,MULT2_def,DIV2_def])
350     )
351  >- (fs[proj_def,updn_def,updn_zero_thm,pr_pr_up_case5_def] >> rw[] >> fs[] >>
352      `(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))`
353         by simp[updn_three_lem_1] >> fs[updn_def,MULT2_def,DIV2_def])
354  >- (fs[proj_def,updn_def,updn_zero_thm,pr_pr_up_case6_def] >> rw[] >> fs[]
355      >- (`(���h. x = [h]) ��� (���h t. x = [h;t])` by simp[updn_two_lem_1] >>
356          fs[updn_def] >> simp[MULT2_def] >> simp[npair_def])
357      >- (`(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))`
358           by simp[updn_three_lem_1] >> fs[updn_def,MULT2_def,DIV2_def])
359     )
360  >- (fs[proj_def,updn_def,updn_zero_thm,pr_pr_up_case7_def] >> rw[] >> fs[]
361
362      >- (Cases_on ���x = []��� >> fs[] >>
363          `(���h. x = [h]) ��� (���h t. x = [h;t])` by simp[updn_two_lem_1] >>
364          fs[updn_def])
365      >- (`(��� a b c. x = [a;b;c]) ��� (��� a b c d e. x = (a::b::c::d::e))`
366            by simp[updn_three_lem_1] >> fs[updn_def])
367     )
368QED
369
370val primrec_cn = List.nth(CONJUNCTS primrec_rules, 3);
371
372val primrec_pr = List.nth(CONJUNCTS primrec_rules, 4);
373
374val primrec_mult2 = Q.store_thm("primrec_mult2",
375`primrec (pr1 MULT2) 1`,
376MATCH_MP_TAC primrec_pr1 >>
377Q.EXISTS_TAC `Cn (pr2 $*) [proj 0; twof]` >> conj_tac >-
378  SRW_TAC [][primrec_rules, alt_Pr_rule,Pr_thm,Pr_def ] >>
379  SRW_TAC [][primrec_rules, alt_Pr_rule,Pr_thm,Pr_def ] >> rw[MULT2_def]);
380
381val primrec_div2 = Q.store_thm("primrec_div2",
382`primrec (pr1 DIV2) 1`,
383MATCH_MP_TAC primrec_pr1 >>
384Q.EXISTS_TAC `Cn (pr_div) [proj 0; twof]` >> conj_tac >-
385SRW_TAC [][primrec_rules, alt_Pr_rule,Pr_thm,Pr_def,primrec_pr_div ] >>
386SRW_TAC [][primrec_rules, alt_Pr_rule,Pr_thm,Pr_def,primrec_pr_div ] >> rw[DIV2_def]);
387
388val primrec_pr_case1 = Q.store_thm("primrec_pr_case1",
389`primrec pr_pr_up_case1 6`,
390SRW_TAC [][pr_pr_up_case1_def] >>
391rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> rw[primrec_mult2]
392                               );
393
394val primrec_pr_case2 = Q.store_thm("primrec_pr_case2",
395`primrec pr_pr_up_case2 6`,
396SRW_TAC [][pr_pr_up_case2_def] >>
397        rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> rw[primrec_mult2]
398                                  );
399
400val primrec_pr_case3 = Q.store_thm("primrec_pr_case3",
401`primrec pr_pr_up_case3 6`,
402SRW_TAC [][pr_pr_up_case3_def] >>
403        rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >>
404        rw[primrec_mult2,primrec_div2]                                  );
405
406val primrec_pr_case4 = Q.store_thm("primrec_pr_case4",
407`primrec pr_pr_up_case4 6`,
408SRW_TAC [][pr_pr_up_case4_def] >>
409        rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> rw[primrec_mult2,primrec_div2]
410                                  );
411
412val primrec_pr_case5 = Q.store_thm("primrec_pr_case5",
413`primrec pr_pr_up_case5 6`,
414SRW_TAC [][pr_pr_up_case5_def] >>
415        rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> rw[primrec_mult2,primrec_div2]
416                                  );
417
418val primrec_pr_case6 = Q.store_thm("primrec_pr_case6",
419`primrec pr_pr_up_case6 6`,
420SRW_TAC [][pr_pr_up_case6_def] >>
421        rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> rw[primrec_mult2,primrec_div2]
422                                  );
423
424val primrec_proj = List.nth(CONJUNCTS primrec_rules, 2);
425
426val primrec_pr_case7 = Q.store_thm("primrec_pr_case7",
427`primrec pr_pr_up_case7 6`,
428SRW_TAC [][pr_pr_up_case7_def] >>
429      `5<6` by fs[]   >> SRW_TAC [][primrec_proj]
430                                  );
431
432val UPDATE_TM_NUM_PRIMREC = Q.store_thm("UPDATE_TM_NUM_PRIMREC",
433`primrec updn 3`,
434SRW_TAC [][updn_def,primrec_rules,prim_pr_rec_updn] >> SRW_TAC [][pr_cond_def] >>
435        rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules])
436        >> fs[primrec_pr_case1,primrec_pr_case2,primrec_pr_case3,primrec_pr_case4,
437               primrec_pr_case5,primrec_pr_case6,primrec_pr_case7,primrec_div2]
438         );
439
440
441val tmstepf_def = tDefine "tmstepf" `
442  tmstepf p tmn =
443     case OLEAST n. (nfst n, CELL_NUM (nsnd n)) ��� FDOM p ��� nfst n<>0 of
444         NONE => 0 *, nsnd tmn
445       | SOME n => let s = nfst n ;
446                       sym = CELL_NUM (nsnd n) ;
447                       (s',actn) = p ' (s,sym)
448                   in
449                     if nfst n = 0 then tmn
450                     else if (nfst tmn = s) ���
451                             ((nsnd (nsnd tmn)) MOD 2 = NUM_CELL sym)
452                     then updn [s'; ACT_TO_NUM actn; tmn]
453                     else tmstepf (p \\ (s,sym)) tmn
454`
455  (WF_REL_TAC `measure (CARD o FDOM o FST)` >> simp[OLEAST_EQ_SOME] >>
456   metis_tac[MEMBER_CARD]);
457
458val HEAD_DECODE_ENCDOE_EQ = Q.store_thm("HEAD_DECODE_ENCDOE_EQ[simp]",
459`(HD (DECODE (ENCODE t)) = Z) ==> (HD t = Z)`,
460Cases_on `t`
461  >- (EVAL_TAC)
462  >- (fs[ENCODE_def,DECODE_def]  >> Cases_on `h` >> fs[] >> `2* ENCODE t' +1 = SUC (2* ENCODE t')` by fs[] >> rw[DECODE_def] >> rfs[ODD_DOUBLE] ) )
463
464val ENCODE_ONE_TL_ZERO = Q.store_thm("ENCODE_ONE_TL_ZERO",
465`(ENCODE t = 1) ==> (ENCODE (TL t) = 0)`,
466Cases_on ` t` >> fs[] >- (EVAL_TAC) >- (fs[ENCODE_def] >> Cases_on `h` >> fs[]) )
467
468
469val HD_DECODE_DOUBLED = Q.store_thm("HD_DECODE_DOUBLED[simp]",
470`(x <> 0) ==> (HD (DECODE (2 * x)) = Z)`,
471Cases_on `x` >> fs[] >> `2*(SUC n) =SUC (SUC (2* n))` by simp[] >> simp[DECODE_def,ODD,ODD_MULT] )
472
473
474val TL_DECODE_DOUBLED = Q.store_thm("TL_DECODE_DOUBLED[simp]",
475`(x <> 0) ==> (TL (DECODE (2 * x)) = DECODE x)`,
476Cases_on `x` >> fs[] >> `2 * (SUC n) =SUC (SUC (2* n))` by simp[] >>
477         simp[DECODE_def,SimpLHS,ODD,ODD_MULT] >> pop_assum(SUBST1_TAC o SYM) >> fs[TWO_TIMES_DIV_TWO_thm] )
478
479val HD_DECODE_DOUBLED = Q.store_thm("HD_DECODE_DOUBLED[simp]",
480`(HD (DECODE (2 * x + 1)) = O)`,
481simp[GSYM(ADD1),DECODE_def,ODD,ODD_MULT]  )
482
483
484val TL_DECODE_DOUBLED = Q.store_thm("TL_DECODE_DOUBLED[simp]",
485`(TL (DECODE (2 * x + 1)) = DECODE x)`,
486simp[GSYM(ADD1),DECODE_def,ODD,ODD_MULT]  )
487
488
489
490val ENCODED_DECODED_ENCODED_UPDATE_TM_thm = Q.store_thm(
491  "ENCODED_DECODED_ENCODED_UPDATE_TM_thm",
492  `���UPDATE_ACT_S_TM (FST (p ' (tm.state,tm.tape_h)))
493                    (SND (p ' (tm.state,tm.tape_h))) (FULL_DECODE_TM ���tm���) ��� =
494   ���(UPDATE_ACT_S_TM (FST (p ' (tm.state,tm.tape_h)))
495                     (SND (p ' (tm.state,tm.tape_h))) (tm) )���`,
496  fs[FULL_DECODE_TM_def,FULL_ENCODE_TM_def] >> rw[]
497  >- (fs[ENCODE_TM_TAPE_def] >> Cases_on `tm.tape_h`
498      >- (fs[SND_SND_DECODE_TM_TAPE_FULL] >>
499          `EVEN (2 * ENCODE tm.tape_r)` by fs[EVEN_DOUBLE] >>
500          fs[FST_SND_DECODE_TM_TAPE_FULL] >> fs[UPDATE_ACT_S_TM_def] >>
501          Cases_on `SND (p ' (tm.state,Z))` >> fs[]
502          >- (Cases_on `tm.tape_l = []` >> fs[ENCODE_def] >>
503              Cases_on `ENCODE tm.tape_l = 0` >> fs[] )
504          >- (Cases_on `tm.tape_r = []` >> fs[ENCODE_def] >>
505              Cases_on `2* ENCODE tm.tape_r DIV 2 = 0` >> fs[]))
506      >- (fs[SND_SND_DECODE_TM_TAPE_FULL] >>
507          fs[UPDATE_ACT_S_TM_def] >>
508          Cases_on `SND (p ' (tm.state,O))` >> fs[]
509          >- (Cases_on `tm.tape_l = []` >> fs[ENCODE_def] >>
510              Cases_on `ENCODE tm.tape_l = 0` >> fs[])
511          >- (Cases_on `tm.tape_r = []` >> fs[ENCODE_def] >>
512              Cases_on `(2 * ENCODE tm.tape_r + 1) DIV 2 = 0` >> fs[])))
513  >- (fs[UPDATE_ACT_S_TM_def] >>
514      Cases_on `SND (p ' (tm.state,tm.tape_h))` >> fs[]
515         >- (simp[ENCODE_TM_TAPE_def,ENCODE_DECODE_thm] >> rw[] )
516         >- (simp[ENCODE_TM_TAPE_def,ENCODE_DECODE_thm] >> rw[])
517         >- (Cases_on `tm.tape_l` >> fs[ENCODE_def]
518            >- (simp[ENCODE_TM_TAPE_def,ENCODE_DECODE_thm])
519            >- (Cases_on `h` >> simp[]
520               >- (rw[]
521                  >- (simp[ENCODE_TM_TAPE_def,ENCODE_def])
522                  >- (simp[ENCODE_TM_TAPE_def,ENCODE_def] >>
523                      simp[ENCODE_DECODE_thm] ))
524               >- (simp[ENCODE_TM_TAPE_def,ENCODE_DECODE_thm] ) ) )
525         >- (Cases_on `tm.tape_r` >> fs[ENCODE_def]
526             >- (simp[ENCODE_TM_TAPE_def,ENCODE_DECODE_thm])
527             >- (Cases_on `h` >> simp[]
528                 >- (rw[]
529                     >- (simp[ENCODE_TM_TAPE_def,ENCODE_def])
530                     >- (simp[ENCODE_TM_TAPE_def,ENCODE_def] >>
531                         simp[ENCODE_DECODE_thm] ))
532                 >- (simp[ENCODE_TM_TAPE_def,ENCODE_DECODE_thm] ) ) ))
533);
534
535
536val UPDATE_TM_NUM_corol = Q.store_thm("UPDATE_TM_NUM_corol",
537`���s' tmn actn'. (updn [s'; ACT_TO_NUM actn'; tmn] =
538                 ���UPDATE_ACT_S_TM s' actn' (FULL_DECODE_TM tmn)���)`,
539fs[ACT_TO_NUM_LESS_4,UPDATE_TM_NUM_thm])
540
541val lemma_11 =
542    UPDATE_TM_ARB_Q |> Q.INST[`q` |-> `tm.prog` ]
543                    |> SIMP_RULE(srw_ss())[tm_with_prog]
544
545val updn_UPDATE_TAPE = Q.store_thm("updn_UPDATE_TAPE",
546  `(tm.state, tm.tape_h) ��� FDOM p ��� tm.state <> 0 ==>
547   ((��(s',actn). updn [s'; ACT_TO_NUM actn; ���tm���]) (p ' (tm.state,tm.tape_h)) =
548   ���UPDATE_TAPE (tm with prog := p)���)`,
549  rw[] >> `ACT_TO_NUM actn < 4` by fs[ACT_TO_NUM_LESS_4] >>
550  qabbrev_tac `ptm = tm with prog := p` >>
551  `(tm.state,tm.tape_h) ��� FDOM ptm.prog` by fs[Abbr`ptm`] >>
552  `(ptm.state,ptm.tape_h) ��� FDOM ptm.prog` by fs[Abbr`ptm`] >>
553  `ptm.state <> 0` by simp[Abbr`ptm`] >>
554  `(UPDATE_ACT_S_TM
555      (FST (ptm.prog ' (ptm.state, ptm.tape_h)))
556      (SND (ptm.prog ' (ptm.state,ptm.tape_h)))
557      ptm =
558    UPDATE_TAPE ptm)`
559      by  fs[UPDATE_TAPE_ACT_STATE_TM_thm] >> rfs[] >>
560   `ACT_TO_NUM (SND (ptm.prog ' (tm.state,tm.tape_h))) < 4`
561     by fs[ACT_TO_NUM_LESS_4] >>
562   `(updn [FST (ptm.prog ' (tm.state,tm.tape_h));
563           ACT_TO_NUM (SND (p ' (tm.state,tm.tape_h)));
564           ���tm���] =
565    ���UPDATE_ACT_S_TM (FST (ptm.prog ' (tm.state,tm.tape_h)))
566                     (SND (p ' (tm.state,tm.tape_h)))
567                     (FULL_DECODE_TM ���tm���)���)`
568      by fs[UPDATE_TM_NUM_corol] >>
569   simp[pairTheory.UNCURRY] >> fs[Abbr`ptm`] >>
570   simp[ENCODED_DECODED_ENCODED_UPDATE_TM_thm,lemma_11]);
571
572val CELL_NUM_NUM_CELL = Q.store_thm("CELL_NUM_NUM_CELL[simp]",
573`CELL_NUM (NUM_CELL x) = x`,
574Cases_on `x` >> fs[CELL_NUM_def])
575
576val CELL_NUM_NUM_CELL_RW = Q.store_thm("CELL_NUM_NUM_CELL_RW",
577  `(NUM_CELL (CELL_NUM c) = c) ==> (NUM_CELL h <> c) ==> (h <> CELL_NUM c)`,
578  strip_tac >> strip_tac >> metis_tac[]  )
579
580val NUM_STATE_CELL_NUM_LEM = Q.store_thm("NUM_STATE_CELL_NUM_LEM",
581  `(NUM_CELL (CELL_NUM c) = c) ��� ((tm.state = n) ��� NUM_CELL tm.tape_h ��� c) ���
582   (tm.state = n) ��� tm.tape_h ��� CELL_NUM c`,
583  strip_tac >> strip_tac >> strip_tac >>
584  fs[CELL_NUM_NUM_CELL_RW]);
585
586val EQ_SND_P_LESS = Q.store_thm("EQ_SND_P_LESS",
587  `a <> b  ==> ((p \\ a) ' b  =  p ' b)`,
588  simp[DOMSUB_FAPPLY_THM]);
589
590val UPDATE_W_PROG_NIN_TM = Q.store_thm("UPDATE_W_PROG_NIN_TM",
591  `((NUM_CELL (CELL_NUM c) = c) ��� ((n,CELL_NUM c) ��� FDOM p) ���
592   n <> 0 ��� ((tm.state = n) ��� NUM_CELL tm.tape_h ��� c))
593    ���
594   (���UPDATE_TAPE (tm with prog := p \\ (n,CELL_NUM c)) ��� =
595    ���UPDATE_TAPE (tm with prog := p)���)`,
596  simp[FULL_ENCODE_TM_def]  >> rw[] >>
597  `(tm.state = n) ��� tm.tape_h ��� CELL_NUM c`
598    by metis_tac[NUM_STATE_CELL_NUM_LEM] >>
599  `(tm.state,tm.tape_h) <> (n,CELL_NUM c)`
600    by (simp[] >> metis_tac[]) >>
601  rw[] >>
602  Cases_on `(tm.state,tm.tape_h) ��� FDOM p` >>
603  rw[UPDATE_TAPE_def] >> fs[EQ_SND_P_LESS] >>
604  Cases_on `SND (p ' (tm.state,tm.tape_h))` >> fs[] >>
605  Cases_on `tm.tape_l = []` >> fs[] >>
606  Cases_on `tm.tape_r = []` >> fs[ENCODE_TM_TAPE_def]);
607
608val tm_eq_tm_with_state = Q.store_thm("tm_eq_tm_with_state",
609  `(tm.state = a) ==> (tm = tm with state := a)`,
610  strip_tac >> `(tm with state := a).state = a` by fs[] >>
611  rfs[TM_component_equality])
612
613val effempty_def = Define`
614  effempty p <=> FDOM p ��� {(a,b) | (a,b) | a = 0}
615`;
616
617val containment_lem_nzero = Q.store_thm("containment_lem_nzero",
618  `((OLEAST n. (nfst n,CELL_NUM (nsnd n)) ��� FDOM p ��� nfst n <>0) = NONE)
619     ���
620   effempty p`,
621  rw[effempty_def] >> eq_tac >> simp[] >> csimp[fmap_EXT] >>
622  simp[pairTheory.FORALL_PROD] >> strip_tac
623  >- (rw[SUBSET_DEF] >> rename[`sc ��� FDOM p`] >>
624      `���s c. sc = (s,c)` by simp[pairTheory.pair_CASES]>>
625      rw[] >> first_x_assum (qspec_then `s *, (NUM_CELL c)` mp_tac) >>simp[])
626  >- (rpt strip_tac >> fs[SUBSET_DEF] >> res_tac >> fs[]));
627
628val effempty_no_update = Q.store_thm("effempty_no_update",
629  `effempty tm.prog ==> (UPDATE_TAPE tm = tm with state := 0)`,
630  rw[effempty_def]>> simp[UPDATE_TAPE_def]>>
631  Cases_on `(tm.state,tm.tape_h) ��� FDOM tm.prog`>> simp[]>>
632  fs[SUBSET_DEF] >> res_tac >> fs[]);
633
634val CELL_NUM_LEM1 = Q.store_thm("CELL_NUM_LEM1",
635  `(���n'. n' < n ��� c ��� nfst n' ��� 0 ���
636     (nfst n',CELL_NUM (nsnd n')) ��� FDOM p) ���
637   (n,CELL_NUM c) ��� FDOM p ��� n<>0
638      ==>
639   (c=0) ��� (c=1)`,
640  spose_not_then strip_assume_tac >> Cases_on `CELL_NUM c`
641  >- (`0<c` by simp[] >>
642      metis_tac[nfst_npair,nsnd_npair,npair2_lt,CELL_NUM_def])
643  >- (`1<c` by simp[] >>
644      metis_tac[nfst_npair,nsnd_npair,npair2_lt,CELL_NUM_def]));
645
646val FULL_ENCODE_IGNORES_PROGS' =
647    FULL_ENCODE_IGNORES_PROGS |> SYM  |> Q.INST[`p`|->`ARB` ]
648
649val tmstepf_update_equiv = Q.store_thm("tmstepf_update_equiv",
650  `���p n tm.
651    (n = ���tm���) ==>
652    (tmstepf p n = FULL_ENCODE_TM (UPDATE_TAPE (tm with prog := p) ))`,
653  ho_match_mp_tac (theorem"tmstepf_ind") >> simp[OLEAST_EQ_SOME] >> rw[] >>
654  pop_assum (assume_tac o CONV_RULE (HO_REWR_CONV npair_lem)) >> fs[] >>
655  simp[Once tmstepf_def] >>
656  Cases_on `
657    OLEAST n. (nfst n,CELL_NUM (nsnd n)) ��� FDOM p ��� nfst n ��� 0
658  `
659  >- (simp[] >> fs[containment_lem_nzero,effempty_no_update] >>
660      simp[UPDATE_TAPE_def,FULL_ENCODE_TM_def, ENCODE_TM_TAPE_def]) >>
661  fs[OLEAST_EQ_SOME] >> rename [`nfst nc ��� 0`] >> simp[] >>
662  `���n c. nc = n *, c` by metis_tac[npair_cases] >>
663  fs[UPDATE_TAPE_ACT_STATE_TM_thm,NUM_TO_CELL_TO_NUM,
664     FULL_ENCODE_TM_STATE] >>
665  `NUM_CELL (CELL_NUM c) = c`
666    by metis_tac[CELL_NUM_LEM1,NUM_TO_CELL_TO_NUM] >> simp[] >> fs[] >>
667  rfs[NUM_CELL_INJ] >>
668  Cases_on `(tm.state = n) ��� (NUM_CELL tm.tape_h = c)` >> rw[]
669  >- (fs[updn_UPDATE_TAPE]) >>
670  `��� a s. p ' (n,CELL_NUM c) = (s,a)` by metis_tac[pairTheory.pair_CASES] >>
671  first_x_assum(qspecl_then[`n`,`c`,`s`,`a`] mp_tac) >> simp[] >>
672  rw[CELL_NUM_NUM_CELL_RW] >> simp[UPDATE_TAPE_def] >>
673  Cases_on `(tm.state,tm.tape_h) ��� FDOM p` >> simp[]
674  >- (Cases_on `tm.state = 0` >>simp[]
675      >- simp_tac bool_ss [FULL_ENCODE_IGNORES_PROGS, GSYM TM_fupdcanon] >>
676      reverse COND_CASES_TAC >- fs[] >>
677      simp[DOMSUB_FAPPLY_THM ] >>
678      `��((n = tm.state) ��� (CELL_NUM c = tm.tape_h))`
679         by fs[CELL_NUM_def,NUM_CELL_def] >> simp[] >>
680      Cases_on `SND (p ' (tm.state,tm.tape_h))` >> rw[] >>
681      ONCE_REWRITE_TAC [FULL_ENCODE_IGNORES_PROGS'] >>
682      CONV_TAC (BINOP_CONV (RAND_CONV (SIMP_CONV (srw_ss()) []))) >>
683      simp[]) >>
684   ONCE_REWRITE_TAC [FULL_ENCODE_IGNORES_PROGS'] >>
685   CONV_TAC (BINOP_CONV (RAND_CONV (SIMP_CONV (srw_ss()) []))) >>
686   simp[]);
687
688val primrec_tmstepf_form = Q.store_thm("primrec_tmstepf_form",
689  `���n.
690    (Cn (proj 0) [
691        pr_cond (Cn (pr2 $* ) [Cn pr_eq [Cn (pr1 nfst) [proj 0] ;
692                                         Cn (pr1 nfst) [K k] ];
693                               Cn pr_eq [Cn pr_mod [
694                                            Cn (pr1 nsnd) [
695                                              Cn (pr1 nsnd) [proj 0]
696                                            ];
697                                            twof
698                                         ];
699                                         Cn (pr1 nsnd) [K k] ] ] )
700                (Cn updn [K snum; K anum ; proj 0] )
701                (Cn (pr1 (tmstepf q)) [proj 0] )
702    ]) [n]
703   =
704    (��tmn. if (nfst tmn = nfst k) ��� (nsnd (nsnd tmn) MOD 2 = nsnd k) then
705             updn [snum; anum; tmn]
706           else tmstepf q tmn) n`,
707  rw[Cn_def,FUN_EQ_THM] >> rw[pr_cond_def]);
708
709
710val primrec_of_tmstepf = Q.store_thm("primrec_of_tmstepf",
711  `primrec (pr1 (tmstepf q)) 1 ==>
712   primrec (Cn (proj 0)  [
713     pr_cond (Cn (pr2 $* ) [
714                     Cn pr_eq [Cn (pr1 nfst) [proj 0] ; Cn (pr1 nfst) [K k] ];
715                     Cn pr_eq [
716                       Cn pr_mod [Cn (pr1 nsnd) [Cn (pr1 nsnd) [proj 0]] ;twof];
717                       Cn (pr1 nsnd) [K k] ] ] )
718             (Cn updn [K snum; K anum ; proj 0] )
719             (Cn (pr1 (tmstepf q)) [proj 0]  )
720   ]) 1`,
721  strip_tac >> SRW_TAC [][primrec_rules] >> SRW_TAC [][pr_cond_def] >>
722  rpt (MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >>
723  fs[UPDATE_TM_NUM_PRIMREC]);
724
725val primrec_tmstepf = Q.store_thm ("primrec_tmstepf",
726  `primrec (pr1 (tmstepf p)) 1`,
727  Induct_on `CARD (FDOM p)`
728  >- (rpt strip_tac >>
729      `FDOM p = {}` by metis_tac[FDOM_FINITE,CARD_EQ_0] >> fs[FDOM_EQ_EMPTY] >>
730      rw[Once tmstepf_def] >> qmatch_abbrev_tac`primrec f 1` >>
731      `f = Cn (pr2 npair) [zerof; Cn (pr1 nsnd) [proj 0]]` suffices_by
732      simp[primrec_rules,primrec_npair,primrec_nsnd] >>
733      simp[Abbr`f`,FUN_EQ_THM] >> Cases >>
734      simp[proj_def,nsnd_def] >> rw[Once tmstepf_def] >> simp[nsnd_def]  )
735  >- (rpt strip_tac >>  MATCH_MP_TAC primrec_pr1  >> rw[Once tmstepf_def] >>
736      `(OLEAST n. (nfst n,CELL_NUM (nsnd n)) ��� FDOM p) <> NONE`
737        by (simp[] >> `FDOM p <> {}` by (strip_tac >> fs[]) >>
738            `���a b. (a,b) IN FDOM p`
739              by metis_tac[SET_CASES,pairTheory.pair_CASES,IN_INSERT] >>
740            qexists_tac`a *, NUM_CELL b` >> simp[]) >>
741      Cases_on `
742        (OLEAST n. (nfst n,CELL_NUM (nsnd n)) ��� FDOM p ��� nfst n ��� 0)` >>
743      fs[]
744      >- (qexists_tac `Cn (pr2 npair) [zerof; Cn (pr1 nsnd) [proj 0]]` >>
745          conj_tac
746          >- simp[primrec_rules,primrec_npair,primrec_nsnd]
747          >- simp[proj_def,nsnd_def]) >>
748      fs[OLEAST_EQ_SOME] >> rename [���nfst k <> 0���] >>
749      `��� s a. (p ' (nfst k,CELL_NUM (nsnd k))) = (s,a)`
750        by metis_tac[pairTheory.pair_CASES] >> simp[] >>
751      `CARD (FDOM (p \\ (nfst k,CELL_NUM (nsnd k)))) = v` by fs[] >>
752      qabbrev_tac`q = p \\ (nfst k,CELL_NUM (nsnd k))` >>
753      `primrec (pr1 (tmstepf q)) 1` by fs[] >>
754      `NUM_CELL (CELL_NUM (nsnd k)) = nsnd k`
755        by metis_tac[npair_11,npair,CELL_NUM_LEM1,NUM_TO_CELL_TO_NUM] >>
756      fs[] >>
757      qabbrev_tac`anum = ACT_TO_NUM a` >>
758      qexists_tac`
759        Cn (proj 0)  [
760          pr_cond
761            (Cn (pr2 $* ) [
762                Cn pr_eq [Cn (pr1 nfst) [proj 0] ; Cn (pr1 nfst) [K k] ];
763                Cn pr_eq [Cn pr_mod [Cn (pr1 nsnd) [Cn (pr1 nsnd) [proj 0]];
764                                     twof];
765                          Cn (pr1 nsnd) [K k]]
766            ])
767            (Cn updn [K s; K anum ; proj 0] )
768            (Cn (pr1 (tmstepf q)) [proj 0]  )
769       ]` >> fs[primrec_of_tmstepf,primrec_tmstepf_form]));
770
771val tm_return_def = tDefine"tm_return"`
772  tm_return tm =
773    if tm.tape_h = Z then 0
774    else
775      case tm.tape_r of
776          [] => 0
777        | h::t  => 1 + tm_return (tm with <| tape_h := h;tape_r:=t|>)
778`
779  (WF_REL_TAC`measure (LENGTH o (��tm. tm.tape_r))` >> simp[]);
780
781val tm_fn_def = Define`
782  tm_fn p args =
783    let tm0 = INITIAL_TM p args
784    in
785      OPTION_MAP (��k. (RUN k tm0)) (OLEAST n. HALTED (RUN n tm0))
786`;
787
788val _ = temp_overload_on ("un_nlist", ���listOfN���)
789
790val INITIAL_TM_NUM_def = Define`
791  INITIAL_TM_NUM = (��l. ���INITIAL_TM FEMPTY (un_nlist (proj 0 l))���)
792`;
793
794val RUN_NUM_def = Define`
795  RUN_NUM p targs = Pr (INITIAL_TM_NUM) (Cn (pr1 (tmstepf p)) [proj 1]) targs
796`;
797
798val INITIAL_TAPE_PROG = Q.store_thm("INITIAL_TAPE_PROG",
799`(INITIAL_TAPE_TM tm l) with prog := p = INITIAL_TAPE_TM (tm with prog := p) l`,
800Cases_on `l` >> simp[INITIAL_TAPE_TM_def])
801
802val UPDATE_TAPE_PROG = Q.store_thm("UPDATE_TAPE_PROG",
803`(tm.prog = p) ==> ((UPDATE_TAPE tm) with prog := p = UPDATE_TAPE tm)`,
804strip_tac >>simp[UPDATE_TAPE_def] >> rw[] >>
805Cases_on `SND (tm.prog ' (tm.state,tm.tape_h))` >>simp[TM_component_equality]);
806
807val UPDATE_PROG_CONSERVE = Q.store_thm("UPDATE_PROG_CONSERVE[simp]",
808`(UPDATE_TAPE tm).prog = tm.prog`,
809simp[UPDATE_TAPE_def] >> rw[] >>
810Cases_on `SND (tm.prog ' (tm.state,tm.tape_h))` >>simp[TM_component_equality]);
811
812val RUN_PROG_CONSERVE = Q.store_thm("RUN_PROG_CONSERVE[simp]",
813`(RUN n tm).prog = tm.prog`,
814Induct_on `n` >> simp[FUNPOW_SUC])
815
816val RUN_PROG = Q.store_thm("RUN_PROG",
817`(tm.prog = p) ==> ((RUN n tm) with prog := p = RUN n tm)`,
818 simp[TM_component_equality] )
819
820val INITIAL_TAPE_TM_PROG = Q.store_thm("INITIAL_TAPE_TM_PROG[simp]",
821`(INITIAL_TAPE_TM tm args).prog = tm.prog`,
822Cases_on `args` >> simp[INITIAL_TAPE_TM_def] )
823
824val INITIAL_TM_PROG = Q.store_thm("INITIAL_TM_PROG[simp]",
825`(INITIAL_TM p args).prog = p`,
826 simp[INITIAL_TM_def])
827
828val RUN_NUM_corr = Q.store_thm("RUN_NUM_corr",
829  `RUN_NUM p [t;args] = ���FUNPOW UPDATE_TAPE t (INITIAL_TM p (un_nlist args))���`,
830  simp[RUN_NUM_def] >> Induct_on `t` >> fs[]
831  >- (simp[INITIAL_TM_NUM_def,INITIAL_TM_def] >>
832      ONCE_REWRITE_TAC[FULL_ENCODE_IGNORES_PROGS
833                         |> Q.INST [`p`|-> `ARB` ] |> SYM] >>
834      simp_tac bool_ss[INITIAL_TAPE_PROG] >>simp[])
835  >- (simp[FUNPOW_SUC] >> rw[SIMP_RULE bool_ss[] tmstepf_update_equiv] >>
836      fs[RUN_PROG]));
837
838val tm_return_num_def = Define`
839  tm_return_num =
840    Pr (Cn (pr1 nsnd) [Cn (pr1 nsnd) [proj 0]])
841       (pr_cond (Cn pr_eq [Cn pr_mod [Cn pr_div [proj 2;proj 0]; twof]; zerof])
842                (proj 1)
843                (Cn (pr2 $+) [proj 1;onef]))
844`;
845
846val _ = temp_set_fixity "*." (Infixl 600)
847val _ = temp_overload_on ("*.", ``��n m. Cn (pr2 $*) [n; m]``)
848
849
850val pr_exp_def = Define`
851pr_exp = Cn (Pr onef ( proj 1 *. ( proj 2))) [proj 1;proj 0]`
852
853val primrec_pr_exp = Q.store_thm(
854"primrec_pr_exp[simp]",
855`primrec pr_exp 2`,
856 rw[pr_exp_def] >> SRW_TAC [][primrec_rules] >> SRW_TAC [][pr_cond_def] >>
857  rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules])  );
858
859
860val tm_log_num_def = Define`
861  tm_log_num =
862    minimise (SOME ���
863              Cn pr_eq [
864                 Cn pr_mod [
865                   Cn pr_div [proj 1; Cn pr_exp [twof;Cn succ [proj 0] ] ];
866                   twof
867                 ];
868                 zerof
869               ])
870`;
871
872val primrec_tm_log_num = Q.store_thm("primrec_tm_log_num",
873  `primrec (Cn pr_eq [Cn pr_mod [Cn pr_div [proj 1;
874                                            Cn pr_exp [twof;Cn succ [proj 0]]];
875                                 twof];
876                      zerof ]) 2`,
877  SRW_TAC [][primrec_rules] >> SRW_TAC [][pr_cond_def] >>
878  rpt (MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >>
879  simp[primrec_pr_exp]);
880
881val recfn_rulesl = CONJUNCTS recfn_rules
882val recfnMin = save_thm("recfnMin", List.nth(recfn_rulesl, 5))
883
884val recfn_tm_log_num = Q.store_thm("recfn_tm_log_num",
885  `recfn tm_log_num 1`,
886  `recfn (SOME o
887          Cn pr_eq [Cn pr_mod [Cn pr_div [proj 1;
888                                          Cn pr_exp [twof;Cn succ [proj 0]]];
889                               twof] ;
890                    zerof]) 2`
891     by simp[primrec_recfn,primrec_tm_log_num] >>
892  rw[tm_log_num_def] >> rfs[recfnMin]);
893
894val primrec_tm_ret_run = Q.store_thm("primrec_tm_ret_run",
895  `primrec tm_return_num 2`,
896  `primrec (Cn (pr1 nsnd) [Cn (pr1 nsnd) [proj 0]]) 1`
897     by (SRW_TAC [][primrec_rules] >>
898         SRW_TAC [][pr_cond_def] >>
899         rpt (MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules])) >>
900  `primrec (pr_cond (Cn pr_eq [Cn pr_mod [Cn pr_div [proj 2;proj 0]; twof];
901                               zerof])
902                    (proj 1)
903                    (Cn (pr2 $+) [proj 1;onef] )) 3`
904     by (SRW_TAC [][primrec_rules] >>
905         SRW_TAC [][pr_cond_def] >>
906         rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]))  >>
907  rw[tm_return_num_def,primrec_pr]);
908
909
910val INITIAL_TAPE_PRES_STATE = Q.store_thm("INITIAL_TAPE_PRES_STATE[simp]",
911  `(INITIAL_TAPE_TM tm k).state = tm.state`,
912  Cases_on `k` >> rw[INITIAL_TAPE_TM_def])
913
914val pr_neq_def = Define`
915  pr_neq = Cn (pr2 $+) [Cn (pr2 $-) [pr_le; cflip pr_le];
916                        Cn (pr2 $-) [cflip pr_le; pr_le]]
917`;
918
919val pr_neq_thm = Q.store_thm(
920  "pr_neq_thm",
921  `pr_neq [n;  m] = nB (n <> m)`,
922  SRW_TAC [ARITH_ss][pr_neq_def] >> Cases_on `n<=m` >> Cases_on `m<=n` >> fs[]);
923
924val primrec_pr_neq = Q.store_thm(
925"primrec_pr_neq[simp]",
926`primrec pr_neq 2`,
927SRW_TAC [][pr_neq_def, primrec_rules]);
928
929val el_zero_def = Define`
930  (el_zero 0 = 1) ���
931  (el_zero (SUC n) =
932    let t = ntl (SUC n)
933    in
934      napp (el_zero n) (ncons (nel t (el_zero n) + 1) 0))
935`;
936
937Theorem ntl_nlist_unnlist:
938  ntl (SUC n) = nlist_of (TL (un_nlist (SUC n)))
939Proof
940  ������n. 0 < n ��� ntl n = nlist_of (TL (listOfN n))��� suffices_by simp[] >>
941  ho_match_mp_tac nlist_ind >> simp[]
942QED
943
944val length_unnlist = Q.store_thm("length_unnlist",
945`0 < LENGTH (un_nlist (SUC n))`,
946fs[DECIDE ���0 < n ��� n ��� 0���])
947
948val ntl_suc_less = Q.store_thm("ntl_suc_less",
949`���n. ntl (SUC n) <= n`,
950strip_tac >> rw[ntl_def,nsnd_le])
951
952Theorem nel_nlist_of:
953  i < nlen l ��� nel i l = EL i (listOfN l)
954Proof
955  simp[GSYM nel_correct]
956QED
957
958Theorem el_zero_corr:
959  el_zero n = nlist_of (GENLIST (LENGTH o un_nlist) (n+1))
960Proof
961  Induct_on `n` >> fs[el_zero_def] >- EVAL_TAC >>
962  `ntl (SUC n) <= n` by simp[ntl_suc_less] >>
963  simp[ADD_CLAUSES,GENLIST,SNOC_APPEND,nel_nlist_of] >>
964  qspec_then ���n + 1��� strip_assume_tac nlist_cases >> fs[ADD1]
965QED
966
967val nleng_def = Define `nleng n = nel n (el_zero n)`
968
969(*  add_persistent_funs ["numpair.nlistrec_def"] *)
970
971val nlen_reduc = Q.store_thm("nlen_reduc",
972  `���n. nlen (SUC n) = nlen (ntl (SUC n)) + 1`,
973  strip_tac >> `SUC n <> 0` by fs[] >>
974  `���h t. SUC n = ncons h t ` by metis_tac[nlist_cases] >> rw[]);
975
976val pr_el_zero_def = Define`
977  pr_el_zero =
978    Cn (Pr (onef)
979           (Cn (pr2 napp) [ proj 1 ;
980                            Cn (pr2 ncons) [
981                              Cn succ [
982                                Cn (pr2 nel) [
983                                  Cn (pr1 ntl) [
984                                    Cn succ [proj 0]
985                                  ];
986                                  proj 1
987                                ]
988                              ];
989                              zerof
990                            ]
991                          ]))
992       [proj 0;onef]
993`;
994
995val primrec_pr_el_zero = Q.store_thm("primrec_pr_el_zero",
996  `primrec pr_el_zero 1`,
997  fs[pr_el_zero_def] >> rpt (irule primrec_cn >> rw[primrec_rules]) >>
998  irule alt_Pr_rule >>
999  fs[primrec_rules] >> rpt (irule primrec_cn >> rw[primrec_rules]))
1000
1001val primrec_el_zero = Q.store_thm("primrec_el_zero",
1002`primrec (pr1 el_zero) 1`,
1003`(���g. primrec g 1 ��� ���n. g [n] = el_zero n)` suffices_by fs[primrec_pr1] >>
1004 qexists_tac `pr_el_zero` >> fs[primrec_pr_el_zero] >> strip_tac >> Induct_on `n` >- EVAL_TAC >>
1005 rw[el_zero_def,pr_el_zero_def] >> `Pr onef (Cn (pr2 napp) [proj 1;
1006 Cn (pr2 ncons) [Cn succ [Cn (pr2 nel) [Cn (pr1 ntl) [Cn succ [proj 0]]; proj 1]]; zerof]]) [n; 1]= pr_el_zero [n]` by
1007 fs[pr_el_zero_def] >> rfs[] >> rw[] >> fs[ADD1] )
1008
1009val primrec_nleng = Q.store_thm("primrec_nleng",
1010`primrec (pr1 nleng) 1`,
1011`(���g. primrec g 1 ��� ���n. g [n] = nleng n)` suffices_by fs[primrec_pr1] >>
1012 qexists_tac`Cn (pr2 nel) [proj 0;Cn (pr1 el_zero) [proj 0]]` >> conj_tac
1013 >- (rpt (irule primrec_cn >> rw[primrec_rules]) >> fs[primrec_el_zero])
1014 >- (strip_tac >> fs[nleng_def]  )  )
1015
1016val Pr_eval = prove(
1017``0 < m ==> (Pr b r (m :: t) = r (m - 1 :: Pr b r (m - 1 :: t) :: t))``,
1018STRIP_TAC THEN SIMP_TAC (srw_ss()) [Once Pr_def, SimpLHS] THEN
1019          Cases_on `m` THEN SRW_TAC [ARITH_ss][]);
1020
1021
1022(* Pr defs, probs use *)
1023val pr_log_def = Define`
1024pr_log = Cn (pr2 $- ) [Cn (Pr (zerof) (Cn (pr2 $+) [proj 1; Cn pr_neq [zerof;Cn pr_div [Cn (pr1 nfst) [proj 2];
1025         Cn pr_exp [Cn (pr1 nsnd) [proj 2];proj 0 ]]]]))
1026            [proj 0;Cn (pr2 npair) [proj 0;proj 1]];onef]`
1027
1028val pr_tl_en_con_fun2_def = Define`
1029pr_tl_en_con_fun2 =
1030               Cn (pr2 $+) [Cn (pr2 $* )
1031  [Cn (pr2 $-) [ Cn pr_exp [twof;Cn (pr2 nel)
1032  [proj 0;proj 2 ]];onef ];
1033      Cn pr_exp [twof;Cn pr_log [proj 1;twof] ] ];
1034                                proj 1] `;
1035
1036val order_flip_def = Define`
1037order_flip = Cn (Pr (zerof )
1038                (Cn (pr2 ncons) [Cn (pr2 nel) [proj 0;proj 2] ;proj 1] ))
1039                [Cn (pr1 nleng) [proj 0];proj 0]`;
1040
1041val pr_tl_en_con_fun4_def = Define`
1042pr_tl_en_con_fun4 = Cn (pr2 $+) [Cn (pr2 $-)
1043                   [Cn pr_exp [twof;Cn (pr2 nel) [proj 0;Cn order_flip [proj 2] ]];onef ];
1044                    Cn (pr2 $* ) [proj 1;Cn pr_exp [twof;Cn succ
1045   [ Cn pr_log [Cn pr_exp [twof;Cn (pr2 nel) [proj 0;Cn order_flip [proj 2]]] ; twof]] ]]] `;
1046
1047val pr_tl_en_con_def = Define`
1048pr_tl_en_con = Cn (pr1 DIV2) [Cn (Pr (zerof) (pr_tl_en_con_fun4)) [Cn (pr1 nleng) [proj 0];proj 0]]`;
1049
1050val primrec_order_flip = Q.store_thm("primrec_order_flip",
1051`primrec order_flip 1`,
1052rw[order_flip_def] >> rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >>fs[primrec_nleng]  )
1053
1054val primrec_pr_log = Q.store_thm("primrec_pr_log",
1055`primrec pr_log 2`,
1056rw[pr_log_def] >> rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> irule alt_Pr_rule >> rw[primrec_rules] >> rpt (irule primrec_cn >> rw[primrec_rules]));
1057
1058
1059val primrec_pr_tl_en_con_fun4 = Q.store_thm("primrec_pr_tl_en_con_fun4",
1060`primrec pr_tl_en_con_fun4 3`,
1061rw[pr_tl_en_con_fun4_def] >> rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules]) >> rw[primrec_rules,primrec_pr_exp,primrec_order_flip,primrec_pr_log] >> fs[primrec_nleng] );
1062
1063val primrec_pr_tl_en_con = Q.store_thm("primrec_pr_tl_en_con",
1064`primrec pr_tl_en_con 1`,
1065SRW_TAC [][pr_tl_en_con_def,primrec_rules] >>
1066        rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules,primrec_div2,primrec_nleng]) >>
1067        fs[primrec_nleng] >>  irule alt_Pr_rule >> rw[primrec_pr_tl_en_con_fun4] );
1068
1069
1070val invtri_zero = Q.store_thm("invtri_zero[simp]",
1071`invtri 0 = 0`,
1072EVAL_TAC)
1073
1074val ntl_zero = Q.store_thm("ntl_zero[simp]",
1075`ntl 0 = 0`,
1076EVAL_TAC)
1077
1078val invtri_nzero = Q.store_thm("invtri_nzero[simp]",
1079`(invtri n = 0) <=> (n = 0)`,
1080eq_tac >> fs[] >>
1081       SRW_TAC [][invtri_def] >>
1082       Q.SPECL_THEN [`n`, `0`] MP_TAC invtri0_thm >>
1083       SRW_TAC [ARITH_ss][tri_def] >> `n < SUC 0` by metis_tac[SND_invtri0] >> rw[]
1084)
1085
1086val nsnd_fun_thm = Q.store_thm("nsnd_fun_thm[simp]",
1087`(nsnd n = n) <=>  (n = 0)`,
1088eq_tac >> rw[nsnd_def]  >> Cases_on `n` >> fs[] >>
1089`tri (invtri (SUC n')) = 0` by  fs[SUB_EQ_EQ_0] >> `tri 0 = 0` by fs[tri_def] >>
1090`invtri (SUC n') = 0` by rfs[tri_11]  >>  fs[])
1091
1092val nsnd_lthen = Q.store_thm("nsnd_lthen[simp]",
1093`���n. (nsnd n < n)<=> (n<> 0)`,
1094strip_tac >> eq_tac >> fs[] >> strip_tac >> `nsnd n <= n` by fs[nsnd_le] >> `nsnd n <> n` by fs[] >> rw[])
1095
1096val FUNPOW_mono = Q.store_thm("FUNPOW_mono",
1097`(���n m. m <= n ==> f m <= f n) ==> (���n m k. m <= n ==> FUNPOW f k m <= FUNPOW f k n)`,
1098rpt strip_tac >> Induct_on `k` >> fs[] >> fs[FUNPOW_SUC] )
1099
1100val ENCODE_TL_DIV2 = Q.store_thm("ENCODE_TL_DIV2",
1101`ENCODE (TL (h::t)) = DIV2 (ENCODE (h::t))`,
1102Cases_on `h` >> fs[ENCODE_def,DIV2_def,TWO_TIMES_DIV_TWO_thm])
1103
1104val el_zero_exp = Q.store_thm("el_zero_exp",
1105`el_zero n = nlist_of ((GENLIST (LENGTH ��� un_nlist) n) ++ [(LENGTH ��� un_nlist) n])`,
1106`n+1 = SUC n` by fs[ADD1] >> rw[GENLIST,SNOC_APPEND,el_zero_corr] )
1107
1108val el_zero_napp = Q.store_thm("el_zero_napp",
1109`el_zero n = napp (nlist_of (GENLIST (LENGTH ��� un_nlist) n)) (nlist_of [(LENGTH ��� un_nlist) n])`,
1110fs[el_zero_exp] )
1111
1112val r_zero_def = Define`
1113  (r_zero 0 = ncons 0 0) ���
1114  (r_zero (SUC n) =
1115   let t = ntl (SUC n); r0n = r_zero n; revt = nel t r0n;
1116      res = napp revt (ncons (nhd (SUC n)) 0)
1117   in
1118     napp r0n (ncons res 0))
1119`;
1120
1121val r_zero_corr = Q.store_thm("r_zero_corr",
1122  `r_zero n = nlist_of (GENLIST (nlist_of o REVERSE o un_nlist) ( n+1))`,
1123  Induct_on `n` >> fs[r_zero_def,ADD_CLAUSES] >>
1124  `ntl (SUC n)<= n` by fs[ntl_suc_less]>>
1125  rw[GENLIST, SNOC_APPEND,nel_nlist_of] >>
1126  `���l. n+1 = nlist_of l` by metis_tac[nlist_of_SURJ] >> rw[ADD1] >>
1127   Cases_on `l` >> fs[])
1128
1129val _ = overload_on ("order_flip" ,``pr1 (��n. nel n (r_zero n))``)
1130
1131val order_flip_corr = Q.store_thm("order_flip_corr",
1132`order_flip [n] = nlist_of (REVERSE (un_nlist n))`,
1133fs[r_zero_corr,nel_nlist_of])
1134
1135Theorem order_flip_ncons[simp]:
1136  order_flip [ncons h t] = napp (order_flip [t]) (ncons h 0)
1137Proof   fs[order_flip_corr]
1138QED
1139
1140Definition list_rec_comb_def:
1141  list_rec_comb c n 0 = ncons n 0  ���
1142  list_rec_comb c n (SUC k) =
1143    let t = ntl (SUC k); h=nhd (SUC k); rl = list_rec_comb c n k;
1144        r = nel t rl
1145    in napp rl (ncons (c [h; t; r]) 0)
1146End
1147
1148val LIST_REC_def = Define`(LIST_REC c (n:num) [] = n) ���
1149     (LIST_REC c n (h::t) = c [h;nlist_of t;LIST_REC c n t])`
1150
1151Theorem list_rec_comb_corr:
1152  list_rec_comb c n k = nlist_of (GENLIST (LIST_REC c n o un_nlist) (k+1))
1153Proof
1154  Induct_on `k` >> fs[list_rec_comb_def,LIST_REC_def,ADD_CLAUSES]>>
1155  `ntl (SUC k)<= k` by fs[ntl_suc_less]>>
1156  rw[GENLIST, SNOC_APPEND,nel_nlist_of] >> rw[] >> rw[ADD1] >>
1157  `���l. k+1 = nlist_of l` by metis_tac[nlist_of_SURJ]>> rw[] >>
1158  Cases_on `l` >> fs[] >> rw[LIST_REC_def]
1159QED
1160
1161Theorem primrec_list_rec_comb:
1162  primrec c 3 ==> primrec (pr1 (list_rec_comb c n)) 1
1163Proof
1164  strip_tac >> irule primrec_pr1 >>
1165  qexists_tac`
1166    Pr1 (ncons n 0) (
1167      Cn (pr2 napp) [
1168        proj 1;
1169        Cn (pr2 ncons) [
1170          Cn c [
1171            Cn (pr1 nhd) [Cn succ [proj 0]];
1172            Cn (pr1 ntl) [Cn succ [proj 0]];
1173            Cn (pr2 nel) [Cn (pr1 ntl) [Cn succ [proj 0]];proj 1 ]
1174          ];
1175          zerof
1176        ]
1177      ]
1178    )
1179  ` >> conj_tac
1180  >- (irule primrec_Pr1 >>
1181      rpt (irule primrec_cn >> rw[primrec_rules,primrec_napp,primrec_ncons])) >>
1182  Induct >> fs[list_rec_comb_def]
1183QED
1184
1185val list_num_rec_thm = Q.store_thm("list_num_rec_thm",
1186`���n c.(primrec c 3)==> ���f.(primrec f 1) ��� (f [0] = n) ��� (���h t. f [ncons h t] = c [h; t; (f [t])])`,
1187rpt strip_tac >> qexists_tac`Cn (pr2 nel) [proj 0;Cn (pr1 (list_rec_comb c n)) [proj 0]] ` >>
1188rpt conj_tac >- (rpt (irule primrec_cn >> rw[primrec_rules,primrec_nel,primrec_list_rec_comb]))>>
1189 simp[list_rec_comb_def] >> simp[list_rec_comb_corr,nel_nlist_of,LIST_REC_def] )
1190
1191val nleng_thm = new_specification("nleng_def", ["nleng"],
1192list_num_rec_thm |> SPECL[``0n``,``Cn succ [proj 2]``]
1193                 |> SIMP_RULE (srw_ss())[primrec_cn, primrec_rules])
1194
1195val nrev_thm = new_specification("nrev_def", ["nrev"],
1196list_num_rec_thm |> SPECL[``0n``,``Cn (pr2 napp) [proj 2;Cn (pr2 ncons) [proj 0;zerof] ]``]
1197                 |> SIMP_RULE (srw_ss())[primrec_cn, primrec_rules])
1198
1199val concatWith_Z_thm = new_specification("concatWith_Z_def", ["concatWith_Z"],
1200 list_num_rec_thm |> SPECL[``0n``,``pr_cond (Cn pr_eq [proj 1;zerof])
1201 (proj 0) (Cn (pr2 napp) [proj 0; Cn (pr2 napp) [onef;proj 2]])``]
1202                 |> SIMP_RULE (srw_ss())[primrec_cn, primrec_rules])
1203
1204Theorem concatWith_Z_corr:
1205  concatWith_Z [x] = nlist_of (concatWith [0] (MAP un_nlist (un_nlist x)))
1206Proof
1207  completeInduct_on `x` >>
1208  `(x = 0) ��� ���h t. x = ncons h t` by metis_tac[nlist_cases] >>
1209  simp[concatWith_Z_thm,concatWith_def] >> rw[] >>
1210  simp[concatWith_Z_thm,concatWith_def] >>
1211  `t < ncons h t`
1212     by (simp[ncons_def] >>
1213         `t = nsnd (h *, t)` by simp[] >>
1214         `nsnd (h *, t) <= h *, t` by simp[nsnd_le] >> simp[] ) >>
1215  RES_TAC >> simp[concatWith_def] >>
1216  `���h' t'. t = ncons h' t'` by metis_tac[nlist_cases] >>
1217  simp[concatWith_def] >>
1218  ���ncons 0 0 = 1��� suffices_by (disch_then (SUBST1_TAC o SYM) >> simp[]) >>
1219  EVAL_TAC
1220QED
1221
1222val INITIAL_TAPE_PRES_L = Q.store_thm("INITIAL_TAPE_PRES_L[simp]",
1223`(INITIAL_TAPE_TM tm (h::t)).tape_l = []`,
1224fs[INITIAL_TAPE_TM_def])
1225
1226val tape_encode_def = Define `tape_encode = pr_cond (Cn pr_eq [proj 1;zerof])
1227   (Cn (pr2 npair) [proj 0;Cn (pr2 $*) [twof;proj 2]])
1228  (Cn (pr2 npair) [proj 0;Cn succ [Cn (pr2 $* ) [twof;proj 2]]])`
1229
1230val primrec_tape_encode = Q.store_thm("primrec_tape_encode[simp]",
1231`primrec tape_encode 3`,
1232fs[tape_encode_def] >> irule primrec_pr_cond >> rpt conj_tac >>
1233rpt (irule primrec_cn >>
1234     rw[primrec_rules,primrec_pr_cond,primrec_pr_eq,primrec_pr_mult]));
1235
1236val tape_encode_corr = Q.store_thm("tape_encode_corr",
1237`tape_encode [ENCODE tm.tape_l;NUM_CELL tm.tape_h;ENCODE tm.tape_r] = ENCODE_TM_TAPE tm`,
1238fs[tape_encode_def,ENCODE_TM_TAPE_def] >> `CELL_NUM (NUM_CELL tm.tape_h) = tm.tape_h` by
1239 fs[CELL_NUM_NUM_CELL]>> `CELL_NUM 0 = Z` by fs[CELL_NUM_def]>>`NUM_CELL Z = 0` by fs[NUM_CELL_def]
1240>>`(NUM_CELL tm.tape_h = 0) ��� (tm.tape_h = Z)` by metis_tac[NUM_CELL_INJ] >>rw[] )
1241
1242val tape_encode_corr_sym = Q.store_thm("tape_encode_corr_sym",
1243`ENCODE_TM_TAPE tm = tape_encode [ENCODE tm.tape_l;NUM_CELL tm.tape_h;ENCODE tm.tape_r]`,
1244fs[tape_encode_corr])
1245
1246
1247(* Define correctly so it matches what it should *)
1248val pr_INITIAL_TAPE_TM_NUM_def = Define`
1249pr_INITIAL_TAPE_TM_NUM = pr_cond (Cn pr_eq [proj 1;zerof]) (proj 0) (Cn (pr2 npair)
1250[Cn (pr1 nfst) [proj 0];Cn (pr2 npair) [Cn (pr1 nhd) [proj 1];Cn (pr1 ntl) [proj 1]] ])`;
1251
1252val primrec_pr_INITIAL_TAPE_TM_NUM = Q.store_thm(
1253  "primrec_pr_INITIAL_TAPE_TM_NUM[simp]",
1254  `primrec pr_INITIAL_TAPE_TM_NUM 2`,
1255  fs[pr_INITIAL_TAPE_TM_NUM_def] >> `0<2` by fs[] >>
1256  irule primrec_pr_cond >> rpt conj_tac >>
1257  rpt (irule primrec_cn >>
1258       rw[primrec_rules,primrec_pr_eq,primrec_nsnd,primrec_nfst]) >>
1259  fs[primrec_proj]);
1260
1261val pr_INITIAL_TM_NUM_def = Define`
1262pr_INITIAL_TM_NUM = Cn (pr2 npair) [zerof;Cn tape_encode
1263 [Cn (pr1 nfst) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]];
1264  Cn (pr1 nfst) [Cn (pr1 nsnd) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]]];
1265  Cn (pr1 nsnd) [Cn (pr1 nsnd) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]]]]]`;
1266
1267val pr_ODD_def = Define`pr_ODD = pr_cond (Cn pr_eq [Cn pr_mod [proj 0;twof];onef]) onef zerof`
1268
1269val pr_ODD_corr = Q.store_thm("pr_ODD_corr",
1270`pr_ODD [x] = if ODD x then 1 else 0`,
1271fs[pr_ODD_def] >> Cases_on `ODD x` >- metis_tac[ODD_MOD_TWO_lem] >>
1272`EVEN x` by metis_tac[EVEN_OR_ODD] >> fs[EVEN_MOD2]);
1273
1274val GENLIST_ZERO = Q.store_thm("GENLIST_ZERO",
1275`(GENLIST a b = []) <=> (b=0)`,
1276eq_tac >> fs[GENLIST] >> strip_tac >> Cases_on `b` >> fs[GENLIST] );
1277
1278val concatWith_Z_empty = Q.store_thm("concatWith_Z_empty",
1279`(concatWith [Z] (MAP (GENLIST (K O)) args) = []) <=> ((args = []) ��� (args = [0]))`,
1280eq_tac >- (strip_tac >> Cases_on `MAP (GENLIST (K O)) args` >> rfs[concatWith_def] >>
1281      Cases_on `t` >> rfs[concatWith_def] >> `GENLIST (K O) x0 = []` by fs[] >> fs[GENLIST_ZERO])
1282       >- (strip_tac >> rw[concatWith_def]));
1283
1284val head_concatWith = Q.store_thm("head_concatWith",
1285`((l<> []) ��� (HD l <> [])) ==> (HD (concatWith a l) = HD (HD l))`,
1286strip_tac >> Cases_on `l` >> fs[concatWith_def] >> Cases_on `t` >> fs[concatWith_def,HD] >>
1287                                 Cases_on `h` >> fs[])
1288
1289val head_nil_concatWith = Q.store_thm("head_nil_concatWith[simp]",
1290`HD (concatWith [a] ([]::b::c)) = a`,
1291rw[concatWith_def])
1292
1293val odd_encode_hd_concat = Q.store_thm("odd_encode_hd_concat",
1294`(concatWith [Z] (MAP (GENLIST (K O)) args) <> []) ==> (NUM_CELL (HD (concatWith [Z] (MAP (GENLIST (K O)) args))) = 1 - pr_eq [proj 0 args;0])`,
1295strip_tac >> fs[concatWith_Z_empty]
1296          >> Cases_on `args` >- rw[concatWith_def] >> Cases_on `h = 0` >> simp[proj_def]>>
1297          Cases_on `MAP (GENLIST (K O)) t`>> simp[]
1298          >- (`t = []` by fs[MAP_EQ_NIL] >> rw[]) >> simp[concatWith_def]
1299          >- (`���h'. h = SUC h'` by metis_tac[num_CASES] >> rw[] >> fs[HD_GENLIST])
1300          >- (`���h'. h = SUC h'` by metis_tac[num_CASES] >> rw[] >> fs[GENLIST_CONS])  )
1301
1302val nfst_zero = Q.store_thm("nfst_zero[simp]", `nfst 0 = 0`, EVAL_TAC)
1303val nsnd_zero = Q.store_thm("nsnd_zero[simp]", `nsnd 0 = 0`, EVAL_TAC)
1304val nhd_zero = Q.store_thm("nhd_zero[simp]", `nhd 0 = 0`, EVAL_TAC)
1305val ntl_zero = Q.store_thm("nstl_zero[simp]", `ntl 0 = 0`, EVAL_TAC)
1306
1307val num_cell_encode_hd_concat = Q.store_thm("num_cell_encode_hd_concat",
1308`(concatWith [Z] (MAP (GENLIST (K O)) args) <> []) ==> (NUM_CELL (HD (concatWith [Z] (MAP (GENLIST (K O)) args))) = 1 - pr_eq [ nhd  (nlist_of args);0])`,
1309rw[odd_encode_hd_concat] >> Cases_on `args` >> simp[nhd_thm]  )
1310
1311val encode_concat_def = tDefine "encode_concat" `
1312    (encode_concat 0 = 0) ���
1313    (encode_concat args = ((2** (nhd args)) - 1) +
1314                          (2* ((2** (nhd args))) * (encode_concat (ntl args))))`
1315(qexists_tac `$<` >> conj_tac >- simp[prim_recTheory.WF_LESS] >> strip_tac >>
1316`ntl (SUC v) <= v` by simp[ntl_suc_less] >> `v < SUC v` by simp[prim_recTheory.LESS_SUC_REFL]>>
1317rw[])
1318
1319val encode_tl_concat_def = Define`encode_tl_concat args = DIV2 (encode_concat args)`
1320
1321val ENCODE_GENLIST_p_Z = Q.store_thm("ENCODE_GENLIST_p_Z",
1322`ENCODE (GENLIST (K O) h ++ [Z] ++ b) = ((2**h) - 1) + (2*((2**h))*(ENCODE b))`,
1323Induct_on `h` >> simp[ENCODE_def] >> simp[GENLIST_CONS] >> simp[ENCODE_def] >>rw[EXP] >>
1324`2 * (2 ** h ��� 1 + 2 * (ENCODE b * 2 ** h)) = 2*2 ** h ��� 2*1 + 4 * (ENCODE b * 2 ** h)` by fs[]>>
1325rw[] >> `2<=2*2**h` by (rpt (pop_assum kall_tac) >> Induct_on `h` >> simp[])  >> simp[])
1326
1327val ENCODE_GENLIST_O = Q.store_thm("ENCODE_GENLIST_O",
1328`ENCODE (GENLIST (K O) h) = 2 ** h ��� 1`,
1329Induct_on `h` >> simp[ENCODE_def,GENLIST_CONS,EXP] >> `1<=2**h` suffices_by simp[] >>
1330          `0<2**h` suffices_by decide_tac >> simp[])
1331
1332val encode_concat_corr = Q.store_thm("encode_concat_corr",
1333`ENCODE (concatWith [Z] (MAP (GENLIST (K O)) args)) = encode_concat (nlist_of args)`,
1334Induct_on `args` >> fs[concatWith_def,ENCODE_def,encode_concat_def] >> strip_tac >>
1335`nhd (ncons h (nlist_of args)) = h` by simp[nhd_thm] >> `ntl (ncons h (nlist_of args)) =
1336nlist_of args` by simp[ntl_thm] >> `ncons h (nlist_of args) <> 0` by simp[ncons_not_nnil] >>
1337`��� n0. ncons h (nlist_of args) = SUC n0 ` by metis_tac[num_CASES] >>rw[encode_concat_def] >>
1338full_simp_tac bool_ss[] >>
1339Cases_on `args` >> simp[concatWith_def] >- simp[encode_concat_def,ENCODE_GENLIST_O] >>
1340simp[ENCODE_GENLIST_p_Z] >> fs[])
1341
1342val pr_INITIAL_TM_NUM_def = Define`
1343pr_INITIAL_TM_NUM = Cn (pr2 npair) [zerof;Cn tape_encode
1344                                             [zerof;
1345                                    Cn (pr2 $-) [onef ;Cn pr_eq [Cn (pr1 nhd) [proj 0];zerof]];
1346                                              Cn (pr1 encode_tl_concat) [proj 0]]]`
1347
1348Theorem encode_concat_list_rec:
1349  encode_concat n =
1350  nel n (
1351    list_rec_comb (
1352      Cn (pr2 $+) [
1353        Cn (pr1 PRE) [Cn (pr2 $EXP) [twof;proj 0]];
1354        Cn (pr2 $*) [twof;Cn (pr2 $*) [proj 2;Cn (pr2 $EXP) [twof;proj 0]]]
1355      ]
1356    ) 0 n
1357  )
1358Proof
1359  rw[list_rec_comb_corr] >>
1360  `���l.  n =  nlist_of l` by metis_tac[nlist_of_SURJ] >> rw[] >>
1361  Induct_on `l` >> simp[LIST_REC_def,encode_concat_def] >> strip_tac >>
1362  `ncons h (nlist_of l) <> 0` by simp[ncons_not_nnil] >>
1363  `��� n0. ncons h (nlist_of l) = SUC n0 ` by metis_tac[num_CASES] >>
1364  rw[encode_concat_def] >>
1365  full_simp_tac bool_ss[] >> pop_assum (SUBST_ALL_TAC o SYM) >>
1366  simp[nel_nlist_of,LIST_REC_def]
1367QED
1368
1369val pr_encode_concat_def = Define`
1370  pr_encode_concat =
1371  Cn (pr2 nel) [
1372   proj 0;
1373   Cn (pr1 (list_rec_comb (Cn (pr2 $+) [
1374     Cn (pr1 PRE) [Cn (pr2 $EXP) [twof;proj 0]];
1375     Cn (pr2 $*) [twof;Cn (pr2 $*) [proj 2;Cn (pr2 $EXP) [twof;proj 0]]]
1376   ]) 0)) [proj 0]
1377  ]`;
1378
1379val pr_encode_tl_concat_def = Define`pr_encode_tl_concat = Cn (pr1 DIV2) [Cn (pr2 nel) [proj 0;
1380   Cn (pr1 (list_rec_comb (Cn (pr2 $+) [Cn (pr1 PRE) [Cn (pr2 $EXP) [twof;proj 0]];
1381   Cn (pr2 $*) [twof;Cn (pr2 $*) [proj 2;Cn (pr2 $EXP) [twof;proj 0]]]]) 0)) [proj 0]]]`
1382
1383
1384val primrec_exp = Q.store_thm("primrec_exp",
1385`primrec (pr2 $**) 2`,
1386 irule primrec_pr2 >>qexists_tac `pr_exp` >> conj_tac >-simp[primrec_pr_exp] >> simp[pr_exp_def]>>
1387Induct >> Induct >> simp[] >> rw[EXP])
1388
1389val primrec_pr_INITIAL_TM_NUM = Q.store_thm("primrec_pr_INITIAL_TM_NUM[simp]",
1390`primrec pr_INITIAL_TM_NUM 1`,
1391SRW_TAC [][pr_INITIAL_TM_NUM_def,primrec_rules] >>
1392        rpt ( MATCH_MP_TAC primrec_cn >> SRW_TAC [][primrec_rules,concatWith_Z_thm,primrec_pr_INITIAL_TAPE_TM_NUM,primrec_tape_encode,primrec_npair,primrec_ntl,primrec_nhd]) >>
1393        irule primrec_pr1 >> qexists_tac `pr_encode_tl_concat` >> conj_tac
1394        >- (rw[pr_encode_tl_concat_def] >>rpt (irule primrec_cn >> rw[primrec_rules,primrec_nel] )>-
1395(`primrec (Cn (pr2 $+)
1396             [Cn (pr1 PRE) [Cn (pr2 $** ) [twof; proj 0]];
1397              twof *. (proj 2 *. Cn (pr2 $** ) [twof; proj 0])]) 3` suffices_by
1398        rw[primrec_list_rec_comb] >> rpt (irule primrec_cn >> rw[primrec_rules,primrec_nel] ) >>
1399        simp[primrec_exp,primrec_div2]) >> simp[primrec_div2] )
1400        >- (strip_tac >> simp[encode_concat_list_rec] >> `���l.  n =  nlist_of l` by metis_tac[nlist_of_SURJ] >> rw[] >> Induct_on `l` >> simp[list_rec_comb_def,encode_tl_concat_def,encode_concat_def,nlist_of_def,pr_encode_concat_def] >- simp[pr_encode_concat_def,pr_encode_tl_concat_def,list_rec_comb_def] >> strip_tac >> simp[pr_encode_tl_concat_def,encode_concat_list_rec]   ) )
1401
1402
1403
1404val tape_encode_thm = Q.store_thm("tape_encode_thm",
1405`tape_encode [a;b;c] = if b=0 then a *, (2* c) else a *, (SUC (2*c))`,
1406fs[tape_encode_def])
1407
1408val tape_encode_eq = Q.store_thm("tape_encode_eq",
1409`(((b=0) ��� (b=1)) ��� ((e=0) ��� (e=1))) ==>
1410                     ( (tape_encode [a;b;c] = tape_encode [d;e;f]) <=> ((a=d) ��� (b=e) ���(c=f)))`,
1411strip_tac >> eq_tac >> rw[tape_encode_thm]
1412         >- (CCONTR_TAC >> rfs[] >> `ODD (SUC (2* f))` by fs[ODD_DOUBLE] >> `EVEN (2*c)` by
1413           fs[EVEN_DOUBLE] >> rfs[EVEN_AND_ODD] >> fs[EVEN,EVEN_DOUBLE] )
1414         >- (CCONTR_TAC >> rfs[] >> `ODD (SUC (2* c))` by fs[ODD_DOUBLE] >> `EVEN (2*f)` by
1415           fs[EVEN_DOUBLE] >> rfs[EVEN_AND_ODD] >> metis_tac[EVEN_AND_ODD])  )
1416
1417val ENCODE_TL_concatWith = Q.store_thm("ENCODE_TL_concatWith",
1418`(concatWith [Z] (MAP (GENLIST (K O)) args) = h::t) ==> (ENCODE t = encode_tl_concat (nlist_of args))`,
1419rw[] >> simp[encode_tl_concat_def] >> `ENCODE t = ENCODE (TL (concatWith [Z] (MAP (GENLIST (K O)) args)))`
1420by simp[] >> metis_tac[encode_concat_corr,ENCODE_TL_DIV2])
1421
1422Theorem primrec_INITIAL_TM_NUM:
1423  primrec INITIAL_TM_NUM 1
1424Proof
1425  `INITIAL_TM_NUM = pr_INITIAL_TM_NUM`
1426    suffices_by fs[primrec_pr_INITIAL_TM_NUM] >>
1427  fs[FUN_EQ_THM] >> strip_tac >>
1428  fs[INITIAL_TM_NUM_def,INITIAL_TM_def,INITIAL_TAPE_TM_def,
1429     FULL_ENCODE_TM_def,pr_INITIAL_TM_NUM_def,tape_encode_corr_sym] >>
1430  Cases_on `(concatWith [Z] (MAP (GENLIST (K O)) (un_nlist (proj 0 x))))` >>
1431  fs[INITIAL_TAPE_TM_def]  >>
1432  fs[pr_INITIAL_TM_NUM_def,pr_INITIAL_TAPE_TM_NUM_def,tape_encode_corr,
1433     concatWith_Z_corr]
1434  >- (`���l. proj 0 x = nlist_of l` by metis_tac[nlist_of_SURJ] >>fs[]>>
1435      `(l = []) ��� (l = [0])` by rfs[concatWith_Z_empty] >>
1436      fs[encode_tl_concat_def,encode_concat_def,ENCODE_def,DIV2_def,
1437         ncons_def]  >>EVAL_TAC) >>
1438  simp[ENCODE_def] >>
1439  `ENCODE t = encode_tl_concat (proj 0 x)`
1440    by metis_tac[ENCODE_TL_concatWith,listOfN_nlist, nlist_listOfN] >>
1441  simp[ENCODE_TL_concatWith] >>
1442  `NUM_CELL h =
1443   NUM_CELL
1444     (HD (concatWith [Z] (MAP (GENLIST (K O)) (un_nlist (proj 0 x)))))`
1445    by simp[] >>
1446  simp[odd_encode_hd_concat] >>
1447  `nB (proj 0 (un_nlist (proj 0 x)) ��� 0) = nB (nhd (proj 0 x) ��� 0)`
1448    suffices_by simp[]  >> rw[] >>
1449  Cases_on `x` >> simp[] >>
1450  `���l.  h' =  nlist_of l` by metis_tac[nlist_of_SURJ] >> rw[]>>
1451  Cases_on `l` >> simp[]
1452QED
1453
1454val RUN_NUM_p = Q.store_thm("RUN_NUM_p",
1455  `RUN_NUM p = Pr INITIAL_TM_NUM (Cn (pr1 (tmstepf p)) [proj 1]) `,
1456  simp[FUN_EQ_THM,RUN_NUM_def]);
1457
1458val primrec_RUN_NUM = Q.store_thm("primrec_RUN_NUM",
1459  `primrec (RUN_NUM p) 2`,
1460  fs[RUN_NUM_p] >> irule alt_Pr_rule >> rpt conj_tac
1461  >- fs[primrec_INITIAL_TM_NUM] >>
1462  irule primrec_cn >> rpt conj_tac >- fs[primrec_rules] >> fs[primrec_tmstepf]);
1463
1464val Pr_thm_one = Q.store_thm("Pr_thm_one",
1465`(Pr b r (1::t) = r (0::Pr b r (0::t)::t))`,
1466rw[Pr_thm] >> `Pr b r (1::t) = Pr b r ((SUC 0)::t)` by metis_tac[ONE] >> rw[])
1467
1468val zero_less_nB = Q.store_thm("zero_less_nB[simp]",
1469`(0 < nB A) <=> A`,
1470Cases_on `A` >> fs[])
1471
1472
1473val recfn_rulesl = CONJUNCTS recfn_rules
1474val recfnCn = save_thm("recfnCn", List.nth(recfn_rulesl, 3))
1475val recfnPr = save_thm("recfnPr", List.nth(recfn_rulesl, 4))
1476val recfnMin = save_thm("recfnMin", List.nth(recfn_rulesl, 5))
1477
1478(* Probably need to include a 'tape reset' type function, ie tm_return_num *)
1479val recfn_tm_def = Define`
1480  recfn_tm p = recCn (SOME o (RUN_NUM p)) [
1481                        minimise (SOME o (Cn (pr1 nfst) [RUN_NUM p]  )  ) ;
1482                        SOME o proj 0] `
1483
1484val recfn_tm_recfn = Q.store_thm("recfn_tm_recfn",
1485  `recfn (recfn_tm p) 1`,
1486  rw[recfn_tm_def] >> fs[primrec_RUN_NUM,primrec_recfn] >> irule recfnCn >>
1487  rw[recfn_rules]
1488  >- (irule recfnMin >> fs[] >> irule primrec_recfn >>
1489      rpt (irule primrec_cn >>
1490           rw[primrec_rules,primrec_pr_eq,primrec_RUN_NUM,primrec_pr_add]))
1491  >- (fs[primrec_RUN_NUM,primrec_recfn]));
1492
1493val UPDATE_TAPE_HALTED = Q.store_thm("UPDATE_TAPE_HALTED[simp]",
1494`(HALTED tm) ==> (UPDATE_TAPE tm = tm)`,
1495rw[] >> fs[UPDATE_TAPE_def,HALTED_def] >> simp[TM_component_equality]);
1496
1497val run_num_halted = Q.store_thm("run_num_halted",
1498  `���n. HALTED (RUN n (INITIAL_TM p args)) ��� n<=m ==>
1499       (RUN_NUM p [m; nlist_of args] = RUN_NUM p [SUC m; nlist_of args])`,
1500  rpt strip_tac >> `���k. m=n+k` by metis_tac[LESS_EQ_EXISTS] >>
1501  rw[RUN_NUM_corr,FUNPOW_SUC] >> qmatch_abbrev_tac `���tm��� = ���UPDATE_TAPE tm���` >>
1502  `HALTED tm` suffices_by simp[] >>
1503  qunabbrev_tac `tm` >> fs[] >> Induct_on `k` >>
1504  simp[] >> rw[] >> simp[FUNPOW_SUC,ADD_CLAUSES]);
1505
1506val main_eq_thm = Q.store_thm("main_eq_thm",
1507  `���p. ���f. recfn f 1 ���
1508           ���args.
1509             OPTION_MAP FULL_ENCODE_TM (tm_fn p args) = f [nlist_of args]`,
1510  strip_tac >> qexists_tac`recfn_tm p` >> conj_tac
1511  >- fs[recfn_tm_recfn] >>
1512  strip_tac >> fs[tm_fn_def,recfn_tm_def] >>
1513  Cases_on `(OLEAST n. HALTED (RUN n (INITIAL_TM p args)))` >>
1514  fs[optionTheory.OPTION_MAP_DEF] >> rw[RUN_NUM_corr] >> fs[recCn_def]
1515  >- (fs[] >>fs[minimise_def] >> rpt strip_tac >> rfs[RUN_NUM_corr] >>
1516      first_x_assum (qspec_then `n` mp_tac) >> simp[HALTED_def] >>
1517      fs[])
1518  >- (fs[OLEAST_EQ_SOME,minimise_def] >> rw[]
1519      >- (rename[`RUN n (INITIAL_TM p args)`] >> qexists_tac `n` >>
1520          fs[HALTED_def,RUN_NUM_corr] >> metis_tac[])
1521      >- (fs[RUN_NUM_corr] >> qmatch_abbrev_tac `���RUN i tm��� = ���RUN j tm���`>>
1522          `i=j` suffices_by simp[] >> qunabbrev_tac `i` >> SELECT_ELIM_TAC >>
1523          rw[]
1524          >- (fs[HALTED_def] >> metis_tac[])
1525          >- (fs[HALTED_def] >>
1526              qmatch_abbrev_tac `a=b` >>`��(a<b)�����(b<a)` suffices_by simp[] >>
1527              rpt strip_tac >> metis_tac[NOT_ZERO_LT_ZERO]))
1528      >- (fs[RUN_NUM_corr] >> first_x_assum (qspec_then `x` mp_tac)>>
1529          rpt strip_tac >> fs[HALTED_def] >>
1530          `���i. i < x ��� ((RUN i (INITIAL_TM p args)).state = 0)` by fs[] >>
1531          metis_tac[])));
1532
1533(* as final step, should show that we can extract number under head *)
1534
1535val _ = export_theory();
1536