--- 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