src/HOL/UNITY/ProgressSets.thy
 author wenzelm Thu Jul 23 22:13:42 2015 +0200 (2015-07-23) changeset 60773 d09c66a0ea10 parent 59807 22bc39064290 child 62343 24106dc44def permissions -rw-r--r--
more symbols by default, without xsymbols mode;
1 (*  Title:      HOL/UNITY/ProgressSets.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   2003  University of Cambridge
5 Progress Sets.  From
7     David Meier and Beverly Sanders,
8     Composing Leads-to Properties
9     Theoretical Computer Science 243:1-2 (2000), 339-361.
11     David Meier,
12     Progress Properties in Program Refinement and Parallel Composition
13     Swiss Federal Institute of Technology Zurich (1997)
14 *)
16 section{*Progress Sets*}
18 theory ProgressSets imports Transformers begin
20 subsection {*Complete Lattices and the Operator @{term cl}*}
22 definition lattice :: "'a set set => bool" where
23    --{*Meier calls them closure sets, but they are just complete lattices*}
24    "lattice L ==
25          (\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)"
27 definition cl :: "['a set set, 'a set] => 'a set" where
28    --{*short for ``closure''*}
29    "cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}"
31 lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L"
32 by (force simp add: lattice_def)
34 lemma empty_in_lattice: "lattice L ==> {} \<in> L"
35 by (force simp add: lattice_def)
37 lemma Union_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Union>M \<in> L"
38 by (simp add: lattice_def)
40 lemma Inter_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Inter>M \<in> L"
41 by (simp add: lattice_def)
43 lemma UN_in_lattice:
44      "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
45 apply (unfold SUP_def)
46 apply (blast intro: Union_in_lattice)
47 done
49 lemma INT_in_lattice:
50      "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i)  \<in> L"
51 apply (unfold INF_def)
52 apply (blast intro: Inter_in_lattice)
53 done
55 lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L"
56   using Union_in_lattice [of "{x, y}" L] by simp
58 lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L"
59   using Inter_in_lattice [of "{x, y}" L] by simp
61 lemma lattice_stable: "lattice {X. F \<in> stable X}"
62 by (simp add: lattice_def stable_def constrains_def, blast)
64 text{*The next three results state that @{term "cl L r"} is the minimal
65  element of @{term L} that includes @{term r}.*}
66 lemma cl_in_lattice: "lattice L ==> cl L r \<in> L"
67 apply (simp add: lattice_def cl_def)
68 apply (erule conjE)
69 apply (drule spec, erule mp, blast)
70 done
72 lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c"
73 by (force simp add: cl_def)
75 text{*The next three lemmas constitute assertion (4.61)*}
76 lemma cl_mono: "r \<subseteq> r' ==> cl L r \<subseteq> cl L r'"
77 by (simp add: cl_def, blast)
79 lemma subset_cl: "r \<subseteq> cl L r"
80 by (simp add: cl_def le_Inf_iff)
82 text{*A reformulation of @{thm subset_cl}*}
83 lemma clI: "x \<in> r ==> x \<in> cl L r"
84 by (simp add: cl_def, blast)
86 text{*A reformulation of @{thm cl_least}*}
87 lemma clD: "[|c \<in> cl L r; B \<in> L; r \<subseteq> B|] ==> c \<in> B"
88 by (force simp add: cl_def)
90 lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)"
91 by (simp add: cl_def, blast)
93 lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s"
94 apply (rule equalityI)
95  prefer 2
96   apply (simp add: cl_def, blast)
97 apply (rule cl_least)
98  apply (blast intro: Un_in_lattice cl_in_lattice)
99 apply (blast intro: subset_cl [THEN subsetD])
100 done
102 lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))"
103 apply (rule equalityI)
104  prefer 2 apply (simp add: cl_def, blast)
105 apply (rule cl_least)
106  apply (blast intro: UN_in_lattice cl_in_lattice)
107 apply (blast intro: subset_cl [THEN subsetD])
108 done
110 lemma cl_Int_subset: "cl L (r\<inter>s) \<subseteq> cl L r \<inter> cl L s"
111 by (simp add: cl_def, blast)
113 lemma cl_idem [simp]: "cl L (cl L r) = cl L r"
114 by (simp add: cl_def, blast)
116 lemma cl_ident: "r\<in>L ==> cl L r = r"
117 by (force simp add: cl_def)
119 lemma cl_empty [simp]: "lattice L ==> cl L {} = {}"
120 by (simp add: cl_ident empty_in_lattice)
122 lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV"
123 by (simp add: cl_ident UNIV_in_lattice)
125 text{*Assertion (4.62)*}
126 lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)"
127 apply (rule iffI)
128  apply (erule subst)
129  apply (erule cl_in_lattice)
130 apply (erule cl_ident)
131 done
133 lemma cl_subset_in_lattice: "[|cl L r \<subseteq> r; lattice L|] ==> r\<in>L"
134 by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
137 subsection {*Progress Sets and the Main Lemma*}
138 text{*A progress set satisfies certain closure conditions and is a
139 simple way of including the set @{term "wens_set F B"}.*}
141 definition closed :: "['a program, 'a set, 'a set,  'a set set] => bool" where
142    "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
143                               T \<inter> (B \<union> wp act M) \<in> L"
145 definition progress_set :: "['a program, 'a set, 'a set] => 'a set set set" where
146    "progress_set F T B ==
147       {L. lattice L & B \<in> L & T \<in> L & closed F T B L}"
149 lemma closedD:
150    "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|]
151     ==> T \<inter> (B \<union> wp act M) \<in> L"
152 by (simp add: closed_def)
154 text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
155 and @{term m} by @{term X}. *}
157 text{*Part of the proof of the claim at the bottom of page 97.  It's
158 proved separately because the argument requires a generalization over
159 all @{term "act \<in> Acts F"}.*}
160 lemma lattice_awp_lemma:
161   assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
162       and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
163       and latt: "lattice C"
164       and TC:   "T \<in> C"
165       and BC:   "B \<in> C"
166       and clos: "closed F T B C"
167     shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C"
168 apply (simp del: INT_simps add: awp_def INT_extend_simps)
169 apply (rule INT_in_lattice [OF latt])
170 apply (erule closedD [OF clos])
171 apply (simp add: subset_trans [OF BsubX Un_upper1])
172 apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)")
173  prefer 2 apply (blast intro: TC clD)
174 apply (erule ssubst)
175 apply (blast intro: Un_in_lattice latt cl_in_lattice TXC)
176 done
178 text{*Remainder of the proof of the claim at the bottom of page 97.*}
179 lemma lattice_lemma:
180   assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
181       and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
182       and act:  "act \<in> Acts F"
183       and latt: "lattice C"
184       and TC:   "T \<in> C"
185       and BC:   "B \<in> C"
186       and clos: "closed F T B C"
187     shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C"
188 apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C")
189  prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
190 apply (drule Int_in_lattice
191               [OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
192                     latt])
193 apply (subgoal_tac
194          "T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) =
195           T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))")
196  prefer 2 apply blast
197 apply simp
198 apply (drule Un_in_lattice [OF _ TXC latt])
199 apply (subgoal_tac
200          "T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X =
201           T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)")
202  apply simp
203 apply (blast intro: BsubX [THEN subsetD])
204 done
207 text{*Induction step for the main lemma*}
208 lemma progress_induction_step:
209   assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
210       and act:  "act \<in> Acts F"
211       and Xwens: "X \<in> wens_set F B"
212       and latt: "lattice C"
213       and  TC:  "T \<in> C"
214       and  BC:  "B \<in> C"
215       and clos: "closed F T B C"
216       and Fstable: "F \<in> stable T"
217   shows "T \<inter> wens F act X \<in> C"
218 proof -
219   from Xwens have BsubX: "B \<subseteq> X"
220     by (rule wens_set_imp_subset)
221   let ?r = "wens F act X"
222   have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X"
223     by (simp add: wens_unfold [symmetric])
224   then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)"
225     by blast
226   then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)"
227     by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast)
228   then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
229     by (blast intro: awp_mono [THEN  rev_subsetD] subset_cl [THEN subsetD])
230   then have "cl C (T\<inter>?r) \<subseteq>
231              cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))"
232     by (rule cl_mono)
233   then have "cl C (T\<inter>?r) \<subseteq>
234              T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
235     by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
236   then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X"
237     by blast
238   then have "cl C (T\<inter>?r) \<subseteq> ?r"
239     by (blast intro!: subset_wens)
240   then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
241     by (simp add: cl_ident TC
242                   subset_trans [OF cl_mono [OF Int_lower1]])
243   show ?thesis
244     by (rule cl_subset_in_lattice [OF cl_subset latt])
245 qed
247 text{*Proved on page 96 of Meier's thesis.  The special case when
248    @{term "T=UNIV"} states that every progress set for the program @{term F}
249    and set @{term B} includes the set @{term "wens_set F B"}.*}
250 lemma progress_set_lemma:
251      "[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C"
252 apply (simp add: progress_set_def, clarify)
253 apply (erule wens_set.induct)
254   txt{*Base*}
255   apply (simp add: Int_in_lattice)
256  txt{*The difficult @{term wens} case*}
257  apply (simp add: progress_induction_step)
258 txt{*Disjunctive case*}
259 apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C")
260  apply simp
261 apply (blast intro: UN_in_lattice)
262 done
265 subsection {*The Progress Set Union Theorem*}
267 lemma closed_mono:
268   assumes BB':  "B \<subseteq> B'"
269       and TBwp: "T \<inter> (B \<union> wp act M) \<in> C"
270       and B'C:  "B' \<in> C"
271       and TC:   "T \<in> C"
272       and latt: "lattice C"
273   shows "T \<inter> (B' \<union> wp act M) \<in> C"
274 proof -
275   from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C"
276     by (simp add: Int_Un_distrib)
277   then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C"
278     by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt)
279   show ?thesis
280     by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC],
281         blast intro: BB' [THEN subsetD])
282 qed
285 lemma progress_set_mono:
286     assumes BB':  "B \<subseteq> B'"
287     shows
288      "[| B' \<in> C;  C \<in> progress_set F T B|]
289       ==> C \<in> progress_set F T B'"
290 by (simp add: progress_set_def closed_def closed_mono [OF BB']
291                  subset_trans [OF BB'])
293 theorem progress_set_Union:
294   assumes leadsTo: "F \<in> A leadsTo B'"
295       and prog: "C \<in> progress_set F T B"
296       and Fstable: "F \<in> stable T"
297       and BB':  "B \<subseteq> B'"
298       and B'C:  "B' \<in> C"
299       and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
300   shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
301 apply (insert prog Fstable)
303   apply (force simp add: progress_set_def awp_iff_stable [symmetric])
304 apply (simp add: awp_iff_constrains)
305 apply (drule progress_set_mono [OF BB' B'C])
306 apply (blast intro: progress_set_lemma Gco constrains_weaken_L
307                     BB' [THEN subsetD])
308 done
311 subsection {*Some Progress Sets*}
313 lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B"
314 by (simp add: progress_set_def lattice_def closed_def)
318 subsubsection {*Lattices and Relations*}
319 text{*From Meier's thesis, section 4.5.3*}
321 definition relcl :: "'a set set => ('a * 'a) set" where
322     -- {*Derived relation from a lattice*}
323     "relcl L == {(x,y). y \<in> cl L {x}}"
325 definition latticeof :: "('a * 'a) set => 'a set set" where
326     -- {*Derived lattice from a relation: the set of upwards-closed sets*}
327     "latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r --> t \<in> X}"
330 lemma relcl_refl: "(a,a) \<in> relcl L"
331 by (simp add: relcl_def subset_cl [THEN subsetD])
333 lemma relcl_trans:
334      "[| (a,b) \<in> relcl L; (b,c) \<in> relcl L; lattice L |] ==> (a,c) \<in> relcl L"
335 apply (simp add: relcl_def)
336 apply (blast intro: clD cl_in_lattice)
337 done
339 lemma refl_relcl: "lattice L ==> refl (relcl L)"
340 by (simp add: refl_onI relcl_def subset_cl [THEN subsetD])
342 lemma trans_relcl: "lattice L ==> trans (relcl L)"
343 by (blast intro: relcl_trans transI)
345 lemma lattice_latticeof: "lattice (latticeof r)"
346 by (auto simp add: lattice_def latticeof_def)
348 lemma lattice_singletonI:
349      "[|lattice L; !!s. s \<in> X ==> {s} \<in> L|] ==> X \<in> L"
350 apply (cut_tac UN_singleton [of X])
351 apply (erule subst)
352 apply (simp only: UN_in_lattice)
353 done
355 text{*Equation (4.71) of Meier's thesis.  He gives no proof.*}
356 lemma cl_latticeof:
357      "[|refl r; trans r|]
358       ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}"
359 apply (rule equalityI)
360  apply (rule cl_least)
361   apply (simp (no_asm_use) add: latticeof_def trans_def, blast)
362  apply (simp add: latticeof_def refl_on_def, blast)
363 apply (simp add: latticeof_def, clarify)
364 apply (unfold cl_def, blast)
365 done
367 text{*Related to (4.71).*}
368 lemma cl_eq_Collect_relcl:
369      "lattice L ==> cl L X = {t. \<exists>s. s\<in>X & (s,t) \<in> relcl L}"
370 apply (cut_tac UN_singleton [of X])
371 apply (erule subst)
372 apply (force simp only: relcl_def cl_UN)
373 done
375 text{*Meier's theorem of section 4.5.3*}
376 theorem latticeof_relcl_eq: "lattice L ==> latticeof (relcl L) = L"
377 apply (rule equalityI)
378  prefer 2 apply (force simp add: latticeof_def relcl_def cl_def, clarify)
379 apply (rename_tac X)
380 apply (rule cl_subset_in_lattice)
381  prefer 2 apply assumption
382 apply (drule cl_ident_iff [OF lattice_latticeof, THEN iffD2])
383 apply (drule equalityD1)
384 apply (rule subset_trans)
385  prefer 2 apply assumption
386 apply (thin_tac "_ \<subseteq> X")
387 apply (cut_tac A=X in UN_singleton)
388 apply (erule subst)
389 apply (simp only: cl_UN lattice_latticeof
390                   cl_latticeof [OF refl_relcl trans_relcl])
391 apply (simp add: relcl_def)
392 done
394 theorem relcl_latticeof_eq:
395      "[|refl r; trans r|] ==> relcl (latticeof r) = r"
396 by (simp add: relcl_def cl_latticeof)
399 subsubsection {*Decoupling Theorems*}
401 definition decoupled :: "['a program, 'a program] => bool" where
402    "decoupled F G ==
403         \<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)"
406 text{*Rao's Decoupling Theorem*}
407 lemma stableco: "F \<in> stable A ==> F \<in> A-B co A"
408 by (simp add: stable_def constrains_def, blast)
410 theorem decoupling:
411   assumes leadsTo: "F \<in> A leadsTo B"
412       and Gstable: "G \<in> stable B"
413       and dec:     "decoupled F G"
414   shows "F\<squnion>G \<in> A leadsTo B"
415 proof -
416   have prog: "{X. G \<in> stable X} \<in> progress_set F UNIV B"
417     by (simp add: progress_set_def lattice_stable Gstable closed_def
418                   stable_Un [OF Gstable] dec [unfolded decoupled_def])
419   have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B"
420     by (rule progress_set_Union [OF leadsTo prog],
421         simp_all add: Gstable stableco)
422   thus ?thesis by simp
423 qed
426 text{*Rao's Weak Decoupling Theorem*}
427 theorem weak_decoupling:
428   assumes leadsTo: "F \<in> A leadsTo B"
429       and stable: "F\<squnion>G \<in> stable B"
430       and dec:     "decoupled F (F\<squnion>G)"
431   shows "F\<squnion>G \<in> A leadsTo B"
432 proof -
433   have prog: "{X. F\<squnion>G \<in> stable X} \<in> progress_set F UNIV B"
434     by (simp del: Join_stable
435              add: progress_set_def lattice_stable stable closed_def
436                   stable_Un [OF stable] dec [unfolded decoupled_def])
437   have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B"
438     by (rule progress_set_Union [OF leadsTo prog],
439         simp_all del: Join_stable add: stable,
440         simp add: stableco)
441   thus ?thesis by simp
442 qed
444 text{*The ``Decoupling via @{term G'} Union Theorem''*}
445 theorem decoupling_via_aux:
446   assumes leadsTo: "F \<in> A leadsTo B"
447       and prog: "{X. G' \<in> stable X} \<in> progress_set F UNIV B"
448       and GG':  "G \<le> G'"
449                --{*Beware!  This is the converse of the refinement relation!*}
450   shows "F\<squnion>G \<in> A leadsTo B"
451 proof -
452   from prog have stable: "G' \<in> stable B"
453     by (simp add: progress_set_def)
454   have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B"
455     by (rule progress_set_Union [OF leadsTo prog],
456         simp_all add: stable stableco component_stable [OF GG'])
457   thus ?thesis by simp
458 qed
461 subsection{*Composition Theorems Based on Monotonicity and Commutativity*}
463 subsubsection{*Commutativity of @{term "cl L"} and assignment.*}
464 definition commutes :: "['a program, 'a set, 'a set,  'a set set] => bool" where
465    "commutes F T B L ==
466        \<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M -->
467            cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))"
470 text{*From Meier's thesis, section 4.5.6*}
471 lemma commutativity1_lemma:
472   assumes commutes: "commutes F T B L"
473       and lattice:  "lattice L"
474       and BL: "B \<in> L"
475       and TL: "T \<in> L"
476   shows "closed F T B L"
477 apply (simp add: closed_def, clarify)
478 apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])
479 apply (simp add: Int_Un_distrib cl_Un [OF lattice]
480                  cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
481 apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))")
482  prefer 2
483  apply (cut_tac commutes, simp add: commutes_def)
484 apply (erule subset_trans)
485 apply (simp add: cl_ident)
486 apply (blast intro: rev_subsetD [OF _ wp_mono])
487 done
489 text{*Version packaged with @{thm progress_set_Union}*}
490 lemma commutativity1:
491   assumes leadsTo: "F \<in> A leadsTo B"
492       and lattice:  "lattice L"
493       and BL: "B \<in> L"
494       and TL: "T \<in> L"
495       and Fstable: "F \<in> stable T"
496       and Gco: "!!X. X\<in>L ==> G \<in> X-B co X"
497       and commutes: "commutes F T B L"
498   shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
499 by (rule progress_set_Union [OF leadsTo _ Fstable subset_refl BL Gco],
500     simp add: progress_set_def commutativity1_lemma commutes lattice BL TL)
504 text{*Possibly move to Relation.thy, after @{term single_valued}*}
505 definition funof :: "[('a*'b)set, 'a] => 'b" where
506    "funof r == (\<lambda>x. THE y. (x,y) \<in> r)"
508 lemma funof_eq: "[|single_valued r; (x,y) \<in> r|] ==> funof r x = y"
509 by (simp add: funof_def single_valued_def, blast)
511 lemma funof_Pair_in:
512      "[|single_valued r; x \<in> Domain r|] ==> (x, funof r x) \<in> r"
513 by (force simp add: funof_eq)
515 lemma funof_in:
516      "[|r``{x} \<subseteq> A; single_valued r; x \<in> Domain r|] ==> funof r x \<in> A"
517 by (force simp add: funof_eq)
519 lemma funof_imp_wp: "[|funof act t \<in> A; single_valued act|] ==> t \<in> wp act A"
520 by (force simp add: in_wp_iff funof_eq)
523 subsubsection{*Commutativity of Functions and Relation*}
524 text{*Thesis, page 109*}
526 (*FIXME: this proof is still an ungodly mess*)
527 text{*From Meier's thesis, section 4.5.6*}
528 lemma commutativity2_lemma:
529   assumes dcommutes:
530       "\<And>act s t. act \<in> Acts F \<Longrightarrow> s \<in> T \<Longrightarrow> (s, t) \<in> relcl L \<Longrightarrow>
531         s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
532     and determ: "!!act. act \<in> Acts F ==> single_valued act"
533     and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
534     and lattice:  "lattice L"
535     and BL: "B \<in> L"
536     and TL: "T \<in> L"
537     and Fstable: "F \<in> stable T"
538   shows  "commutes F T B L"
539 proof -
540   { fix M and act and t
541     assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)"
542     then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M"
543       by (force simp add: cl_eq_Collect_relcl [OF lattice])
544     then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M"
545       by blast
546     then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u"
547       apply (intro ballI impI)
548       apply (subst cl_ident [symmetric], assumption)
549       apply (simp add: relcl_def)
550       apply (blast intro: cl_mono [THEN  rev_subsetD])
551       done
552     with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M"
553       by (force intro!: funof_in
554         simp add: wp_def stable_def constrains_def determ total)
555     with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
556       by (intro dcommutes) assumption+
557     with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)"
558       by (simp add: relcl_def) (blast intro: BL cl_mono [THEN  rev_subsetD])
559     with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))"
560       by (blast intro: funof_imp_wp determ)
561     with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))"
562       by (blast intro: TL cl_mono [THEN  rev_subsetD])
563     then have"t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))"
564       by simp
565   }
566   then show "commutes F T B L" unfolding commutes_def by clarify
567 qed
569 text{*Version packaged with @{thm progress_set_Union}*}
570 lemma commutativity2:
571   assumes leadsTo: "F \<in> A leadsTo B"
572       and dcommutes:
573         "\<forall>act \<in> Acts F.
574          \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L -->
575                       s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
576       and determ: "!!act. act \<in> Acts F ==> single_valued act"
577       and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
578       and lattice:  "lattice L"
579       and BL: "B \<in> L"
580       and TL: "T \<in> L"
581       and Fstable: "F \<in> stable T"
582       and Gco: "!!X. X\<in>L ==> G \<in> X-B co X"
583   shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
584 apply (rule commutativity1 [OF leadsTo lattice])
585 apply (simp_all add: Gco commutativity2_lemma dcommutes determ total
586                      lattice BL TL Fstable)
587 done
590 subsection {*Monotonicity*}
591 text{*From Meier's thesis, section 4.5.7, page 110*}
592 (*to be continued?*)
594 end