src/HOL/UNITY/ProgressSets.thy
 author wenzelm Mon Mar 16 18:24:30 2009 +0100 (2009-03-16) changeset 30549 d2d7874648bd parent 30198 922f944f03b2 child 32139 e271a64f03ff permissions -rw-r--r--
simplified method setup;
1 (*  Title:      HOL/UNITY/ProgressSets
2     ID:         \$Id\$
3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4     Copyright   2003  University of Cambridge
6 Progress Sets.  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 ProgressSets imports Transformers begin
21 subsection {*Complete Lattices and the Operator @{term cl}*}
23 constdefs
24   lattice :: "'a set set => bool"
25    --{*Meier calls them closure sets, but they are just complete lattices*}
26    "lattice L ==
27 	 (\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)"
29   cl :: "['a set set, 'a set] => 'a set"
30    --{*short for ``closure''*}
31    "cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}"
33 lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L"
34 by (force simp add: lattice_def)
36 lemma empty_in_lattice: "lattice L ==> {} \<in> L"
37 by (force simp add: lattice_def)
39 lemma Union_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Union>M \<in> L"
42 lemma Inter_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Inter>M \<in> L"
45 lemma UN_in_lattice:
46      "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
48 apply (blast intro: Union_in_lattice)
49 done
51 lemma INT_in_lattice:
52      "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i)  \<in> L"
54 apply (blast intro: Inter_in_lattice)
55 done
57 lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L"
58 apply (simp only: Un_eq_Union)
59 apply (blast intro: Union_in_lattice)
60 done
62 lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L"
63 apply (simp only: Int_eq_Inter)
64 apply (blast intro: Inter_in_lattice)
65 done
67 lemma lattice_stable: "lattice {X. F \<in> stable X}"
68 by (simp add: lattice_def stable_def constrains_def, blast)
70 text{*The next three results state that @{term "cl L r"} is the minimal
71  element of @{term L} that includes @{term r}.*}
72 lemma cl_in_lattice: "lattice L ==> cl L r \<in> L"
73 apply (simp add: lattice_def cl_def)
74 apply (erule conjE)
75 apply (drule spec, erule mp, blast)
76 done
78 lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c"
79 by (force simp add: cl_def)
81 text{*The next three lemmas constitute assertion (4.61)*}
82 lemma cl_mono: "r \<subseteq> r' ==> cl L r \<subseteq> cl L r'"
83 by (simp add: cl_def, blast)
85 lemma subset_cl: "r \<subseteq> cl L r"
86 by (simp add: cl_def, blast)
88 text{*A reformulation of @{thm subset_cl}*}
89 lemma clI: "x \<in> r ==> x \<in> cl L r"
90 by (simp add: cl_def, blast)
92 text{*A reformulation of @{thm cl_least}*}
93 lemma clD: "[|c \<in> cl L r; B \<in> L; r \<subseteq> B|] ==> c \<in> B"
94 by (force simp add: cl_def)
96 lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)"
97 by (simp add: cl_def, blast)
99 lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s"
100 apply (rule equalityI)
101  prefer 2
102   apply (simp add: cl_def, blast)
103 apply (rule cl_least)
104  apply (blast intro: Un_in_lattice cl_in_lattice)
105 apply (blast intro: subset_cl [THEN subsetD])
106 done
108 lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))"
109 apply (rule equalityI)
110  prefer 2 apply (simp add: cl_def, blast)
111 apply (rule cl_least)
112  apply (blast intro: UN_in_lattice cl_in_lattice)
113 apply (blast intro: subset_cl [THEN subsetD])
114 done
116 lemma cl_Int_subset: "cl L (r\<inter>s) \<subseteq> cl L r \<inter> cl L s"
117 by (simp add: cl_def, blast)
119 lemma cl_idem [simp]: "cl L (cl L r) = cl L r"
120 by (simp add: cl_def, blast)
122 lemma cl_ident: "r\<in>L ==> cl L r = r"
123 by (force simp add: cl_def)
125 lemma cl_empty [simp]: "lattice L ==> cl L {} = {}"
126 by (simp add: cl_ident empty_in_lattice)
128 lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV"
129 by (simp add: cl_ident UNIV_in_lattice)
131 text{*Assertion (4.62)*}
132 lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)"
133 apply (rule iffI)
134  apply (erule subst)
135  apply (erule cl_in_lattice)
136 apply (erule cl_ident)
137 done
139 lemma cl_subset_in_lattice: "[|cl L r \<subseteq> r; lattice L|] ==> r\<in>L"
140 by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
143 subsection {*Progress Sets and the Main Lemma*}
144 text{*A progress set satisfies certain closure conditions and is a
145 simple way of including the set @{term "wens_set F B"}.*}
147 constdefs
148   closed :: "['a program, 'a set, 'a set,  'a set set] => bool"
149    "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
150                               T \<inter> (B \<union> wp act M) \<in> L"
152   progress_set :: "['a program, 'a set, 'a set] => 'a set set set"
153    "progress_set F T B ==
154       {L. lattice L & B \<in> L & T \<in> L & closed F T B L}"
156 lemma closedD:
157    "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|]
158     ==> T \<inter> (B \<union> wp act M) \<in> L"
161 text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
162 and @{term m} by @{term X}. *}
164 text{*Part of the proof of the claim at the bottom of page 97.  It's
165 proved separately because the argument requires a generalization over
166 all @{term "act \<in> Acts F"}.*}
167 lemma lattice_awp_lemma:
168   assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
169       and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
170       and latt: "lattice C"
171       and TC:   "T \<in> C"
172       and BC:   "B \<in> C"
173       and clos: "closed F T B C"
174     shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C"
175 apply (simp del: INT_simps add: awp_def INT_extend_simps)
176 apply (rule INT_in_lattice [OF latt])
177 apply (erule closedD [OF clos])
178 apply (simp add: subset_trans [OF BsubX Un_upper1])
179 apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)")
180  prefer 2 apply (blast intro: TC clD)
181 apply (erule ssubst)
182 apply (blast intro: Un_in_lattice latt cl_in_lattice TXC)
183 done
185 text{*Remainder of the proof of the claim at the bottom of page 97.*}
186 lemma lattice_lemma:
187   assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
188       and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
189       and act:  "act \<in> Acts F"
190       and latt: "lattice C"
191       and TC:   "T \<in> C"
192       and BC:   "B \<in> C"
193       and clos: "closed F T B C"
194     shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C"
195 apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C")
196  prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
197 apply (drule Int_in_lattice
198               [OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
199                     latt])
200 apply (subgoal_tac
201 	 "T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) =
202 	  T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))")
203  prefer 2 apply blast
204 apply simp
205 apply (drule Un_in_lattice [OF _ TXC latt])
206 apply (subgoal_tac
207 	 "T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X =
208 	  T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)")
209  apply simp
210 apply (blast intro: BsubX [THEN subsetD])
211 done
214 text{*Induction step for the main lemma*}
215 lemma progress_induction_step:
216   assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
217       and act:  "act \<in> Acts F"
218       and Xwens: "X \<in> wens_set F B"
219       and latt: "lattice C"
220       and  TC:  "T \<in> C"
221       and  BC:  "B \<in> C"
222       and clos: "closed F T B C"
223       and Fstable: "F \<in> stable T"
224   shows "T \<inter> wens F act X \<in> C"
225 proof -
226   from Xwens have BsubX: "B \<subseteq> X"
227     by (rule wens_set_imp_subset)
228   let ?r = "wens F act X"
229   have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X"
230     by (simp add: wens_unfold [symmetric])
231   then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)"
232     by blast
233   then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)"
234     by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast)
235   then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
236     by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
237   then have "cl C (T\<inter>?r) \<subseteq>
238              cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))"
239     by (rule cl_mono)
240   then have "cl C (T\<inter>?r) \<subseteq>
241              T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
242     by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
243   then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X"
244     by blast
245   then have "cl C (T\<inter>?r) \<subseteq> ?r"
246     by (blast intro!: subset_wens)
247   then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
248     by (simp add: Int_subset_iff cl_ident TC
249                   subset_trans [OF cl_mono [OF Int_lower1]])
250   show ?thesis
251     by (rule cl_subset_in_lattice [OF cl_subset latt])
252 qed
254 text{*Proved on page 96 of Meier's thesis.  The special case when
255    @{term "T=UNIV"} states that every progress set for the program @{term F}
256    and set @{term B} includes the set @{term "wens_set F B"}.*}
257 lemma progress_set_lemma:
258      "[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C"
259 apply (simp add: progress_set_def, clarify)
260 apply (erule wens_set.induct)
261   txt{*Base*}
263  txt{*The difficult @{term wens} case*}
265 txt{*Disjunctive case*}
266 apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C")
268 apply (blast intro: UN_in_lattice)
269 done
272 subsection {*The Progress Set Union Theorem*}
274 lemma closed_mono:
275   assumes BB':  "B \<subseteq> B'"
276       and TBwp: "T \<inter> (B \<union> wp act M) \<in> C"
277       and B'C:  "B' \<in> C"
278       and TC:   "T \<in> C"
279       and latt: "lattice C"
280   shows "T \<inter> (B' \<union> wp act M) \<in> C"
281 proof -
282   from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C"
284   then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C"
285     by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt)
286   show ?thesis
287     by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC],
288         blast intro: BB' [THEN subsetD])
289 qed
292 lemma progress_set_mono:
293     assumes BB':  "B \<subseteq> B'"
294     shows
295      "[| B' \<in> C;  C \<in> progress_set F T B|]
296       ==> C \<in> progress_set F T B'"
297 by (simp add: progress_set_def closed_def closed_mono [OF BB']
298                  subset_trans [OF BB'])
300 theorem progress_set_Union:
302       and prog: "C \<in> progress_set F T B"
303       and Fstable: "F \<in> stable T"
304       and BB':  "B \<subseteq> B'"
305       and B'C:  "B' \<in> C"
306       and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
307   shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
308 apply (insert prog Fstable)
310   apply (force simp add: progress_set_def awp_iff_stable [symmetric])
312 apply (drule progress_set_mono [OF BB' B'C])
313 apply (blast intro: progress_set_lemma Gco constrains_weaken_L
314                     BB' [THEN subsetD])
315 done
318 subsection {*Some Progress Sets*}
320 lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B"
321 by (simp add: progress_set_def lattice_def closed_def)
325 subsubsection {*Lattices and Relations*}
326 text{*From Meier's thesis, section 4.5.3*}
328 constdefs
329   relcl :: "'a set set => ('a * 'a) set"
330     -- {*Derived relation from a lattice*}
331     "relcl L == {(x,y). y \<in> cl L {x}}"
333   latticeof :: "('a * 'a) set => 'a set set"
334     -- {*Derived lattice from a relation: the set of upwards-closed sets*}
335     "latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r --> t \<in> X}"
338 lemma relcl_refl: "(a,a) \<in> relcl L"
339 by (simp add: relcl_def subset_cl [THEN subsetD])
341 lemma relcl_trans:
342      "[| (a,b) \<in> relcl L; (b,c) \<in> relcl L; lattice L |] ==> (a,c) \<in> relcl L"
344 apply (blast intro: clD cl_in_lattice)
345 done
347 lemma refl_relcl: "lattice L ==> refl (relcl L)"
348 by (simp add: refl_onI relcl_def subset_cl [THEN subsetD])
350 lemma trans_relcl: "lattice L ==> trans (relcl L)"
351 by (blast intro: relcl_trans transI)
353 lemma lattice_latticeof: "lattice (latticeof r)"
354 by (auto simp add: lattice_def latticeof_def)
356 lemma lattice_singletonI:
357      "[|lattice L; !!s. s \<in> X ==> {s} \<in> L|] ==> X \<in> L"
358 apply (cut_tac UN_singleton [of X])
359 apply (erule subst)
360 apply (simp only: UN_in_lattice)
361 done
363 text{*Equation (4.71) of Meier's thesis.  He gives no proof.*}
364 lemma cl_latticeof:
365      "[|refl r; trans r|]
366       ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}"
367 apply (rule equalityI)
368  apply (rule cl_least)
369   apply (simp (no_asm_use) add: latticeof_def trans_def, blast)
370  apply (simp add: latticeof_def refl_on_def, blast)
371 apply (simp add: latticeof_def, clarify)
372 apply (unfold cl_def, blast)
373 done
375 text{*Related to (4.71).*}
376 lemma cl_eq_Collect_relcl:
377      "lattice L ==> cl L X = {t. \<exists>s. s\<in>X & (s,t) \<in> relcl L}"
378 apply (cut_tac UN_singleton [of X])
379 apply (erule subst)
380 apply (force simp only: relcl_def cl_UN)
381 done
383 text{*Meier's theorem of section 4.5.3*}
384 theorem latticeof_relcl_eq: "lattice L ==> latticeof (relcl L) = L"
385 apply (rule equalityI)
386  prefer 2 apply (force simp add: latticeof_def relcl_def cl_def, clarify)
387 apply (rename_tac X)
388 apply (rule cl_subset_in_lattice)
389  prefer 2 apply assumption
390 apply (drule cl_ident_iff [OF lattice_latticeof, THEN iffD2])
391 apply (drule equalityD1)
392 apply (rule subset_trans)
393  prefer 2 apply assumption
394 apply (thin_tac "?U \<subseteq> X")
395 apply (cut_tac A=X in UN_singleton)
396 apply (erule subst)
397 apply (simp only: cl_UN lattice_latticeof
398                   cl_latticeof [OF refl_relcl trans_relcl])
400 done
402 theorem relcl_latticeof_eq:
403      "[|refl r; trans r|] ==> relcl (latticeof r) = r"
404 by (simp add: relcl_def cl_latticeof)
407 subsubsection {*Decoupling Theorems*}
409 constdefs
410   decoupled :: "['a program, 'a program] => bool"
411    "decoupled F G ==
412 	\<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)"
415 text{*Rao's Decoupling Theorem*}
416 lemma stableco: "F \<in> stable A ==> F \<in> A-B co A"
417 by (simp add: stable_def constrains_def, blast)
419 theorem decoupling:
421       and Gstable: "G \<in> stable B"
422       and dec:     "decoupled F G"
423   shows "F\<squnion>G \<in> A leadsTo B"
424 proof -
425   have prog: "{X. G \<in> stable X} \<in> progress_set F UNIV B"
426     by (simp add: progress_set_def lattice_stable Gstable closed_def
427                   stable_Un [OF Gstable] dec [unfolded decoupled_def])
428   have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B"
429     by (rule progress_set_Union [OF leadsTo prog],
431   thus ?thesis by simp
432 qed
435 text{*Rao's Weak Decoupling Theorem*}
436 theorem weak_decoupling:
438       and stable: "F\<squnion>G \<in> stable B"
439       and dec:     "decoupled F (F\<squnion>G)"
440   shows "F\<squnion>G \<in> A leadsTo B"
441 proof -
442   have prog: "{X. F\<squnion>G \<in> stable X} \<in> progress_set F UNIV B"
443     by (simp del: Join_stable
444              add: progress_set_def lattice_stable stable closed_def
445                   stable_Un [OF stable] dec [unfolded decoupled_def])
446   have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B"
447     by (rule progress_set_Union [OF leadsTo prog],
448         simp_all del: Join_stable add: stable,
450   thus ?thesis by simp
451 qed
453 text{*The ``Decoupling via @{term G'} Union Theorem''*}
454 theorem decoupling_via_aux:
456       and prog: "{X. G' \<in> stable X} \<in> progress_set F UNIV B"
457       and GG':  "G \<le> G'"
458                --{*Beware!  This is the converse of the refinement relation!*}
459   shows "F\<squnion>G \<in> A leadsTo B"
460 proof -
461   from prog have stable: "G' \<in> stable B"
463   have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B"
464     by (rule progress_set_Union [OF leadsTo prog],
465         simp_all add: stable stableco component_stable [OF GG'])
466   thus ?thesis by simp
467 qed
470 subsection{*Composition Theorems Based on Monotonicity and Commutativity*}
472 subsubsection{*Commutativity of @{term "cl L"} and assignment.*}
473 constdefs
474   commutes :: "['a program, 'a set, 'a set,  'a set set] => bool"
475    "commutes F T B L ==
476        \<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M -->
477            cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))"
480 text{*From Meier's thesis, section 4.5.6*}
481 lemma commutativity1_lemma:
482   assumes commutes: "commutes F T B L"
483       and lattice:  "lattice L"
484       and BL: "B \<in> L"
485       and TL: "T \<in> L"
486   shows "closed F T B L"
487 apply (simp add: closed_def, clarify)
488 apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])
489 apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff
490                  cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
491 apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))")
492  prefer 2
493  apply (cut_tac commutes, simp add: commutes_def)
494 apply (erule subset_trans)
496 apply (blast intro: rev_subsetD [OF _ wp_mono])
497 done
499 text{*Version packaged with @{thm progress_set_Union}*}
500 lemma commutativity1:
502       and lattice:  "lattice L"
503       and BL: "B \<in> L"
504       and TL: "T \<in> L"
505       and Fstable: "F \<in> stable T"
506       and Gco: "!!X. X\<in>L ==> G \<in> X-B co X"
507       and commutes: "commutes F T B L"
508   shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
509 by (rule progress_set_Union [OF leadsTo _ Fstable subset_refl BL Gco],
510     simp add: progress_set_def commutativity1_lemma commutes lattice BL TL)
514 text{*Possibly move to Relation.thy, after @{term single_valued}*}
515 constdefs
516   funof :: "[('a*'b)set, 'a] => 'b"
517    "funof r == (\<lambda>x. THE y. (x,y) \<in> r)"
519 lemma funof_eq: "[|single_valued r; (x,y) \<in> r|] ==> funof r x = y"
520 by (simp add: funof_def single_valued_def, blast)
522 lemma funof_Pair_in:
523      "[|single_valued r; x \<in> Domain r|] ==> (x, funof r x) \<in> r"
524 by (force simp add: funof_eq)
526 lemma funof_in:
527      "[|r``{x} \<subseteq> A; single_valued r; x \<in> Domain r|] ==> funof r x \<in> A"
528 by (force simp add: funof_eq)
530 lemma funof_imp_wp: "[|funof act t \<in> A; single_valued act|] ==> t \<in> wp act A"
531 by (force simp add: in_wp_iff funof_eq)
534 subsubsection{*Commutativity of Functions and Relation*}
535 text{*Thesis, page 109*}
537 (*FIXME: this proof is an ungodly mess*)
538 text{*From Meier's thesis, section 4.5.6*}
539 lemma commutativity2_lemma:
540   assumes dcommutes:
541         "\<forall>act \<in> Acts F.
542          \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L -->
543                       s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
544       and determ: "!!act. act \<in> Acts F ==> single_valued act"
545       and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
546       and lattice:  "lattice L"
547       and BL: "B \<in> L"
548       and TL: "T \<in> L"
549       and Fstable: "F \<in> stable T"
550   shows  "commutes F T B L"
551 apply (simp add: commutes_def del: Int_subset_iff, clarify)
552 apply (rename_tac t)
553 apply (subgoal_tac "\<exists>s. (s,t) \<in> relcl L & s \<in> T \<inter> wp act M")
554  prefer 2
555  apply (force simp add: cl_eq_Collect_relcl [OF lattice], simp, clarify)
556 apply (subgoal_tac "\<forall>u\<in>L. s \<in> u --> t \<in> u")
557  prefer 2
558  apply (intro ballI impI)
559  apply (subst cl_ident [symmetric], assumption)
561  apply (blast intro: cl_mono [THEN [2] rev_subsetD])
562 apply (subgoal_tac "funof act s \<in> T\<inter>M")
563  prefer 2
564  apply (cut_tac Fstable)
565  apply (force intro!: funof_in
566               simp add: wp_def stable_def constrains_def determ total)
567 apply (subgoal_tac "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L")
568  prefer 2
569  apply (rule dcommutes [rule_format], assumption+)
570 apply (subgoal_tac "t \<in> B | funof act t \<in> cl L (T\<inter>M)")
571  prefer 2
573  apply (blast intro: BL cl_mono [THEN [2] rev_subsetD])
574 apply (subgoal_tac "t \<in> B | t \<in> wp act (cl L (T\<inter>M))")
575  prefer 2
576  apply (blast intro: funof_imp_wp determ)
577 apply (blast intro: TL cl_mono [THEN [2] rev_subsetD])
578 done
581 text{*Version packaged with @{thm progress_set_Union}*}
582 lemma commutativity2:
584       and dcommutes:
585         "\<forall>act \<in> Acts F.
586          \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L -->
587                       s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
588       and determ: "!!act. act \<in> Acts F ==> single_valued act"
589       and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
590       and lattice:  "lattice L"
591       and BL: "B \<in> L"
592       and TL: "T \<in> L"
593       and Fstable: "F \<in> stable T"
594       and Gco: "!!X. X\<in>L ==> G \<in> X-B co X"
595   shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
596 apply (rule commutativity1 [OF leadsTo lattice])
597 apply (simp_all add: Gco commutativity2_lemma dcommutes determ total
598                      lattice BL TL Fstable)
599 done
602 subsection {*Monotonicity*}
603 text{*From Meier's thesis, section 4.5.7, page 110*}
604 (*to be continued?*)
606 end