diff -r 25b1633a278d -r e7d845acb0a7 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Sat Jan 19 12:46:28 2013 +0000
+++ b/thys/uncomputable.thy	Sat Jan 19 14:29:56 2013 +0000
@@ -146,8 +146,7 @@
 qed
     
 lemma init_correct: 
-  "x > 0 \<Longrightarrow> 
-  {inv_init1 x} (tcopy_init, 0) {inv_init0 x}"
+  "x > 0 \<Longrightarrow> {inv_init1 x} tcopy_init {inv_init0 x}"
 proof(rule_tac HoareI)
   fix l r
   assume h: "0 < x"
@@ -661,8 +660,7 @@
 qed
 
 lemma loop_correct:
-  "x > 0 \<Longrightarrow> 
-      {inv_loop1 x} (tcopy_loop, 0) {inv_loop0 x}"
+  "x > 0 \<Longrightarrow> {inv_loop1 x} tcopy_loop {inv_loop0 x}"
 proof(rule_tac HoareI)
   fix l r
   assume h: "0 < x"
@@ -950,8 +948,7 @@
 qed
 
 lemma end_correct:
-  "x > 0 \<Longrightarrow> 
-      {inv_end1 x} (tcopy_end, 0) {inv_end0 x}"
+  "x > 0 \<Longrightarrow> {inv_end1 x} tcopy_end {inv_end0 x}"
 proof(rule_tac HoareI)
   fix l r
   assume h: "0 < x"
@@ -992,7 +989,7 @@
 done
 
 lemma tcopy_correct1: 
-  "\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} (tcopy, 0) {inv_end0 x}"
+  "\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} tcopy {inv_end0 x}"
 proof(simp add: tcopy_def, rule_tac Hoare_plus_halt)
   show "inv_loop0 x \<mapsto> inv_end1 x"
     by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)
@@ -1002,7 +999,7 @@
   show "tm_wf (tcopy_end, 0)" by auto
 next
   assume "0 < x"
-  thus "{inv_init1 x} (tcopy_init |+| tcopy_loop, 0) {inv_loop0 x}"
+  thus "{inv_init1 x} (tcopy_init |+| tcopy_loop) {inv_loop0 x}"
   proof(rule_tac Hoare_plus_halt)
     show "inv_init0 x \<mapsto> inv_loop1 x"
       apply(auto simp: inv_init0.simps inv_loop1.simps assert_imp_def)
@@ -1014,16 +1011,16 @@
     show "tm_wf (tcopy_loop, 0)" by auto
   next
     assume "0 < x"
-    thus "{inv_init1 x} (tcopy_init, 0) {inv_init0 x}"
+    thus "{inv_init1 x} tcopy_init {inv_init0 x}"
       by(erule_tac init_correct)
   next
     assume "0 < x"
-    thus "{inv_loop1 x} (tcopy_loop, 0) {inv_loop0 x}"
+    thus "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
       by(erule_tac loop_correct)
   qed
 next
   assume "0 < x"
-  thus "{inv_end1 x} (tcopy_end, 0) {inv_end0 x}"
+  thus "{inv_end1 x} tcopy_end {inv_end0 x}"
     by(erule_tac end_correct)
 qed
 
@@ -1147,32 +1144,14 @@
 done
 
 lemma Hoare_weak:
-  "\<lbrakk>{P} (p, off) {Q}; P'\<mapsto>P; Q\<mapsto>Q'\<rbrakk> \<Longrightarrow> {P'} (p, off) {Q'}"
-using Hoare_def
-proof(auto simp: assert_imp_def)
-  fix l r
-  assume 
-    ho1: "\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps (Suc 0, l, r) (p, off) n) 
-    \<and> Q holds_for steps (Suc 0, l, r) (p, off) n)"
-    and imp1: "\<forall>l r. P' (l, r) \<longrightarrow> P (l, r)"
-    and imp2: "\<forall>l r. Q (l, r) \<longrightarrow> Q' (l, r)"
-    and cond: "P' (l, r)"
-    and ho2: "\<And>P a b Q. {P} (a, b) {Q} \<equiv> \<forall>l r. P (l, r) \<longrightarrow>
-    (\<exists>n. is_final (steps (Suc 0, l, r) (a, b) n) \<and> Q holds_for steps (Suc 0, l, r) (a, b) n)"
-  have "P (l, r)"
-    using cond imp1 by auto
-  hence "(\<exists>n. is_final (steps (Suc 0, l, r) (p, off) n) 
-    \<and> Q holds_for steps (Suc 0, l, r) (p, off) n)"
-    using ho1 by auto
-  from this obtain n where "is_final (steps (Suc 0, l, r) (p, off) n) 
-    \<and> Q holds_for steps (Suc 0, l, r) (p, off) n" ..
-  thus "\<exists>n. is_final (steps (Suc 0, l, r) (p, off) n) \<and> 
-    Q' holds_for steps (Suc 0, l, r) (p, off) n"
-    apply(rule_tac x = n in exI, auto)
-    apply(case_tac "steps (Suc 0, l, r) (p, off) n", simp)
-    using imp2
-    by simp
-qed
+  fixes p::tprog0
+  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
+by (blast intro: holds_for_imp[simplified assert_imp_def])
 
 text {*
   The following locale specifies that TM @{text "H"} can be used to solve 
@@ -1299,25 +1278,25 @@
   let ?P3 = ?Q2
   let ?Q3 = ?P3
   assume h: "\<not> haltP (?tcontr, 0) [code ?tcontr]"
-  have "{?P1} (?tcontr, 0) {?Q3}"
+  have "{?P1} ?tcontr {?Q3}"
   proof(rule_tac Hoare_plus_halt, auto)
     show "?Q2 \<mapsto> ?P3"
       apply(simp add: assert_imp_def)
       done
   next
-    show "{?P1} (tcopy|+|H, 0) {?Q2}"
+    show "{?P1} (tcopy|+|H) {?Q2}"
     proof(rule_tac Hoare_plus_halt, auto)
       show "?Q1 \<mapsto> ?P2"
         apply(simp add: assert_imp_def)
         done
     next
-      show "{?P1} (tcopy, 0) {?Q1}"
+      show "{?P1} tcopy {?Q1}"
       proof -
-        have g: "{inv_init1 ?cn} (tcopy, 0) {inv_end0 ?cn}"
+        have g: "{inv_init1 ?cn} tcopy {inv_end0 ?cn}"
           by(rule_tac tcopy_correct1, simp)
         thus "?thesis"
         proof(rule_tac Hoare_weak)           
-          show "{inv_init1 ?cn} (tcopy, 0)
+          show "{inv_init1 ?cn} tcopy
             {inv_end0 ?cn} " using g by simp
         next
           show "?P1 \<mapsto> inv_init1 (?cn)"
@@ -1330,7 +1309,7 @@
         qed
       qed
     next
-      show "{?P2} (H, 0) {?Q2}"
+      show "{?P2} H {?Q2}"
         using Hoare_def nh_newcase[of ?tcontr "[code ?tcontr]" 1] h
         apply(auto)
         apply(rule_tac x = na in exI)
@@ -1338,7 +1317,7 @@
         done
     qed
   next
-    show "{?P3}(dither, 0){?Q3}"
+    show "{?P3} dither {?Q3}"
       using Hoare_def
     proof(auto)
       fix nd
@@ -1375,25 +1354,25 @@
   let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
   let ?P3 = ?Q2
   assume h: "haltP (?tcontr, 0) [code ?tcontr]"
-  have "{?P1} (?tcontr, 0)"
+  have "{?P1} ?tcontr"
   proof(rule_tac Hoare_plus_unhalt, auto)
     show "?Q2 \<mapsto> ?P3"
       apply(simp add: assert_imp_def)
       done
   next
-    show "{?P1} (tcopy|+|H, 0) {?Q2}"
+    show "{?P1} (tcopy |+| H) {?Q2}"
     proof(rule_tac Hoare_plus_halt, auto)
       show "?Q1 \<mapsto> ?P2"
         apply(simp add: assert_imp_def)
         done
     next
-      show "{?P1} (tcopy, 0) {?Q1}"
+      show "{?P1} tcopy {?Q1}"
       proof -
-        have g: "{inv_init1 ?cn} (tcopy, 0) {inv_end0 ?cn}"
+        have g: "{inv_init1 ?cn} tcopy {inv_end0 ?cn}"
           by(rule_tac tcopy_correct1, simp)
         thus "?thesis"
         proof(rule_tac Hoare_weak)           
-          show "{inv_init1 ?cn} (tcopy, 0)
+          show "{inv_init1 ?cn} tcopy
             {inv_end0 ?cn} " using g by simp
         next
           show "?P1 \<mapsto> inv_init1 (?cn)"
@@ -1406,7 +1385,7 @@
         qed
       qed
     next
-      show "{?P2} (H, 0) {?Q2}"
+      show "{?P2} H {?Q2}"
         using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] h
         apply(auto)
         apply(rule_tac x = na in exI)
@@ -1414,7 +1393,7 @@
         done
     qed
   next
-    show "{?P3}(dither, 0)"
+    show "{?P3} dither"
       using Hoare_unhalt_def
     proof(auto)
       fix nd n