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