src/HOL/UNITY/ProgressSets.thy
 author paulson Tue Mar 18 18:07:06 2003 +0100 (2003-03-18) changeset 13870 cf947d1ec5ff parent 13866 b42d7983a822 child 13874 0da2141606c6 permissions -rw-r--r--
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
to the new Group setup.

Deleted Ring, Module from GroupTheory

Minor UNITY changes
```     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. 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  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; F \<in> stable T|] ==> 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 Fstable: "F \<in> stable T"
```
```   282       and BB':  "B \<subseteq> B'"
```
```   283       and B'C:  "B' \<in> C"
```
```   284       and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
```
```   285       and leadsTo: "F \<in> A leadsTo B'"
```
```   286   shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
```
```   287 apply (insert prog Fstable)
```
```   288 apply (rule leadsTo_Join [OF leadsTo])
```
```   289   apply (force simp add: progress_set_def awp_iff_stable [symmetric])
```
```   290 apply (simp add: awp_iff_constrains)
```
```   291 apply (drule progress_set_mono [OF BB' B'C])
```
```   292 apply (blast intro: progress_set_lemma Gco constrains_weaken_L
```
```   293                     BB' [THEN subsetD])
```
```   294 done
```
```   295
```
```   296
```
```   297 subsection {*Some Progress Sets*}
```
```   298
```
```   299 lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B"
```
```   300 by (simp add: progress_set_def lattice_def closed_def)
```
```   301
```
```   302 end
```