# HG changeset patch
# User haftmann
# Date 1253338691 -7200
# Node ID 1392578231336fdaf6bb4a4221f290eb3897f1f0
# Parent  210fa627d7677eea6faf28451f9d42344795e673# Parent  7c1fe854ca6a3d9b2eabce77acf584be7f65e8f4
merged

diff -r 210fa627d767 -r 139257823133 NEWS
--- a/NEWS	Sat Sep 19 07:35:27 2009 +0200
+++ b/NEWS	Sat Sep 19 07:38:11 2009 +0200
@@ -87,6 +87,8 @@
   - mere abbreviations:
     Set.empty               (for bot)
     Set.UNIV                (for top)
+    Set.inter               (for inf)
+    Set.union               (for sup)
     Complete_Lattice.Inter  (for Inf)
     Complete_Lattice.Union  (for Sup)
     Complete_Lattice.INTER  (for INFI)
diff -r 210fa627d767 -r 139257823133 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Sat Sep 19 07:38:11 2009 +0200
@@ -1566,8 +1566,6 @@
   prefer 2
   apply assumption
   apply auto
-  apply (rule setsum_cong)
-  apply auto
 done
 
 lemma setsum_right_distrib: 
diff -r 210fa627d767 -r 139257823133 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Inductive.thy	Sat Sep 19 07:38:11 2009 +0200
@@ -83,7 +83,7 @@
       and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
   shows "P(a)"
   by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
-    (auto simp: inf_set_eq intro: indhyp)
+    (auto simp: intro: indhyp)
 
 lemma lfp_ordinal_induct:
   fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
@@ -184,7 +184,7 @@
 
 text{*strong version, thanks to Coen and Frost*}
 lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
-by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
+by (blast intro: weak_coinduct [OF _ coinduct_lemma])
 
 lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
   apply (rule order_trans)
diff -r 210fa627d767 -r 139257823133 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Sat Sep 19 07:38:11 2009 +0200
@@ -12,6 +12,21 @@
 
 declare member [code] 
 
+definition empty :: "'a set" where
+  "empty = {}"
+
+declare empty_def [symmetric, code_unfold]
+
+definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  "inter = op \<inter>"
+
+declare inter_def [symmetric, code_unfold]
+
+definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  "union = op \<union>"
+
+declare union_def [symmetric, code_unfold]
+
 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "subset = op \<le>"
 
@@ -69,7 +84,7 @@
   Set ("\<module>Set")
 
 consts_code
-  "Set.empty"         ("{*Fset.empty*}")
+  "empty"             ("{*Fset.empty*}")
   "List_Set.is_empty" ("{*Fset.is_empty*}")
   "Set.insert"        ("{*Fset.insert*}")
   "List_Set.remove"   ("{*Fset.remove*}")
@@ -77,8 +92,8 @@
   "List_Set.project"  ("{*Fset.filter*}")
   "Ball"              ("{*flip Fset.forall*}")
   "Bex"               ("{*flip Fset.exists*}")
-  "op \<union>"              ("{*Fset.union*}")
-  "op \<inter>"              ("{*Fset.inter*}")
+  "union"             ("{*Fset.union*}")
+  "inter"             ("{*Fset.inter*}")
   "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
   "Union"             ("{*Fset.Union*}")
   "Inter"             ("{*Fset.Inter*}")
diff -r 210fa627d767 -r 139257823133 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Set.thy	Sat Sep 19 07:38:11 2009 +0200
@@ -652,8 +652,8 @@
 
 subsubsection {* Binary union -- Un *}
 
-definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
-  sup_set_eq [symmetric]: "A Un B = sup A B"
+abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
+  "op Un \<equiv> sup"
 
 notation (xsymbols)
   union  (infixl "\<union>" 65)
@@ -663,7 +663,7 @@
 
 lemma Un_def:
   "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
-  by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
+  by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
 
 lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
   by (unfold Un_def) blast
@@ -689,15 +689,13 @@
   by (simp add: Collect_def mem_def insert_compr Un_def)
 
 lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
-  apply (fold sup_set_eq)
-  apply (erule mono_sup)
-  done
+  by (fact mono_sup)
 
 
 subsubsection {* Binary intersection -- Int *}
 
-definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
-  inf_set_eq [symmetric]: "A Int B = inf A B"
+abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
+  "op Int \<equiv> inf"
 
 notation (xsymbols)
   inter  (infixl "\<inter>" 70)
@@ -707,7 +705,7 @@
 
 lemma Int_def:
   "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
-  by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
+  by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
 
 lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   by (unfold Int_def) blast
@@ -725,9 +723,7 @@
   by simp
 
 lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
-  apply (fold inf_set_eq)
-  apply (erule mono_inf)
-  done
+  by (fact mono_inf)
 
 
 subsubsection {* Set difference *}
diff -r 210fa627d767 -r 139257823133 src/HOL/Tools/Function/fundef_lib.ML
--- a/src/HOL/Tools/Function/fundef_lib.ML	Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_lib.ML	Sat Sep 19 07:38:11 2009 +0200
@@ -170,7 +170,7 @@
  end
 
 (* instance for unions *)
-fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Set.union}
+fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
   (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
                                      @{thms Un_empty_right} @
                                      @{thms Un_empty_left})) t
diff -r 210fa627d767 -r 139257823133 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Sat Sep 19 07:38:11 2009 +0200
@@ -145,7 +145,7 @@
 
 fun mk_sum_skel rel =
   let
-    val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
+    val cs = FundefLib.dest_binop_list @{const_name Lattices.sup} rel
     fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
       let
         val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
@@ -233,7 +233,7 @@
 fun CALLS tac i st =
   if Thm.no_prems st then all_tac st
   else case Thm.term_of (Thm.cprem_of st i) of
-    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
+    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Lattices.sup} rel, i) st
   |_ => no_tac st
 
 type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
@@ -293,7 +293,7 @@
           if null ineqs then
               Const (@{const_name Set.empty}, fastype_of rel)
           else
-              foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
+              foldr1 (HOLogic.mk_binop @{const_name Lattices.sup}) (map mk_compr ineqs)
 
       fun solve_membership_tac i =
           (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
diff -r 210fa627d767 -r 139257823133 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Sat Sep 19 07:38:11 2009 +0200
@@ -74,8 +74,8 @@
         in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
           (p (fold (Logic.all o Var) vs t) f)
         end;
-      fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
-        | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
+      fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
+        | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
         | mkop _ _ _ = NONE;
       fun mk_collect p T t =
         let val U = HOLogic.dest_setT T
diff -r 210fa627d767 -r 139257823133 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Sat Sep 19 07:38:11 2009 +0200
@@ -2152,7 +2152,7 @@
     val (ts, _) = Predicate.yieldn k t;
     val elemsT = HOLogic.mk_set T ts;
   in if k = ~1 orelse length ts < k then elemsT
-    else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
+    else Const (@{const_name Lattices.sup}, setT --> setT --> setT) $ elemsT $ t_compr
   end;
 
 fun values_cmd modes k raw_t state =