merged
authorhaftmann
Mon Sep 21 12:24:21 2009 +0200 (2009-09-21)
changeset 3268858b561b415a2
parent 32625 f270520df7de
parent 32687 27530efec97a
child 32689 860e1a2317bd
merged
     1.1 --- a/NEWS	Mon Sep 21 12:23:05 2009 +0200
     1.2 +++ b/NEWS	Mon Sep 21 12:24:21 2009 +0200
     1.3 @@ -94,6 +94,8 @@
     1.4    - mere abbreviations:
     1.5      Set.empty               (for bot)
     1.6      Set.UNIV                (for top)
     1.7 +    Set.inter               (for inf)
     1.8 +    Set.union               (for sup)
     1.9      Complete_Lattice.Inter  (for Inf)
    1.10      Complete_Lattice.Union  (for Sup)
    1.11      Complete_Lattice.INTER  (for INFI)
     2.1 --- a/src/HOL/Finite_Set.thy	Mon Sep 21 12:23:05 2009 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Mon Sep 21 12:24:21 2009 +0200
     2.3 @@ -1566,8 +1566,6 @@
     2.4    prefer 2
     2.5    apply assumption
     2.6    apply auto
     2.7 -  apply (rule setsum_cong)
     2.8 -  apply auto
     2.9  done
    2.10  
    2.11  lemma setsum_right_distrib: 
     3.1 --- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Mon Sep 21 12:23:05 2009 +0200
     3.2 +++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Mon Sep 21 12:24:21 2009 +0200
     3.3 @@ -253,7 +253,7 @@
     3.4      \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."
     3.5  apply (unfold Propagate_Black_def  PBInv_def Auxk_def collector_defs)
     3.6  apply annhoare
     3.7 -apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
     3.8 +apply(simp_all add: Graph6 Graph7 Graph8 Graph12)
     3.9         apply force
    3.10        apply force
    3.11       apply force
    3.12 @@ -297,8 +297,6 @@
    3.13  apply(erule subset_psubset_trans)
    3.14  apply(erule Graph11)
    3.15  apply fast
    3.16 ---{* 3 subgoals left *}
    3.17 -apply force
    3.18  --{* 2 subgoals left *}
    3.19  apply clarify
    3.20  apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
     4.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Sep 21 12:23:05 2009 +0200
     4.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Sep 21 12:24:21 2009 +0200
     4.3 @@ -276,8 +276,6 @@
     4.4    apply(force)
     4.5   apply(force)
     4.6  apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
     4.7 ---{* 3 subgoals left *}
     4.8 -apply force
     4.9  --{* 2 subgoals left *}
    4.10  apply clarify
    4.11  apply(conjI_tac)
    4.12 @@ -1235,9 +1233,9 @@
    4.13  apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
    4.14  apply(tactic  {* TRYALL (interfree_aux_tac) *})
    4.15  --{* 76 subgoals left *}
    4.16 -apply (clarify,simp add: nth_list_update)+
    4.17 +apply (clarsimp simp add: nth_list_update)+
    4.18  --{* 56 subgoals left *}
    4.19 -apply(clarify,simp add:Mul_AppendInv_def Append_to_free0 nth_list_update)+
    4.20 +apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+
    4.21  done
    4.22  
    4.23  subsubsection {* The Multi-Mutator Garbage Collection Algorithm *}
     5.1 --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Mon Sep 21 12:23:05 2009 +0200
     5.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Mon Sep 21 12:24:21 2009 +0200
     5.3 @@ -4,8 +4,8 @@
     5.4  
     5.5  subsection {* Proof System for Component Programs *}
     5.6  
     5.7 -declare Un_subset_iff [iff del]
     5.8 -declare Cons_eq_map_conv[iff]
     5.9 +declare Un_subset_iff [simp del] le_sup_iff [simp del]
    5.10 +declare Cons_eq_map_conv [iff]
    5.11  
    5.12  constdefs
    5.13    stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"  
     6.1 --- a/src/HOL/Inductive.thy	Mon Sep 21 12:23:05 2009 +0200
     6.2 +++ b/src/HOL/Inductive.thy	Mon Sep 21 12:24:21 2009 +0200
     6.3 @@ -83,7 +83,7 @@
     6.4        and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
     6.5    shows "P(a)"
     6.6    by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
     6.7 -    (auto simp: inf_set_eq intro: indhyp)
     6.8 +    (auto simp: intro: indhyp)
     6.9  
    6.10  lemma lfp_ordinal_induct:
    6.11    fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
    6.12 @@ -184,7 +184,7 @@
    6.13  
    6.14  text{*strong version, thanks to Coen and Frost*}
    6.15  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
    6.16 -by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
    6.17 +by (blast intro: weak_coinduct [OF _ coinduct_lemma])
    6.18  
    6.19  lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
    6.20    apply (rule order_trans)
     7.1 --- a/src/HOL/Library/Euclidean_Space.thy	Mon Sep 21 12:23:05 2009 +0200
     7.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon Sep 21 12:24:21 2009 +0200
     7.3 @@ -3649,10 +3649,7 @@
     7.4      from setsum_restrict_set[OF fS, of "\<lambda>v. u v *s v" S', symmetric] SS'
     7.5      have "setsum (\<lambda>v. ?u v *s v) S = setsum (\<lambda>v. u v *s v) S'"
     7.6        unfolding cond_value_iff cond_application_beta
     7.7 -      apply (simp add: cond_value_iff cong del: if_weak_cong)
     7.8 -      apply (rule setsum_cong)
     7.9 -      apply auto
    7.10 -      done
    7.11 +      by (simp add: cond_value_iff cong del: if_weak_cong)
    7.12      hence "setsum (\<lambda>v. ?u v *s v) S = y" by (metis u)
    7.13      hence "y \<in> ?rhs" by auto}
    7.14    moreover
     8.1 --- a/src/HOL/Library/Executable_Set.thy	Mon Sep 21 12:23:05 2009 +0200
     8.2 +++ b/src/HOL/Library/Executable_Set.thy	Mon Sep 21 12:24:21 2009 +0200
     8.3 @@ -12,6 +12,21 @@
     8.4  
     8.5  declare member [code] 
     8.6  
     8.7 +definition empty :: "'a set" where
     8.8 +  "empty = {}"
     8.9 +
    8.10 +declare empty_def [symmetric, code_unfold]
    8.11 +
    8.12 +definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    8.13 +  "inter = op \<inter>"
    8.14 +
    8.15 +declare inter_def [symmetric, code_unfold]
    8.16 +
    8.17 +definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    8.18 +  "union = op \<union>"
    8.19 +
    8.20 +declare union_def [symmetric, code_unfold]
    8.21 +
    8.22  definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    8.23    "subset = op \<le>"
    8.24  
    8.25 @@ -69,7 +84,7 @@
    8.26    Set ("\<module>Set")
    8.27  
    8.28  consts_code
    8.29 -  "Set.empty"         ("{*Fset.empty*}")
    8.30 +  "empty"             ("{*Fset.empty*}")
    8.31    "List_Set.is_empty" ("{*Fset.is_empty*}")
    8.32    "Set.insert"        ("{*Fset.insert*}")
    8.33    "List_Set.remove"   ("{*Fset.remove*}")
    8.34 @@ -77,8 +92,8 @@
    8.35    "List_Set.project"  ("{*Fset.filter*}")
    8.36    "Ball"              ("{*flip Fset.forall*}")
    8.37    "Bex"               ("{*flip Fset.exists*}")
    8.38 -  "op \<union>"              ("{*Fset.union*}")
    8.39 -  "op \<inter>"              ("{*Fset.inter*}")
    8.40 +  "union"             ("{*Fset.union*}")
    8.41 +  "inter"             ("{*Fset.inter*}")
    8.42    "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
    8.43    "Union"             ("{*Fset.Union*}")
    8.44    "Inter"             ("{*Fset.Inter*}")
     9.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Sep 21 12:23:05 2009 +0200
     9.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Sep 21 12:24:21 2009 +0200
     9.3 @@ -99,11 +99,9 @@
     9.4  
     9.5  lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast
     9.6  lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
     9.7 -  apply (auto simp add: closedin_def)
     9.8 +  apply (auto simp add: closedin_def Diff_Diff_Int)
     9.9    apply (metis openin_subset subset_eq)
    9.10 -  apply (auto simp add: Diff_Diff_Int)
    9.11 -  apply (subgoal_tac "topspace U \<inter> S = S")
    9.12 -  by auto
    9.13 +  done
    9.14  
    9.15  lemma openin_closedin:  "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
    9.16    by (simp add: openin_closedin_eq)
    10.1 --- a/src/HOL/MetisExamples/Message.thy	Mon Sep 21 12:23:05 2009 +0200
    10.2 +++ b/src/HOL/MetisExamples/Message.thy	Mon Sep 21 12:24:21 2009 +0200
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOL/MetisTest/Message.thy
    10.5 -    ID:         $Id$
    10.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7  
    10.8  Testing the metis method
    10.9 @@ -711,17 +710,17 @@
   10.10  proof (neg_clausify)
   10.11  assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
   10.12  have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
   10.13 -  by (metis analz_synth_Un sup_set_eq sup_set_eq sup_set_eq)
   10.14 +  by (metis analz_synth_Un)
   10.15  have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
   10.16 -  by (metis 0 sup_set_eq)
   10.17 +  by (metis 0)
   10.18  have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
   10.19 -  by (metis 1 Un_commute sup_set_eq sup_set_eq)
   10.20 +  by (metis 1 Un_commute)
   10.21  have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
   10.22 -  by (metis 3 Un_empty_right sup_set_eq)
   10.23 +  by (metis 3 Un_empty_right)
   10.24  have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
   10.25 -  by (metis 4 Un_empty_right sup_set_eq)
   10.26 +  by (metis 4 Un_empty_right)
   10.27  have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
   10.28 -  by (metis 5 Un_commute sup_set_eq sup_set_eq)
   10.29 +  by (metis 5 Un_commute)
   10.30  show "False"
   10.31    by (metis 2 6)
   10.32  qed
    11.1 --- a/src/HOL/MetisExamples/set.thy	Mon Sep 21 12:23:05 2009 +0200
    11.2 +++ b/src/HOL/MetisExamples/set.thy	Mon Sep 21 12:24:21 2009 +0200
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      HOL/MetisExamples/set.thy
    11.5 -    ID:         $Id$
    11.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7  
    11.8  Testing the metis method
    11.9 @@ -36,23 +35,23 @@
   11.10  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   11.11  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
   11.12  have 6: "sup Y Z = X \<or> Y \<subseteq> X"
   11.13 -  by (metis 0 sup_set_eq)
   11.14 +  by (metis 0)
   11.15  have 7: "sup Y Z = X \<or> Z \<subseteq> X"
   11.16 -  by (metis 1 sup_set_eq)
   11.17 +  by (metis 1)
   11.18  have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3"
   11.19 -  by (metis 5 sup_set_eq)
   11.20 +  by (metis 5)
   11.21  have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   11.22 -  by (metis 2 sup_set_eq)
   11.23 +  by (metis 2)
   11.24  have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   11.25 -  by (metis 3 sup_set_eq)
   11.26 +  by (metis 3)
   11.27  have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   11.28 -  by (metis 4 sup_set_eq)
   11.29 +  by (metis 4)
   11.30  have 12: "Z \<subseteq> X"
   11.31 -  by (metis Un_upper2 sup_set_eq 7)
   11.32 +  by (metis Un_upper2 7)
   11.33  have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
   11.34 -  by (metis 8 Un_upper2 sup_set_eq)
   11.35 +  by (metis 8 Un_upper2)
   11.36  have 14: "Y \<subseteq> X"
   11.37 -  by (metis Un_upper1 sup_set_eq 6)
   11.38 +  by (metis Un_upper1 6)
   11.39  have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   11.40    by (metis 10 12)
   11.41  have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   11.42 @@ -66,17 +65,17 @@
   11.43  have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X"
   11.44    by (metis 16 14)
   11.45  have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
   11.46 -  by (metis 13 Un_upper1 sup_set_eq)
   11.47 +  by (metis 13 Un_upper1)
   11.48  have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
   11.49    by (metis equalityI 21)
   11.50  have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
   11.51 -  by (metis 22 Un_least sup_set_eq)
   11.52 +  by (metis 22 Un_least)
   11.53  have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X"
   11.54    by (metis 23 12)
   11.55  have 25: "sup Y Z = X"
   11.56    by (metis 24 14)
   11.57  have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3"
   11.58 -  by (metis Un_least sup_set_eq 25)
   11.59 +  by (metis Un_least 25)
   11.60  have 27: "Y \<subseteq> x"
   11.61    by (metis 20 25)
   11.62  have 28: "Z \<subseteq> x"
   11.63 @@ -105,31 +104,31 @@
   11.64  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   11.65  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
   11.66  have 6: "sup Y Z = X \<or> Y \<subseteq> X"
   11.67 -  by (metis 0 sup_set_eq)
   11.68 +  by (metis 0)
   11.69  have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   11.70 -  by (metis 2 sup_set_eq)
   11.71 +  by (metis 2)
   11.72  have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   11.73 -  by (metis 4 sup_set_eq)
   11.74 +  by (metis 4)
   11.75  have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
   11.76 -  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
   11.77 +  by (metis 5 Un_upper2)
   11.78  have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   11.79 -  by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
   11.80 +  by (metis 3 Un_upper2)
   11.81  have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
   11.82 -  by (metis 8 Un_upper2 sup_set_eq sup_set_eq)
   11.83 +  by (metis 8 Un_upper2)
   11.84  have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
   11.85 -  by (metis 10 Un_upper1 sup_set_eq)
   11.86 +  by (metis 10 Un_upper1)
   11.87  have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
   11.88 -  by (metis 9 Un_upper1 sup_set_eq)
   11.89 +  by (metis 9 Un_upper1)
   11.90  have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
   11.91 -  by (metis equalityI 13 Un_least sup_set_eq)
   11.92 +  by (metis equalityI 13 Un_least)
   11.93  have 15: "sup Y Z = X"
   11.94 -  by (metis 14 sup_set_eq 1 sup_set_eq sup_set_eq 6)
   11.95 +  by (metis 14 1 6)
   11.96  have 16: "Y \<subseteq> x"
   11.97 -  by (metis 7 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq 15)
   11.98 +  by (metis 7 Un_upper2 Un_upper1 15)
   11.99  have 17: "\<not> X \<subseteq> x"
  11.100 -  by (metis 11 Un_upper1 sup_set_eq 15)
  11.101 +  by (metis 11 Un_upper1 15)
  11.102  have 18: "X \<subseteq> x"
  11.103 -  by (metis Un_least sup_set_eq 15 12 15 16)
  11.104 +  by (metis Un_least 15 12 15 16)
  11.105  show "False"
  11.106    by (metis 18 17)
  11.107  qed
  11.108 @@ -148,23 +147,23 @@
  11.109  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
  11.110  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
  11.111  have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
  11.112 -  by (metis 3 sup_set_eq)
  11.113 +  by (metis 3)
  11.114  have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
  11.115 -  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
  11.116 +  by (metis 5 Un_upper2)
  11.117  have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
  11.118 -  by (metis 2 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
  11.119 +  by (metis 2 Un_upper2)
  11.120  have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
  11.121 -  by (metis 6 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq)
  11.122 +  by (metis 6 Un_upper2 Un_upper1)
  11.123  have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
  11.124 -  by (metis equalityI 7 Un_upper1 sup_set_eq)
  11.125 +  by (metis equalityI 7 Un_upper1)
  11.126  have 11: "sup Y Z = X"
  11.127 -  by (metis 10 Un_least sup_set_eq sup_set_eq 1 sup_set_eq sup_set_eq 0 sup_set_eq)
  11.128 +  by (metis 10 Un_least 1 0)
  11.129  have 12: "Z \<subseteq> x"
  11.130    by (metis 9 11)
  11.131  have 13: "X \<subseteq> x"
  11.132 -  by (metis Un_least sup_set_eq 11 12 8 Un_upper1 sup_set_eq sup_set_eq 11)
  11.133 +  by (metis Un_least 11 12 8 Un_upper1 11)
  11.134  show "False"
  11.135 -  by (metis 13 4 sup_set_eq Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq 11)
  11.136 +  by (metis 13 4 Un_upper2 Un_upper1 11)
  11.137  qed
  11.138  
  11.139  (*Example included in TPHOLs paper*)
  11.140 @@ -183,19 +182,19 @@
  11.141  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
  11.142  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
  11.143  have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
  11.144 -  by (metis 4 sup_set_eq)
  11.145 +  by (metis 4)
  11.146  have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
  11.147 -  by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
  11.148 +  by (metis 3 Un_upper2)
  11.149  have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
  11.150 -  by (metis 7 Un_upper1 sup_set_eq sup_set_eq)
  11.151 +  by (metis 7 Un_upper1)
  11.152  have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
  11.153 -  by (metis equalityI 5 sup_set_eq Un_upper2 sup_set_eq Un_upper1 sup_set_eq Un_least sup_set_eq)
  11.154 +  by (metis equalityI 5 Un_upper2 Un_upper1 Un_least)
  11.155  have 10: "Y \<subseteq> x"
  11.156 -  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)
  11.157 +  by (metis 2 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
  11.158  have 11: "X \<subseteq> x"
  11.159 -  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)
  11.160 +  by (metis Un_least 9 Un_upper2 1 Un_upper1 0 8 9 Un_upper2 1 Un_upper1 0 10)
  11.161  show "False"
  11.162 -  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)
  11.163 +  by (metis 11 6 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
  11.164  qed 
  11.165  
  11.166  ML {*AtpWrapper.problem_name := "set__equal_union"*}
  11.167 @@ -238,7 +237,7 @@
  11.168  
  11.169  lemma (*singleton_example_2:*)
  11.170       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
  11.171 -by (metis Set.subsetI Union_upper insert_code mem_def set_eq_subset)
  11.172 +by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
  11.173  
  11.174  lemma singleton_example_2:
  11.175       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    12.1 --- a/src/HOL/Set.thy	Mon Sep 21 12:23:05 2009 +0200
    12.2 +++ b/src/HOL/Set.thy	Mon Sep 21 12:24:21 2009 +0200
    12.3 @@ -652,8 +652,8 @@
    12.4  
    12.5  subsubsection {* Binary union -- Un *}
    12.6  
    12.7 -definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
    12.8 -  sup_set_eq [symmetric]: "A Un B = sup A B"
    12.9 +abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
   12.10 +  "op Un \<equiv> sup"
   12.11  
   12.12  notation (xsymbols)
   12.13    union  (infixl "\<union>" 65)
   12.14 @@ -663,7 +663,7 @@
   12.15  
   12.16  lemma Un_def:
   12.17    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
   12.18 -  by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
   12.19 +  by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
   12.20  
   12.21  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
   12.22    by (unfold Un_def) blast
   12.23 @@ -689,15 +689,13 @@
   12.24    by (simp add: Collect_def mem_def insert_compr Un_def)
   12.25  
   12.26  lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
   12.27 -  apply (fold sup_set_eq)
   12.28 -  apply (erule mono_sup)
   12.29 -  done
   12.30 +  by (fact mono_sup)
   12.31  
   12.32  
   12.33  subsubsection {* Binary intersection -- Int *}
   12.34  
   12.35 -definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
   12.36 -  inf_set_eq [symmetric]: "A Int B = inf A B"
   12.37 +abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
   12.38 +  "op Int \<equiv> inf"
   12.39  
   12.40  notation (xsymbols)
   12.41    inter  (infixl "\<inter>" 70)
   12.42 @@ -707,7 +705,7 @@
   12.43  
   12.44  lemma Int_def:
   12.45    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
   12.46 -  by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
   12.47 +  by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
   12.48  
   12.49  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   12.50    by (unfold Int_def) blast
   12.51 @@ -725,9 +723,7 @@
   12.52    by simp
   12.53  
   12.54  lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   12.55 -  apply (fold inf_set_eq)
   12.56 -  apply (erule mono_inf)
   12.57 -  done
   12.58 +  by (fact mono_inf)
   12.59  
   12.60  
   12.61  subsubsection {* Set difference *}
    13.1 --- a/src/HOL/Tools/Function/fundef_lib.ML	Mon Sep 21 12:23:05 2009 +0200
    13.2 +++ b/src/HOL/Tools/Function/fundef_lib.ML	Mon Sep 21 12:24:21 2009 +0200
    13.3 @@ -170,7 +170,7 @@
    13.4   end
    13.5  
    13.6  (* instance for unions *)
    13.7 -fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Set.union}
    13.8 +fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
    13.9    (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
   13.10                                       @{thms Un_empty_right} @
   13.11                                       @{thms Un_empty_left})) t
    14.1 --- a/src/HOL/Tools/Function/termination.ML	Mon Sep 21 12:23:05 2009 +0200
    14.2 +++ b/src/HOL/Tools/Function/termination.ML	Mon Sep 21 12:24:21 2009 +0200
    14.3 @@ -145,7 +145,7 @@
    14.4  
    14.5  fun mk_sum_skel rel =
    14.6    let
    14.7 -    val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
    14.8 +    val cs = FundefLib.dest_binop_list @{const_name Lattices.sup} rel
    14.9      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   14.10        let
   14.11          val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
   14.12 @@ -233,7 +233,7 @@
   14.13  fun CALLS tac i st =
   14.14    if Thm.no_prems st then all_tac st
   14.15    else case Thm.term_of (Thm.cprem_of st i) of
   14.16 -    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
   14.17 +    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Lattices.sup} rel, i) st
   14.18    |_ => no_tac st
   14.19  
   14.20  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
   14.21 @@ -293,7 +293,7 @@
   14.22            if null ineqs then
   14.23                Const (@{const_name Set.empty}, fastype_of rel)
   14.24            else
   14.25 -              foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
   14.26 +              foldr1 (HOLogic.mk_binop @{const_name Lattices.sup}) (map mk_compr ineqs)
   14.27  
   14.28        fun solve_membership_tac i =
   14.29            (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
    15.1 --- a/src/HOL/Tools/inductive_set.ML	Mon Sep 21 12:23:05 2009 +0200
    15.2 +++ b/src/HOL/Tools/inductive_set.ML	Mon Sep 21 12:24:21 2009 +0200
    15.3 @@ -74,8 +74,8 @@
    15.4          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
    15.5            (p (fold (Logic.all o Var) vs t) f)
    15.6          end;
    15.7 -      fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
    15.8 -        | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
    15.9 +      fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
   15.10 +        | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
   15.11          | mkop _ _ _ = NONE;
   15.12        fun mk_collect p T t =
   15.13          let val U = HOLogic.dest_setT T
    16.1 --- a/src/HOL/ex/predicate_compile.ML	Mon Sep 21 12:23:05 2009 +0200
    16.2 +++ b/src/HOL/ex/predicate_compile.ML	Mon Sep 21 12:24:21 2009 +0200
    16.3 @@ -2152,7 +2152,7 @@
    16.4      val (ts, _) = Predicate.yieldn k t;
    16.5      val elemsT = HOLogic.mk_set T ts;
    16.6    in if k = ~1 orelse length ts < k then elemsT
    16.7 -    else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
    16.8 +    else Const (@{const_name Lattices.sup}, setT --> setT --> setT) $ elemsT $ t_compr
    16.9    end;
   16.10  
   16.11  fun values_cmd modes k raw_t state =