diff -r eb589fa73fc1 -r 2e9881578cb2 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Fri Jan 25 15:57:58 2013 +0100
+++ b/thys/uncomputable.thy	Fri Jan 25 21:15:09 2013 +0000
@@ -64,24 +64,23 @@
   inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
   inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-  "inv_init0 x (l, r) = ((x > 1 \<and> l = Oc \<up> (x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>   
-                         (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"
-| "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)"
-| "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)"
-| "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])"
-| "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))"
+  "inv_init0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>   
+                         (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"
+| "inv_init1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
+| "inv_init2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
+| "inv_init3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
+| "inv_init4 n (l, r) = (n > 0 \<and> ((l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc])))"
 
 fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
   where
-  "inv_init x (s, l, r) = 
-        (if s = 0 then inv_init0 x (l, r) 
-         else if s = 1 then inv_init1 x (l, r)
-         else if s = 2 then inv_init2 x (l, r)
-         else if s = 3 then inv_init3 x (l, r)
-         else if s = 4 then inv_init4 x (l, r)
+  "inv_init n (s, l, r) = 
+        (if s = 0 then inv_init0 n (l, r) else
+         if s = 1 then inv_init1 n (l, r) else
+         if s = 2 then inv_init2 n (l, r) else
+         if s = 3 then inv_init3 n (l, r) else
+         if s = 4 then inv_init4 n (l, r) 
          else False)"
 
-declare inv_init.simps[simp del]
 
 
 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 
@@ -109,20 +108,19 @@
 
 fun init_state :: "config \<Rightarrow> nat"
   where
-  "init_state (s, l, r) = (if s = 0 then 0
-                             else 5 - s)"
+  "init_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
 
 fun init_step :: "config \<Rightarrow> nat"
   where
-  "init_step (s, l, r) = (if s = 2 then length r
-                            else if s = 3 then if r = [] \<or> r = [Bk] then Suc 0 else 0
-                            else if s = 4 then length l
-                            else 0)"
+  "init_step (s, l, r) = 
+        (if s = 2 then length r else
+         if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else
+         if s = 4 then length l 
+         else 0)"
 
 fun init_measure :: "config \<Rightarrow> nat \<times> nat"
   where
-  "init_measure c = 
-   (init_state c, init_step c)"
+  "init_measure c = (init_state c, init_step c)"
 
 
 definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
@@ -131,11 +129,11 @@
 
 definition init_LE :: "(config \<times> config) set"
   where
-   "init_LE \<equiv> (inv_image lex_pair init_measure)"
+  "init_LE \<equiv> (inv_image lex_pair init_measure)"
 
 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
-apply(case_tac r, auto, case_tac a, auto)
-done
+by (case_tac r, auto, case_tac a, auto)
+
 
 lemma wf_init_le: "wf init_LE"
 by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)
@@ -164,11 +162,10 @@
     ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n), 
       steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"
       using a 
-    proof(simp)
+    proof(simp del: inv_init.simps)
       assume "inv_init x (s, l, r)" "0 < s"
       thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE"
-        apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral 
-          split: if_splits)
+        apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_init_def numeral split: if_splits)
         apply(case_tac r, auto, case_tac a, auto)
         done
     qed
@@ -199,48 +196,31 @@
 
 (* tcopy_loop *)
 
-fun inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop1_loop x (l, r) = 
-       (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)"
-
-fun inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop1_exit x (l, r) = 
-      (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
-
-fun inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
-
-fun inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop2 x (l, r) = 
-       (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)"
-
-fun inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop3 x (l, r) = 
-         (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)"
-
-fun inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop4 x (l, r) = 
-           (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)"
-
-fun inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+fun 
+  inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-  "inv_loop5_loop x (l, r) = 
-          (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)"
-
-fun inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop5_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and>  l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)"
-
-fun inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> 
-                         inv_loop5_exit x (l, r))"
+  "inv_loop0 x (l, r) =  (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
+| "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)"
+| "inv_loop1_exit x (l, r) = (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0)"
+| "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
+| "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)"
+| "inv_loop3 x (l, r) = 
+     (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)"
+| "inv_loop4 x (l, r) = 
+     (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)"
+| "inv_loop5_loop x (l, r) = 
+     (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)"
+| "inv_loop5_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and>  l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)"
+| "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"
 
 fun inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
@@ -256,11 +236,6 @@
   where
   "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
 
-fun inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_loop0 x (l, r) = 
-      (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
-
 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
   where
   "inv_loop x (s, l, r) = 
@@ -277,21 +252,20 @@
         inv_loop2.simps[simp del] inv_loop3.simps[simp del] 
         inv_loop4.simps[simp del] inv_loop5.simps[simp del] 
         inv_loop6.simps[simp del]
+
 lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
-apply(case_tac t, auto)
-done
-
+by (case_tac t, auto)
 
 lemma [simp]: "inv_loop1 x (b, []) = False"
 by(simp add: inv_loop1.simps)
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
-apply(auto simp: inv_loop2.simps inv_loop3.simps)
-done
+by (auto simp: inv_loop2.simps inv_loop3.simps)
+
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
-apply(auto simp: inv_loop3.simps)
-done
+by (auto simp: inv_loop3.simps)
+
 
 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
 apply(auto simp: inv_loop4.simps inv_loop5.simps)
@@ -1070,10 +1044,10 @@
 
 (* invariants of dither *)
 abbreviation
-  "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc, Oc]"
+  "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
 
 abbreviation
-  "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc]"
+  "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
 
 lemma dither_loops_aux: 
   "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> 
@@ -1330,9 +1304,9 @@
   shows "False"
 proof -
   (* invariants *)
-  def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
-  def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
-  def P3 \<equiv> "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+  def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)"
+  def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)"
+  def P3 \<equiv> "\<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
 
   (*
   {P1} tcopy {P2}  {P2} H {P3} 
@@ -1349,12 +1323,12 @@
   proof (cases rule: Hoare_plus_halt_simple)
     case A_halt (* of tcopy *)
     show "{P1} tcopy {P2}" unfolding P1_def P2_def
-      by (rule tcopy_correct2)
+      by (simp) (rule tcopy_correct2)
   next
     case B_halt (* of H *)
     show "{P2} H {P3}"
       unfolding P2_def P3_def
-      using assms by (rule H_halt_inv)
+      using assms by (simp) (rule H_halt_inv)
   qed (simp)
 
   (* {P3} dither {P3} *)
@@ -1384,9 +1358,9 @@
   shows "False"
 proof - 
   (* invariants *)
-  def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
-  def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
-  def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
+  def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)"
+  def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)"
+  def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
 
   (*
   {P1} tcopy {P2}  {P2} H {P3} 
@@ -1403,12 +1377,12 @@
   proof (cases rule: Hoare_plus_halt_simple)
     case A_halt (* of tcopy *)
     show "{P1} tcopy {P2}" unfolding P1_def P2_def
-      by (rule tcopy_correct2)
+      by (simp) (rule tcopy_correct2)
   next
     case B_halt (* of H *)
     then show "{P2} H {P3}"
       unfolding P2_def P3_def
-      using assms by (rule H_unhalt_inv)
+      using assms by (simp) (rule H_unhalt_inv)
   qed (simp)
 
   (* {P3} dither loops *)