# HG changeset patch
# User haftmann
# Date 1253275778 -7200
# Node ID b5c3a8a7577245b91aa805e57c327fef1ed93088
# Parent  43ed78ee285d9d89948b527db334df11d3bc5193
INTER and UNION are mere abbreviations for INFI and SUPR

diff -r 43ed78ee285d -r b5c3a8a75772 NEWS
--- a/NEWS	Fri Sep 18 09:35:23 2009 +0200
+++ b/NEWS	Fri Sep 18 14:09:38 2009 +0200
@@ -79,8 +79,8 @@
     Set.INTER ~>    Complete_Lattice.INTER
     Set.UNION ~>    Complete_Lattice.UNION
   - more convenient names for set intersection and union:
-    Set.Int ~>  Set.inter
-    Set.Un ~>   Set.union
+    Set.Int ~>      Set.inter
+    Set.Un ~>       Set.union
   - authentic syntax for
     Set.Pow
     Set.image
@@ -89,6 +89,8 @@
     Set.UNIV                (for top)
     Complete_Lattice.Inter  (for Inf)
     Complete_Lattice.Union  (for Sup)
+    Complete_Lattice.INTER  (for INFI)
+    Complete_Lattice.UNION  (for SUPR)
   - object-logic definitions as far as appropriate
 
   INCOMPATIBILITY.
diff -r 43ed78ee285d -r b5c3a8a75772 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Fri Sep 18 09:35:23 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy	Fri Sep 18 14:09:38 2009 +0200
@@ -278,8 +278,8 @@
 
 subsection {* Unions of families *}
 
-definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
-  SUPR_set_eq [symmetric]: "UNION S f = (SUP x:S. f x)"
+abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+  "UNION \<equiv> SUPR"
 
 syntax
   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
@@ -314,7 +314,7 @@
 
 lemma UNION_eq_Union_image:
   "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
-  by (simp add: SUPR_def SUPR_set_eq [symmetric])
+  by (fact SUPR_def)
 
 lemma Union_def:
   "\<Union>S = (\<Union>x\<in>S. x)"
@@ -351,7 +351,7 @@
   by blast
 
 lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
-  by blast
+  by (fact le_SUPI)
 
 lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
   by (iprover intro: subsetI elim: UN_E dest: subsetD)
@@ -514,8 +514,8 @@
 
 subsection {* Intersections of families *}
 
-definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
-  INFI_set_eq [symmetric]: "INTER S f = (INF x:S. f x)"
+abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+  "INTER \<equiv> INFI"
 
 syntax
   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
@@ -541,7 +541,7 @@
 
 lemma INTER_eq_Inter_image:
   "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
-  by (simp add: INFI_def INFI_set_eq [symmetric])
+  by (fact INFI_def)
   
 lemma Inter_def:
   "\<Inter>S = (\<Inter>x\<in>S. x)"
@@ -579,10 +579,10 @@
   by blast
 
 lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
-  by blast
+  by (fact INF_leI)
 
 lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
-  by (iprover intro: INT_I subsetI dest: subsetD)
+  by (fact le_INFI)
 
 lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
   by blast
diff -r 43ed78ee285d -r b5c3a8a75772 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Fri Sep 18 09:35:23 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Fri Sep 18 14:09:38 2009 +0200
@@ -32,8 +32,8 @@
 
 declare inter [code]
 
-declare Inter_image_eq [symmetric, code]
-declare Union_image_eq [symmetric, code]
+declare Inter_image_eq [symmetric, code_unfold]
+declare Union_image_eq [symmetric, code_unfold]
 
 declare List_Set.project_def [symmetric, code_unfold]