# HG changeset patch
# User haftmann
# Date 1253535792 -7200
# Node ID 5fb07ec998286870194947b6197f4d626505ea88
# Parent  860e1a2317bd09ae55e3f428d1bd3ad7a3a9cbee# Parent  542f0563d7b4ae76e3340e3e6fc9a624ad770f14
merged

diff -r 542f0563d7b4 -r 5fb07ec99828 NEWS
--- a/NEWS	Mon Sep 21 14:22:32 2009 +0200
+++ b/NEWS	Mon Sep 21 14:23:12 2009 +0200
@@ -94,6 +94,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 542f0563d7b4 -r 5fb07ec99828 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Sep 21 14:23:12 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 542f0563d7b4 -r 5fb07ec99828 src/HOL/Hoare_Parallel/Gar_Coll.thy
--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Mon Sep 21 14:23:12 2009 +0200
@@ -253,7 +253,7 @@
     \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."
 apply (unfold Propagate_Black_def  PBInv_def Auxk_def collector_defs)
 apply annhoare
-apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
+apply(simp_all add: Graph6 Graph7 Graph8 Graph12)
        apply force
       apply force
      apply force
@@ -297,8 +297,6 @@
 apply(erule subset_psubset_trans)
 apply(erule Graph11)
 apply fast
---{* 3 subgoals left *}
-apply force
 --{* 2 subgoals left *}
 apply clarify
 apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
diff -r 542f0563d7b4 -r 5fb07ec99828 src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Sep 21 14:23:12 2009 +0200
@@ -276,8 +276,6 @@
   apply(force)
  apply(force)
 apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
---{* 3 subgoals left *}
-apply force
 --{* 2 subgoals left *}
 apply clarify
 apply(conjI_tac)
@@ -1235,9 +1233,9 @@
 apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
 apply(tactic  {* TRYALL (interfree_aux_tac) *})
 --{* 76 subgoals left *}
-apply (clarify,simp add: nth_list_update)+
+apply (clarsimp simp add: nth_list_update)+
 --{* 56 subgoals left *}
-apply(clarify,simp add:Mul_AppendInv_def Append_to_free0 nth_list_update)+
+apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+
 done
 
 subsubsection {* The Multi-Mutator Garbage Collection Algorithm *}
diff -r 542f0563d7b4 -r 5fb07ec99828 src/HOL/Hoare_Parallel/RG_Hoare.thy
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Mon Sep 21 14:23:12 2009 +0200
@@ -4,8 +4,8 @@
 
 subsection {* Proof System for Component Programs *}
 
-declare Un_subset_iff [iff del]
-declare Cons_eq_map_conv[iff]
+declare Un_subset_iff [simp del] le_sup_iff [simp del]
+declare Cons_eq_map_conv [iff]
 
 constdefs
   stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"  
diff -r 542f0563d7b4 -r 5fb07ec99828 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Inductive.thy	Mon Sep 21 14:23:12 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 542f0563d7b4 -r 5fb07ec99828 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Mon Sep 21 14:23:12 2009 +0200
@@ -3649,10 +3649,7 @@
     from setsum_restrict_set[OF fS, of "\<lambda>v. u v *s v" S', symmetric] SS'
     have "setsum (\<lambda>v. ?u v *s v) S = setsum (\<lambda>v. u v *s v) S'"
       unfolding cond_value_iff cond_application_beta
-      apply (simp add: cond_value_iff cong del: if_weak_cong)
-      apply (rule setsum_cong)
-      apply auto
-      done
+      by (simp add: cond_value_iff cong del: if_weak_cong)
     hence "setsum (\<lambda>v. ?u v *s v) S = y" by (metis u)
     hence "y \<in> ?rhs" by auto}
   moreover
diff -r 542f0563d7b4 -r 5fb07ec99828 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Mon Sep 21 14:23:12 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 542f0563d7b4 -r 5fb07ec99828 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Sep 21 14:23:12 2009 +0200
@@ -99,11 +99,9 @@
 
 lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast
 lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
-  apply (auto simp add: closedin_def)
+  apply (auto simp add: closedin_def Diff_Diff_Int)
   apply (metis openin_subset subset_eq)
-  apply (auto simp add: Diff_Diff_Int)
-  apply (subgoal_tac "topspace U \<inter> S = S")
-  by auto
+  done
 
 lemma openin_closedin:  "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
   by (simp add: openin_closedin_eq)
diff -r 542f0563d7b4 -r 5fb07ec99828 src/HOL/MetisExamples/Message.thy
--- a/src/HOL/MetisExamples/Message.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/MetisExamples/Message.thy	Mon Sep 21 14:23:12 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MetisTest/Message.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Testing the metis method
@@ -711,17 +710,17 @@
 proof (neg_clausify)
 assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
 have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
-  by (metis analz_synth_Un sup_set_eq sup_set_eq sup_set_eq)
+  by (metis analz_synth_Un)
 have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
-  by (metis 0 sup_set_eq)
+  by (metis 0)
 have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
-  by (metis 1 Un_commute sup_set_eq sup_set_eq)
+  by (metis 1 Un_commute)
 have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
-  by (metis 3 Un_empty_right sup_set_eq)
+  by (metis 3 Un_empty_right)
 have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
-  by (metis 4 Un_empty_right sup_set_eq)
+  by (metis 4 Un_empty_right)
 have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
-  by (metis 5 Un_commute sup_set_eq sup_set_eq)
+  by (metis 5 Un_commute)
 show "False"
   by (metis 2 6)
 qed
diff -r 542f0563d7b4 -r 5fb07ec99828 src/HOL/MetisExamples/set.thy
--- a/src/HOL/MetisExamples/set.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/MetisExamples/set.thy	Mon Sep 21 14:23:12 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MetisExamples/set.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Testing the metis method
@@ -36,23 +35,23 @@
 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
 have 6: "sup Y Z = X \<or> Y \<subseteq> X"
-  by (metis 0 sup_set_eq)
+  by (metis 0)
 have 7: "sup Y Z = X \<or> Z \<subseteq> X"
-  by (metis 1 sup_set_eq)
+  by (metis 1)
 have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3"
-  by (metis 5 sup_set_eq)
+  by (metis 5)
 have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 2 sup_set_eq)
+  by (metis 2)
 have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 3 sup_set_eq)
+  by (metis 3)
 have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 4 sup_set_eq)
+  by (metis 4)
 have 12: "Z \<subseteq> X"
-  by (metis Un_upper2 sup_set_eq 7)
+  by (metis Un_upper2 7)
 have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
-  by (metis 8 Un_upper2 sup_set_eq)
+  by (metis 8 Un_upper2)
 have 14: "Y \<subseteq> X"
-  by (metis Un_upper1 sup_set_eq 6)
+  by (metis Un_upper1 6)
 have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   by (metis 10 12)
 have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
@@ -66,17 +65,17 @@
 have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X"
   by (metis 16 14)
 have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
-  by (metis 13 Un_upper1 sup_set_eq)
+  by (metis 13 Un_upper1)
 have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
   by (metis equalityI 21)
 have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 22 Un_least sup_set_eq)
+  by (metis 22 Un_least)
 have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X"
   by (metis 23 12)
 have 25: "sup Y Z = X"
   by (metis 24 14)
 have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3"
-  by (metis Un_least sup_set_eq 25)
+  by (metis Un_least 25)
 have 27: "Y \<subseteq> x"
   by (metis 20 25)
 have 28: "Z \<subseteq> x"
@@ -105,31 +104,31 @@
 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
 have 6: "sup Y Z = X \<or> Y \<subseteq> X"
-  by (metis 0 sup_set_eq)
+  by (metis 0)
 have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 2 sup_set_eq)
+  by (metis 2)
 have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 4 sup_set_eq)
+  by (metis 4)
 have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
-  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
+  by (metis 5 Un_upper2)
 have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
+  by (metis 3 Un_upper2)
 have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
-  by (metis 8 Un_upper2 sup_set_eq sup_set_eq)
+  by (metis 8 Un_upper2)
 have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
-  by (metis 10 Un_upper1 sup_set_eq)
+  by (metis 10 Un_upper1)
 have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
-  by (metis 9 Un_upper1 sup_set_eq)
+  by (metis 9 Un_upper1)
 have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis equalityI 13 Un_least sup_set_eq)
+  by (metis equalityI 13 Un_least)
 have 15: "sup Y Z = X"
-  by (metis 14 sup_set_eq 1 sup_set_eq sup_set_eq 6)
+  by (metis 14 1 6)
 have 16: "Y \<subseteq> x"
-  by (metis 7 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq 15)
+  by (metis 7 Un_upper2 Un_upper1 15)
 have 17: "\<not> X \<subseteq> x"
-  by (metis 11 Un_upper1 sup_set_eq 15)
+  by (metis 11 Un_upper1 15)
 have 18: "X \<subseteq> x"
-  by (metis Un_least sup_set_eq 15 12 15 16)
+  by (metis Un_least 15 12 15 16)
 show "False"
   by (metis 18 17)
 qed
@@ -148,23 +147,23 @@
 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
 have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 3 sup_set_eq)
+  by (metis 3)
 have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
-  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
+  by (metis 5 Un_upper2)
 have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 2 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
+  by (metis 2 Un_upper2)
 have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
-  by (metis 6 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq)
+  by (metis 6 Un_upper2 Un_upper1)
 have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
-  by (metis equalityI 7 Un_upper1 sup_set_eq)
+  by (metis equalityI 7 Un_upper1)
 have 11: "sup Y Z = X"
-  by (metis 10 Un_least sup_set_eq sup_set_eq 1 sup_set_eq sup_set_eq 0 sup_set_eq)
+  by (metis 10 Un_least 1 0)
 have 12: "Z \<subseteq> x"
   by (metis 9 11)
 have 13: "X \<subseteq> x"
-  by (metis Un_least sup_set_eq 11 12 8 Un_upper1 sup_set_eq sup_set_eq 11)
+  by (metis Un_least 11 12 8 Un_upper1 11)
 show "False"
-  by (metis 13 4 sup_set_eq Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq 11)
+  by (metis 13 4 Un_upper2 Un_upper1 11)
 qed
 
 (*Example included in TPHOLs paper*)
@@ -183,19 +182,19 @@
 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
 have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 4 sup_set_eq)
+  by (metis 4)
 have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
+  by (metis 3 Un_upper2)
 have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
-  by (metis 7 Un_upper1 sup_set_eq sup_set_eq)
+  by (metis 7 Un_upper1)
 have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis equalityI 5 sup_set_eq Un_upper2 sup_set_eq Un_upper1 sup_set_eq Un_least sup_set_eq)
+  by (metis equalityI 5 Un_upper2 Un_upper1 Un_least)
 have 10: "Y \<subseteq> x"
-  by (metis 2 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
+  by (metis 2 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
 have 11: "X \<subseteq> x"
-  by (metis Un_least sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 8 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 10)
+  by (metis Un_least 9 Un_upper2 1 Un_upper1 0 8 9 Un_upper2 1 Un_upper1 0 10)
 show "False"
-  by (metis 11 6 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
+  by (metis 11 6 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
 qed 
 
 ML {*AtpWrapper.problem_name := "set__equal_union"*}
@@ -238,7 +237,7 @@
 
 lemma (*singleton_example_2:*)
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-by (metis Set.subsetI Union_upper insert_code mem_def set_eq_subset)
+by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
 
 lemma singleton_example_2:
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
diff -r 542f0563d7b4 -r 5fb07ec99828 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Set.thy	Mon Sep 21 14:23:12 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 542f0563d7b4 -r 5fb07ec99828 src/HOL/Tools/Function/fundef_lib.ML
--- a/src/HOL/Tools/Function/fundef_lib.ML	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_lib.ML	Mon Sep 21 14:23:12 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 542f0563d7b4 -r 5fb07ec99828 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Mon Sep 21 14:23:12 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 542f0563d7b4 -r 5fb07ec99828 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Mon Sep 21 14:23:12 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 542f0563d7b4 -r 5fb07ec99828 src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/UNITY/Follows.thy	Mon Sep 21 14:23:12 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/UNITY/Follows
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 *)
@@ -160,7 +159,7 @@
 lemma Follows_Un: 
     "[| F \<in> f' Fols f;  F \<in> g' Fols g |]  
      ==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
-apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff, auto)
+apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff le_sup_iff, auto)
 apply (rule LeadsTo_Trans)
 apply (blast intro: Follows_Un_lemma)
 (*Weakening is used to exchange Un's arguments*)
diff -r 542f0563d7b4 -r 5fb07ec99828 src/HOL/UNITY/UNITY_Main.thy
--- a/src/HOL/UNITY/UNITY_Main.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy	Mon Sep 21 14:23:12 2009 +0200
@@ -1,13 +1,14 @@
 (*  Title:      HOL/UNITY/UNITY_Main.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2003  University of Cambridge
 *)
 
 header{*Comprehensive UNITY Theory*}
 
-theory UNITY_Main imports Detects PPROD Follows ProgressSets
-uses "UNITY_tactics.ML" begin
+theory UNITY_Main
+imports Detects PPROD Follows ProgressSets
+uses "UNITY_tactics.ML"
+begin
 
 method_setup safety = {*
     Scan.succeed (fn ctxt =>
diff -r 542f0563d7b4 -r 5fb07ec99828 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Mon Sep 21 14:23:12 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 =