# HG changeset patch
# User haftmann
# Date 1253540115 -7200
# Node ID 6c6b1ba5e71e8a1209cc234977a4389f55ebdbf7
# Parent  90c8af39e21544be8c202b69c7659bc156fedb71
tuned proofs

diff -r 90c8af39e215 -r 6c6b1ba5e71e src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Mon Sep 21 15:35:14 2009 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Sep 21 15:35:15 2009 +0200
@@ -212,7 +212,7 @@
   apply (induct set: finite)
    apply simp
   apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
-    Int_mono2 Un_subset_iff)
+    Int_mono2)
   done
 
 lemma (in LCD) foldD_nest_Un_disjoint:
@@ -274,14 +274,14 @@
   apply (simp add: AC insert_absorb Int_insert_left
     LCD.foldD_insert [OF LCD.intro [of D]]
     LCD.foldD_closed [OF LCD.intro [of D]]
-    Int_mono2 Un_subset_iff)
+    Int_mono2)
   done
 
 lemma (in ACeD) foldD_Un_disjoint:
   "[| finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D |] ==>
     foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
   by (simp add: foldD_Un_Int
-    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
+    left_commute LCD.foldD_closed [OF LCD.intro [of D]])
 
 
 subsubsection {* Products over Finite Sets *}
@@ -377,7 +377,7 @@
   from insert have A: "g \<in> A -> carrier G" by fast
   from insert A a show ?case
     by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
-          Int_mono2 Un_subset_iff) 
+          Int_mono2) 
 qed
 
 lemma finprod_Un_disjoint:
diff -r 90c8af39e215 -r 6c6b1ba5e71e src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Mon Sep 21 15:35:14 2009 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Mon Sep 21 15:35:15 2009 +0200
@@ -1747,7 +1747,7 @@
       have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"
 	by (simp add: need_second_arg_def)
       with s2
-      show ?thesis using False by (simp add: Un_subset_iff)
+      show ?thesis using False by simp
     qed
   next
     case Super thus ?case by simp
diff -r 90c8af39e215 -r 6c6b1ba5e71e src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Mon Sep 21 15:35:14 2009 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Mon Sep 21 15:35:15 2009 +0200
@@ -2953,7 +2953,7 @@
 	  by simp
 	from da_e1 s0_s1 True obtain E1' where
 	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
-	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
+	  by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
 	with conf_s1 wt_e1
 	obtain 
 	  "s2\<Colon>\<preceq>(G, L)"
@@ -2972,7 +2972,7 @@
 	  by simp
 	from da_e2 s0_s1 False obtain E2' where
 	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
-	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
+	  by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
 	with conf_s1 wt_e2
 	obtain 
 	  "s2\<Colon>\<preceq>(G, L)"
diff -r 90c8af39e215 -r 6c6b1ba5e71e src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Mon Sep 21 15:35:14 2009 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Mon Sep 21 15:35:15 2009 +0200
@@ -140,7 +140,7 @@
   apply fastsimp
   
   apply (erule disjE)
-   apply (clarsimp simp add: Un_subset_iff)  
+   apply clarsimp
    apply (drule method_wf_mdecl, assumption+)
    apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
    apply fastsimp
diff -r 90c8af39e215 -r 6c6b1ba5e71e src/HOL/UNITY/ProgressSets.thy
--- a/src/HOL/UNITY/ProgressSets.thy	Mon Sep 21 15:35:14 2009 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy	Mon Sep 21 15:35:15 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/UNITY/ProgressSets
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2003  University of Cambridge
 
@@ -245,7 +244,7 @@
   then have "cl C (T\<inter>?r) \<subseteq> ?r"
     by (blast intro!: subset_wens) 
   then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
-    by (simp add: Int_subset_iff cl_ident TC
+    by (simp add: cl_ident TC
                   subset_trans [OF cl_mono [OF Int_lower1]]) 
   show ?thesis
     by (rule cl_subset_in_lattice [OF cl_subset latt]) 
@@ -486,7 +485,7 @@
   shows "closed F T B L"
 apply (simp add: closed_def, clarify)
 apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])  
-apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff 
+apply (simp add: Int_Un_distrib cl_Un [OF lattice] 
                  cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
 apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") 
  prefer 2 
diff -r 90c8af39e215 -r 6c6b1ba5e71e src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Mon Sep 21 15:35:14 2009 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Mon Sep 21 15:35:15 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/UNITY/Transformers
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2003  University of Cambridge
 
@@ -133,7 +132,7 @@
 apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
 apply (simp add: Un_Int_distrib2 Compl_partition2) 
 apply (erule constrains_weaken, blast) 
-apply (simp add: Un_subset_iff wens_weakening) 
+apply (simp add: wens_weakening)
 done
 
 text{*Assertion 4.20 in the thesis.*}
@@ -151,7 +150,7 @@
       "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
        ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
 apply (rule equalityI)
- apply (simp_all add: Int_lower1 Int_subset_iff) 
+ apply (simp_all add: Int_lower1) 
  apply (rule wens_Int_eq_lemma, assumption+) 
 apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 
 done
@@ -176,7 +175,7 @@
  apply (drule_tac act1=act and A1=X 
         in constrains_Un [OF Diff_wens_constrains]) 
  apply (erule constrains_weaken, blast) 
- apply (simp add: Un_subset_iff wens_weakening) 
+ apply (simp add: wens_weakening) 
 apply (rule constrains_weaken) 
 apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+)
 done
@@ -229,7 +228,7 @@
 apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq> 
                     wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T") 
  apply (rule subset_wens) 
- apply (simp add: awp_Join_eq awp_Int_eq Int_subset_iff Un_commute)
+ apply (simp add: awp_Join_eq awp_Int_eq Un_commute)
  apply (simp add: awp_def wp_def, blast) 
 apply (insert wens_subset [of F act B], blast) 
 done
@@ -253,7 +252,7 @@
  apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
 apply (rule equalityI) 
  prefer 2 apply blast
-apply (simp add: Int_lower1 Int_subset_iff) 
+apply (simp add: Int_lower1) 
 apply (frule wens_set_imp_subset) 
 apply (subgoal_tac "T-X \<subseteq> awp F T")  
  prefer 2 apply (blast intro: awpF [THEN subsetD]) 
@@ -347,7 +346,7 @@
       "single_valued act
        ==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B"
 apply (rule equalityI)
- apply (simp_all add: Un_upper1 Un_subset_iff) 
+ apply (simp_all add: Un_upper1) 
 apply (simp add: wens_single_def wp_UN_eq, clarify) 
 apply (rule_tac a="Suc(i)" in UN_I, auto) 
 done
diff -r 90c8af39e215 -r 6c6b1ba5e71e src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Mon Sep 21 15:35:14 2009 +0200
+++ b/src/HOL/UNITY/WFair.thy	Mon Sep 21 15:35:15 2009 +0200
@@ -113,7 +113,7 @@
 lemma totalize_transient_iff:
    "(totalize F \<in> transient A) = (\<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A)"
 apply (simp add: totalize_def totalize_act_def transient_def 
-                 Un_Image Un_subset_iff, safe)
+                 Un_Image, safe)
 apply (blast intro!: rev_bexI)+
 done