--- a/thys/turing_hoare.thy	Sat Jan 19 14:44:07 2013 +0000
+++ b/thys/turing_hoare.thy	Sat Jan 19 15:27:21 2013 +0000
@@ -2,8 +2,6 @@
 imports turing_basic
 begin
 
-
-
 type_synonym assert = "tape \<Rightarrow> bool"
 
 definition 
@@ -11,8 +9,6 @@
 where
   "P \<mapsto> Q \<equiv> \<forall>l r. P (l, r) \<longrightarrow> Q (l, r)"
 
-
-
 fun 
   holds_for :: "(tape \<Rightarrow> bool) \<Rightarrow> config \<Rightarrow> bool" ("_ holds'_for _" [100, 99] 100)
 where
@@ -48,8 +44,8 @@
 
 
 text {*
-  {P1} A {Q1}   {P2} B {Q2}  Q1 \<mapsto> P2
-  -----------------------------------
+  {P1} A {Q1}   {P2} B {Q2}  Q1 \<mapsto> P2   A, B well-formed
+  ------------------------------------------------------
   {P1} A |+| B {Q2}
 *}
 
@@ -79,12 +75,12 @@
     where "is_final (steps0 (1, l', r') B n2)" and "Q2 holds_for (steps0 (1, l', r') B n2)"
     using B_halt unfolding Hoare_def by auto
   then obtain l'' r'' where "steps0 (1, l', r') B n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')"
-    by (case_tac "steps0 (1, l', r') B n2", auto)
+    by (case_tac "steps0 (1, l', r') B n2") (auto)
   then have "steps0 (Suc (length A div 2), l', r')  (A |+| B) n2 = (0, l'', r'')"
     by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf)
   ultimately show 
     "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps0 (1, l, r) (A |+| B) n)"
-    using g
+    using g 
     apply(rule_tac x = "stpa + n2" in exI)
     apply(simp add: steps_add)
     done
@@ -93,8 +89,7 @@
 definition
   Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_))" 50)
 where
-  "{P} p \<equiv> 
-     (\<forall>l r. P (l, r) \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, (l, r)) p n))))"
+  "{P} p \<equiv> (\<forall>l r. P (l, r) \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, (l, r)) p n))))"
 
 lemma Hoare_unhalt_I:
   assumes "\<And>l r. P (l, r) \<Longrightarrow> \<forall> n. \<not> is_final (steps0 (1, (l, r)) p n)"