src/HOL/UNITY/Transformers.thy
 author wenzelm Sat Jun 14 23:19:51 2008 +0200 (2008-06-14) changeset 27208 5fe899199f85 parent 26806 40b411ec05aa child 30952 7ab2716dd93b permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
1 (*  Title:      HOL/UNITY/Transformers
2     ID:         \$Id\$
3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4     Copyright   2003  University of Cambridge
6 Predicate Transformers.  From
8     David Meier and Beverly Sanders,
10     Theoretical Computer Science 243:1-2 (2000), 339-361.
12     David Meier,
13     Progress Properties in Program Refinement and Parallel Composition
14     Swiss Federal Institute of Technology Zurich (1997)
15 *)
19 theory Transformers imports Comp begin
21 subsection{*Defining the Predicate Transformers @{term wp},
22    @{term awp} and  @{term wens}*}
24 constdefs
25   wp :: "[('a*'a) set, 'a set] => 'a set"
26     --{*Dijkstra's weakest-precondition operator (for an individual command)*}
27     "wp act B == - (act^-1 `` (-B))"
29   awp :: "['a program, 'a set] => 'a set"
30     --{*Dijkstra's weakest-precondition operator (for a program)*}
31     "awp F B == (\<Inter>act \<in> Acts F. wp act B)"
33   wens :: "['a program, ('a*'a) set, 'a set] => 'a set"
34     --{*The weakest-ensures transformer*}
35     "wens F act B == gfp(\<lambda>X. (wp act B \<inter> awp F (B \<union> X)) \<union> B)"
37 text{*The fundamental theorem for wp*}
38 theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
39 by (force simp add: wp_def)
41 text{*This lemma is a good deal more intuitive than the definition!*}
42 lemma in_wp_iff: "(a \<in> wp act B) = (\<forall>x. (a,x) \<in> act --> x \<in> B)"
43 by (simp add: wp_def, blast)
45 lemma Compl_Domain_subset_wp: "- (Domain act) \<subseteq> wp act B"
46 by (force simp add: wp_def)
48 lemma wp_empty [simp]: "wp act {} = - (Domain act)"
49 by (force simp add: wp_def)
51 text{*The identity relation is the skip action*}
52 lemma wp_Id [simp]: "wp Id B = B"
55 lemma wp_totalize_act:
56      "wp (totalize_act act) B = (wp act B \<inter> Domain act) \<union> (B - Domain act)"
57 by (simp add: wp_def totalize_act_def, blast)
59 lemma awp_subset: "(awp F A \<subseteq> A)"
60 by (force simp add: awp_def wp_def)
62 lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B"
63 by (simp add: awp_def wp_def, blast)
65 text{*The fundamental theorem for awp*}
66 theorem awp_iff_constrains: "(A <= awp F B) = (F \<in> A co B)"
67 by (simp add: awp_def constrains_def wp_iff INT_subset_iff)
69 lemma awp_iff_stable: "(A \<subseteq> awp F A) = (F \<in> stable A)"
70 by (simp add: awp_iff_constrains stable_def)
72 lemma stable_imp_awp_ident: "F \<in> stable A ==> awp F A = A"
73 apply (rule equalityI [OF awp_subset])
75 done
77 lemma wp_mono: "(A \<subseteq> B) ==> wp act A \<subseteq> wp act B"
78 by (simp add: wp_def, blast)
80 lemma awp_mono: "(A \<subseteq> B) ==> awp F A \<subseteq> awp F B"
81 by (simp add: awp_def wp_def, blast)
83 lemma wens_unfold:
84      "wens F act B = (wp act B \<inter> awp F (B \<union> wens F act B)) \<union> B"
86 apply (rule gfp_unfold)
87 apply (simp add: mono_def wp_def awp_def, blast)
88 done
90 lemma wens_Id [simp]: "wens F Id B = B"
91 by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
93 text{*These two theorems justify the claim that @{term wens} returns the
94 weakest assertion satisfying the ensures property*}
95 lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B"
96 apply (simp add: wens_def ensures_def transient_def, clarify)
97 apply (rule rev_bexI, assumption)
98 apply (rule gfp_upperbound)
99 apply (simp add: constrains_def awp_def wp_def, blast)
100 done
102 lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
103 by (simp add: wens_def gfp_def constrains_def awp_def wp_def
104               ensures_def transient_def Sup_set_eq, blast)
106 text{*These two results constitute assertion (4.13) of the thesis*}
107 lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
108 apply (simp add: wens_def wp_def awp_def)
109 apply (rule gfp_mono, blast)
110 done
112 lemma wens_weakening: "B \<subseteq> wens F act B"
113 by (simp add: wens_def gfp_def Sup_set_eq, blast)
115 text{*Assertion (6), or 4.16 in the thesis*}
116 lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B"
117 apply (simp add: wens_def wp_def awp_def)
118 apply (rule gfp_upperbound, blast)
119 done
121 text{*Assertion 4.17 in the thesis*}
122 lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
123 by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
124   --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
125       is declared as an iff-rule, then it's almost impossible to prove.
126       One proof is via @{text meson} after expanding all definitions, but it's
127       slow!*}
129 text{*Assertion (7): 4.18 in the thesis.  NOTE that many of these results
130 hold for an arbitrary action.  We often do not require @{term "act \<in> Acts F"}*}
131 lemma stable_wens: "F \<in> stable A ==> F \<in> stable (wens F act A)"
133 apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]])
134 apply (simp add: Un_Int_distrib2 Compl_partition2)
135 apply (erule constrains_weaken, blast)
136 apply (simp add: Un_subset_iff wens_weakening)
137 done
139 text{*Assertion 4.20 in the thesis.*}
140 lemma wens_Int_eq_lemma:
141       "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
142        ==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
143 apply (rule subset_wens)
144 apply (rule_tac P="\<lambda>x. ?f x \<subseteq> ?b" in ssubst [OF wens_unfold])
145 apply (simp add: wp_def awp_def, blast)
146 done
148 text{*Assertion (8): 4.21 in the thesis. Here we indeed require
149       @{term "act \<in> Acts F"}*}
150 lemma wens_Int_eq:
151       "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
152        ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
153 apply (rule equalityI)
154  apply (simp_all add: Int_lower1 Int_subset_iff)
155  apply (rule wens_Int_eq_lemma, assumption+)
156 apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto)
157 done
160 subsection{*Defining the Weakest Ensures Set*}
162 inductive_set
163   wens_set :: "['a program, 'a set] => 'a set set"
164   for F :: "'a program" and B :: "'a set"
165 where
167   Basis: "B \<in> wens_set F B"
169 | Wens:  "[|X \<in> wens_set F B; act \<in> Acts F|] ==> wens F act X \<in> wens_set F B"
171 | Union: "W \<noteq> {} ==> \<forall>U \<in> W. U \<in> wens_set F B ==> \<Union>W \<in> wens_set F B"
173 lemma wens_set_imp_co: "A \<in> wens_set F B ==> F \<in> (A-B) co A"
174 apply (erule wens_set.induct)
176  apply (drule_tac act1=act and A1=X
177         in constrains_Un [OF Diff_wens_constrains])
178  apply (erule constrains_weaken, blast)
179  apply (simp add: Un_subset_iff wens_weakening)
180 apply (rule constrains_weaken)
181 apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+)
182 done
184 lemma wens_set_imp_leadsTo: "A \<in> wens_set F B ==> F \<in> A leadsTo B"
185 apply (erule wens_set.induct)
187  apply (blast intro: wens_ensures leadsTo_Trans)
189 done
191 lemma leadsTo_imp_wens_set: "F \<in> A leadsTo B ==> \<exists>C \<in> wens_set F B. A \<subseteq> C"
193   apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens)
194  apply (clarify, drule ensures_weaken_R, assumption)
195  apply (blast dest!: ensures_imp_wens intro: wens_set.Wens)
196 apply (case_tac "S={}")
197  apply (simp, blast intro: wens_set.Basis)
198 apply (clarsimp dest!: bchoice simp: ball_conj_distrib Bex_def)
199 apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>S. Z = f U}" in exI)
200 apply (blast intro: wens_set.Union)
201 done
203 text{*Assertion (9): 4.27 in the thesis.*}
204 lemma leadsTo_iff_wens_set: "(F \<in> A leadsTo B) = (\<exists>C \<in> wens_set F B. A \<subseteq> C)"
207 text{*This is the result that requires the definition of @{term wens_set} to
208   require @{term W} to be non-empty in the Unio case, for otherwise we should
209   always have @{term "{} \<in> wens_set F B"}.*}
210 lemma wens_set_imp_subset: "A \<in> wens_set F B ==> B \<subseteq> A"
211 apply (erule wens_set.induct)
212   apply (blast intro: wens_weakening [THEN subsetD])+
213 done
216 subsection{*Properties Involving Program Union*}
218 text{*Assertion (4.30) of thesis, reoriented*}
219 lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B \<inter> awp G B"
220 by (simp add: awp_def wp_def, blast)
222 lemma wens_subset: "wens F act B - B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)"
223 by (subst wens_unfold, fast)
225 text{*Assertion (4.31)*}
226 lemma subset_wens_Join:
227       "[|A = T \<inter> wens F act B;  T-B \<subseteq> awp F T; A-B \<subseteq> awp G (A \<union> B)|]
228        ==> A \<subseteq> wens (F\<squnion>G) act B"
229 apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq>
230                     wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T")
231  apply (rule subset_wens)
232  apply (simp add: awp_Join_eq awp_Int_eq Int_subset_iff Un_commute)
233  apply (simp add: awp_def wp_def, blast)
234 apply (insert wens_subset [of F act B], blast)
235 done
237 text{*Assertion (4.32)*}
238 lemma wens_Join_subset: "wens (F\<squnion>G) act B \<subseteq> wens F act B"
240 apply (rule gfp_mono)
241 apply (auto simp add: awp_Join_eq)
242 done
244 text{*Lemma, because the inductive step is just too messy.*}
245 lemma wens_Union_inductive_step:
246   assumes awpF: "T-B \<subseteq> awp F T"
247       and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
248   shows "[|X \<in> wens_set F B; act \<in> Acts F; Y \<subseteq> X; T\<inter>X = T\<inter>Y|]
249          ==> wens (F\<squnion>G) act Y \<subseteq> wens F act X \<and>
250              T \<inter> wens F act X = T \<inter> wens (F\<squnion>G) act Y"
251 apply (subgoal_tac "wens (F\<squnion>G) act Y \<subseteq> wens F act X")
252  prefer 2
253  apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
254 apply (rule equalityI)
255  prefer 2 apply blast
256 apply (simp add: Int_lower1 Int_subset_iff)
257 apply (frule wens_set_imp_subset)
258 apply (subgoal_tac "T-X \<subseteq> awp F T")
259  prefer 2 apply (blast intro: awpF [THEN subsetD])
260 apply (rule_tac B = "wens (F\<squnion>G) act (T\<inter>X)" in subset_trans)
261  prefer 2 apply (blast intro!: wens_mono)
262 apply (subst wens_Int_eq, assumption+)
263 apply (rule subset_wens_Join [of _ T], simp, blast)
264 apply (subgoal_tac "T \<inter> wens F act (T\<inter>X) \<union> T\<inter>X = T \<inter> wens F act X")
265  prefer 2
266  apply (subst wens_Int_eq [symmetric], assumption+)
267  apply (blast intro: wens_weakening [THEN subsetD], simp)
268 apply (blast intro: awpG [THEN subsetD] wens_set.Wens)
269 done
271 theorem wens_Union:
272   assumes awpF: "T-B \<subseteq> awp F T"
273       and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
274       and major: "X \<in> wens_set F B"
275   shows "\<exists>Y \<in> wens_set (F\<squnion>G) B. Y \<subseteq> X & T\<inter>X = T\<inter>Y"
276 apply (rule wens_set.induct [OF major])
277   txt{*Basis: trivial*}
278   apply (blast intro: wens_set.Basis)
279  txt{*Inductive step*}
280  apply clarify
281  apply (rule_tac x = "wens (F\<squnion>G) act Y" in rev_bexI)
282   apply (force intro: wens_set.Wens)
283  apply (simp add: wens_Union_inductive_step [OF awpF awpG])
284 txt{*Union: by Axiom of Choice*}
285 apply (simp add: ball_conj_distrib Bex_def)
286 apply (clarify dest!: bchoice)
287 apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>W. Z = f U}" in exI)
288 apply (blast intro: wens_set.Union)
289 done
293       and awpF: "T-B \<subseteq> awp F T"
294       and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
295   shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
297 apply (rule wens_Union [THEN bexE])
298    apply (rule awpF)
299   apply (erule awpG, assumption)
301 done
304 subsection {*The Set @{term "wens_set F B"} for a Single-Assignment Program*}
305 text{*Thesis Section 4.3.3*}
307 text{*We start by proving laws about single-assignment programs*}
308 lemma awp_single_eq [simp]:
309      "awp (mk_program (init, {act}, allowed)) B = B \<inter> wp act B"
310 by (force simp add: awp_def wp_def)
312 lemma wp_Un_subset: "wp act A \<union> wp act B \<subseteq> wp act (A \<union> B)"
313 by (force simp add: wp_def)
315 lemma wp_Un_eq: "single_valued act ==> wp act (A \<union> B) = wp act A \<union> wp act B"
316 apply (rule equalityI)
317  apply (force simp add: wp_def single_valued_def)
318 apply (rule wp_Un_subset)
319 done
321 lemma wp_UN_subset: "(\<Union>i\<in>I. wp act (A i)) \<subseteq> wp act (\<Union>i\<in>I. A i)"
322 by (force simp add: wp_def)
324 lemma wp_UN_eq:
325      "[|single_valued act; I\<noteq>{}|]
326       ==> wp act (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. wp act (A i))"
327 apply (rule equalityI)
328  prefer 2 apply (rule wp_UN_subset)
329  apply (simp add: wp_def Image_INT_eq)
330 done
332 lemma wens_single_eq:
333      "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
334 by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
337 text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
339 constdefs
340   wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set"
341     "wens_single_finite act B k == \<Union>i \<in> atMost k. ((wp act)^i) B"
343   wens_single :: "[('a*'a) set, 'a set] => 'a set"
344     "wens_single act B == \<Union>i. ((wp act)^i) B"
346 lemma wens_single_Un_eq:
347       "single_valued act
348        ==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B"
349 apply (rule equalityI)
350  apply (simp_all add: Un_upper1 Un_subset_iff)
351 apply (simp add: wens_single_def wp_UN_eq, clarify)
352 apply (rule_tac a="Suc(i)" in UN_I, auto)
353 done
355 lemma atMost_nat_nonempty: "atMost (k::nat) \<noteq> {}"
356 by force
358 lemma wens_single_finite_0 [simp]: "wens_single_finite act B 0 = B"
361 lemma wens_single_finite_Suc:
362       "single_valued act
363        ==> wens_single_finite act B (Suc k) =
364            wens_single_finite act B k \<union> wp act (wens_single_finite act B k)"
365 apply (simp add: wens_single_finite_def image_def
366                  wp_UN_eq [OF _ atMost_nat_nonempty])
367 apply (force elim!: le_SucE)
368 done
370 lemma wens_single_finite_Suc_eq_wens:
371      "single_valued act
372        ==> wens_single_finite act B (Suc k) =
373            wens (mk_program (init, {act}, allowed)) act
374                 (wens_single_finite act B k)"
375 by (simp add: wens_single_finite_Suc wens_single_eq)
377 lemma def_wens_single_finite_Suc_eq_wens:
378      "[|F = mk_program (init, {act}, allowed); single_valued act|]
379        ==> wens_single_finite act B (Suc k) =
380            wens F act (wens_single_finite act B k)"
383 lemma wens_single_finite_Un_eq:
384       "single_valued act
385        ==> wens_single_finite act B k \<union> wp act (wens_single_finite act B k)
386            \<in> range (wens_single_finite act B)"
387 by (simp add: wens_single_finite_Suc [symmetric])
389 lemma wens_single_eq_Union:
390       "wens_single act B = \<Union>range (wens_single_finite act B)"
391 by (simp add: wens_single_finite_def wens_single_def, blast)
393 lemma wens_single_finite_eq_Union:
394      "wens_single_finite act B n = (\<Union>k\<in>atMost n. wens_single_finite act B k)"
395 apply (auto simp add: wens_single_finite_def)
396 apply (blast intro: le_trans)
397 done
399 lemma wens_single_finite_mono:
400      "m \<le> n ==> wens_single_finite act B m \<subseteq> wens_single_finite act B n"
401 by (force simp add:  wens_single_finite_eq_Union [of act B n])
403 lemma wens_single_finite_subset_wens_single:
404       "wens_single_finite act B k \<subseteq> wens_single act B"
405 by (simp add: wens_single_eq_Union, blast)
407 lemma subset_wens_single_finite:
408       "[|W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}|]
409        ==> \<exists>m. \<Union>W = wens_single_finite act B m"
410 apply (induct k)
411  apply (rule_tac x=0 in exI, simp, blast)
412 apply (auto simp add: atMost_Suc)
413 apply (case_tac "wens_single_finite act B (Suc k) \<in> W")
414  prefer 2 apply blast
415 apply (drule_tac x="Suc k" in spec)
416 apply (erule notE, rule equalityI)
417  prefer 2 apply blast
418 apply (subst wens_single_finite_eq_Union)
419 apply (simp add: atMost_Suc, blast)
420 done
422 text{*lemma for Union case*}
423 lemma Union_eq_wens_single:
424       "\<lbrakk>\<forall>k. \<not> W \<subseteq> wens_single_finite act B ` {..k};
425         W \<subseteq> insert (wens_single act B)
426             (range (wens_single_finite act B))\<rbrakk>
427        \<Longrightarrow> \<Union>W = wens_single act B"
428 apply (case_tac "wens_single act B \<in> W")
429  apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD])
431 apply (rule equalityI, blast)
432 apply (simp add: UN_subset_iff, clarify)
433 apply (subgoal_tac "\<exists>y\<in>W. \<exists>n. y = wens_single_finite act B n & i\<le>n")
434  apply (blast intro: wens_single_finite_mono [THEN subsetD])
435 apply (drule_tac x=i in spec)
436 apply (force simp add: atMost_def)
437 done
439 lemma wens_set_subset_single:
440       "single_valued act
441        ==> wens_set (mk_program (init, {act}, allowed)) B \<subseteq>
442            insert (wens_single act B) (range (wens_single_finite act B))"
443 apply (rule subsetI)
444 apply (erule wens_set.induct)
445   txt{*Basis*}
446   apply (fastsimp simp add: wens_single_finite_def)
447  txt{*Wens inductive step*}
448  apply (case_tac "acta = Id", simp)
450  apply (elim disjE)
452  apply (force simp add: wens_single_finite_Un_eq)
453 txt{*Union inductive step*}
454 apply (case_tac "\<exists>k. W \<subseteq> wens_single_finite act B ` (atMost k)")
455  apply (blast dest!: subset_wens_single_finite, simp)
456 apply (rule disjI1 [OF Union_eq_wens_single], blast+)
457 done
459 lemma wens_single_finite_in_wens_set:
460       "single_valued act \<Longrightarrow>
461          wens_single_finite act B k
462          \<in> wens_set (mk_program (init, {act}, allowed)) B"
463 apply (induct_tac k)
464  apply (simp add: wens_single_finite_def wens_set.Basis)
466                  wens_single_finite_Suc_eq_wens [of act B _ init allowed])
467 done
469 lemma single_subset_wens_set:
470       "single_valued act
471        ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq>
472            wens_set (mk_program (init, {act}, allowed)) B"
473 apply (simp add: wens_single_eq_Union UN_eq)
474 apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
475 done
477 text{*Theorem (4.29)*}
478 theorem wens_set_single_eq:
479      "[|F = mk_program (init, {act}, allowed); single_valued act|]
480       ==> wens_set F B =
481           insert (wens_single act B) (range (wens_single_finite act B))"
482 apply (rule equalityI)