1open HolKernel Parse boolLib bossLib finite_mapTheory;
2open recursivefnsTheory;
3open prnlistTheory;
4open nlistTheory
5open primrecfnsTheory;
6open listTheory;
7open arithmeticTheory;
8open numpairTheory;
9open pred_setTheory;
10val _ = new_theory "turing_machine";
11
12(*
13Li and Vitayi book
14Turing mahines consist of
15    Finite program
16    Cells
17    List of cells called tape
18    Head, on one of the cells
19    Tape has left and right
20    Each cell is either 0,1 or Blank
21    Finite program can be in a finite set of states Q
22    Time, which is in the set {0,1,2,...}
23    Head is said     to 'scan' the cell it is currently over
24    At time 0 the cell the head is over is called the start cell
25    At time 0 every cell is Blank except
26        a finite congituous sequence from the strat cell to the right, containing only 0' and 1's
27    This sequence is called the input
28
29    We have two operations
30        We can write A = {0,1,B} in the cell being scanned
31        The head can shift left or right
32    There is one operation per time unit (step)
33    After each step, the program takes on a state from Q
34
35    The machine follows a set of rules
36    The rules are of the form (p,s,a,q)
37        p is the current state of the program
38        s is the symbol under scan
39        a is the next operation to be exectued, in S = {0,1,B,L,R}
40        q is the next state of the program
41    For any two rules, the first two elements must differ
42    Not every possible rule (in particular, combination of first two rules) is in the set of rules
43    This way the device can perform the 'no' operation, if this happens the device halts
44
45    We define a turing machine as a mapping from a finite subset of QxA to SxQ
46
47    We can associate a partial function to each Turing machine
48        The input to the machine is presented as an n-tuple (x1,...xn) of binary strings
49        in the form of a single binary string consisting of self-deliminating versions of xi's
50        The integer repesented by the maxiaml binary string of which some bit is scanned
51        or '0' if Blank is scanned by the time the machine halts is the output
52
53
54    This all leads to this definition
55    Each turing machine defines a partial function from n-tuples of integers into inetgers n>0
56    Such a function is called 'partially recursive' or 'computable'
57    If total then just recursive
58                           *)
59
60
61val _ = remove_termtok {term_name = "O", tok = "O"}
62
63val _ = Datatype `action = Wr0 | Wr1 | L | R`;
64
65
66val _ = Datatype `cell = Z | O `;
67
68val _ = Datatype `TM = <| state : num;
69                          prog : ((num # cell) |->  (num # action));
70                          tape_l : cell list;
71                          tape_h : cell;
72                          tape_r : cell list
73                       |>`;
74
75val concatWith_def = Define`
76  (concatWith sep [] = []) /\
77  (concatWith sep [x] = x) /\
78  (concatWith sep (x::y::rest) = x ++ sep ++ concatWith sep (y::rest))`;
79
80val INITIAL_TAPE_TM_def = Define `
81  (INITIAL_TAPE_TM tm [] = tm) ���
82  (INITIAL_TAPE_TM tm (h::t) =
83    tm with <|tape_l := [] ; tape_h := h ; tape_r := t|>)
84`;
85
86val INITIAL_TM_def = Define`
87  INITIAL_TM p args =
88    INITIAL_TAPE_TM <| state := 0;  prog := p;tape_l := [];
89                       tape_h := Z;tape_r := [] |>
90                    (concatWith [Z] (MAP (GENLIST (K O)) args))`;
91
92val UPDATE_TAPE_def = Define `
93  UPDATE_TAPE tm =
94    if (tm.state,tm.tape_h) IN FDOM tm.prog ��� tm.state <> 0 then
95      let tm' = tm with state := FST (tm.prog ' (tm.state, tm.tape_h))
96      in
97        case SND (tm.prog ' (tm.state ,tm.tape_h)) of
98          Wr0 => tm' with tape_h := Z
99        | Wr1 => tm' with tape_h := O
100        | L   => if (tm.tape_l = [])
101                 then tm' with <| tape_l := []; tape_h := Z ;
102                                  tape_r := tm.tape_h::tm.tape_r |>
103                 else tm' with <| tape_l := TL tm.tape_l;
104                                  tape_h := HD tm.tape_l ;
105                                  tape_r := tm.tape_h::tm.tape_r |>
106        | R   => if (tm.tape_r = []) then
107                  tm' with <| tape_l := tm.tape_h::tm.tape_l; tape_h := Z;
108                              tape_r := [] |>
109                 else tm' with <| tape_l := tm.tape_h::tm.tape_l;
110                                  tape_h := HD tm.tape_r;
111                                  tape_r := TL tm.tape_r |>
112    else tm with state := 0
113`;
114
115val _ = overload_on("RUN",``FUNPOW UPDATE_TAPE``);
116
117
118val DECODE_def = tDefine "DECODE" `
119  (DECODE 0 = []) ���
120  (DECODE n = if (ODD n) then [O] ++ (DECODE ((n-1) DIV 2))
121              else [Z] ++ (DECODE (n DIV 2)))`
122  (WF_REL_TAC `$<` >> rw[] >> fs[ODD_EXISTS] >>
123   `2 * m DIV 2 = m` by metis_tac[MULT_COMM, DECIDE ���0 < 2���, MULT_DIV] >>
124   simp[])
125
126val ENCODE_def = Define `
127  (ENCODE [] = 0) ���
128  (ENCODE (h::t) = case h of
129                     Z => 0 + (2 * (ENCODE t))
130                   | O => 1 + (2 * (ENCODE t))
131                   | _ => 0)`;
132
133(* Change TO simpler def of DECODE*)
134
135(* Lemmas for ENCODE/DECODE*)
136
137val ENCODE_DECODE_thm = store_thm(
138  "ENCODE_DECODE_thm",
139  ``!n. ENCODE (DECODE n) = n``,
140  completeInduct_on `n` >> Cases_on `n` >- EVAL_TAC >> rw[DECODE_def]
141  >- (rw[ENCODE_def]
142      >> `0<2` by fs[] >> `n' DIV 2 <= n'` by metis_tac[DIV_LESS_EQ]
143      >> `n' < SUC n'` by fs[] >> `n' DIV 2 < SUC n'` by fs[]
144      >> `ENCODE (DECODE (n' DIV 2)) = n' DIV 2` by fs[] >> rw[]
145      >> `~ODD n'` by metis_tac[ODD]
146      >> `EVEN n'` by metis_tac[EVEN_OR_ODD]
147      >> `n' MOD 2 =0` by metis_tac[EVEN_MOD2]
148      >> `2 * (n' DIV 2) = n'` by metis_tac[MULT_EQ_DIV]
149      >> rw[])
150  >> rw[ENCODE_def]
151  >> `EVEN (SUC n')` by metis_tac[EVEN_OR_ODD]
152  >> `(SUC n') MOD 2 =0` by metis_tac[EVEN_MOD2]
153  >> `2 * ((SUC n') DIV 2) = SUC n'` by fs[MULT_EQ_DIV]);
154
155val DECODE_EMPTY_lem = Q.store_thm (
156  "DECODE_EMPTY_lem",
157  `��� n. (DECODE n = []) ==> (n=0)`,
158  Induct_on `n` >- EVAL_TAC >> fs[] >> rw[DECODE_def]  );
159
160val ENCODE_TM_TAPE_def = Define `
161  ENCODE_TM_TAPE tm =
162       if tm.tape_h = Z then
163           (ENCODE tm.tape_l   *,   (2 * (ENCODE tm.tape_r)))
164       else
165           (ENCODE tm.tape_l   *,   (2 * (ENCODE tm.tape_r) + 1))
166`;
167
168val DECODE_TM_TAPE_def = Define `
169  DECODE_TM_TAPE n =
170       if EVEN (nsnd n) then
171           (DECODE (nfst n), Z , DECODE ( (nsnd n) DIV 2))
172       else
173           (DECODE (nfst n), O , DECODE ( (nsnd n - 1) DIV 2))`;
174
175(* Halted definition and TM examples *)
176val HALTED_def = Define `HALTED tm <=> (tm.state = 0)`;
177
178(*
179
180The set of Partial Recursive Functions is identical to the set of
181Turing Machines computable functions
182
183Total Recursive Function correspond to Turing Machine computable functions that always halt
184
185One can enumerate the Valid Turing Machines (by enumerating programs)
186
187*)
188
189val NUM_CELL_def = Define `
190  (NUM_CELL Z = 0:num) ���
191  (NUM_CELL O = 1:num) `;
192
193val CELL_NUM_def = Define `
194  (CELL_NUM 0n = Z) ���
195  (CELL_NUM 1 = O) `;
196
197val ACT_TO_NUM_def = Define `
198  (ACT_TO_NUM Wr0 = 0:num) ���
199  (ACT_TO_NUM Wr1 = 1:num) ���
200  (ACT_TO_NUM L   = 2:num) ���
201  (ACT_TO_NUM R   = 3:num) `;
202
203val NUM_TO_ACT_def = Define `
204  (NUM_TO_ACT 0n = Wr0 ) ���
205  (NUM_TO_ACT 1 = Wr1) ���
206  (NUM_TO_ACT 2 = L) ���
207  (NUM_TO_ACT 3 = R) `;
208
209val FULL_ENCODE_TM_def = Define `
210  FULL_ENCODE_TM tm = tm.state *, ENCODE_TM_TAPE tm
211`;
212
213
214val FULL_DECODE_TM_def = Define `
215  FULL_DECODE_TM n = <| state:=  nfst n;
216                        tape_l := FST (DECODE_TM_TAPE (nsnd n));
217                        tape_h := FST (SND (DECODE_TM_TAPE (nsnd n)));
218                        tape_r := SND (SND (DECODE_TM_TAPE (nsnd n)))|>
219`;
220
221(* Perform action an move to state *)
222val UPDATE_ACT_S_TM_def = Define `UPDATE_ACT_S_TM s act tm =
223           let tm' = tm with state := s
224           in
225               case act of
226                   Wr0 => tm' with tape_h := Z
227                 | Wr1 => tm' with tape_h := O
228                 | L   => if (tm.tape_l = [])
229                          then tm' with <| tape_l := [];
230                               tape_h := Z ;
231                               tape_r := tm.tape_h::tm.tape_r |>
232                          else tm' with <| tape_l := TL tm.tape_l;
233               tape_h := HD tm.tape_l ;
234               tape_r := tm.tape_h::tm.tape_r |>
235               | R   => if (tm.tape_r = [])
236                        then tm' with <| tape_l := tm.tape_h::tm.tape_l;
237                             tape_h := Z ;
238                             tape_r := [] |>
239                        else tm' with <| tape_l := tm.tape_h::tm.tape_l;
240               tape_h := HD tm.tape_r;
241               tape_r := TL tm.tape_r |>`;
242
243val ODD_DIV_2_lem = Q.store_thm ("ODD_DIV_2_lem",
244  `��� y. ODD y ==> (y DIV 2 = (y-1) DIV 2)`,
245  simp[ODD_EXISTS, PULL_EXISTS, ADD1, ADD_DIV_RWT]);
246
247val WRITE_0_HEAD_lem = Q.store_thm("WRITE_0_HEAD_lem",
248  `��� tm s. (UPDATE_ACT_S_TM s Wr0 tm).tape_h = Z`,
249  rpt strip_tac >> rw[UPDATE_ACT_S_TM_def] );
250
251
252val WRITE_1_HEAD_lem = Q.store_thm("WRITE_1_HEAD_lem",
253  `��� tm s. (UPDATE_ACT_S_TM s Wr1 tm).tape_h = O`,
254  rpt strip_tac >> rw[UPDATE_ACT_S_TM_def] );
255
256val ODD_TL_DECODE_lem = Q.store_thm ("ODD_TL_DECODE_lem",
257  `��� n. ODD n ==> (TL (DECODE n) = DECODE ((n-1) DIV 2))`,
258  rpt strip_tac >> `EVEN 0` by EVAL_TAC >> `n ��� 0` by metis_tac[EVEN_AND_ODD]>>
259  rw[DECODE_def] >> Cases_on `DECODE n` >- `n=0` by fs[DECODE_EMPTY_lem] >>
260  EVAL_TAC >> Cases_on `n` >- fs[] >> fs[DECODE_def] >> rfs[] );
261
262val EVEN_TL_DECODE_lem = Q.store_thm ("EVEN_TL_DECODE_lem",
263  `��� n. ((EVEN n) ��� (n > 0)) ==> (TL (DECODE n) = DECODE (n DIV 2))`,
264  rpt strip_tac >> Cases_on `n` >- fs[]  >>
265  rw[DECODE_def] >> metis_tac[EVEN_AND_ODD] );
266
267val ODD_MOD_TWO_lem = Q.store_thm ("ODD_MOD_TWO_lem",
268  `���n. (ODD n) ==> (n MOD 2 = 1)`,
269  rpt strip_tac  >> fs[MOD_2] >> `~EVEN n` by metis_tac[EVEN_AND_ODD] >> rw[]);
270
271val containment_lem = Q.store_thm("containment_lem",
272  `((OLEAST n. (nfst n,CELL_NUM (nsnd n)) ��� FDOM p) = NONE) <=> (p = FEMPTY)`,
273  rw[] >> eq_tac >> simp[] >> csimp[fmap_EXT] >>
274  simp[EXTENSION,pairTheory.FORALL_PROD] >> strip_tac >>
275  qx_gen_tac `a` >> qx_gen_tac `b` >>
276  `���c. b = CELL_NUM c` by metis_tac[CELL_NUM_def,theorem"cell_nchotomy"] >>
277  rw[] >>
278  pop_assum (qspec_then `a *, c` mp_tac) >> simp[]);
279
280
281val UPDATE_TAPE_ACT_STATE_TM_thm = Q.store_thm("UPDATE_TAPE_ACT_STATE_TM_thm",
282  `��� tm.
283    ((tm.state , tm.tape_h) ��� FDOM tm.prog) ��� tm.state <> 0 ==>
284    (UPDATE_ACT_S_TM (FST (tm.prog ' (tm.state, tm.tape_h)))
285                     (SND (tm.prog ' (tm.state, tm.tape_h)))
286                     tm
287       =
288     UPDATE_TAPE tm)`,
289  strip_tac >> fs[UPDATE_ACT_S_TM_def,UPDATE_TAPE_def]  );
290
291val NUM_TO_ACT_TO_NUM = Q.store_thm("NUM_TO_ACT_TO_NUM[simp]",
292  `((ACT_TO_NUM k) < 4) ==> (NUM_TO_ACT (ACT_TO_NUM k) = k)`,
293  rw[NUM_TO_ACT_def,ACT_TO_NUM_def] >>
294  `(ACT_TO_NUM k = 0) ��� (ACT_TO_NUM k = 1) ���(ACT_TO_NUM k = 2)���
295   (ACT_TO_NUM k = 3)` by simp[] >>rw[]>>
296  EVAL_TAC >> Cases_on `k` >> rfs[ACT_TO_NUM_def] >> EVAL_TAC);
297val _ = export_rewrites ["NUM_CELL_def"]
298
299val TM_PROG_P_TAPE_H = Q.store_thm("TM_PROG_P_TAPE_H[simp]",
300  `(tm with prog := p).tape_h = tm.tape_h`,
301  fs[]);
302
303val TM_PROG_P_STATE = Q.store_thm("TM_PROG_P_STATE[simp]",
304  `(tm with prog := p).state = tm.state`,
305  fs[]);
306
307val UPDATE_TM_ARB_Q = Q.store_thm("UPDATE_TM_ARB_Q",
308  `(tm.state,tm.tape_h) ��� FDOM p ��� tm.state <> 0 ==>
309   (UPDATE_ACT_S_TM (FST (p ' (tm.state,tm.tape_h)))
310                    (SND (p ' (tm.state,tm.tape_h)))
311                    (tm with prog := q) =
312    (UPDATE_TAPE (tm with prog := p)) with prog := q)`,
313  rw[UPDATE_TAPE_def,UPDATE_ACT_S_TM_def] >>
314  Cases_on `SND (p ' (tm.state,tm.tape_h))` >> simp[] )
315
316val tm_with_prog = Q.store_thm("tm_with_prog",
317  `tm with prog := tm.prog = tm`,simp[theorem("TM_component_equality")])
318
319val FST_DECODE_TM_TAPE = Q.store_thm(
320  "FST_DECODE_TM_TAPE[simp]",
321  `FST (DECODE_TM_TAPE tp) = DECODE (nfst tp)`,
322  rw[DECODE_TM_TAPE_def])
323
324val DECODE_EQ_NIL = Q.store_thm(
325  "DECODE_EQ_NIL[simp]",
326  `(DECODE n = []) ��� (n = 0)`,
327  metis_tac[DECODE_EMPTY_lem, DECODE_def]);
328
329val ODD_HD_DECODE = Q.store_thm(
330  "ODD_HD_DECODE",
331  `ODD n ==> (HD (DECODE n) = O)`,
332  Cases_on `n` >> simp[DECODE_def]);
333
334val EVEN_HD_DECODE = Q.store_thm(
335 "EVEN_HD_DECODE",
336`EVEN n ��� (n ��� 0)  ==> (HD (DECODE n) = Z)`,
337Cases_on `n` >> simp[DECODE_def] >> metis_tac[EVEN_AND_ODD,listTheory.HD]);
338
339val SND_SND_DECODE_TM_TAPE = Q.store_thm("SND_SND_DECODE_TM_TAPE",
340`SND (SND (DECODE_TM_TAPE (nsnd tmn))) = DECODE (nsnd (nsnd tmn) DIV 2)`,
341rw[DECODE_TM_TAPE_def] >> `ODD (nsnd (nsnd tmn))` by metis_tac[EVEN_OR_ODD] >>
342  rw[ODD_DIV_2_lem]);
343
344val SND_SND_DECODE_TM_TAPE_FULL = Q.store_thm(
345  "SND_SND_DECODE_TM_TAPE_FULL[simp]",
346  `SND (SND (DECODE_TM_TAPE (t))) = DECODE (nsnd ( t) DIV 2)`,
347  rw[DECODE_TM_TAPE_def] >> `ODD (nsnd (t))` by metis_tac[EVEN_OR_ODD] >>
348  rw[ODD_DIV_2_lem]);
349
350val FST_SND_DECODE_TM_TAPE_FULL = Q.store_thm(
351  "FST_SND_DECODE_TM_TAPE_FULL[simp]",
352  `ODD (nsnd (t)) ==> (FST (SND (DECODE_TM_TAPE (t))) = O)`,
353  rw[DECODE_TM_TAPE_def] >> metis_tac[EVEN_AND_ODD]);
354
355val FST_SND_DECODE_TM_TAPE_EVEN_FULL = Q.store_thm(
356  "FST_SND_DECODE_TM_TAPE_EVEN_FULL[simp]",
357  `EVEN (nsnd (t)) ==> (FST (SND (DECODE_TM_TAPE (t))) = Z)`,
358  rw[DECODE_TM_TAPE_def]);
359
360val MEMBER_CARD = Q.store_thm(
361  "MEMBER_CARD",
362  `a ��� FDOM p ��� 0 < CARD (FDOM p)`,
363  Induct_on `p` >> simp[] );
364
365val npair_lem = Q.store_thm("npair_lem",
366  `(���n. P n) <=> (���j k. P (j *, k))`,
367  eq_tac >> simp[] >>
368  rpt strip_tac >> `���j k. j *, k = n` by metis_tac[npair_cases] >> rw[] );
369
370val NUM_TO_CELL_TO_NUM = Q.store_thm("NUM_TO_CELL_TO_NUM",
371  `((c=0) ��� (c=1)) ==> (NUM_CELL (CELL_NUM c) = c)`,
372  strip_tac >> rw[NUM_CELL_def,CELL_NUM_def]);
373
374val FULL_ENCODE_TM_STATE = Q.store_thm("FULL_ENCODE_TM_STATE[simp]",
375  `nfst (FULL_ENCODE_TM tm) = tm.state`,
376  fs[FULL_ENCODE_TM_def]);
377
378val tri_mono = Q.store_thm ("tri_mono[simp]",
379  `���x y. (tri x <= tri y) <=> (x <= y)`,
380  Induct_on `y` >> simp[]  );
381
382val CELL_NUM_LEM1 = Q.store_thm("CELL_NUM_LEM1",
383  `(���n'. n' < n ��� c ��� (nfst n',CELL_NUM (nsnd n')) ��� FDOM p) ���
384   (n,CELL_NUM c) ��� FDOM p ==> (c=0) ��� (c=1)`,
385  spose_not_then strip_assume_tac >> Cases_on `CELL_NUM c`
386  >- (`0<c` by simp[] >>
387      metis_tac[nfst_npair,nsnd_npair,npair2_lt,CELL_NUM_def]) >>
388  `1<c` by simp[] >> metis_tac[nfst_npair,nsnd_npair,npair2_lt,CELL_NUM_def]);
389
390val TM_ACT_LEM_1 = Q.store_thm("TM_ACT_LEM_1[simp]",
391  `( (nsnd (nsnd (FULL_ENCODE_TM tm))) MOD 2) = NUM_CELL (tm.tape_h)`,
392  simp[FULL_ENCODE_TM_def,ENCODE_TM_TAPE_def] >> rw[] >> Cases_on `tm.tape_h` >- fs[] >- EVAL_TAC)
393
394val _ = add_rule {term_name = "FULL_ENCODE_TM",fixity = Closefix,
395                  block_style = (AroundEachPhrase,(PP.CONSISTENT,0)),
396                  paren_style = OnlyIfNecessary,
397                  pp_elements = [TOK "���",TM,TOK"���"]}
398
399val FULL_ENCODE_IGNORES_PROGS = Q.store_thm("FULL_ENCODE_IGNORES_PROGS[simp]",
400`���tm with prog := p��� = ���tm���`,
401simp[FULL_ENCODE_TM_def,ENCODE_TM_TAPE_def]);
402
403val NUM_CELL_INJ = Q.store_thm("NUM_CELL_INJ",
404`(NUM_CELL a = NUM_CELL b) <=> (a = b)`,
405eq_tac >- (Cases_on ` a` >> Cases_on `b` >> rw[] ) >- (rw[]) )
406
407val ACT_TO_NUM_LESS_4 = Q.store_thm("ACT_TO_NUM_LESS_4",
408`ACT_TO_NUM a < 4`,
409Cases_on `a` >> EVAL_TAC)
410
411val TWO_TIMES_DIV_TWO_thm = Q.store_thm("TWO_TIMES_DIV_TWO_thm[simp]",
412  `2 *  n DIV 2 = n`,
413  metis_tac[DECIDE ���0 < 2���, MULT_DIV, MULT_COMM]);
414
415val TWO_TIMES_P_ONE_DIV_TWO_thm = Q.store_thm(
416  "TWO_TIMES_P_ONE_DIV_TWO_thm[simp]",
417  `(2 * n + 1) DIV 2 = n`,
418  metis_tac[DECIDE ���1 < 2���, DIV_MULT, MULT_COMM]);
419
420val ENCODE_CONS_DECODE_ENCODE_thm = Q.store_thm(
421  "ENCODE_CONS_DECODE_ENCODE_thm[simp]",
422  `ENCODE (h::DECODE (ENCODE t)) = ENCODE (h::t)`,
423  fs[ENCODE_def,DECODE_def,ENCODE_DECODE_thm]);
424
425val NFST_ENCODE_TM_TAPE = Q.store_thm("NFST_ENCODE_TM_TAPE[simp]",
426`nfst (ENCODE_TM_TAPE tm) = ENCODE tm.tape_l`,
427rw[ENCODE_TM_TAPE_def]);
428
429val FST_SND_DECODE_TM_TAPE = Q.store_thm("FST_SND_DECODE_TM_TAPE[simp]",
430`FST (SND (DECODE_TM_TAPE (ENCODE_TM_TAPE tm))) = tm.tape_h`,
431rw[DECODE_TM_TAPE_def,ENCODE_TM_TAPE_def] >> fs[EVEN_MULT,EVEN_ADD] >>
432Cases_on `tm.tape_h` >> fs[]);
433
434val NSND_ENCODE_TM_TAPE_DIV2 = Q.store_thm("NSND_ENCODE_TM_TAPE_DIV2[simp]",
435`(nsnd (ENCODE_TM_TAPE tm) DIV 2) = ENCODE tm.tape_r`,
436rw[ENCODE_TM_TAPE_def]);
437
438val _ = export_theory();
439