--- a/thys/turing_hoare.thy	Wed Jan 23 20:18:40 2013 +0100
+++ b/thys/turing_hoare.thy	Thu Jan 24 00:20:26 2013 +0100
@@ -15,32 +15,6 @@
 where
   "P holds_for (s, l, r) = P (l, r)"  
 
-(* halting case *)
-definition
-  Hoare :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" [50, 49] 50)
-where
-  "{P} p {Q} \<equiv> 
-     (\<forall>tp. P tp \<longrightarrow> (\<exists>n. is_final (steps0 (1, tp) p n) \<and> Q holds_for (steps0 (1, tp) p n)))"
-
-(* not halting case *)
-definition
-  Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" [50, 49] 50)
-where
-  "{P} p \<up> \<equiv> (\<forall>tp. P tp \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, tp) p n))))"
-
-
-lemma HoareI:
-  assumes "\<And>l r. P (l, r) \<Longrightarrow> \<exists>n. is_final (steps0 (1, (l, r)) p n) \<and> Q holds_for (steps0 (1, (l, r)) p n)"
-  shows "{P} p {Q}"
-unfolding Hoare_def 
-using assms by auto
-
-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 
-using assms by auto
-
 lemma is_final_holds[simp]:
   assumes "is_final c"
   shows "Q holds_for (steps c p n) = Q holds_for c"
@@ -51,6 +25,35 @@
 apply(auto)
 done
 
+(* Hoare Rules *)
+
+(* halting case *)
+definition
+  Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" [50, 49] 50)
+where
+  "{P} p {Q} \<equiv> \<forall>tp. P tp \<longrightarrow> (\<exists>n. is_final (steps0 (1, tp) p n) \<and> Q holds_for (steps0 (1, tp) p n))"
+
+(* not halting case *)
+definition
+  Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" [50, 49] 50)
+where
+  "{P} p \<up> \<equiv> \<forall>tp. P tp \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, tp) p n)))"
+
+
+lemma Hoare_haltI:
+  assumes "\<And>l r. P (l, r) \<Longrightarrow> \<exists>n. is_final (steps0 (1, (l, r)) p n) \<and> Q holds_for (steps0 (1, (l, r)) p n)"
+  shows "{P} p {Q}"
+unfolding Hoare_halt_def 
+using assms by auto
+
+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 
+using assms by auto
+
+
+
 
 text {*
   {P1} A {Q1}   {P2} B {Q2}  Q1 \<mapsto> P2   A well-formed
@@ -59,20 +62,20 @@
 *}
 
 
-lemma Hoare_plus_halt: 
+lemma Hoare_plus_halt [case_names A_halt B_halt Imp A_wf]: 
   assumes A_halt : "{P1} A {Q1}"
   and B_halt : "{P2} B {Q2}"
   and a_imp: "Q1 \<mapsto> P2"
   and A_wf : "tm_wf (A, 0)"
   shows "{P1} A |+| B {Q2}"
-proof(rule HoareI)
+proof(rule Hoare_haltI)
   fix l r
   assume h: "P1 (l, r)"
   then obtain n1 l' r' 
     where "is_final (steps0 (1, l, r) A n1)"  
       and a1: "Q1 holds_for (steps0 (1, l, r) A n1)"
       and a2: "steps0 (1, l, r) A n1 = (0, l', r')"
-    using A_halt unfolding Hoare_def
+    using A_halt unfolding Hoare_halt_def
     by (metis is_final_eq surj_pair) 
   then obtain n2 
     where "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')"
@@ -83,10 +86,10 @@
     where "is_final (steps0 (1, l', r') B n3)" 
     and b1: "Q2 holds_for (steps0 (1, l', r') B n3)"
     and b2: "steps0 (1, l', r') B n3 = (0, l'', r'')"
-    using B_halt unfolding Hoare_def 
+    using B_halt unfolding Hoare_halt_def 
     by (metis is_final_eq surj_pair) 
   then have "steps0 (Suc (length A div 2), l', r')  (A |+| B) n3 = (0, l'', r'')"
-    using A_wf by (rule_tac t_merge_second_halt_same) 
+    using A_wf by (rule_tac tm_comp_second_halt_same) 
   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 b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp)
@@ -108,7 +111,7 @@
           {P1} A |+| B  loops
 *}
 
-lemma Hoare_plus_unhalt:
+lemma Hoare_plus_unhalt [case_names A_halt B_unhalt Imp A_wf]:
   assumes A_halt: "{P1} A {Q1}"
   and B_uhalt: "{P2} B \<up>"
   and a_imp: "Q1 \<mapsto> P2"
@@ -121,7 +124,7 @@
     where a: "is_final (steps0 (1, l, r) A n1)" 
     and b: "Q1 holds_for (steps0 (1, l, r) A n1)"
     and c: "steps0 (1, l, r) A n1 = (0, l', r')"
-    using A_halt unfolding Hoare_def 
+    using A_halt unfolding Hoare_halt_def 
     by (metis is_final_eq surj_pair) 
   then obtain n2 where eq: "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')"
     using A_wf by (rule_tac tm_comp_pre_halt_same)
@@ -136,7 +139,7 @@
       where "steps0 (Suc 0, l', r') B (n - n2) = (s'', l'', r'')" 
       and "\<not> is_final (s'', l'', r'')" by (metis surj_pair)
     then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')"
-      using A_wf by (auto dest: t_merge_second_same simp del: tm_wf.simps)
+      using A_wf by (auto dest: tm_comp_second_same simp del: tm_wf.simps)
     then have "\<not> is_final (steps0 (1, l, r) (A |+| B) (n2 + (n  - n2)))"
       using A_wf by (simp only: steps_add eq) (simp add: tm_wf.simps)
     then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" 
@@ -160,13 +163,13 @@
    (simp add: assert_imp_def)
 
 
-lemma Hoare_weak:
+lemma Hoare_weaken:
   assumes a: "{P} p {Q}"
   and b: "P' \<mapsto> P" 
   and c: "Q \<mapsto> Q'"
   shows "{P'} p {Q'}"
 using assms
-unfolding Hoare_def assert_imp_def
+unfolding Hoare_halt_def assert_imp_def
 by (metis holds_for.simps surj_pair)