--- a/thys/turing_basic.thy Sat Jan 19 12:46:28 2013 +0000
+++ b/thys/turing_basic.thy Sat Jan 19 14:29:56 2013 +0000
@@ -21,6 +21,8 @@
type_synonym tprog = "instr list \<times> nat"
+type_synonym tprog0 = "instr list"
+
type_synonym config = "state \<times> tape"
fun nth_of where
@@ -78,6 +80,13 @@
"steps c p 0 = c" |
"steps c p (Suc n) = steps (step c p) p n"
+
+abbreviation
+ "step0 c p \<equiv> step c (p, 0)"
+
+abbreviation
+ "steps0 c p n \<equiv> steps c (p, 0) n"
+
lemma step_red [simp]:
shows "steps c p (Suc n) = step (steps c p n) p"
by (induct n arbitrary: c) (auto)
@@ -90,8 +99,7 @@
tm_wf :: "tprog \<Rightarrow> bool"
where
"tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and>
- (\<forall>(a, s) \<in> set p. s \<le> length p div 2
- + off \<and> s \<ge> off))"
+ (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))"
lemma halt_lemma:
"\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
@@ -121,16 +129,15 @@
where
"shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)"
-
-lemma length_shift [simp]:
- "length (shift p n) = length p"
-by (simp)
-
fun
adjust :: "instr list \<Rightarrow> instr list"
where
"adjust p = map (\<lambda> (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"
+lemma length_shift [simp]:
+ "length (shift p n) = length p"
+by simp
+
lemma length_adjust[simp]:
shows "length (adjust p) = length p"
by (induct p) (auto)
@@ -138,7 +145,7 @@
fun
tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100)
where
- "tm_comp p1 p2 = ((adjust p1) @ (shift p2 ((length p1) div 2)))"
+ "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))"
fun
is_final :: "config \<Rightarrow> bool"
@@ -155,21 +162,12 @@
where
"P holds_for (s, l, r) = P (l, r)"
-(*
-lemma step_0 [simp]:
- shows "step (0, (l, r)) p = (0, (l, r))"
-by simp
-
-lemma steps_0 [simp]:
- 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, off) n) = Q holds_for c"
using assms
apply(induct n)
+apply(auto)
apply(case_tac [!] c)
apply(auto)
done
@@ -179,22 +177,23 @@
definition
assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100)
where
- "P \<mapsto> Q = (\<forall>l r. P (l, r) \<longrightarrow> Q (l, r))"
+ "P \<mapsto> Q \<equiv> \<forall>l r. P (l, r) \<longrightarrow> Q (l, r)"
lemma holds_for_imp:
assumes "P holds_for c"
and "P \<mapsto> Q"
shows "Q holds_for c"
-using assms unfolding assert_imp_def by (case_tac c, auto)
+using assms unfolding assert_imp_def
+by (case_tac c) (auto)
definition
- Hoare :: "assert \<Rightarrow> tprog \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)
+ Hoare :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)
where
"{P} p {Q} \<equiv>
- (\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)))"
+ (\<forall>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)))"
lemma HoareI:
- assumes "\<And>l r. P (l, r) \<Longrightarrow> \<exists>n. is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)"
+ 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
@@ -207,85 +206,46 @@
shows "steps (0, (l, r)) p n = (0, (l, r))"
by (induct n) (simp_all)
-declare steps.simps[simp del]
-
-lemma before_final_old:
- assumes "steps (1, tp) A n = (0, tp')"
- obtains n' where "\<not> is_final (steps (1, tp) A n')"
- and "steps (1, tp) A (Suc n') = (0, tp')"
-proof -
- from assms have "\<exists> n'. \<not> is_final (steps (1, tp) A n') \<and>
- steps (1, tp) A (Suc n') = (0, tp')"
- proof(induct n arbitrary: tp', simp add: steps.simps)
- fix n tp'
- assume ind:
- "\<And>tp'. steps (1, tp) A n = (0, tp') \<Longrightarrow>
- \<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
- and h: " steps (1, tp) A (Suc n) = (0, tp')"
- from h show "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
- proof(simp add: step_red del: steps.simps,
- case_tac "(steps (Suc 0, tp) A n)", case_tac "a = 0", simp)
- fix a b c
- assume " steps (Suc 0, tp) A n = (0, tp')"
- hence "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
- apply(rule_tac ind, simp)
- done
- thus "\<exists>n'. \<not> is_final (steps (Suc 0, tp) A n') \<and> step (steps (Suc 0, tp) A n') A = (0, tp')"
- apply(simp)
- done
- next
- fix a b c
- assume "steps (Suc 0, tp) A n = (a, b, c)"
- "step (steps (Suc 0, tp) A n) A = (0, tp')"
- "a \<noteq> 0"
- thus "\<exists>n'. \<not> is_final (steps (Suc 0, tp) A n') \<and>
- step (steps (Suc 0, tp) A n') A = (0, tp')"
- apply(rule_tac x = n in exI)
- apply(simp)
- done
- qed
- qed
- thus "(\<And>n'. \<lbrakk>\<not> is_final (steps (1, tp) A n');
- steps (1, tp) A (Suc n') = (0, tp')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis"
- by auto
-qed
-
+(* if the machine is in the halting state, there must have
+ been a state just before the halting state *)
lemma before_final:
- assumes "steps (1, tp) A n = (0, tp')"
- shows "\<exists> n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
+ assumes "steps0 (1, tp) A n = (0, tp')"
+ shows "\<exists> n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
using assms
proof(induct n arbitrary: tp')
case (0 tp')
- have asm: "steps (1, tp) A 0 = (0, tp')" by fact
- then show "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
- by (simp add: steps.simps)
+ have asm: "steps0 (1, tp) A 0 = (0, tp')" by fact
+ then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
+ by simp
next
case (Suc n tp')
- have ih: "\<And>tp'. steps (1, tp) A n = (0, tp') \<Longrightarrow>
- \<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" by fact
- have asm: "steps (1, tp) A (Suc n) = (0, tp')" by fact
- obtain s l r where cases: "steps (1, tp) A n = (s, l, r)"
+ have ih: "\<And>tp'. steps0 (1, tp) A n = (0, tp') \<Longrightarrow>
+ \<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')" by fact
+ have asm: "steps0 (1, tp) A (Suc n) = (0, tp')" by fact
+ obtain s l r where cases: "steps0 (1, tp) A n = (s, l, r)"
by (auto intro: is_final.cases)
- then show "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
+ then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
proof (cases "s = 0")
case True (* in halting state *)
- then have "steps (1, tp) A n = (0, tp')"
- using asm cases by simp
+ then have "steps0 (1, tp) A n = (0, tp')"
+ using asm cases by (simp del: steps.simps)
then show ?thesis using ih by simp
next
case False (* not in halting state *)
- then have "\<not> is_final (steps (1, tp) A n) \<and> steps (1, tp) A (Suc n) = (0, tp')"
+ then have "\<not> is_final (steps0 (1, tp) A n) \<and> steps0 (1, tp) A (Suc n) = (0, tp')"
using asm cases by simp
then show ?thesis by auto
qed
qed
-declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]
lemma length_comp:
-"length (A |+| B) = length A + length B"
-apply(auto simp: tm_comp.simps)
-done
+ shows "length (A |+| B) = length A + length B"
+by auto
+
+declare steps.simps[simp del]
+declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]
+
lemma tmcomp_fetch_in_first:
assumes "case (fetch A a x) of (ac, ns) \<Rightarrow> ns \<noteq> 0"
@@ -532,32 +492,32 @@
assumes aimpb: "Q1 \<mapsto> P2"
and A_wf : "tm_wf (A, 0)"
and B_wf : "tm_wf (B, 0)"
- and A_halt : "{P1} (A, 0) {Q1}"
- and B_halt : "{P2} (B, 0) {Q2}"
- shows "{P1} (A |+| B, 0) {Q2}"
+ and A_halt : "{P1} A {Q1}"
+ and B_halt : "{P2} B {Q2}"
+ shows "{P1} A |+| B {Q2}"
proof(rule HoareI)
fix l r
assume h: "P1 (l, r)"
then obtain n1
- where "is_final (steps (1, l, r) (A, 0) n1)" and "Q1 holds_for (steps (1, l, r) (A, 0) n1)"
+ where "is_final (steps0 (1, l, r) A n1)" and "Q1 holds_for (steps0 (1, l, r) A n1)"
using A_halt unfolding Hoare_def by auto
- then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"
- by(case_tac "steps (1, l, r) (A, 0) n1") (auto)
- then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')"
+ then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"
+ by(case_tac "steps0 (1, l, r) A n1") (auto)
+ then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')"
using A_wf by(rule_tac t_merge_pre_halt_same) (auto)
moreover
from c aimpb have "P2 holds_for (0, l', r')"
by (rule holds_for_imp)
then have "P2 (l', r')" by auto
then obtain n2
- where "is_final (steps (1, l', r') (B, 0) n2)" and "Q2 holds_for (steps (1, l', r') (B, 0) n2)"
+ where "is_final (steps0 (1, l', r') B n2)" and "Q2 holds_for (steps0 (1, l', r') B n2)"
using B_halt unfolding Hoare_def by auto
- then obtain l'' r'' where "steps (1, l', r') (B, 0) n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')"
- by (case_tac "steps (1, l', r') (B, 0) n2", auto)
- then have "steps (Suc (length A div 2), l', r') (A |+| B, 0) n2 = (0, l'', r'')"
+ then obtain l'' r'' where "steps0 (1, l', r') B n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')"
+ by (case_tac "steps0 (1, l', r') B n2", auto)
+ then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n2 = (0, l'', r'')"
by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf)
ultimately show
- "\<exists>n. is_final (steps (1, l, r) (A |+| B, 0) n) \<and> Q2 holds_for (steps (1, l, r) (A |+| B, 0) n)"
+ "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps0 (1, l, r) (A |+| B) n)"
using g
apply(rule_tac x = "stpa + n2" in exI)
apply(simp add: steps_add)
@@ -565,69 +525,70 @@
qed
definition
- Hoare_unhalt :: "assert \<Rightarrow> tprog \<Rightarrow> bool" ("({(1_)}/ (_))" 50)
+ Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_))" 50)
where
"{P} p \<equiv>
- (\<forall>l r. P (l, r) \<longrightarrow> (\<forall> n . \<not> (is_final (steps (1, (l, r)) p n))))"
+ (\<forall>l r. P (l, r) \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, (l, r)) p n))))"
lemma Hoare_unhalt_I:
- assumes "\<And>l r. P (l, r) \<Longrightarrow> \<forall> n. \<not> is_final (steps (1, (l, r)) p n)"
+ assumes "\<And>l r. P (l, r) \<Longrightarrow> \<forall> n. \<not> is_final (steps0 (1, (l, r)) p n)"
shows "{P} p"
unfolding Hoare_unhalt_def using assms by auto
-lemma Hoare_plus_unhalt:
+lemma Hoare_plus_unhalt:
+ fixes A B :: tprog0
assumes aimpb: "Q1 \<mapsto> P2"
and A_wf : "tm_wf (A, 0)"
and B_wf : "tm_wf (B, 0)"
- and A_halt : "{P1} (A, 0) {Q1}"
- and B_uhalt : "{P2} (B, 0)"
- shows "{P1} (A |+| B, 0)"
+ and A_halt : "{P1} A {Q1}"
+ and B_uhalt : "{P2} B"
+ shows "{P1} (A |+| B)"
proof(rule_tac Hoare_unhalt_I)
fix l r
assume h: "P1 (l, r)"
- then obtain n1 where a: "is_final (steps (1, l, r) (A, 0) n1)" and b: "Q1 holds_for (steps (1, l, r) (A, 0) n1)"
+ then obtain n1 where a: "is_final (steps0 (1, l, r) A n1)" and b: "Q1 holds_for (steps0 (1, l, r) A n1)"
using A_halt unfolding Hoare_def by auto
- then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"
- by(case_tac "steps (1, l, r) (A, 0) n1", auto)
- then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')"
+ then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"
+ by(case_tac "steps0 (1, l, r) A n1", auto)
+ then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')"
using A_wf
by(rule_tac t_merge_pre_halt_same, auto)
from c aimpb have "P2 holds_for (0, l', r')"
by(rule holds_for_imp)
from this have "P2 (l', r')" by auto
- from this have e: "\<forall> n. \<not> is_final (steps (Suc 0, l', r') (B, 0) n) "
+ from this have e: "\<forall> n. \<not> is_final (steps0 (Suc 0, l', r') B n) "
using B_uhalt unfolding Hoare_unhalt_def
by auto
- from e show "\<forall>n. \<not> is_final (steps (1, l, r) (A |+| B, 0) n)"
+ from e show "\<forall>n. \<not> is_final (steps0 (1, l, r) (A |+| B) n)"
proof(rule_tac allI, case_tac "n > stpa")
fix n
assume h2: "stpa < n"
- hence "\<not> is_final (steps (Suc 0, l', r') (B, 0) (n - stpa))"
+ hence "\<not> is_final (steps0 (Suc 0, l', r') B (n - stpa))"
using e
apply(erule_tac x = "n - stpa" in allE) by simp
- then obtain s'' l'' r'' where f: "steps (Suc 0, l', r') (B, 0) (n - stpa) = (s'', l'', r'')" and g: "s'' \<noteq> 0"
- apply(case_tac "steps (Suc 0, l', r') (B, 0) (n - stpa)", auto)
+ then obtain s'' l'' r'' where f: "steps0 (Suc 0, l', r') B (n - stpa) = (s'', l'', r'')" and g: "s'' \<noteq> 0"
+ apply(case_tac "steps0 (Suc 0, l', r') B (n - stpa)", auto)
done
- have k: "steps (Suc (length A div 2), l', r') (A |+| B, 0) (n - stpa) = (s''+ length A div 2, l'', r'') "
+ have k: "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - stpa) = (s''+ length A div 2, l'', r'') "
using A_wf B_wf f g
apply(drule_tac t_merge_second_same, auto)
done
- show "\<not> is_final (steps (1, l, r) (A |+| B, 0) n)"
+ show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)"
proof -
- have "\<not> is_final (steps (1, l, r) (A |+| B, 0) (stpa + (n - stpa)))"
+ have "\<not> is_final (steps0 (1, l, r) (A |+| B) (stpa + (n - stpa)))"
using d k A_wf
apply(simp only: steps_add d, simp add: tm_wf.simps)
done
- thus "\<not> is_final (steps (1, l, r) (A |+| B, 0) n)"
+ thus "\<not> is_final (steps0 (1, l, r) (A |+| B) n)"
using h2 by simp
qed
next
fix n
assume h2: "\<not> stpa < n"
- with d show "\<not> is_final (steps (1, l, r) (A |+| B, 0) n)"
+ with d show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)"
apply(auto)
apply(subgoal_tac "\<exists> d. stpa = n + d", auto)
- apply(case_tac "(steps (Suc 0, l, r) (A |+| B, 0) n)", simp)
+ apply(case_tac "(steps0 (Suc 0, l, r) (A |+| B) n)", simp)
apply(rule_tac x = "stpa - n" in exI, simp)
done
qed
--- 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