--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Turing2.thy	Wed May 22 13:50:20 2013 +0100
@@ -0,0 +1,121 @@
+(* Title: thys/Turing.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+*)
+
+header {* Turing Machines *}
+
+theory Turing2
+imports Main
+begin
+
+section {* Basic definitions of Turing machine *}
+
+datatype action = W0 | W1 | L | R | Nop
+
+datatype cell = Bk | Oc
+
+type_synonym tape = "cell list \<times> cell list"
+
+type_synonym state = nat
+
+type_synonym instr = "action \<times> state"
+
+type_synonym tprog = "(instr \<times> instr) list"
+
+type_synonym config = "state \<times> tape"
+
+fun nth_of where
+  "nth_of xs i = (if i \<ge> length xs then None else Some (xs ! i))"
+
+fun 
+  fetch :: "tprog \<Rightarrow> state \<Rightarrow> cell \<Rightarrow> instr"
+where
+  "fetch tm 0 b = (Nop, 0)"
+| "fetch tm (Suc s) b = 
+     (case nth_of tm s of
+        Some i \<Rightarrow> (case b of Bk \<Rightarrow> fst i | Oc \<Rightarrow> snd i)
+      | None \<Rightarrow> (Nop, 0))"
+
+fun 
+  update :: "action \<Rightarrow> tape \<Rightarrow> tape"
+where 
+  "update W0 (l, r) = (l, Bk # (tl r))" 
+| "update W1 (l, r) = (l, Oc # (tl r))"
+| "update L  (l, r) = (if l = [] then ([], Bk # r) else (tl l, (hd l) # r))" 
+| "update R  (l, r) = (if r = [] then (Bk # l, []) else ((hd r) # l, tl r))" 
+| "update Nop (l, r) = (l, r)"
+
+abbreviation 
+  "read r == if (r = []) then Bk else hd r"
+
+fun step :: "config \<Rightarrow> tprog \<Rightarrow> config"
+  where 
+  "step (s, l, r) p = 
+     (let (a, s') = fetch p s (read r) in (s', update a (l, r)))"
+
+fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config"
+  where
+  "steps cf p 0 = cf" |
+  "steps cf p (Suc n) = steps (step cf p) p n"
+
+fun
+  is_final :: "config \<Rightarrow> bool"
+where
+  "is_final cf = (fst cf = 0)"
+
+
+(* well-formedness of Turing machine programs *)
+
+fun 
+  tm_wf :: "tprog \<Rightarrow> bool"
+where
+  "tm_wf p = (1 \<le> length p \<and> (\<forall>((_, s1), (_, s2)) \<in> set p. s1 \<le> length p \<and> s2 \<le> length p))"
+
+(* short-hand notation for tapes *)
+
+abbreviation cell_replicate :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100)
+  where "x \<up> n \<equiv> replicate n x"
+
+class tape_of =
+  fixes tape_of :: "'a \<Rightarrow> cell list" ("<_>" [64] 67)
+
+instantiation nat :: tape_of 
+begin
+
+fun tape_of_nat where 
+  "<(n::nat)> = Oc \<up> (Suc n)"
+
+instance ..
+
+end
+
+instantiation list :: (tape_of) tape_of 
+begin
+
+fun tape_of_list :: "'a list \<Rightarrow> cell list" 
+  where 
+  "<[]> = []" |
+  "<[n]> = <n>" |
+  "<n # ns> = <n> @ [Bk] @ <ns>"
+
+instance ..
+
+end
+
+instantiation prod :: (tape_of, tape_of) tape_of 
+begin
+
+fun tape_of_prod :: "'a \<times> 'b \<Rightarrow> cell list" 
+  where 
+  "<(n, m)> = <n> @ [Bk] @ <m>" 
+
+instance ..
+
+end
+
+definition 
+  "std_tape tp \<equiv> \<exists>k l (n::nat). tp = (Bk \<up> k, <n> @ Bk \<up> l)"
+
+
+end
+