src/HOL/UNITY/ProgressSets.thy
author paulson
Mon Mar 17 17:37:48 2003 +0100 (2003-03-17)
changeset 13866 b42d7983a822
parent 13861 0c18f31d901a
child 13870 cf947d1ec5ff
permissions -rw-r--r--
More "progress set" material
     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 lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)"
    89 by (simp add: cl_def, blast)
    90 
    91 lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s"
    92 apply (rule equalityI) 
    93  prefer 2 
    94   apply (simp add: cl_def, blast)
    95 apply (rule cl_least)
    96  apply (blast intro: Un_in_lattice cl_in_lattice)
    97 apply (blast intro: subset_cl [THEN subsetD])  
    98 done
    99 
   100 lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))"
   101 apply (rule equalityI) 
   102  prefer 2 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_idem [simp]: "cl L (cl L r) = cl L r"
   109 by (simp add: cl_def, blast)
   110 
   111 lemma cl_ident: "r\<in>L ==> cl L r = r" 
   112 by (force simp add: cl_def)
   113 
   114 text{*Assertion (4.62)*}
   115 lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)" 
   116 apply (rule iffI) 
   117  apply (erule subst)
   118  apply (erule cl_in_lattice)  
   119 apply (erule cl_ident) 
   120 done
   121 
   122 lemma cl_subset_in_lattice: "[|cl L r \<subseteq> r; lattice L|] ==> r\<in>L" 
   123 by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
   124 
   125 
   126 subsection {*Progress Sets and the Main Lemma*}
   127 
   128 constdefs 
   129   closed :: "['a program, 'a set, 'a set,  'a set set] => bool"
   130    "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
   131                               T \<inter> (B \<union> wp act M) \<in> L"
   132 
   133   progress_set :: "['a program, 'a set, 'a set] => 'a set set set"
   134    "progress_set F T B ==
   135       {L. F \<in> stable T & lattice L & B \<in> L & T \<in> L & closed F T B L}"
   136 
   137 lemma closedD:
   138    "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] 
   139     ==> T \<inter> (B \<union> wp act M) \<in> L"
   140 by (simp add: closed_def) 
   141 
   142 text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
   143 and @{term m} by @{term X}. *}
   144 
   145 text{*Part of the proof of the claim at the bottom of page 97.  It's
   146 proved separately because the argument requires a generalization over
   147 all @{term "act \<in> Acts F"}.*}
   148 lemma lattice_awp_lemma:
   149   assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
   150       and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
   151       and latt: "lattice C"
   152       and TC:   "T \<in> C"
   153       and BC:   "B \<in> C"
   154       and clos: "closed F T B C"
   155     shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C"
   156 apply (simp del: INT_simps add: awp_def INT_extend_simps) 
   157 apply (rule INT_in_lattice [OF latt]) 
   158 apply (erule closedD [OF clos]) 
   159 apply (simp add: subset_trans [OF BsubX Un_upper1]) 
   160 apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)")
   161  prefer 2 apply (blast intro: TC rev_subsetD [OF _ cl_least]) 
   162 apply (erule ssubst) 
   163 apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) 
   164 done
   165 
   166 text{*Remainder of the proof of the claim at the bottom of page 97.*}
   167 lemma lattice_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 act:  "act \<in> Acts F"
   171       and latt: "lattice C"
   172       and TC:   "T \<in> C"
   173       and BC:   "B \<in> C"
   174       and clos: "closed F T B C"
   175     shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C"
   176 apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C")
   177  prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
   178 apply (drule Int_in_lattice
   179               [OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
   180                     latt])
   181 apply (subgoal_tac
   182 	 "T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) = 
   183 	  T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))") 
   184  prefer 2 apply blast 
   185 apply simp  
   186 apply (drule Un_in_lattice [OF _ TXC latt])  
   187 apply (subgoal_tac
   188 	 "T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X = 
   189 	  T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)")
   190  apply simp 
   191 apply (blast intro: BsubX [THEN subsetD]) 
   192 done
   193 
   194 
   195 text{*Induction step for the main lemma*}
   196 lemma progress_induction_step:
   197   assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
   198       and act:  "act \<in> Acts F"
   199       and Xwens: "X \<in> wens_set F B"
   200       and latt: "lattice C"
   201       and  TC:  "T \<in> C"
   202       and  BC:  "B \<in> C"
   203       and clos: "closed F T B C"
   204       and Fstable: "F \<in> stable T"
   205   shows "T \<inter> wens F act X \<in> C"
   206 proof -
   207   from Xwens have BsubX: "B \<subseteq> X"
   208     by (rule wens_set_imp_subset) 
   209   let ?r = "wens F act X"
   210   have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X"
   211     by (simp add: wens_unfold [symmetric])
   212   then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)"
   213     by blast
   214   then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)"
   215     by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) 
   216   then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
   217     by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
   218   then have "cl C (T\<inter>?r) \<subseteq> 
   219              cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))"
   220     by (rule cl_mono) 
   221   then have "cl C (T\<inter>?r) \<subseteq> 
   222              T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
   223     by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
   224   then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X"
   225     by blast
   226   then have "cl C (T\<inter>?r) \<subseteq> ?r"
   227     by (blast intro!: subset_wens) 
   228   then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
   229     by (simp add: Int_subset_iff cl_ident TC
   230                   subset_trans [OF cl_mono [OF Int_lower1]]) 
   231   show ?thesis
   232     by (rule cl_subset_in_lattice [OF cl_subset latt]) 
   233 qed
   234 
   235 text{*The Lemma proved on page 96*}
   236 lemma progress_set_lemma:
   237      "[|C \<in> progress_set F T B; r \<in> wens_set F B|] ==> T\<inter>r \<in> C"
   238 apply (simp add: progress_set_def, clarify) 
   239 apply (erule wens_set.induct) 
   240   txt{*Base*}
   241   apply (simp add: Int_in_lattice) 
   242  txt{*The difficult @{term wens} case*}
   243  apply (simp add: progress_induction_step) 
   244 txt{*Disjunctive case*}
   245 apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 
   246  apply (simp add: Int_Union) 
   247 apply (blast intro: UN_in_lattice) 
   248 done
   249 
   250 
   251 subsection {*The Progress Set Union Theorem*}
   252 
   253 lemma closed_mono:
   254   assumes BB':  "B \<subseteq> B'"
   255       and TBwp: "T \<inter> (B \<union> wp act M) \<in> C"
   256       and B'C:  "B' \<in> C"
   257       and TC:   "T \<in> C"
   258       and latt: "lattice C"
   259   shows "T \<inter> (B' \<union> wp act M) \<in> C"
   260 proof -
   261   from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C"
   262     by (simp add: Int_Un_distrib)
   263   then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C"
   264     by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt) 
   265   show ?thesis
   266     by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC], 
   267         blast intro: BB' [THEN subsetD]) 
   268 qed
   269 
   270 
   271 lemma progress_set_mono:
   272     assumes BB':  "B \<subseteq> B'"
   273     shows
   274      "[| B' \<in> C;  C \<in> progress_set F T B|] 
   275       ==> C \<in> progress_set F T B'"
   276 by (simp add: progress_set_def closed_def closed_mono [OF BB'] 
   277                  subset_trans [OF BB']) 
   278 
   279 theorem progress_set_Union:
   280   assumes prog: "C \<in> progress_set F T B"
   281       and BB':  "B \<subseteq> B'"
   282       and B'C:  "B' \<in> C"
   283       and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
   284       and leadsTo: "F \<in> A leadsTo B'"
   285   shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
   286 apply (insert prog) 
   287 apply (rule leadsTo_Join [OF leadsTo]) 
   288   apply (force simp add: progress_set_def awp_iff_stable [symmetric]) 
   289 apply (simp add: awp_iff_constrains)
   290 apply (drule progress_set_mono [OF BB' B'C]) 
   291 apply (blast intro: progress_set_lemma Gco constrains_weaken_L 
   292                     BB' [THEN subsetD]) 
   293 done
   294 
   295 end