1 (* Title: thys/Turing.thy

     2    Author: Jian Xu, Xingyuan Zhang, and Christian Urban

     3 *)

     4 

     5 header {* Turing Machines *}

     6 

     7 theory Turing2

     8 imports Main

     9 begin

    10 

    11 section {* Basic definitions of Turing machine *}

    12 

    13 datatype action = W0 | W1 | L | R | Nop

    14 

    15 datatype cell = Bk | Oc

    16 

    17 type_synonym tape = "cell list \<times> cell list"

    18 

    19 type_synonym state = nat

    20 

    21 type_synonym instr = "action \<times> state"

    22 

    23 type_synonym tprog = "(instr \<times> instr) list"

    24 

    25 type_synonym config = "state \<times> tape"

    26 

    27 fun nth_of where

    28   "nth_of xs i = (if i \<ge> length xs then None else Some (xs ! i))"

    29 

    30 fun 

    31   fetch :: "tprog \<Rightarrow> state \<Rightarrow> cell \<Rightarrow> instr"

    32 where

    33   "fetch tm 0 b = (Nop, 0)"

    34 | "fetch tm (Suc s) b = 

    35      (case nth_of tm s of

    36         Some i \<Rightarrow> (case b of Bk \<Rightarrow> fst i | Oc \<Rightarrow> snd i)

    37       | None \<Rightarrow> (Nop, 0))"

    38 

    39 fun 

    40   update :: "action \<Rightarrow> tape \<Rightarrow> tape"

    41 where 

    42   "update W0 (l, r) = (l, Bk # (tl r))" 

    43 | "update W1 (l, r) = (l, Oc # (tl r))"

    44 | "update L  (l, r) = (if l = [] then ([], Bk # r) else (tl l, (hd l) # r))" 

    45 | "update R  (l, r) = (if r = [] then (Bk # l, []) else ((hd r) # l, tl r))" 

    46 | "update Nop (l, r) = (l, r)"

    47 

    48 abbreviation 

    49   "read r == if (r = []) then Bk else hd r"

    50 

    51 fun step :: "config \<Rightarrow> tprog \<Rightarrow> config"

    52   where 

    53   "step (s, l, r) p = 

    54      (let (a, s') = fetch p s (read r) in (s', update a (l, r)))"

    55 

    56 fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config"

    57   where

    58   "steps cf p 0 = cf" |

    59   "steps cf p (Suc n) = steps (step cf p) p n"

    60 

    61 fun

    62   is_final :: "config \<Rightarrow> bool"

    63 where

    64   "is_final cf = (fst cf = 0)"

    65 

    66 

    67 (* well-formedness of Turing machine programs *)

    68 

    69 fun 

    70   tm_wf :: "tprog \<Rightarrow> bool"

    71 where

    72   "tm_wf p = (1 \<le> length p \<and> (\<forall>((_, s1), (_, s2)) \<in> set p. s1 \<le> length p \<and> s2 \<le> length p))"

    73 

    74 (* short-hand notation for tapes *)

    75 

    76 abbreviation cell_replicate :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100)

    77   where "x \<up> n \<equiv> replicate n x"

    78 

    79 class tape_of =

    80   fixes tape_of :: "'a \<Rightarrow> cell list" ("<_>" [64] 67)

    81 

    82 instantiation nat :: tape_of 

    83 begin

    84 

    85 fun tape_of_nat where 

    86   "<(n::nat)> = Oc \<up> (Suc n)"

    87 

    88 instance ..

    89 

    90 end

    91 

    92 instantiation list :: (tape_of) tape_of 

    93 begin

    94 

    95 fun tape_of_list :: "'a list \<Rightarrow> cell list" 

    96   where 

    97   "<[]> = []" |

    98   "<[n]> = <n>" |

    99   "<n # ns> = <n> @ [Bk] @ <ns>"

   100 

   101 instance ..

   102 

   103 end

   104 

   105 instantiation prod :: (tape_of, tape_of) tape_of 

   106 begin

   107 

   108 fun tape_of_prod :: "'a \<times> 'b \<Rightarrow> cell list" 

   109   where 

   110   "<(n, m)> = <n> @ [Bk] @ <m>" 

   111 

   112 instance ..

   113 

   114 end

   115 

   116 definition 

   117   "std_tape tp \<equiv> \<exists>k l (n::nat). tp = (Bk \<up> k, <n> @ Bk \<up> l)"

   118 

   119 

   120 end

   121