|
1 header {* |
|
2 {\em abacus} a kind of register machine |
|
3 *} |
|
4 |
|
5 theory abacus |
|
6 imports Main StateMonad |
|
7 begin |
|
8 |
|
9 text {* |
|
10 {\em Abacus} instructions: |
|
11 *} |
|
12 |
|
13 datatype abc_inst = |
|
14 -- {* @{text "Inc n"} increments the memory cell (or register) |
|
15 with address @{text "n"} by one. |
|
16 *} |
|
17 Inc nat |
|
18 -- {* |
|
19 @{text "Dec n label"} decrements the memory cell with address @{text "n"} by one. |
|
20 If cell @{text "n"} is already zero, no decrements happens and the executio jumps to |
|
21 the instruction labeled by @{text "label"}. |
|
22 *} |
|
23 | Dec nat nat |
|
24 -- {* |
|
25 @{text "Goto label"} unconditionally jumps to the instruction labeled by @{text "label"}. |
|
26 *} |
|
27 | Goto nat |
|
28 |
|
29 |
|
30 fun splits :: "'a set \<Rightarrow> ('a set \<times> 'a set) \<Rightarrow> bool" |
|
31 where "splits s (u, v) = (u \<union> v = s \<and> u \<inter> v = {})" |
|
32 |
|
33 declare splits.simps [simp del] |
|
34 |
|
35 definition "stimes p q = {s . \<exists> u v. u \<in> p \<and> v \<in> q \<and> splits s (u, v)}" |
|
36 lemmas st_def = stimes_def[unfolded splits.simps] |
|
37 |
|
38 notation stimes (infixr "*" 70) |
|
39 |
|
40 lemma stimes_comm: "(p::('a set set)) * q = q * p" |
|
41 by (unfold st_def, auto) |
|
42 |
|
43 lemma splits_simp: "splits s (u, v) = (v = (s - u) \<and> v \<subseteq> s \<and> u \<subseteq> s)" |
|
44 by (unfold splits.simps, auto) |
|
45 |
|
46 lemma stimes_assoc: "p * q * r = (p * q) * (r::'a set set)" |
|
47 by (unfold st_def, blast) |
|
48 |
|
49 definition |
|
50 "emp = {{}}" |
|
51 |
|
52 lemma emp_unit_r [simp]: "p * emp = p" |
|
53 by (unfold st_def emp_def, auto) |
|
54 |
|
55 lemma emp_unit_l [simp]: "emp * p = p" |
|
56 by (metis emp_unit_r stimes_comm) |
|
57 |
|
58 lemma stimes_mono: "p \<subseteq> q \<Longrightarrow> p * r \<subseteq> q * r" |
|
59 by (unfold st_def, auto) |
|
60 |
|
61 lemma stimes_left_commute: |
|
62 "(q * (p * r)) = ((p::'a set set) * (q * r))" |
|
63 by (metis stimes_assoc stimes_comm) |
|
64 |
|
65 lemmas stimes_ac = stimes_comm stimes_assoc stimes_left_commute |
|
66 |
|
67 lemma "x * y * z = z * y * (x::'a set set)" |
|
68 by (metis stimes_ac) |
|
69 |
|
70 |
|
71 definition pasrt :: "bool \<Rightarrow> ('a set set)" ("<_>" [71] 71) |
|
72 where "pasrt b = {s . s = {} \<and> b}" |
|
73 |
|
74 datatype apg = |
|
75 Instr abc_inst |
|
76 | Label nat |
|
77 | Seq apg apg |
|
78 | Local "(nat \<Rightarrow> apg)" |
|
79 |
|
80 abbreviation prog_instr :: "abc_inst \<Rightarrow> apg" ("\<guillemotright>_" [61] 61) |
|
81 where "\<guillemotright>i \<equiv> Instr i" |
|
82 |
|
83 abbreviation prog_seq :: "apg \<Rightarrow> apg \<Rightarrow> apg" (infixr ";" 52) |
|
84 where "c1 ; c2 \<equiv> Seq c1 c2" |
|
85 |
|
86 type_synonym aconf = "((nat \<rightharpoonup> abc_inst) \<times> nat \<times> (nat \<rightharpoonup> nat) \<times> nat)" |
|
87 |
|
88 fun astep :: "aconf \<Rightarrow> aconf" |
|
89 where "astep (prog, pc, m, faults) = |
|
90 (case (prog pc) of |
|
91 Some (Inc i) \<Rightarrow> |
|
92 case m(i) of |
|
93 Some n \<Rightarrow> (prog, pc + 1, m(i:= Some (n + 1)), faults) |
|
94 | None \<Rightarrow> (prog, pc, m, faults + 1) |
|
95 | Some (Dec i e) \<Rightarrow> |
|
96 case m(i) of |
|
97 Some n \<Rightarrow> if (n = 0) then (prog, e, m, faults) |
|
98 else (prog, pc + 1, m(i:= Some (n - 1)), faults) |
|
99 | None \<Rightarrow> (prog, pc, m, faults + 1) |
|
100 | Some (Goto pc') \<Rightarrow> (prog, pc', m, faults) |
|
101 | None \<Rightarrow> (prog, pc, m, faults + 1))" |
|
102 |
|
103 definition "run n = astep ^^ n" |
|
104 |
|
105 datatype aresource = |
|
106 M nat nat |
|
107 | C nat abc_inst |
|
108 | At nat |
|
109 | Faults nat |
|
110 |
|
111 definition "prog_set prog = {C i inst | i inst. prog i = Some inst}" |
|
112 definition "pc_set pc = {At pc}" |
|
113 definition "mem_set m = {M i n | i n. m (i) = Some n} " |
|
114 definition "faults_set faults = {Faults faults}" |
|
115 |
|
116 lemmas cpn_set_def = prog_set_def pc_set_def mem_set_def faults_set_def |
|
117 |
|
118 fun rset_of :: "aconf \<Rightarrow> aresource set" |
|
119 where "rset_of (prog, pc, m, faults) = |
|
120 prog_set prog \<union> pc_set pc \<union> mem_set m \<union> faults_set faults" |
|
121 |
|
122 definition "pc l = {pc_set l}" |
|
123 |
|
124 |
|
125 definition "m a v = {{M a v}}" |
|
126 |
|
127 |
|
128 declare rset_of.simps[simp del] |
|
129 |
|
130 type_synonym assert = "aresource set set" |
|
131 |
|
132 primrec assemble_to :: "apg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> assert" |
|
133 where |
|
134 "assemble_to (Instr ai) i j = ({{C i ai}} * <(j = i + 1)>)" | |
|
135 "assemble_to (Seq p1 p2) i j = (\<Union> j'. (assemble_to p1 i j') * (assemble_to p2 j' j))" | |
|
136 "assemble_to (Local fp) i j = (\<Union> l. (assemble_to (fp l) i j))" | |
|
137 "assemble_to (Label l) i j = <(i = j \<and> j = l)>" |
|
138 |
|
139 abbreviation asmb_to :: "nat \<Rightarrow> apg \<Rightarrow> nat \<Rightarrow> assert" ("_ :[ _ ]: _" [60, 60, 60] 60) |
|
140 where "i :[ apg ]: j \<equiv> assemble_to apg i j" |
|
141 |
|
142 lemma stimes_sgD: "s \<in> {x} * q \<Longrightarrow> (s - x) \<in> q \<and> x \<subseteq> s" |
|
143 apply (unfold st_def, auto) |
|
144 by (smt Diff_disjoint Un_Diff_cancel2 Un_Int_distrib |
|
145 Un_commute Un_empty_right Un_left_absorb) |
|
146 |
|
147 lemma pcD: "rset_of (prog, i', mem, fault) \<in> pc i * r |
|
148 \<Longrightarrow> i' = i" |
|
149 proof - |
|
150 assume "rset_of (prog, i', mem, fault) \<in> pc i * r" |
|
151 from stimes_sgD [OF this[unfolded pc_def], unfolded rset_of.simps] |
|
152 have "pc_set i \<subseteq> prog_set prog \<union> pc_set i' \<union> mem_set mem \<union> faults_set fault" by auto |
|
153 thus ?thesis |
|
154 by (unfold cpn_set_def, auto) |
|
155 qed |
|
156 |
|
157 lemma codeD: "rset_of (prog, pos, mem, fault) \<in> pc i * {{C i inst}} * r |
|
158 \<Longrightarrow> prog pos = Some inst" |
|
159 proof - |
|
160 assume h: "rset_of (prog, pos, mem, fault) \<in> pc i * {{C i inst}} * r" (is "?c \<in> ?X") |
|
161 from pcD[OF this] have "i = pos" by simp |
|
162 with h show ?thesis |
|
163 by (unfold rset_of.simps st_def pc_def prog_set_def |
|
164 pc_set_def mem_set_def faults_set_def, auto) |
|
165 qed |
|
166 |
|
167 lemma memD: "rset_of (prog, pos, mem, fault) \<in> (m a v) * r \<Longrightarrow> mem a = Some v" |
|
168 proof - |
|
169 assume "rset_of (prog, pos, mem, fault) \<in> (m a v) * r" |
|
170 from stimes_sgD[OF this[unfolded rset_of.simps cpn_set_def m_def]] |
|
171 have "{M a v} \<subseteq> {C i inst |i inst. prog i = Some inst} \<union> |
|
172 {At pos} \<union> {M i n |i n. mem i = Some n} \<union> {Faults fault}" by auto |
|
173 thus ?thesis by auto |
|
174 qed |
|
175 |
|
176 definition |
|
177 Hoare_abc :: "assert \<Rightarrow> assert \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
|
178 where |
|
179 "{p} c {q} \<equiv> (\<forall> s r. (rset_of s) \<in> (p*c*r) \<longrightarrow> |
|
180 (\<exists> k. ((rset_of (run k s)) \<in> (q*c*r))))" |
|
181 |
|
182 definition "dec_fun v j e = (if (v = 0) then (e, v) else (j, v - 1))" |
|
183 |
|
184 lemma disj_Diff: "a \<inter> b = {} \<Longrightarrow> a \<union> b - b = a" |
|
185 by (metis (lifting) Diff_cancel Un_Diff Un_Diff_Int) |
|
186 |
|
187 lemma diff_pc_set: "prog_set aa \<union> pc_set i \<union> mem_set ab \<union> faults_set b - pc_set i = |
|
188 prog_set aa \<union> mem_set ab \<union> faults_set b" (is "?L = ?R") |
|
189 proof - |
|
190 have "?L = (prog_set aa \<union> mem_set ab \<union> faults_set b \<union> pc_set i) - pc_set i" |
|
191 by auto |
|
192 also have "\<dots> = ?R" |
|
193 proof(rule disj_Diff) |
|
194 show " (prog_set aa \<union> mem_set ab \<union> faults_set b) \<inter> pc_set i = {}" |
|
195 by (unfold cpn_set_def, auto) |
|
196 qed |
|
197 finally show ?thesis . |
|
198 qed |
|
199 |
|
200 lemma M_in_simp: "({M a v} \<subseteq> prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f) = |
|
201 ({M a v} \<subseteq> mem_set mem)" |
|
202 by (unfold cpn_set_def, auto) |
|
203 |
|
204 lemma mem_set_upd: |
|
205 "{M a v} \<subseteq> mem_set mem \<Longrightarrow> mem_set (mem(a:=Some v')) = ((mem_set mem) - {M a v}) \<union> {M a v'}" |
|
206 by (unfold cpn_set_def, auto) |
|
207 |
|
208 lemma mem_set_disj: "{M a v} \<subseteq> mem_set mem \<Longrightarrow> {M a v'} \<inter> (mem_set mem - {M a v}) = {}" |
|
209 by (unfold cpn_set_def, auto) |
|
210 |
|
211 lemma stimesE: |
|
212 assumes h: "s \<in> x * y" |
|
213 obtains s1 s2 where "s = s1 \<union> s2" and "s1 \<inter> s2 = {}" and "s1 \<in> x" and "s2 \<in> y" |
|
214 by (insert h, auto simp:st_def) |
|
215 |
|
216 lemma stimesI: |
|
217 "\<lbrakk>s = s1 \<union> s2; s1 \<inter> s2 = {}; s1 \<in> x; s2 \<in> y\<rbrakk> \<Longrightarrow> s \<in> x * y" |
|
218 by (auto simp:st_def) |
|
219 |
|
220 lemma smem_upd: "(rset_of (x, y, mem, f)) \<in> (m a v)*r \<Longrightarrow> |
|
221 (rset_of (x, y, mem(a := Some v'), f) \<in> (m a v')*r)" |
|
222 proof - |
|
223 assume h: " rset_of (x, y, mem, f) \<in> m a v * r" |
|
224 from h[unfolded rset_of.simps m_def] |
|
225 have "prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f \<in> {{M a v}} * r" . |
|
226 from stimes_sgD [OF this] |
|
227 have h1: "prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f - {M a v} \<in> r" |
|
228 "{M a v} \<subseteq> prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f" by auto |
|
229 moreover have "prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f - {M a v} = |
|
230 prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f" |
|
231 by (unfold cpn_set_def, auto) |
|
232 ultimately have h0: "prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f \<in> r" |
|
233 by simp |
|
234 from h1(2) and M_in_simp have "{M a v} \<subseteq> mem_set mem" by simp |
|
235 from mem_set_upd [OF this] mem_set_disj[OF this] |
|
236 have h2: "mem_set (mem(a \<mapsto> v')) = {M a v'} \<union> (mem_set mem - {M a v})" |
|
237 "{M a v'} \<inter> (mem_set mem - {M a v}) = {}" by auto |
|
238 show ?thesis |
|
239 proof - |
|
240 have "mem_set (mem(a \<mapsto> v')) \<union> prog_set x \<union> pc_set y \<union> faults_set f \<in> m a v' * r" |
|
241 proof(rule stimesI[OF _ _ _ h0]) |
|
242 show "{M a v'} \<in> m a v'" by (unfold m_def, auto) |
|
243 next |
|
244 show "mem_set (mem(a \<mapsto> v')) \<union> prog_set x \<union> pc_set y \<union> faults_set f = |
|
245 {M a v'} \<union> (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f)" |
|
246 apply (unfold h2(1)) |
|
247 by (smt Un_commute Un_insert_left Un_insert_right |
|
248 Un_left_commute |
|
249 `prog_set x \<union> pc_set y \<union> mem_set mem \<union> |
|
250 faults_set f - {M a v} =prog_set x \<union> pc_set y |
|
251 \<union> (mem_set mem - {M a v}) \<union> faults_set f`) |
|
252 next |
|
253 from h2(2) |
|
254 show "{M a v'} \<inter> (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f) = {}" |
|
255 by (unfold cpn_set_def, auto) |
|
256 qed |
|
257 thus ?thesis |
|
258 apply (unfold rset_of.simps) |
|
259 by (metis `mem_set (mem(a \<mapsto> v')) |
|
260 \<union> prog_set x \<union> pc_set y \<union> faults_set f \<in> m a v' * r` |
|
261 stimes_comm sup_commute sup_left_commute) |
|
262 qed |
|
263 qed |
|
264 |
|
265 lemma spc_upd: "rset_of (x, i, y, z) \<in> pc i' * r \<Longrightarrow> |
|
266 rset_of (x, i'', y, z) \<in> pc i'' * r" |
|
267 proof - |
|
268 assume h: "rset_of (x, i, y, z) \<in> pc i' * r" |
|
269 from stimes_sgD [OF h[unfolded rset_of.simps pc_set_def pc_def]] |
|
270 have h1: "prog_set x \<union> {At i} \<union> mem_set y \<union> faults_set z - {At i'} \<in> r" |
|
271 "{At i'} \<subseteq> prog_set x \<union> {At i} \<union> mem_set y \<union> faults_set z" by auto |
|
272 from h1(2) have eq_i: "i' = i" by (unfold cpn_set_def, auto) |
|
273 have "prog_set x \<union> {At i} \<union> mem_set y \<union> faults_set z - {At i'} = |
|
274 prog_set x \<union> mem_set y \<union> faults_set z " |
|
275 apply (unfold eq_i) |
|
276 by (metis (full_types) Un_insert_left Un_insert_right |
|
277 diff_pc_set faults_set_def insert_commute insert_is_Un |
|
278 pc_set_def sup_assoc sup_bot_left sup_commute) |
|
279 with h1(1) have in_r: "prog_set x \<union> mem_set y \<union> faults_set z \<in> r" by auto |
|
280 show ?thesis |
|
281 proof(unfold rset_of.simps, rule stimesI[OF _ _ _ in_r]) |
|
282 show "{At i''} \<in> pc i''" by (unfold pc_def pc_set_def, simp) |
|
283 next |
|
284 show "prog_set x \<union> pc_set i'' \<union> mem_set y \<union> faults_set z = |
|
285 {At i''} \<union> (prog_set x \<union> mem_set y \<union> faults_set z)" |
|
286 by (unfold pc_set_def, auto) |
|
287 next |
|
288 show "{At i''} \<inter> (prog_set x \<union> mem_set y \<union> faults_set z) = {}" |
|
289 by (auto simp:cpn_set_def) |
|
290 qed |
|
291 qed |
|
292 |
|
293 lemma condD: "s \<in> <b>*r \<Longrightarrow> b" |
|
294 by (unfold st_def pasrt_def, auto) |
|
295 |
|
296 lemma condD1: "s \<in> <b>*r \<Longrightarrow> s \<in> r" |
|
297 by (unfold st_def pasrt_def, auto) |
|
298 |
|
299 lemma hoare_dec_suc: "{(pc i * m a v) * <(v > 0)>} |
|
300 i:[\<guillemotright>(Dec a e) ]:j |
|
301 {pc j * m a (v - 1)}" |
|
302 proof(unfold Hoare_abc_def, clarify) |
|
303 fix prog i' ab b r |
|
304 assume h: "rset_of (prog, i', ab, b) \<in> ((pc i * m a v) * <(0 < v)>) * (i :[ \<guillemotright>Dec a e ]: j) * r" |
|
305 (is "?r \<in> ?S") |
|
306 show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> (pc j * m a (v - 1)) * (i :[ \<guillemotright>Dec a e ]: j) * r" |
|
307 proof - |
|
308 from h [unfolded assemble_to.simps] |
|
309 have h1: "?r \<in> pc i * {{C i (Dec a e)}} * m a v * <(0 < v)> * <(j = i + 1)> * r" |
|
310 "?r \<in> m a v * pc i * {{C i (Dec a e)}} * <(0 < v)> * <(j = i + 1)> * r" |
|
311 "?r \<in> <(0 < v)> * <(j = i + 1)> * m a v * pc i * {{C i (Dec a e)}} * r" |
|
312 "?r \<in> <(j = i + 1)> * <(0 < v)> * m a v * pc i * {{C i (Dec a e)}} * r" |
|
313 by ((metis stimes_ac)+) |
|
314 note h2 = condD [OF h1(3)] condD[OF h1(4)] pcD[OF h1(1)] codeD[OF h1(1)] memD[OF h1(2)] |
|
315 hence stp: "run 1 (prog, i', ab, b) = (prog, Suc i, ab(a \<mapsto> v - Suc 0), b)" (is "?x = ?y") |
|
316 by (unfold run_def, auto) |
|
317 have "rset_of ?x \<in> (pc j * m a (v - 1)) * (i :[ \<guillemotright>Dec a e ]: j) * r" |
|
318 proof - |
|
319 have "rset_of ?y \<in> (pc j * m a (v - 1)) * (i :[ \<guillemotright>Dec a e ]: j) * r" |
|
320 proof - |
|
321 from spc_upd[OF h1(1), of "Suc i"] |
|
322 have "rset_of (prog, (Suc i), ab, b) \<in> |
|
323 m a v * pc (Suc i) * {{C i (Dec a e)}} * <(0 < v)> * <(j = i + 1)> * r" |
|
324 by (metis stimes_ac) |
|
325 from smem_upd[OF this, of "v - (Suc 0)"] |
|
326 have "rset_of ?y \<in> |
|
327 m a (v - Suc 0) * pc (Suc i) * {{C i (Dec a e)}} * <(0 < v)> * <(j = i + 1)> * r" . |
|
328 hence "rset_of ?y \<in> <(0 < v)> * |
|
329 (pc (Suc i) * m a (v - Suc 0)) * ({{C i (Dec a e)}} * <(j = i + 1)>) * r" |
|
330 by (metis stimes_ac) |
|
331 from condD1[OF this] |
|
332 have "rset_of ?y \<in> (pc (Suc i) * m a (v - Suc 0)) * ({{C i (Dec a e)}} * <(j = i + 1)>) * r" . |
|
333 thus ?thesis |
|
334 by (unfold h2(2) assemble_to.simps, simp) |
|
335 qed |
|
336 with stp show ?thesis by simp |
|
337 qed |
|
338 thus ?thesis by blast |
|
339 qed |
|
340 qed |
|
341 |
|
342 lemma hoare_dec_fail: "{pc i * m a 0} |
|
343 i:[ \<guillemotright>(Dec a e) ]:j |
|
344 {pc e * m a 0}" |
|
345 proof(unfold Hoare_abc_def, clarify) |
|
346 fix prog i' ab b r |
|
347 assume h: "rset_of (prog, i', ab, b) \<in> (pc i * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r" |
|
348 (is "?r \<in> ?S") |
|
349 show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> (pc e * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r" |
|
350 proof - |
|
351 from h [unfolded assemble_to.simps] |
|
352 have h1: "?r \<in> pc i * {{C i (Dec a e)}} * m a 0 * <(j = i + 1)> * r" |
|
353 "?r \<in> m a 0 * pc i * {{C i (Dec a e)}} * <(j = i + 1)> * r" |
|
354 "?r \<in> <(j = i + 1)> * m a 0 * pc i * {{C i (Dec a e)}} * r" |
|
355 by ((metis stimes_ac)+) |
|
356 note h2 = condD [OF h1(3)] pcD[OF h1(1)] codeD[OF h1(1)] memD[OF h1(2)] |
|
357 hence stp: "run 1 (prog, i', ab, b) = (prog, e, ab, b)" (is "?x = ?y") |
|
358 by (unfold run_def, auto) |
|
359 have "rset_of ?x \<in> (pc e * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r" |
|
360 proof - |
|
361 have "rset_of ?y \<in> (pc e * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r" |
|
362 proof - |
|
363 from spc_upd[OF h1(1), of "e"] |
|
364 have "rset_of ?y \<in> pc e * {{C i (Dec a e)}} * m a 0 * <(j = i + 1)> * r" . |
|
365 thus ?thesis |
|
366 by (unfold assemble_to.simps, metis stimes_ac) |
|
367 qed |
|
368 with stp show ?thesis by simp |
|
369 qed |
|
370 thus ?thesis by blast |
|
371 qed |
|
372 qed |
|
373 |
|
374 lemma pasrtD_p: "\<lbrakk>{p*<b>} c {q}\<rbrakk> \<Longrightarrow> (b \<longrightarrow> {p} c {q})" |
|
375 apply (unfold Hoare_abc_def pasrt_def, auto) |
|
376 by (fold emp_def, simp add:emp_unit_r) |
|
377 |
|
378 lemma hoare_dec: "dec_fun v j e = (pc', v') \<Longrightarrow> |
|
379 {pc i * m a v} |
|
380 i:[ \<guillemotright>(Dec a e) ]:j |
|
381 {pc pc' * m a v'}" |
|
382 proof - |
|
383 assume "dec_fun v j e = (pc', v')" |
|
384 thus "{pc i * m a v} |
|
385 i:[ \<guillemotright>(Dec a e) ]:j |
|
386 {pc pc' * m a v'}" |
|
387 apply (auto split:if_splits simp:dec_fun_def) |
|
388 apply (insert hoare_dec_fail, auto)[1] |
|
389 apply (insert hoare_dec_suc, auto) |
|
390 apply (atomize) |
|
391 apply (erule_tac x = i in allE, erule_tac x = a in allE, |
|
392 erule_tac x = v in allE, erule_tac x = e in allE, erule_tac x = pc' in allE) |
|
393 by (drule_tac pasrtD_p, clarify) |
|
394 qed |
|
395 |
|
396 lemma hoare_inc: "{pc i * m a v} |
|
397 i:[ \<guillemotright>(Inc a) ]:j |
|
398 {pc j * m a (v + 1)}" |
|
399 proof(unfold Hoare_abc_def, clarify) |
|
400 fix prog i' ab b r |
|
401 assume h: "rset_of (prog, i', ab, b) \<in> (pc i * m a v) * (i :[ \<guillemotright>Inc a ]: j) * r" |
|
402 (is "?r \<in> ?S") |
|
403 show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> (pc j * m a (v + 1)) * (i :[ \<guillemotright>Inc a ]: j) * r" |
|
404 proof - |
|
405 from h [unfolded assemble_to.simps] |
|
406 have h1: "?r \<in> pc i * {{C i (Inc a)}} * m a v * <(j = i + 1)> * r" |
|
407 "?r \<in> m a v * pc i * {{C i (Inc a)}} * <(j = i + 1)> * r" |
|
408 "?r \<in> <(j = i + 1)> * m a v * pc i * {{C i (Inc a)}} * r" |
|
409 by ((metis stimes_ac)+) |
|
410 note h2 = condD [OF h1(3)] pcD[OF h1(1)] codeD[OF h1(1)] memD[OF h1(2)] |
|
411 hence stp: "run 1 (prog, i', ab, b) = (prog, Suc i, ab(a \<mapsto> Suc v), b)" (is "?x = ?y") |
|
412 by (unfold run_def, auto) |
|
413 have "rset_of ?x \<in> (pc j * m a (v + 1)) * (i :[ \<guillemotright>Inc a]: j) * r" |
|
414 proof - |
|
415 have "rset_of ?y \<in> (pc j * m a (v + 1)) * (i :[ \<guillemotright>Inc a ]: j) * r" |
|
416 proof - |
|
417 from spc_upd[OF h1(1), of "Suc i"] |
|
418 have "rset_of (prog, (Suc i), ab, b) \<in> |
|
419 m a v * pc (Suc i) * {{C i (Inc a)}} * <(j = i + 1)> * r" |
|
420 by (metis stimes_ac) |
|
421 from smem_upd[OF this, of "Suc v"] |
|
422 have "rset_of ?y \<in> |
|
423 m a (v + 1) * pc (i + 1) * {{C i (Inc a)}} * <(j = i + 1)> * r" by simp |
|
424 thus ?thesis |
|
425 by (unfold h2(1) assemble_to.simps, metis stimes_ac) |
|
426 qed |
|
427 with stp show ?thesis by simp |
|
428 qed |
|
429 thus ?thesis by blast |
|
430 qed |
|
431 qed |
|
432 |
|
433 lemma hoare_goto: "{pc i} |
|
434 i:[ \<guillemotright>(Goto e) ]:j |
|
435 {pc e}" |
|
436 proof(unfold Hoare_abc_def, clarify) |
|
437 fix prog i' ab b r |
|
438 assume h: "rset_of (prog, i', ab, b) \<in> pc i * (i :[ \<guillemotright>Goto e ]: j) * r" |
|
439 (is "?r \<in> ?S") |
|
440 show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> pc e * (i :[ \<guillemotright>Goto e ]: j) * r" |
|
441 proof - |
|
442 from h [unfolded assemble_to.simps] |
|
443 have h1: "?r \<in> pc i * {{C i (Goto e)}} * <(j = i + 1)> * r" |
|
444 by ((metis stimes_ac)+) |
|
445 note h2 = pcD[OF h1(1)] codeD[OF h1(1)] |
|
446 hence stp: "run 1 (prog, i', ab, b) = (prog, e, ab, b)" (is "?x = ?y") |
|
447 by (unfold run_def, auto) |
|
448 have "rset_of ?x \<in> pc e * (i :[ \<guillemotright>Goto e]: j) * r" |
|
449 proof - |
|
450 from spc_upd[OF h1(1), of "e"] |
|
451 show ?thesis |
|
452 by (unfold stp assemble_to.simps, metis stimes_ac) |
|
453 qed |
|
454 thus ?thesis by blast |
|
455 qed |
|
456 qed |
|
457 |
|
458 no_notation stimes (infixr "*" 70) |
|
459 |
|
460 interpretation foo: comm_monoid_mult |
|
461 "stimes :: 'a set set => 'a set set => 'a set set" "emp::'a set set" |
|
462 apply(default) |
|
463 apply(simp add: stimes_assoc) |
|
464 apply(simp add: stimes_comm) |
|
465 apply(simp add: emp_def[symmetric]) |
|
466 done |
|
467 |
|
468 |
|
469 notation stimes (infixr "*" 70) |
|
470 |
|
471 (*used by simplifier for numbers *) |
|
472 thm mult_cancel_left |
|
473 |
|
474 (* |
|
475 interpretation foo: comm_ring_1 "op * :: 'a set set => 'a set set => 'a set set" "{{}}::'a set set" |
|
476 apply(default) |
|
477 *) |
|
478 |
|
479 lemma frame: "{p} c {q} \<Longrightarrow> \<forall> r. {p * r} c {q * r}" |
|
480 apply (unfold Hoare_abc_def, clarify) |
|
481 apply (erule_tac x = "(a, aa, ab, b)" in allE) |
|
482 apply (erule_tac x = "r * ra" in allE) |
|
483 apply(metis stimes_ac) |
|
484 done |
|
485 |
|
486 lemma code_extension: "\<lbrakk>{p} c {q}\<rbrakk> \<Longrightarrow> (\<forall> e. {p} c * e {q})" |
|
487 apply (unfold Hoare_abc_def, clarify) |
|
488 apply (erule_tac x = "(a, aa, ab, b)" in allE) |
|
489 apply (erule_tac x = "e * r" in allE) |
|
490 apply(metis stimes_ac) |
|
491 done |
|
492 |
|
493 lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)" |
|
494 apply (unfold run_def) |
|
495 by (metis funpow_add o_apply) |
|
496 |
|
497 lemma composition: "\<lbrakk>{p} c1 {q}; {q} c2 {r}\<rbrakk> \<Longrightarrow> {p} c1 * c2 {r}" |
|
498 proof - |
|
499 assume h: "{p} c1 {q}" "{q} c2 {r}" |
|
500 from code_extension [OF h(1), rule_format, of "c2"] |
|
501 have "{p} c1 * c2 {q}" . |
|
502 moreover from code_extension [OF h(2), rule_format, of "c1"] and stimes_comm |
|
503 have "{q} c1 * c2 {r}" by metis |
|
504 ultimately show "{p} c1 * c2 {r}" |
|
505 apply (unfold Hoare_abc_def, clarify) |
|
506 proof - |
|
507 fix a aa ab b ra |
|
508 assume h1: "\<forall>s r. rset_of s \<in> p * (c1 * c2) * r \<longrightarrow> |
|
509 (\<exists>k. rset_of (run k s) \<in> q * (c1 * c2) * r)" |
|
510 and h2: "\<forall>s ra. rset_of s \<in> q * (c1 * c2) * ra \<longrightarrow> |
|
511 (\<exists>k. rset_of (run k s) \<in> r * (c1 * c2) * ra)" |
|
512 and h3: "rset_of (a, aa, ab, b) \<in> p * (c1 * c2) * ra" |
|
513 show "\<exists>k. rset_of (run k (a, aa, ab, b)) \<in> r * (c1 * c2) * ra" |
|
514 proof - |
|
515 let ?s = "(a, aa, ab, b)" |
|
516 from h1 [rule_format, of ?s, OF h3] |
|
517 obtain n1 where "rset_of (run n1 ?s) \<in> q * (c1 * c2) * ra" by blast |
|
518 from h2 [rule_format, OF this] |
|
519 obtain n2 where "rset_of (run n2 (run n1 ?s)) \<in> r * (c1 * c2) * ra" by blast |
|
520 with run_add show ?thesis by metis |
|
521 qed |
|
522 qed |
|
523 qed |
|
524 |
|
525 lemma stimes_simp: "s \<in> x * y = (\<exists> s1 s2. (s = s1 \<union> s2 \<and> s1 \<inter> s2 = {} \<and> s1 \<in> x \<and> s2 \<in> y))" |
|
526 by (metis (lifting) stimesE stimesI) |
|
527 |
|
528 lemma hoare_seq: |
|
529 "\<lbrakk>\<forall> i j. {pc i * p} i:[c1]:j {pc j * q}; |
|
530 \<forall> j k. {pc j * q} j:[c2]:k {pc k * r}\<rbrakk> \<Longrightarrow> {pc i * p} i:[(c1 ; c2)]:k {pc k *r}" |
|
531 proof - |
|
532 assume h: "\<forall>i j. {pc i * p} i :[ c1 ]: j {pc j * q}" "\<forall> j k. {pc j * q} j:[c2]:k {pc k * r}" |
|
533 show "{pc i * p} i:[(c1 ; c2)]:k {pc k *r}" |
|
534 proof(subst Hoare_abc_def, clarify) |
|
535 fix a aa ab b ra |
|
536 assume "rset_of (a, aa, ab, b) \<in> (pc i * p) * (i :[ (c1 ; c2) ]: k) * ra" |
|
537 hence "rset_of (a, aa, ab, b) \<in> (i :[ (c1 ; c2) ]: k) * (pc i * p * ra)" (is "?s \<in> ?X * ?Y") |
|
538 by (metis stimes_ac) |
|
539 from stimesE[OF this] obtain s1 s2 where |
|
540 sp: "rset_of(a, aa, ab, b) = s1 \<union> s2" "s1 \<inter> s2 = {}" "s1 \<in> ?X" "s2 \<in> ?Y" by blast |
|
541 from sp (3) obtain j' where |
|
542 "s1 \<in> (i:[c1]:j') * (j':[c2]:k)" (is "s1 \<in> ?Z") |
|
543 by (auto simp:assemble_to.simps) |
|
544 from stimesI[OF sp(1, 2) this sp(4)] |
|
545 have "?s \<in> (pc i * p) * (i :[ c1 ]: j') * (j' :[ c2 ]: k) * ra" by (metis stimes_ac) |
|
546 from h(1)[unfolded Hoare_abc_def, rule_format, OF this] |
|
547 obtain ka where |
|
548 "rset_of (run ka (a, aa, ab, b)) \<in> (pc j' * q) * (j' :[ c2 ]: k) * ((i :[ c1 ]: j') * ra)" |
|
549 sorry |
|
550 from h(2)[unfolded Hoare_abc_def, rule_format, OF this] |
|
551 obtain kb where |
|
552 "rset_of (run kb (run ka (a, aa, ab, b))) |
|
553 \<in> (pc k * r) * (j' :[ c2 ]: k) * (i :[ c1 ]: j') * ra" by blast |
|
554 hence h3: "rset_of (run (kb + ka) (a, aa, ab, b)) |
|
555 \<in> pc k * r * (j' :[ c2 ]: k) * ((i :[ c1 ]: j') * ra)" |
|
556 sorry |
|
557 hence "rset_of (run (kb + ka) (a, aa, ab, b)) \<in> pc k * r * (i :[ (c1 ; c2) ]: k) * ra" |
|
558 proof - |
|
559 have "rset_of (run (kb + ka) (a, aa, ab, b)) \<in> (i :[ (c1 ; c2) ]: k) * (pc k * r * ra)" |
|
560 proof - |
|
561 from h3 have "rset_of (run (kb + ka) (a, aa, ab, b)) |
|
562 \<in> ((j' :[ c2 ]: k) * ((i :[ c1 ]: j'))) * (pc k * r * ra)" |
|
563 by (metis stimes_ac) |
|
564 then obtain |
|
565 s1 s2 where h4: "rset_of (run (kb + ka) (a, aa, ab, b)) = s1 \<union> s2" |
|
566 " s1 \<inter> s2 = {}" "s1 \<in> (j' :[ c2 ]: k) * (i :[ c1 ]: j')" |
|
567 "s2 \<in> pc k * r * ra" by (rule stimesE, blast) |
|
568 from h4(3) have "s1 \<in> (i :[ (c1 ; c2) ]: k)" |
|
569 sorry |
|
570 from stimesI [OF h4(1, 2) this h4(4)] |
|
571 show ?thesis . |
|
572 qed |
|
573 thus ?thesis by (metis stimes_ac) |
|
574 qed |
|
575 thus "\<exists>ka. rset_of (run ka (a, aa, ab, b)) \<in> (pc k * r) * (i :[ (c1 ; c2) ]: k) * ra" |
|
576 by (metis stimes_ac) |
|
577 qed |
|
578 qed |
|
579 |
|
580 lemma hoare_local: |
|
581 "\<forall> l i j. {pc i*p} i:[c(l)]:j {pc j * q} |
|
582 \<Longrightarrow> {pc i * p} i:[Local c]:j {pc j * q}" |
|
583 proof - |
|
584 assume h: "\<forall> l i j. {pc i*p} i:[c(l)]:j {pc j * q} " |
|
585 show "{pc i * p} i:[Local c]:j {pc j * q}" |
|
586 proof(unfold assemble_to.simps Hoare_abc_def, clarify) |
|
587 fix a aa ab b r |
|
588 assume h1: "rset_of (a, aa, ab, b) \<in> (pc i * p) * (\<Union>l. i :[ c l ]: j) * r" |
|
589 hence "rset_of (a, aa, ab, b) \<in> (\<Union>l. i :[ c l ]: j) * (pc i * p * r)" |
|
590 by (metis stimes_ac) |
|
591 then obtain s1 s2 l |
|
592 where "rset_of (a, aa, ab, b) = s1 \<union> s2" |
|
593 "s1 \<inter> s2 = {}" |
|
594 "s1 \<in> (i :[ c l ]: j)" |
|
595 "s2 \<in> pc i * p * r" |
|
596 by (rule stimesE, auto) |
|
597 from stimesI[OF this] |
|
598 have "rset_of (a, aa, ab, b) \<in> (pc i * p) * (i :[ c l ]: j) * r" |
|
599 by (metis stimes_ac) |
|
600 from h[unfolded Hoare_abc_def, rule_format, OF this] |
|
601 obtain k where "rset_of (run k (a, aa, ab, b)) \<in> (i :[ c l ]: j) * (pc j * q * r)" |
|
602 sorry |
|
603 then obtain s1 s2 |
|
604 where h3: "rset_of (run k (a, aa, ab, b)) = s1 \<union> s2" |
|
605 " s1 \<inter> s2 = {}" "s1 \<in> (\<Union> l. (i :[ c l ]: j))" "s2 \<in> pc j * q * r" |
|
606 by(rule stimesE, auto) |
|
607 from stimesI[OF this] |
|
608 show "\<exists>k. rset_of (run k (a, aa, ab, b)) \<in> (pc j * q) * (\<Union>l. i :[ c l ]: j) * r" |
|
609 by (metis stimes_ac) |
|
610 qed |
|
611 qed |
|
612 |
|
613 lemma move_pure: "{p*<b>} c {q} = (b \<longrightarrow> {p} c {q})" |
|
614 proof(unfold Hoare_abc_def, default, clarify) |
|
615 fix prog i' mem ft r |
|
616 assume h: "\<forall>s r. rset_of s \<in> (p * <b>) * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)" |
|
617 "b" "rset_of (prog, i', mem, ft) \<in> p * c * r" |
|
618 show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * c * r" |
|
619 proof(rule h(1)[rule_format]) |
|
620 have "(p * <b>) * c * r = <b> * p * c * r" by (metis stimes_ac) |
|
621 moreover have "rset_of (prog, i', mem, ft) \<in> \<dots>" |
|
622 proof(rule stimesI[OF _ _ _ h(3)]) |
|
623 from h(2) show "{} \<in> <b>" by (auto simp:pasrt_def) |
|
624 qed auto |
|
625 ultimately show "rset_of (prog, i', mem, ft) \<in> (p * <b>) * c * r" |
|
626 by (simp) |
|
627 qed |
|
628 next |
|
629 assume h: "b \<longrightarrow> (\<forall>s r. rset_of s \<in> p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r))" |
|
630 show "\<forall>s r. rset_of s \<in> (p * <b>) * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)" |
|
631 proof - |
|
632 { fix s r |
|
633 assume "rset_of s \<in> (p * <b>) * c * r" |
|
634 hence h1: "rset_of s \<in> <b> * p * c * r" by (metis stimes_ac) |
|
635 have "(\<exists>k. rset_of (run k s) \<in> q * c * r)" |
|
636 proof(rule h[rule_format]) |
|
637 from condD[OF h1] show b . |
|
638 next |
|
639 from condD1[OF h1] show "rset_of s \<in> p * c * r" . |
|
640 qed |
|
641 } thus ?thesis by blast |
|
642 qed |
|
643 qed |
|
644 |
|
645 lemma precond_ex: "{\<Union> x. p x} c {q} = (\<forall> x. {p x} c {q})" |
|
646 proof(unfold Hoare_abc_def, default, clarify) |
|
647 fix x prog i' mem ft r |
|
648 assume h: "\<forall>s r. rset_of s \<in> UNION UNIV p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)" |
|
649 "rset_of (prog, i', mem, ft) \<in> p x * c * r" |
|
650 show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * c * r" |
|
651 proof(rule h[rule_format]) |
|
652 from h(2) show "rset_of (prog, i', mem, ft) \<in> UNION UNIV p * c * r" by (auto simp:stimes_def) |
|
653 qed |
|
654 next |
|
655 assume h: "\<forall>x s r. rset_of s \<in> p x * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)" |
|
656 show "\<forall>s r. rset_of s \<in> UNION UNIV p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)" |
|
657 proof - |
|
658 { fix s r |
|
659 assume "rset_of s \<in> UNION UNIV p * c * r" |
|
660 then obtain x where "rset_of s \<in> p x * c * r" |
|
661 by (unfold st_def, auto, metis) |
|
662 hence "(\<exists>k. rset_of (run k s) \<in> q * c * r)" |
|
663 by(rule h[rule_format]) |
|
664 } thus ?thesis by blast |
|
665 qed |
|
666 qed |
|
667 |
|
668 lemma code_exI: "\<lbrakk>\<And>l. {p} c l * c' {q}\<rbrakk> \<Longrightarrow> {p} (\<Union> l. c l) * c' {q}" |
|
669 proof(unfold Hoare_abc_def, default, clarify) |
|
670 fix prog i' mem ft r |
|
671 assume h: "\<And>l. \<forall>s r. rset_of s \<in> p * (c l * c') * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * (c l * c') * r)" |
|
672 "rset_of (prog, i', mem, ft) \<in> p * (UNION UNIV c * c') * r" |
|
673 show " \<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * (UNION UNIV c * c') * r" |
|
674 proof - |
|
675 from h(2) obtain l where "rset_of (prog, i', mem, ft) \<in> p * (c l * c') * r" |
|
676 apply (unfold st_def, auto) |
|
677 by metis |
|
678 from h(1)[rule_format, OF this] |
|
679 obtain k where " rset_of (run k (prog, i', mem, ft)) \<in> q * (c l * c') * r" by blast |
|
680 thus ?thesis by (unfold st_def, auto, metis) |
|
681 qed |
|
682 qed |
|
683 |
|
684 lemma code_exIe: "\<lbrakk>\<And>l. {p} c l{q}\<rbrakk> \<Longrightarrow> {p} \<Union> l. (c l) {q}" |
|
685 proof - |
|
686 assume "\<And>l. {p} c l {q}" |
|
687 thus "{p} \<Union>l. c l {q}" |
|
688 by(rule code_exI[where c'= "emp", unfolded emp_unit_r]) |
|
689 qed |
|
690 |
|
691 lemma pre_stren: "\<lbrakk>{p} c {q}; r \<subseteq> p\<rbrakk> \<Longrightarrow> {r} c {q}" |
|
692 proof(unfold Hoare_abc_def, clarify) |
|
693 fix prog i' mem ft r' |
|
694 assume h: "\<forall>s r. rset_of s \<in> p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)" |
|
695 " r \<subseteq> p" " rset_of (prog, i', mem, ft) \<in> r * c * r'" |
|
696 show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * c * r'" |
|
697 proof(rule h(1)[rule_format]) |
|
698 from stimes_mono[OF h(2), of "c * r'"] h(3) |
|
699 show "rset_of (prog, i', mem, ft) \<in> p * c * r'" by auto |
|
700 qed |
|
701 qed |
|
702 |
|
703 lemma post_weaken: "\<lbrakk>{p} c {q}; q \<subseteq> r\<rbrakk> \<Longrightarrow> {p} c {r}" |
|
704 proof(unfold Hoare_abc_def, clarify) |
|
705 fix prog i' mem ft r' |
|
706 assume h: "\<forall>s r. rset_of s \<in> p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)" |
|
707 " q \<subseteq> r" "rset_of (prog, i', mem, ft) \<in> p * c * r'" |
|
708 show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> r * c * r'" |
|
709 proof - |
|
710 from h(1)[rule_format, OF h(3)] |
|
711 obtain k where "rset_of (run k (prog, i', mem, ft)) \<in> q * c * r'" by auto |
|
712 moreover from h(2) have "\<dots> \<subseteq> r * c * r'" by (metis stimes_mono) |
|
713 ultimately show ?thesis by auto |
|
714 qed |
|
715 qed |
|
716 |
|
717 definition "clear a = |
|
718 Local (\<lambda> start. (Local (\<lambda> exit. Label start; \<guillemotright>Dec a exit; \<guillemotright> Goto start; Label exit)))" |
|
719 |
|
720 lemma "{pc i * m a v} i:[clear a]:j {pc j*m a 0}" |
|
721 proof (unfold clear_def, rule hoare_local, default+) |
|
722 fix l i j |
|
723 show "{pc i * m a v} i :[ Local (\<lambda>exit. Label l ; \<guillemotright>Dec a exit ; \<guillemotright>Goto l ; Label exit) ]: j |
|
724 {pc j * m a 0}" |
|
725 proof(rule hoare_local, default+) |
|
726 fix la i j |
|
727 show "{pc i * m a v} i :[ (Label l ; \<guillemotright>Dec a la ; \<guillemotright>Goto l ; Label la) ]: j {pc j * m a 0}" |
|
728 proof(subst assemble_to.simps, rule code_exIe) |
|
729 have "\<And>j'. {pc i * m a v} (j' :[ (\<guillemotright>Dec a la ; \<guillemotright>Goto l ; Label la) ]: j) * (i :[ Label l ]: j') |
|
730 {pc j * m a 0}" |
|
731 proof(subst assemble_to.simps, rule code_exI) |
|
732 fix j' j'a |
|
733 show "{pc i * m a v} |
|
734 ((j' :[ \<guillemotright>Dec a la ]: j'a) * (j'a :[ (\<guillemotright>Goto l ; Label la) ]: j)) * (i :[ Label l ]: j') |
|
735 {pc j * m a 0}" |
|
736 proof(unfold assemble_to.simps) |
|
737 have "{pc i * m a v} |
|
738 ((\<Union>j'. ({{C j'a (Goto l)}} * <(j' = j'a + 1)>) * ({{C j' (Dec a la)}} * <(j'a = j' + 1)>) |
|
739 * <(j' = j \<and> j = la)>)) * |
|
740 <(i = j' \<and> j' = l)> |
|
741 {pc j * m a 0}" |
|
742 proof(rule code_exI, fold assemble_to.simps) |
|
743 qed |
|
744 thus "{pc i * m a v} |
|
745 (({{C j' (Dec a la)}} * <(j'a = j' + 1)>) * |
|
746 (\<Union>j'. ({{C j'a (Goto l)}} * <(j' = j'a + 1)>) * <(j' = j \<and> j = la)>)) * |
|
747 <(i = j' \<and> j' = l)> |
|
748 {pc j * m a 0}" sorry |
|
749 qed |
|
750 qed |
|
751 thus "\<And>j'. {pc i * m a v} (i :[ Label l ]: j') * (j' :[ (\<guillemotright>Dec a la ; \<guillemotright>Goto l ; Label la) ]: j) |
|
752 {pc j * m a 0}" by (metis stimes_ac) |
|
753 qed |
|
754 qed |
|
755 qed |
|
756 |
|
757 end |