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.4  
     1.5  subsection {* Union *}
     1.6  
     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.11  
    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.19 +    by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
    1.20  qed
    1.21  
    1.22  lemma Union_iff [simp, noatp]:
    1.23 @@ -314,7 +314,7 @@
    1.24  
    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.29  
    1.30  lemma Union_def:
    1.31    "\<Union>S = (\<Union>x\<in>S. x)"
    1.32 @@ -439,8 +439,8 @@
    1.33  
    1.34  subsection {* Inter *}
    1.35  
    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.40    
    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)
    1.48 +    by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
    1.49  qed
    1.50  
    1.51  lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
    1.52 @@ -541,7 +541,7 @@
    1.53  
    1.54  lemma INTER_eq_Inter_image:
    1.55    "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
    1.56 -  by (simp add: INFI_def INFI_set_eq [symmetric] Inf_set_eq)
    1.57 +  by (simp add: INFI_def INFI_set_eq [symmetric])
    1.58    
    1.59  lemma Inter_def:
    1.60    "\<Inter>S = (\<Inter>x\<in>S. x)"