src/HOL/Complete_Lattice.thy
changeset 32606 b5c3a8a75772
parent 32587 caa5ada96a00
child 32642 026e7c6a6d08
     1.1 --- a/src/HOL/Complete_Lattice.thy	Fri Sep 18 09:35:23 2009 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Fri Sep 18 14:09:38 2009 +0200
     1.3 @@ -278,8 +278,8 @@
     1.4  
     1.5  subsection {* Unions of families *}
     1.6  
     1.7 -definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
     1.8 -  SUPR_set_eq [symmetric]: "UNION S f = (SUP x:S. f x)"
     1.9 +abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
    1.10 +  "UNION \<equiv> SUPR"
    1.11  
    1.12  syntax
    1.13    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
    1.14 @@ -314,7 +314,7 @@
    1.15  
    1.16  lemma UNION_eq_Union_image:
    1.17    "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
    1.18 -  by (simp add: SUPR_def SUPR_set_eq [symmetric])
    1.19 +  by (fact SUPR_def)
    1.20  
    1.21  lemma Union_def:
    1.22    "\<Union>S = (\<Union>x\<in>S. x)"
    1.23 @@ -351,7 +351,7 @@
    1.24    by blast
    1.25  
    1.26  lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
    1.27 -  by blast
    1.28 +  by (fact le_SUPI)
    1.29  
    1.30  lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
    1.31    by (iprover intro: subsetI elim: UN_E dest: subsetD)
    1.32 @@ -514,8 +514,8 @@
    1.33  
    1.34  subsection {* Intersections of families *}
    1.35  
    1.36 -definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
    1.37 -  INFI_set_eq [symmetric]: "INTER S f = (INF x:S. f x)"
    1.38 +abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
    1.39 +  "INTER \<equiv> INFI"
    1.40  
    1.41  syntax
    1.42    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
    1.43 @@ -541,7 +541,7 @@
    1.44  
    1.45  lemma INTER_eq_Inter_image:
    1.46    "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
    1.47 -  by (simp add: INFI_def INFI_set_eq [symmetric])
    1.48 +  by (fact INFI_def)
    1.49    
    1.50  lemma Inter_def:
    1.51    "\<Inter>S = (\<Inter>x\<in>S. x)"
    1.52 @@ -579,10 +579,10 @@
    1.53    by blast
    1.54  
    1.55  lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
    1.56 -  by blast
    1.57 +  by (fact INF_leI)
    1.58  
    1.59  lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
    1.60 -  by (iprover intro: INT_I subsetI dest: subsetD)
    1.61 +  by (fact le_INFI)
    1.62  
    1.63  lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
    1.64    by blast