--- 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:
--- 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
--- 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)"
--- 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
--- 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
--- 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
--- 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