--- a/thys/turing_hoare.thy	Wed Jan 23 08:01:35 2013 +0100
+++ b/thys/turing_hoare.thy	Wed Jan 23 12:25:24 2013 +0100
@@ -35,7 +35,7 @@
 unfolding Hoare_def 
 using assms by auto
 
-lemma Hoare_unhalt_I:
+lemma Hoare_unhaltI:
   assumes "\<And>l r n. P (l, r) \<Longrightarrow> \<not> is_final (steps0 (1, (l, r)) p n)"
   shows "{P} p \<up>"
 unfolding Hoare_unhalt_def 
@@ -92,6 +92,15 @@
     using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp)
 qed
 
+lemma Hoare_plus_halt_simple [case_names A_halt B_halt A_wf]: 
+  assumes A_halt : "{P1} A {P2}"
+  and B_halt : "{P2} B {P3}"
+  and A_wf : "tm_wf (A, 0)"
+  shows "{P1} A |+| B {P3}"
+by (rule Hoare_plus_halt[OF A_halt B_halt _ A_wf])
+   (simp add: assert_imp_def)
+
+
 
 text {*
   {P1} A {Q1}   {P2} B loops    Q1 \<mapsto> P2   A well-formed
@@ -99,16 +108,13 @@
           {P1} A |+| B  loops
 *}
 
-
-
-
 lemma Hoare_plus_unhalt:
   assumes A_halt: "{P1} A {Q1}"
   and B_uhalt: "{P2} B \<up>"
   and a_imp: "Q1 \<mapsto> P2"
   and A_wf : "tm_wf (A, 0)"
   shows "{P1} (A |+| B) \<up>"
-proof(rule_tac Hoare_unhalt_I)
+proof(rule_tac Hoare_unhaltI)
   fix n l r 
   assume h: "P1 (l, r)"
   then obtain n1 l' r'
@@ -145,6 +151,15 @@
   qed
 qed
 
+lemma Hoare_plus_unhalt_simple [case_names A_halt B_unhalt A_wf]: 
+ assumes A_halt: "{P1} A {P2}"
+  and B_uhalt: "{P2} B \<up>"
+  and A_wf : "tm_wf (A, 0)"
+  shows "{P1} (A |+| B) \<up>"
+by (rule Hoare_plus_unhalt[OF A_halt B_uhalt _ A_wf])
+   (simp add: assert_imp_def)
+
+
 lemma Hoare_weak:
   assumes a: "{P} p {Q}"
   and b: "P' \<mapsto> P"