Proved the main lemma on progress sets
authorpaulson
Fri Mar 14 10:30:46 2003 +0100 (2003-03-14)
changeset 138610c18f31d901a
parent 13860 b681a3cb0beb
child 13862 7cbc89aa79db
Proved the main lemma on progress sets
src/HOL/UNITY/ProgressSets.thy
src/HOL/UNITY/Transformers.thy
src/HOL/UNITY/UNITY.thy
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Fri Mar 14 10:30:15 2003 +0100
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Fri Mar 14 10:30:46 2003 +0100
     1.3 @@ -8,6 +8,10 @@
     1.4      David Meier and Beverly Sanders,
     1.5      Composing Leads-to Properties
     1.6      Theoretical Computer Science 243:1-2 (2000), 339-361.
     1.7 +
     1.8 +    David Meier,
     1.9 +    Progress Properties in Program Refinement and Parallel Composition
    1.10 +    Swiss Federal Institute of Technology Zurich (1997)
    1.11  *)
    1.12  
    1.13  header{*Progress Sets*}
    1.14 @@ -15,102 +19,220 @@
    1.15  theory ProgressSets = Transformers:
    1.16  
    1.17  constdefs
    1.18 -  closure_set :: "'a set set => bool"
    1.19 -   "closure_set C ==
    1.20 -	 (\<forall>D. D \<subseteq> C --> \<Inter>D \<in> C) & (\<forall>D. D \<subseteq> C --> \<Union>D \<in> C)"
    1.21 +  lattice :: "'a set set => bool"
    1.22 +   --{*Meier calls them closure sets, but they are just complete lattices*}
    1.23 +   "lattice L ==
    1.24 +	 (\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)"
    1.25  
    1.26    cl :: "['a set set, 'a set] => 'a set"
    1.27     --{*short for ``closure''*}
    1.28 -   "cl C r == \<Inter>{x. x\<in>C & r \<subseteq> x}"
    1.29 +   "cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}"
    1.30  
    1.31 -lemma UNIV_in_closure_set: "closure_set C ==> UNIV \<in> C"
    1.32 -by (force simp add: closure_set_def)
    1.33 +lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L"
    1.34 +by (force simp add: lattice_def)
    1.35  
    1.36 -lemma empty_in_closure_set: "closure_set C ==> {} \<in> C"
    1.37 -by (force simp add: closure_set_def)
    1.38 +lemma empty_in_lattice: "lattice L ==> {} \<in> L"
    1.39 +by (force simp add: lattice_def)
    1.40  
    1.41 -lemma Union_in_closure_set: "[|D \<subseteq> C; closure_set C|] ==> \<Union>D \<in> C"
    1.42 -by (simp add: closure_set_def)
    1.43 +lemma Union_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Union>M \<in> L"
    1.44 +by (simp add: lattice_def)
    1.45  
    1.46 -lemma Inter_in_closure_set: "[|D \<subseteq> C; closure_set C|] ==> \<Inter>D \<in> C"
    1.47 -by (simp add: closure_set_def)
    1.48 +lemma Inter_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Inter>M \<in> L"
    1.49 +by (simp add: lattice_def)
    1.50  
    1.51 -lemma UN_in_closure_set:
    1.52 -     "[|closure_set C; !!i. i\<in>I ==> r i \<in> C|] ==> (\<Union>i\<in>I. r i) \<in> C"
    1.53 +lemma UN_in_lattice:
    1.54 +     "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
    1.55  apply (simp add: Set.UN_eq) 
    1.56 -apply (blast intro: Union_in_closure_set) 
    1.57 +apply (blast intro: Union_in_lattice) 
    1.58  done
    1.59  
    1.60 -lemma IN_in_closure_set:
    1.61 -     "[|closure_set C; !!i. i\<in>I ==> r i \<in> C|] ==> (\<Inter>i\<in>I. r i)  \<in> C"
    1.62 +lemma INT_in_lattice:
    1.63 +     "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i)  \<in> L"
    1.64  apply (simp add: INT_eq) 
    1.65 -apply (blast intro: Inter_in_closure_set) 
    1.66 +apply (blast intro: Inter_in_lattice) 
    1.67  done
    1.68  
    1.69 -lemma Un_in_closure_set: "[|x\<in>C; y\<in>C; closure_set C|] ==> x\<union>y \<in> C"
    1.70 +lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L"
    1.71  apply (simp only: Un_eq_Union) 
    1.72 -apply (blast intro: Union_in_closure_set) 
    1.73 +apply (blast intro: Union_in_lattice) 
    1.74  done
    1.75  
    1.76 -lemma Int_in_closure_set: "[|x\<in>C; y\<in>C; closure_set C|] ==> x\<inter>y \<in> C"
    1.77 +lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L"
    1.78  apply (simp only: Int_eq_Inter) 
    1.79 -apply (blast intro: Inter_in_closure_set) 
    1.80 +apply (blast intro: Inter_in_lattice) 
    1.81  done
    1.82  
    1.83 -lemma closure_set_stable: "closure_set {X. F \<in> stable X}"
    1.84 -by (simp add: closure_set_def stable_def constrains_def, blast)
    1.85 +lemma lattice_stable: "lattice {X. F \<in> stable X}"
    1.86 +by (simp add: lattice_def stable_def constrains_def, blast)
    1.87  
    1.88 -text{*The next three results state that @{term "cl C r"} is the minimal
    1.89 - element of @{term C} that includes @{term r}.*}
    1.90 -lemma cl_in_closure_set: "closure_set C ==> cl C r \<in> C"
    1.91 -apply (simp add: closure_set_def cl_def)
    1.92 +text{*The next three results state that @{term "cl L r"} is the minimal
    1.93 + element of @{term L} that includes @{term r}.*}
    1.94 +lemma cl_in_lattice: "lattice L ==> cl L r \<in> L"
    1.95 +apply (simp add: lattice_def cl_def)
    1.96  apply (erule conjE)  
    1.97  apply (drule spec, erule mp, blast) 
    1.98  done
    1.99  
   1.100 -lemma cl_least: "[|c\<in>C; r\<subseteq>c|] ==> cl C r \<subseteq> c" 
   1.101 +lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c" 
   1.102  by (force simp add: cl_def)
   1.103  
   1.104  text{*The next three lemmas constitute assertion (4.61)*}
   1.105 -lemma cl_mono: "r \<subseteq> r' ==> cl C r \<subseteq> cl C r'"
   1.106 +lemma cl_mono: "r \<subseteq> r' ==> cl L r \<subseteq> cl L r'"
   1.107 +by (simp add: cl_def, blast)
   1.108 +
   1.109 +lemma subset_cl: "r \<subseteq> cl L r"
   1.110 +by (simp add: cl_def, blast)
   1.111 +
   1.112 +lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)"
   1.113  by (simp add: cl_def, blast)
   1.114  
   1.115 -lemma subset_cl: "r \<subseteq> cl C r"
   1.116 -by (simp add: cl_def, blast)
   1.117 +lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s"
   1.118 +apply (rule equalityI) 
   1.119 + prefer 2 
   1.120 +  apply (simp add: cl_def, blast)
   1.121 +apply (rule cl_least)
   1.122 + apply (blast intro: Un_in_lattice cl_in_lattice)
   1.123 +apply (blast intro: subset_cl [THEN subsetD])  
   1.124 +done
   1.125  
   1.126 -lemma cl_UN_subset: "(\<Union>i\<in>I. cl C (r i)) \<subseteq> cl C (\<Union>i\<in>I. r i)"
   1.127 -by (simp add: cl_def, blast)
   1.128 -
   1.129 -lemma cl_Un: "closure_set C ==> cl C (r\<union>s) = cl C r \<union> cl C s"
   1.130 +lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))"
   1.131  apply (rule equalityI) 
   1.132   prefer 2 
   1.133    apply (simp add: cl_def, blast)
   1.134  apply (rule cl_least)
   1.135 - apply (blast intro: Un_in_closure_set cl_in_closure_set)
   1.136 -apply (blast intro: subset_cl [THEN subsetD])  
   1.137 -done
   1.138 -
   1.139 -lemma cl_UN: "closure_set C ==> cl C (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl C (r i))"
   1.140 -apply (rule equalityI) 
   1.141 - prefer 2 
   1.142 -  apply (simp add: cl_def, blast)
   1.143 -apply (rule cl_least)
   1.144 - apply (blast intro: UN_in_closure_set cl_in_closure_set)
   1.145 + apply (blast intro: UN_in_lattice cl_in_lattice)
   1.146  apply (blast intro: subset_cl [THEN subsetD])  
   1.147  done
   1.148  
   1.149 -lemma cl_idem [simp]: "cl C (cl C r) = cl C r"
   1.150 +lemma cl_idem [simp]: "cl L (cl L r) = cl L r"
   1.151  by (simp add: cl_def, blast)
   1.152  
   1.153 -lemma cl_ident: "r\<in>C ==> cl C r = r" 
   1.154 +lemma cl_ident: "r\<in>L ==> cl L r = r" 
   1.155  by (force simp add: cl_def)
   1.156  
   1.157  text{*Assertion (4.62)*}
   1.158 -lemma cl_ident_iff: "closure_set C ==> (cl C r = r) = (r\<in>C)" 
   1.159 +lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)" 
   1.160  apply (rule iffI) 
   1.161   apply (erule subst)
   1.162 - apply (erule cl_in_closure_set)  
   1.163 + apply (erule cl_in_lattice)  
   1.164  apply (erule cl_ident) 
   1.165  done
   1.166  
   1.167 +lemma cl_subset_in_lattice: "[|cl L r \<subseteq> r; lattice L|] ==> r\<in>L" 
   1.168 +by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
   1.169 +
   1.170 +
   1.171 +constdefs 
   1.172 +  closed :: "['a program, 'a set, 'a set,  'a set set] => bool"
   1.173 +   "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
   1.174 +                              T \<inter> (B \<union> wp act M) \<in> L"
   1.175 +
   1.176 +  progress_set :: "['a program, 'a set, 'a set] => 'a set set set"
   1.177 +   "progress_set F T B ==
   1.178 +      {L. F \<in> stable T & lattice L & B \<in> L & T \<in> L & closed F T B L}"
   1.179 +
   1.180 +lemma closedD:
   1.181 +   "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] 
   1.182 +    ==> T \<inter> (B \<union> wp act M) \<in> L"
   1.183 +by (simp add: closed_def) 
   1.184 +
   1.185 +lemma lattice_awp_lemma:
   1.186 +  assumes tmc:  "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
   1.187 +      and qsm:  "q \<subseteq> m"   --{*holds in inductive step*}
   1.188 +      and latt: "lattice C"
   1.189 +      and tc:   "T \<in> C"
   1.190 +      and qc:   "q \<in> C"
   1.191 +      and clos: "closed F T q C"
   1.192 +    shows "T \<inter> (q \<union> awp F (m \<union> cl C (T\<inter>r))) \<in> C"
   1.193 +apply (simp del: INT_simps add: awp_def INT_extend_simps) 
   1.194 +apply (rule INT_in_lattice [OF latt]) 
   1.195 +apply (erule closedD [OF clos]) 
   1.196 +apply (simp add: subset_trans [OF qsm Un_upper1]) 
   1.197 +apply (subgoal_tac "T \<inter> (m \<union> cl C (T\<inter>r)) = (T\<inter>m) \<union> cl C (T\<inter>r)")
   1.198 + prefer 2 apply (blast intro: tc rev_subsetD [OF _ cl_least]) 
   1.199 +apply (erule ssubst) 
   1.200 +apply (blast intro: Un_in_lattice latt cl_in_lattice tmc) 
   1.201 +done
   1.202 +
   1.203 +lemma lattice_lemma:
   1.204 +  assumes tmc:  "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
   1.205 +      and qsm:  "q \<subseteq> m"   --{*holds in inductive step*}
   1.206 +      and act:  "act \<in> Acts F"
   1.207 +      and latt: "lattice C"
   1.208 +      and tc:   "T \<in> C"
   1.209 +      and qc:   "q \<in> C"
   1.210 +      and clos: "closed F T q C"
   1.211 +    shows "T \<inter> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)) \<union> m) \<in> C"
   1.212 +apply (subgoal_tac "T \<inter> (q \<union> wp act m) \<in> C")
   1.213 + prefer 2 apply (simp add: closedD [OF clos] act qsm tmc)
   1.214 +apply (drule Int_in_lattice
   1.215 +              [OF _ lattice_awp_lemma [OF tmc qsm latt tc qc clos, of r]
   1.216 +                    latt])
   1.217 +apply (subgoal_tac
   1.218 +	 "T \<inter> (q \<union> wp act m) \<inter> (T \<inter> (q \<union> awp F (m \<union> cl C (T\<inter>r)))) = 
   1.219 +	  T \<inter> (q \<union> wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)))") 
   1.220 + prefer 2 apply blast 
   1.221 +apply simp  
   1.222 +apply (drule Un_in_lattice [OF _ tmc latt]) 
   1.223 +apply (subgoal_tac
   1.224 +	 "T \<inter> (q \<union> wp act m \<inter> awp F (m \<union> cl C (T\<inter>r))) \<union> T\<inter>m = 
   1.225 +	  T \<inter> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)) \<union> m)")
   1.226 + prefer 2 apply (blast intro: qsm [THEN subsetD], simp) 
   1.227 +done
   1.228 +
   1.229 +
   1.230 +lemma progress_induction_step:
   1.231 +  assumes tmc:  "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
   1.232 +      and act:  "act \<in> Acts F"
   1.233 +      and mwens: "m \<in> wens_set F q"
   1.234 +      and latt: "lattice C"
   1.235 +      and  tc:  "T \<in> C"
   1.236 +      and  qc:  "q \<in> C"
   1.237 +      and clos: "closed F T q C"
   1.238 +      and Fstable: "F \<in> stable T"
   1.239 +  shows "T \<inter> wens F act m \<in> C"
   1.240 +proof -
   1.241 +from mwens have qsm: "q \<subseteq> m"
   1.242 + by (rule wens_set_imp_subset) 
   1.243 +let ?r = "wens F act m"
   1.244 +have "?r \<subseteq> (wp act m \<inter> awp F (m\<union>?r)) \<union> m"
   1.245 + by (simp add: wens_unfold [symmetric])
   1.246 +then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (m\<union>?r)) \<union> m)"
   1.247 + by blast
   1.248 +then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (T \<inter> (m\<union>?r))) \<union> m)"
   1.249 + by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) 
   1.250 +then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m)"
   1.251 + by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
   1.252 +then have "cl C (T\<inter>?r) \<subseteq> 
   1.253 +           cl C (T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m))"
   1.254 + by (rule cl_mono) 
   1.255 +then have "cl C (T\<inter>?r) \<subseteq> 
   1.256 +           T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m)"
   1.257 + by (simp add: cl_ident lattice_lemma [OF tmc qsm act latt tc qc clos])
   1.258 +then have "cl C (T\<inter>?r) \<subseteq> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m"
   1.259 + by blast
   1.260 +then have "cl C (T\<inter>?r) \<subseteq> ?r"
   1.261 + by (blast intro!: subset_wens) 
   1.262 +then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
   1.263 + by (simp add: Int_subset_iff cl_ident tc
   1.264 +               subset_trans [OF cl_mono [OF Int_lower1]]) 
   1.265 +show ?thesis
   1.266 + by (rule cl_subset_in_lattice [OF cl_subset latt]) 
   1.267 +qed
   1.268 +
   1.269 +
   1.270 +lemma progress_set_lemma:
   1.271 +      "[|C \<in> progress_set F T B; r \<in> wens_set F B|] ==> T\<inter>r \<in> C"
   1.272 +apply (simp add: progress_set_def, clarify) 
   1.273 +apply (erule wens_set.induct) 
   1.274 +  txt{*Base*}
   1.275 +  apply (simp add: Int_in_lattice) 
   1.276 + txt{*The difficult @{term wens} case*}
   1.277 + apply (simp add: progress_induction_step) 
   1.278 +txt{*Disjunctive case*}
   1.279 +apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 
   1.280 + apply (simp add: Int_Union) 
   1.281 +apply (blast intro: UN_in_lattice) 
   1.282 +done
   1.283 +
   1.284  end
     2.1 --- a/src/HOL/UNITY/Transformers.thy	Fri Mar 14 10:30:15 2003 +0100
     2.2 +++ b/src/HOL/UNITY/Transformers.thy	Fri Mar 14 10:30:46 2003 +0100
     2.3 @@ -48,15 +48,23 @@
     2.4       "wp (totalize_act act) B = (wp act B \<inter> Domain act) \<union> (B - Domain act)"
     2.5  by (simp add: wp_def totalize_act_def, blast)
     2.6  
     2.7 +lemma awp_subset: "(awp F A \<subseteq> A)"
     2.8 +by (force simp add: awp_def wp_def)
     2.9 +
    2.10  lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B"
    2.11  by (simp add: awp_def wp_def, blast) 
    2.12  
    2.13  text{*The fundamental theorem for awp*}
    2.14 -theorem awp_iff: "(A <= awp F B) = (F \<in> A co B)"
    2.15 +theorem awp_iff_constrains: "(A <= awp F B) = (F \<in> A co B)"
    2.16  by (simp add: awp_def constrains_def wp_iff INT_subset_iff) 
    2.17  
    2.18 -theorem stable_iff_awp: "(A \<subseteq> awp F A) = (F \<in> stable A)"
    2.19 -by (simp add: awp_iff stable_def) 
    2.20 +lemma awp_iff_stable: "(A \<subseteq> awp F A) = (F \<in> stable A)"
    2.21 +by (simp add: awp_iff_constrains stable_def) 
    2.22 +
    2.23 +lemma stable_imp_awp_ident: "F \<in> stable A ==> awp F A = A"
    2.24 +apply (rule equalityI [OF awp_subset]) 
    2.25 +apply (simp add: awp_iff_stable) 
    2.26 +done
    2.27  
    2.28  lemma awp_mono: "(A \<subseteq> B) ==> awp F A \<subseteq> awp F B"
    2.29  by (simp add: awp_def wp_def, blast)
    2.30 @@ -168,8 +176,8 @@
    2.31  
    2.32  lemma leadsTo_imp_wens_set: "F \<in> A leadsTo B ==> \<exists>C \<in> wens_set F B. A \<subseteq> C"
    2.33  apply (erule leadsTo_induct_pre)
    2.34 -  apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens, clarify) 
    2.35 - apply (drule ensures_weaken_R, assumption)  
    2.36 +  apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens) 
    2.37 + apply (clarify, drule ensures_weaken_R, assumption)  
    2.38   apply (blast dest!: ensures_imp_wens intro: wens_set.Wens)
    2.39  apply (case_tac "S={}") 
    2.40   apply (simp, blast intro: wens_set.Basis)
    2.41 @@ -197,8 +205,7 @@
    2.42  lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B \<inter> awp G B"
    2.43  by (simp add: awp_def wp_def, blast)
    2.44  
    2.45 -lemma wens_subset: 
    2.46 -     "wens F act B - B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)"
    2.47 +lemma wens_subset: "wens F act B - B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)"
    2.48  by (subst wens_unfold, fast) 
    2.49  
    2.50  text{*Assertion (4.31)*}
    2.51 @@ -239,8 +246,7 @@
    2.52  apply (rule_tac B = "wens (F\<squnion>G) act (T\<inter>X)" in subset_trans) 
    2.53   prefer 2 apply (blast intro!: wens_mono)
    2.54  apply (subst wens_Int_eq, assumption+) 
    2.55 -apply (rule subset_wens_Join [of _ T], simp) 
    2.56 - apply blast
    2.57 +apply (rule subset_wens_Join [of _ T], simp, blast)
    2.58  apply (subgoal_tac "T \<inter> wens F act (T\<inter>X) \<union> T\<inter>X = T \<inter> wens F act X")
    2.59   prefer 2
    2.60   apply (subst wens_Int_eq [symmetric], assumption+) 
    2.61 @@ -388,8 +394,7 @@
    2.62        "[|W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}|]
    2.63         ==> \<exists>m. \<Union>W = wens_single_finite act B m"
    2.64  apply (induct k)
    2.65 - apply (rule_tac x=0 in exI, simp) 
    2.66 - apply blast 
    2.67 + apply (rule_tac x=0 in exI, simp, blast) 
    2.68  apply (auto simp add: atMost_Suc) 
    2.69  apply (case_tac "wens_single_finite act B (Suc n) \<in> W") 
    2.70   prefer 2 apply blast 
    2.71 @@ -469,11 +474,8 @@
    2.72  
    2.73  lemma fp_leadsTo_Union:
    2.74      "[|T-B \<subseteq> awp F T; T-B \<subseteq> FP G; F \<in> A leadsTo B|] ==> F\<squnion>G \<in> T\<inter>A leadsTo B"
    2.75 -apply (rule leadsTo_Union) 
    2.76 -apply assumption; 
    2.77 - apply (simp add: FP_def awp_iff stable_def constrains_def) 
    2.78 - apply (blast intro: elim:); 
    2.79 -apply assumption; 
    2.80 +apply (rule leadsTo_Union, assumption)
    2.81 + apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast, assumption)
    2.82  done
    2.83  
    2.84  end
     3.1 --- a/src/HOL/UNITY/UNITY.thy	Fri Mar 14 10:30:15 2003 +0100
     3.2 +++ b/src/HOL/UNITY/UNITY.thy	Fri Mar 14 10:30:46 2003 +0100
     3.3 @@ -72,6 +72,9 @@
     3.4  lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
     3.5  by (simp add: insert_absorb Id_in_Acts)
     3.6  
     3.7 +lemma Acts_nonempty [simp]: "Acts F \<noteq> {}"
     3.8 +by auto
     3.9 +
    3.10  lemma Id_in_AllowedActs [iff]: "Id \<in> AllowedActs F"
    3.11  apply (cut_tac x = F in Rep_Program)
    3.12  apply (auto simp add: program_typedef)