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