--- a/NEWS Sat Mar 15 16:54:32 2014 +0100
+++ b/NEWS Sun Mar 16 18:09:04 2014 +0100
@@ -98,6 +98,12 @@
*** HOL ***
+* More aggressive normalization of expressions involving INF and Inf
+or SUP and Sup. INCOMPATIBILITY.
+
+* INF_image and SUP_image do not unfold composition.
+INCOMPATIBILITY.
+
* Swapped orientation of facts image_comp and vimage_comp:
image_compose ~> image_comp [symmetric]
image_comp ~> image_comp [symmetric]
--- a/src/HOL/BNF_Comp.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/BNF_Comp.thy Sun Mar 16 18:09:04 2014 +0100
@@ -25,7 +25,7 @@
fset_bd: "\<And>x. |fset x| \<le>o fbd" and
gset_bd: "\<And>x. |gset x| \<le>o gbd"
shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
-apply (subst sym[OF SUP_def])
+apply simp
apply (rule ordLeq_transitive)
apply (rule card_of_UNION_Sigma)
apply (subst SIGMA_CSUM)
@@ -69,7 +69,7 @@
by blast
lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
-by (unfold comp_apply collect_def SUP_def)
+by (unfold comp_apply collect_def) simp
lemma wpull_cong:
"\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
--- a/src/HOL/Complete_Lattices.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Complete_Lattices.thy Sun Mar 16 18:09:04 2014 +0100
@@ -1,4 +1,4 @@
- (* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
+(* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
header {* Complete lattices *}
@@ -20,10 +20,24 @@
definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
INF_def: "INFI A f = \<Sqinter>(f ` A)"
-lemma INF_image [simp]: "INFI (f`A) g = INFI A (\<lambda>x. g (f x))"
- by (simp add: INF_def image_image)
+lemma Inf_image_eq [simp]:
+ "\<Sqinter>(f ` A) = INFI A f"
+ by (simp add: INF_def)
+
+lemma INF_image [simp]:
+ "INFI (f ` A) g = INFI A (g \<circ> f)"
+ by (simp only: INF_def image_comp)
-lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFI A C = INFI B D"
+lemma INF_identity_eq [simp]:
+ "INFI A (\<lambda>x. x) = \<Sqinter>A"
+ by (simp add: INF_def)
+
+lemma INF_id_eq [simp]:
+ "INFI A id = \<Sqinter>A"
+ by (simp add: id_def)
+
+lemma INF_cong:
+ "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFI A C = INFI B D"
by (simp add: INF_def image_def)
end
@@ -35,10 +49,24 @@
definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
SUP_def: "SUPR A f = \<Squnion>(f ` A)"
-lemma SUP_image [simp]: "SUPR (f`A) g = SUPR A (%x. g (f x))"
- by (simp add: SUP_def image_image)
+lemma Sup_image_eq [simp]:
+ "\<Squnion>(f ` A) = SUPR A f"
+ by (simp add: SUP_def)
+
+lemma SUP_image [simp]:
+ "SUPR (f ` A) g = SUPR A (g \<circ> f)"
+ by (simp only: SUP_def image_comp)
-lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPR A C = SUPR B D"
+lemma SUP_identity_eq [simp]:
+ "SUPR A (\<lambda>x. x) = \<Squnion>A"
+ by (simp add: SUP_def)
+
+lemma SUP_id_eq [simp]:
+ "SUPR A id = \<Squnion>A"
+ by (simp add: id_def)
+
+lemma SUP_cong:
+ "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPR A C = SUPR B D"
by (simp add: SUP_def image_def)
end
@@ -112,10 +140,11 @@
lemma INF_foundation_dual:
"Sup.SUPR Inf = INFI"
- by (simp add: fun_eq_iff INF_def Sup.SUP_def)
+ by (simp add: fun_eq_iff Sup.SUP_def)
lemma SUP_foundation_dual:
- "Inf.INFI Sup = SUPR" by (simp add: fun_eq_iff SUP_def Inf.INF_def)
+ "Inf.INFI Sup = SUPR"
+ 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"
@@ -127,23 +156,23 @@
lemma SUP_eqI:
"(\<And>i. i \<in> A \<Longrightarrow> f i \<le> x) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> (\<Squnion>i\<in>A. f i) = x"
- unfolding SUP_def by (rule Sup_eqI) auto
+ using Sup_eqI [of "f ` A" x] by auto
lemma INF_eqI:
"(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (\<Sqinter>i\<in>A. f i) = x"
- unfolding INF_def by (rule Inf_eqI) auto
+ using Inf_eqI [of "f ` A" x] by auto
lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
- by (auto simp add: INF_def intro: Inf_lower)
+ using Inf_lower [of _ "f ` A"] by simp
lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
- by (auto simp add: INF_def intro: Inf_greatest)
+ using Inf_greatest [of "f ` A"] by auto
lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
- by (auto simp add: SUP_def intro: Sup_upper)
+ using Sup_upper [of _ "f ` A"] by simp
lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
- by (auto simp add: SUP_def intro: Sup_least)
+ using Sup_least [of "f ` A"] by auto
lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
using Inf_lower [of u A] by auto
@@ -161,25 +190,25 @@
by (auto intro: Inf_greatest dest: Inf_lower)
lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
- by (auto simp add: INF_def le_Inf_iff)
+ using le_Inf_iff [of _ "f ` A"] by simp
lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
by (auto intro: Sup_least dest: Sup_upper)
lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
- by (auto simp add: SUP_def Sup_le_iff)
+ using Sup_le_iff [of "f ` A"] by simp
lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
-lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
- by (simp add: INF_def)
+lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
+ unfolding INF_def Inf_insert by simp
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: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
- by (simp add: SUP_def)
+lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
+ unfolding SUP_def Sup_insert by simp
lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
by (simp add: INF_def)
@@ -219,7 +248,7 @@
lemma INF_mono:
"(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<sqsubseteq> (\<Sqinter>n\<in>B. g n)"
- unfolding INF_def by (rule Inf_mono) fast
+ using Inf_mono [of "g ` B" "f ` A"] by auto
lemma Sup_mono:
assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
@@ -233,7 +262,7 @@
lemma SUP_mono:
"(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)"
- unfolding SUP_def by (rule Sup_mono) fast
+ using Sup_mono [of "f ` A" "g ` B"] by auto
lemma INF_superset_mono:
"B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
@@ -267,13 +296,13 @@
lemma SUPR_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 "(SUP i:A. f i) = (SUP j:B. g j)"
+ shows "(\<Squnion>i\<in>A. f i) = (\<Squnion>j\<in>B. g j)"
by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
lemma INFI_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 "(INF i:A. f i) = (INF j:B. g j)"
+ 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)"
@@ -329,9 +358,9 @@
qed
lemma INF_top_conv [simp]:
- "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
- "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
- by (auto simp add: INF_def)
+ "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
+ "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
+ using Inf_top_conv [of "B ` A"] by simp_all
lemma Sup_bot_conv [simp]:
"\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
@@ -342,7 +371,7 @@
lemma SUP_bot_conv [simp]:
"(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
"\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
- by (auto simp add: SUP_def)
+ using Sup_bot_conv [of "B ` A"] by simp_all
lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
by (auto intro: antisym INF_lower INF_greatest)
@@ -367,7 +396,7 @@
shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
proof -
from assms obtain J where "I = insert k J" by blast
- then show ?thesis by (simp add: INF_insert)
+ then show ?thesis by simp
qed
lemma SUP_absorb:
@@ -375,7 +404,7 @@
shows "A k \<squnion> (\<Squnion>i\<in>I. A i) = (\<Squnion>i\<in>I. A i)"
proof -
from assms obtain J where "I = insert k J" by blast
- then show ?thesis by (simp add: SUP_insert)
+ then show ?thesis by simp
qed
lemma INF_constant:
@@ -406,17 +435,17 @@
lemma INF_UNIV_bool_expand:
"(\<Sqinter>b. A b) = A True \<sqinter> A False"
- by (simp add: UNIV_bool INF_insert inf_commute)
+ by (simp add: UNIV_bool inf_commute)
lemma SUP_UNIV_bool_expand:
"(\<Squnion>b. A b) = A True \<squnion> A False"
- by (simp add: UNIV_bool SUP_insert sup_commute)
+ by (simp add: UNIV_bool sup_commute)
lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
by (blast intro: Sup_upper2 Inf_lower ex_in_conv)
lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
- unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
+ using Inf_le_Sup [of "f ` A"] by simp
lemma SUP_eq_const:
"I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPR I f = x"
@@ -443,11 +472,11 @@
lemma sup_INF:
"a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
- by (simp add: INF_def sup_Inf image_image)
+ by (simp only: INF_def sup_Inf image_image)
lemma inf_SUP:
"a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
- by (simp add: SUP_def inf_Sup image_image)
+ by (simp only: SUP_def inf_Sup image_image)
lemma dual_complete_distrib_lattice:
"class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
@@ -529,17 +558,17 @@
qed
lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
- by (simp add: INF_def SUP_def uminus_Inf image_image)
+ by (simp only: INF_def SUP_def uminus_Inf image_image)
lemma uminus_Sup:
"- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
proof -
- have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_Inf)
+ have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_INF)
then show ?thesis by simp
qed
lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
- by (simp add: INF_def SUP_def uminus_Sup image_image)
+ by (simp only: INF_def SUP_def uminus_Sup image_image)
end
@@ -562,7 +591,7 @@
lemma INF_less_iff:
"(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
- unfolding INF_def Inf_less_iff by auto
+ using Inf_less_iff [of "f ` A"] by simp
lemma less_Sup_iff:
"a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
@@ -570,7 +599,7 @@
lemma less_SUP_iff:
"a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
- unfolding SUP_def less_Sup_iff by auto
+ using less_Sup_iff [of _ "f ` A"] by simp
lemma Sup_eq_top_iff [simp]:
"\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
@@ -596,7 +625,7 @@
lemma SUP_eq_top_iff [simp]:
"(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
- unfolding SUP_def by auto
+ using Sup_eq_top_iff [of "f ` A"] by simp
lemma Inf_eq_bot_iff [simp]:
"\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
@@ -605,18 +634,7 @@
lemma INF_eq_bot_iff [simp]:
"(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
- unfolding INF_def by auto
-
-lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
-proof safe
- fix y assume "x \<le> \<Squnion>A" "y < x"
- then have "y < \<Squnion>A" by auto
- then show "\<exists>a\<in>A. y < a"
- unfolding less_Sup_iff .
-qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
-
-lemma le_SUP_iff: "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
- unfolding le_Sup_iff SUP_def by simp
+ using Inf_eq_bot_iff [of "f ` A"] by simp
lemma Inf_le_iff: "\<Sqinter>A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
proof safe
@@ -628,7 +646,18 @@
lemma INF_le_iff:
"INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
- unfolding Inf_le_iff INF_def by simp
+ using Inf_le_iff [of "f ` A"] by simp
+
+lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
+proof safe
+ fix y assume "x \<le> \<Squnion>A" "y < x"
+ then have "y < \<Squnion>A" by auto
+ then show "\<exists>a\<in>A. y < a"
+ unfolding less_Sup_iff .
+qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
+
+lemma le_SUP_iff: "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
+ using le_Sup_iff [of _ "f ` A"] by simp
subclass complete_distrib_lattice
proof
@@ -704,14 +733,15 @@
lemma INF_apply [simp]:
"(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
- by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def)
+ using Inf_apply [of "f ` A"] by (simp add: comp_def)
lemma SUP_apply [simp]:
"(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
- by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def)
+ 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 image_image)
+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)
instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
@@ -888,14 +918,14 @@
lemma INTER_eq:
"(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
- by (auto simp add: INF_def)
+ by (auto intro!: INF_eqI)
-lemma Inter_image_eq [simp]:
- "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
- by (rule sym) (fact INF_def)
+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)"
- by (auto simp add: INF_def image_def)
+ 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)
@@ -1077,7 +1107,7 @@
lemma UNION_eq:
"(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
- by (auto simp add: SUP_def)
+ by (auto intro!: SUP_eqI)
lemma bind_UNION [code]:
"Set.bind A f = UNION A f"
@@ -1087,12 +1117,12 @@
"x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
by (simp add: bind_UNION)
-lemma Union_image_eq [simp]:
+lemma Union_image_eq:
"\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
- by (rule sym) (fact SUP_def)
+ by (fact Sup_image_eq)
lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
- by (auto simp add: SUP_def image_def)
+ using Union_iff [of _ "B ` A"] by simp
lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"
-- {* The order of the premises presupposes that @{term A} is rigid;
@@ -1214,13 +1244,13 @@
lemma UN_Un_distrib: "(\<Union>i\<in>I. A i \<union> B i) = (\<Union>i\<in>I. A i) \<union> (\<Union>i\<in>I. B i)"
by (rule sym) (rule SUP_sup_distrib)
-lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)"
- by (simp only: INT_Int_distrib INF_def)
+lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)" -- {* FIXME drop *}
+ by (simp add: INT_Int_distrib)
-lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)"
+lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)" -- {* FIXME drop *}
-- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}
-- {* Union of a family of unions *}
- by (simp only: UN_Un_distrib SUP_def)
+ by (simp add: UN_Un_distrib)
lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
by (fact sup_INF)
--- a/src/HOL/Conditionally_Complete_Lattices.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Sun Mar 16 18:09:04 2014 +0100
@@ -275,16 +275,16 @@
by (auto intro!: cInf_eq_minimum)
lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFI A f \<le> f x"
- unfolding INF_def by (rule cInf_lower) auto
+ using cInf_lower [of _ "f ` A"] by simp
lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> INFI A f"
- unfolding INF_def by (rule cInf_greatest) auto
+ using cInf_greatest [of "f ` A"] by auto
lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPR A f"
- unfolding SUP_def by (rule cSup_upper) auto
+ using cSup_upper [of _ "f ` A"] by simp
lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> SUPR A f \<le> M"
- unfolding SUP_def by (rule cSup_least) auto
+ using cSup_least [of "f ` A"] by auto
lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFI A f \<le> u"
by (auto intro: cINF_lower assms order_trans)
@@ -311,16 +311,16 @@
by (metis cSUP_upper le_less_trans)
lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)"
- by (metis INF_def cInf_insert assms empty_is_image image_insert)
+ by (metis cInf_insert Inf_image_eq image_insert image_is_empty)
lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR (insert a A) f = sup (f a) (SUPR A f)"
- by (metis SUP_def cSup_insert assms empty_is_image image_insert)
+ by (metis cSup_insert Sup_image_eq 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> INFI A f \<le> INFI B g"
- unfolding INF_def by (auto intro: cInf_mono)
+ using cInf_mono [of "g ` B" "f ` A"] by auto
lemma cSUP_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> SUPR A f \<le> SUPR B g"
- unfolding SUP_def by (auto intro: cSup_mono)
+ using cSup_mono [of "f ` A" "g ` B"] by auto
lemma cINF_superset_mono: "A \<noteq> {} \<Longrightarrow> bdd_below (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> g x \<le> f x) \<Longrightarrow> INFI B g \<le> INFI A f"
by (rule cINF_mono) auto
@@ -338,13 +338,13 @@
by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower)
lemma cINF_union: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below (f`B) \<Longrightarrow> INFI (A \<union> B) f = inf (INFI A f) (INFI B f)"
- unfolding INF_def using assms by (auto simp add: image_Un intro: cInf_union_distrib)
+ using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
lemma cSup_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)"
by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper)
lemma cSUP_union: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above (f`B) \<Longrightarrow> SUPR (A \<union> B) f = sup (SUPR A f) (SUPR B f)"
- unfolding SUP_def by (auto simp add: image_Un intro: cSup_union_distrib)
+ using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> inf (INFI A f) (INFI A g) = (INF a:A. inf (f a) (g a))"
by (intro antisym le_infI cINF_greatest cINF_lower2)
@@ -388,10 +388,10 @@
by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
lemma cINF_less_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
- unfolding INF_def using cInf_less_iff[of "f`A"] by auto
+ using cInf_less_iff[of "f`A"] by auto
lemma less_cSUP_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
- unfolding SUP_def using less_cSup_iff[of "f`A"] by auto
+ using less_cSup_iff[of "f`A"] by auto
lemma less_cSupE:
assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
--- a/src/HOL/Finite_Set.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Finite_Set.thy Sun Mar 16 18:09:04 2014 +0100
@@ -1041,7 +1041,7 @@
interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
from `finite A` show "?fold = ?inf"
by (induct A arbitrary: B)
- (simp_all add: INF_def inf_left_commute)
+ (simp_all add: inf_left_commute)
qed
lemma sup_SUP_fold_sup:
@@ -1052,7 +1052,7 @@
interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
from `finite A` show "?fold = ?sup"
by (induct A arbitrary: B)
- (simp_all add: SUP_def sup_left_commute)
+ (simp_all add: sup_left_commute)
qed
lemma INF_fold_inf:
--- a/src/HOL/GCD.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/GCD.thy Sun Mar 16 18:09:04 2014 +0100
@@ -1581,6 +1581,9 @@
from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR 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]
+
lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
by (fact Lcm_nat_empty)
@@ -1736,11 +1739,11 @@
lemma Lcm_set_int [code, code_unfold]:
"Lcm (set xs) = fold lcm xs (1::int)"
- by (induct xs rule: rev_induct, simp_all add: lcm_commute_int)
+ by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int)
lemma Gcd_set_int [code, code_unfold]:
"Gcd (set xs) = fold gcd xs (0::int)"
- by (induct xs rule: rev_induct, simp_all add: gcd_commute_int)
+ by (induct xs rule: rev_induct) (simp_all add: gcd_commute_int)
end
--- a/src/HOL/Groups_Big.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Groups_Big.thy Sun Mar 16 18:09:04 2014 +0100
@@ -162,8 +162,7 @@
proof cases
assume "finite C"
from UNION_disjoint [OF this assms]
- show ?thesis
- by (simp add: SUP_def)
+ show ?thesis by simp
qed (auto dest: finite_UnionD intro: infinite)
lemma distrib:
@@ -1020,7 +1019,7 @@
(ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
==> card (Union C) = setsum card C"
apply (frule card_UN_disjoint [of C id])
-apply (simp_all add: SUP_def id_def)
+apply simp_all
done
--- a/src/HOL/Library/Extended_Real.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Library/Extended_Real.thy Sun Mar 16 18:09:04 2014 +0100
@@ -1389,16 +1389,26 @@
qed
lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
- by (auto intro!: Sup_eqI
+ by (auto intro!: SUP_eqI
simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
intro!: complete_lattice_class.Inf_lower2)
+lemma ereal_SUP_uminus_eq:
+ fixes f :: "'a \<Rightarrow> ereal"
+ shows "(SUP x:S. uminus (f x)) = - (INF x:S. f x)"
+ using ereal_Sup_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
+
lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
by (auto intro!: inj_onI)
lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S::ereal set) = - Sup S"
using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp
+lemma ereal_INF_uminus_eq:
+ fixes f :: "'a \<Rightarrow> ereal"
+ shows "(INF x:S. uminus (f x)) = - (SUP x:S. f x)"
+ using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
+
lemma ereal_SUP_not_infty:
fixes f :: "_ \<Rightarrow> ereal"
shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>SUPR A f\<bar> \<noteq> \<infinity>"
@@ -1415,7 +1425,7 @@
fixes f :: "'a \<Rightarrow> ereal"
shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
using ereal_Sup_uminus_image_eq[of "f`R"]
- by (simp add: SUP_def INF_def image_image)
+ by (simp add: image_image)
lemma ereal_INFI_uminus:
fixes f :: "'a \<Rightarrow> ereal"
@@ -1763,7 +1773,7 @@
lemma SUPR_countable_SUPR:
"A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
using Sup_countable_SUPR[of "g`A"]
- by (auto simp: SUP_def)
+ by auto
lemma Sup_ereal_cadd:
fixes A :: "ereal set"
@@ -1772,7 +1782,7 @@
shows "Sup ((\<lambda>x. a + x) ` A) = a + Sup A"
proof (rule antisym)
have *: "\<And>a::ereal. \<And>A. Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A"
- by (auto intro!: add_mono complete_lattice_class.Sup_least complete_lattice_class.Sup_upper)
+ by (auto intro!: add_mono complete_lattice_class.SUP_least complete_lattice_class.Sup_upper)
then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
proof (cases a)
@@ -1794,8 +1804,8 @@
assumes "A \<noteq> {}"
and "a \<noteq> -\<infinity>"
shows "Sup ((\<lambda>x. a - x) ` A) = a - Inf A"
- using Sup_ereal_cadd[of "uminus ` A" a] assms
- by (simp add: comp_def image_image minus_ereal_def ereal_Sup_uminus_image_eq)
+ using Sup_ereal_cadd [of "uminus ` A" a] assms
+ unfolding image_image minus_ereal_def by (simp add: ereal_SUP_uminus_eq)
lemma SUPR_ereal_cminus:
fixes f :: "'i \<Rightarrow> ereal"
@@ -1820,8 +1830,8 @@
then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
by (auto simp: image_image)
with * show ?thesis
- using Sup_ereal_cminus[of "uminus ` A" "-a"] assms
- by (auto simp add: ereal_Sup_uminus_image_eq ereal_Inf_uminus_image_eq)
+ using Sup_ereal_cminus [of "uminus ` A" "- a"] assms
+ by (auto simp add: ereal_INF_uminus_eq ereal_SUP_uminus_eq)
qed
lemma INFI_ereal_cminus:
--- a/src/HOL/Library/FSet.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Library/FSet.thy Sun Mar 16 18:09:04 2014 +0100
@@ -143,7 +143,7 @@
lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus
parametric right_total_Compl_transfer Compl_transfer by simp
-instance by (default, simp_all only: INF_def SUP_def) (transfer, auto)+
+instance by (default, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
end
--- a/src/HOL/Library/Option_ord.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Library/Option_ord.thy Sun Mar 16 18:09:04 2014 +0100
@@ -292,11 +292,11 @@
lemma Some_INF:
"Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))"
- by (simp add: INF_def Some_Inf image_image)
+ using Some_Inf [of "f ` A"] by (simp add: comp_def)
lemma Some_SUP:
"A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
- by (simp add: SUP_def Some_Sup image_image)
+ using Some_Sup [of "f ` A"] by (simp add: comp_def)
instantiation option :: (complete_distrib_lattice) complete_distrib_lattice
begin
@@ -319,7 +319,7 @@
case False then have B: "{x \<in> B. \<exists>y. x = Some y} = B" by auto (metis not_Some_eq)
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)
+ by (simp add: Some_INF Some_Inf comp_def)
with Some B show ?thesis by (simp add: Some_image_these_eq)
qed
qed
@@ -332,7 +332,7 @@
show ?thesis
proof (cases "B = {} \<or> B = {None}")
case True
- then show ?thesis by (auto simp add: SUP_def)
+ then show ?thesis by auto
next
have B: "B = {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}"
by auto
@@ -347,7 +347,7 @@
moreover from inf_Sup have "Some c \<sqinter> Some (\<Squnion>Option.these B) = Some (\<Squnion>b\<in>Option.these B. c \<sqinter> b)"
by simp
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)
+ 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)
qed
--- a/src/HOL/Library/Product_Order.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Library/Product_Order.thy Sun Mar 16 18:09:04 2014 +0100
@@ -178,7 +178,7 @@
instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
conditionally_complete_lattice
by default (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
- INF_def SUP_def intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
+ 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
by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
@@ -197,46 +197,46 @@
unfolding Inf_prod_def by simp
lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
- by (simp add: SUP_def fst_Sup image_image)
+ using fst_Sup [of "f ` A", symmetric] by (simp add: comp_def)
lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
- by (simp add: SUP_def snd_Sup image_image)
+ using snd_Sup [of "f ` A", symmetric] by (simp add: comp_def)
lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
- by (simp add: INF_def fst_Inf image_image)
+ using fst_Inf [of "f ` A", symmetric] by (simp add: comp_def)
lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
- by (simp add: INF_def snd_Inf image_image)
+ 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)"
- by (simp add: SUP_def Sup_prod_def image_image)
+ unfolding SUP_def 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)"
- by (simp add: INF_def Inf_prod_def image_image)
+ unfolding INF_def Inf_prod_def by (simp add: comp_def)
text {* Alternative formulations for set infima and suprema over the product
of two complete lattices: *}
lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
-by (auto simp: Inf_prod_def INF_def)
+by (auto simp: Inf_prod_def)
lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
-by (auto simp: Sup_prod_def SUP_def)
+by (auto simp: Sup_prod_def)
lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
-by (auto simp: INF_def Inf_prod_def image_comp)
+ unfolding INF_def Inf_prod_def by simp
lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
-by (auto simp: SUP_def Sup_prod_def image_comp)
+ unfolding SUP_def Sup_prod_def by simp
lemma INF_prod_alt_def:
"(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
-by (metis fst_INF snd_INF surjective_pairing)
+ by (simp add: INFI_prod_alt_def comp_def)
lemma SUP_prod_alt_def:
"(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
-by (metis fst_SUP snd_SUP surjective_pairing)
+ by (simp add: SUPR_prod_alt_def comp_def)
subsection {* Complete distributive lattices *}
--- a/src/HOL/Lifting_Set.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Lifting_Set.thy Sun Mar 16 18:09:04 2014 +0100
@@ -125,7 +125,7 @@
lemma UNION_transfer [transfer_rule]:
"(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
- unfolding SUP_def [abs_def] by transfer_prover
+ unfolding Union_image_eq [symmetric, abs_def] by transfer_prover
lemma Ball_transfer [transfer_rule]:
"(rel_set A ===> (A ===> op =) ===> op =) Ball Ball"
--- a/src/HOL/List.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/List.thy Sun Mar 16 18:09:04 2014 +0100
@@ -2877,13 +2877,13 @@
lemma (in complete_lattice) INF_set_fold:
"INFI (set xs) f = fold (inf \<circ> f) xs top"
- unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
+ using Inf_set_fold [of "map f xs "] by (simp add: fold_map)
declare INF_set_fold [code]
lemma (in complete_lattice) SUP_set_fold:
"SUPR (set xs) f = fold (sup \<circ> f) xs bot"
- unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
+ using Sup_set_fold [of "map f xs "] by (simp add: fold_map)
declare SUP_set_fold [code]
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Sun Mar 16 18:09:04 2014 +0100
@@ -917,8 +917,8 @@
fixes f :: "nat \<Rightarrow> ereal"
assumes "\<And>n. 0 \<le> f n"
shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
- unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def
- by (auto intro: complete_lattice_class.Sup_upper)
+ unfolding suminf_ereal_eq_SUPR[OF assms]
+ by (auto intro: complete_lattice_class.SUP_upper)
lemma suminf_0_le:
fixes f :: "nat \<Rightarrow> ereal"
@@ -1215,8 +1215,9 @@
apply (subst SUP_inf)
apply (intro SUP_cong[OF refl])
apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
- apply (simp add: INF_def del: inf_ereal_def)
- done
+ apply (drule sym)
+ apply auto
+ by (metis INF_absorb centre_in_ball)
subsection {* monoset *}
--- a/src/HOL/Multivariate_Analysis/Integration.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Sun Mar 16 18:09:04 2014 +0100
@@ -18,7 +18,7 @@
lemma cInf_abs_ge: (* TODO: is this really needed? *)
fixes S :: "real set"
shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
- by (simp add: Inf_real_def) (rule cSup_abs_le, auto)
+ by (simp add: Inf_real_def) (insert cSup_abs_le [of "uminus ` S"], auto)
lemma cSup_asclose: (* TODO: is this really needed? *)
fixes S :: "real set"
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sun Mar 16 18:09:04 2014 +0100
@@ -2709,7 +2709,7 @@
lemma infnorm_Max:
fixes x :: "'a::euclidean_space"
shows "infnorm x = Max ((\<lambda>i. abs (x \<bullet> i)) ` Basis)"
- by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)
+ by (simp add: infnorm_def infnorm_set_image cSup_eq_Max del: Sup_image_eq)
lemma infnorm_set_lemma:
fixes x :: "'a::euclidean_space"
--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Sun Mar 16 18:09:04 2014 +0100
@@ -39,10 +39,12 @@
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
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)+
+ 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)+
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)"
@@ -51,7 +53,7 @@
lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
- by (simp_all add: INF_def SUP_def eucl_Sup eucl_Inf)
+ using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
lemma abs_inner: "i \<in> Basis \<Longrightarrow> abs x \<bullet> i = abs (x \<bullet> i)"
by (auto simp: eucl_abs)
@@ -87,7 +89,7 @@
shows "Sup s = X"
using assms
unfolding eucl_Sup euclidean_representation_setsum
- by (auto simp: Sup_class.SUP_def intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
+ by (auto simp: Sup_class.SUP_def simp del: Sup_class.Sup_image_eq 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"
@@ -96,7 +98,7 @@
shows "Inf s = X"
using assms
unfolding eucl_Inf euclidean_representation_setsum
- by (auto simp: Inf_class.INF_def intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
+ by (auto simp: Inf_class.INF_def simp del: Inf_class.Inf_image_eq intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
end
@@ -115,10 +117,11 @@
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)
+ by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq)
hence "x \<bullet> b = Inf X \<bullet> b"
- by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis`
- setsum_delta cong: if_cong)
+ by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum_delta
+ simp del: Inf_class.Inf_image_eq
+ 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
@@ -137,10 +140,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)
+ by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq)
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 `b \<in> Basis`
- setsum_delta cong: if_cong)
+ by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum_delta
+ simp del: Sup_image_eq 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
@@ -715,7 +718,7 @@
lemma diameter_closed_interval:
fixes a b::"'a::ordered_euclidean_space"
shows "a \<le> b \<Longrightarrow> diameter {a..b} = dist a b"
- by (force simp add: diameter_def SUP_def intro!: cSup_eq_maximum setL2_mono
+ by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono
simp: euclidean_dist_l2[where 'a='a] eucl_le[where 'a='a] dist_norm)
text {* Intervals in general, including infinite and mixtures of open and closed. *}
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Mar 16 18:09:04 2014 +0100
@@ -1548,7 +1548,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)
+ by (auto intro!: cInf_lower bdd_belowI2 simp del: Inf_image_eq)
with a have "a < f y"
by (blast intro: less_le_trans)
}
@@ -3116,7 +3116,7 @@
fix X
assume "X \<subseteq> P' ` insert U A" "finite X" "Inf X = bot"
then obtain B where "B \<subseteq> insert U A" "finite B" and B: "Inf (P' ` B) = bot"
- unfolding subset_image_iff by (auto intro: inj_P' finite_imageD)
+ unfolding subset_image_iff by (auto intro: inj_P' finite_imageD simp del: Inf_image_eq)
with A(2)[THEN spec, of "B - {U}"] have "U \<inter> \<Inter>(B - {U}) \<noteq> {}"
by auto
with B show False
--- a/src/HOL/Predicate.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Predicate.thy Sun Mar 16 18:09:04 2014 +0100
@@ -85,11 +85,11 @@
lemma eval_INFI [simp]:
"eval (INFI A f) = INFI A (eval \<circ> f)"
- by (simp only: INF_def eval_Inf image_comp)
+ using eval_Inf [of "f ` A"] by simp
lemma eval_SUPR [simp]:
"eval (SUPR A f) = SUPR A (eval \<circ> f)"
- by (simp only: SUP_def eval_Sup image_comp)
+ using eval_Sup [of "f ` A"] by simp
instantiation pred :: (type) complete_boolean_algebra
begin
--- a/src/HOL/Probability/Caratheodory.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Sun Mar 16 18:09:04 2014 +0100
@@ -975,7 +975,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: Union_image_eq
+ (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq
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))"
@@ -987,7 +987,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: Union_image_eq
+ (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq
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/Lebesgue_Integration.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Sun Mar 16 18:09:04 2014 +0100
@@ -936,7 +936,7 @@
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
- by (auto simp add: less_Sup_iff)
+ by (auto simp add: less_SUP_iff)
hence "a * u x \<le> f i x" by auto
thus ?thesis using `x \<in> space M` by auto
qed
--- a/src/HOL/Probability/Probability_Measure.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Sun Mar 16 18:09:04 2014 +0100
@@ -159,7 +159,7 @@
moreover
{ fix y assume y: "y \<in> I"
with q(2) `open I` 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) }
+ 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) }
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 Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Sun Mar 16 18:09:04 2014 +0100
@@ -386,7 +386,7 @@
also have "\<dots> = ?y"
proof (rule antisym)
show "(SUP i. integral\<^sup>P M (?g i)) \<le> ?y"
- using g_in_G by (auto intro: Sup_mono simp: SUP_def)
+ using g_in_G by (auto intro: SUP_mono)
show "?y \<le> (SUP i. integral\<^sup>P M (?g i))" unfolding y_eq
by (auto intro!: SUP_mono positive_integral_mono Max_ge)
qed
--- a/src/HOL/Probability/Regularity.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Probability/Regularity.thy Sun Mar 16 18:09:04 2014 +0100
@@ -319,8 +319,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])
- (rule INF_cong, auto simp add: sU intro!: INF_cong)
+ by (subst INF_image [of "\<lambda>u. space M - u", symmetric, unfolded comp_def])
+ (rule INF_cong, auto simp add: sU intro!: INF_cong)
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,7 +335,7 @@
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])
+ by (subst SUP_image [of "\<lambda>u. space M - u", symmetric, simplified comp_def])
(rule SUP_cong, auto simp: sU)
also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
proof (safe intro!: antisym SUP_least)
--- a/src/HOL/Topological_Spaces.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy Sun Mar 16 18:09:04 2014 +0100
@@ -31,13 +31,13 @@
using open_Union [of "{S, T}"] by simp
lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
- unfolding SUP_def by (rule open_Union) auto
+ using open_Union [of "B ` A"] by simp
lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
by (induct set: finite) auto
lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
- unfolding INF_def by (rule open_Inter) auto
+ using open_Inter [of "B ` A"] by simp
lemma openI:
assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"
@@ -70,7 +70,7 @@
by (induct set: finite) auto
lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
- unfolding SUP_def by (rule closed_Union) auto
+ using closed_Union [of "B ` A"] by simp
lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
unfolding closed_def by simp
@@ -169,7 +169,7 @@
lemma generate_topology_Union:
"(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
- unfolding SUP_def by (intro generate_topology.UN) auto
+ using generate_topology.UN [of "K ` I"] by auto
lemma topological_space_generate_topology:
"class.topological_space (generate_topology S)"
@@ -1952,10 +1952,25 @@
unfolding compact_fip by auto
lemma compact_imp_fip_image:
- "compact s \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> closed (f i)) \<Longrightarrow> (\<And>I'. finite I' \<Longrightarrow> I' \<subseteq> I \<Longrightarrow> (s \<inter> (\<Inter>i\<in>I'. f i) \<noteq> {})) \<Longrightarrow>
- s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
- using finite_subset_image[of _ f I] compact_imp_fip[of s "f`I"] unfolding ball_simps[symmetric] INF_def
- by (metis image_iff)
+ assumes "compact s"
+ and P: "\<And>i. i \<in> I \<Longrightarrow> closed (f i)"
+ and Q: "\<And>I'. finite I' \<Longrightarrow> I' \<subseteq> I \<Longrightarrow> (s \<inter> (\<Inter>i\<in>I'. f i) \<noteq> {})"
+ shows "s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
+proof -
+ note `compact s`
+ moreover from P have "\<forall>i \<in> f ` I. closed i" by blast
+ moreover have "\<forall>A. finite A \<and> A \<subseteq> f ` I \<longrightarrow> (s \<inter> (\<Inter>A) \<noteq> {})"
+ proof (rule, rule, erule conjE)
+ fix A :: "'a set set"
+ assume "finite A"
+ moreover assume "A \<subseteq> f ` I"
+ ultimately obtain B where "B \<subseteq> I" and "finite B" and "A = f ` B"
+ using finite_subset_image [of A f I] by blast
+ with Q [of B] show "s \<inter> \<Inter>A \<noteq> {}" by simp
+ qed
+ ultimately have "s \<inter> (\<Inter>(f ` I)) \<noteq> {}" by (rule compact_imp_fip)
+ then show ?thesis by simp
+qed
end
--- a/src/HOL/UNITY/ProgressSets.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/UNITY/ProgressSets.thy Sun Mar 16 18:09:04 2014 +0100
@@ -257,7 +257,7 @@
apply (simp add: progress_induction_step)
txt{*Disjunctive case*}
apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C")
- apply (simp add: Int_Union)
+ apply simp
apply (blast intro: UN_in_lattice)
done
--- a/src/HOL/Wellfounded.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Wellfounded.thy Sun Mar 16 18:09:04 2014 +0100
@@ -306,7 +306,7 @@
"[| ALL r:R. wf r;
ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}
|] ==> wf(Union R)"
- using wf_UN[of R "\<lambda>i. i"] by (simp add: SUP_def)
+ using wf_UN[of R "\<lambda>i. i"] by simp
(*Intuition: we find an (R u S)-min element of a nonempty subset A
by case distinction.