--- a/CONTRIBUTORS Wed Feb 17 21:51:55 2016 +0100
+++ b/CONTRIBUTORS Wed Feb 17 21:51:56 2016 +0100
@@ -6,6 +6,10 @@
Contributions to this Isabelle version
--------------------------------------
+* January 2016: Florian Haftmann
+ Abolition of compound operators INFIMUM and SUPREMUM
+ for complete lattices.
+
Contributions to Isabelle2016
-----------------------------
--- a/NEWS Wed Feb 17 21:51:55 2016 +0100
+++ b/NEWS Wed Feb 17 21:51:56 2016 +0100
@@ -32,6 +32,9 @@
pred_prod_apply ~> pred_prod_inject
INCOMPATIBILITY.
+* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
+INCOMPATIBILITY.
+
New in Isabelle2016 (February 2016)
-----------------------------------
--- a/src/HOL/Algebra/AbelCoset.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Wed Feb 17 21:51:56 2016 +0100
@@ -258,7 +258,7 @@
from a_subgroup have Hcarr: "H \<subseteq> carrier G"
unfolding subgroup_def by simp
from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
- using m_comm [simplified] by fast
+ using m_comm [simplified] by fastforce
qed
qed
--- a/src/HOL/Algebra/Coset.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Algebra/Coset.thy Wed Feb 17 21:51:56 2016 +0100
@@ -517,7 +517,7 @@
by (auto simp add: set_mult_def subsetD)
lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
-apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
+apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def)
apply (rule_tac x = x in bexI)
apply (rule bexI [of _ "\<one>"])
apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])
@@ -932,10 +932,22 @@
obtain g where g: "g \<in> carrier G"
and "X = kernel G H h #> g"
by (auto simp add: FactGroup_def RCOSETS_def)
- hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)
+ hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def g intro!: imageI)
thus ?thesis by (auto simp add: g)
qed
+lemma the_elem_image_unique: -- {* FIXME move *}
+ assumes "A \<noteq> {}"
+ assumes *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
+ shows "the_elem (f ` A) = f x"
+unfolding the_elem_def proof (rule the1_equality)
+ from `A \<noteq> {}` obtain y where "y \<in> A" by auto
+ with * have "f x = f y" by simp
+ with `y \<in> A` have "f x \<in> f ` A" by blast
+ with * show "f ` A = {f x}" by auto
+ then show "\<exists>!x. f ` A = {x}" by auto
+qed
+
lemma (in group_hom) FactGroup_hom:
"(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
@@ -952,11 +964,11 @@
and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
by (force simp add: kernel_def r_coset_def image_def)+
hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
- by (auto dest!: FactGroup_nonempty
- simp add: set_mult_def image_eq_UN
+ by (auto dest!: FactGroup_nonempty intro!: image_eqI
+ simp add: set_mult_def
subsetD [OF Xsub] subsetD [OF X'sub])
- thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
- by (simp add: all image_eq_UN FactGroup_nonempty X X')
+ then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
+ by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
qed
@@ -964,7 +976,7 @@
lemma (in group_hom) FactGroup_subset:
"\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
\<Longrightarrow> kernel G H h #> g \<subseteq> kernel G H h #> g'"
-apply (clarsimp simp add: kernel_def r_coset_def image_def)
+apply (clarsimp simp add: kernel_def r_coset_def)
apply (rename_tac y)
apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
apply (simp add: G.m_assoc)
@@ -985,7 +997,7 @@
by (force simp add: kernel_def r_coset_def image_def)+
assume "the_elem (h ` X) = the_elem (h ` X')"
hence h: "h g = h g'"
- by (simp add: image_eq_UN all FactGroup_nonempty X X')
+ by (simp add: all FactGroup_nonempty X X' the_elem_image_unique)
show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
qed
@@ -1006,7 +1018,10 @@
hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}"
by (auto simp add: y kernel_def r_coset_def)
with g show "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
- by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
+ apply (auto intro!: bexI image_eqI simp add: FactGroup_def RCOSETS_def)
+ apply (subst the_elem_image_unique)
+ apply auto
+ done
qed
qed
@@ -1019,5 +1034,4 @@
by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
FactGroup_onto)
-
end
--- a/src/HOL/Auth/Guard/Proto.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy Wed Feb 17 21:51:56 2016 +0100
@@ -56,7 +56,7 @@
Nonce n ~:parts (apm s `(msg `(fst R))) |] ==>
(EX k. Nonce k:parts {X} & nonce s k = n)"
apply (erule Nonce_apm, unfold wdef_def)
-apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp simp: image_eq_UN)
+apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp)
apply (drule_tac x=x in bspec, simp)
apply (drule_tac Y="msg x" and s=s in apm_parts, simp)
by (blast dest: parts_parts)
@@ -134,7 +134,7 @@
lemma ok_not_used: "[| Nonce n ~:used evs; ok evs R s;
ALL x. x:fst R --> is_Says x |] ==> Nonce n ~:parts (apm s `(msg `(fst R)))"
-apply (unfold ok_def, clarsimp simp: image_eq_UN)
+apply (unfold ok_def, clarsimp)
apply (drule_tac x=x in spec, drule_tac x=x in spec)
by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts)
@@ -188,10 +188,10 @@
apply (drule wdef_Nonce, simp+)
apply (frule ok_not_used, simp+)
apply (clarify, erule ok_is_Says, simp+)
-apply (clarify, rule_tac x=k in exI, simp add: newn_def image_eq_UN)
+apply (clarify, rule_tac x=k in exI, simp add: newn_def)
apply (clarify, drule_tac Y="msg x" and s=s in apm_parts)
apply (drule ok_not_used, simp+)
-by (clarify, erule ok_is_Says, simp_all add: image_eq_UN)
+by (clarify, erule ok_is_Says, simp_all)
lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs;
Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev"
--- a/src/HOL/Auth/Message.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Auth/Message.thy Wed Feb 17 21:51:56 2016 +0100
@@ -207,8 +207,16 @@
apply (erule parts.induct, blast+)
done
-lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
-by (intro equalityI parts_UN_subset1 parts_UN_subset2)
+lemma parts_UN [simp]:
+ "parts (\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts (H x))"
+ by (intro equalityI parts_UN_subset1 parts_UN_subset2)
+
+lemma parts_image [simp]:
+ "parts (f ` A) = (\<Union>x\<in>A. parts {f x})"
+ apply auto
+ apply (metis (mono_tags, hide_lams) image_iff parts_singleton)
+ apply (metis empty_subsetI image_eqI insert_absorb insert_subset parts_mono)
+ done
text\<open>Added to simplify arguments to parts, analz and synth.
NOTE: the UN versions are no longer used!\<close>
@@ -299,10 +307,7 @@
done
lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
-apply auto
-apply (erule parts.induct, auto)
-done
-
+by auto
text\<open>In any message, there is an upper bound N on its greatest nonce.\<close>
lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
--- a/src/HOL/Auth/Recur.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Auth/Recur.thy Wed Feb 17 21:51:56 2016 +0100
@@ -337,7 +337,7 @@
RB \<in> responses evs |]
==> (Key K \<in> parts{RB} | Key K \<in> analz H)"
apply (erule rev_mp, erule responses.induct)
-apply (simp_all del: image_insert
+apply (simp_all del: image_insert parts_image
add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
txt\<open>Simplification using two distinct treatments of "image"\<close>
apply (simp add: parts_insert2, blast)
@@ -389,7 +389,7 @@
apply (erule respond.induct)
apply (frule_tac [2] respond_imp_responses)
apply (frule_tac [2] respond_imp_not_used)
-apply (simp_all del: image_insert
+apply (simp_all del: image_insert parts_image
add: analz_image_freshK_simps split_ifs shrK_in_analz_respond
resp_analz_image_freshK parts_insert2)
txt\<open>Base case of respond\<close>
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Wed Feb 17 21:51:56 2016 +0100
@@ -809,9 +809,9 @@
(*Because initState contains a set of nonces, this is needed for base case of
analz_image_freshK*)
-lemma analz_image_Key_Un_Nonce: "analz (Key`K \<union> Nonce`N) = Key`K \<union> Nonce`N"
-apply auto
-done
+lemma analz_image_Key_Un_Nonce:
+ "analz (Key ` K \<union> Nonce ` N) = Key ` K \<union> Nonce ` N"
+ by (auto simp del: parts_image)
method_setup sc_analz_freshK = \<open>
Scan.succeed (fn ctxt =>
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Wed Feb 17 21:51:56 2016 +0100
@@ -819,9 +819,9 @@
(*Because initState contains a set of nonces, this is needed for base case of
analz_image_freshK*)
-lemma analz_image_Key_Un_Nonce: "analz (Key`K \<union> Nonce`N) = Key`K \<union> Nonce`N"
-apply auto
-done
+lemma analz_image_Key_Un_Nonce:
+ "analz (Key ` K \<union> Nonce ` N) = Key ` K \<union> Nonce ` N"
+ by (auto simp del: parts_image)
method_setup sc_analz_freshK = \<open>
Scan.succeed (fn ctxt =>
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Wed Feb 17 21:51:56 2016 +0100
@@ -115,10 +115,7 @@
text\<open>Added to extend initstate with set of nonces\<close>
lemma parts_image_Nonce [simp]: "parts (Nonce`N) = Nonce`N"
-apply auto
-apply (erule parts.induct)
-apply auto
-done
+ by auto
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
apply (unfold keysFor_def)
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Wed Feb 17 21:51:56 2016 +0100
@@ -711,7 +711,7 @@
lemma card_of_UNION_Sigma:
"|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
-using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by blast
+using Ex_inj_on_UNION_Sigma [of A I] card_of_ordLeq by blast
lemma card_of_bool:
assumes "a1 \<noteq> a2"
--- a/src/HOL/Cardinals/Wellorder_Relation.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy Wed Feb 17 21:51:56 2016 +0100
@@ -450,8 +450,7 @@
lemma ofilter_under_Union:
"ofilter A \<Longrightarrow> A = \<Union>{under a| a. a \<in> A}"
-using ofilter_under_UNION[of A]
-by(unfold Union_eq, auto)
+using ofilter_under_UNION [of A] by auto
subsubsection {* Other properties *}
--- a/src/HOL/Complete_Lattices.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Complete_Lattices.thy Wed Feb 17 21:51:56 2016 +0100
@@ -17,28 +17,25 @@
fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
begin
-definition INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
- INF_def: "INFIMUM A f = \<Sqinter>(f ` A)"
-
-lemma Inf_image_eq [simp]:
- "\<Sqinter>(f ` A) = INFIMUM A f"
- by (simp add: INF_def)
+abbreviation INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
+where
+ "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
lemma INF_image [simp]:
"INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
- by (simp only: INF_def image_comp)
+ by (simp add: image_comp)
lemma INF_identity_eq [simp]:
"INFIMUM A (\<lambda>x. x) = \<Sqinter>A"
- by (simp add: INF_def)
+ by simp
lemma INF_id_eq [simp]:
"INFIMUM A id = \<Sqinter>A"
- by (simp add: id_def)
+ by simp
lemma INF_cong:
"A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
- by (simp add: INF_def image_def)
+ by (simp add: image_def)
lemma strong_INF_cong [cong]:
"A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
@@ -50,20 +47,17 @@
fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
begin
-definition SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
- SUP_def: "SUPREMUM A f = \<Squnion>(f ` A)"
-
-lemma Sup_image_eq [simp]:
- "\<Squnion>(f ` A) = SUPREMUM A f"
- by (simp add: SUP_def)
+abbreviation SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
+where
+ "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
lemma SUP_image [simp]:
"SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
- by (simp only: SUP_def image_comp)
+ by (simp add: image_comp)
lemma SUP_identity_eq [simp]:
"SUPREMUM A (\<lambda>x. x) = \<Squnion>A"
- by (simp add: SUP_def)
+ by simp
lemma SUP_id_eq [simp]:
"SUPREMUM A id = \<Squnion>A"
@@ -71,7 +65,7 @@
lemma SUP_cong:
"A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
- by (simp add: SUP_def image_def)
+ by (simp add: image_def)
lemma strong_SUP_cong [cong]:
"A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
@@ -153,14 +147,6 @@
context complete_lattice
begin
-lemma INF_foundation_dual:
- "Sup.SUPREMUM Inf = INFIMUM"
- by (simp add: fun_eq_iff Sup.SUP_def)
-
-lemma SUP_foundation_dual:
- "Inf.INFIMUM Sup = SUPREMUM"
- by (simp add: fun_eq_iff Inf.INF_def)
-
lemma Sup_eqI:
"(\<And>y. y \<in> A \<Longrightarrow> y \<le> x) \<Longrightarrow> (\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> \<Squnion>A = x"
by (blast intro: antisym Sup_least Sup_upper)
@@ -217,19 +203,19 @@
by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFIMUM A f"
- unfolding INF_def Inf_insert by simp
+ by (simp cong del: strong_INF_cong)
lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPREMUM A f"
- unfolding SUP_def Sup_insert by simp
+ by (simp cong del: strong_SUP_cong)
lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
- by (simp add: INF_def)
+ by (simp cong del: strong_INF_cong)
lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
- by (simp add: SUP_def)
+ by (simp cong del: strong_SUP_cong)
lemma Inf_UNIV [simp]:
"\<Sqinter>UNIV = \<bottom>"
@@ -308,18 +294,18 @@
ultimately show ?thesis by (rule Sup_upper2)
qed
+lemma INF_eq:
+ assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
+ assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
+ shows "INFIMUM A f = INFIMUM B g"
+ by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
+
lemma SUP_eq:
assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
- shows "(\<Squnion>i\<in>A. f i) = (\<Squnion>j\<in>B. g j)"
+ shows "SUPREMUM A f = SUPREMUM B g"
by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
-lemma INF_eq:
- assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
- assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
- shows "(\<Sqinter>i\<in>A. f i) = (\<Sqinter>j\<in>B. g j)"
- by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
-
lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
by (auto intro: Inf_greatest Inf_lower)
@@ -498,24 +484,24 @@
lemma sup_INF:
"a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
- by (simp only: INF_def sup_Inf image_image)
+ unfolding sup_Inf by simp
lemma inf_SUP:
"a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
- by (simp only: SUP_def inf_Sup image_image)
+ unfolding inf_Sup by simp
lemma dual_complete_distrib_lattice:
"class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
apply (rule class.complete_distrib_lattice.intro)
apply (fact dual_complete_lattice)
apply (rule class.complete_distrib_lattice_axioms.intro)
- apply (simp_all only: INF_foundation_dual SUP_foundation_dual inf_Sup sup_Inf)
+ apply (simp_all add: inf_Sup sup_Inf)
done
subclass distrib_lattice proof
fix a b c
from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
- then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def)
+ then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by simp
qed
lemma Inf_sup:
@@ -592,7 +578,7 @@
qed
lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
- by (simp only: INF_def SUP_def uminus_Inf image_image)
+ by (simp add: uminus_Inf image_image)
lemma uminus_Sup:
"- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
@@ -602,7 +588,7 @@
qed
lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
- by (simp only: INF_def SUP_def uminus_Sup image_image)
+ by (simp add: uminus_Sup image_image)
end
@@ -731,11 +717,11 @@
lemma INF_bool_eq [simp]:
"INFIMUM = Ball"
- by (simp add: fun_eq_iff INF_def)
+ by (simp add: fun_eq_iff)
lemma SUP_bool_eq [simp]:
"SUPREMUM = Bex"
- by (simp add: fun_eq_iff SUP_def)
+ by (simp add: fun_eq_iff)
instance bool :: complete_boolean_algebra proof
qed (auto intro: bool_induct)
@@ -788,8 +774,7 @@
using Sup_apply [of "f ` A"] by (simp add: comp_def)
instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
-qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf fun_eq_iff image_image
- simp del: Inf_image_eq Sup_image_eq)
+qed (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image)
instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
@@ -903,7 +888,7 @@
instance "set" :: (type) complete_boolean_algebra
proof
-qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def)
+qed (auto simp add: Inf_set_def Sup_set_def image_def)
subsubsection \<open>Inter\<close>
@@ -1011,22 +996,18 @@
"(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
by (auto intro!: INF_eqI)
-lemma Inter_image_eq:
- "\<Inter>(B ` A) = (\<Inter>x\<in>A. B x)"
- by (fact Inf_image_eq)
-
lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
using Inter_iff [of _ "B ` A"] by simp
lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
- by (auto simp add: INF_def image_def)
+ by auto
lemma INT_D [elim, Pure.elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> B a"
by auto
lemma INT_E [elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> (b \<in> B a \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
\<comment> \<open>"Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}.\<close>
- by (auto simp add: INF_def image_def)
+ by auto
lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
by blast
@@ -1198,10 +1179,6 @@
"x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
by (simp add: bind_UNION)
-lemma Union_image_eq:
- "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
- by (fact Sup_image_eq)
-
lemma Union_SetCompr_eq: "\<Union>{f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
by blast
@@ -1214,10 +1191,7 @@
by auto
lemma UN_E [elim!]: "b \<in> (\<Union>x\<in>A. B x) \<Longrightarrow> (\<And>x. x\<in>A \<Longrightarrow> b \<in> B x \<Longrightarrow> R) \<Longrightarrow> R"
- by (auto simp add: SUP_def image_def)
-
-lemma image_eq_UN: "f ` A = (\<Union>x\<in>A. {f x})"
- by blast
+ by auto
lemma UN_upper: "a \<in> A \<Longrightarrow> B a \<subseteq> (\<Union>x\<in>A. B x)"
by (fact SUP_upper)
@@ -1273,7 +1247,7 @@
by blast
lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
- by (auto simp add: split_if_mem2)
+ by safe (auto simp add: split_if_mem2)
lemma UN_bool_eq: "(\<Union>b. A b) = (A True \<union> A False)"
by (fact SUP_UNIV_bool_expand)
@@ -1355,7 +1329,7 @@
lemma inj_on_INTER:
"I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)) \<Longrightarrow> inj_on f (\<Inter>i \<in> I. A i)"
- unfolding inj_on_def by blast
+ unfolding inj_on_def by safe simp
lemma inj_on_UNION_chain:
assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
@@ -1414,20 +1388,19 @@
lemma image_INT:
"[| inj_on f C; ALL x:A. B x <= C; j:A |]
==> f ` (INTER A B) = (INT x:A. f ` B x)"
-apply (simp add: inj_on_def, blast)
-done
+ by (simp add: inj_on_def, auto) blast
-(*Compare with image_INT: no use of inj_on, and if f is surjective then
- it doesn't matter whether A is empty*)
lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)"
-apply (simp add: bij_def)
-apply (simp add: inj_on_def surj_def, blast)
-done
+ apply (simp add: bij_def)
+ apply (simp add: inj_on_def surj_def)
+ apply auto
+ apply blast
+ done
lemma UNION_fun_upd:
- "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
-by (auto split: if_splits)
-
+ "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
+ by (auto simp add: set_eq_iff)
+
subsubsection \<open>Complement\<close>
--- a/src/HOL/Conditionally_Complete_Lattices.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Wed Feb 17 21:51:56 2016 +0100
@@ -321,10 +321,10 @@
by (metis cSUP_upper le_less_trans)
lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFIMUM (insert a A) f = inf (f a) (INFIMUM A f)"
- by (metis cInf_insert Inf_image_eq image_insert image_is_empty)
+ by (metis cInf_insert image_insert image_is_empty)
lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM (insert a A) f = sup (f a) (SUPREMUM A f)"
- by (metis cSup_insert Sup_image_eq image_insert image_is_empty)
+ by (metis cSup_insert image_insert image_is_empty)
lemma cINF_mono: "B \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> INFIMUM A f \<le> INFIMUM B g"
using cInf_mono [of "g ` B" "f ` A"] by auto
--- a/src/HOL/Enum.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Enum.thy Wed Feb 17 21:51:56 2016 +0100
@@ -556,7 +556,7 @@
end
instance finite_1 :: complete_distrib_lattice
-by intro_classes(simp_all add: INF_def SUP_def)
+ by standard simp_all
instance finite_1 :: complete_linorder ..
@@ -679,7 +679,7 @@
end
instance finite_2 :: complete_distrib_lattice
-by(intro_classes)(auto simp add: INF_def SUP_def sup_finite_2_def inf_finite_2_def Inf_finite_2_def Sup_finite_2_def)
+ by standard (auto simp add: sup_finite_2_def inf_finite_2_def Inf_finite_2_def Sup_finite_2_def)
instance finite_2 :: complete_linorder ..
@@ -797,11 +797,11 @@
then have "\<And>x. x \<in> B \<Longrightarrow> x = a\<^sub>3"
by(case_tac x)(auto simp add: Inf_finite_3_def split: split_if_asm)
then show ?thesis using a\<^sub>2_a\<^sub>3
- by(auto simp add: INF_def Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: split_if_asm)
- qed(auto simp add: INF_def Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
+ by(auto simp add: Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: split_if_asm)
+ qed (auto simp add: Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
- by(cases a "\<Squnion>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
- (auto simp add: SUP_def Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
+ by (cases a "\<Squnion>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
+ (auto simp add: Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
qed
instance finite_3 :: complete_linorder ..
@@ -920,10 +920,10 @@
fix a :: finite_4 and B
show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
by(cases a "\<Sqinter>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
- (auto simp add: sup_finite_4_def Inf_finite_4_def INF_def split: finite_4.splits split_if_asm)
+ (auto simp add: sup_finite_4_def Inf_finite_4_def split: finite_4.splits split_if_asm)
show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
by(cases a "\<Squnion>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
- (auto simp add: inf_finite_4_def Sup_finite_4_def SUP_def split: finite_4.splits split_if_asm)
+ (auto simp add: inf_finite_4_def Sup_finite_4_def split: finite_4.splits split_if_asm)
qed
instantiation finite_4 :: complete_boolean_algebra begin
--- a/src/HOL/Filter.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Filter.thy Wed Feb 17 21:51:56 2016 +0100
@@ -437,8 +437,8 @@
qed
lemma eventually_INF: "eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (INF b:X. F b))"
- unfolding INF_def[of B] eventually_Inf[of P "F`B"]
- by (metis Inf_image_eq finite_imageI image_mono finite_subset_image)
+ unfolding eventually_Inf [of P "F`B"]
+ by (metis finite_imageI image_mono finite_subset_image)
lemma Inf_filter_not_bot:
fixes B :: "'a filter set"
@@ -449,7 +449,7 @@
lemma INF_filter_not_bot:
fixes F :: "'i \<Rightarrow> 'a filter"
shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> (INF b:X. F b) \<noteq> bot) \<Longrightarrow> (INF b:B. F b) \<noteq> bot"
- unfolding trivial_limit_def eventually_INF[of _ B]
+ unfolding trivial_limit_def eventually_INF [of _ _ B]
bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
lemma eventually_Inf_base:
@@ -477,7 +477,7 @@
lemma eventually_INF_base:
"B \<noteq> {} \<Longrightarrow> (\<And>a b. a \<in> B \<Longrightarrow> b \<in> B \<Longrightarrow> \<exists>x\<in>B. F x \<le> inf (F a) (F b)) \<Longrightarrow>
eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
- unfolding INF_def by (subst eventually_Inf_base) auto
+ by (subst eventually_Inf_base) auto
subsubsection \<open>Map function for filters\<close>
@@ -573,7 +573,7 @@
by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
- unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
+ unfolding filter_eq_iff eventually_Sup by (auto simp: eventually_principal)
lemma INF_principal_finite: "finite X \<Longrightarrow> (INF x:X. principal (f x)) = principal (\<Inter>x\<in>X. f x)"
by (induct X rule: finite_induct) auto
--- a/src/HOL/GCD.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/GCD.thy Wed Feb 17 21:51:56 2016 +0100
@@ -1990,6 +1990,8 @@
definition
"Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
+interpretation bla: semilattice_neutr_set gcd "0::nat" ..
+
instance ..
end
@@ -2012,19 +2014,7 @@
interpretation gcd_lcm_complete_lattice_nat:
complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
-rewrites "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
- and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
-proof -
- show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
- by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
- then interpret gcd_lcm_complete_lattice_nat:
- complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
- from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
- from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" .
-qed
-
-declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
-declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del]
+ by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
lemma Lcm_empty_nat:
"Lcm {} = (1::nat)"
--- a/src/HOL/Hilbert_Choice.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Hilbert_Choice.thy Wed Feb 17 21:51:56 2016 +0100
@@ -253,10 +253,10 @@
done
lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A"
-by (simp add: image_eq_UN surj_f_inv_f)
+ by (simp add: surj_f_inv_f image_comp comp_def)
lemma image_inv_f_f: "inj f ==> inv f ` (f ` A) = A"
- by (simp add: image_eq_UN)
+ by simp
lemma inv_image_comp: "inj f ==> inv f ` (f ` X) = X"
by (fact image_inv_f_f)
--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Wed Feb 17 21:51:56 2016 +0100
@@ -111,7 +111,8 @@
apply(rule conjI)
apply (blast dest: L3_5i)
apply(simp add: SEM_def sem_def id_def)
-apply (blast dest: Basic_ntran rtrancl_imp_UN_relpow)
+apply (auto dest: Basic_ntran rtrancl_imp_UN_relpow)
+apply blast
done
lemma atom_hoare_sound [rule_format]:
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Feb 17 21:51:56 2016 +0100
@@ -1266,23 +1266,23 @@
apply simp
apply clarify
apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))")
- apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> \<Turnstile> (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption)
+ apply(erule_tac x=xa and P="\<lambda>i. H i \<longrightarrow> \<Turnstile> (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption)
apply(simp add:com_validity_def)
apply(erule_tac x=s in allE)
- apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (I j) \<in> cp (J j) s" for H I J in allE,simp)
- apply(drule_tac c="clist!i" in subsetD)
+ apply(erule_tac x=xa and P="\<lambda>j. H j \<longrightarrow> (I j) \<in> cp (J j) s" for H I J in allE,simp)
+ apply(drule_tac c="clist!xa" in subsetD)
apply (force simp add:Com_def)
apply(simp add:comm_def conjoin_def same_program_def del:last.simps)
apply clarify
apply(erule_tac x="length x - 1" and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in allE)
apply (simp add:All_None_def same_length_def)
- apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> length(J j)=(K j)" for H J K in allE)
+ apply(erule_tac x=xa and P="\<lambda>j. H j \<longrightarrow> length(J j)=(K j)" for H J K in allE)
apply(subgoal_tac "length x - 1 < length x",simp)
apply(case_tac "x\<noteq>[]")
apply(simp add: last_conv_nth)
- apply(erule_tac x="clist!i" in ballE)
+ apply(erule_tac x="clist!xa" in ballE)
apply(simp add:same_state_def)
- apply(subgoal_tac "clist!i\<noteq>[]")
+ apply(subgoal_tac "clist!xa\<noteq>[]")
apply(simp add: last_conv_nth)
apply(case_tac x)
apply (force simp add:par_cp_def)
@@ -1297,19 +1297,19 @@
apply(rule conjI)
apply(simp add:conjoin_def same_state_def par_cp_def)
apply clarify
- apply(erule_tac x=ia and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
+ apply(erule_tac x=i and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
apply(case_tac x,simp+)
apply (simp add:par_assum_def)
apply clarify
- apply(drule_tac c="snd (clist ! ia ! 0)" in subsetD)
+ apply(drule_tac c="snd (clist ! i ! 0)" in subsetD)
apply assumption
apply simp
apply clarify
-apply(erule_tac x=ia in all_dupE)
+apply(erule_tac x=i in all_dupE)
apply(rule subsetD, erule mp, assumption)
apply(erule_tac pre=pre and rely=rely and x=x and s=s in three)
- apply(erule_tac x=ic in allE,erule mp)
+ apply(erule_tac x=ib in allE,erule mp)
apply simp_all
apply(simp add:ParallelCom_def)
apply(force simp add:Com_def)
--- a/src/HOL/IMP/Denotational.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/IMP/Denotational.thy Wed Feb 17 21:51:56 2016 +0100
@@ -98,6 +98,9 @@
theorem lfp_if_cont:
assumes "cont f" shows "lfp f = (UN n. (f^^n) {})" (is "_ = ?U")
proof
+ from assms mono_if_cont
+ have mono: "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" for n
+ using funpow_decreasing [of n "Suc n"] by auto
show "lfp f \<subseteq> ?U"
proof (rule lfp_lowerbound)
have "f ?U = (UN n. (f^^Suc n){})"
@@ -105,7 +108,7 @@
by(simp add: cont_def)
also have "\<dots> = (f^^0){} \<union> \<dots>" by simp
also have "\<dots> = ?U"
- using assms funpow_decreasing le_SucI mono_if_cont by blast
+ using mono by auto (metis funpow_simps_right(2) funpow_swap1 o_apply)
finally show "f ?U \<subseteq> ?U" by simp
qed
next
--- a/src/HOL/Library/Countable_Set_Type.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Wed Feb 17 21:51:56 2016 +0100
@@ -123,7 +123,11 @@
lemma cUnion_transfer [transfer_rule]:
"rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) Union cUnion"
-unfolding cUnion_def[abs_def] Union_conv_UNION[abs_def] by transfer_prover
+proof -
+ have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. UNION A id) (\<lambda>A. cUNION A id)"
+ by transfer_prover
+ then show ?thesis by (simp add: cUnion_def [symmetric])
+qed
lemmas cset_eqI = set_eqI[Transfer.transferred]
lemmas cset_eq_iff[no_atp] = set_eq_iff[Transfer.transferred]
@@ -342,11 +346,9 @@
lemmas cin_mono = in_mono[Transfer.transferred]
lemmas cLeast_mono = Least_mono[Transfer.transferred]
lemmas cequalityI = equalityI[Transfer.transferred]
-lemmas cUnion_cimage_eq [simp] = Union_image_eq[Transfer.transferred]
lemmas cUN_iff [simp] = UN_iff[Transfer.transferred]
lemmas cUN_I [intro] = UN_I[Transfer.transferred]
lemmas cUN_E [elim!] = UN_E[Transfer.transferred]
-lemmas cimage_eq_cUN = image_eq_UN[Transfer.transferred]
lemmas cUN_upper = UN_upper[Transfer.transferred]
lemmas cUN_least = UN_least[Transfer.transferred]
lemmas cUN_cinsert_distrib = UN_insert_distrib[Transfer.transferred]
--- a/src/HOL/Library/Extended_Real.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy Wed Feb 17 21:51:56 2016 +0100
@@ -2002,12 +2002,11 @@
proof cases
assume "(SUP i:I. f i) = - \<infinity>"
moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
- unfolding Sup_eq_MInfty Sup_image_eq[symmetric] by auto
+ unfolding Sup_eq_MInfty by auto
ultimately show ?thesis
by (cases c) (auto simp: \<open>I \<noteq> {}\<close>)
next
assume "(SUP i:I. f i) \<noteq> - \<infinity>" then show ?thesis
- unfolding Sup_image_eq[symmetric]
by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
(auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>)
qed
@@ -2130,7 +2129,6 @@
by simp
next
assume "(SUP i:I. f i) \<noteq> 0" then show ?thesis
- unfolding SUP_def
by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
(auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close>
intro!: ereal_mult_left_mono c)
--- a/src/HOL/Library/FSet.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/FSet.thy Wed Feb 17 21:51:56 2016 +0100
@@ -147,7 +147,7 @@
parametric right_total_Compl_transfer Compl_transfer by simp
instance
- by (standard, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
+ by (standard; transfer) (simp_all add: Diff_eq)
end
--- a/src/HOL/Library/Finite_Lattice.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/Finite_Lattice.thy Wed Feb 17 21:51:56 2016 +0100
@@ -116,12 +116,12 @@
lemma finite_Inf_prod:
"Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
Finite_Set.fold inf top A"
- by (metis Inf_fold_inf finite_code)
+ by (metis Inf_fold_inf finite)
lemma finite_Sup_prod:
"Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
Finite_Set.fold sup bot A"
- by (metis Sup_fold_sup finite_code)
+ by (metis Sup_fold_sup finite)
instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
by standard (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
@@ -130,20 +130,20 @@
already form a finite lattice.\<close>
lemma finite_bot_fun: "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
- by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
+ by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite)
lemma finite_top_fun: "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
- by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
+ by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite)
lemma finite_Inf_fun:
"Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
Finite_Set.fold inf top A"
- by (metis Inf_fold_inf finite_code)
+ by (metis Inf_fold_inf finite)
lemma finite_Sup_fun:
"Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
Finite_Set.fold sup bot A"
- by (metis Sup_fold_sup finite_code)
+ by (metis Sup_fold_sup finite)
instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
by standard (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
@@ -165,11 +165,7 @@
lemma finite_distrib_lattice_complete_inf_Sup:
"inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
- apply (rule finite_induct)
- apply (metis finite_code)
- apply (metis SUP_empty Sup_empty inf_bot_right)
- apply (metis SUP_insert Sup_insert inf_sup_distrib1)
- done
+ using finite [of A] by induct (simp_all add: inf_sup_distrib1)
instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
proof
--- a/src/HOL/Library/Formal_Power_Series.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Feb 17 21:51:56 2016 +0100
@@ -3181,7 +3181,7 @@
let ?KM = "{(k,m). k + m \<le> n}"
let ?f = "\<lambda>s. UNION {(0::nat)..s} (\<lambda>i. {(i,s - i)})"
have th0: "?KM = UNION {0..n} ?f"
- by (auto simp add: set_eq_iff Bex_def)
+ by auto
show "?l = ?r "
unfolding th0
apply (subst setsum.UNION_disjoint)
--- a/src/HOL/Library/Liminf_Limsup.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy Wed Feb 17 21:51:56 2016 +0100
@@ -380,7 +380,7 @@
note * = this
have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))"
- unfolding Liminf_def SUP_def
+ unfolding Liminf_def
by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
@@ -405,7 +405,7 @@
note * = this
have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))"
- unfolding Limsup_def INF_def
+ unfolding Limsup_def
by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
@@ -429,7 +429,7 @@
by auto
qed
have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
- unfolding Limsup_def INF_def
+ unfolding Limsup_def
by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
@@ -455,7 +455,7 @@
note * = this
have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))"
- unfolding Liminf_def SUP_def
+ unfolding Liminf_def
by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
--- a/src/HOL/Library/Lub_Glb.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/Lub_Glb.thy Wed Feb 17 21:51:56 2016 +0100
@@ -230,7 +230,7 @@
by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle)
also have "(SUP i. X i) = u"
using isLub_cSup[of "range X"] u[THEN isLubD1]
- by (intro isLub_unique[OF _ u]) (auto simp add: SUP_def image_def eq_commute)
+ by (intro isLub_unique[OF _ u]) (auto simp add: image_def eq_commute)
finally show ?thesis .
qed
--- a/src/HOL/Library/Option_ord.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/Option_ord.thy Wed Feb 17 21:51:56 2016 +0100
@@ -289,7 +289,7 @@
show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
proof (cases a)
case None
- then show ?thesis by (simp add: INF_def)
+ then show ?thesis by simp
next
case (Some c)
show ?thesis
@@ -303,13 +303,13 @@
from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b\<in>Option.these B. c \<squnion> b)" by simp
then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x\<in>Some ` Option.these B. Some c \<squnion> x)"
by (simp add: Some_INF Some_Inf comp_def)
- with Some B show ?thesis by (simp add: Some_image_these_eq)
+ with Some B show ?thesis by (simp add: Some_image_these_eq cong del: strong_INF_cong)
qed
qed
show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
proof (cases a)
case None
- then show ?thesis by (simp add: SUP_def image_constant_conv bot_option_def)
+ then show ?thesis by (simp add: image_constant_conv bot_option_def cong del: strong_SUP_cong)
next
case (Some c)
show ?thesis
@@ -332,7 +332,7 @@
ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x\<in>Some ` Option.these B. Some c \<sqinter> x)"
by (simp add: Some_SUP Some_Sup comp_def)
with Some show ?thesis
- by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib)
+ by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib cong del: strong_SUP_cong)
qed
qed
qed
--- a/src/HOL/Library/Product_Order.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/Product_Order.thy Wed Feb 17 21:51:56 2016 +0100
@@ -179,7 +179,6 @@
instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
conditionally_complete_lattice
by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
- INF_def SUP_def simp del: Inf_image_eq Sup_image_eq
intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
instance prod :: (complete_lattice, complete_lattice) complete_lattice
@@ -211,10 +210,10 @@
using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def)
lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
- unfolding SUP_def Sup_prod_def by (simp add: comp_def)
+ unfolding Sup_prod_def by (simp add: comp_def)
lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
- unfolding INF_def Inf_prod_def by (simp add: comp_def)
+ unfolding Inf_prod_def by (simp add: comp_def)
text \<open>Alternative formulations for set infima and suprema over the product
@@ -222,11 +221,11 @@
lemma INF_prod_alt_def:
"INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))"
- unfolding INF_def Inf_prod_def by simp
+ unfolding Inf_prod_def by simp
lemma SUP_prod_alt_def:
"SUPREMUM A f = (SUPREMUM A (fst o f), SUPREMUM A (snd o f))"
- unfolding SUP_def Sup_prod_def by simp
+ unfolding Sup_prod_def by simp
subsection \<open>Complete distributive lattices\<close>
--- a/src/HOL/Lifting_Set.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Lifting_Set.thy Wed Feb 17 21:51:56 2016 +0100
@@ -138,7 +138,7 @@
lemma UNION_transfer [transfer_rule]:
"(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
- unfolding Union_image_eq [symmetric, abs_def] by transfer_prover
+ by transfer_prover
lemma Ball_transfer [transfer_rule]:
"(rel_set A ===> (A ===> op =) ===> op =) Ball Ball"
@@ -176,11 +176,11 @@
lemma INF_parametric [transfer_rule]:
"(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) INFIMUM INFIMUM"
- unfolding INF_def [abs_def] by transfer_prover
+ by transfer_prover
lemma SUP_parametric [transfer_rule]:
"(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) SUPREMUM SUPREMUM"
- unfolding SUP_def [abs_def] by transfer_prover
+ by transfer_prover
subsubsection \<open>Rules requiring bi-unique, bi-total or right-total relations\<close>
--- a/src/HOL/List.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/List.thy Wed Feb 17 21:51:56 2016 +0100
@@ -6774,7 +6774,7 @@
lemma set_relcomp [code]:
"set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
- by (auto simp add: Bex_def)
+ by auto (auto simp add: Bex_def image_def)
lemma wf_set [code]:
"wf (set xs) = acyclic (set xs)"
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Wed Feb 17 21:51:56 2016 +0100
@@ -116,7 +116,7 @@
also assume "dist f g = 0"
finally show "f = g"
by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse)
- qed (auto simp: dist_bcontfun_def SUP_def simp del: Sup_image_eq intro!: cSup_eq)
+ qed (auto simp: dist_bcontfun_def intro!: cSup_eq)
show "dist f g \<le> dist f h + dist g h"
proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
fix x
@@ -374,7 +374,7 @@
ultimately
show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
by (simp add: norm_bcontfun_def dist_bcontfun_def norm_conv_dist Abs_bcontfun_inverse
- zero_bcontfun_def const_bcontfun SUP_def del: Sup_image_eq)
+ zero_bcontfun_def const_bcontfun image_image) presburger
qed
qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Feb 17 21:51:56 2016 +0100
@@ -6690,7 +6690,7 @@
using \<open>open s\<close>
apply (simp add: open_contains_ball Ball_def)
apply (erule all_forward)
- using "*" by blast
+ using "*" by auto blast+
have 2: "closedin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
using assms
by (auto intro: continuous_closed_in_preimage_constant holomorphic_on_imp_continuous_on holomorphic_higher_deriv)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Feb 17 21:51:56 2016 +0100
@@ -421,13 +421,13 @@
lemma interval_upperbound[simp]:
"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
interval_upperbound (cbox a b) = (b::'a::euclidean_space)"
- unfolding interval_upperbound_def euclidean_representation_setsum cbox_def SUP_def
+ unfolding interval_upperbound_def euclidean_representation_setsum cbox_def
by (safe intro!: cSup_eq) auto
lemma interval_lowerbound[simp]:
"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
interval_lowerbound (cbox a b) = (a::'a::euclidean_space)"
- unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def INF_def
+ unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def
by (safe intro!: cInf_eq) auto
lemmas interval_bounds = interval_upperbound interval_lowerbound
@@ -436,7 +436,7 @@
fixes X::"real set"
shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X"
and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X"
- by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def)
+ by (auto simp: interval_upperbound_def interval_lowerbound_def)
lemma interval_bounds'[simp]:
assumes "cbox a b \<noteq> {}"
@@ -496,7 +496,7 @@
using assms box_ne_empty(1) content_cbox by blast
lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
- by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def content_def)
+ by (auto simp: interval_upperbound_def interval_lowerbound_def content_def)
lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})"
by (auto simp: content_real)
@@ -856,7 +856,7 @@
by auto
show "\<Union>?A = s1 \<inter> s2"
apply (rule set_eqI)
- unfolding * and Union_image_eq UN_iff
+ unfolding * and UN_iff
using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)]
apply auto
done
@@ -9394,7 +9394,6 @@
prefer 3
apply assumption
apply rule
- apply (rule finite_imageI)
apply (rule r)
apply safe
apply (drule qq)
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Feb 17 21:51:56 2016 +0100
@@ -2752,7 +2752,7 @@
lemma infnorm_Max:
fixes x :: "'a::euclidean_space"
shows "infnorm x = Max ((\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis)"
- by (simp add: infnorm_def infnorm_set_image cSup_eq_Max del: Sup_image_eq)
+ by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)
lemma infnorm_set_lemma:
fixes x :: "'a::euclidean_space"
--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Wed Feb 17 21:51:56 2016 +0100
@@ -38,13 +38,11 @@
assume "X \<noteq> {}"
hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
thus "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
- by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
- simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq
+ by (auto simp: eucl_Inf eucl_Sup eucl_le
intro!: cInf_greatest cSup_least)
qed (force intro!: cInf_lower cSup_upper
simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
- eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
- simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq)+
+ eucl_Inf eucl_Sup eucl_le)+
lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
@@ -89,7 +87,7 @@
shows "Sup s = X"
using assms
unfolding eucl_Sup euclidean_representation_setsum
- by (auto simp: Sup_class.SUP_def simp del: Sup_class.Sup_image_eq intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
+ by (auto intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
lemma Inf_eq_minimum_componentwise:
assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
@@ -98,7 +96,7 @@
shows "Inf s = X"
using assms
unfolding eucl_Inf euclidean_representation_setsum
- by (auto simp: Inf_class.INF_def simp del: Inf_class.Inf_image_eq intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
+ by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
end
@@ -117,10 +115,9 @@
and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
by auto
hence "Inf ?proj = x \<bullet> b"
- by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq)
+ by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
hence "x \<bullet> b = Inf X \<bullet> b"
- by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> setsum.delta
- simp del: Inf_class.Inf_image_eq
+ by (auto simp: eucl_Inf inner_setsum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> setsum.delta
cong: if_cong)
with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast
qed
@@ -140,10 +137,10 @@
and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
by auto
hence "Sup ?proj = x \<bullet> b"
- by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq)
+ by (auto intro!: cSup_eq_maximum)
hence "x \<bullet> b = Sup X \<bullet> b"
- by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> setsum.delta
- simp del: Sup_image_eq cong: if_cong)
+ by (auto simp: eucl_Sup[where 'a='a] inner_setsum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> setsum.delta
+ cong: if_cong)
with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast
qed
@@ -152,7 +149,7 @@
by (auto)
instance real :: ordered_euclidean_space
- by standard (auto simp: INF_def SUP_def)
+ by standard auto
lemma in_Basis_prod_iff:
fixes i::"'a::euclidean_space*'b::euclidean_space"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Feb 17 21:51:56 2016 +0100
@@ -532,7 +532,6 @@
lemma closedin_INT[intro]:
assumes "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> closedin U (B x)"
shows "closedin U (\<Inter>x\<in>A. B x)"
- unfolding Inter_image_eq [symmetric]
apply (rule closedin_Inter)
using assms
apply auto
@@ -605,7 +604,7 @@
ultimately have "?L (\<Union>K)" by blast
}
ultimately show ?thesis
- unfolding subset_eq mem_Collect_eq istopology_def by blast
+ unfolding subset_eq mem_Collect_eq istopology_def by auto
qed
lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)"
@@ -2426,7 +2425,7 @@
fix y
assume "y \<in> {x<..} \<inter> I"
with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
- by (auto intro!: cInf_lower bdd_belowI2 simp del: Inf_image_eq)
+ by (auto intro!: cInf_lower bdd_belowI2)
with a have "a < f y"
by (blast intro: less_le_trans)
}
@@ -3802,7 +3801,7 @@
lemma compact_UN [intro]:
"finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
- unfolding SUP_def by (rule compact_Union) auto
+ by (rule compact_Union) auto
lemma closed_inter_compact [intro]:
assumes "closed s"
@@ -4090,7 +4089,7 @@
by metis
def X \<equiv> "\<lambda>n. X' (from_nat_into A ` {.. n})"
have X: "\<And>n. X n \<in> U - (\<Union>i\<le>n. from_nat_into A i)"
- using \<open>A \<noteq> {}\<close> unfolding X_def SUP_def by (intro T) (auto intro: from_nat_into)
+ using \<open>A \<noteq> {}\<close> unfolding X_def by (intro T) (auto intro: from_nat_into)
then have "range X \<subseteq> U"
by auto
with subseq[of X] obtain r x where "x \<in> U" and r: "subseq r" "(X \<circ> r) \<longlonglongrightarrow> x"
@@ -4198,7 +4197,7 @@
then have s: "\<And>x. x \<in> s \<Longrightarrow> \<exists>U. x\<in>U \<and> open U \<and> finite (U \<inter> t)" by metis
have "s \<subseteq> \<Union>C"
using \<open>t \<subseteq> s\<close>
- unfolding C_def Union_image_eq
+ unfolding C_def
apply (safe dest!: s)
apply (rule_tac a="U \<inter> t" in UN_I)
apply (auto intro!: interiorI simp add: finite_subset)
@@ -4211,7 +4210,7 @@
by (rule countably_compactE)
then obtain E where E: "E \<subseteq> {F. finite F \<and> F \<subseteq> t }" "finite E"
and s: "s \<subseteq> (\<Union>F\<in>E. interior (F \<union> (- t)))"
- by (metis (lifting) Union_image_eq finite_subset_image C_def)
+ by (metis (lifting) finite_subset_image C_def)
from s \<open>t \<subseteq> s\<close> have "t \<subseteq> \<Union>E"
using interior_subset by blast
moreover have "finite (\<Union>E)"
@@ -4348,7 +4347,7 @@
from Rats_dense_in_real[OF \<open>0 < e / 2\<close>] obtain r where "r \<in> \<rat>" "0 < r" "r < e / 2"
by auto
from f[rule_format, of r] \<open>0 < r\<close> \<open>x \<in> s\<close> obtain k where "k \<in> f r" "x \<in> ball k r"
- unfolding Union_image_eq by auto
+ by auto
from \<open>r \<in> \<rat>\<close> \<open>0 < r\<close> \<open>k \<in> f r\<close> have "ball k r \<in> K"
by (auto simp: K_def)
then show "\<exists>b\<in>K. x \<in> b \<and> b \<inter> s \<subseteq> T"
@@ -7412,7 +7411,7 @@
lemma diameter_cbox:
fixes a b::"'a::euclidean_space"
shows "(\<forall>i \<in> Basis. a \<bullet> i \<le> b \<bullet> i) \<Longrightarrow> diameter (cbox a b) = dist a b"
- by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono
+ by (force simp add: diameter_def intro!: cSup_eq_maximum setL2_mono
simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
lemma eucl_less_eq_halfspaces:
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Wed Feb 17 21:51:56 2016 +0100
@@ -259,7 +259,7 @@
(ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
==> finprod G f (\<Union>C) = finprod G (finprod G f) C"
apply (frule finprod_UN_disjoint [of C id f])
- apply (auto simp add: SUP_def)
+ apply auto
done
lemma (in comm_monoid) finprod_one:
--- a/src/HOL/Probability/Caratheodory.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Wed Feb 17 21:51:56 2016 +0100
@@ -396,8 +396,8 @@
from \<open>outer_measure M f X \<noteq> \<infinity>\<close> have fin: "\<bar>outer_measure M f X\<bar> \<noteq> \<infinity>"
using outer_measure_nonneg[OF posf, of X] by auto
show ?thesis
- using Inf_ereal_close[OF fin[unfolded outer_measure_def INF_def], OF \<open>0 < e\<close>]
- unfolding INF_def[symmetric] outer_measure_def[symmetric] by (auto intro: less_imp_le)
+ using Inf_ereal_close [OF fin [unfolded outer_measure_def], OF \<open>0 < e\<close>]
+ by (auto intro: less_imp_le simp add: outer_measure_def)
qed
lemma (in ring_of_sets) countably_subadditive_outer_measure:
@@ -574,7 +574,7 @@
shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
proof -
have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M"
- using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image)
+ using A by (auto simp: disjoint_family_on_disjoint_image)
with \<open>volume M f\<close> have "f (\<Union>(A`I)) = (\<Sum>a\<in>A`I. f a)"
unfolding volume_def by blast
also have "\<dots> = (\<Sum>i\<in>I. f (A i))"
@@ -713,7 +713,7 @@
then have "disjoint_family F"
using F'_disj by (auto simp: disjoint_family_on_def)
moreover from F' have "(\<Union>i. F i) = \<Union>C"
- by (auto simp: F_def set_eq_iff split: split_if_asm)
+ by (auto simp add: F_def split: split_if_asm) blast
moreover have sets_F: "\<And>i. F i \<in> M"
using F' sets_C by (auto simp: F_def)
moreover note sets_C
@@ -783,9 +783,10 @@
by (auto simp: disjoint_family_on_def f_def)
moreover
have Ai_eq: "A i = (\<Union>x<card C. f x)"
- using f C Ai unfolding bij_betw_def by (simp add: Union_image_eq[symmetric])
+ using f C Ai unfolding bij_betw_def by auto
then have "\<Union>range f = A i"
- using f C Ai unfolding bij_betw_def by (auto simp: f_def)
+ using f C Ai unfolding bij_betw_def
+ by (auto simp add: f_def cong del: strong_SUP_cong)
moreover
{ have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
@@ -841,7 +842,7 @@
have "(\<Sum>n. \<mu>_r (A' n)) = (\<Sum>n. \<Sum>c\<in>C'. \<mu>_r (A' n \<inter> c))"
using C' A'
by (subst volume_finite_additive[symmetric, OF V(1)])
- (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq
+ (auto simp: disjoint_def disjoint_family_on_def
intro!: G.Int G.finite_Union arg_cong[where f="\<lambda>X. suminf (\<lambda>i. \<mu>_r (X i))"] ext
intro: generated_ringI_Basic)
also have "\<dots> = (\<Sum>c\<in>C'. \<Sum>n. \<mu>_r (A' n \<inter> c))"
@@ -853,7 +854,7 @@
also have "\<dots> = \<mu>_r (\<Union>C')"
using C' Un_A
by (subst volume_finite_additive[symmetric, OF V(1)])
- (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq
+ (auto simp: disjoint_family_on_def disjoint_def
intro: generated_ringI_Basic)
finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)"
using C' by simp
--- a/src/HOL/Probability/Complete_Measure.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy Wed Feb 17 21:51:56 2016 +0100
@@ -205,7 +205,7 @@
unfolding binary_def by (auto split: split_if_asm)
show "emeasure M (main_part M (S \<union> T)) = emeasure M (main_part M S \<union> main_part M T)"
using emeasure_main_part_UN[of "binary S T" M] assms
- unfolding range_binary_eq Un_range_binary UN by auto
+ by (simp add: range_binary_eq, simp add: Un_range_binary UN)
qed (auto intro: S T)
lemma sets_completionI_sub:
--- a/src/HOL/Probability/Embed_Measure.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Embed_Measure.thy Wed Feb 17 21:51:56 2016 +0100
@@ -36,7 +36,8 @@
then obtain A' where "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M"
by (auto simp: subset_eq choice_iff)
moreover from this have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast
- ultimately show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}" by blast
+ ultimately show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}"
+ by simp blast
qed (auto dest: sets.sets_into_space)
lemma the_inv_into_vimage:
--- a/src/HOL/Probability/Fin_Map.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Wed Feb 17 21:51:56 2016 +0100
@@ -696,7 +696,7 @@
have "A -` y \<inter> space (PiF I M) = (\<Union>J\<in>I. A -` y \<inter> space (PiF {J} M))"
by (auto simp: space_PiF)
also have "\<dots> \<in> sets (PiF I M)"
- proof
+ proof (rule sets.finite_UN)
show "finite I" by fact
fix J assume "J \<in> I"
with assms have "finite J" by simp
@@ -1055,8 +1055,8 @@
by (intro Pi'_cong) (simp_all add: S_union)
also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>' j\<in>I. if i = j then A else S j (xs ! T j))"
using T
- apply auto
- apply (simp_all add: Pi'_iff bchoice_iff)
+ apply (auto simp del: Union_iff)
+ apply (simp_all add: Pi'_iff bchoice_iff del: Union_iff)
apply (erule conjE exE)+
apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
apply (auto simp: bij_betw_def)
--- a/src/HOL/Probability/Independent_Family.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Independent_Family.thy Wed Feb 17 21:51:56 2016 +0100
@@ -491,11 +491,18 @@
where a: "a = (\<Inter>k\<in>Ka. Ea k)" "finite Ka" "Ka \<noteq> {}" "Ka \<subseteq> I j" "\<And>k. k\<in>Ka \<Longrightarrow> Ea k \<in> E k" by auto
fix b assume "b \<in> ?E j" then obtain Kb Eb
where b: "b = (\<Inter>k\<in>Kb. Eb k)" "finite Kb" "Kb \<noteq> {}" "Kb \<subseteq> I j" "\<And>k. k\<in>Kb \<Longrightarrow> Eb k \<in> E k" by auto
- let ?A = "\<lambda>k. (if k \<in> Ka \<inter> Kb then Ea k \<inter> Eb k else if k \<in> Kb then Eb k else if k \<in> Ka then Ea k else {})"
- have "a \<inter> b = INTER (Ka \<union> Kb) ?A"
- by (simp add: a b set_eq_iff) auto
+ let ?f = "\<lambda>k. (if k \<in> Ka \<inter> Kb then Ea k \<inter> Eb k else if k \<in> Kb then Eb k else if k \<in> Ka then Ea k else {})"
+ have "Ka \<union> Kb = (Ka \<inter> Kb) \<union> (Kb - Ka) \<union> (Ka - Kb)"
+ by blast
+ moreover have "(\<Inter>x\<in>Ka \<inter> Kb. Ea x \<inter> Eb x) \<inter>
+ (\<Inter>x\<in>Kb - Ka. Eb x) \<inter> (\<Inter>x\<in>Ka - Kb. Ea x) = (\<Inter>k\<in>Ka. Ea k) \<inter> (\<Inter>k\<in>Kb. Eb k)"
+ by auto
+ ultimately have "(\<Inter>k\<in>Ka \<union> Kb. ?f k) = (\<Inter>k\<in>Ka. Ea k) \<inter> (\<Inter>k\<in>Kb. Eb k)" (is "?lhs = ?rhs")
+ by (simp only: image_Un Inter_Un_distrib) simp
+ then have "a \<inter> b = (\<Inter>k\<in>Ka \<union> Kb. ?f k)"
+ by (simp only: a(1) b(1))
with a b \<open>j \<in> J\<close> Int_stableD[OF Int_stable] show "a \<inter> b \<in> ?E j"
- by (intro CollectI exI[of _ "Ka \<union> Kb"] exI[of _ ?A]) auto
+ by (intro CollectI exI[of _ "Ka \<union> Kb"] exI[of _ ?f]) auto
qed
qed
ultimately show ?thesis
@@ -804,14 +811,18 @@
proof -
have [measurable]: "\<And>m. {x\<in>space M. P m x} \<in> sets M"
using assms by (auto simp: indep_events_def)
- have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1"
- by (rule borel_0_1_law) fact
+ have *: "(\<Inter>n. \<Union>m\<in>{n..}. {x \<in> space M. P m x}) \<in> events"
+ by simp
+ from assms have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1"
+ by (rule borel_0_1_law)
+ also have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1 \<longleftrightarrow> (AE x in M. infinite {m. P m x})"
+ using * by (simp add: prob_eq_1)
+ (simp add: Bex_def infinite_nat_iff_unbounded_le)
also have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 0 \<longleftrightarrow> (AE x in M. finite {m. P m x})"
- by (subst prob_eq_0) (auto simp add: finite_nat_iff_bounded Ball_def not_less[symmetric])
- also have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1 \<longleftrightarrow> (AE x in M. infinite {m. P m x})"
- by (subst prob_eq_1) (simp_all add: Bex_def infinite_nat_iff_unbounded_le)
+ using * by (simp add: prob_eq_0)
+ (auto simp add: Ball_def finite_nat_iff_bounded not_less [symmetric])
finally show ?thesis
- by metis
+ by blast
qed
lemma (in prob_space) indep_sets_finite:
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Feb 17 21:51:56 2016 +0100
@@ -181,7 +181,7 @@
proof -
have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^sub>E j\<in>{..i}. E j))"
using E E[THEN sets.sets_into_space]
- by (auto simp: prod_emb_def Pi_iff extensional_def) blast
+ by (auto simp: prod_emb_def Pi_iff extensional_def)
with E show ?thesis by auto
qed
@@ -194,7 +194,7 @@
using E by (simp add: measure_PiM_emb)
moreover have "Pi UNIV E = (\<Inter>n. ?E n)"
using E E[THEN sets.sets_into_space]
- by (auto simp: prod_emb_def extensional_def Pi_iff) blast
+ by (auto simp: prod_emb_def extensional_def Pi_iff)
moreover have "range ?E \<subseteq> sets S"
using E by auto
moreover have "decseq ?E"
--- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Feb 17 21:51:56 2016 +0100
@@ -536,7 +536,7 @@
moreover have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0"
by (rule emeasure_UN_eq_0) auto
ultimately have "emeasure lborel A \<le> 0" using emeasure_mono
- by (metis assms bot.extremum_unique emeasure_empty image_eq_UN range_from_nat_into sets.empty_sets)
+ by (smt UN_E emeasure_empty equalityI from_nat_into order_refl singletonD subsetI)
thus ?thesis by (auto simp add: emeasure_le_0_iff)
qed
--- a/src/HOL/Probability/Measurable.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Measurable.thy Wed Feb 17 21:51:56 2016 +0100
@@ -152,7 +152,7 @@
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>X. N x i))"
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
- by (auto simp: Bex_def Ball_def)
+ by simp_all (auto simp: Bex_def Ball_def)
lemma pred_intros_finite[measurable (raw)]:
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))"
--- a/src/HOL/Probability/Measure_Space.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Wed Feb 17 21:51:56 2016 +0100
@@ -884,7 +884,7 @@
have "(\<Union>i\<in>I. N i) = \<Union>(N ` range (from_nat_into I))"
using I by simp
also have "\<dots> = (\<Union>i. (N \<circ> from_nat_into I) i)"
- by (simp only: SUP_def image_comp)
+ by simp
finally show ?thesis by simp
qed
@@ -1228,7 +1228,7 @@
range: "range A \<subseteq> sets M" and
space: "(\<Union>i. A i) = space M" and
measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
- using sigma_finite by auto
+ using sigma_finite by blast
show thesis
proof (rule that[of "disjointed A"])
show "range (disjointed A) \<subseteq> sets M"
@@ -1252,7 +1252,7 @@
proof -
obtain F :: "nat \<Rightarrow> 'a set" where
F: "range F \<subseteq> sets M" "(\<Union>i. F i) = space M" "\<And>i. emeasure M (F i) \<noteq> \<infinity>"
- using sigma_finite by auto
+ using sigma_finite by blast
show thesis
proof (rule that[of "\<lambda>n. \<Union>i\<le>n. F i"])
show "range (\<lambda>n. \<Union>i\<le>n. F i) \<subseteq> sets M"
@@ -1731,8 +1731,10 @@
assumes upper: "space M \<subseteq> (\<Union>i \<in> s. f i)"
shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
proof -
- have e: "e = (\<Union>i \<in> s. e \<inter> f i)"
+ have "e \<subseteq> (\<Union>i\<in>s. f i)"
using \<open>e \<in> sets M\<close> sets.sets_into_space upper by blast
+ then have e: "e = (\<Union>i \<in> s. e \<inter> f i)"
+ by auto
hence "measure M e = measure M (\<Union>i \<in> s. e \<inter> f i)" by simp
also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
proof (rule finite_measure_finite_Union)
@@ -2074,7 +2076,7 @@
using E \<Omega> by (subst (1 2) emeasure_restrict_space) (auto simp: sets_eq sets_eq[THEN sets_eq_imp_space_eq])
next
show "range (from_nat_into A) \<subseteq> E" "(\<Union>i. from_nat_into A i) = \<Omega>"
- unfolding Sup_image_eq[symmetric, where f="from_nat_into A"] using A by auto
+ using A by (auto cong del: strong_SUP_cong)
next
fix i
have "emeasure (restrict_space M \<Omega>) (from_nat_into A i) = emeasure M (from_nat_into A i)"
@@ -2333,12 +2335,12 @@
assumes A: "Complete_Partial_Order.chain op \<le> (f ` A)" and a: "a \<in> A" "f a \<noteq> bot"
shows space_SUP: "space (SUP M:A. f M) = space (f a)"
and sets_SUP: "sets (SUP M:A. f M) = sets (f a)"
-unfolding SUP_def by(rule space_Sup[OF A a(2) imageI[OF a(1)]] sets_Sup[OF A a(2) imageI[OF a(1)]])+
+by(rule space_Sup[OF A a(2) imageI[OF a(1)]] sets_Sup[OF A a(2) imageI[OF a(1)]])+
lemma emeasure_SUP:
assumes A: "Complete_Partial_Order.chain op \<le> (f ` A)" "A \<noteq> {}"
assumes "X \<in> sets (SUP M:A. f M)"
shows "emeasure (SUP M:A. f M) X = (SUP M:A. emeasure (f M)) X"
-using \<open>X \<in> _\<close> unfolding SUP_def by(subst emeasure_Sup[OF A(1)]; simp add: A)
+using \<open>X \<in> _\<close> by(subst emeasure_Sup[OF A(1)]; simp add: A)
end
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Feb 17 21:51:56 2016 +0100
@@ -932,7 +932,7 @@
have "a * u x < 1 * u x"
by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)
also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def)
- finally obtain i where "a * u x < f i x" unfolding SUP_def
+ finally obtain i where "a * u x < f i x"
by (auto simp add: less_SUP_iff)
hence "a * u x \<le> f i x" by auto
thus ?thesis using \<open>x \<in> space M\<close> by auto
@@ -2042,7 +2042,7 @@
by (auto intro!: SUP_least SUP_upper nn_integral_mono)
next
have "\<And>x. \<exists>g. incseq g \<and> range g \<subseteq> (\<lambda>i. f i x) ` Y \<and> (SUP i:Y. f i x) = (SUP i. g i)"
- unfolding Sup_class.SUP_def by(rule Sup_countable_SUP[unfolded Sup_class.SUP_def])(simp add: nonempty)
+ by (rule Sup_countable_SUP) (simp add: nonempty)
then obtain g where incseq: "\<And>x. incseq (g x)"
and range: "\<And>x. range (g x) \<subseteq> (\<lambda>i. f i x) ` Y"
and sup: "\<And>x. (SUP i:Y. f i x) = (SUP i. g x i)" by moura
@@ -2088,8 +2088,8 @@
assume "x \<in> {..<m}"
hence "x < m" by simp
have "g x n = f (I x) x" by(simp add: I)
- also have "\<dots> \<le> (SUP i:?Y. f i) x" unfolding SUP_def Sup_fun_def image_image
- using \<open>x \<in> {..<m}\<close> by(rule Sup_upper[OF imageI])
+ also have "\<dots> \<le> (SUP i:?Y. f i) x" unfolding Sup_fun_def image_image
+ using \<open>x \<in> {..<m}\<close> by (rule Sup_upper [OF imageI])
also have "\<dots> = f (I m') x" unfolding m' by simp
finally show "g x n \<le> f (I m') x" .
qed
@@ -2264,7 +2264,7 @@
by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm)
qed
then show ?thesis
- unfolding nn_integral_def_finite SUP_def by simp
+ unfolding nn_integral_def_finite by (simp cong del: strong_SUP_cong)
qed
lemma nn_integral_count_space_indicator:
--- a/src/HOL/Probability/Probability_Measure.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Wed Feb 17 21:51:56 2016 +0100
@@ -247,7 +247,7 @@
moreover
{ fix y assume y: "y \<in> I"
with q(2) \<open>open I\<close> have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
- by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open simp del: Sup_image_eq Inf_image_eq) }
+ by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open) }
ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
by simp
also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
--- a/src/HOL/Probability/Radon_Nikodym.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Feb 17 21:51:56 2016 +0100
@@ -51,7 +51,7 @@
space: "(\<Union>i. A i) = space M" and
measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>" and
disjoint: "disjoint_family A"
- using sigma_finite_disjoint by auto
+ using sigma_finite_disjoint by blast
let ?B = "\<lambda>i. 2^Suc i * emeasure M (A i)"
have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
proof
@@ -560,7 +560,7 @@
proof (rule antisym)
show "?a \<le> (SUP i. emeasure M (?O i))" unfolding a_Lim
using Q' by (auto intro!: SUP_mono emeasure_mono)
- show "(SUP i. emeasure M (?O i)) \<le> ?a" unfolding SUP_def
+ show "(SUP i. emeasure M (?O i)) \<le> ?a"
proof (safe intro!: Sup_mono, unfold bex_simps)
fix i
have *: "(\<Union>(Q' ` {..i})) = ?O i" by auto
--- a/src/HOL/Probability/Regularity.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Regularity.thy Wed Feb 17 21:51:56 2016 +0100
@@ -138,7 +138,8 @@
proof safe
fix x from X(2)[OF open_ball[of x r]] \<open>r > 0\<close> obtain d where d: "d\<in>X" "d \<in> ball x r" by auto
show "x \<in> ?U"
- using X(1) d by (auto intro!: exI[where x="to_nat_on X d"] simp: dist_commute Bex_def)
+ using X(1) d
+ by simp (auto intro!: exI [where x = "to_nat_on X d"] simp: dist_commute Bex_def)
qed (simp add: sU)
finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) \<longlonglongrightarrow> M (space M)" .
} note M_space = this
@@ -319,8 +320,8 @@
by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
- by (subst INF_image [of "\<lambda>u. space M - u", symmetric, unfolded comp_def])
- (rule INF_cong, auto simp add: sU intro!: INF_cong)
+ unfolding INF_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]
+ by (rule INF_cong) (auto simp add: sU open_Compl Compl_eq_Diff_UNIV [symmetric, simp])
finally have
"(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
moreover have
@@ -335,8 +336,8 @@
also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
- by (subst SUP_image [of "\<lambda>u. space M - u", symmetric, simplified comp_def])
- (rule SUP_cong, auto simp: sU)
+ unfolding SUP_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]
+ by (rule SUP_cong) (auto simp add: sU)
also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
proof (safe intro!: antisym SUP_least)
fix K assume "closed K" "K \<subseteq> space M - B"
--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Feb 17 21:51:56 2016 +0100
@@ -432,10 +432,10 @@
by (auto simp add: binary_def)
lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
- by (simp add: SUP_def range_binary_eq)
+ by (simp add: range_binary_eq cong del: strong_SUP_cong)
lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
- by (simp add: INF_def range_binary_eq)
+ by (simp add: range_binary_eq cong del: strong_INF_cong)
lemma sigma_algebra_iff2:
"sigma_algebra \<Omega> M \<longleftrightarrow>
@@ -535,11 +535,14 @@
finally show ?thesis .
qed
-lemma sigma_sets_UNION: "countable B \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets X A) \<Longrightarrow> (\<Union>B) \<in> sigma_sets X A"
- using from_nat_into[of B] range_from_nat_into[of B] sigma_sets.Union[of "from_nat_into B" X A]
+lemma sigma_sets_UNION:
+ "countable B \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets X A) \<Longrightarrow> (\<Union>B) \<in> sigma_sets X A"
apply (cases "B = {}")
apply (simp add: sigma_sets.Empty)
- apply (simp del: Union_image_eq add: Union_image_eq[symmetric])
+ using from_nat_into [of B] range_from_nat_into [of B] sigma_sets.Union [of "from_nat_into B" X A]
+ apply simp
+ apply auto
+ apply (metis Sup_bot_conv(1) Union_empty `\<lbrakk>B \<noteq> {}; countable B\<rbrakk> \<Longrightarrow> range (from_nat_into B) = B`)
done
lemma (in sigma_algebra) sigma_sets_eq:
@@ -835,7 +838,7 @@
lemma (in semiring_of_sets) generated_ring_disjoint_UNION:
"finite I \<Longrightarrow> disjoint (A ` I) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> UNION I A \<in> generated_ring"
- unfolding SUP_def by (intro generated_ring_disjoint_Union) auto
+ by (intro generated_ring_disjoint_Union) auto
lemma (in semiring_of_sets) generated_ring_Int:
assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring"
@@ -873,7 +876,7 @@
lemma (in semiring_of_sets) generated_ring_INTER:
"finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> INTER I A \<in> generated_ring"
- unfolding INF_def by (intro generated_ring_Inter) auto
+ by (intro generated_ring_Inter) auto
lemma (in semiring_of_sets) generating_ring:
"ring_of_sets \<Omega> generated_ring"
@@ -898,6 +901,7 @@
fix a b assume "a \<in> Ca" "b \<in> Cb"
with Ca Cb Diff_cover[of a b] show "a - b \<in> ?R"
by (auto simp add: generated_ring_def)
+ (metis DiffI Diff_eq_empty_iff empty_iff)
next
show "disjoint ((\<lambda>a'. \<Inter>b'\<in>Cb. a' - b')`Ca)"
using Ca by (auto simp add: disjoint_def \<open>Cb \<noteq> {}\<close>)
@@ -935,7 +939,7 @@
done
lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
- by (simp add: SUP_def range_binaryset_eq)
+ by (simp add: range_binaryset_eq cong del: strong_SUP_cong)
subsubsection \<open>Closed CDI\<close>
--- a/src/HOL/Relation.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Relation.thy Wed Feb 17 21:51:56 2016 +0100
@@ -1060,10 +1060,11 @@
text\<open>Converse inclusion requires some assumptions\<close>
lemma Image_INT_eq:
- "[|single_valued (r\<inverse>); A\<noteq>{}|] ==> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)"
+ "single_valued (r\<inverse>) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)"
apply (rule equalityI)
apply (rule Image_INT_subset)
-apply (simp add: single_valued_def, blast)
+apply (auto simp add: single_valued_def)
+apply blast
done
lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"
--- a/src/HOL/Set_Interval.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Set_Interval.thy Wed Feb 17 21:51:56 2016 +0100
@@ -1085,26 +1085,33 @@
qed
qed
-lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
+lemma UN_UN_finite_eq:
+ "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
by (auto simp add: atLeast0LessThan)
-lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
+lemma UN_finite_subset:
+ "(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
by (subst UN_UN_finite_eq [symmetric]) blast
lemma UN_finite2_subset:
- "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
- apply (rule UN_finite_subset)
- apply (subst UN_UN_finite_eq [symmetric, of B])
- apply blast
- done
+ assumes "\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n + k}. B i)"
+ shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
+proof (rule UN_finite_subset, rule)
+ fix n and a
+ from assms have "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n + k}. B i)" .
+ moreover assume "a \<in> (\<Union>i\<in>{0..<n}. A i)"
+ ultimately have "a \<in> (\<Union>i\<in>{0..<n + k}. B i)" by blast
+ then show "a \<in> (\<Union>i. B i)" by (auto simp add: UN_UN_finite_eq)
+qed
lemma UN_finite2_eq:
- "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) = (\<Union>n. B n)"
+ "(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n + k}. B i)) \<Longrightarrow>
+ (\<Union>n. A n) = (\<Union>n. B n)"
apply (rule subset_antisym)
apply (rule UN_finite2_subset, blast)
- apply (rule UN_finite2_subset [where k=k])
- apply (force simp add: atLeastLessThan_add_Un [of 0])
- done
+ apply (rule UN_finite2_subset [where k=k])
+ apply (force simp add: atLeastLessThan_add_Un [of 0])
+ done
subsubsection \<open>Cardinality\<close>
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Wed Feb 17 21:51:56 2016 +0100
@@ -251,7 +251,7 @@
val simplified_set_simps =
@{thms collect_def[abs_def] UN_insert UN_empty Un_empty_right Un_empty_left
- o_def Union_Un_distrib Union_image_eq UN_empty2 UN_singleton id_bnf_def};
+ o_def Union_Un_distrib UN_empty2 UN_singleton id_bnf_def};
fun mk_simplified_set_tac ctxt collect_set_map =
unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Wed Feb 17 21:51:56 2016 +0100
@@ -540,8 +540,8 @@
fun mk_ctor_set_tac ctxt set set_map set_maps =
let
val n = length set_maps;
- fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN'
- rtac ctxt @{thm Union_image_eq};
+ fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans)
+ THEN' rtac ctxt @{thm refl};
in
EVERY' [rtac ctxt (set RS @{thm comp_eq_dest} RS trans), rtac ctxt Un_cong,
rtac ctxt (trans OF [set_map, trans_fun_cong_image_id_id_apply]),
--- a/src/HOL/Tools/BNF/bnf_util.ML Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Feb 17 21:51:56 2016 +0100
@@ -257,8 +257,12 @@
Const (@{const_name Bex}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f;
fun mk_UNION X f =
- let val (T, U) = dest_funT (fastype_of f);
- in Const (@{const_name SUPREMUM}, fastype_of X --> (T --> U) --> U) $ X $ f end;
+ let
+ val (T, U) = dest_funT (fastype_of f);
+ in
+ Const (@{const_name Sup}, HOLogic.mk_setT U --> U)
+ $ (Const (@{const_name image}, (T --> U) --> fastype_of X --> HOLogic.mk_setT U) $ f $ X)
+ end;
fun mk_Union T =
Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T);
--- a/src/HOL/Topological_Spaces.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy Wed Feb 17 21:51:56 2016 +0100
@@ -1133,10 +1133,11 @@
using A by auto
show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))"
using A unfolding nhds_def
- apply (intro INF_eq)
+ apply -
+ apply (rule INF_eq)
apply simp_all
- apply force
- apply (intro exI[of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
+ apply fastforce
+ apply (intro exI [of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
apply auto
done
qed
@@ -1464,7 +1465,7 @@
lemma continuous_on_open_UN:
"(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
- unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
+ by (rule continuous_on_open_Union) auto
lemma continuous_on_open_Un:
"open s \<Longrightarrow> open t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
@@ -1689,7 +1690,7 @@
lemma compactE_image:
assumes "compact s" and "\<forall>t\<in>C. open (f t)" and "s \<subseteq> (\<Union>c\<in>C. f c)"
obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> (\<Union>c\<in>C'. f c)"
- using assms unfolding ball_simps[symmetric] SUP_def
+ using assms unfolding ball_simps [symmetric]
by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
lemma compact_inter_closed [intro]:
--- a/src/HOL/Transitive_Closure.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Transitive_Closure.thy Wed Feb 17 21:51:56 2016 +0100
@@ -946,7 +946,7 @@
apply (rule iffI)
apply (drule tranclD2)
apply (clarsimp simp: rtrancl_is_UN_relpow)
- apply (rule_tac x="Suc n" in exI)
+ apply (rule_tac x="Suc x" in exI)
apply (clarsimp simp: relcomp_unfold)
apply fastforce
apply clarsimp
@@ -1093,9 +1093,9 @@
assumes "finite R" and "finite S"
shows "finite(R O S)"
proof-
- have "R O S = (UN (x,y) : R. \<Union>((%(u,v). if u=y then {(x,v)} else {}) ` S))"
- by(force simp add: split_def)
- thus ?thesis using assms by(clarsimp)
+ have "R O S = (\<Union>(x, y)\<in>R. \<Union>(u, v)\<in>S. if u = y then {(x, v)} else {})"
+ by (force simp add: split_def image_constant_conv split: if_splits)
+ then show ?thesis using assms by clarsimp
qed
lemma finite_relpow[simp,intro]:
--- a/src/HOL/UNITY/Comp/Alloc.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Wed Feb 17 21:51:56 2016 +0100
@@ -1035,7 +1035,7 @@
apply (simp only: o_apply sub_def)
apply (insert Alloc_Progress [THEN rename_guarantees_sysOfAlloc_I])
apply (simp add: o_def del: INT_iff)
- apply (erule component_guaranteesD)
+ apply (drule component_guaranteesD)
apply (auto simp add:
System_Increasing_allocRel [simplified sub_apply o_def]
System_Increasing_allocAsk [simplified sub_apply o_def]
@@ -1047,6 +1047,7 @@
lemma System_Progress: "System : system_progress"
apply (unfold system_progress_def)
apply (cut_tac System_Alloc_Progress)
+ apply auto
apply (blast intro: LeadsTo_Trans
System_Follows_allocGiv [THEN Follows_LeadsTo_pfixLe]
System_Follows_ask [THEN Follows_LeadsTo])
--- a/src/HOL/UNITY/ELT.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/UNITY/ELT.thy Wed Feb 17 21:51:56 2016 +0100
@@ -141,7 +141,6 @@
lemma leadsETo_UN:
"(!!i. i : I ==> F : (A i) leadsTo[CC] B)
==> F : (UN i:I. A i) leadsTo[CC] B"
-apply (subst Union_image_eq [symmetric])
apply (blast intro: leadsETo_Union)
done
@@ -397,7 +396,6 @@
lemma LeadsETo_UN:
"(!!i. i : I ==> F : (A i) LeadsTo[CC] B)
==> F : (UN i:I. A i) LeadsTo[CC] B"
-apply (simp only: Union_image_eq [symmetric])
apply (blast intro: LeadsETo_Union)
done
--- a/src/HOL/UNITY/Extend.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/UNITY/Extend.thy Wed Feb 17 21:51:56 2016 +0100
@@ -382,21 +382,25 @@
(project_act h -` AllowedActs F)})"
apply (rule program_equalityI)
apply simp
- apply (simp add: image_eq_UN)
+ apply (simp add: image_image)
apply (simp add: project_def)
done
lemma extend_inverse [simp]:
"project h UNIV (extend h F) = F"
-apply (simp (no_asm_simp) add: project_extend_eq image_eq_UN
+apply (simp (no_asm_simp) add: project_extend_eq
subset_UNIV [THEN subset_trans, THEN Restrict_triv])
apply (rule program_equalityI)
apply (simp_all (no_asm))
apply (subst insert_absorb)
apply (simp (no_asm) add: bexI [of _ Id])
apply auto
+apply (simp add: image_def)
+using project_act_Id apply blast
+apply (simp add: image_def)
apply (rename_tac "act")
-apply (rule_tac x = "extend_act h act" in bexI, auto)
+apply (rule_tac x = "extend_act h act" in exI)
+apply simp
done
lemma inj_extend: "inj (extend h)"
@@ -641,11 +645,12 @@
subsection{*Guarantees*}
lemma project_extend_Join: "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
-apply (rule program_equalityI)
- apply (simp add: project_set_extend_set_Int)
- apply (auto simp add: image_eq_UN)
-done
-
+ apply (rule program_equalityI)
+ apply (auto simp add: project_set_extend_set_Int image_iff)
+ apply (metis Un_iff extend_act_inverse image_iff)
+ apply (metis Un_iff extend_act_inverse image_iff)
+ done
+
lemma extend_Join_eq_extend_D:
"(extend h F)\<squnion>G = extend h H ==> H = F\<squnion>(project h UNIV G)"
apply (drule_tac f = "project h UNIV" in arg_cong)
--- a/src/HOL/UNITY/ProgressSets.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/UNITY/ProgressSets.thy Wed Feb 17 21:51:56 2016 +0100
@@ -42,13 +42,11 @@
lemma UN_in_lattice:
"[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
-apply (unfold SUP_def)
apply (blast intro: Union_in_lattice)
done
lemma INT_in_lattice:
"[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i) \<in> L"
-apply (unfold INF_def)
apply (blast intro: Inter_in_lattice)
done
--- a/src/HOL/UNITY/Rename.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/UNITY/Rename.thy Wed Feb 17 21:51:56 2016 +0100
@@ -272,7 +272,7 @@
(F \<in> (rename (inv h) ` X) guarantees
(rename (inv h) ` Y))"
apply (subst rename_rename_guarantees_eq [symmetric], assumption)
-apply (simp add: image_eq_UN o_def bij_is_surj [THEN surj_f_inv_f])
+apply (simp add: o_def bij_is_surj [THEN surj_f_inv_f] image_comp)
done
lemma rename_preserves:
--- a/src/HOL/UNITY/SubstAx.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Wed Feb 17 21:51:56 2016 +0100
@@ -84,7 +84,6 @@
lemma LeadsTo_UN:
"(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B"
-apply (unfold SUP_def)
apply (blast intro: LeadsTo_Union)
done
@@ -188,7 +187,6 @@
lemma LeadsTo_UN_UN:
"(!! i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i))
==> F \<in> (\<Union>i \<in> I. A i) LeadsTo (\<Union>i \<in> I. A' i)"
-apply (simp only: Union_image_eq [symmetric])
apply (blast intro: LeadsTo_Union LeadsTo_weaken_R)
done
--- a/src/HOL/UNITY/Transformers.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/UNITY/Transformers.thy Wed Feb 17 21:51:56 2016 +0100
@@ -467,7 +467,7 @@
"single_valued act
==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq>
wens_set (mk_program (init, {act}, allowed)) B"
-apply (simp add: SUP_def image_def wens_single_eq_Union)
+apply (simp add: image_def wens_single_eq_Union)
apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
done
--- a/src/HOL/UNITY/Union.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/UNITY/Union.thy Wed Feb 17 21:51:56 2016 +0100
@@ -396,11 +396,30 @@
lemma safety_prop_Int [simp]:
"safety_prop X \<Longrightarrow> safety_prop Y \<Longrightarrow> safety_prop (X \<inter> Y)"
- by (simp add: safety_prop_def) blast
+proof (clarsimp simp add: safety_prop_def)
+ fix G
+ assume "\<forall>G. Acts G \<subseteq> (\<Union>x\<in>X. Acts x) \<longrightarrow> G \<in> X"
+ then have X: "Acts G \<subseteq> (\<Union>x\<in>X. Acts x) \<Longrightarrow> G \<in> X" by blast
+ assume "\<forall>G. Acts G \<subseteq> (\<Union>x\<in>Y. Acts x) \<longrightarrow> G \<in> Y"
+ then have Y: "Acts G \<subseteq> (\<Union>x\<in>Y. Acts x) \<Longrightarrow> G \<in> Y" by blast
+ assume Acts: "Acts G \<subseteq> (\<Union>x\<in>X \<inter> Y. Acts x)"
+ with X and Y show "G \<in> X \<and> G \<in> Y" by auto
+qed
lemma safety_prop_INTER [simp]:
"(\<And>i. i \<in> I \<Longrightarrow> safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i\<in>I. X i)"
- by (simp add: safety_prop_def) blast
+proof (clarsimp simp add: safety_prop_def)
+ fix G and i
+ assume "\<And>i. i \<in> I \<Longrightarrow> \<bottom> \<in> X i \<and>
+ (\<forall>G. Acts G \<subseteq> (\<Union>x\<in>X i. Acts x) \<longrightarrow> G \<in> X i)"
+ then have *: "i \<in> I \<Longrightarrow> Acts G \<subseteq> (\<Union>x\<in>X i. Acts x) \<Longrightarrow> G \<in> X i"
+ by blast
+ assume "i \<in> I"
+ moreover assume "Acts G \<subseteq> (\<Union>j\<in>\<Inter>i\<in>I. X i. Acts j)"
+ ultimately have "Acts G \<subseteq> (\<Union>i\<in>X i. Acts i)"
+ by auto
+ with * `i \<in> I` show "G \<in> X i" by blast
+qed
lemma safety_prop_INTER1 [simp]:
"(\<And>i. safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i. X i)"
--- a/src/HOL/UNITY/WFair.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/UNITY/WFair.thy Wed Feb 17 21:51:56 2016 +0100
@@ -203,7 +203,6 @@
lemma leadsTo_UN:
"(!!i. i \<in> I ==> F \<in> (A i) leadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) leadsTo B"
-apply (subst Union_image_eq [symmetric])
apply (blast intro: leadsTo_Union)
done
@@ -310,7 +309,6 @@
lemma leadsTo_UN_UN:
"(!! i. i \<in> I ==> F \<in> (A i) leadsTo (A' i))
==> F \<in> (\<Union>i \<in> I. A i) leadsTo (\<Union>i \<in> I. A' i)"
-apply (simp only: Union_image_eq [symmetric])
apply (blast intro: leadsTo_Union leadsTo_weaken_R)
done