--- a/thys/Turing.thy	Wed Jan 14 09:08:51 2015 +0000
+++ b/thys/Turing.thy	Wed Dec 19 16:10:58 2018 +0100
@@ -2,7 +2,7 @@
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 *)
 
-header {* Turing Machines *}
+chapter {* Turing Machines *}
 
 theory Turing
 imports Main
@@ -216,25 +216,33 @@
 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100)
   where "x \<up> n == replicate n x"
 
-consts tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100)
-
-defs (overloaded)
-  tape_of_nat_abv: "<(n::nat)> \<equiv> Oc \<up> (Suc n)"
-
-fun tape_of_nat_list :: "'a list \<Rightarrow> cell list" 
-  where 
-  "tape_of_nat_list [] = []" |
-  "tape_of_nat_list [n] = <n>" |
-  "tape_of_nat_list (n#ns) = <n> @ Bk # (tape_of_nat_list ns)"
-
-fun tape_of_nat_pair :: "'a \<times> 'b \<Rightarrow> cell list" 
-  where 
-  "tape_of_nat_pair (n, m) = <n> @ [Bk] @ <m>" 
+class tape =
+  fixes tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100)
 
 
-defs (overloaded)
-  tape_of_nl_abv: "<(ns::'a list)> \<equiv> tape_of_nat_list ns"
-  tape_of_nat_pair: "<(np::'a\<times>'b)> \<equiv> tape_of_nat_pair np"
+instantiation nat::tape begin
+  definition tape_of_nat where "tape_of_nat (n::nat) \<equiv> Oc \<up> (Suc n)"
+  instance by standard
+end
+
+type_synonym nat_list = "nat list"
+
+instantiation list::(tape) tape begin
+  fun tape_of_nat_list :: "('a::tape) list \<Rightarrow> cell list" 
+    where 
+    "tape_of_nat_list [] = []" |
+    "tape_of_nat_list [n] = <n>" |
+    "tape_of_nat_list (n#ns) = <n> @ Bk # (tape_of_nat_list ns)"
+  definition tape_of_list where "tape_of_list \<equiv> tape_of_nat_list"
+  instance by standard
+end
+
+instantiation prod:: (tape, tape) tape begin
+  fun tape_of_nat_prod :: "('a::tape) \<times> ('b::tape) \<Rightarrow> cell list" 
+    where "tape_of_nat_prod (n, m) = <n> @ [Bk] @ <m>" 
+  definition tape_of_prod where "tape_of_prod \<equiv> tape_of_nat_prod"
+  instance by standard
+end
 
 fun 
   shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"
@@ -270,7 +278,7 @@
 
 lemma tm_comp_wf[intro]: 
   "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
-by (auto)
+by (fastforce)
 
 lemma tm_comp_step: 
   assumes unfinal: "\<not> is_final (step0 c A)"
@@ -333,9 +341,8 @@
 apply(auto simp del: tm_comp.simps)
 apply(case_tac "fetch A a Bk")
 apply(simp del: tm_comp.simps)
-apply(subst tm_comp_fetch_in_A)
-apply(auto)[4]
-apply(case_tac "fetch A a (hd c)")
+apply(subst tm_comp_fetch_in_A;force)
+apply(case_tac "fetch A a (hd ca)")
 apply(simp del: tm_comp.simps)
 apply(subst tm_comp_fetch_in_A)
 apply(auto)[4]
@@ -348,9 +355,9 @@
 using h1 h2
 apply(case_tac c)
 apply(case_tac a)
-apply(auto simp add: prod_case_unfold Let_def)
-apply(case_tac "hd c")
-apply(auto simp add: prod_case_unfold)
+apply(auto simp add: Let_def case_prod_beta')
+apply(case_tac "hd ca")
+apply(auto simp add: case_prod_beta')
 done
 
 lemma steps_in_range: