src/HOL/UNITY/ProgressSets.thy
changeset 44106 0e018cbcc0de
parent 35416 d8d7d1b785af
child 44918 6a80fbc4e72c
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Tue Aug 09 18:52:18 2011 +0200
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Tue Aug 09 20:24:48 2011 +0200
     1.3 @@ -42,25 +42,21 @@
     1.4  
     1.5  lemma UN_in_lattice:
     1.6       "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
     1.7 -apply (simp add: UN_eq) 
     1.8 +apply (unfold SUP_def)
     1.9  apply (blast intro: Union_in_lattice) 
    1.10  done
    1.11  
    1.12  lemma INT_in_lattice:
    1.13       "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i)  \<in> L"
    1.14 -apply (simp add: INT_eq) 
    1.15 +apply (unfold INF_def)
    1.16  apply (blast intro: Inter_in_lattice) 
    1.17  done
    1.18  
    1.19  lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L"
    1.20 -apply (simp only: Un_eq_Union) 
    1.21 -apply (blast intro: Union_in_lattice) 
    1.22 -done
    1.23 +  using Union_in_lattice [of "{x, y}" L] by simp
    1.24  
    1.25  lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L"
    1.26 -apply (simp only: Int_eq_Inter) 
    1.27 -apply (blast intro: Inter_in_lattice) 
    1.28 -done
    1.29 +  using Inter_in_lattice [of "{x, y}" L] by simp
    1.30  
    1.31  lemma lattice_stable: "lattice {X. F \<in> stable X}"
    1.32  by (simp add: lattice_def stable_def constrains_def, blast)