src/HOL/UNITY/ProgressSets.thy
 author paulson Fri Mar 14 10:30:46 2003 +0100 (2003-03-14) changeset 13861 0c18f31d901a parent 13853 89131afa9f01 child 13866 b42d7983a822 permissions -rw-r--r--
Proved the main lemma on progress sets
```     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 constdefs
```
```    22   lattice :: "'a set set => bool"
```
```    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   cl :: "['a set set, 'a set] => 'a set"
```
```    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: Set.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 lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)"
```
```    87 by (simp add: cl_def, blast)
```
```    88
```
```    89 lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s"
```
```    90 apply (rule equalityI)
```
```    91  prefer 2
```
```    92   apply (simp add: cl_def, blast)
```
```    93 apply (rule cl_least)
```
```    94  apply (blast intro: Un_in_lattice cl_in_lattice)
```
```    95 apply (blast intro: subset_cl [THEN subsetD])
```
```    96 done
```
```    97
```
```    98 lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))"
```
```    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_idem [simp]: "cl L (cl L r) = cl L r"
```
```   108 by (simp add: cl_def, blast)
```
```   109
```
```   110 lemma cl_ident: "r\<in>L ==> cl L r = r"
```
```   111 by (force simp add: cl_def)
```
```   112
```
```   113 text{*Assertion (4.62)*}
```
```   114 lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)"
```
```   115 apply (rule iffI)
```
```   116  apply (erule subst)
```
```   117  apply (erule cl_in_lattice)
```
```   118 apply (erule cl_ident)
```
```   119 done
```
```   120
```
```   121 lemma cl_subset_in_lattice: "[|cl L r \<subseteq> r; lattice L|] ==> r\<in>L"
```
```   122 by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
```
```   123
```
```   124
```
```   125 constdefs
```
```   126   closed :: "['a program, 'a set, 'a set,  'a set set] => bool"
```
```   127    "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
```
```   128                               T \<inter> (B \<union> wp act M) \<in> L"
```
```   129
```
```   130   progress_set :: "['a program, 'a set, 'a set] => 'a set set set"
```
```   131    "progress_set F T B ==
```
```   132       {L. F \<in> stable T & lattice L & B \<in> L & T \<in> L & closed F T B L}"
```
```   133
```
```   134 lemma closedD:
```
```   135    "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|]
```
```   136     ==> T \<inter> (B \<union> wp act M) \<in> L"
```
```   137 by (simp add: closed_def)
```
```   138
```
```   139 lemma lattice_awp_lemma:
```
```   140   assumes tmc:  "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
```
```   141       and qsm:  "q \<subseteq> m"   --{*holds in inductive step*}
```
```   142       and latt: "lattice C"
```
```   143       and tc:   "T \<in> C"
```
```   144       and qc:   "q \<in> C"
```
```   145       and clos: "closed F T q C"
```
```   146     shows "T \<inter> (q \<union> awp F (m \<union> cl C (T\<inter>r))) \<in> C"
```
```   147 apply (simp del: INT_simps add: awp_def INT_extend_simps)
```
```   148 apply (rule INT_in_lattice [OF latt])
```
```   149 apply (erule closedD [OF clos])
```
```   150 apply (simp add: subset_trans [OF qsm Un_upper1])
```
```   151 apply (subgoal_tac "T \<inter> (m \<union> cl C (T\<inter>r)) = (T\<inter>m) \<union> cl C (T\<inter>r)")
```
```   152  prefer 2 apply (blast intro: tc rev_subsetD [OF _ cl_least])
```
```   153 apply (erule ssubst)
```
```   154 apply (blast intro: Un_in_lattice latt cl_in_lattice tmc)
```
```   155 done
```
```   156
```
```   157 lemma lattice_lemma:
```
```   158   assumes tmc:  "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
```
```   159       and qsm:  "q \<subseteq> m"   --{*holds in inductive step*}
```
```   160       and act:  "act \<in> Acts F"
```
```   161       and latt: "lattice C"
```
```   162       and tc:   "T \<in> C"
```
```   163       and qc:   "q \<in> C"
```
```   164       and clos: "closed F T q C"
```
```   165     shows "T \<inter> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)) \<union> m) \<in> C"
```
```   166 apply (subgoal_tac "T \<inter> (q \<union> wp act m) \<in> C")
```
```   167  prefer 2 apply (simp add: closedD [OF clos] act qsm tmc)
```
```   168 apply (drule Int_in_lattice
```
```   169               [OF _ lattice_awp_lemma [OF tmc qsm latt tc qc clos, of r]
```
```   170                     latt])
```
```   171 apply (subgoal_tac
```
```   172 	 "T \<inter> (q \<union> wp act m) \<inter> (T \<inter> (q \<union> awp F (m \<union> cl C (T\<inter>r)))) =
```
```   173 	  T \<inter> (q \<union> wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)))")
```
```   174  prefer 2 apply blast
```
```   175 apply simp
```
```   176 apply (drule Un_in_lattice [OF _ tmc latt])
```
```   177 apply (subgoal_tac
```
```   178 	 "T \<inter> (q \<union> wp act m \<inter> awp F (m \<union> cl C (T\<inter>r))) \<union> T\<inter>m =
```
```   179 	  T \<inter> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)) \<union> m)")
```
```   180  prefer 2 apply (blast intro: qsm [THEN subsetD], simp)
```
```   181 done
```
```   182
```
```   183
```
```   184 lemma progress_induction_step:
```
```   185   assumes tmc:  "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
```
```   186       and act:  "act \<in> Acts F"
```
```   187       and mwens: "m \<in> wens_set F q"
```
```   188       and latt: "lattice C"
```
```   189       and  tc:  "T \<in> C"
```
```   190       and  qc:  "q \<in> C"
```
```   191       and clos: "closed F T q C"
```
```   192       and Fstable: "F \<in> stable T"
```
```   193   shows "T \<inter> wens F act m \<in> C"
```
```   194 proof -
```
```   195 from mwens have qsm: "q \<subseteq> m"
```
```   196  by (rule wens_set_imp_subset)
```
```   197 let ?r = "wens F act m"
```
```   198 have "?r \<subseteq> (wp act m \<inter> awp F (m\<union>?r)) \<union> m"
```
```   199  by (simp add: wens_unfold [symmetric])
```
```   200 then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (m\<union>?r)) \<union> m)"
```
```   201  by blast
```
```   202 then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (T \<inter> (m\<union>?r))) \<union> m)"
```
```   203  by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast)
```
```   204 then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m)"
```
```   205  by (blast intro: awp_mono [THEN  rev_subsetD] subset_cl [THEN subsetD])
```
```   206 then have "cl C (T\<inter>?r) \<subseteq>
```
```   207            cl C (T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m))"
```
```   208  by (rule cl_mono)
```
```   209 then have "cl C (T\<inter>?r) \<subseteq>
```
```   210            T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m)"
```
```   211  by (simp add: cl_ident lattice_lemma [OF tmc qsm act latt tc qc clos])
```
```   212 then have "cl C (T\<inter>?r) \<subseteq> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m"
```
```   213  by blast
```
```   214 then have "cl C (T\<inter>?r) \<subseteq> ?r"
```
```   215  by (blast intro!: subset_wens)
```
```   216 then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
```
```   217  by (simp add: Int_subset_iff cl_ident tc
```
```   218                subset_trans [OF cl_mono [OF Int_lower1]])
```
```   219 show ?thesis
```
```   220  by (rule cl_subset_in_lattice [OF cl_subset latt])
```
```   221 qed
```
```   222
```
```   223
```
```   224 lemma progress_set_lemma:
```
```   225       "[|C \<in> progress_set F T B; r \<in> wens_set F B|] ==> T\<inter>r \<in> C"
```
```   226 apply (simp add: progress_set_def, clarify)
```
```   227 apply (erule wens_set.induct)
```
```   228   txt{*Base*}
```
```   229   apply (simp add: Int_in_lattice)
```
```   230  txt{*The difficult @{term wens} case*}
```
```   231  apply (simp add: progress_induction_step)
```
```   232 txt{*Disjunctive case*}
```
```   233 apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C")
```
```   234  apply (simp add: Int_Union)
```
```   235 apply (blast intro: UN_in_lattice)
```
```   236 done
```
```   237
```
```   238 end
```