src/HOL/Complete_Lattice.thy
 changeset 32587 caa5ada96a00 parent 32436 10cd49e0c067 child 32606 b5c3a8a75772
1.1 --- a/src/HOL/Complete_Lattice.thy	Wed Sep 16 09:04:41 2009 +0200
1.2 +++ b/src/HOL/Complete_Lattice.thy	Wed Sep 16 13:43:05 2009 +0200
1.3 @@ -203,8 +203,8 @@
1.5  subsection {* Union *}
1.7 -definition Union :: "'a set set \<Rightarrow> 'a set" where
1.8 -  Sup_set_eq [symmetric]: "Union S = \<Squnion>S"
1.9 +abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
1.10 +  "Union S \<equiv> \<Squnion>S"
1.12  notation (xsymbols)
1.13    Union  ("\<Union>_" [90] 90)
1.14 @@ -216,7 +216,7 @@
1.15    have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
1.16      by auto
1.17    then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
1.18 -    by (simp add: Sup_set_eq [symmetric] Sup_fun_def Sup_bool_def) (simp add: mem_def)
1.20  qed
1.22  lemma Union_iff [simp, noatp]:
1.23 @@ -314,7 +314,7 @@
1.25  lemma UNION_eq_Union_image:
1.26    "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
1.27 -  by (simp add: SUPR_def SUPR_set_eq [symmetric] Sup_set_eq)
1.28 +  by (simp add: SUPR_def SUPR_set_eq [symmetric])
1.30  lemma Union_def:
1.31    "\<Union>S = (\<Union>x\<in>S. x)"
1.32 @@ -439,8 +439,8 @@
1.34  subsection {* Inter *}
1.36 -definition Inter :: "'a set set \<Rightarrow> 'a set" where
1.37 -  Inf_set_eq [symmetric]: "Inter S = \<Sqinter>S"
1.38 +abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
1.39 +  "Inter S \<equiv> \<Sqinter>S"
1.41  notation (xsymbols)
1.42    Inter  ("\<Inter>_" [90] 90)
1.43 @@ -452,7 +452,7 @@
1.44    have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
1.45      by auto
1.46    then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
1.47 -    by (simp add: Inf_fun_def Inf_bool_def Inf_set_eq [symmetric]) (simp add: mem_def)