|
1 theory Abacus_Hoare |
|
2 imports Abacus |
|
3 begin |
|
4 |
|
5 type_synonym abc_assert = "nat list \<Rightarrow> bool" |
|
6 |
|
7 definition |
|
8 assert_imp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100) |
|
9 where |
|
10 "assert_imp P Q \<equiv> \<forall>xs. P xs \<longrightarrow> Q xs" |
|
11 |
|
12 fun abc_holds_for :: "(nat list \<Rightarrow> bool) \<Rightarrow> (nat \<times> nat list) \<Rightarrow> bool" ("_ abc'_holds'_for _" [100, 99] 100) |
|
13 where |
|
14 "P abc_holds_for (s, lm) = P lm" |
|
15 |
|
16 (* Hoare Rules *) |
|
17 (* halting case *) |
|
18 (*consts abc_Hoare_halt :: "abc_assert \<Rightarrow> abc_prog \<Rightarrow> abc_assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)*) |
|
19 |
|
20 fun abc_final :: "(nat \<times> nat list) \<Rightarrow> abc_prog \<Rightarrow> bool" |
|
21 where |
|
22 "abc_final (s, lm) p = (s = length p)" |
|
23 |
|
24 fun abc_notfinal :: "abc_conf \<Rightarrow> abc_prog \<Rightarrow> bool" |
|
25 where |
|
26 "abc_notfinal (s, lm) p = (s < length p)" |
|
27 |
|
28 definition |
|
29 abc_Hoare_halt :: "abc_assert \<Rightarrow> abc_prog \<Rightarrow> abc_assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
|
30 where |
|
31 "abc_Hoare_halt P p Q \<equiv> \<forall>lm. P lm \<longrightarrow> (\<exists>n. abc_final (abc_steps_l (0, lm) p n) p \<and> Q abc_holds_for (abc_steps_l (0, lm) p n))" |
|
32 |
|
33 lemma abc_Hoare_haltI: |
|
34 assumes "\<And>lm. P lm \<Longrightarrow> \<exists>n. abc_final (abc_steps_l (0, lm) p n) p \<and> Q abc_holds_for (abc_steps_l (0, lm) p n)" |
|
35 shows "{P} (p::abc_prog) {Q}" |
|
36 unfolding abc_Hoare_halt_def |
|
37 using assms by auto |
|
38 |
|
39 text {* |
|
40 {P} A {Q} {Q} B {S} |
|
41 ----------------------------------------- |
|
42 {P} A [+] B {S} |
|
43 *} |
|
44 |
|
45 definition |
|
46 abc_Hoare_unhalt :: "abc_assert \<Rightarrow> abc_prog \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" 50) |
|
47 where |
|
48 "abc_Hoare_unhalt P p \<equiv> \<forall>args. P args \<longrightarrow> (\<forall> n .abc_notfinal (abc_steps_l (0, args) p n) p)" |
|
49 |
|
50 lemma abc_Hoare_unhaltI: |
|
51 assumes "\<And>args n. P args \<Longrightarrow> abc_notfinal (abc_steps_l (0, args) p n) p" |
|
52 shows "{P} (p::abc_prog) \<up>" |
|
53 unfolding abc_Hoare_unhalt_def |
|
54 using assms by auto |
|
55 |
|
56 fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst" |
|
57 where |
|
58 "abc_inst_shift (Inc m) n = Inc m" | |
|
59 "abc_inst_shift (Dec m e) n = Dec m (e + n)" | |
|
60 "abc_inst_shift (Goto m) n = Goto (m + n)" |
|
61 |
|
62 fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list" |
|
63 where |
|
64 "abc_shift xs n = map (\<lambda> x. abc_inst_shift x n) xs" |
|
65 |
|
66 fun abc_comp :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow> |
|
67 abc_inst list" (infixl "[+]" 99) |
|
68 where |
|
69 "abc_comp al bl = (let al_len = length al in |
|
70 al @ abc_shift bl al_len)" |
|
71 |
|
72 lemma abc_comp_first_step_eq_pre: |
|
73 "s < length A |
|
74 \<Longrightarrow> abc_step_l (s, lm) (abc_fetch s (A [+] B)) = |
|
75 abc_step_l (s, lm) (abc_fetch s A)" |
|
76 by(simp add: abc_step_l.simps abc_fetch.simps nth_append) |
|
77 |
|
78 lemma abc_before_final: |
|
79 "\<lbrakk>abc_final (abc_steps_l (0, lm) p n) p; p \<noteq> []\<rbrakk> |
|
80 \<Longrightarrow> \<exists> n'. abc_notfinal (abc_steps_l (0, lm) p n') p \<and> |
|
81 abc_final (abc_steps_l (0, lm) p (Suc n')) p" |
|
82 proof(induct n) |
|
83 case 0 |
|
84 thus "?thesis" |
|
85 by(simp add: abc_steps_l.simps) |
|
86 next |
|
87 case (Suc n) |
|
88 have ind: " \<lbrakk>abc_final (abc_steps_l (0, lm) p n) p; p \<noteq> []\<rbrakk> \<Longrightarrow> |
|
89 \<exists>n'. abc_notfinal (abc_steps_l (0, lm) p n') p \<and> abc_final (abc_steps_l (0, lm) p (Suc n')) p" |
|
90 by fact |
|
91 have final: "abc_final (abc_steps_l (0, lm) p (Suc n)) p" by fact |
|
92 have notnull: "p \<noteq> []" by fact |
|
93 show "?thesis" |
|
94 proof(cases "abc_final (abc_steps_l (0, lm) p n) p") |
|
95 case True |
|
96 have "abc_final (abc_steps_l (0, lm) p n) p" by fact |
|
97 then have "\<exists>n'. abc_notfinal (abc_steps_l (0, lm) p n') p \<and> abc_final (abc_steps_l (0, lm) p (Suc n')) p" |
|
98 using ind notnull |
|
99 by simp |
|
100 thus "?thesis" |
|
101 by simp |
|
102 next |
|
103 case False |
|
104 have "\<not> abc_final (abc_steps_l (0, lm) p n) p" by fact |
|
105 from final this have "abc_notfinal (abc_steps_l (0, lm) p n) p" |
|
106 by(case_tac "abc_steps_l (0, lm) p n", simp add: abc_step_red2 |
|
107 abc_step_l.simps abc_fetch.simps split: if_splits) |
|
108 thus "?thesis" |
|
109 using final |
|
110 by(rule_tac x = n in exI, simp) |
|
111 qed |
|
112 qed |
|
113 |
|
114 lemma notfinal_Suc: |
|
115 "abc_notfinal (abc_steps_l (0, lm) A (Suc n)) A \<Longrightarrow> |
|
116 abc_notfinal (abc_steps_l (0, lm) A n) A" |
|
117 apply(case_tac "abc_steps_l (0, lm) A n") |
|
118 apply(simp add: abc_step_red2 abc_fetch.simps abc_step_l.simps split: if_splits) |
|
119 done |
|
120 |
|
121 lemma abc_comp_frist_steps_eq_pre: |
|
122 assumes notfinal: "abc_notfinal (abc_steps_l (0, lm) A n) A" |
|
123 and notnull: "A \<noteq> []" |
|
124 shows "abc_steps_l (0, lm) (A [+] B) n = abc_steps_l (0, lm) A n" |
|
125 using notfinal |
|
126 proof(induct n) |
|
127 case 0 |
|
128 thus "?case" |
|
129 by(simp add: abc_steps_l.simps) |
|
130 next |
|
131 case (Suc n) |
|
132 have ind: "abc_notfinal (abc_steps_l (0, lm) A n) A \<Longrightarrow> abc_steps_l (0, lm) (A [+] B) n = abc_steps_l (0, lm) A n" |
|
133 by fact |
|
134 have h: "abc_notfinal (abc_steps_l (0, lm) A (Suc n)) A" by fact |
|
135 then have a: "abc_notfinal (abc_steps_l (0, lm) A n) A" |
|
136 by(simp add: notfinal_Suc) |
|
137 then have b: "abc_steps_l (0, lm) (A [+] B) n = abc_steps_l (0, lm) A n" |
|
138 using ind by simp |
|
139 obtain s lm' where c: "abc_steps_l (0, lm) A n = (s, lm')" |
|
140 by (metis prod.exhaust) |
|
141 then have d: "s < length A \<and> abc_steps_l (0, lm) (A [+] B) n = (s, lm')" |
|
142 using a b by simp |
|
143 thus "?case" |
|
144 using c |
|
145 by(simp add: abc_step_red2 abc_fetch.simps abc_step_l.simps nth_append) |
|
146 qed |
|
147 |
|
148 declare abc_shift.simps[simp del] abc_comp.simps[simp del] |
|
149 lemma halt_steps2: "st \<ge> length A \<Longrightarrow> abc_steps_l (st, lm) A stp = (st, lm)" |
|
150 apply(induct stp) |
|
151 by(simp_all add: abc_step_red2 abc_steps_l.simps abc_step_l.simps abc_fetch.simps) |
|
152 |
|
153 lemma halt_steps: "abc_steps_l (length A, lm) A n = (length A, lm)" |
|
154 apply(induct n, simp add: abc_steps_l.simps) |
|
155 apply(simp add: abc_step_red2 abc_step_l.simps nth_append abc_fetch.simps) |
|
156 done |
|
157 |
|
158 lemma abc_steps_add: |
|
159 "abc_steps_l (as, lm) ap (m + n) = |
|
160 abc_steps_l (abc_steps_l (as, lm) ap m) ap n" |
|
161 apply(induct m arbitrary: n as lm, simp add: abc_steps_l.simps) |
|
162 proof - |
|
163 fix m n as lm |
|
164 assume ind: |
|
165 "\<And>n as lm. abc_steps_l (as, lm) ap (m + n) = |
|
166 abc_steps_l (abc_steps_l (as, lm) ap m) ap n" |
|
167 show "abc_steps_l (as, lm) ap (Suc m + n) = |
|
168 abc_steps_l (abc_steps_l (as, lm) ap (Suc m)) ap n" |
|
169 apply(insert ind[of as lm "Suc n"], simp) |
|
170 apply(insert ind[of as lm "Suc 0"], simp add: abc_steps_l.simps) |
|
171 apply(case_tac "(abc_steps_l (as, lm) ap m)", simp) |
|
172 apply(simp add: abc_steps_l.simps) |
|
173 apply(case_tac "abc_step_l (a, b) (abc_fetch a ap)", |
|
174 simp add: abc_steps_l.simps) |
|
175 done |
|
176 qed |
|
177 |
|
178 lemma equal_when_halt: |
|
179 assumes exc1: "abc_steps_l (s, lm) A na = (length A, lma)" |
|
180 and exc2: "abc_steps_l (s, lm) A nb = (length A, lmb)" |
|
181 shows "lma = lmb" |
|
182 proof(cases "na > nb") |
|
183 case True |
|
184 then obtain d where "na = nb + d" |
|
185 by (metis add_Suc_right less_iff_Suc_add) |
|
186 thus "?thesis" using assms halt_steps |
|
187 by(simp add: abc_steps_add) |
|
188 next |
|
189 case False |
|
190 then obtain d where "nb = na + d" |
|
191 by (metis add.comm_neutral less_imp_add_positive nat_neq_iff) |
|
192 thus "?thesis" using assms halt_steps |
|
193 by(simp add: abc_steps_add) |
|
194 qed |
|
195 |
|
196 lemma abc_comp_frist_steps_halt_eq': |
|
197 assumes final: "abc_steps_l (0, lm) A n = (length A, lm')" |
|
198 and notnull: "A \<noteq> []" |
|
199 shows "\<exists> n'. abc_steps_l (0, lm) (A [+] B) n' = (length A, lm')" |
|
200 proof - |
|
201 have "\<exists> n'. abc_notfinal (abc_steps_l (0, lm) A n') A \<and> |
|
202 abc_final (abc_steps_l (0, lm) A (Suc n')) A" |
|
203 using assms |
|
204 by(rule_tac n = n in abc_before_final, simp_all) |
|
205 then obtain na where a: |
|
206 "abc_notfinal (abc_steps_l (0, lm) A na) A \<and> |
|
207 abc_final (abc_steps_l (0, lm) A (Suc na)) A" .. |
|
208 obtain sa lma where b: "abc_steps_l (0, lm) A na = (sa, lma)" |
|
209 by (metis prod.exhaust) |
|
210 then have c: "abc_steps_l (0, lm) (A [+] B) na = (sa, lma)" |
|
211 using a abc_comp_frist_steps_eq_pre[of lm A na B] assms |
|
212 by simp |
|
213 have d: "sa < length A" using b a by simp |
|
214 then have e: "abc_step_l (sa, lma) (abc_fetch sa (A [+] B)) = |
|
215 abc_step_l (sa, lma) (abc_fetch sa A)" |
|
216 by(rule_tac abc_comp_first_step_eq_pre) |
|
217 from a have "abc_steps_l (0, lm) A (Suc na) = (length A, lm')" |
|
218 using final equal_when_halt |
|
219 by(case_tac "abc_steps_l (0, lm) A (Suc na)" , simp) |
|
220 then have "abc_steps_l (0, lm) (A [+] B) (Suc na) = (length A, lm')" |
|
221 using a b c e |
|
222 by(simp add: abc_step_red2) |
|
223 thus "?thesis" |
|
224 by blast |
|
225 qed |
|
226 |
|
227 lemma abc_exec_null: "abc_steps_l sam [] n = sam" |
|
228 apply(cases sam) |
|
229 apply(induct n) |
|
230 apply(auto simp: abc_step_red2) |
|
231 apply(auto simp: abc_step_l.simps abc_steps_l.simps abc_fetch.simps) |
|
232 done |
|
233 |
|
234 lemma abc_comp_frist_steps_halt_eq: |
|
235 assumes final: "abc_steps_l (0, lm) A n = (length A, lm')" |
|
236 shows "\<exists> n'. abc_steps_l (0, lm) (A [+] B) n' = (length A, lm')" |
|
237 using final |
|
238 apply(case_tac "A = []") |
|
239 apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps abc_exec_null) |
|
240 apply(rule_tac abc_comp_frist_steps_halt_eq', simp_all) |
|
241 done |
|
242 |
|
243 lemma abc_comp_second_step_eq: |
|
244 assumes exec: "abc_step_l (s, lm) (abc_fetch s B) = (sa, lma)" |
|
245 shows "abc_step_l (s + length A, lm) (abc_fetch (s + length A) (A [+] B)) |
|
246 = (sa + length A, lma)" |
|
247 using assms |
|
248 apply(auto simp: abc_step_l.simps abc_fetch.simps nth_append abc_comp.simps abc_shift.simps split : if_splits ) |
|
249 apply(case_tac [!] "B ! s", auto simp: Let_def) |
|
250 done |
|
251 |
|
252 lemma abc_comp_second_steps_eq: |
|
253 assumes exec: "abc_steps_l (0, lm) B n = (sa, lm')" |
|
254 shows "abc_steps_l (length A, lm) (A [+] B) n = (sa + length A, lm')" |
|
255 using assms |
|
256 proof(induct n arbitrary: sa lm') |
|
257 case 0 |
|
258 thus "?case" |
|
259 by(simp add: abc_steps_l.simps) |
|
260 next |
|
261 case (Suc n) |
|
262 have ind: "\<And>sa lm'. abc_steps_l (0, lm) B n = (sa, lm') \<Longrightarrow> |
|
263 abc_steps_l (length A, lm) (A [+] B) n = (sa + length A, lm')" by fact |
|
264 have exec: "abc_steps_l (0, lm) B (Suc n) = (sa, lm')" by fact |
|
265 obtain sb lmb where a: " abc_steps_l (0, lm) B n = (sb, lmb)" |
|
266 by (metis prod.exhaust) |
|
267 then have "abc_steps_l (length A, lm) (A [+] B) n = (sb + length A, lmb)" |
|
268 using ind by simp |
|
269 moreover have "abc_step_l (sb + length A, lmb) (abc_fetch (sb + length A) (A [+] B)) = (sa + length A, lm') " |
|
270 using a exec abc_comp_second_step_eq |
|
271 by(simp add: abc_step_red2) |
|
272 ultimately show "?case" |
|
273 by(simp add: abc_step_red2) |
|
274 qed |
|
275 |
|
276 lemma length_abc_comp[simp, intro]: |
|
277 "length (A [+] B) = length A + length B" |
|
278 by(auto simp: abc_comp.simps abc_shift.simps) |
|
279 |
|
280 lemma abc_Hoare_plus_halt : |
|
281 assumes A_halt : "{P} (A::abc_prog) {Q}" |
|
282 and B_halt : "{Q} (B::abc_prog) {S}" |
|
283 shows "{P} (A [+] B) {S}" |
|
284 proof(rule_tac abc_Hoare_haltI) |
|
285 fix lm |
|
286 assume a: "P lm" |
|
287 then obtain na lma where |
|
288 "abc_final (abc_steps_l (0, lm) A na) A" |
|
289 and b: "abc_steps_l (0, lm) A na = (length A, lma)" |
|
290 and c: "Q abc_holds_for (length A, lma)" |
|
291 using A_halt unfolding abc_Hoare_halt_def |
|
292 by (metis (full_types) abc_final.simps abc_holds_for.simps prod.exhaust) |
|
293 have "\<exists> n. abc_steps_l (0, lm) (A [+] B) n = (length A, lma)" |
|
294 using abc_comp_frist_steps_halt_eq b |
|
295 by(simp) |
|
296 then obtain nx where h1: "abc_steps_l (0, lm) (A [+] B) nx = (length A, lma)" .. |
|
297 from c have "Q lma" |
|
298 using c unfolding abc_holds_for.simps |
|
299 by simp |
|
300 then obtain nb lmb where |
|
301 "abc_final (abc_steps_l (0, lma) B nb) B" |
|
302 and d: "abc_steps_l (0, lma) B nb = (length B, lmb)" |
|
303 and e: "S abc_holds_for (length B, lmb)" |
|
304 using B_halt unfolding abc_Hoare_halt_def |
|
305 by (metis (full_types) abc_final.simps abc_holds_for.simps prod.exhaust) |
|
306 have h2: "abc_steps_l (length A, lma) (A [+] B) nb = (length B + length A, lmb)" |
|
307 using d abc_comp_second_steps_eq |
|
308 by simp |
|
309 thus "\<exists>n. abc_final (abc_steps_l (0, lm) (A [+] B) n) (A [+] B) \<and> |
|
310 S abc_holds_for abc_steps_l (0, lm) (A [+] B) n" |
|
311 using h1 e |
|
312 by(rule_tac x = "nx + nb" in exI, simp add: abc_steps_add) |
|
313 qed |
|
314 |
|
315 lemma abc_unhalt_append_eq: |
|
316 assumes unhalt: "{P} (A::abc_prog) \<up>" |
|
317 and P: "P args" |
|
318 shows "abc_steps_l (0, args) (A [+] B) stp = abc_steps_l (0, args) A stp" |
|
319 proof(induct stp) |
|
320 case 0 |
|
321 thus "?case" |
|
322 by(simp add: abc_steps_l.simps) |
|
323 next |
|
324 case (Suc stp) |
|
325 have ind: "abc_steps_l (0, args) (A [+] B) stp = abc_steps_l (0, args) A stp" |
|
326 by fact |
|
327 obtain s nl where a: "abc_steps_l (0, args) A stp = (s, nl)" |
|
328 by (metis prod.exhaust) |
|
329 then have b: "s < length A" |
|
330 using unhalt P |
|
331 apply(auto simp: abc_Hoare_unhalt_def) |
|
332 by (metis abc_notfinal.simps) |
|
333 thus "?case" |
|
334 using a ind |
|
335 by(simp add: abc_step_red2 abc_step_l.simps abc_fetch.simps nth_append abc_comp.simps) |
|
336 qed |
|
337 |
|
338 lemma abc_Hoare_plus_unhalt1: |
|
339 "{P} (A::abc_prog) \<up> \<Longrightarrow> {P} (A [+] B) \<up>" |
|
340 apply(rule_tac abc_Hoare_unhaltI) |
|
341 apply(frule_tac args = args and B = B and stp = n in abc_unhalt_append_eq) |
|
342 apply(simp_all add: abc_Hoare_unhalt_def) |
|
343 apply(erule_tac x = args in allE, simp) |
|
344 apply(erule_tac x = n in allE) |
|
345 apply(case_tac "(abc_steps_l (0, args) A n)", simp) |
|
346 done |
|
347 |
|
348 |
|
349 lemma notfinal_all_before: |
|
350 "\<lbrakk>abc_notfinal (abc_steps_l (0, args) A x) A; y\<le>x \<rbrakk> |
|
351 \<Longrightarrow> abc_notfinal (abc_steps_l (0, args) A y) A " |
|
352 apply(subgoal_tac "\<exists> d. x = y + d", auto) |
|
353 apply(case_tac "abc_steps_l (0, args) A y",simp) |
|
354 apply(rule_tac classical, simp add: abc_steps_add leI halt_steps2) |
|
355 by arith |
|
356 |
|
357 lemma abc_Hoare_plus_unhalt2': |
|
358 assumes unhalt: "{Q} (B::abc_prog) \<up>" |
|
359 and halt: "{P} (A::abc_prog) {Q}" |
|
360 and notnull: "A \<noteq> []" |
|
361 and P: "P args" |
|
362 shows "abc_notfinal (abc_steps_l (0, args) (A [+] B) n) (A [+] B)" |
|
363 proof - |
|
364 obtain st nl stp where a: "abc_final (abc_steps_l (0, args) A stp) A" |
|
365 and b: "Q abc_holds_for (length A, nl)" |
|
366 and c: "abc_steps_l (0, args) A stp = (st, nl)" |
|
367 using halt P unfolding abc_Hoare_halt_def |
|
368 by (metis abc_holds_for.simps prod.exhaust) |
|
369 thm abc_before_final |
|
370 obtain stpa where d: |
|
371 "abc_notfinal (abc_steps_l (0, args) A stpa) A \<and> abc_final (abc_steps_l (0, args) A (Suc stpa)) A" |
|
372 using a notnull abc_before_final[of args A stp] |
|
373 by(auto) |
|
374 thus "?thesis" |
|
375 proof(cases "n < Suc stpa") |
|
376 case True |
|
377 have h: "n < Suc stpa" by fact |
|
378 then have "abc_notfinal (abc_steps_l (0, args) A n) A" |
|
379 using d |
|
380 by(rule_tac notfinal_all_before, auto) |
|
381 moreover then have "abc_steps_l (0, args) (A [+] B) n = abc_steps_l (0, args) A n" |
|
382 using notnull |
|
383 by(rule_tac abc_comp_frist_steps_eq_pre, simp_all) |
|
384 ultimately show "?thesis" |
|
385 by(case_tac "abc_steps_l (0, args) A n", simp) |
|
386 next |
|
387 case False |
|
388 have "\<not> n < Suc stpa" by fact |
|
389 then obtain d where i1: "n = Suc stpa + d" |
|
390 by (metis add_Suc less_iff_Suc_add not_less_eq) |
|
391 have "abc_steps_l (0, args) A (Suc stpa) = (length A, nl)" |
|
392 using d a c |
|
393 apply(case_tac "abc_steps_l (0, args) A stp", simp add: equal_when_halt) |
|
394 by(case_tac "abc_steps_l (0, args) A (Suc stpa)", simp add: equal_when_halt) |
|
395 moreover have "abc_steps_l (0, args) (A [+] B) stpa = abc_steps_l (0, args) A stpa" |
|
396 using notnull d |
|
397 by(rule_tac abc_comp_frist_steps_eq_pre, simp_all) |
|
398 ultimately have i2: "abc_steps_l (0, args) (A [+] B) (Suc stpa) = (length A, nl)" |
|
399 using d |
|
400 apply(case_tac "abc_steps_l (0, args) A stpa", simp) |
|
401 by(simp add: abc_step_red2 abc_steps_l.simps abc_fetch.simps abc_comp.simps nth_append) |
|
402 obtain s' nl' where i3:"abc_steps_l (0, nl) B d = (s', nl')" |
|
403 by (metis prod.exhaust) |
|
404 then have i4: "abc_steps_l (0, args) (A [+] B) (Suc stpa + d) = (length A + s', nl')" |
|
405 using i2 apply(simp only: abc_steps_add) |
|
406 using abc_comp_second_steps_eq[of nl B d s' nl'] |
|
407 by simp |
|
408 moreover have "s' < length B" |
|
409 using unhalt b i3 |
|
410 apply(simp add: abc_Hoare_unhalt_def) |
|
411 apply(erule_tac x = nl in allE, simp) |
|
412 by(erule_tac x = d in allE, simp) |
|
413 ultimately show "?thesis" |
|
414 using i1 |
|
415 by(simp) |
|
416 qed |
|
417 qed |
|
418 |
|
419 lemma abc_comp_null_left[simp]: "[] [+] A = A" |
|
420 apply(induct A) |
|
421 apply(case_tac [2] a) |
|
422 apply(auto simp: abc_comp.simps abc_shift.simps abc_inst_shift.simps) |
|
423 done |
|
424 |
|
425 lemma abc_comp_null_right[simp]: "A [+] [] = A" |
|
426 apply(induct A) |
|
427 apply(case_tac [2] a) |
|
428 apply(auto simp: abc_comp.simps abc_shift.simps abc_inst_shift.simps) |
|
429 done |
|
430 |
|
431 lemma abc_Hoare_plus_unhalt2: |
|
432 "\<lbrakk>{Q} (B::abc_prog)\<up>; {P} (A::abc_prog) {Q}\<rbrakk>\<Longrightarrow> {P} (A [+] B) \<up>" |
|
433 apply(case_tac "A = []") |
|
434 apply(simp add: abc_Hoare_halt_def abc_Hoare_unhalt_def abc_exec_null) |
|
435 apply(rule_tac abc_Hoare_unhaltI) |
|
436 apply(erule_tac abc_Hoare_plus_unhalt2', simp) |
|
437 apply(simp, simp) |
|
438 done |
|
439 |
|
440 end |
|
441 |
|
442 |