--- a/thys/turing_basic.thy	Sun Jan 13 09:57:28 2013 +0000
+++ b/thys/turing_basic.thy	Sun Jan 13 11:29:33 2013 +0000
@@ -121,6 +121,11 @@
 where
   "is_final (s, l, r) = (s = 0)"
 
+lemma is_final_steps:
+  assumes "is_final (s, l, r)"
+  shows "is_final (steps (s, l, r) p n)"
+using assms by (induct n) (auto)
+
 fun 
   holds_for :: "(tape \<Rightarrow> bool) \<Rightarrow> config \<Rightarrow> bool" ("_ holds'_for _" [100, 99] 100)
 where
@@ -134,12 +139,32 @@
   shows "steps (0, (l, r)) p n = (0, (l, r))"
 by (induct n) (simp_all)
 
+lemma is_final_holds[simp]:
+  assumes "is_final c"
+  shows "Q holds_for (steps c p n) = Q holds_for c"
+using assms 
+apply(induct n)
+apply(case_tac [!] c)
+apply(auto)
+done
+
 type_synonym assert = "tape \<Rightarrow> bool"
 
 definition assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100)
   where
   "assert_imp P Q = (\<forall>l r. P (l, r) \<longrightarrow> Q (l, r))"
 
+lemma test:
+  assumes "is_final (steps (1, (l, r)) p n1)"
+  and     "is_final (steps (1, (l, r)) p n2)"
+  shows "Q holds_for (steps (1, (l, r)) p n1) \<longleftrightarrow> Q holds_for (steps (1, (l, r)) p n2)"
+proof -
+  obtain n3 where "n1 = n2 + n3 \<or> n2 = n1 + n3"
+    by (metis le_iff_add nat_le_linear)
+  with assms show "Q holds_for (steps (1, (l, r)) p n1) \<longleftrightarrow> Q holds_for (steps (1, (l, r)) p n2)"  
+    by auto
+qed
+
 definition
   Hoare :: "assert \<Rightarrow> tprog \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)
 where
@@ -151,11 +176,6 @@
   shows "{P} p {Q}"
 unfolding Hoare_def using assms by auto
 
-lemma HoareI2:
-  assumes "\<And>l r n. P (l, r) \<and> is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)"
-  shows "{P} p {Q}"
-unfolding Hoare_def using assms by auto
-
 text {*
 {P1} A {Q1}   {P2} B {Q2}  Q1 \<mapsto> P2
 -----------------------------------
@@ -173,10 +193,10 @@
 proof(rule HoareI)
   fix a b
   assume h: "P1 (a, b)"
-  hence "\<exists>n. let (s, tp') = steps (Suc 0, a, b) A n in s = 0 \<and> Q1 tp'"
-    using A_halt unfolding hoare_def by simp
-  from this obtain stp1 where "let (s, tp') = steps (Suc 0, a, b) A stp1 in s = 0 \<and> Q1 tp'" ..
-  then show "\<exists>n. case steps (Suc 0, a, b) (A |+| B) n of (s, tp') \<Rightarrow> s = 0 \<and> Q2 tp'"
+  then have "\<exists>n. is_final (steps (1, a, b) A n) \<and> Q1 holds_for (steps (1, a, b) A n)"
+    using A_halt unfolding Hoare_def by simp
+  then obtain n1 where "is_final (steps (1, a, b) A n1) \<and> Q1 holds_for (steps (1, a, b) A stp1)" ..
+  then show "\<exists>n. is_final (steps (1, a, b) (A |+| B) n) \<and> Q2 holds_for (steps (1, a, b) (A |+| B) n)"
   proof(case_tac "steps (Suc 0, a, b) A stp1", simp, erule_tac conjE)
     fix aa ba c
     assume g1: "Q1 (ba, c)" 
@@ -184,9 +204,10 @@
     hence "P2 (ba, c)"
       using aimpb apply(simp add: assert_imp_def)
       done
-    hence "\<exists> stp. let (s, tp') = steps (Suc 0, ba, c) B stp in s = 0 \<and> Q2 tp'"
-      using B_halt unfolding hoare_def by simp
-    from this obtain stp2 where "let (s, tp') = steps (Suc 0, ba, c) B stp2 in s = 0 \<and> Q2 tp'" ..
+    hence "\<exists> stp. is_final (steps (Suc 0, ba, c) B stp) \<and> Q2 holds_for (steps (Suc 0, ba, c) B stp)"
+      using B_halt unfolding Hoare_def by simp
+    from this obtain stp2 where 
+      "is_final (steps (Suc 0, ba, c) B stp2) \<and> Q2 holds_for (steps (Suc 0, ba, c) B stp2)" ..
     thus "?thesis"
     proof(case_tac "steps (Suc 0, ba, c) B stp2", simp, erule_tac conjE)
       fix aa bb ca
@@ -205,7 +226,7 @@
   qed
 qed
 
-lemma hoare_plus: 
+lemma Hoare_plus2: 
   assumes A_wf : "tm_wf A"
   and B_wf : "tm_wf B"
   and A_halt : "{P1} A {Q1}"