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