src/HOL/UNITY/ProgressSets.thy
author paulson
Mon Mar 31 12:29:54 2003 +0200 (2003-03-31)
changeset 13888 16f424af58a2
parent 13885 de6fac7d5351
child 14150 9a23e4eb5eb3
permissions -rw-r--r--
more comments and tweaks
     1 (*  Title:      HOL/UNITY/ProgressSets
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   2003  University of Cambridge
     5 
     6 Progress Sets.  From 
     7 
     8     David Meier and Beverly Sanders,
     9     Composing Leads-to Properties
    10     Theoretical Computer Science 243:1-2 (2000), 339-361.
    11 
    12     David Meier,
    13     Progress Properties in Program Refinement and Parallel Composition
    14     Swiss Federal Institute of Technology Zurich (1997)
    15 *)
    16 
    17 header{*Progress Sets*}
    18 
    19 theory ProgressSets = Transformers:
    20 
    21 subsection {*Complete Lattices and the Operator @{term cl}*}
    22 
    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)"
    28 
    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}"
    32 
    33 lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L"
    34 by (force simp add: lattice_def)
    35 
    36 lemma empty_in_lattice: "lattice L ==> {} \<in> L"
    37 by (force simp add: lattice_def)
    38 
    39 lemma Union_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Union>M \<in> L"
    40 by (simp add: lattice_def)
    41 
    42 lemma Inter_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Inter>M \<in> L"
    43 by (simp add: lattice_def)
    44 
    45 lemma UN_in_lattice:
    46      "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
    47 apply (simp add: Set.UN_eq) 
    48 apply (blast intro: Union_in_lattice) 
    49 done
    50 
    51 lemma INT_in_lattice:
    52      "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i)  \<in> L"
    53 apply (simp add: INT_eq) 
    54 apply (blast intro: Inter_in_lattice) 
    55 done
    56 
    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
    61 
    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
    66 
    67 lemma lattice_stable: "lattice {X. F \<in> stable X}"
    68 by (simp add: lattice_def stable_def constrains_def, blast)
    69 
    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
    77 
    78 lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c" 
    79 by (force simp add: cl_def)
    80 
    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)
    84 
    85 lemma subset_cl: "r \<subseteq> cl L r"
    86 by (simp add: cl_def, blast)
    87 
    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)
    91 
    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)
    95 
    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)
    98 
    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
   107 
   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
   115 
   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)
   118 
   119 lemma cl_idem [simp]: "cl L (cl L r) = cl L r"
   120 by (simp add: cl_def, blast)
   121 
   122 lemma cl_ident: "r\<in>L ==> cl L r = r" 
   123 by (force simp add: cl_def)
   124 
   125 lemma cl_empty [simp]: "lattice L ==> cl L {} = {}"
   126 by (simp add: cl_ident empty_in_lattice)
   127 
   128 lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV"
   129 by (simp add: cl_ident UNIV_in_lattice)
   130 
   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
   138 
   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)
   141 
   142 
   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"}.*}
   146 
   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"
   151 
   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}"
   155 
   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"
   159 by (simp add: closed_def) 
   160 
   161 text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
   162 and @{term m} by @{term X}. *}
   163 
   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
   184 
   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
   212 
   213 
   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
   253 
   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*}
   262   apply (simp add: Int_in_lattice) 
   263  txt{*The difficult @{term wens} case*}
   264  apply (simp add: progress_induction_step) 
   265 txt{*Disjunctive case*}
   266 apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 
   267  apply (simp add: Int_Union) 
   268 apply (blast intro: UN_in_lattice) 
   269 done
   270 
   271 
   272 subsection {*The Progress Set Union Theorem*}
   273 
   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"
   283     by (simp add: Int_Un_distrib)
   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
   290 
   291 
   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']) 
   299 
   300 theorem progress_set_Union:
   301   assumes leadsTo: "F \<in> A leadsTo B'"
   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) 
   309 apply (rule leadsTo_Join [OF leadsTo]) 
   310   apply (force simp add: progress_set_def awp_iff_stable [symmetric]) 
   311 apply (simp add: awp_iff_constrains)
   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
   316 
   317 
   318 subsection {*Some Progress Sets*}
   319 
   320 lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B"
   321 by (simp add: progress_set_def lattice_def closed_def)
   322 
   323 
   324 
   325 subsubsection {*Lattices and Relations*}
   326 text{*From Meier's thesis, section 4.5.3*}
   327 
   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}}"
   332   
   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}"
   336 
   337 
   338 lemma relcl_refl: "(a,a) \<in> relcl L"
   339 by (simp add: relcl_def subset_cl [THEN subsetD])
   340 
   341 lemma relcl_trans:
   342      "[| (a,b) \<in> relcl L; (b,c) \<in> relcl L; lattice L |] ==> (a,c) \<in> relcl L"
   343 apply (simp add: relcl_def)
   344 apply (blast intro: clD cl_in_lattice)
   345 done
   346 
   347 lemma refl_relcl: "lattice L ==> refl UNIV (relcl L)"
   348 by (simp add: reflI relcl_def subset_cl [THEN subsetD])
   349 
   350 lemma trans_relcl: "lattice L ==> trans (relcl L)"
   351 by (blast intro: relcl_trans transI)
   352 
   353 lemma lattice_latticeof: "lattice (latticeof r)"
   354 by (auto simp add: lattice_def latticeof_def)
   355 
   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
   362 
   363 text{*Equation (4.71) of Meier's thesis.  He gives no proof.*}
   364 lemma cl_latticeof:
   365      "[|refl UNIV 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_def, blast)
   371 apply (simp add: latticeof_def, clarify)
   372 apply (unfold cl_def, blast) 
   373 done
   374 
   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
   382 
   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]) 
   399 apply (simp add: relcl_def) 
   400 done
   401 
   402 theorem relcl_latticeof_eq:
   403      "[|refl UNIV r; trans r|] ==> relcl (latticeof r) = r"
   404 by (simp add: relcl_def cl_latticeof, blast)
   405 
   406 
   407 subsubsection {*Decoupling Theorems*}
   408 
   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)"
   413 
   414 
   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) 
   418 
   419 theorem decoupling:
   420   assumes leadsTo: "F \<in> A leadsTo B"
   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],
   430         simp_all add: Gstable stableco)
   431   thus ?thesis by simp
   432 qed
   433 
   434 
   435 text{*Rao's Weak Decoupling Theorem*}
   436 theorem weak_decoupling:
   437   assumes leadsTo: "F \<in> A leadsTo B"
   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,
   449         simp add: stableco) 
   450   thus ?thesis by simp
   451 qed
   452 
   453 text{*The ``Decoupling via @{term G'} Union Theorem''*}
   454 theorem decoupling_via_aux:
   455   assumes leadsTo: "F \<in> A leadsTo B"
   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"
   462     by (simp add: progress_set_def)
   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
   468 
   469 
   470 subsection{*Composition Theorems Based on Monotonicity and Commutativity*}
   471 
   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)))"
   478 
   479 
   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 (simp add: commutes [unfolded commutes_def]) 
   494 apply (erule subset_trans) 
   495 apply (simp add: cl_ident)
   496 apply (blast intro: rev_subsetD [OF _ wp_mono]) 
   497 done
   498 
   499 text{*Version packaged with @{thm progress_set_Union}*}
   500 lemma commutativity1:
   501   assumes leadsTo: "F \<in> A leadsTo B"
   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) 
   511 
   512 
   513 
   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)"
   518 
   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)
   521 
   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) 
   525 
   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)
   529  
   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)
   532 
   533 
   534 subsubsection{*Commutativity of Functions and Relation*}
   535 text{*Thesis, page 109*}
   536 
   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, 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)
   560  apply (simp add: relcl_def)  
   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 
   572  apply (simp add: relcl_def)
   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
   579 
   580 
   581 text{*Version packaged with @{thm progress_set_Union}*}
   582 lemma commutativity2:
   583   assumes leadsTo: "F \<in> A leadsTo B"
   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
   600 
   601 
   602 subsection {*Monotonicity*}
   603 (*to be continued?*)
   604 
   605 end