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