55
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
theory turing_hoare
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
imports turing_basic
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
begin
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
5 |
declare step.simps[simp del]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
6 |
declare steps.simps[simp del]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
7 |
declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
8 |
declare tm_wf.simps[simp del]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
9 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
10 |
|
55
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
type_synonym assert = "tape \<Rightarrow> bool"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
"P \<mapsto> Q \<equiv> \<forall>l r. P (l, r) \<longrightarrow> Q (l, r)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
fun
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
holds_for :: "(tape \<Rightarrow> bool) \<Rightarrow> config \<Rightarrow> bool" ("_ holds'_for _" [100, 99] 100)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
"P holds_for (s, l, r) = P (l, r)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
lemma is_final_holds[simp]:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
assumes "is_final c"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
shows "Q holds_for (steps c (p, off) n) = Q holds_for c"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
using assms
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
apply(induct n)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
apply(auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
apply(case_tac [!] c)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
apply(auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
lemma holds_for_imp:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
assumes "P holds_for c"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
and "P \<mapsto> Q"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
shows "Q holds_for c"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
using assms unfolding assert_imp_def
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
by (case_tac c) (auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
Hoare :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
"{P} p {Q} \<equiv>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
(\<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)))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
46 |
lemma HoareI:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
47 |
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)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
shows "{P} p {Q}"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
unfolding Hoare_def using assms by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
51 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
text {*
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
53 |
{P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 A, B well-formed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
54 |
------------------------------------------------------
|
55
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
{P1} A |+| B {Q2}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
58 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
lemma Hoare_plus_halt:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
assumes aimpb: "Q1 \<mapsto> P2"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
61 |
and A_wf : "tm_wf (A, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
62 |
and B_wf : "tm_wf (B, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
63 |
and A_halt : "{P1} A {Q1}"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
64 |
and B_halt : "{P2} B {Q2}"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
65 |
shows "{P1} A |+| B {Q2}"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
66 |
proof(rule HoareI)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
67 |
fix l r
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
68 |
assume h: "P1 (l, r)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
69 |
then obtain n1
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
70 |
where "is_final (steps0 (1, l, r) A n1)" and "Q1 holds_for (steps0 (1, l, r) A n1)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
71 |
using A_halt unfolding Hoare_def by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
72 |
then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
73 |
by(case_tac "steps0 (1, l, r) A n1") (auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
74 |
then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')"
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
75 |
using A_wf by(rule_tac tm_comp_pre_halt_same) (auto)
|
55
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
76 |
moreover
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
77 |
from c aimpb have "P2 holds_for (0, l', r')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
78 |
by (rule holds_for_imp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
79 |
then have "P2 (l', r')" by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
80 |
then obtain n2
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
81 |
where "is_final (steps0 (1, l', r') B n2)" and "Q2 holds_for (steps0 (1, l', r') B n2)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
82 |
using B_halt unfolding Hoare_def by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
83 |
then obtain l'' r'' where "steps0 (1, l', r') B n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')"
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
84 |
by (case_tac "steps0 (1, l', r') B n2") (auto)
|
55
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
85 |
then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n2 = (0, l'', r'')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
86 |
by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
87 |
ultimately show
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
88 |
"\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps0 (1, l, r) (A |+| B) n)"
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
89 |
using g
|
55
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
90 |
apply(rule_tac x = "stpa + n2" in exI)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
91 |
apply(simp add: steps_add)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
92 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
93 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
94 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
95 |
definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
96 |
Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_))" 50)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
97 |
where
|
56
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
98 |
"{P} p \<equiv> (\<forall>l r. P (l, r) \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, (l, r)) p n))))"
|
55
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
99 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
100 |
lemma Hoare_unhalt_I:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
101 |
assumes "\<And>l r. P (l, r) \<Longrightarrow> \<forall> n. \<not> is_final (steps0 (1, (l, r)) p n)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
102 |
shows "{P} p"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
103 |
unfolding Hoare_unhalt_def using assms by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
104 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
105 |
lemma Hoare_plus_unhalt:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
106 |
fixes A B :: tprog0
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
107 |
assumes aimpb: "Q1 \<mapsto> P2"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
108 |
and A_wf : "tm_wf (A, 0)"
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
109 |
and B_wf : "tm_wf (B, 0)" (* probably not needed *)
|
55
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
110 |
and A_halt : "{P1} A {Q1}"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
111 |
and B_uhalt : "{P2} B"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
112 |
shows "{P1} (A |+| B)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
113 |
proof(rule_tac Hoare_unhalt_I)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
114 |
fix l r
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
115 |
assume h: "P1 (l, r)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
116 |
then obtain n1 where a: "is_final (steps0 (1, l, r) A n1)" and b: "Q1 holds_for (steps0 (1, l, r) A n1)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
117 |
using A_halt unfolding Hoare_def by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
118 |
then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
119 |
by(case_tac "steps0 (1, l, r) A n1", auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
120 |
then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
121 |
using A_wf
|
59
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
122 |
by(rule_tac tm_comp_pre_halt_same, auto)
|
55
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
123 |
from c aimpb have "P2 holds_for (0, l', r')"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
124 |
by(rule holds_for_imp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
125 |
from this have "P2 (l', r')" by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
126 |
from this have e: "\<forall> n. \<not> is_final (steps0 (Suc 0, l', r') B n) "
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
127 |
using B_uhalt unfolding Hoare_unhalt_def
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
128 |
by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
129 |
from e show "\<forall>n. \<not> is_final (steps0 (1, l, r) (A |+| B) n)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
130 |
proof(rule_tac allI, case_tac "n > stpa")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
131 |
fix n
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
132 |
assume h2: "stpa < n"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
133 |
hence "\<not> is_final (steps0 (Suc 0, l', r') B (n - stpa))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
134 |
using e
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
135 |
apply(erule_tac x = "n - stpa" in allE) by simp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
136 |
then obtain s'' l'' r'' where f: "steps0 (Suc 0, l', r') B (n - stpa) = (s'', l'', r'')" and g: "s'' \<noteq> 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
137 |
apply(case_tac "steps0 (Suc 0, l', r') B (n - stpa)", auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
138 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
139 |
have k: "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - stpa) = (s''+ length A div 2, l'', r'') "
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
140 |
using A_wf B_wf f g
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
141 |
apply(drule_tac t_merge_second_same, auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
142 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
143 |
show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
144 |
proof -
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
145 |
have "\<not> is_final (steps0 (1, l, r) (A |+| B) (stpa + (n - stpa)))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
146 |
using d k A_wf
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
147 |
apply(simp only: steps_add d, simp add: tm_wf.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
148 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
149 |
thus "\<not> is_final (steps0 (1, l, r) (A |+| B) n)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
150 |
using h2 by simp
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
151 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
152 |
next
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
153 |
fix n
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
154 |
assume h2: "\<not> stpa < n"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
155 |
with d show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
156 |
apply(auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
157 |
apply(subgoal_tac "\<exists> d. stpa = n + d", auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
158 |
apply(case_tac "(steps0 (Suc 0, l, r) (A |+| B) n)", simp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
159 |
apply(rule_tac x = "stpa - n" in exI, simp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
160 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
161 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
162 |
qed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
163 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
164 |
lemma Hoare_weak:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
165 |
fixes p::tprog0
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
166 |
assumes a: "{P} p {Q}"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
167 |
and b: "P' \<mapsto> P"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
168 |
and c: "Q \<mapsto> Q'"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
169 |
shows "{P'} p {Q'}"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
170 |
using assms
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
171 |
unfolding Hoare_def assert_imp_def
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
172 |
by (blast intro: holds_for_imp[simplified assert_imp_def])
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
173 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
174 |
end |