merged
authorhaftmann
Wed Sep 23 08:26:12 2009 +0200 (2009-09-23)
changeset 32699250b4d8342ca
parent 32646 962b4354ed90
parent 32698 be4b248616c0
child 32700 e743ca6e97e7
merged
     1.1 --- a/NEWS	Tue Sep 22 11:26:46 2009 +0200
     1.2 +++ b/NEWS	Wed Sep 23 08:26:12 2009 +0200
     1.3 @@ -94,13 +94,18 @@
     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)
    1.12      Complete_Lattice.UNION  (for SUPR)
    1.13    - object-logic definitions as far as appropriate
    1.14  
    1.15 -  INCOMPATIBILITY.
    1.16 +INCOMPATIBILITY.  Care is required when theorems Int_subset_iff or
    1.17 +Un_subset_iff are explicitly deleted as default simp rules;  then
    1.18 +also their lattice counterparts le_inf_iff and le_sup_iff have to be
    1.19 +deleted to achieve the desired effect.
    1.20  
    1.21  * Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no
    1.22  simp rules by default any longer.  The same applies to
     2.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Tue Sep 22 11:26:46 2009 +0200
     2.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Wed Sep 23 08:26:12 2009 +0200
     2.3 @@ -212,7 +212,7 @@
     2.4    apply (induct set: finite)
     2.5     apply simp
     2.6    apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
     2.7 -    Int_mono2 Un_subset_iff)
     2.8 +    Int_mono2)
     2.9    done
    2.10  
    2.11  lemma (in LCD) foldD_nest_Un_disjoint:
    2.12 @@ -274,14 +274,14 @@
    2.13    apply (simp add: AC insert_absorb Int_insert_left
    2.14      LCD.foldD_insert [OF LCD.intro [of D]]
    2.15      LCD.foldD_closed [OF LCD.intro [of D]]
    2.16 -    Int_mono2 Un_subset_iff)
    2.17 +    Int_mono2)
    2.18    done
    2.19  
    2.20  lemma (in ACeD) foldD_Un_disjoint:
    2.21    "[| finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D |] ==>
    2.22      foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
    2.23    by (simp add: foldD_Un_Int
    2.24 -    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
    2.25 +    left_commute LCD.foldD_closed [OF LCD.intro [of D]])
    2.26  
    2.27  
    2.28  subsubsection {* Products over Finite Sets *}
    2.29 @@ -377,7 +377,7 @@
    2.30    from insert have A: "g \<in> A -> carrier G" by fast
    2.31    from insert A a show ?case
    2.32      by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
    2.33 -          Int_mono2 Un_subset_iff) 
    2.34 +          Int_mono2) 
    2.35  qed
    2.36  
    2.37  lemma finprod_Un_disjoint:
     3.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Tue Sep 22 11:26:46 2009 +0200
     3.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Wed Sep 23 08:26:12 2009 +0200
     3.3 @@ -11,7 +11,9 @@
     3.4  
     3.5  header {*Extensions to Standard Theories*}
     3.6  
     3.7 -theory Extensions imports "../Event" begin
     3.8 +theory Extensions
     3.9 +imports "../Event"
    3.10 +begin
    3.11  
    3.12  subsection{*Extensions to Theory @{text Set}*}
    3.13  
    3.14 @@ -173,7 +175,7 @@
    3.15  subsubsection{*lemmas on analz*}
    3.16  
    3.17  lemma analz_UnI1 [intro]: "X:analz G ==> X:analz (G Un H)"
    3.18 -by (subgoal_tac "G <= G Un H", auto dest: analz_mono)
    3.19 +  by (subgoal_tac "G <= G Un H") (blast dest: analz_mono)+
    3.20  
    3.21  lemma analz_sub: "[| X:analz G; G <= H |] ==> X:analz H"
    3.22  by (auto dest: analz_mono)
     4.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Sep 22 11:26:46 2009 +0200
     4.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed Sep 23 08:26:12 2009 +0200
     4.3 @@ -1747,7 +1747,7 @@
     4.4        have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"
     4.5  	by (simp add: need_second_arg_def)
     4.6        with s2
     4.7 -      show ?thesis using False by (simp add: Un_subset_iff)
     4.8 +      show ?thesis using False by simp
     4.9      qed
    4.10    next
    4.11      case Super thus ?case by simp
     5.1 --- a/src/HOL/Bali/TypeSafe.thy	Tue Sep 22 11:26:46 2009 +0200
     5.2 +++ b/src/HOL/Bali/TypeSafe.thy	Wed Sep 23 08:26:12 2009 +0200
     5.3 @@ -2953,7 +2953,7 @@
     5.4  	  by simp
     5.5  	from da_e1 s0_s1 True obtain E1' where
     5.6  	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
     5.7 -	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
     5.8 +	  by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
     5.9  	with conf_s1 wt_e1
    5.10  	obtain 
    5.11  	  "s2\<Colon>\<preceq>(G, L)"
    5.12 @@ -2972,7 +2972,7 @@
    5.13  	  by simp
    5.14  	from da_e2 s0_s1 False obtain E2' where
    5.15  	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
    5.16 -	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
    5.17 +	  by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
    5.18  	with conf_s1 wt_e2
    5.19  	obtain 
    5.20  	  "s2\<Colon>\<preceq>(G, L)"
     6.1 --- a/src/HOL/Finite_Set.thy	Tue Sep 22 11:26:46 2009 +0200
     6.2 +++ b/src/HOL/Finite_Set.thy	Wed Sep 23 08:26:12 2009 +0200
     6.3 @@ -1565,9 +1565,7 @@
     6.4    apply (rule finite_subset)
     6.5    prefer 2
     6.6    apply assumption
     6.7 -  apply auto
     6.8 -  apply (rule setsum_cong)
     6.9 -  apply auto
    6.10 +  apply (auto simp add: sup_absorb2)
    6.11  done
    6.12  
    6.13  lemma setsum_right_distrib: 
     7.1 --- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Tue Sep 22 11:26:46 2009 +0200
     7.2 +++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Wed Sep 23 08:26:12 2009 +0200
     7.3 @@ -253,7 +253,7 @@
     7.4      \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."
     7.5  apply (unfold Propagate_Black_def  PBInv_def Auxk_def collector_defs)
     7.6  apply annhoare
     7.7 -apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
     7.8 +apply(simp_all add: Graph6 Graph7 Graph8 Graph12)
     7.9         apply force
    7.10        apply force
    7.11       apply force
    7.12 @@ -297,8 +297,6 @@
    7.13  apply(erule subset_psubset_trans)
    7.14  apply(erule Graph11)
    7.15  apply fast
    7.16 ---{* 3 subgoals left *}
    7.17 -apply force
    7.18  --{* 2 subgoals left *}
    7.19  apply clarify
    7.20  apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
     8.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Tue Sep 22 11:26:46 2009 +0200
     8.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Wed Sep 23 08:26:12 2009 +0200
     8.3 @@ -276,8 +276,6 @@
     8.4    apply(force)
     8.5   apply(force)
     8.6  apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
     8.7 ---{* 3 subgoals left *}
     8.8 -apply force
     8.9  --{* 2 subgoals left *}
    8.10  apply clarify
    8.11  apply(conjI_tac)
    8.12 @@ -1235,9 +1233,9 @@
    8.13  apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
    8.14  apply(tactic  {* TRYALL (interfree_aux_tac) *})
    8.15  --{* 76 subgoals left *}
    8.16 -apply (clarify,simp add: nth_list_update)+
    8.17 +apply (clarsimp simp add: nth_list_update)+
    8.18  --{* 56 subgoals left *}
    8.19 -apply(clarify,simp add:Mul_AppendInv_def Append_to_free0 nth_list_update)+
    8.20 +apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+
    8.21  done
    8.22  
    8.23  subsubsection {* The Multi-Mutator Garbage Collection Algorithm *}
     9.1 --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Tue Sep 22 11:26:46 2009 +0200
     9.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Sep 23 08:26:12 2009 +0200
     9.3 @@ -4,8 +4,8 @@
     9.4  
     9.5  subsection {* Proof System for Component Programs *}
     9.6  
     9.7 -declare Un_subset_iff [iff del]
     9.8 -declare Cons_eq_map_conv[iff]
     9.9 +declare Un_subset_iff [simp del] le_sup_iff [simp del]
    9.10 +declare Cons_eq_map_conv [iff]
    9.11  
    9.12  constdefs
    9.13    stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"  
    10.1 --- a/src/HOL/Inductive.thy	Tue Sep 22 11:26:46 2009 +0200
    10.2 +++ b/src/HOL/Inductive.thy	Wed Sep 23 08:26:12 2009 +0200
    10.3 @@ -83,7 +83,7 @@
    10.4        and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
    10.5    shows "P(a)"
    10.6    by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
    10.7 -    (auto simp: inf_set_eq intro: indhyp)
    10.8 +    (auto simp: intro: indhyp)
    10.9  
   10.10  lemma lfp_ordinal_induct:
   10.11    fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
   10.12 @@ -184,7 +184,7 @@
   10.13  
   10.14  text{*strong version, thanks to Coen and Frost*}
   10.15  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
   10.16 -by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
   10.17 +by (blast intro: weak_coinduct [OF _ coinduct_lemma])
   10.18  
   10.19  lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
   10.20    apply (rule order_trans)
    11.1 --- a/src/HOL/Library/Euclidean_Space.thy	Tue Sep 22 11:26:46 2009 +0200
    11.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Wed Sep 23 08:26:12 2009 +0200
    11.3 @@ -3649,10 +3649,7 @@
    11.4      from setsum_restrict_set[OF fS, of "\<lambda>v. u v *s v" S', symmetric] SS'
    11.5      have "setsum (\<lambda>v. ?u v *s v) S = setsum (\<lambda>v. u v *s v) S'"
    11.6        unfolding cond_value_iff cond_application_beta
    11.7 -      apply (simp add: cond_value_iff cong del: if_weak_cong)
    11.8 -      apply (rule setsum_cong)
    11.9 -      apply auto
   11.10 -      done
   11.11 +      by (simp add: cond_value_iff inf_absorb2 cong del: if_weak_cong)
   11.12      hence "setsum (\<lambda>v. ?u v *s v) S = y" by (metis u)
   11.13      hence "y \<in> ?rhs" by auto}
   11.14    moreover
    12.1 --- a/src/HOL/Library/Executable_Set.thy	Tue Sep 22 11:26:46 2009 +0200
    12.2 +++ b/src/HOL/Library/Executable_Set.thy	Wed Sep 23 08:26:12 2009 +0200
    12.3 @@ -12,6 +12,21 @@
    12.4  
    12.5  declare member [code] 
    12.6  
    12.7 +definition empty :: "'a set" where
    12.8 +  "empty = {}"
    12.9 +
   12.10 +declare empty_def [symmetric, code_unfold]
   12.11 +
   12.12 +definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   12.13 +  "inter = op \<inter>"
   12.14 +
   12.15 +declare inter_def [symmetric, code_unfold]
   12.16 +
   12.17 +definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   12.18 +  "union = op \<union>"
   12.19 +
   12.20 +declare union_def [symmetric, code_unfold]
   12.21 +
   12.22  definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   12.23    "subset = op \<le>"
   12.24  
   12.25 @@ -69,7 +84,7 @@
   12.26    Set ("\<module>Set")
   12.27  
   12.28  consts_code
   12.29 -  "Set.empty"         ("{*Fset.empty*}")
   12.30 +  "empty"             ("{*Fset.empty*}")
   12.31    "List_Set.is_empty" ("{*Fset.is_empty*}")
   12.32    "Set.insert"        ("{*Fset.insert*}")
   12.33    "List_Set.remove"   ("{*Fset.remove*}")
   12.34 @@ -77,8 +92,8 @@
   12.35    "List_Set.project"  ("{*Fset.filter*}")
   12.36    "Ball"              ("{*flip Fset.forall*}")
   12.37    "Bex"               ("{*flip Fset.exists*}")
   12.38 -  "op \<union>"              ("{*Fset.union*}")
   12.39 -  "op \<inter>"              ("{*Fset.inter*}")
   12.40 +  "union"             ("{*Fset.union*}")
   12.41 +  "inter"             ("{*Fset.inter*}")
   12.42    "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
   12.43    "Union"             ("{*Fset.Union*}")
   12.44    "Inter"             ("{*Fset.Inter*}")
    13.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Sep 22 11:26:46 2009 +0200
    13.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Wed Sep 23 08:26:12 2009 +0200
    13.3 @@ -99,11 +99,9 @@
    13.4  
    13.5  lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast
    13.6  lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
    13.7 -  apply (auto simp add: closedin_def)
    13.8 +  apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)
    13.9    apply (metis openin_subset subset_eq)
   13.10 -  apply (auto simp add: Diff_Diff_Int)
   13.11 -  apply (subgoal_tac "topspace U \<inter> S = S")
   13.12 -  by auto
   13.13 +  done
   13.14  
   13.15  lemma openin_closedin:  "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
   13.16    by (simp add: openin_closedin_eq)
    14.1 --- a/src/HOL/MetisExamples/Message.thy	Tue Sep 22 11:26:46 2009 +0200
    14.2 +++ b/src/HOL/MetisExamples/Message.thy	Wed Sep 23 08:26:12 2009 +0200
    14.3 @@ -1,5 +1,4 @@
    14.4  (*  Title:      HOL/MetisTest/Message.thy
    14.5 -    ID:         $Id$
    14.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.7  
    14.8  Testing the metis method
    14.9 @@ -711,17 +710,17 @@
   14.10  proof (neg_clausify)
   14.11  assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
   14.12  have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
   14.13 -  by (metis analz_synth_Un sup_set_eq sup_set_eq sup_set_eq)
   14.14 +  by (metis analz_synth_Un)
   14.15  have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
   14.16 -  by (metis 0 sup_set_eq)
   14.17 +  by (metis 0)
   14.18  have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
   14.19 -  by (metis 1 Un_commute sup_set_eq sup_set_eq)
   14.20 +  by (metis 1 Un_commute)
   14.21  have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
   14.22 -  by (metis 3 Un_empty_right sup_set_eq)
   14.23 +  by (metis 3 Un_empty_right)
   14.24  have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
   14.25 -  by (metis 4 Un_empty_right sup_set_eq)
   14.26 +  by (metis 4 Un_empty_right)
   14.27  have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
   14.28 -  by (metis 5 Un_commute sup_set_eq sup_set_eq)
   14.29 +  by (metis 5 Un_commute)
   14.30  show "False"
   14.31    by (metis 2 6)
   14.32  qed
    15.1 --- a/src/HOL/MetisExamples/set.thy	Tue Sep 22 11:26:46 2009 +0200
    15.2 +++ b/src/HOL/MetisExamples/set.thy	Wed Sep 23 08:26:12 2009 +0200
    15.3 @@ -1,5 +1,4 @@
    15.4  (*  Title:      HOL/MetisExamples/set.thy
    15.5 -    ID:         $Id$
    15.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.7  
    15.8  Testing the metis method
    15.9 @@ -36,23 +35,23 @@
   15.10  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   15.11  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
   15.12  have 6: "sup Y Z = X \<or> Y \<subseteq> X"
   15.13 -  by (metis 0 sup_set_eq)
   15.14 +  by (metis 0)
   15.15  have 7: "sup Y Z = X \<or> Z \<subseteq> X"
   15.16 -  by (metis 1 sup_set_eq)
   15.17 +  by (metis 1)
   15.18  have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3"
   15.19 -  by (metis 5 sup_set_eq)
   15.20 +  by (metis 5)
   15.21  have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   15.22 -  by (metis 2 sup_set_eq)
   15.23 +  by (metis 2)
   15.24  have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   15.25 -  by (metis 3 sup_set_eq)
   15.26 +  by (metis 3)
   15.27  have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   15.28 -  by (metis 4 sup_set_eq)
   15.29 +  by (metis 4)
   15.30  have 12: "Z \<subseteq> X"
   15.31 -  by (metis Un_upper2 sup_set_eq 7)
   15.32 +  by (metis Un_upper2 7)
   15.33  have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
   15.34 -  by (metis 8 Un_upper2 sup_set_eq)
   15.35 +  by (metis 8 Un_upper2)
   15.36  have 14: "Y \<subseteq> X"
   15.37 -  by (metis Un_upper1 sup_set_eq 6)
   15.38 +  by (metis Un_upper1 6)
   15.39  have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   15.40    by (metis 10 12)
   15.41  have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   15.42 @@ -66,17 +65,17 @@
   15.43  have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X"
   15.44    by (metis 16 14)
   15.45  have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
   15.46 -  by (metis 13 Un_upper1 sup_set_eq)
   15.47 +  by (metis 13 Un_upper1)
   15.48  have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
   15.49    by (metis equalityI 21)
   15.50  have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
   15.51 -  by (metis 22 Un_least sup_set_eq)
   15.52 +  by (metis 22 Un_least)
   15.53  have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X"
   15.54    by (metis 23 12)
   15.55  have 25: "sup Y Z = X"
   15.56    by (metis 24 14)
   15.57  have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3"
   15.58 -  by (metis Un_least sup_set_eq 25)
   15.59 +  by (metis Un_least 25)
   15.60  have 27: "Y \<subseteq> x"
   15.61    by (metis 20 25)
   15.62  have 28: "Z \<subseteq> x"
   15.63 @@ -105,31 +104,31 @@
   15.64  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
   15.65  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
   15.66  have 6: "sup Y Z = X \<or> Y \<subseteq> X"
   15.67 -  by (metis 0 sup_set_eq)
   15.68 +  by (metis 0)
   15.69  have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   15.70 -  by (metis 2 sup_set_eq)
   15.71 +  by (metis 2)
   15.72  have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   15.73 -  by (metis 4 sup_set_eq)
   15.74 +  by (metis 4)
   15.75  have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
   15.76 -  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
   15.77 +  by (metis 5 Un_upper2)
   15.78  have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
   15.79 -  by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
   15.80 +  by (metis 3 Un_upper2)
   15.81  have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
   15.82 -  by (metis 8 Un_upper2 sup_set_eq sup_set_eq)
   15.83 +  by (metis 8 Un_upper2)
   15.84  have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
   15.85 -  by (metis 10 Un_upper1 sup_set_eq)
   15.86 +  by (metis 10 Un_upper1)
   15.87  have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
   15.88 -  by (metis 9 Un_upper1 sup_set_eq)
   15.89 +  by (metis 9 Un_upper1)
   15.90  have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
   15.91 -  by (metis equalityI 13 Un_least sup_set_eq)
   15.92 +  by (metis equalityI 13 Un_least)
   15.93  have 15: "sup Y Z = X"
   15.94 -  by (metis 14 sup_set_eq 1 sup_set_eq sup_set_eq 6)
   15.95 +  by (metis 14 1 6)
   15.96  have 16: "Y \<subseteq> x"
   15.97 -  by (metis 7 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq 15)
   15.98 +  by (metis 7 Un_upper2 Un_upper1 15)
   15.99  have 17: "\<not> X \<subseteq> x"
  15.100 -  by (metis 11 Un_upper1 sup_set_eq 15)
  15.101 +  by (metis 11 Un_upper1 15)
  15.102  have 18: "X \<subseteq> x"
  15.103 -  by (metis Un_least sup_set_eq 15 12 15 16)
  15.104 +  by (metis Un_least 15 12 15 16)
  15.105  show "False"
  15.106    by (metis 18 17)
  15.107  qed
  15.108 @@ -148,23 +147,23 @@
  15.109  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
  15.110  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
  15.111  have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
  15.112 -  by (metis 3 sup_set_eq)
  15.113 +  by (metis 3)
  15.114  have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
  15.115 -  by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
  15.116 +  by (metis 5 Un_upper2)
  15.117  have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
  15.118 -  by (metis 2 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
  15.119 +  by (metis 2 Un_upper2)
  15.120  have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
  15.121 -  by (metis 6 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq)
  15.122 +  by (metis 6 Un_upper2 Un_upper1)
  15.123  have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
  15.124 -  by (metis equalityI 7 Un_upper1 sup_set_eq)
  15.125 +  by (metis equalityI 7 Un_upper1)
  15.126  have 11: "sup Y Z = X"
  15.127 -  by (metis 10 Un_least sup_set_eq sup_set_eq 1 sup_set_eq sup_set_eq 0 sup_set_eq)
  15.128 +  by (metis 10 Un_least 1 0)
  15.129  have 12: "Z \<subseteq> x"
  15.130    by (metis 9 11)
  15.131  have 13: "X \<subseteq> x"
  15.132 -  by (metis Un_least sup_set_eq 11 12 8 Un_upper1 sup_set_eq sup_set_eq 11)
  15.133 +  by (metis Un_least 11 12 8 Un_upper1 11)
  15.134  show "False"
  15.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)
  15.136 +  by (metis 13 4 Un_upper2 Un_upper1 11)
  15.137  qed
  15.138  
  15.139  (*Example included in TPHOLs paper*)
  15.140 @@ -183,19 +182,19 @@
  15.141  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
  15.142  assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
  15.143  have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
  15.144 -  by (metis 4 sup_set_eq)
  15.145 +  by (metis 4)
  15.146  have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
  15.147 -  by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
  15.148 +  by (metis 3 Un_upper2)
  15.149  have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
  15.150 -  by (metis 7 Un_upper1 sup_set_eq sup_set_eq)
  15.151 +  by (metis 7 Un_upper1)
  15.152  have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
  15.153 -  by (metis equalityI 5 sup_set_eq Un_upper2 sup_set_eq Un_upper1 sup_set_eq Un_least sup_set_eq)
  15.154 +  by (metis equalityI 5 Un_upper2 Un_upper1 Un_least)
  15.155  have 10: "Y \<subseteq> x"
  15.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)
  15.157 +  by (metis 2 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
  15.158  have 11: "X \<subseteq> x"
  15.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)
  15.160 +  by (metis Un_least 9 Un_upper2 1 Un_upper1 0 8 9 Un_upper2 1 Un_upper1 0 10)
  15.161  show "False"
  15.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)
  15.163 +  by (metis 11 6 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
  15.164  qed 
  15.165  
  15.166  ML {*AtpWrapper.problem_name := "set__equal_union"*}
  15.167 @@ -238,7 +237,7 @@
  15.168  
  15.169  lemma (*singleton_example_2:*)
  15.170       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
  15.171 -by (metis Set.subsetI Union_upper insert_code mem_def set_eq_subset)
  15.172 +by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
  15.173  
  15.174  lemma singleton_example_2:
  15.175       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    16.1 --- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Tue Sep 22 11:26:46 2009 +0200
    16.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Wed Sep 23 08:26:12 2009 +0200
    16.3 @@ -140,7 +140,7 @@
    16.4    apply fastsimp
    16.5    
    16.6    apply (erule disjE)
    16.7 -   apply (clarsimp simp add: Un_subset_iff)  
    16.8 +   apply clarsimp
    16.9     apply (drule method_wf_mdecl, assumption+)
   16.10     apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
   16.11     apply fastsimp
    17.1 --- a/src/HOL/Set.thy	Tue Sep 22 11:26:46 2009 +0200
    17.2 +++ b/src/HOL/Set.thy	Wed Sep 23 08:26:12 2009 +0200
    17.3 @@ -652,8 +652,8 @@
    17.4  
    17.5  subsubsection {* Binary union -- Un *}
    17.6  
    17.7 -definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
    17.8 -  sup_set_eq [symmetric]: "A Un B = sup A B"
    17.9 +abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
   17.10 +  "op Un \<equiv> sup"
   17.11  
   17.12  notation (xsymbols)
   17.13    union  (infixl "\<union>" 65)
   17.14 @@ -663,7 +663,7 @@
   17.15  
   17.16  lemma Un_def:
   17.17    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
   17.18 -  by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
   17.19 +  by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
   17.20  
   17.21  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
   17.22    by (unfold Un_def) blast
   17.23 @@ -689,15 +689,13 @@
   17.24    by (simp add: Collect_def mem_def insert_compr Un_def)
   17.25  
   17.26  lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
   17.27 -  apply (fold sup_set_eq)
   17.28 -  apply (erule mono_sup)
   17.29 -  done
   17.30 +  by (fact mono_sup)
   17.31  
   17.32  
   17.33  subsubsection {* Binary intersection -- Int *}
   17.34  
   17.35 -definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
   17.36 -  inf_set_eq [symmetric]: "A Int B = inf A B"
   17.37 +abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
   17.38 +  "op Int \<equiv> inf"
   17.39  
   17.40  notation (xsymbols)
   17.41    inter  (infixl "\<inter>" 70)
   17.42 @@ -707,7 +705,7 @@
   17.43  
   17.44  lemma Int_def:
   17.45    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
   17.46 -  by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
   17.47 +  by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
   17.48  
   17.49  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   17.50    by (unfold Int_def) blast
   17.51 @@ -725,9 +723,7 @@
   17.52    by simp
   17.53  
   17.54  lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   17.55 -  apply (fold inf_set_eq)
   17.56 -  apply (erule mono_inf)
   17.57 -  done
   17.58 +  by (fact mono_inf)
   17.59  
   17.60  
   17.61  subsubsection {* Set difference *}
    18.1 --- a/src/HOL/Tools/Function/fundef_lib.ML	Tue Sep 22 11:26:46 2009 +0200
    18.2 +++ b/src/HOL/Tools/Function/fundef_lib.ML	Wed Sep 23 08:26:12 2009 +0200
    18.3 @@ -170,7 +170,7 @@
    18.4   end
    18.5  
    18.6  (* instance for unions *)
    18.7 -fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Set.union}
    18.8 +fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
    18.9    (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
   18.10                                       @{thms Un_empty_right} @
   18.11                                       @{thms Un_empty_left})) t
    19.1 --- a/src/HOL/Tools/Function/termination.ML	Tue Sep 22 11:26:46 2009 +0200
    19.2 +++ b/src/HOL/Tools/Function/termination.ML	Wed Sep 23 08:26:12 2009 +0200
    19.3 @@ -145,7 +145,7 @@
    19.4  
    19.5  fun mk_sum_skel rel =
    19.6    let
    19.7 -    val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
    19.8 +    val cs = FundefLib.dest_binop_list @{const_name Lattices.sup} rel
    19.9      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   19.10        let
   19.11          val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
   19.12 @@ -233,7 +233,7 @@
   19.13  fun CALLS tac i st =
   19.14    if Thm.no_prems st then all_tac st
   19.15    else case Thm.term_of (Thm.cprem_of st i) of
   19.16 -    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
   19.17 +    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Lattices.sup} rel, i) st
   19.18    |_ => no_tac st
   19.19  
   19.20  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
   19.21 @@ -293,7 +293,7 @@
   19.22            if null ineqs then
   19.23                Const (@{const_name Set.empty}, fastype_of rel)
   19.24            else
   19.25 -              foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
   19.26 +              foldr1 (HOLogic.mk_binop @{const_name Lattices.sup}) (map mk_compr ineqs)
   19.27  
   19.28        fun solve_membership_tac i =
   19.29            (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
    20.1 --- a/src/HOL/Tools/inductive_set.ML	Tue Sep 22 11:26:46 2009 +0200
    20.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Sep 23 08:26:12 2009 +0200
    20.3 @@ -74,8 +74,8 @@
    20.4          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
    20.5            (p (fold (Logic.all o Var) vs t) f)
    20.6          end;
    20.7 -      fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
    20.8 -        | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
    20.9 +      fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
   20.10 +        | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
   20.11          | mkop _ _ _ = NONE;
   20.12        fun mk_collect p T t =
   20.13          let val U = HOLogic.dest_setT T
    21.1 --- a/src/HOL/UNITY/Follows.thy	Tue Sep 22 11:26:46 2009 +0200
    21.2 +++ b/src/HOL/UNITY/Follows.thy	Wed Sep 23 08:26:12 2009 +0200
    21.3 @@ -1,5 +1,4 @@
    21.4  (*  Title:      HOL/UNITY/Follows
    21.5 -    ID:         $Id$
    21.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    21.7      Copyright   1998  University of Cambridge
    21.8  *)
    21.9 @@ -160,7 +159,7 @@
   21.10  lemma Follows_Un: 
   21.11      "[| F \<in> f' Fols f;  F \<in> g' Fols g |]  
   21.12       ==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
   21.13 -apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff, auto)
   21.14 +apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff le_sup_iff, auto)
   21.15  apply (rule LeadsTo_Trans)
   21.16  apply (blast intro: Follows_Un_lemma)
   21.17  (*Weakening is used to exchange Un's arguments*)
    22.1 --- a/src/HOL/UNITY/ProgressSets.thy	Tue Sep 22 11:26:46 2009 +0200
    22.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Wed Sep 23 08:26:12 2009 +0200
    22.3 @@ -1,5 +1,4 @@
    22.4  (*  Title:      HOL/UNITY/ProgressSets
    22.5 -    ID:         $Id$
    22.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.7      Copyright   2003  University of Cambridge
    22.8  
    22.9 @@ -245,7 +244,7 @@
   22.10    then have "cl C (T\<inter>?r) \<subseteq> ?r"
   22.11      by (blast intro!: subset_wens) 
   22.12    then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
   22.13 -    by (simp add: Int_subset_iff cl_ident TC
   22.14 +    by (simp add: cl_ident TC
   22.15                    subset_trans [OF cl_mono [OF Int_lower1]]) 
   22.16    show ?thesis
   22.17      by (rule cl_subset_in_lattice [OF cl_subset latt]) 
   22.18 @@ -486,7 +485,7 @@
   22.19    shows "closed F T B L"
   22.20  apply (simp add: closed_def, clarify)
   22.21  apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])  
   22.22 -apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff 
   22.23 +apply (simp add: Int_Un_distrib cl_Un [OF lattice] 
   22.24                   cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
   22.25  apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") 
   22.26   prefer 2 
    24.1 --- a/src/HOL/UNITY/Transformers.thy	Tue Sep 22 11:26:46 2009 +0200
    24.2 +++ b/src/HOL/UNITY/Transformers.thy	Wed Sep 23 08:26:12 2009 +0200
    24.3 @@ -1,5 +1,4 @@
    24.4  (*  Title:      HOL/UNITY/Transformers
    24.5 -    ID:         $Id$
    24.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    24.7      Copyright   2003  University of Cambridge
    24.8  
    24.9 @@ -133,7 +132,7 @@
   24.10  apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
   24.11  apply (simp add: Un_Int_distrib2 Compl_partition2) 
   24.12  apply (erule constrains_weaken, blast) 
   24.13 -apply (simp add: Un_subset_iff wens_weakening) 
   24.14 +apply (simp add: wens_weakening)
   24.15  done
   24.16  
   24.17  text{*Assertion 4.20 in the thesis.*}
   24.18 @@ -151,7 +150,7 @@
   24.19        "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
   24.20         ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
   24.21  apply (rule equalityI)
   24.22 - apply (simp_all add: Int_lower1 Int_subset_iff) 
   24.23 + apply (simp_all add: Int_lower1) 
   24.24   apply (rule wens_Int_eq_lemma, assumption+) 
   24.25  apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 
   24.26  done
   24.27 @@ -176,7 +175,7 @@
   24.28   apply (drule_tac act1=act and A1=X 
   24.29          in constrains_Un [OF Diff_wens_constrains]) 
   24.30   apply (erule constrains_weaken, blast) 
   24.31 - apply (simp add: Un_subset_iff wens_weakening) 
   24.32 + apply (simp add: wens_weakening) 
   24.33  apply (rule constrains_weaken) 
   24.34  apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+)
   24.35  done
   24.36 @@ -229,7 +228,7 @@
   24.37  apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq> 
   24.38                      wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T") 
   24.39   apply (rule subset_wens) 
   24.40 - apply (simp add: awp_Join_eq awp_Int_eq Int_subset_iff Un_commute)
   24.41 + apply (simp add: awp_Join_eq awp_Int_eq Un_commute)
   24.42   apply (simp add: awp_def wp_def, blast) 
   24.43  apply (insert wens_subset [of F act B], blast) 
   24.44  done
   24.45 @@ -253,7 +252,7 @@
   24.46   apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
   24.47  apply (rule equalityI) 
   24.48   prefer 2 apply blast
   24.49 -apply (simp add: Int_lower1 Int_subset_iff) 
   24.50 +apply (simp add: Int_lower1) 
   24.51  apply (frule wens_set_imp_subset) 
   24.52  apply (subgoal_tac "T-X \<subseteq> awp F T")  
   24.53   prefer 2 apply (blast intro: awpF [THEN subsetD]) 
   24.54 @@ -347,7 +346,7 @@
   24.55        "single_valued act
   24.56         ==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B"
   24.57  apply (rule equalityI)
   24.58 - apply (simp_all add: Un_upper1 Un_subset_iff) 
   24.59 + apply (simp_all add: Un_upper1) 
   24.60  apply (simp add: wens_single_def wp_UN_eq, clarify) 
   24.61  apply (rule_tac a="Suc(i)" in UN_I, auto) 
   24.62  done
    25.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Tue Sep 22 11:26:46 2009 +0200
    25.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Wed Sep 23 08:26:12 2009 +0200
    25.3 @@ -1,13 +1,14 @@
    25.4  (*  Title:      HOL/UNITY/UNITY_Main.thy
    25.5 -    ID:         $Id$
    25.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    25.7      Copyright   2003  University of Cambridge
    25.8  *)
    25.9  
   25.10  header{*Comprehensive UNITY Theory*}
   25.11  
   25.12 -theory UNITY_Main imports Detects PPROD Follows ProgressSets
   25.13 -uses "UNITY_tactics.ML" begin
   25.14 +theory UNITY_Main
   25.15 +imports Detects PPROD Follows ProgressSets
   25.16 +uses "UNITY_tactics.ML"
   25.17 +begin
   25.18  
   25.19  method_setup safety = {*
   25.20      Scan.succeed (fn ctxt =>
    26.1 --- a/src/HOL/UNITY/WFair.thy	Tue Sep 22 11:26:46 2009 +0200
    26.2 +++ b/src/HOL/UNITY/WFair.thy	Wed Sep 23 08:26:12 2009 +0200
    26.3 @@ -113,7 +113,7 @@
    26.4  lemma totalize_transient_iff:
    26.5     "(totalize F \<in> transient A) = (\<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A)"
    26.6  apply (simp add: totalize_def totalize_act_def transient_def 
    26.7 -                 Un_Image Un_subset_iff, safe)
    26.8 +                 Un_Image, safe)
    26.9  apply (blast intro!: rev_bexI)+
   26.10  done
   26.11  
    27.1 --- a/src/HOL/ex/predicate_compile.ML	Tue Sep 22 11:26:46 2009 +0200
    27.2 +++ b/src/HOL/ex/predicate_compile.ML	Wed Sep 23 08:26:12 2009 +0200
    27.3 @@ -2152,7 +2152,7 @@
    27.4      val (ts, _) = Predicate.yieldn k t;
    27.5      val elemsT = HOLogic.mk_set T ts;
    27.6    in if k = ~1 orelse length ts < k then elemsT
    27.7 -    else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
    27.8 +    else Const (@{const_name Lattices.sup}, setT --> setT --> setT) $ elemsT $ t_compr
    27.9    end;
   27.10  
   27.11  fun values_cmd modes k raw_t state =