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
```