author | wenzelm |
Sat, 21 Jul 2007 23:25:00 +0200 | |
changeset 23894 | 1a4167d761ac |
parent 23746 | a455e69c31cc |
child 27208 | 5fe899199f85 |
permissions | -rw-r--r-- |
8177 | 1 |
(* Title: HOL/IMPP/Hoare.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 TUM |
|
5 |
*) |
|
6 |
||
17477 | 7 |
header {* Inductive definition of Hoare logic for partial correctness *} |
8 |
||
9 |
theory Hoare |
|
10 |
imports Natural |
|
11 |
begin |
|
12 |
||
13 |
text {* |
|
14 |
Completeness is taken relative to completeness of the underlying logic. |
|
15 |
||
16 |
Two versions of completeness proof: nested single recursion |
|
17 |
vs. simultaneous recursion in call rule |
|
18 |
*} |
|
8177 | 19 |
|
20 |
types 'a assn = "'a => state => bool" |
|
21 |
translations |
|
17477 | 22 |
"a assn" <= (type)"a => state => bool" |
8177 | 23 |
|
24 |
constdefs |
|
25 |
state_not_singleton :: bool |
|
17477 | 26 |
"state_not_singleton == \<exists>s t::state. s ~= t" (* at least two elements *) |
8177 | 27 |
|
28 |
peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35) |
|
17477 | 29 |
"peek_and P p == %Z s. P Z s & p s" |
8177 | 30 |
|
31 |
datatype 'a triple = |
|
17477 | 32 |
triple "'a assn" com "'a assn" ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58) |
33 |
||
8177 | 34 |
consts |
17477 | 35 |
triple_valid :: "nat => 'a triple => bool" ( "|=_:_" [0 , 58] 57) |
36 |
hoare_valids :: "'a triple set => 'a triple set => bool" ("_||=_" [58, 58] 57) |
|
8177 | 37 |
syntax |
17477 | 38 |
triples_valid:: "nat => 'a triple set => bool" ("||=_:_" [0 , 58] 57) |
39 |
hoare_valid :: "'a triple set => 'a triple => bool" ("_|=_" [58, 58] 57) |
|
8177 | 40 |
|
17477 | 41 |
defs triple_valid_def: "|=n:t == case t of {P}.c.{Q} => |
42 |
!Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s')" |
|
8177 | 43 |
translations "||=n:G" == "Ball G (triple_valid n)" |
17477 | 44 |
defs hoare_valids_def: "G||=ts == !n. ||=n:G --> ||=n:ts" |
8177 | 45 |
translations "G |=t " == " G||={t}" |
46 |
||
47 |
(* Most General Triples *) |
|
17477 | 48 |
constdefs MGT :: "com => state triple" ("{=}._.{->}" [60] 58) |
8177 | 49 |
"{=}.c.{->} == {%Z s0. Z = s0}. c .{%Z s1. <c,Z> -c-> s1}" |
50 |
||
23746 | 51 |
inductive |
52 |
hoare_derivs :: "'a triple set => 'a triple set => bool" ("_||-_" [58, 58] 57) |
|
53 |
and hoare_deriv :: "'a triple set => 'a triple => bool" ("_|-_" [58, 58] 57) |
|
54 |
where |
|
55 |
"G |-t == G||-{t}" |
|
17477 | 56 |
|
23746 | 57 |
| empty: "G||-{}" |
58 |
| insert: "[| G |-t; G||-ts |] |
|
17477 | 59 |
==> G||-insert t ts" |
8177 | 60 |
|
23746 | 61 |
| asm: "ts <= G ==> |
17477 | 62 |
G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *) |
8177 | 63 |
|
23746 | 64 |
| cut: "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *) |
8177 | 65 |
|
23746 | 66 |
| weaken: "[| G||-ts' ; ts <= ts' |] ==> G||-ts" |
8177 | 67 |
|
23746 | 68 |
| conseq: "!Z s. P Z s --> (? P' Q'. G|-{P'}.c.{Q'} & |
17477 | 69 |
(!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s')) |
70 |
==> G|-{P}.c.{Q}" |
|
8177 | 71 |
|
72 |
||
23746 | 73 |
| Skip: "G|-{P}. SKIP .{P}" |
8177 | 74 |
|
23746 | 75 |
| Ass: "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}" |
8177 | 76 |
|
23746 | 77 |
| Local: "G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])} |
17477 | 78 |
==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}" |
8177 | 79 |
|
23746 | 80 |
| Comp: "[| G|-{P}.c.{Q}; |
17477 | 81 |
G|-{Q}.d.{R} |] |
82 |
==> G|-{P}. (c;;d) .{R}" |
|
8177 | 83 |
|
23746 | 84 |
| If: "[| G|-{P &> b }.c.{Q}; |
17477 | 85 |
G|-{P &> (Not o b)}.d.{Q} |] |
86 |
==> G|-{P}. IF b THEN c ELSE d .{Q}" |
|
8177 | 87 |
|
23746 | 88 |
| Loop: "G|-{P &> b}.c.{P} ==> |
17477 | 89 |
G|-{P}. WHILE b DO c .{P &> (Not o b)}" |
8177 | 90 |
|
91 |
(* |
|
17477 | 92 |
BodyN: "(insert ({P}. BODY pn .{Q}) G) |
93 |
|-{P}. the (body pn) .{Q} ==> |
|
94 |
G|-{P}. BODY pn .{Q}" |
|
8177 | 95 |
*) |
23746 | 96 |
| Body: "[| G Un (%p. {P p}. BODY p .{Q p})`Procs |
17477 | 97 |
||-(%p. {P p}. the (body p) .{Q p})`Procs |] |
98 |
==> G||-(%p. {P p}. BODY p .{Q p})`Procs" |
|
8177 | 99 |
|
23746 | 100 |
| Call: "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} |
17477 | 101 |
==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}. |
102 |
X:=CALL pn(a) .{Q}" |
|
103 |
||
19803 | 104 |
|
105 |
section {* Soundness and relative completeness of Hoare rules wrt operational semantics *} |
|
106 |
||
107 |
lemma single_stateE: |
|
108 |
"state_not_singleton ==> !t. (!s::state. s = t) --> False" |
|
109 |
apply (unfold state_not_singleton_def) |
|
110 |
apply clarify |
|
111 |
apply (case_tac "ta = t") |
|
112 |
apply blast |
|
113 |
apply (blast dest: not_sym) |
|
114 |
done |
|
115 |
||
116 |
declare peek_and_def [simp] |
|
117 |
||
118 |
||
119 |
subsection "validity" |
|
120 |
||
121 |
lemma triple_valid_def2: |
|
122 |
"|=n:{P}.c.{Q} = (!Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s'))" |
|
123 |
apply (unfold triple_valid_def) |
|
124 |
apply auto |
|
125 |
done |
|
126 |
||
127 |
lemma Body_triple_valid_0: "|=0:{P}. BODY pn .{Q}" |
|
128 |
apply (simp (no_asm) add: triple_valid_def2) |
|
129 |
apply clarsimp |
|
130 |
done |
|
131 |
||
132 |
(* only ==> direction required *) |
|
133 |
lemma Body_triple_valid_Suc: "|=n:{P}. the (body pn) .{Q} = |=Suc n:{P}. BODY pn .{Q}" |
|
134 |
apply (simp (no_asm) add: triple_valid_def2) |
|
135 |
apply force |
|
136 |
done |
|
137 |
||
138 |
lemma triple_valid_Suc [rule_format (no_asm)]: "|=Suc n:t --> |=n:t" |
|
139 |
apply (unfold triple_valid_def) |
|
140 |
apply (induct_tac t) |
|
141 |
apply simp |
|
142 |
apply (fast intro: evaln_Suc) |
|
143 |
done |
|
144 |
||
145 |
lemma triples_valid_Suc: "||=Suc n:ts ==> ||=n:ts" |
|
146 |
apply (fast intro: triple_valid_Suc) |
|
147 |
done |
|
148 |
||
149 |
||
150 |
subsection "derived rules" |
|
151 |
||
152 |
lemma conseq12: "[| G|-{P'}.c.{Q'}; !Z s. P Z s --> |
|
153 |
(!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s') |] |
|
154 |
==> G|-{P}.c.{Q}" |
|
155 |
apply (rule hoare_derivs.conseq) |
|
156 |
apply blast |
|
157 |
done |
|
158 |
||
159 |
lemma conseq1: "[| G|-{P'}.c.{Q}; !Z s. P Z s --> P' Z s |] ==> G|-{P}.c.{Q}" |
|
160 |
apply (erule conseq12) |
|
161 |
apply fast |
|
162 |
done |
|
163 |
||
164 |
lemma conseq2: "[| G|-{P}.c.{Q'}; !Z s. Q' Z s --> Q Z s |] ==> G|-{P}.c.{Q}" |
|
165 |
apply (erule conseq12) |
|
166 |
apply fast |
|
167 |
done |
|
168 |
||
169 |
lemma Body1: "[| G Un (%p. {P p}. BODY p .{Q p})`Procs |
|
170 |
||- (%p. {P p}. the (body p) .{Q p})`Procs; |
|
171 |
pn:Procs |] ==> G|-{P pn}. BODY pn .{Q pn}" |
|
172 |
apply (drule hoare_derivs.Body) |
|
173 |
apply (erule hoare_derivs.weaken) |
|
174 |
apply fast |
|
175 |
done |
|
176 |
||
177 |
lemma BodyN: "(insert ({P}. BODY pn .{Q}) G) |-{P}. the (body pn) .{Q} ==> |
|
178 |
G|-{P}. BODY pn .{Q}" |
|
179 |
apply (rule Body1) |
|
180 |
apply (rule_tac [2] singletonI) |
|
181 |
apply clarsimp |
|
182 |
done |
|
183 |
||
184 |
lemma escape: "[| !Z s. P Z s --> G|-{%Z s'. s'=s}.c.{%Z'. Q Z} |] ==> G|-{P}.c.{Q}" |
|
185 |
apply (rule hoare_derivs.conseq) |
|
186 |
apply fast |
|
187 |
done |
|
188 |
||
189 |
lemma constant: "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}" |
|
190 |
apply (rule hoare_derivs.conseq) |
|
191 |
apply fast |
|
192 |
done |
|
193 |
||
194 |
lemma LoopF: "G|-{%Z s. P Z s & ~b s}.WHILE b DO c.{P}" |
|
195 |
apply (rule hoare_derivs.Loop [THEN conseq2]) |
|
196 |
apply (simp_all (no_asm)) |
|
197 |
apply (rule hoare_derivs.conseq) |
|
198 |
apply fast |
|
199 |
done |
|
200 |
||
201 |
(* |
|
202 |
Goal "[| G'||-ts; G' <= G |] ==> G||-ts" |
|
203 |
by (etac hoare_derivs.cut 1); |
|
204 |
by (etac hoare_derivs.asm 1); |
|
205 |
qed "thin"; |
|
206 |
*) |
|
207 |
lemma thin [rule_format]: "G'||-ts ==> !G. G' <= G --> G||-ts" |
|
208 |
apply (erule hoare_derivs.induct) |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23746
diff
changeset
|
209 |
apply (tactic {* ALLGOALS (EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1]) *}) |
19803 | 210 |
apply (rule hoare_derivs.empty) |
211 |
apply (erule (1) hoare_derivs.insert) |
|
212 |
apply (fast intro: hoare_derivs.asm) |
|
213 |
apply (fast intro: hoare_derivs.cut) |
|
214 |
apply (fast intro: hoare_derivs.weaken) |
|
215 |
apply (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI) |
|
216 |
prefer 7 |
|
217 |
apply (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast) |
|
218 |
apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW CLASET' fast_tac) *}) |
|
219 |
done |
|
220 |
||
221 |
lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}" |
|
222 |
apply (rule BodyN) |
|
223 |
apply (erule thin) |
|
224 |
apply auto |
|
225 |
done |
|
226 |
||
227 |
lemma derivs_insertD: "G||-insert t ts ==> G|-t & G||-ts" |
|
228 |
apply (fast intro: hoare_derivs.weaken) |
|
229 |
done |
|
230 |
||
231 |
lemma finite_pointwise [rule_format (no_asm)]: "[| finite U; |
|
232 |
!p. G |- {P' p}.c0 p.{Q' p} --> G |- {P p}.c0 p.{Q p} |] ==> |
|
233 |
G||-(%p. {P' p}.c0 p.{Q' p}) ` U --> G||-(%p. {P p}.c0 p.{Q p}) ` U" |
|
234 |
apply (erule finite_induct) |
|
235 |
apply simp |
|
236 |
apply clarsimp |
|
237 |
apply (drule derivs_insertD) |
|
238 |
apply (rule hoare_derivs.insert) |
|
239 |
apply auto |
|
240 |
done |
|
241 |
||
242 |
||
243 |
subsection "soundness" |
|
244 |
||
245 |
lemma Loop_sound_lemma: |
|
246 |
"G|={P &> b}. c .{P} ==> |
|
247 |
G|={P}. WHILE b DO c .{P &> (Not o b)}" |
|
248 |
apply (unfold hoare_valids_def) |
|
249 |
apply (simp (no_asm_use) add: triple_valid_def2) |
|
250 |
apply (rule allI) |
|
251 |
apply (subgoal_tac "!d s s'. <d,s> -n-> s' --> d = WHILE b DO c --> ||=n:G --> (!Z. P Z s --> P Z s' & ~b s') ") |
|
252 |
apply (erule thin_rl, fast) |
|
253 |
apply ((rule allI)+, rule impI) |
|
254 |
apply (erule evaln.induct) |
|
255 |
apply (simp_all (no_asm)) |
|
256 |
apply fast |
|
257 |
apply fast |
|
258 |
done |
|
259 |
||
260 |
lemma Body_sound_lemma: |
|
261 |
"[| G Un (%pn. {P pn}. BODY pn .{Q pn})`Procs |
|
262 |
||=(%pn. {P pn}. the (body pn) .{Q pn})`Procs |] ==> |
|
263 |
G||=(%pn. {P pn}. BODY pn .{Q pn})`Procs" |
|
264 |
apply (unfold hoare_valids_def) |
|
265 |
apply (rule allI) |
|
266 |
apply (induct_tac n) |
|
267 |
apply (fast intro: Body_triple_valid_0) |
|
268 |
apply clarsimp |
|
269 |
apply (drule triples_valid_Suc) |
|
270 |
apply (erule (1) notE impE) |
|
271 |
apply (simp add: ball_Un) |
|
272 |
apply (drule spec, erule impE, erule conjI, assumption) |
|
273 |
apply (fast intro!: Body_triple_valid_Suc [THEN iffD1]) |
|
274 |
done |
|
275 |
||
276 |
lemma hoare_sound: "G||-ts ==> G||=ts" |
|
277 |
apply (erule hoare_derivs.induct) |
|
278 |
apply (tactic {* TRYALL (eresolve_tac [thm "Loop_sound_lemma", thm "Body_sound_lemma"] THEN_ALL_NEW atac) *}) |
|
279 |
apply (unfold hoare_valids_def) |
|
280 |
apply blast |
|
281 |
apply blast |
|
282 |
apply (blast) (* asm *) |
|
283 |
apply (blast) (* cut *) |
|
284 |
apply (blast) (* weaken *) |
|
23746 | 285 |
apply (tactic {* ALLGOALS (EVERY'[REPEAT o thin_tac "hoare_derivs ?x ?y", SIMPSET' simp_tac, CLASET' clarify_tac, REPEAT o smp_tac 1]) *}) |
19803 | 286 |
apply (simp_all (no_asm_use) add: triple_valid_def2) |
287 |
apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *) |
|
288 |
apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *) |
|
289 |
prefer 3 apply (force) (* Call *) |
|
290 |
apply (erule_tac [2] evaln_elim_cases) (* If *) |
|
291 |
apply blast+ |
|
292 |
done |
|
293 |
||
294 |
||
295 |
section "completeness" |
|
296 |
||
297 |
(* Both versions *) |
|
298 |
||
299 |
(*unused*) |
|
300 |
lemma MGT_alternI: "G|-MGT c ==> |
|
301 |
G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1}" |
|
302 |
apply (unfold MGT_def) |
|
303 |
apply (erule conseq12) |
|
304 |
apply auto |
|
305 |
done |
|
306 |
||
307 |
(* requires com_det *) |
|
308 |
lemma MGT_alternD: "state_not_singleton ==> |
|
309 |
G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1} ==> G|-MGT c" |
|
310 |
apply (unfold MGT_def) |
|
311 |
apply (erule conseq12) |
|
312 |
apply auto |
|
313 |
apply (case_tac "? t. <c,?s> -c-> t") |
|
314 |
apply (fast elim: com_det) |
|
315 |
apply clarsimp |
|
316 |
apply (drule single_stateE) |
|
317 |
apply blast |
|
318 |
done |
|
319 |
||
320 |
lemma MGF_complete: |
|
321 |
"{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}" |
|
322 |
apply (unfold MGT_def) |
|
323 |
apply (erule conseq12) |
|
324 |
apply (clarsimp simp add: hoare_valids_def eval_eq triple_valid_def2) |
|
325 |
done |
|
326 |
||
327 |
declare WTs_elim_cases [elim!] |
|
328 |
declare not_None_eq [iff] |
|
329 |
(* requires com_det, escape (i.e. hoare_derivs.conseq) *) |
|
330 |
lemma MGF_lemma1 [rule_format (no_asm)]: "state_not_singleton ==> |
|
331 |
!pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}" |
|
332 |
apply (induct_tac c) |
|
333 |
apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) |
|
334 |
prefer 7 apply (fast intro: domI) |
|
335 |
apply (erule_tac [6] MGT_alternD) |
|
336 |
apply (unfold MGT_def) |
|
337 |
apply (drule_tac [7] bspec, erule_tac [7] domI) |
|
338 |
apply (rule_tac [7] escape, tactic {* CLASIMPSET' clarsimp_tac 7 *}, |
|
339 |
rule_tac [7] P1 = "%Z' s. s= (setlocs Z newlocs) [Loc Arg ::= fun Z]" in hoare_derivs.Call [THEN conseq1], erule_tac [7] conseq12) |
|
340 |
apply (erule_tac [!] thin_rl) |
|
341 |
apply (rule hoare_derivs.Skip [THEN conseq2]) |
|
342 |
apply (rule_tac [2] hoare_derivs.Ass [THEN conseq1]) |
|
343 |
apply (rule_tac [3] escape, tactic {* CLASIMPSET' clarsimp_tac 3 *}, |
|
344 |
rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1], |
|
345 |
erule_tac [3] conseq12) |
|
346 |
apply (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12) |
|
347 |
apply (tactic {* (rtac (thm "hoare_derivs.If") THEN_ALL_NEW etac (thm "conseq12")) 6 *}) |
|
348 |
apply (rule_tac [8] hoare_derivs.Loop [THEN conseq2], erule_tac [8] conseq12) |
|
349 |
apply auto |
|
350 |
done |
|
351 |
||
352 |
(* Version: nested single recursion *) |
|
353 |
||
354 |
lemma nesting_lemma [rule_format]: |
|
355 |
assumes "!!G ts. ts <= G ==> P G ts" |
|
356 |
and "!!G pn. P (insert (mgt_call pn) G) {mgt(the(body pn))} ==> P G {mgt_call pn}" |
|
357 |
and "!!G c. [| wt c; !pn:U. P G {mgt_call pn} |] ==> P G {mgt c}" |
|
358 |
and "!!pn. pn : U ==> wt (the (body pn))" |
|
359 |
shows "finite U ==> uG = mgt_call`U ==> |
|
360 |
!G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})" |
|
361 |
apply (induct_tac n) |
|
362 |
apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) |
|
363 |
apply (subgoal_tac "G = mgt_call ` U") |
|
364 |
prefer 2 |
|
365 |
apply (simp add: card_seteq finite_imageI) |
|
366 |
apply simp |
|
367 |
apply (erule prems(3-)) (*MGF_lemma1*) |
|
368 |
apply (rule ballI) |
|
369 |
apply (rule prems) (*hoare_derivs.asm*) |
|
370 |
apply fast |
|
371 |
apply (erule prems(3-)) (*MGF_lemma1*) |
|
372 |
apply (rule ballI) |
|
373 |
apply (case_tac "mgt_call pn : G") |
|
374 |
apply (rule prems) (*hoare_derivs.asm*) |
|
375 |
apply fast |
|
376 |
apply (rule prems(2-)) (*MGT_BodyN*) |
|
377 |
apply (drule spec, erule impE, erule_tac [2] impE, drule_tac [3] spec, erule_tac [3] mp) |
|
378 |
apply (erule_tac [3] prems(4-)) |
|
379 |
apply fast |
|
380 |
apply (drule finite_subset) |
|
381 |
apply (erule finite_imageI) |
|
382 |
apply (simp (no_asm_simp)) |
|
383 |
done |
|
384 |
||
385 |
lemma MGT_BodyN: "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==> |
|
386 |
G|-{=}.BODY pn.{->}" |
|
387 |
apply (unfold MGT_def) |
|
388 |
apply (rule BodyN) |
|
389 |
apply (erule conseq2) |
|
390 |
apply force |
|
391 |
done |
|
392 |
||
393 |
(* requires BodyN, com_det *) |
|
394 |
lemma MGF: "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c" |
|
395 |
apply (rule_tac P = "%G ts. G||-ts" and U = "dom body" in nesting_lemma) |
|
396 |
apply (erule hoare_derivs.asm) |
|
397 |
apply (erule MGT_BodyN) |
|
398 |
apply (rule_tac [3] finite_dom_body) |
|
399 |
apply (erule MGF_lemma1) |
|
400 |
prefer 2 apply (assumption) |
|
401 |
apply blast |
|
402 |
apply clarsimp |
|
403 |
apply (erule (1) WT_bodiesD) |
|
404 |
apply (rule_tac [3] le_refl) |
|
405 |
apply auto |
|
406 |
done |
|
407 |
||
408 |
||
409 |
(* Version: simultaneous recursion in call rule *) |
|
410 |
||
411 |
(* finiteness not really necessary here *) |
|
412 |
lemma MGT_Body: "[| G Un (%pn. {=}. BODY pn .{->})`Procs |
|
413 |
||-(%pn. {=}. the (body pn) .{->})`Procs; |
|
414 |
finite Procs |] ==> G ||-(%pn. {=}. BODY pn .{->})`Procs" |
|
415 |
apply (unfold MGT_def) |
|
416 |
apply (rule hoare_derivs.Body) |
|
417 |
apply (erule finite_pointwise) |
|
418 |
prefer 2 apply (assumption) |
|
419 |
apply clarify |
|
420 |
apply (erule conseq2) |
|
421 |
apply auto |
|
422 |
done |
|
423 |
||
424 |
(* requires empty, insert, com_det *) |
|
425 |
lemma MGF_lemma2_simult [rule_format (no_asm)]: "[| state_not_singleton; WT_bodies; |
|
426 |
F<=(%pn. {=}.the (body pn).{->})`dom body |] ==> |
|
427 |
(%pn. {=}. BODY pn .{->})`dom body||-F" |
|
428 |
apply (frule finite_subset) |
|
429 |
apply (rule finite_dom_body [THEN finite_imageI]) |
|
430 |
apply (rotate_tac 2) |
|
431 |
apply (tactic "make_imp_tac 1") |
|
432 |
apply (erule finite_induct) |
|
433 |
apply (clarsimp intro!: hoare_derivs.empty) |
|
434 |
apply (clarsimp intro!: hoare_derivs.insert simp del: range_composition) |
|
435 |
apply (erule MGF_lemma1) |
|
436 |
prefer 2 apply (fast dest: WT_bodiesD) |
|
437 |
apply clarsimp |
|
438 |
apply (rule hoare_derivs.asm) |
|
439 |
apply (fast intro: domI) |
|
440 |
done |
|
441 |
||
442 |
(* requires Body, empty, insert, com_det *) |
|
443 |
lemma MGF': "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c" |
|
444 |
apply (rule MGF_lemma1) |
|
445 |
apply assumption |
|
446 |
prefer 2 apply (assumption) |
|
447 |
apply clarsimp |
|
448 |
apply (subgoal_tac "{}||- (%pn. {=}. BODY pn .{->}) `dom body") |
|
449 |
apply (erule hoare_derivs.weaken) |
|
450 |
apply (fast intro: domI) |
|
451 |
apply (rule finite_dom_body [THEN [2] MGT_Body]) |
|
452 |
apply (simp (no_asm)) |
|
453 |
apply (erule (1) MGF_lemma2_simult) |
|
454 |
apply (rule subset_refl) |
|
455 |
done |
|
456 |
||
457 |
(* requires Body+empty+insert / BodyN, com_det *) |
|
458 |
lemmas hoare_complete = MGF' [THEN MGF_complete, standard] |
|
459 |
||
460 |
||
461 |
subsection "unused derived rules" |
|
462 |
||
463 |
lemma falseE: "G|-{%Z s. False}.c.{Q}" |
|
464 |
apply (rule hoare_derivs.conseq) |
|
465 |
apply fast |
|
466 |
done |
|
467 |
||
468 |
lemma trueI: "G|-{P}.c.{%Z s. True}" |
|
469 |
apply (rule hoare_derivs.conseq) |
|
470 |
apply (fast intro!: falseE) |
|
471 |
done |
|
472 |
||
473 |
lemma disj: "[| G|-{P}.c.{Q}; G|-{P'}.c.{Q'} |] |
|
474 |
==> G|-{%Z s. P Z s | P' Z s}.c.{%Z s. Q Z s | Q' Z s}" |
|
475 |
apply (rule hoare_derivs.conseq) |
|
476 |
apply (fast elim: conseq12) |
|
477 |
done (* analogue conj non-derivable *) |
|
478 |
||
479 |
lemma hoare_SkipI: "(!Z s. P Z s --> Q Z s) ==> G|-{P}. SKIP .{Q}" |
|
480 |
apply (rule conseq12) |
|
481 |
apply (rule hoare_derivs.Skip) |
|
482 |
apply fast |
|
483 |
done |
|
484 |
||
485 |
||
486 |
subsection "useful derived rules" |
|
487 |
||
488 |
lemma single_asm: "{t}|-t" |
|
489 |
apply (rule hoare_derivs.asm) |
|
490 |
apply (rule subset_refl) |
|
491 |
done |
|
492 |
||
493 |
lemma export_s: "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}" |
|
494 |
apply (rule hoare_derivs.conseq) |
|
495 |
apply auto |
|
496 |
done |
|
497 |
||
498 |
||
499 |
lemma weak_Local: "[| G|-{P}. c .{Q}; !k Z s. Q Z s --> Q Z (s[Loc Y::=k]) |] ==> |
|
500 |
G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{Q}" |
|
501 |
apply (rule export_s) |
|
502 |
apply (rule hoare_derivs.Local) |
|
503 |
apply (erule conseq2) |
|
504 |
apply (erule spec) |
|
505 |
done |
|
506 |
||
507 |
(* |
|
508 |
Goal "!Q. G |-{%Z s. ~(? s'. <c,s> -c-> s')}. c .{Q}" |
|
509 |
by (induct_tac "c" 1); |
|
510 |
by Auto_tac; |
|
511 |
by (rtac conseq1 1); |
|
512 |
by (rtac hoare_derivs.Skip 1); |
|
513 |
force 1; |
|
514 |
by (rtac conseq1 1); |
|
515 |
by (rtac hoare_derivs.Ass 1); |
|
516 |
force 1; |
|
517 |
by (defer_tac 1); |
|
518 |
### |
|
519 |
by (rtac hoare_derivs.Comp 1); |
|
520 |
by (dtac spec 2); |
|
521 |
by (dtac spec 2); |
|
522 |
by (assume_tac 2); |
|
523 |
by (etac conseq1 2); |
|
524 |
by (Clarsimp_tac 2); |
|
525 |
force 1; |
|
526 |
*) |
|
8177 | 527 |
|
528 |
end |