--- a/thys/Turing2.thy	Tue May 21 13:50:15 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(* 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 p 0 b = (Nop, 0)"
-| "fetch p (Suc s) b = 
-     (case nth_of p 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 c p 0 = c" |
-  "steps c p (Suc n) = steps (step c p) p n"
-
-(* well-formedness of Turing machine programs *)
-
-fun 
-  tm_wf :: "tprog \<Rightarrow> bool"
-where
-  "tm_wf p = (length p \<ge> 1 \<and> (\<forall>((_, s1), (_, s2)) \<in> set p. s1 \<le> length p \<and> s2 \<le> length p))"
-
-end
-