merged
authorhaftmann
Mon Sep 21 11:01:49 2009 +0200 (2009-09-21)
changeset 32686a62c8627931b
parent 32621 a073cb249a06
parent 32685 29e4e567b5f4
child 32687 27530efec97a
merged
NEWS
     1.1 --- a/NEWS	Mon Sep 21 10:58:25 2009 +0200
     1.2 +++ b/NEWS	Mon Sep 21 11:01:49 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 10:58:25 2009 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Mon Sep 21 11:01:49 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/Inductive.thy	Mon Sep 21 10:58:25 2009 +0200
     3.2 +++ b/src/HOL/Inductive.thy	Mon Sep 21 11:01:49 2009 +0200
     3.3 @@ -83,7 +83,7 @@
     3.4        and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
     3.5    shows "P(a)"
     3.6    by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
     3.7 -    (auto simp: inf_set_eq intro: indhyp)
     3.8 +    (auto simp: intro: indhyp)
     3.9  
    3.10  lemma lfp_ordinal_induct:
    3.11    fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
    3.12 @@ -184,7 +184,7 @@
    3.13  
    3.14  text{*strong version, thanks to Coen and Frost*}
    3.15  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
    3.16 -by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
    3.17 +by (blast intro: weak_coinduct [OF _ coinduct_lemma])
    3.18  
    3.19  lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
    3.20    apply (rule order_trans)
     4.1 --- a/src/HOL/Library/Euclidean_Space.thy	Mon Sep 21 10:58:25 2009 +0200
     4.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon Sep 21 11:01:49 2009 +0200
     4.3 @@ -3649,10 +3649,7 @@
     4.4      from setsum_restrict_set[OF fS, of "\<lambda>v. u v *s v" S', symmetric] SS'
     4.5      have "setsum (\<lambda>v. ?u v *s v) S = setsum (\<lambda>v. u v *s v) S'"
     4.6        unfolding cond_value_iff cond_application_beta
     4.7 -      apply (simp add: cond_value_iff cong del: if_weak_cong)
     4.8 -      apply (rule setsum_cong)
     4.9 -      apply auto
    4.10 -      done
    4.11 +      by (simp add: cond_value_iff cong del: if_weak_cong)
    4.12      hence "setsum (\<lambda>v. ?u v *s v) S = y" by (metis u)
    4.13      hence "y \<in> ?rhs" by auto}
    4.14    moreover
     5.1 --- a/src/HOL/Library/Executable_Set.thy	Mon Sep 21 10:58:25 2009 +0200
     5.2 +++ b/src/HOL/Library/Executable_Set.thy	Mon Sep 21 11:01:49 2009 +0200
     5.3 @@ -12,6 +12,21 @@
     5.4  
     5.5  declare member [code] 
     5.6  
     5.7 +definition empty :: "'a set" where
     5.8 +  "empty = {}"
     5.9 +
    5.10 +declare empty_def [symmetric, code_unfold]
    5.11 +
    5.12 +definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    5.13 +  "inter = op \<inter>"
    5.14 +
    5.15 +declare inter_def [symmetric, code_unfold]
    5.16 +
    5.17 +definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    5.18 +  "union = op \<union>"
    5.19 +
    5.20 +declare union_def [symmetric, code_unfold]
    5.21 +
    5.22  definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    5.23    "subset = op \<le>"
    5.24  
    5.25 @@ -69,7 +84,7 @@
    5.26    Set ("\<module>Set")
    5.27  
    5.28  consts_code
    5.29 -  "Set.empty"         ("{*Fset.empty*}")
    5.30 +  "empty"             ("{*Fset.empty*}")
    5.31    "List_Set.is_empty" ("{*Fset.is_empty*}")
    5.32    "Set.insert"        ("{*Fset.insert*}")
    5.33    "List_Set.remove"   ("{*Fset.remove*}")
    5.34 @@ -77,8 +92,8 @@
    5.35    "List_Set.project"  ("{*Fset.filter*}")
    5.36    "Ball"              ("{*flip Fset.forall*}")
    5.37    "Bex"               ("{*flip Fset.exists*}")
    5.38 -  "op \<union>"              ("{*Fset.union*}")
    5.39 -  "op \<inter>"              ("{*Fset.inter*}")
    5.40 +  "union"             ("{*Fset.union*}")
    5.41 +  "inter"             ("{*Fset.inter*}")
    5.42    "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
    5.43    "Union"             ("{*Fset.Union*}")
    5.44    "Inter"             ("{*Fset.Inter*}")
     6.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Sep 21 10:58:25 2009 +0200
     6.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Sep 21 11:01:49 2009 +0200
     6.3 @@ -99,11 +99,9 @@
     6.4  
     6.5  lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast
     6.6  lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
     6.7 -  apply (auto simp add: closedin_def)
     6.8 +  apply (auto simp add: closedin_def Diff_Diff_Int)
     6.9    apply (metis openin_subset subset_eq)
    6.10 -  apply (auto simp add: Diff_Diff_Int)
    6.11 -  apply (subgoal_tac "topspace U \<inter> S = S")
    6.12 -  by auto
    6.13 +  done
    6.14  
    6.15  lemma openin_closedin:  "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
    6.16    by (simp add: openin_closedin_eq)
     7.1 --- a/src/HOL/MetisExamples/Message.thy	Mon Sep 21 10:58:25 2009 +0200
     7.2 +++ b/src/HOL/MetisExamples/Message.thy	Mon Sep 21 11:01:49 2009 +0200
     7.3 @@ -1,5 +1,4 @@
     7.4  (*  Title:      HOL/MetisTest/Message.thy
     7.5 -    ID:         $Id$
     7.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7  
     7.8  Testing the metis method
     7.9 @@ -711,17 +710,17 @@
    7.10  proof (neg_clausify)
    7.11  assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
    7.12  have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
    7.13 -  by (metis analz_synth_Un sup_set_eq sup_set_eq sup_set_eq)
    7.14 +  by (metis analz_synth_Un)
    7.15  have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
    7.16 -  by (metis 0 sup_set_eq)
    7.17 +  by (metis 0)
    7.18  have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
    7.19 -  by (metis 1 Un_commute sup_set_eq sup_set_eq)
    7.20 +  by (metis 1 Un_commute)
    7.21  have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
    7.22 -  by (metis 3 Un_empty_right sup_set_eq)
    7.23 +  by (metis 3 Un_empty_right)
    7.24  have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
    7.25 -  by (metis 4 Un_empty_right sup_set_eq)
    7.26 +  by (metis 4 Un_empty_right)
    7.27  have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
    7.28 -  by (metis 5 Un_commute sup_set_eq sup_set_eq)
    7.29 +  by (metis 5 Un_commute)
    7.30  show "False"
    7.31    by (metis 2 6)
    7.32  qed
     8.1 --- a/src/HOL/MetisExamples/set.thy	Mon Sep 21 10:58:25 2009 +0200
     8.2 +++ b/src/HOL/MetisExamples/set.thy	Mon Sep 21 11:01:49 2009 +0200
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      HOL/MetisExamples/set.thy
     8.5 -    ID:         $Id$
     8.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7  
     8.8  Testing the metis method
     8.9 @@ -36,23 +35,23 @@
    8.10  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    8.11  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
    8.12  have 6: "sup Y Z = X \<or> Y \<subseteq> X"
    8.13 -  by (metis 0 sup_set_eq)
    8.14 +  by (metis 0)
    8.15  have 7: "sup Y Z = X \<or> Z \<subseteq> X"
    8.16 -  by (metis 1 sup_set_eq)
    8.17 +  by (metis 1)
    8.18  have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3"
    8.19 -  by (metis 5 sup_set_eq)
    8.20 +  by (metis 5)
    8.21  have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
    8.22 -  by (metis 2 sup_set_eq)
    8.23 +  by (metis 2)
    8.24  have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
    8.25 -  by (metis 3 sup_set_eq)
    8.26 +  by (metis 3)
    8.27  have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
    8.28 -  by (metis 4 sup_set_eq)
    8.29 +  by (metis 4)
    8.30  have 12: "Z \<subseteq> X"
    8.31 -  by (metis Un_upper2 sup_set_eq 7)
    8.32 +  by (metis Un_upper2 7)
    8.33  have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
    8.34 -  by (metis 8 Un_upper2 sup_set_eq)
    8.35 +  by (metis 8 Un_upper2)
    8.36  have 14: "Y \<subseteq> X"
    8.37 -  by (metis Un_upper1 sup_set_eq 6)
    8.38 +  by (metis Un_upper1 6)
    8.39  have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
    8.40    by (metis 10 12)
    8.41  have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
    8.42 @@ -66,17 +65,17 @@
    8.43  have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X"
    8.44    by (metis 16 14)
    8.45  have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
    8.46 -  by (metis 13 Un_upper1 sup_set_eq)
    8.47 +  by (metis 13 Un_upper1)
    8.48  have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
    8.49    by (metis equalityI 21)
    8.50  have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
    8.51 -  by (metis 22 Un_least sup_set_eq)
    8.52 +  by (metis 22 Un_least)
    8.53  have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X"
    8.54    by (metis 23 12)
    8.55  have 25: "sup Y Z = X"
    8.56    by (metis 24 14)
    8.57  have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3"
    8.58 -  by (metis Un_least sup_set_eq 25)
    8.59 +  by (metis Un_least 25)
    8.60  have 27: "Y \<subseteq> x"
    8.61    by (metis 20 25)
    8.62  have 28: "Z \<subseteq> x"
    8.63 @@ -105,31 +104,31 @@
    8.64  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    8.65  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
    8.66  have 6: "sup Y Z = X \<or> Y \<subseteq> X"
    8.67 -  by (metis 0 sup_set_eq)
    8.68 +  by (metis 0)
    8.69  have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
    8.70 -  by (metis 2 sup_set_eq)
    8.71 +  by (metis 2)
    8.72  have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
    8.73 -  by (metis 4 sup_set_eq)
    8.74 +  by (metis 4)
    8.75  have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
    8.76 -  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
    8.77 +  by (metis 5 Un_upper2)
    8.78  have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
    8.79 -  by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
    8.80 +  by (metis 3 Un_upper2)
    8.81  have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
    8.82 -  by (metis 8 Un_upper2 sup_set_eq sup_set_eq)
    8.83 +  by (metis 8 Un_upper2)
    8.84  have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
    8.85 -  by (metis 10 Un_upper1 sup_set_eq)
    8.86 +  by (metis 10 Un_upper1)
    8.87  have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
    8.88 -  by (metis 9 Un_upper1 sup_set_eq)
    8.89 +  by (metis 9 Un_upper1)
    8.90  have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
    8.91 -  by (metis equalityI 13 Un_least sup_set_eq)
    8.92 +  by (metis equalityI 13 Un_least)
    8.93  have 15: "sup Y Z = X"
    8.94 -  by (metis 14 sup_set_eq 1 sup_set_eq sup_set_eq 6)
    8.95 +  by (metis 14 1 6)
    8.96  have 16: "Y \<subseteq> x"
    8.97 -  by (metis 7 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq 15)
    8.98 +  by (metis 7 Un_upper2 Un_upper1 15)
    8.99  have 17: "\<not> X \<subseteq> x"
   8.100 -  by (metis 11 Un_upper1 sup_set_eq 15)
   8.101 +  by (metis 11 Un_upper1 15)
   8.102  have 18: "X \<subseteq> x"
   8.103 -  by (metis Un_least sup_set_eq 15 12 15 16)
   8.104 +  by (metis Un_least 15 12 15 16)
   8.105  show "False"
   8.106    by (metis 18 17)
   8.107  qed
   8.108 @@ -148,23 +147,23 @@
   8.109  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   8.110  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
   8.111  have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   8.112 -  by (metis 3 sup_set_eq)
   8.113 +  by (metis 3)
   8.114  have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
   8.115 -  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
   8.116 +  by (metis 5 Un_upper2)
   8.117  have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   8.118 -  by (metis 2 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
   8.119 +  by (metis 2 Un_upper2)
   8.120  have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
   8.121 -  by (metis 6 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq)
   8.122 +  by (metis 6 Un_upper2 Un_upper1)
   8.123  have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
   8.124 -  by (metis equalityI 7 Un_upper1 sup_set_eq)
   8.125 +  by (metis equalityI 7 Un_upper1)
   8.126  have 11: "sup Y Z = X"
   8.127 -  by (metis 10 Un_least sup_set_eq sup_set_eq 1 sup_set_eq sup_set_eq 0 sup_set_eq)
   8.128 +  by (metis 10 Un_least 1 0)
   8.129  have 12: "Z \<subseteq> x"
   8.130    by (metis 9 11)
   8.131  have 13: "X \<subseteq> x"
   8.132 -  by (metis Un_least sup_set_eq 11 12 8 Un_upper1 sup_set_eq sup_set_eq 11)
   8.133 +  by (metis Un_least 11 12 8 Un_upper1 11)
   8.134  show "False"
   8.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)
   8.136 +  by (metis 13 4 Un_upper2 Un_upper1 11)
   8.137  qed
   8.138  
   8.139  (*Example included in TPHOLs paper*)
   8.140 @@ -183,19 +182,19 @@
   8.141  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   8.142  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
   8.143  have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   8.144 -  by (metis 4 sup_set_eq)
   8.145 +  by (metis 4)
   8.146  have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   8.147 -  by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
   8.148 +  by (metis 3 Un_upper2)
   8.149  have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
   8.150 -  by (metis 7 Un_upper1 sup_set_eq sup_set_eq)
   8.151 +  by (metis 7 Un_upper1)
   8.152  have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
   8.153 -  by (metis equalityI 5 sup_set_eq Un_upper2 sup_set_eq Un_upper1 sup_set_eq Un_least sup_set_eq)
   8.154 +  by (metis equalityI 5 Un_upper2 Un_upper1 Un_least)
   8.155  have 10: "Y \<subseteq> x"
   8.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)
   8.157 +  by (metis 2 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
   8.158  have 11: "X \<subseteq> x"
   8.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)
   8.160 +  by (metis Un_least 9 Un_upper2 1 Un_upper1 0 8 9 Un_upper2 1 Un_upper1 0 10)
   8.161  show "False"
   8.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)
   8.163 +  by (metis 11 6 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
   8.164  qed 
   8.165  
   8.166  ML {*AtpWrapper.problem_name := "set__equal_union"*}
   8.167 @@ -238,7 +237,7 @@
   8.168  
   8.169  lemma (*singleton_example_2:*)
   8.170       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
   8.171 -by (metis Set.subsetI Union_upper insert_code mem_def set_eq_subset)
   8.172 +by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
   8.173  
   8.174  lemma singleton_example_2:
   8.175       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
     9.1 --- a/src/HOL/Set.thy	Mon Sep 21 10:58:25 2009 +0200
     9.2 +++ b/src/HOL/Set.thy	Mon Sep 21 11:01:49 2009 +0200
     9.3 @@ -652,8 +652,8 @@
     9.4  
     9.5  subsubsection {* Binary union -- Un *}
     9.6  
     9.7 -definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
     9.8 -  sup_set_eq [symmetric]: "A Un B = sup A B"
     9.9 +abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
    9.10 +  "op Un \<equiv> sup"
    9.11  
    9.12  notation (xsymbols)
    9.13    union  (infixl "\<union>" 65)
    9.14 @@ -663,7 +663,7 @@
    9.15  
    9.16  lemma Un_def:
    9.17    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
    9.18 -  by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
    9.19 +  by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
    9.20  
    9.21  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
    9.22    by (unfold Un_def) blast
    9.23 @@ -689,15 +689,13 @@
    9.24    by (simp add: Collect_def mem_def insert_compr Un_def)
    9.25  
    9.26  lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
    9.27 -  apply (fold sup_set_eq)
    9.28 -  apply (erule mono_sup)
    9.29 -  done
    9.30 +  by (fact mono_sup)
    9.31  
    9.32  
    9.33  subsubsection {* Binary intersection -- Int *}
    9.34  
    9.35 -definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    9.36 -  inf_set_eq [symmetric]: "A Int B = inf A B"
    9.37 +abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    9.38 +  "op Int \<equiv> inf"
    9.39  
    9.40  notation (xsymbols)
    9.41    inter  (infixl "\<inter>" 70)
    9.42 @@ -707,7 +705,7 @@
    9.43  
    9.44  lemma Int_def:
    9.45    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
    9.46 -  by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
    9.47 +  by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
    9.48  
    9.49  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
    9.50    by (unfold Int_def) blast
    9.51 @@ -725,9 +723,7 @@
    9.52    by simp
    9.53  
    9.54  lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
    9.55 -  apply (fold inf_set_eq)
    9.56 -  apply (erule mono_inf)
    9.57 -  done
    9.58 +  by (fact mono_inf)
    9.59  
    9.60  
    9.61  subsubsection {* Set difference *}
    10.1 --- a/src/HOL/Tools/Function/fundef_lib.ML	Mon Sep 21 10:58:25 2009 +0200
    10.2 +++ b/src/HOL/Tools/Function/fundef_lib.ML	Mon Sep 21 11:01:49 2009 +0200
    10.3 @@ -170,7 +170,7 @@
    10.4   end
    10.5  
    10.6  (* instance for unions *)
    10.7 -fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Set.union}
    10.8 +fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
    10.9    (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
   10.10                                       @{thms Un_empty_right} @
   10.11                                       @{thms Un_empty_left})) t
    11.1 --- a/src/HOL/Tools/Function/termination.ML	Mon Sep 21 10:58:25 2009 +0200
    11.2 +++ b/src/HOL/Tools/Function/termination.ML	Mon Sep 21 11:01:49 2009 +0200
    11.3 @@ -145,7 +145,7 @@
    11.4  
    11.5  fun mk_sum_skel rel =
    11.6    let
    11.7 -    val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
    11.8 +    val cs = FundefLib.dest_binop_list @{const_name Lattices.sup} rel
    11.9      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   11.10        let
   11.11          val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
   11.12 @@ -233,7 +233,7 @@
   11.13  fun CALLS tac i st =
   11.14    if Thm.no_prems st then all_tac st
   11.15    else case Thm.term_of (Thm.cprem_of st i) of
   11.16 -    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
   11.17 +    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Lattices.sup} rel, i) st
   11.18    |_ => no_tac st
   11.19  
   11.20  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
   11.21 @@ -293,7 +293,7 @@
   11.22            if null ineqs then
   11.23                Const (@{const_name Set.empty}, fastype_of rel)
   11.24            else
   11.25 -              foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
   11.26 +              foldr1 (HOLogic.mk_binop @{const_name Lattices.sup}) (map mk_compr ineqs)
   11.27  
   11.28        fun solve_membership_tac i =
   11.29            (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
    12.1 --- a/src/HOL/Tools/inductive_set.ML	Mon Sep 21 10:58:25 2009 +0200
    12.2 +++ b/src/HOL/Tools/inductive_set.ML	Mon Sep 21 11:01:49 2009 +0200
    12.3 @@ -74,8 +74,8 @@
    12.4          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
    12.5            (p (fold (Logic.all o Var) vs t) f)
    12.6          end;
    12.7 -      fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
    12.8 -        | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
    12.9 +      fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
   12.10 +        | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
   12.11          | mkop _ _ _ = NONE;
   12.12        fun mk_collect p T t =
   12.13          let val U = HOLogic.dest_setT T
    13.1 --- a/src/HOL/ex/predicate_compile.ML	Mon Sep 21 10:58:25 2009 +0200
    13.2 +++ b/src/HOL/ex/predicate_compile.ML	Mon Sep 21 11:01:49 2009 +0200
    13.3 @@ -2152,7 +2152,7 @@
    13.4      val (ts, _) = Predicate.yieldn k t;
    13.5      val elemsT = HOLogic.mk_set T ts;
    13.6    in if k = ~1 orelse length ts < k then elemsT
    13.7 -    else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
    13.8 +    else Const (@{const_name Lattices.sup}, setT --> setT --> setT) $ elemsT $ t_compr
    13.9    end;
   13.10  
   13.11  fun values_cmd modes k raw_t state =