--- a/src/HOL/Complete_Lattices.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Complete_Lattices.thy Sat Nov 10 07:57:19 2018 +0000
@@ -16,21 +16,9 @@
class Inf =
fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter> _" [900] 900)
-begin
-
-abbreviation (input) INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
- where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
-
-end
class Sup =
fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion> _" [900] 900)
-begin
-
-abbreviation (input) SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
- where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
-
-end
syntax (ASCII)
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10)
@@ -858,9 +846,6 @@
subsubsection \<open>Intersections of families\<close>
-abbreviation (input) INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" \<comment> \<open>legacy\<close>
- where "INTER \<equiv> INFIMUM"
-
syntax (ASCII)
"_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3INT _./ _)" [0, 10] 10)
"_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10)
@@ -915,7 +900,7 @@
lemma INT_subset_iff: "B \<subseteq> (\<Inter>i\<in>I. A i) \<longleftrightarrow> (\<forall>i\<in>I. B \<subseteq> A i)"
by (fact le_INF_iff)
-lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
+lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> \<Inter> (B ` A)"
by (fact INF_insert)
lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
@@ -1018,9 +1003,6 @@
subsubsection \<open>Unions of families\<close>
-abbreviation (input) UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" \<comment> \<open>legacy\<close>
- where "UNION \<equiv> SUPREMUM"
-
syntax (ASCII)
"_UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)
"_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 0, 10] 10)
@@ -1050,10 +1032,10 @@
lemma UNION_eq: "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
by (auto intro!: SUP_eqI)
-lemma bind_UNION [code]: "Set.bind A f = UNION A f"
+lemma bind_UNION [code]: "Set.bind A f = \<Union>(f ` A)"
by (simp add: bind_def UNION_eq)
-lemma member_bind [simp]: "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
+lemma member_bind [simp]: "x \<in> Set.bind A f \<longleftrightarrow> x \<in> \<Union>(f ` A)"
by (simp add: bind_UNION)
lemma Union_SetCompr_eq: "\<Union>{f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
@@ -1091,7 +1073,7 @@
lemma UN_absorb: "k \<in> I \<Longrightarrow> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
by (fact SUP_absorb)
-lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
+lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> \<Union>(B ` A)"
by (fact SUP_insert)
lemma UN_Un [simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
@@ -1120,10 +1102,10 @@
lemma Collect_ex_eq: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
by blast
-lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
+lemma ball_UN: "(\<forall>z \<in> \<Union>(B ` A). P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
by blast
-lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
+lemma bex_UN: "(\<exists>z \<in> \<Union>(B ` A). P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
by blast
lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
@@ -1150,7 +1132,7 @@
\<comment> \<open>NOT suitable for rewriting\<close>
by blast
-lemma image_UN: "f ` UNION A B = (\<Union>x\<in>A. f ` B x)"
+lemma image_UN: "f ` \<Union>(B ` A) = (\<Union>x\<in>A. f ` B x)"
by blast
lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
@@ -1251,14 +1233,14 @@
proof safe
have "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)"
using bij bij_betw_def[of f] by auto
- then show "inj_on f (UNION I A)"
+ then show "inj_on f (\<Union>(A ` I))"
using chain inj_on_UNION_chain[of I A f] by auto
next
fix i x
assume *: "i \<in> I" "x \<in> A i"
with bij have "f x \<in> A' i"
by (auto simp: bij_betw_def)
- with * show "f x \<in> UNION I A'" by blast
+ with * show "f x \<in> \<Union>(A' ` I)" by blast
next
fix i x'
assume *: "i \<in> I" "x' \<in> A' i"
@@ -1266,18 +1248,18 @@
unfolding bij_betw_def by blast
with * have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
by blast
- then show "x' \<in> f ` UNION I A"
+ then show "x' \<in> f ` \<Union>(A ` I)"
by blast
qed
(*injectivity's required. Left-to-right inclusion holds even if A is empty*)
-lemma image_INT: "inj_on f C \<Longrightarrow> \<forall>x\<in>A. B x \<subseteq> C \<Longrightarrow> j \<in> A \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)"
+lemma image_INT: "inj_on f C \<Longrightarrow> \<forall>x\<in>A. B x \<subseteq> C \<Longrightarrow> j \<in> A \<Longrightarrow> f ` (\<Inter>(B ` A)) = (\<Inter>x\<in>A. f ` B x)"
by (auto simp add: inj_on_def) blast
-lemma bij_image_INT: "bij f \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)"
+lemma bij_image_INT: "bij f \<Longrightarrow> f ` (\<Inter>(B ` A)) = (\<Inter>x\<in>A. f ` B x)"
by (auto simp: bij_def inj_def surj_def) blast
-lemma UNION_fun_upd: "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
+lemma UNION_fun_upd: "\<Union>(A(i := B) ` J) = \<Union>(A ` (J - {i})) \<union> (if i \<in> J then B else {})"
by (auto simp add: set_eq_iff)
lemma bij_betw_Pow:
@@ -1321,7 +1303,7 @@
"\<And>A B C. (\<Union>x\<in>C. A x - B) = ((\<Union>x\<in>C. A x) - B)"
"\<And>A B C. (\<Union>x\<in>C. A - B x) = (A - (\<Inter>x\<in>C. B x))"
"\<And>A B. (\<Union>x\<in>\<Union>A. B x) = (\<Union>y\<in>A. \<Union>x\<in>y. B x)"
- "\<And>A B C. (\<Union>z\<in>UNION A B. C z) = (\<Union>x\<in>A. \<Union>z\<in>B x. C z)"
+ "\<And>A B C. (\<Union>z\<in>(\<Union>(B ` A)). C z) = (\<Union>x\<in>A. \<Union>z\<in>B x. C z)"
"\<And>A B f. (\<Union>x\<in>f`A. B x) = (\<Union>a\<in>A. B (f a))"
by auto
@@ -1334,15 +1316,15 @@
"\<And>A B C. (\<Inter>x\<in>C. A x \<union> B) = ((\<Inter>x\<in>C. A x) \<union> B)"
"\<And>A B C. (\<Inter>x\<in>C. A \<union> B x) = (A \<union> (\<Inter>x\<in>C. B x))"
"\<And>A B. (\<Inter>x\<in>\<Union>A. B x) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B x)"
- "\<And>A B C. (\<Inter>z\<in>UNION A B. C z) = (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z)"
+ "\<And>A B C. (\<Inter>z\<in>(\<Union>(B ` A)). C z) = (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z)"
"\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))"
by auto
lemma UN_ball_bex_simps [simp]:
"\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)"
- "\<And>A B P. (\<forall>x\<in>UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
+ "\<And>A B P. (\<forall>x\<in>(\<Union>(B ` A)). P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
"\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)"
- "\<And>A B P. (\<exists>x\<in>UNION A B. P x) \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x\<in>B a. P x)"
+ "\<And>A B P. (\<exists>x\<in>(\<Union>(B ` A)). P x) \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x\<in>B a. P x)"
by auto
@@ -1357,7 +1339,7 @@
"\<And>A B C. ((\<Union>x\<in>C. A x) - B) = (\<Union>x\<in>C. A x - B)"
"\<And>A B C. (A - (\<Inter>x\<in>C. B x)) = (\<Union>x\<in>C. A - B x)"
"\<And>A B. (\<Union>y\<in>A. \<Union>x\<in>y. B x) = (\<Union>x\<in>\<Union>A. B x)"
- "\<And>A B C. (\<Union>x\<in>A. \<Union>z\<in>B x. C z) = (\<Union>z\<in>UNION A B. C z)"
+ "\<And>A B C. (\<Union>x\<in>A. \<Union>z\<in>B x. C z) = (\<Union>z\<in>(\<Union>(B ` A)). C z)"
"\<And>A B f. (\<Union>a\<in>A. B (f a)) = (\<Union>x\<in>f`A. B x)"
by auto
@@ -1370,7 +1352,7 @@
"\<And>A B C. ((\<Inter>x\<in>C. A x) \<union> B) = (\<Inter>x\<in>C. A x \<union> B)"
"\<And>A B C. A \<union> (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. A \<union> B x)"
"\<And>A B. (\<Inter>y\<in>A. \<Inter>x\<in>y. B x) = (\<Inter>x\<in>\<Union>A. B x)"
- "\<And>A B C. (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z) = (\<Inter>z\<in>UNION A B. C z)"
+ "\<And>A B C. (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z) = (\<Inter>z\<in>(\<Union>(B ` A)). C z)"
"\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
by auto
--- a/src/HOL/Conditionally_Complete_Lattices.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Sat Nov 10 07:57:19 2018 +0000
@@ -286,22 +286,22 @@
lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
by (auto intro!: cInf_eq_minimum)
-lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFIMUM A f \<le> f x"
+lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> \<Sqinter>(f ` A) \<le> f x"
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> INFIMUM A f"
+lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> \<Sqinter>(f ` A)"
using cInf_greatest [of "f ` A"] by auto
-lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPREMUM A f"
+lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> \<Squnion>(f ` A)"
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> SUPREMUM A f \<le> M"
+lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> \<Squnion>(f ` A) \<le> M"
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> INFIMUM A f \<le> u"
+lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> \<Sqinter>(f ` A) \<le> u"
by (auto intro: cINF_lower order_trans)
-lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPREMUM A f"
+lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> \<Squnion>(f ` A)"
by (auto intro: cSUP_upper order_trans)
lemma cSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>x\<in>A. c) = c"
@@ -310,10 +310,10 @@
lemma cINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>x\<in>A. c) = c"
by (intro antisym cINF_greatest) (auto intro: cINF_lower)
-lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFIMUM A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
+lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> \<Sqinter>(f ` A) \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
by (metis cINF_greatest cINF_lower order_trans)
-lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
+lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> \<Squnion>(f ` A) \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
by (metis cSUP_least cSUP_upper order_trans)
lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (\<Sqinter>i\<in>A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i"
@@ -322,22 +322,22 @@
lemma cSUP_lessD: "bdd_above (f`A) \<Longrightarrow> (\<Squnion>i\<in>A. f i) < y \<Longrightarrow> i \<in> A \<Longrightarrow> f i < y"
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 image_insert image_is_empty)
+lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> \<Sqinter>(f ` insert a A) = inf (f a) (\<Sqinter>(f ` A))"
+ by (simp add: cInf_insert cong del: INF_cong)
-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 image_insert image_is_empty)
+lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> \<Squnion>(f ` insert a A) = sup (f a) (\<Squnion>(f ` A))"
+ by (simp add: cSup_insert cong del: SUP_cong)
-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"
+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> \<Sqinter>(f ` A) \<le> \<Sqinter>(g ` B)"
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> SUPREMUM A f \<le> SUPREMUM B g"
+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> \<Squnion>(f ` A) \<le> \<Squnion>(g ` B)"
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> INFIMUM B g \<le> INFIMUM A f"
+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> \<Sqinter>(g ` B) \<le> \<Sqinter>(f ` A)"
by (rule cINF_mono) auto
-lemma cSUP_subset_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> SUPREMUM A f \<le> SUPREMUM B g"
+lemma cSUP_subset_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> \<Squnion>(f ` A) \<le> \<Squnion>(g ` B)"
by (rule cSUP_mono) auto
lemma less_eq_cInf_inter: "bdd_below A \<Longrightarrow> bdd_below B \<Longrightarrow> A \<inter> B \<noteq> {} \<Longrightarrow> inf (Inf A) (Inf B) \<le> Inf (A \<inter> B)"
@@ -349,20 +349,20 @@
lemma cInf_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below B \<Longrightarrow> Inf (A \<union> B) = inf (Inf A) (Inf B)"
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> INFIMUM (A \<union> B) f = inf (INFIMUM A f) (INFIMUM B f)"
- using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
+lemma cINF_union: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below (f ` B) \<Longrightarrow> \<Sqinter> (f ` (A \<union> B)) = \<Sqinter> (f ` A) \<sqinter> \<Sqinter> (f ` B)"
+ using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un cong del: INF_cong)
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> SUPREMUM (A \<union> B) f = sup (SUPREMUM A f) (SUPREMUM B f)"
- using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
+lemma cSUP_union: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above (f ` B) \<Longrightarrow> \<Squnion> (f ` (A \<union> B)) = \<Squnion> (f ` A) \<squnion> \<Squnion> (f ` B)"
+ using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un cong del: SUP_cong)
-lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> inf (INFIMUM A f) (INFIMUM A g) = (\<Sqinter>a\<in>A. inf (f a) (g a))"
+lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> \<Sqinter> (f ` A) \<sqinter> \<Sqinter> (g ` A) = (\<Sqinter>a\<in>A. inf (f a) (g a))"
by (intro antisym le_infI cINF_greatest cINF_lower2)
(auto intro: le_infI1 le_infI2 cINF_greatest cINF_lower le_infI)
-lemma SUP_sup_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> bdd_above (g`A) \<Longrightarrow> sup (SUPREMUM A f) (SUPREMUM A g) = (\<Squnion>a\<in>A. sup (f a) (g a))"
+lemma SUP_sup_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> bdd_above (g`A) \<Longrightarrow> \<Squnion> (f ` A) \<squnion> \<Squnion> (g ` A) = (\<Squnion>a\<in>A. sup (f a) (g a))"
by (intro antisym le_supI cSUP_least cSUP_upper2)
(auto intro: le_supI1 le_supI2 cSUP_least cSUP_upper le_supI)
--- a/src/HOL/Enum.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Enum.thy Sat Nov 10 07:57:19 2018 +0000
@@ -846,8 +846,8 @@
by simp
qed
-lemma finite_Inf_Sup: "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
-proof (rule finite_induct [of A "\<lambda> A .INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"], simp_all add: finite_UnionD)
+lemma finite_Inf_Sup: "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+proof (rule finite_induct [of A "\<lambda>A. \<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"], simp_all add: finite_UnionD)
fix x::"'a set"
fix F
assume "x \<notin> F"
@@ -858,13 +858,13 @@
by (auto simp add: fa_def)
from this have B: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> fa b f ` ({x} \<union> F) \<in> {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)}"
by blast
- have [simp]: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> b \<sqinter> (\<Sqinter>x\<in>F. f x) \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
+ have [simp]: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> b \<sqinter> (\<Sqinter>x\<in>F. f x) \<le> \<Squnion>(Inf ` {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)})"
using B apply (rule SUP_upper2, simp_all)
by (simp_all add: INF_greatest Inf_lower inf.coboundedI2 fa_def)
- assume "INFIMUM F Sup \<le> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf"
+ assume "\<Sqinter>(Sup ` F) \<le> \<Squnion>(Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y})"
- from this have "\<Squnion>x \<sqinter> INFIMUM F Sup \<le> \<Squnion>x \<sqinter> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf"
+ from this have "\<Squnion>x \<sqinter> \<Sqinter>(Sup ` F) \<le> \<Squnion>x \<sqinter> \<Squnion>(Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y})"
apply simp
using inf.coboundedI2 by blast
also have "... = Sup {\<Squnion>x \<sqinter> (Inf (f ` F)) |f . (\<forall>Y\<in>F. f Y \<in> Y)}"
@@ -874,11 +874,11 @@
apply (subst inf_commute)
by (simp add: finite_inf_Sup)
- also have "... \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
+ also have "... \<le> \<Squnion>(Inf ` {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)})"
apply (rule Sup_least, clarsimp)+
by (subst inf_commute, simp)
- finally show "\<Squnion>x \<sqinter> INFIMUM F Sup \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
+ finally show "\<Squnion>x \<sqinter> \<Sqinter>(Sup ` F) \<le> \<Squnion>(Inf ` {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)})"
by simp
qed
--- a/src/HOL/Filter.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Filter.thy Sat Nov 10 07:57:19 2018 +0000
@@ -669,9 +669,9 @@
by (subst eventually_INF) blast
also have "\<dots> \<longleftrightarrow> (\<exists>X. (X \<subseteq> B \<and> finite X) \<and> eventually P (filtercomap f (\<Sqinter>b\<in>X. F b)))"
by (rule ex_cong) (simp add: *)
- also have "\<dots> \<longleftrightarrow> eventually P (filtercomap f (INFIMUM B F))"
+ also have "\<dots> \<longleftrightarrow> eventually P (filtercomap f (\<Sqinter>(F ` B)))"
unfolding eventually_filtercomap by (subst eventually_INF) blast
- finally show "eventually P (filtercomap f (INFIMUM B F)) =
+ finally show "eventually P (filtercomap f (\<Sqinter>(F ` B))) =
eventually P (\<Sqinter>b\<in>B. filtercomap f (F b))" ..
qed
qed
--- a/src/HOL/Finite_Set.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Finite_Set.thy Sat Nov 10 07:57:19 2018 +0000
@@ -256,7 +256,7 @@
"finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> finite (B a)) \<Longrightarrow> finite (\<Union>a\<in>A. B a)"
by (induct rule: finite_induct) simp_all
-lemma finite_UN [simp]: "finite A \<Longrightarrow> finite (UNION A B) \<longleftrightarrow> (\<forall>x\<in>A. finite (B x))"
+lemma finite_UN [simp]: "finite A \<Longrightarrow> finite (\<Union>(B ` A)) \<longleftrightarrow> (\<forall>x\<in>A. finite (B x))"
by (blast intro: finite_subset)
lemma finite_Inter [intro]: "\<exists>A\<in>M. finite A \<Longrightarrow> finite (\<Inter>M)"
@@ -1254,7 +1254,7 @@
lemma inf_INF_fold_inf:
assumes "finite A"
- shows "inf B (INFIMUM A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold")
+ shows "inf B (\<Sqinter>(f ` A)) = fold (inf \<circ> f) B A" (is "?inf = ?fold")
proof -
interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
@@ -1265,7 +1265,7 @@
lemma sup_SUP_fold_sup:
assumes "finite A"
- shows "sup B (SUPREMUM A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold")
+ shows "sup B (\<Squnion>(f ` A)) = fold (sup \<circ> f) B A" (is "?sup = ?fold")
proof -
interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
@@ -1274,10 +1274,10 @@
then show ?thesis ..
qed
-lemma INF_fold_inf: "finite A \<Longrightarrow> INFIMUM A f = fold (inf \<circ> f) top A"
+lemma INF_fold_inf: "finite A \<Longrightarrow> \<Sqinter>(f ` A) = fold (inf \<circ> f) top A"
using inf_INF_fold_inf [of A top] by simp
-lemma SUP_fold_sup: "finite A \<Longrightarrow> SUPREMUM A f = fold (sup \<circ> f) bot A"
+lemma SUP_fold_sup: "finite A \<Longrightarrow> \<Squnion>(f ` A) = fold (sup \<circ> f) bot A"
using sup_SUP_fold_sup [of A bot] by simp
end
--- a/src/HOL/Groups_Big.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Groups_Big.thy Sat Nov 10 07:57:19 2018 +0000
@@ -161,14 +161,14 @@
lemma UNION_disjoint:
assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
- shows "F g (UNION I A) = F (\<lambda>x. F g (A x)) I"
+ shows "F g (\<Union>(A ` I)) = F (\<lambda>x. F g (A x)) I"
apply (insert assms)
apply (induct rule: finite_induct)
apply simp
apply atomize
apply (subgoal_tac "\<forall>i\<in>Fa. x \<noteq> i")
prefer 2 apply blast
- apply (subgoal_tac "A x \<inter> UNION Fa A = {}")
+ apply (subgoal_tac "A x \<inter> \<Union>(A ` Fa) = {}")
prefer 2 apply blast
apply (simp add: union_disjoint)
done
@@ -1023,7 +1023,7 @@
lemma card_UN_disjoint:
assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
- shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
+ shows "card (\<Union>(A ` I)) = (\<Sum>i\<in>I. card(A i))"
proof -
have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)"
by simp
--- a/src/HOL/Hilbert_Choice.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Hilbert_Choice.thy Sat Nov 10 07:57:19 2018 +0000
@@ -911,39 +911,39 @@
begin
lemma Sup_Inf: "Sup (Inf ` A) = Inf (Sup ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})"
proof (rule antisym)
- show "SUPREMUM A Inf \<le> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup"
+ show "\<Squnion>(Inf ` A) \<le> \<Sqinter>(Sup ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
apply (rule Sup_least, rule INF_greatest)
using Inf_lower2 Sup_upper by auto
next
- show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup \<le> SUPREMUM A Inf"
+ show "\<Sqinter>(Sup ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> \<Squnion>(Inf ` A)"
proof (simp add: Inf_Sup, rule SUP_least, simp, safe)
fix f
assume "\<forall>Y. (\<exists>f. Y = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<longrightarrow> f Y \<in> Y"
from this have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y) \<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z"
by auto
- show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> SUPREMUM A Inf"
- proof (cases "\<exists> Z \<in> A . INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> Inf Z")
+ show "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> \<Squnion>(Inf ` A)"
+ proof (cases "\<exists> Z \<in> A . \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> Inf Z")
case True
- from this obtain Z where [simp]: "Z \<in> A" and A: "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> Inf Z"
+ from this obtain Z where [simp]: "Z \<in> A" and A: "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> Inf Z"
by blast
- have B: "... \<le> SUPREMUM A Inf"
+ have B: "... \<le> \<Squnion>(Inf ` A)"
by (simp add: SUP_upper)
from A and B show ?thesis
by simp
next
case False
- from this have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x \<in> Z \<and> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> x"
+ from this have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x \<in> Z \<and> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> x"
using Inf_greatest by blast
- define F where "F = (\<lambda> Z . SOME x . x \<in> Z \<and> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> x)"
+ define F where "F = (\<lambda> Z . SOME x . x \<in> Z \<and> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> x)"
have C: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
using X by (simp add: F_def, rule someI2_ex, auto)
- have E: "\<And> Y . Y \<in> A \<Longrightarrow> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> F Y"
+ have E: "\<And> Y . Y \<in> A \<Longrightarrow> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> F Y"
using X by (simp add: F_def, rule someI2_ex, auto)
from C and B obtain Z where D: "Z \<in> A " and Y: "f (F ` A) = F Z"
by blast
- from E and D have W: "\<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> F Z"
+ from E and D have W: "\<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> F Z"
by simp
- have "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> f (F ` A)"
+ have "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> f (F ` A)"
apply (rule INF_lower)
using C by blast
from this and W and Y show ?thesis
@@ -966,7 +966,7 @@
next
have "\<Sqinter>((\<squnion>) a ` B) \<le> \<Sqinter>(Sup ` {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B})"
by (rule INF_greatest, auto simp add: INF_lower)
- also have "... = SUPREMUM {{a}, B} Inf"
+ also have "... = \<Squnion>(Inf ` {{a}, B})"
by (unfold Sup_Inf, simp)
finally show "\<Sqinter>((\<squnion>) a ` B) \<le> a \<squnion> \<Sqinter>B"
by simp
@@ -1024,7 +1024,7 @@
by (rule INF_lower2, blast+)
have B: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> f xa \<in> xa"
by blast
- have A: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> (\<Sqinter>x\<in>A. g (f x)) \<le> SUPREMUM xa g"
+ have A: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> (\<Sqinter>x\<in>A. g (f x)) \<le> \<Squnion>(g ` xa)"
by (rule SUP_upper2, rule B, simp_all, simp)
show "(\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)"
apply (rule SUP_least, simp, safe, rule INF_greatest, simp)
@@ -1175,13 +1175,13 @@
subclass complete_distrib_lattice
proof (standard, rule ccontr)
fix A
- assume "\<not> INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
- from this have C: "INFIMUM A Sup > SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
- using local.not_le by blast
- show "False"
- proof (cases "\<exists> z . INFIMUM A Sup > z \<and> z > SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
+ assume "\<not> \<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+ then have C: "\<Sqinter>(Sup ` A) > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+ by (simp add: not_le)
+ show False
+ proof (cases "\<exists> z . \<Sqinter>(Sup ` A) > z \<and> z > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})")
case True
- from this obtain z where A: "z < INFIMUM A Sup" and X: "SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < z"
+ from this obtain z where A: "z < \<Sqinter>(Sup ` A)" and X: "z > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
by blast
from A have "\<And> Y . Y \<in> A \<Longrightarrow> z < Sup Y"
@@ -1204,28 +1204,28 @@
have "z \<le> Inf (F ` A)"
by (simp add: D local.INF_greatest local.order.strict_implies_order)
- also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ also have "... \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
apply (rule SUP_upper, safe)
using E by blast
- finally have "z \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ finally have "z \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
by simp
from X and this show ?thesis
using local.not_less by blast
next
case False
- from this have A: "\<And> z . INFIMUM A Sup \<le> z \<or> z \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ from this have A: "\<And> z . \<Sqinter>(Sup ` A) \<le> z \<or> z \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
using local.le_less_linear by blast
-
- from C have "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < Sup Y"
+
+ from C have "\<And> Y . Y \<in> A \<Longrightarrow> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < Sup Y"
by (simp add: less_INF_D)
-
- from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < k"
+
+ from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < k"
using local.less_Sup_iff by blast
- define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < k)"
-
- have D: "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < F Y"
+ define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < k)"
+
+ have D: "\<And> Y . Y \<in> A \<Longrightarrow> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < F Y"
using B apply (simp add: F_def)
by (rule someI2_ex, auto)
@@ -1233,17 +1233,17 @@
using B apply (simp add: F_def)
by (rule someI2_ex, auto)
- have "\<And> Y . Y \<in> A \<Longrightarrow> INFIMUM A Sup \<le> F Y"
+ have "\<And> Y . Y \<in> A \<Longrightarrow> \<Sqinter>(Sup ` A) \<le> F Y"
using D False local.leI by blast
- from this have "INFIMUM A Sup \<le> Inf (F ` A)"
+ from this have "\<Sqinter>(Sup ` A) \<le> Inf (F ` A)"
by (simp add: local.INF_greatest)
- also have "Inf (F ` A) \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ also have "Inf (F ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
apply (rule SUP_upper, safe)
using E by blast
-
- finally have "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+
+ finally have "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
by simp
from C and this show ?thesis
--- a/src/HOL/Lifting_Set.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Lifting_Set.thy Sat Nov 10 07:57:19 2018 +0000
@@ -134,8 +134,8 @@
"((A ===> B) ===> rel_set A ===> rel_set B) image image"
unfolding rel_fun_def rel_set_def by simp fast
-lemma UNION_transfer [transfer_rule]:
- "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
+lemma UNION_transfer [transfer_rule]: \<comment> \<open>TODO deletion candidate\<close>
+ "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) (\<lambda>A f. \<Union>(f ` A)) (\<lambda>A f. \<Union>(f ` A))"
by transfer_prover
lemma Ball_transfer [transfer_rule]:
@@ -172,12 +172,12 @@
"(rel_set A ===> (A ===> rel_set B) ===> rel_set B) Set.bind Set.bind"
unfolding bind_UNION [abs_def] by transfer_prover
-lemma INF_parametric [transfer_rule]:
- "(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) INFIMUM INFIMUM"
+lemma INF_parametric [transfer_rule]: \<comment> \<open>TODO deletion candidate\<close>
+ "(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) (\<lambda>A f. Inf (f ` A)) (\<lambda>A f. Inf (f ` A))"
by transfer_prover
-lemma SUP_parametric [transfer_rule]:
- "(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) SUPREMUM SUPREMUM"
+lemma SUP_parametric [transfer_rule]: \<comment> \<open>TODO deletion candidate\<close>
+ "(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) (\<lambda>A f. Sup (f ` A)) (\<lambda>A f. Sup (f ` A))"
by transfer_prover
@@ -316,7 +316,7 @@
lemma rel_set_UNION:
assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g"
- shows "rel_set R (UNION A f) (UNION B g)"
+ shows "rel_set R (\<Union>(f ` A)) (\<Union>(g ` B))"
by transfer_prover
end
--- a/src/HOL/List.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/List.thy Sat Nov 10 07:57:19 2018 +0000
@@ -2985,11 +2985,11 @@
declare Sup_set_fold [where 'a = "'a set", code]
lemma (in complete_lattice) INF_set_fold:
- "INFIMUM (set xs) f = fold (inf \<circ> f) xs top"
+ "\<Sqinter>(f ` set xs) = fold (inf \<circ> f) xs top"
using Inf_set_fold [of "map f xs"] by (simp add: fold_map)
lemma (in complete_lattice) SUP_set_fold:
- "SUPREMUM (set xs) f = fold (sup \<circ> f) xs bot"
+ "\<Squnion>(f ` set xs) = fold (sup \<circ> f) xs bot"
using Sup_set_fold [of "map f xs"] by (simp add: fold_map)
--- a/src/HOL/Main.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Main.thy Sat Nov 10 07:57:19 2018 +0000
@@ -11,12 +11,50 @@
Quickcheck_Narrowing
Extraction
Nunchaku
- BNF_Greatest_Fixpoint Filter
+ BNF_Greatest_Fixpoint
+ Filter
Conditionally_Complete_Lattices
Binomial
GCD
begin
+text \<open>Legacy\<close>
+
+context Inf
+begin
+
+abbreviation (input) INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
+ where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
+
+end
+
+context Sup
+begin
+
+abbreviation (input) SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
+ where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
+
+end
+
+abbreviation (input) INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+ where "INTER \<equiv> INFIMUM"
+
+abbreviation (input) UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+ where "UNION \<equiv> SUPREMUM"
+
+
+text \<open>Namespace cleanup\<close>
+
+hide_const (open)
+ czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
+ fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
+ shift proj id_bnf
+
+hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
+
+
+text \<open>Syntax cleanup\<close>
+
no_notation
bot ("\<bottom>") and
top ("\<top>") and
@@ -29,17 +67,10 @@
ordLess2 (infix "<o" 50) and
ordIso2 (infix "=o" 50) and
card_of ("|_|") and
- csum (infixr "+c" 65) and
- cprod (infixr "*c" 80) and
- cexp (infixr "^c" 90) and
- convol ("\<langle>(_,/ _)\<rangle>")
-
-hide_const (open)
- czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
- fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
- shift proj id_bnf
-
-hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
+ BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
+ BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
+ BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90) and
+ BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
no_syntax
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
--- a/src/HOL/Option.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Option.thy Sat Nov 10 07:57:19 2018 +0000
@@ -260,7 +260,7 @@
lemma bind_map_option: "bind (map_option f x) g = bind x (g \<circ> f)"
by(cases x) simp_all
-lemma set_bind_option [simp]: "set_option (bind x f) = UNION (set_option x) (set_option \<circ> f)"
+lemma set_bind_option [simp]: "set_option (bind x f) = (\<Union>((set_option \<circ> f) ` set_option x))"
by(cases x) auto
lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \<circ> f)"
--- a/src/HOL/Predicate.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Predicate.thy Sat Nov 10 07:57:19 2018 +0000
@@ -58,17 +58,17 @@
by (simp add: sup_pred_def)
definition
- "\<Sqinter>A = Pred (INFIMUM A eval)"
+ "\<Sqinter>A = Pred (\<Sqinter>(eval ` A))"
lemma eval_Inf [simp]:
- "eval (\<Sqinter>A) = INFIMUM A eval"
+ "eval (\<Sqinter>A) = \<Sqinter>(eval ` A)"
by (simp add: Inf_pred_def)
definition
- "\<Squnion>A = Pred (SUPREMUM A eval)"
+ "\<Squnion>A = Pred (\<Squnion>(eval ` A))"
lemma eval_Sup [simp]:
- "eval (\<Squnion>A) = SUPREMUM A eval"
+ "eval (\<Squnion>A) = \<Squnion>(eval ` A)"
by (simp add: Sup_pred_def)
instance proof
@@ -77,12 +77,12 @@
end
lemma eval_INF [simp]:
- "eval (INFIMUM A f) = INFIMUM A (eval \<circ> f)"
- using eval_Inf [of "f ` A"] by simp
+ "eval (\<Sqinter>(f ` A)) = \<Sqinter>((eval \<circ> f) ` A)"
+ by simp
lemma eval_SUP [simp]:
- "eval (SUPREMUM A f) = SUPREMUM A (eval \<circ> f)"
- using eval_Sup [of "f ` A"] by simp
+ "eval (\<Squnion>(f ` A)) = \<Squnion>((eval \<circ> f) ` A)"
+ by simp
instantiation pred :: (type) complete_boolean_algebra
begin
@@ -103,7 +103,7 @@
instance proof
fix A::"'a pred set set"
- show "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ show "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
proof (simp add: less_eq_pred_def Sup_fun_def Inf_fun_def, safe)
fix w
assume A: "\<forall>x\<in>A. \<exists>f\<in>x. eval f w"
@@ -127,10 +127,10 @@
by (simp add: single_def)
definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<bind>" 70) where
- "P \<bind> f = (SUPREMUM {x. eval P x} f)"
+ "P \<bind> f = (\<Squnion>(f ` {x. eval P x}))"
lemma eval_bind [simp]:
- "eval (P \<bind> f) = eval (SUPREMUM {x. eval P x} f)"
+ "eval (P \<bind> f) = eval (\<Squnion>(f ` {x. eval P x}))"
by (simp add: bind_def)
lemma bind_bind:
--- a/src/HOL/Product_Type.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Product_Type.thy Sat Nov 10 07:57:19 2018 +0000
@@ -1049,7 +1049,7 @@
\<Longrightarrow> A \<subseteq> Collect (case_prod P) \<Longrightarrow> A \<subseteq> Collect (case_prod Q)"
by fastforce
-lemma UN_Times_distrib: "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
+lemma UN_Times_distrib: "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = \<Union>(E ` A) \<times> \<Union>(F ` B)"
\<comment> \<open>Suggested by Pierre Chartier\<close>
by blast
--- a/src/HOL/Relation.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Relation.thy Sat Nov 10 07:57:19 2018 +0000
@@ -120,25 +120,25 @@
lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))"
by (simp add: fun_eq_iff)
-lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
+lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> (\<Inter>(Collect ` S)))"
by (simp add: fun_eq_iff)
lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
by (simp add: fun_eq_iff)
-lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (case_prod ` S) Collect)"
+lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> (\<Inter>(Collect ` case_prod ` S)))"
by (simp add: fun_eq_iff)
lemma INF_Int_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Inter>S)"
by (simp add: fun_eq_iff)
-lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> UNION S Collect)"
+lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> \<Union>(Collect ` S))"
by (simp add: fun_eq_iff)
lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)"
by (simp add: fun_eq_iff)
-lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (case_prod ` S) Collect)"
+lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> (\<Union>(Collect ` case_prod ` S)))"
by (simp add: fun_eq_iff)
lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
@@ -198,10 +198,10 @@
lemma reflp_sup: "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<squnion> s)"
by (auto intro: reflpI elim: reflpE)
-lemma refl_on_INTER: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (INTER S A) (INTER S r)"
+lemma refl_on_INTER: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (\<Inter>(A ` S)) (\<Inter>(r ` S))"
unfolding refl_on_def by fast
-lemma refl_on_UNION: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)"
+lemma refl_on_UNION: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (\<Union>(A ` S)) (\<Union>(r ` S))"
unfolding refl_on_def by blast
lemma refl_on_empty [simp]: "refl_on {} {}"
@@ -303,16 +303,16 @@
lemma symp_sup: "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<squnion> s)"
by (fact sym_Un [to_pred])
-lemma sym_INTER: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (INTER S r)"
+lemma sym_INTER: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (\<Inter>(r ` S))"
by (fast intro: symI elim: symE)
-lemma symp_INF: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFIMUM S r)"
+lemma symp_INF: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (\<Sqinter>(r ` S))"
by (fact sym_INTER [to_pred])
-lemma sym_UNION: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (UNION S r)"
+lemma sym_UNION: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (\<Union>(r ` S))"
by (fast intro: symI elim: symE)
-lemma symp_SUP: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPREMUM S r)"
+lemma symp_SUP: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (\<Squnion>(r ` S))"
by (fact sym_UNION [to_pred])
@@ -411,10 +411,10 @@
lemma transp_inf: "transp r \<Longrightarrow> transp s \<Longrightarrow> transp (r \<sqinter> s)"
by (fact trans_Int [to_pred])
-lemma trans_INTER: "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (INTER S r)"
+lemma trans_INTER: "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (\<Inter>(r ` S))"
by (fast intro: transI elim: transD)
-lemma transp_INF: "\<forall>x\<in>S. transp (r x) \<Longrightarrow> transp (INFIMUM S r)"
+lemma transp_INF: "\<forall>x\<in>S. transp (r x) \<Longrightarrow> transp (\<Sqinter>(r ` S))"
by (fact trans_INTER [to_pred])
lemma trans_join [code]: "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
@@ -683,16 +683,16 @@
lemma relcompp_distrib2 [simp]: "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
by (fact relcomp_distrib2 [to_pred])
-lemma relcomp_UNION_distrib: "s O UNION I r = (\<Union>i\<in>I. s O r i) "
+lemma relcomp_UNION_distrib: "s O \<Union>(r ` I) = (\<Union>i\<in>I. s O r i) "
by auto
-lemma relcompp_SUP_distrib: "s OO SUPREMUM I r = (\<Squnion>i\<in>I. s OO r i)"
+lemma relcompp_SUP_distrib: "s OO \<Squnion>(r ` I) = (\<Squnion>i\<in>I. s OO r i)"
by (fact relcomp_UNION_distrib [to_pred])
-lemma relcomp_UNION_distrib2: "UNION I r O s = (\<Union>i\<in>I. r i O s) "
+lemma relcomp_UNION_distrib2: "\<Union>(r ` I) O s = (\<Union>i\<in>I. r i O s) "
by auto
-lemma relcompp_SUP_distrib2: "SUPREMUM I r OO s = (\<Squnion>i\<in>I. r i OO s)"
+lemma relcompp_SUP_distrib2: "\<Squnion>(r ` I) OO s = (\<Squnion>i\<in>I. r i OO s)"
by (fact relcomp_UNION_distrib2 [to_pred])
lemma single_valued_relcomp: "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)"
@@ -781,10 +781,10 @@
lemma converse_join: "(r \<squnion> s)\<inverse>\<inverse> = r\<inverse>\<inverse> \<squnion> s\<inverse>\<inverse>"
by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
-lemma converse_INTER: "(INTER S r)\<inverse> = (INT x:S. (r x)\<inverse>)"
+lemma converse_INTER: "(\<Inter>(r ` S))\<inverse> = (\<Inter>x\<in>S. (r x)\<inverse>)"
by fast
-lemma converse_UNION: "(UNION S r)\<inverse> = (UN x:S. (r x)\<inverse>)"
+lemma converse_UNION: "(\<Union>(r ` S))\<inverse> = (\<Union>x\<in>S. (r x)\<inverse>)"
by blast
lemma converse_mono[simp]: "r\<inverse> \<subseteq> s \<inverse> \<longleftrightarrow> r \<subseteq> s"
@@ -1078,17 +1078,17 @@
lemma Image_mono: "r' \<subseteq> r \<Longrightarrow> A' \<subseteq> A \<Longrightarrow> (r' `` A') \<subseteq> (r `` A)"
by blast
-lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))"
+lemma Image_UN: "r `` (\<Union>(B ` A)) = (\<Union>x\<in>A. r `` (B x))"
by blast
lemma UN_Image: "(\<Union>i\<in>I. X i) `` S = (\<Union>i\<in>I. X i `` S)"
by auto
-lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
+lemma Image_INT_subset: "(r `` (\<Inter>(B ` A))) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
by blast
text \<open>Converse inclusion requires some assumptions\<close>
-lemma Image_INT_eq: "single_valued (r\<inverse>) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)"
+lemma Image_INT_eq: "single_valued (r\<inverse>) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> r `` (\<Inter>(B ` A)) = (\<Inter>x\<in>A. r `` B x)"
apply (rule equalityI)
apply (rule Image_INT_subset)
apply (auto simp add: single_valued_def)
--- a/src/HOL/Wellfounded.thy Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Wellfounded.thy Sat Nov 10 07:57:19 2018 +0000
@@ -325,7 +325,7 @@
proof clarify
fix A and a :: "'b"
assume "a \<in> A"
- show "\<exists>z\<in>A. \<forall>y. (y, z) \<in> UNION I r \<longrightarrow> y \<notin> A"
+ show "\<exists>z\<in>A. \<forall>y. (y, z) \<in> \<Union>(r ` I) \<longrightarrow> y \<notin> A"
proof (cases "\<exists>i\<in>I. \<exists>a\<in>A. \<exists>b\<in>A. (b, a) \<in> r i")
case True
then obtain i b c where ibc: "i \<in> I" "b \<in> A" "c \<in> A" "(c,b) \<in> r i"
@@ -344,7 +344,7 @@
lemma wfP_SUP:
"\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow>
- wfP (SUPREMUM UNIV r)"
+ wfP (\<Squnion>(range r))"
by (rule wf_UN[to_pred]) simp_all
lemma wf_Union: