(* Title: HOL/Complete_Lattices.thy
Author: Tobias Nipkow
Author: Lawrence C Paulson
Author: Markus Wenzel
Author: Florian Haftmann
Author: Viorel Preoteasa (Complete Distributive Lattices)
*)
section \<open>Complete lattices\<close>
theory Complete_Lattices
imports Fun
begin
subsection \<open>Syntactic infimum and supremum operations\<close>
class Inf =
fixes Inf :: "'a set \ 'a" ("\")
class Sup =
fixes Sup :: "'a set \ 'a" ("\")
syntax
"_INF1" :: "pttrns \ 'b \ 'b" ("(3INF _./ _)" [0, 10] 10)
"_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3INF _\_./ _)" [0, 0, 10] 10)
"_SUP1" :: "pttrns \ 'b \ 'b" ("(3SUP _./ _)" [0, 10] 10)
"_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3SUP _\_./ _)" [0, 0, 10] 10)
syntax
"_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)
"_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)
"_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)
"_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)
translations
"\x y. f" \ "\x. \y. f"
"\x. f" \ "\(CONST range (\x. f))"
"\x\A. f" \ "CONST Inf ((\x. f) ` A)"
"\x y. f" \ "\x. \y. f"
"\x. f" \ "\(CONST range (\x. f))"
"\x\A. f" \ "CONST Sup ((\x. f) ` A)"
context Inf
begin
lemma INF_image: "\ (g ` f ` A) = \ ((g \ f) ` A)"
by (simp add: image_comp)
lemma INF_identity_eq [simp]: "(\x\A. x) = \A"
by simp
lemma INF_id_eq [simp]: "\(id ` A) = \A"
by simp
lemma INF_cong: "A = B \ (\x. x \ B \ C x = D x) \ \(C ` A) = \(D ` B)"
by (simp add: image_def)
lemma INF_cong_simp:
"A = B \ (\x. x \ B =simp=> C x = D x) \ \(C ` A) = \(D ` B)"
unfolding simp_implies_def by (fact INF_cong)
end
context Sup
begin
lemma SUP_image: "\ (g ` f ` A) = \ ((g \ f) ` A)"
by(fact Inf.INF_image)
lemma SUP_identity_eq [simp]: "(\x\A. x) = \A"
by(fact Inf.INF_identity_eq)
lemma SUP_id_eq [simp]: "\(id ` A) = \A"
by(fact Inf.INF_id_eq)
lemma SUP_cong: "A = B \ (\x. x \ B \ C x = D x) \ \(C ` A) = \(D ` B)"
by (fact Inf.INF_cong)
lemma SUP_cong_simp:
"A = B \ (\x. x \ B =simp=> C x = D x) \ \(C ` A) = \(D ` B)"
by (fact Inf.INF_cong_simp)
end
subsection \<open>Abstract complete lattices\<close>
text \<open>A complete lattice always has a bottom and a top,
so we include them into the following type class,
along with assumptions that define bottom and top
in terms of infimum and supremum.\<close>
class complete_lattice = lattice + Inf + Sup + bot + top +
assumes Inf_lower: "x \ A \ \A \ x"
and Inf_greatest: "(\x. x \ A \ z \ x) \ z \ \A"
and Sup_upper: "x \ A \ x \ \A"
and Sup_least: "(\x. x \ A \ x \ z) \ \A \ z"
and Inf_empty [simp]: "\{} = \"
and Sup_empty [simp]: "\{} = \"
begin
subclass bounded_lattice
proof
fix a
show "\ \ a"
by (auto intro: Sup_least simp only: Sup_empty [symmetric])
show "a \ \"
by (auto intro: Inf_greatest simp only: Inf_empty [symmetric])
qed
lemma dual_complete_lattice: "class.complete_lattice Sup Inf sup (\) (>) inf \ \"
by (auto intro!: class.complete_lattice.intro dual_lattice)
(unfold_locales, (fact Inf_empty Sup_empty Sup_upper Sup_least Inf_lower Inf_greatest)+)
end
context complete_lattice
begin
lemma Sup_eqI:
"(\y. y \ A \ y \ x) \ (\y. (\z. z \ A \ z \ y) \ x \ y) \ \A = x"
by (blast intro: antisym Sup_least Sup_upper)
lemma Inf_eqI:
"(\i. i \ A \ x \ i) \ (\y. (\i. i \ A \ y \ i) \ y \ x) \ \A = x"
by (blast intro: antisym Inf_greatest Inf_lower)
lemma SUP_eqI:
"(\i. i \ A \ f i \ x) \ (\y. (\i. i \ A \ f i \ y) \ x \ y) \ (\i\A. f i) = x"
using Sup_eqI [of "f ` A" x] by auto
lemma INF_eqI:
"(\i. i \ A \ x \ f i) \ (\y. (\i. i \ A \ f i \ y) \ x \ y) \ (\i\A. f i) = x"
using Inf_eqI [of "f ` A" x] by auto
lemma INF_lower: "i \ A \ (\i\A. f i) \ f i"
using Inf_lower [of _ "f ` A"] by simp
lemma INF_greatest: "(\i. i \ A \ u \ f i) \ u \ (\i\A. f i)"
using Inf_greatest [of "f ` A"] by auto
lemma SUP_upper: "i \ A \ f i \ (\i\A. f i)"
using Sup_upper [of _ "f ` A"] by simp
lemma SUP_least: "(\i. i \ A \ f i \ u) \ (\i\A. f i) \ u"
using Sup_least [of "f ` A"] by auto
lemma Inf_lower2: "u \ A \ u \ v \ \A \ v"
using Inf_lower [of u A] by auto
lemma INF_lower2: "i \ A \ f i \ u \ (\i\A. f i) \ u"
using INF_lower [of i A f] by auto
lemma Sup_upper2: "u \ A \ v \ u \ v \ \A"
using Sup_upper [of u A] by auto
lemma SUP_upper2: "i \ A \ u \ f i \ u \ (\i\A. f i)"
using SUP_upper [of i A f] by auto
lemma le_Inf_iff: "b \ \A \ (\a\A. b \ a)"
by (auto intro: Inf_greatest dest: Inf_lower)
lemma le_INF_iff: "u \ (\i\A. f i) \ (\i\A. u \ f i)"
using le_Inf_iff [of _ "f ` A"] by simp
lemma Sup_le_iff: "\A \ b \ (\a\A. a \ b)"
by (auto intro: Sup_least dest: Sup_upper)
lemma SUP_le_iff: "(\i\A. f i) \ u \ (\i\A. f i \ u)"
using Sup_le_iff [of "f ` A"] by simp
lemma Inf_insert [simp]: "\(insert a A) = a \ \A"
by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
lemma INF_insert: "(\x\insert a A. f x) = f a \ \(f ` A)"
by simp
lemma Sup_insert [simp]: "\(insert a A) = a \ \A"
by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
lemma SUP_insert: "(\x\insert a A. f x) = f a \ \(f ` A)"
by simp
lemma INF_empty: "(\x\{}. f x) = \"
by simp
lemma SUP_empty: "(\x\{}. f x) = \"
by simp
lemma Inf_UNIV [simp]: "\UNIV = \"
by (auto intro!: antisym Inf_lower)
lemma Sup_UNIV [simp]: "\UNIV = \"
by (auto intro!: antisym Sup_upper)
lemma Inf_eq_Sup: "\A = \{b. \a \ A. b \ a}"
by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
lemma Sup_eq_Inf: "\A = \{b. \a \ A. a \ b}"
by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
lemma Inf_superset_mono: "B \ A \ \A \ \B"
by (auto intro: Inf_greatest Inf_lower)
lemma Sup_subset_mono: "A \ B \ \A \ \B"
by (auto intro: Sup_least Sup_upper)
lemma Inf_mono:
assumes "\b. b \ B \ \a\A. a \ b"
shows "\A \ \B"
proof (rule Inf_greatest)
fix b assume "b \ B"
with assms obtain a where "a \ A" and "a \ b" by blast
from \<open>a \<in> A\<close> have "\<Sqinter>A \<le> a" by (rule Inf_lower)
with \<open>a \<le> b\<close> show "\<Sqinter>A \<le> b" by auto
qed
lemma INF_mono: "(\m. m \ B \ \n\A. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)"
using Inf_mono [of "g ` B" "f ` A"] by auto
lemma INF_mono': "(\x. f x \ g x) \ (\x\A. f x) \ (\x\A. g x)"
by (rule INF_mono) auto
lemma Sup_mono:
assumes "\a. a \ A \ \b\B. a \ b"
shows "\A \ \B"
proof (rule Sup_least)
fix a assume "a \ A"
with assms obtain b where "b \ B" and "a \ b" by blast
from \<open>b \<in> B\<close> have "b \<le> \<Squnion>B" by (rule Sup_upper)
with \<open>a \<le> b\<close> show "a \<le> \<Squnion>B" by auto
qed
lemma SUP_mono: "(\n. n \ A \ \m\B. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)"
using Sup_mono [of "f ` A" "g ` B"] by auto
lemma SUP_mono': "(\x. f x \ g x) \ (\x\A. f x) \ (\x\A. g x)"
by (rule SUP_mono) auto
lemma INF_superset_mono: "B \ A \ (\x. x \ B \ f x \ g x) \ (\x\A. f x) \ (\x\B. g x)"
\<comment> \<open>The last inclusion is POSITIVE!\<close>
by (blast intro: INF_mono dest: subsetD)
lemma SUP_subset_mono: "A \ B \ (\x. x \ A \ f x \ g x) \ (\x\A. f x) \ (\x\B. g x)"
by (blast intro: SUP_mono dest: subsetD)
lemma Inf_less_eq:
assumes "\v. v \ A \ v \ u"
and "A \ {}"
shows "\A \ u"
proof -
from \<open>A \<noteq> {}\<close> obtain v where "v \<in> A" by blast
moreover from \<open>v \<in> A\<close> assms(1) have "v \<le> u" by blast
ultimately show ?thesis by (rule Inf_lower2)
qed
lemma less_eq_Sup:
assumes "\v. v \ A \ u \ v"
and "A \ {}"
shows "u \ \A"
proof -
from \<open>A \<noteq> {}\<close> obtain v where "v \<in> A" by blast
moreover from \<open>v \<in> A\<close> assms(1) have "u \<le> v" by blast
ultimately show ?thesis by (rule Sup_upper2)
qed
lemma INF_eq:
assumes "\i. i \ A \ \j\B. f i \ g j"
and "\j. j \ B \ \i\A. g j \ f i"
shows "\(f ` A) = \(g ` B)"
by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
lemma SUP_eq:
assumes "\i. i \ A \ \j\B. f i \ g j"
and "\j. j \ B \ \i\A. g j \ f i"
shows "\(f ` A) = \(g ` B)"
by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
lemma less_eq_Inf_inter: "\A \ \B \ \(A \ B)"
by (auto intro: Inf_greatest Inf_lower)
lemma Sup_inter_less_eq: "\(A \ B) \ \A \ \B "
by (auto intro: Sup_least Sup_upper)
lemma Inf_union_distrib: "\(A \ B) = \A \ \B"
by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
lemma INF_union: "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)"
by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower)
lemma Sup_union_distrib: "\(A \ B) = \A \ \B"
by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
lemma SUP_union: "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)"
by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper)
lemma INF_inf_distrib: "(\a\A. f a) \ (\a\A. g a) = (\a\A. f a \ g a)"
by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono)
lemma SUP_sup_distrib: "(\a\A. f a) \ (\a\A. g a) = (\a\A. f a \ g a)"
(is "?L = ?R")
proof (rule antisym)
show "?L \ ?R"
by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
show "?R \ ?L"
by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper)
qed
lemma Inf_top_conv [simp]:
"\A = \ \ (\x\A. x = \)"
"\ = \A \ (\x\A. x = \)"
proof -
show "\A = \ \ (\x\A. x = \)"
proof
assume "\x\A. x = \"
then have "A = {} \ A = {\}" by auto
then show "\A = \" by auto
next
assume "\A = \"
show "\x\A. x = \"
proof (rule ccontr)
assume "\ (\x\A. x = \)"
then obtain x where "x \ A" and "x \ \" by blast
then obtain B where "A = insert x B" by blast
with \<open>\<Sqinter>A = \<top>\<close> \<open>x \<noteq> \<top>\<close> show False by simp
qed
qed
then show "\ = \A \ (\x\A. x = \)" by auto
qed
lemma INF_top_conv [simp]:
"(\x\A. B x) = \ \ (\x\A. B x = \)"
"\ = (\x\A. B x) \ (\x\A. B x = \)"
using Inf_top_conv [of "B ` A"] by simp_all
lemma Sup_bot_conv [simp]:
"\A = \ \ (\x\A. x = \)"
"\ = \A \ (\x\A. x = \)"
using dual_complete_lattice
by (rule complete_lattice.Inf_top_conv)+
lemma SUP_bot_conv [simp]:
"(\x\A. B x) = \ \ (\x\A. B x = \)"
"\ = (\x\A. B x) \ (\x\A. B x = \)"
using Sup_bot_conv [of "B ` A"] by simp_all
lemma INF_const [simp]: "A \ {} \ (\i\A. f) = f"
by (auto intro: antisym INF_lower INF_greatest)
lemma SUP_const [simp]: "A \ {} \ (\i\A. f) = f"
by (auto intro: antisym SUP_upper SUP_least)
lemma INF_top [simp]: "(\x\A. \) = \"
by (cases "A = {}") simp_all
lemma SUP_bot [simp]: "(\x\A. \) = \"
by (cases "A = {}") simp_all
lemma INF_commute: "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)"
by (iprover intro: INF_lower INF_greatest order_trans antisym)
lemma SUP_commute: "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)"
by (iprover intro: SUP_upper SUP_least order_trans antisym)
lemma INF_absorb:
assumes "k \ I"
shows "A k \ (\i\I. A i) = (\i\I. A i)"
proof -
from assms obtain J where "I = insert k J" by blast
then show ?thesis by simp
qed
lemma SUP_absorb:
assumes "k \ I"
shows "A k \ (\i\I. A i) = (\i\I. A i)"
proof -
from assms obtain J where "I = insert k J" by blast
then show ?thesis by simp
qed
lemma INF_inf_const1: "I \ {} \ (\i\I. inf x (f i)) = inf x (\i\I. f i)"
by (intro antisym INF_greatest inf_mono order_refl INF_lower)
(auto intro: INF_lower2 le_infI2 intro!: INF_mono)
lemma INF_inf_const2: "I \ {} \ (\i\I. inf (f i) x) = inf (\i\I. f i) x"
using INF_inf_const1[of I x f] by (simp add: inf_commute)
lemma INF_constant: "(\y\A. c) = (if A = {} then \ else c)"
by simp
lemma SUP_constant: "(\y\A. c) = (if A = {} then \ else c)"
by simp
lemma less_INF_D:
assumes "y < (\i\A. f i)" "i \ A"
shows "y < f i"
proof -
note \<open>y < (\<Sqinter>i\<in>A. f i)\<close>
also have "(\i\A. f i) \ f i" using \i \ A\
by (rule INF_lower)
finally show "y < f i" .
qed
lemma SUP_lessD:
assumes "(\i\A. f i) < y" "i \ A"
shows "f i < y"
proof -
have "f i \ (\i\A. f i)"
using \<open>i \<in> A\<close> by (rule SUP_upper)
also note \<open>(\<Squnion>i\<in>A. f i) < y\<close>
finally show "f i < y" .
qed
lemma INF_UNIV_bool_expand: "(\b. A b) = A True \ A False"
by (simp add: UNIV_bool inf_commute)
lemma SUP_UNIV_bool_expand: "(\b. A b) = A True \ A False"
by (simp add: UNIV_bool sup_commute)
lemma Inf_le_Sup: "A \ {} \ Inf A \ Sup A"
by (blast intro: Sup_upper2 Inf_lower ex_in_conv)
lemma INF_le_SUP: "A \ {} \ \(f ` A) \ \(f ` A)"
using Inf_le_Sup [of "f ` A"] by simp
lemma INF_eq_const: "I \ {} \ (\i. i \ I \ f i = x) \ \(f ` I) = x"
by (auto intro: INF_eqI)
lemma SUP_eq_const: "I \ {} \ (\i. i \ I \ f i = x) \ \(f ` I) = x"
by (auto intro: SUP_eqI)
lemma INF_eq_iff: "I \ {} \ (\i. i \ I \ f i \ c) \ \(f ` I) = c \ (\i\I. f i = c)"
by (auto intro: INF_eq_const INF_lower antisym)
lemma SUP_eq_iff: "I \ {} \ (\i. i \ I \ c \ f i) \ \(f ` I) = c \ (\i\I. f i = c)"
by (auto intro: SUP_eq_const SUP_upper antisym)
end
context complete_lattice
begin
lemma Sup_Inf_le: "Sup (Inf ` {f ` A | f . (\ Y \ A . f Y \ Y)}) \ Inf (Sup ` A)"
by (rule SUP_least, clarify, rule INF_greatest, simp add: INF_lower2 Sup_upper)
end
class complete_distrib_lattice = complete_lattice +
assumes Inf_Sup_le: "Inf (Sup ` A) \ Sup (Inf ` {f ` A | f . (\ Y \ A . f Y \ Y)})"
begin
lemma Inf_Sup: "Inf (Sup ` A) = Sup (Inf ` {f ` A | f . (\ Y \ A . f Y \ Y)})"
by (rule antisym, rule Inf_Sup_le, rule Sup_Inf_le)
subclass distrib_lattice
proof
fix a b c
show "a \ b \ c = (a \ b) \ (a \ c)"
proof (rule antisym, simp_all, safe)
show "b \ c \ a \ b"
by (rule le_infI1, simp)
show "b \ c \ a \ c"
by (rule le_infI2, simp)
have [simp]: "a \ c \ a \ b \ c"
by (rule le_infI1, simp)
have [simp]: "b \ a \ a \ b \ c"
by (rule le_infI2, simp)
have "\(Sup ` {{a, b}, {a, c}}) =
\<Squnion>(Inf ` {f ` {{a, b}, {a, c}} | f. \<forall>Y\<in>{{a, b}, {a, c}}. f Y \<in> Y})"
by (rule Inf_Sup)
from this show "(a \ b) \ (a \ c) \ a \ b \ c"
apply simp
by (rule SUP_least, safe, simp_all)
qed
qed
end
context complete_lattice
begin
context
fixes f :: "'a \ 'b::complete_lattice"
assumes "mono f"
begin
lemma mono_Inf: "f (\A) \ (\x\A. f x)"
using \<open>mono f\<close> by (auto intro: complete_lattice_class.INF_greatest Inf_lower dest: monoD)
lemma mono_Sup: "(\x\A. f x) \ f (\A)"
using \<open>mono f\<close> by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD)
lemma mono_INF: "f (\i\I. A i) \ (\x\I. f (A x))"
by (intro complete_lattice_class.INF_greatest monoD[OF \<open>mono f\<close>] INF_lower)
lemma mono_SUP: "(\x\I. f (A x)) \ f (\i\I. A i)"
by (intro complete_lattice_class.SUP_least monoD[OF \<open>mono f\<close>] SUP_upper)
end
end
class complete_boolean_algebra = boolean_algebra + complete_distrib_lattice
begin
lemma uminus_Inf: "- (\A) = \(uminus ` A)"
proof (rule antisym)
show "- \A \ \(uminus ` A)"
by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp
show "\(uminus ` A) \ - \A"
by (rule Sup_least, rule compl_le_swap1, rule Inf_lower) auto
qed
lemma uminus_INF: "- (\x\A. B x) = (\x\A. - B x)"
by (simp add: uminus_Inf image_image)
lemma uminus_Sup: "- (\A) = \(uminus ` A)"
proof -
have "\A = - \(uminus ` A)"
by (simp add: image_image uminus_INF)
then show ?thesis by simp
qed
lemma uminus_SUP: "- (\x\A. B x) = (\x\A. - B x)"
by (simp add: uminus_Sup image_image)
end
class complete_linorder = linorder + complete_lattice
begin
lemma dual_complete_linorder:
"class.complete_linorder Sup Inf sup (\) (>) inf \ \"
by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
lemma complete_linorder_inf_min: "inf = min"
by (auto intro: antisym simp add: min_def fun_eq_iff)
lemma complete_linorder_sup_max: "sup = max"
by (auto intro: antisym simp add: max_def fun_eq_iff)
lemma Inf_less_iff: "\S < a \ (\x\S. x < a)"
by (simp add: not_le [symmetric] le_Inf_iff)
lemma INF_less_iff: "(\i\A. f i) < a \ (\x\A. f x < a)"
by (simp add: Inf_less_iff [of "f ` A"])
lemma less_Sup_iff: "a < \S \ (\x\S. a < x)"
by (simp add: not_le [symmetric] Sup_le_iff)
lemma less_SUP_iff: "a < (\i\A. f i) \ (\x\A. a < f x)"
by (simp add: less_Sup_iff [of _ "f ` A"])
lemma Sup_eq_top_iff [simp]: "\A = \ \ (\x<\. \i\A. x < i)"
proof
assume *: "\A = \"
show "(\x<\. \i\A. x < i)"
unfolding * [symmetric]
proof (intro allI impI)
fix x
assume "x < \A"
then show "\i\A. x < i"
by (simp add: less_Sup_iff)
qed
next
assume *: "\x<\. \i\A. x < i"
show "\A = \"
proof (rule ccontr)
assume "\A \ \"
with top_greatest [of "\A"] have "\A < \"
unfolding le_less by auto
with * have "\A < \A"
unfolding less_Sup_iff by auto
then show False by auto
qed
qed
lemma SUP_eq_top_iff [simp]: "(\i\A. f i) = \ \ (\x<\. \i\A. x < f i)"
using Sup_eq_top_iff [of "f ` A"] by simp
lemma Inf_eq_bot_iff [simp]: "\A = \ \ (\x>\. \i\A. i < x)"
using dual_complete_linorder
by (rule complete_linorder.Sup_eq_top_iff)
lemma INF_eq_bot_iff [simp]: "(\i\A. f i) = \ \ (\x>\. \i\A. f i < x)"
using Inf_eq_bot_iff [of "f ` A"] by simp
lemma Inf_le_iff: "\A \ x \ (\y>x. \a\A. y > a)"
proof safe
fix y
assume "x \ \A" "y > x"
then have "y > \A" by auto
then show "\a\A. y > a"
unfolding Inf_less_iff .
qed (auto elim!: allE[of _ "\A"] simp add: not_le[symmetric] Inf_lower)
lemma INF_le_iff: "\(f ` A) \ x \ (\y>x. \i\A. y > f i)"
using Inf_le_iff [of "f ` A"] by simp
lemma le_Sup_iff: "x \ \A \ (\ya\A. y < a)"
proof safe
fix y
assume "x \ \A" "y < x"
then have "y < \A" by auto
then show "\a\A. y < a"
unfolding less_Sup_iff .
qed (auto elim!: allE[of _ "\A"] simp add: not_le[symmetric] Sup_upper)
lemma le_SUP_iff: "x \ \(f ` A) \ (\yi\A. y < f i)"
using le_Sup_iff [of _ "f ` A"] by simp
end
subsection \<open>Complete lattice on \<^typ>\<open>bool\<close>\<close>
instantiation bool :: complete_lattice
begin
definition [simp, code]: "\A \ False \ A"
definition [simp, code]: "\A \ True \ A"
instance
by standard (auto intro: bool_induct)
end
lemma not_False_in_image_Ball [simp]: "False \ P ` A \ Ball A P"
by auto
lemma True_in_image_Bex [simp]: "True \ P ` A \ Bex A P"
by auto
lemma INF_bool_eq [simp]: "(\A f. \(f ` A)) = Ball"
by (simp add: fun_eq_iff)
lemma SUP_bool_eq [simp]: "(\A f. \(f ` A)) = Bex"
by (simp add: fun_eq_iff)
instance bool :: complete_boolean_algebra
by (standard, fastforce)
subsection \<open>Complete lattice on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close>
instantiation "fun" :: (type, Inf) Inf
begin
definition "\A = (\x. \f\A. f x)"
lemma Inf_apply [simp, code]: "(\A) x = (\f\A. f x)"
by (simp add: Inf_fun_def)
instance ..
end
instantiation "fun" :: (type, Sup) Sup
begin
definition "\A = (\x. \f\A. f x)"
lemma Sup_apply [simp, code]: "(\A) x = (\f\A. f x)"
by (simp add: Sup_fun_def)
instance ..
end
instantiation "fun" :: (type, complete_lattice) complete_lattice
begin
instance
by standard (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)
end
lemma INF_apply [simp]: "(\y\A. f y) x = (\y\A. f y x)"
by (simp add: image_comp)
lemma SUP_apply [simp]: "(\y\A. f y) x = (\y\A. f y x)"
by (simp add: image_comp)
subsection \<open>Complete lattice on unary and binary predicates\<close>
lemma Inf1_I: "(\P. P \ A \ P a) \ (\A) a"
by auto
lemma INF1_I: "(\x. x \ A \ B x b) \ (\x\A. B x) b"
by simp
lemma INF2_I: "(\x. x \ A \ B x b c) \ (\x\A. B x) b c"
by simp
lemma Inf2_I: "(\r. r \ A \ r a b) \ (\A) a b"
by auto
lemma Inf1_D: "(\A) a \ P \ A \ P a"
by auto
lemma INF1_D: "(\x\A. B x) b \ a \ A \ B a b"
by simp
lemma Inf2_D: "(\A) a b \ r \ A \ r a b"
by auto
lemma INF2_D: "(\x\A. B x) b c \ a \ A \ B a b c"
by simp
lemma Inf1_E:
assumes "(\A) a"
obtains "P a" | "P \ A"
using assms by auto
lemma INF1_E:
assumes "(\x\A. B x) b"
obtains "B a b" | "a \ A"
using assms by auto
lemma Inf2_E:
assumes "(\A) a b"
obtains "r a b" | "r \ A"
using assms by auto
lemma INF2_E:
assumes "(\x\A. B x) b c"
obtains "B a b c" | "a \ A"
using assms by auto
lemma Sup1_I: "P \ A \ P a \ (\A) a"
by auto
lemma SUP1_I: "a \ A \ B a b \ (\x\A. B x) b"
by auto
lemma Sup2_I: "r \ A \ r a b \ (\A) a b"
by auto
lemma SUP2_I: "a \ A \ B a b c \ (\x\A. B x) b c"
by auto
lemma Sup1_E:
assumes "(\A) a"
obtains P where "P \ A" and "P a"
using assms by auto
lemma SUP1_E:
assumes "(\x\A. B x) b"
obtains x where "x \ A" and "B x b"
using assms by auto
lemma Sup2_E:
assumes "(\A) a b"
obtains r where "r \ A" "r a b"
using assms by auto
lemma SUP2_E:
assumes "(\x\A. B x) b c"
obtains x where "x \ A" "B x b c"
using assms by auto
subsection \<open>Complete lattice on \<^typ>\<open>_ set\<close>\<close>
instantiation "set" :: (type) complete_lattice
begin
definition "\A = {x. \((\B. x \ B) ` A)}"
definition "\A = {x. \((\B. x \ B) ` A)}"
instance
by standard (auto simp add: less_eq_set_def Inf_set_def Sup_set_def le_fun_def)
end
subsubsection \<open>Inter\<close>
abbreviation Inter :: "'a set set \ 'a set" ("\")
where "\S \ \S"
lemma Inter_eq: "\A = {x. \B \ A. x \ B}"
proof (rule set_eqI)
fix x
have "(\Q\{P. \B\A. P \ x \ B}. Q) \ (\B\A. x \ B)"
by auto
then show "x \ \A \ x \ {x. \B \ A. x \ B}"
by (simp add: Inf_set_def image_def)
qed
lemma Inter_iff [simp]: "A \ \C \ (\X\C. A \ X)"
by (unfold Inter_eq) blast
lemma InterI [intro!]: "(\X. X \ C \ A \ X) \ A \ \C"
by (simp add: Inter_eq)
text \<open>
\<^medskip> A ``destruct'' rule -- every \<^term>\<open>X\<close> in \<^term>\<open>C\<close>
contains \<^term>\<open>A\<close> as an element, but \<^prop>\<open>A \<in> X\<close> can hold when
\<^prop>\<open>X \<in> C\<close> does not! This rule is analogous to \<open>spec\<close>.
\<close>
lemma InterD [elim, Pure.elim]: "A \ \C \ X \ C \ A \ X"
by auto
lemma InterE [elim]: "A \ \C \ (X \ C \ R) \ (A \ X \ R) \ R"
\<comment> \<open>``Classical'' elimination rule -- does not require proving
\<^prop>\<open>X \<in> C\<close>.\<close>
unfolding Inter_eq by blast
lemma Inter_lower: "B \ A \ \A \ B"
by (fact Inf_lower)
lemma Inter_subset: "(\X. X \ A \ X \ B) \ A \ {} \ \A \ B"
by (fact Inf_less_eq)
lemma Inter_greatest: "(\X. X \ A \ C \ X) \ C \ \A"
by (fact Inf_greatest)
lemma Inter_empty: "\{} = UNIV"
by (fact Inf_empty) (* already simp *)
lemma Inter_UNIV: "\UNIV = {}"
by (fact Inf_UNIV) (* already simp *)
lemma Inter_insert: "\(insert a B) = a \ \B"
by (fact Inf_insert) (* already simp *)
lemma Inter_Un_subset: "\A \ \B \ \(A \ B)"
by (fact less_eq_Inf_inter)
lemma Inter_Un_distrib: "\(A \ B) = \A \ \B"
by (fact Inf_union_distrib)
lemma Inter_UNIV_conv [simp]:
"\A = UNIV \ (\x\A. x = UNIV)"
"UNIV = \A \ (\x\A. x = UNIV)"
by (fact Inf_top_conv)+
lemma Inter_anti_mono: "B \ A \ \A \ \B"
by (fact Inf_superset_mono)
subsubsection \<open>Intersections of families\<close>
syntax (ASCII)
"_INTER1" :: "pttrns \ 'b set \ 'b set" ("(3INT _./ _)" [0, 10] 10)
"_INTER" :: "pttrn \ 'a set \ 'b set \ 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10)
syntax
"_INTER1" :: "pttrns \ 'b set \ 'b set" ("(3\_./ _)" [0, 10] 10)
"_INTER" :: "pttrn \ 'a set \ 'b set \ 'b set" ("(3\_\_./ _)" [0, 0, 10] 10)
syntax (latex output)
"_INTER1" :: "pttrns \ 'b set \ 'b set" ("(3\(\unbreakable\\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
"_INTER" :: "pttrn \ 'a set \ 'b set \ 'b set" ("(3\(\unbreakable\\<^bsub>_\_\<^esub>)/ _)" [0, 0, 10] 10)
translations
"\x y. f" \ "\x. \y. f"
"\x. f" \ "\(CONST range (\x. f))"
"\x\A. f" \ "CONST Inter ((\x. f) ` A)"
lemma INTER_eq: "(\x\A. B x) = {y. \x\A. y \ B x}"
by (auto intro!: INF_eqI)
lemma INT_iff [simp]: "b \ (\x\A. B x) \ (\x\A. b \ B x)"
using Inter_iff [of _ "B ` A"] by simp
lemma INT_I [intro!]: "(\x. x \ A \ b \ B x) \ b \ (\x\A. B x)"
by auto
lemma INT_D [elim, Pure.elim]: "b \ (\x\A. B x) \ a \ A \ b \ B a"
by auto
lemma INT_E [elim]: "b \ (\x\A. B x) \ (b \ B a \ R) \ (a \ A \ R) \ R"
\<comment> \<open>"Classical" elimination -- by the Excluded Middle on \<^prop>\<open>a\<in>A\<close>.\<close>
by auto
lemma Collect_ball_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})"
by blast
lemma Collect_all_eq: "{x. \y. P x y} = (\y. {x. P x y})"
by blast
lemma INT_lower: "a \ A \ (\x\A. B x) \ B a"
by (fact INF_lower)
lemma INT_greatest: "(\x. x \ A \ C \ B x) \ C \ (\x\A. B x)"
by (fact INF_greatest)
lemma INT_empty: "(\x\{}. B x) = UNIV"
by (fact INF_empty)
lemma INT_absorb: "k \ I \ A k \ (\i\I. A i) = (\i\I. A i)"
by (fact INF_absorb)
lemma INT_subset_iff: "B \ (\i\I. A i) \ (\i\I. B \ A i)"
by (fact le_INF_iff)
lemma INT_insert [simp]: "(\x \ insert a A. B x) = B a \ \ (B ` A)"
by (fact INF_insert)
lemma INT_Un: "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)"
by (fact INF_union)
lemma INT_insert_distrib: "u \ A \ (\x\A. insert a (B x)) = insert a (\x\A. B x)"
by blast
lemma INT_constant [simp]: "(\y\A. c) = (if A = {} then UNIV else c)"
by (fact INF_constant)
lemma INTER_UNIV_conv:
"(UNIV = (\x\A. B x)) = (\x\A. B x = UNIV)"
"((\x\A. B x) = UNIV) = (\x\A. B x = UNIV)"
by (fact INF_top_conv)+ (* already simp *)
lemma INT_bool_eq: "(\b. A b) = A True \ A False"
by (fact INF_UNIV_bool_expand)
lemma INT_anti_mono: "A \ B \ (\x. x \ A \ f x \ g x) \ (\x\B. f x) \ (\x\A. g x)"
\<comment> \<open>The last inclusion is POSITIVE!\<close>
by (fact INF_superset_mono)
lemma Pow_INT_eq: "Pow (\x\A. B x) = (\x\A. Pow (B x))"
by blast
lemma vimage_INT: "f -` (\x\A. B x) = (\x\A. f -` B x)"
by blast
subsubsection \<open>Union\<close>
abbreviation Union :: "'a set set \ 'a set" ("\")
where "\S \ \S"
lemma Union_eq: "\A = {x. \B \ A. x \ B}"
proof (rule set_eqI)
fix x
have "(\Q\{P. \B\A. P \ x \ B}. Q) \ (\B\A. x \ B)"
by auto
then show "x \ \A \ x \ {x. \B\A. x \ B}"
by (simp add: Sup_set_def image_def)
qed
lemma Union_iff [simp]: "A \ \C \ (\X\C. A\X)"
by (unfold Union_eq) blast
lemma UnionI [intro]: "X \ C \ A \ X \ A \ \C"
\<comment> \<open>The order of the premises presupposes that \<^term>\<open>C\<close> is rigid;
\<^term>\<open>A\<close> may be flexible.\<close>
by auto
lemma UnionE [elim!]: "A \ \C \ (\X. A \ X \ X \ C \ R) \ R"
by auto
lemma Union_upper: "B \ A \ B \ \A"
by (fact Sup_upper)
lemma Union_least: "(\X. X \ A \ X \ C) \ \A \ C"
by (fact Sup_least)
lemma Union_empty: "\{} = {}"
by (fact Sup_empty) (* already simp *)
lemma Union_UNIV: "\UNIV = UNIV"
by (fact Sup_UNIV) (* already simp *)
lemma Union_insert: "\(insert a B) = a \ \B"
by (fact Sup_insert) (* already simp *)
lemma Union_Un_distrib [simp]: "\(A \ B) = \A \ \B"
by (fact Sup_union_distrib)
lemma Union_Int_subset: "\(A \ B) \ \A \ \B"
by (fact Sup_inter_less_eq)
lemma Union_empty_conv: "(\A = {}) \ (\x\A. x = {})"
by (fact Sup_bot_conv) (* already simp *)
lemma empty_Union_conv: "({} = \A) \ (\x\A. x = {})"
by (fact Sup_bot_conv) (* already simp *)
lemma subset_Pow_Union: "A \ Pow (\A)"
by blast
lemma Union_Pow_eq [simp]: "\(Pow A) = A"
by blast
lemma Union_mono: "A \ B \ \A \ \B"
by (fact Sup_subset_mono)
lemma Union_subsetI: "(\x. x \ A \ \y. y \ B \ x \ y) \ \A \ \B"
by blast
lemma disjnt_inj_on_iff:
"\inj_on f (\\); X \ \; Y \ \\ \ disjnt (f ` X) (f ` Y) \ disjnt X Y"
apply (auto simp: disjnt_def)
using inj_on_eq_iff by fastforce
lemma disjnt_Union1 [simp]: "disjnt (\\) B \ (\A \ \. disjnt A B)"
by (auto simp: disjnt_def)
lemma disjnt_Union2 [simp]: "disjnt B (\\) \ (\A \ \. disjnt B A)"
by (auto simp: disjnt_def)
subsubsection \<open>Unions of families\<close>
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)
syntax
"_UNION1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" [0, 10] 10)
"_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10)
syntax (latex output)
"_UNION1" :: "pttrns => 'b set => 'b set" ("(3\(\unbreakable\\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
"_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(\unbreakable\\<^bsub>_\_\<^esub>)/ _)" [0, 0, 10] 10)
translations
"\x y. f" \ "\x. \y. f"
"\x. f" \ "\(CONST range (\x. f))"
"\x\A. f" \ "CONST Union ((\x. f) ` A)"
text \<open>
Note the difference between ordinary syntax of indexed
unions and intersections (e.g.\ \<open>\<Union>a\<^sub>1\<in>A\<^sub>1. B\<close>)
and their \LaTeX\ rendition: \<^term>\<open>\<Union>a\<^sub>1\<in>A\<^sub>1. B\<close>.
\<close>
lemma disjoint_UN_iff: "disjnt A (\i\I. B i) \ (\i\I. disjnt A (B i))"
by (auto simp: disjnt_def)
lemma UNION_eq: "(\x\A. B x) = {y. \x\A. y \ B x}"
by (auto intro!: SUP_eqI)
lemma bind_UNION [code]: "Set.bind A f = \(f ` A)"
by (simp add: bind_def UNION_eq)
lemma member_bind [simp]: "x \ Set.bind A f \ x \ \(f ` A)"
by (simp add: bind_UNION)
lemma Union_SetCompr_eq: "\{f x| x. P x} = {a. \x. P x \ a \ f x}"
by blast
lemma UN_iff [simp]: "b \ (\x\A. B x) \ (\x\A. b \ B x)"
using Union_iff [of _ "B ` A"] by simp
lemma UN_I [intro]: "a \ A \ b \ B a \ b \ (\x\A. B x)"
\<comment> \<open>The order of the premises presupposes that \<^term>\<open>A\<close> is rigid;
\<^term>\<open>b\<close> may be flexible.\<close>
by auto
lemma UN_E [elim!]: "b \ (\x\A. B x) \ (\x. x\A \ b \ B x \ R) \ R"
by auto
lemma UN_upper: "a \ A \ B a \ (\x\A. B x)"
by (fact SUP_upper)
lemma UN_least: "(\x. x \ A \ B x \ C) \ (\x\A. B x) \ C"
by (fact SUP_least)
lemma Collect_bex_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})"
by blast
lemma UN_insert_distrib: "u \ A \ (\x\A. insert a (B x)) = insert a (\x\A. B x)"
by blast
lemma UN_empty: "(\x\{}. B x) = {}"
by (fact SUP_empty)
lemma UN_empty2: "(\x\A. {}) = {}"
by (fact SUP_bot) (* already simp *)
lemma UN_absorb: "k \ I \ A k \ (\i\I. A i) = (\i\I. A i)"
by (fact SUP_absorb)
lemma UN_insert [simp]: "(\x\insert a A. B x) = B a \ \(B ` A)"
by (fact SUP_insert)
lemma UN_Un [simp]: "(\i \ A \ B. M i) = (\i\A. M i) \ (\i\B. M i)"
by (fact SUP_union)
lemma UN_UN_flatten: "(\x \ (\y\A. B y). C x) = (\y\A. \x\B y. C x)"
by blast
lemma UN_subset_iff: "((\i\I. A i) \ B) = (\i\I. A i \ B)"
by (fact SUP_le_iff)
lemma UN_constant [simp]: "(\y\A. c) = (if A = {} then {} else c)"
by (fact SUP_constant)
lemma UNION_singleton_eq_range: "(\x\A. {f x}) = f ` A"
by blast
lemma image_Union: "f ` \S = (\x\S. f ` x)"
by blast
lemma UNION_empty_conv:
"{} = (\x\A. B x) \ (\x\A. B x = {})"
"(\x\A. B x) = {} \ (\x\A. B x = {})"
by (fact SUP_bot_conv)+ (* already simp *)
lemma Collect_ex_eq: "{x. \y. P x y} = (\y. {x. P x y})"
by blast
lemma ball_UN: "(\z \ \(B ` A). P z) \ (\x\A. \z \ B x. P z)"
by blast
lemma bex_UN: "(\z \ \(B ` A). P z) \ (\x\A. \z\B x. P z)"
by blast
lemma Un_eq_UN: "A \ B = (\b. if b then A else B)"
by safe (auto simp add: if_split_mem2)
lemma UN_bool_eq: "(\b. A b) = (A True \ A False)"
by (fact SUP_UNIV_bool_expand)
lemma UN_Pow_subset: "(\x\A. Pow (B x)) \ Pow (\x\A. B x)"
by blast
lemma UN_mono:
"A \ B \ (\x. x \ A \ f x \ g x) \
(\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
by (fact SUP_subset_mono)
lemma vimage_Union: "f -` (\A) = (\X\A. f -` X)"
by blast
lemma vimage_UN: "f -` (\x\A. B x) = (\x\A. f -` B x)"
by blast
lemma vimage_eq_UN: "f -` B = (\y\B. f -` {y})"
\<comment> \<open>NOT suitable for rewriting\<close>
by blast
lemma image_UN: "f ` \(B ` A) = (\x\A. f ` B x)"
by blast
lemma UN_singleton [simp]: "(\x\A. {x}) = A"
by blast
lemma inj_on_image: "inj_on f (\A) \ inj_on ((`) f) A"
unfolding inj_on_def by blast
subsubsection \<open>Distributive laws\<close>
lemma Int_Union: "A \ \B = (\C\B. A \ C)"
by blast
lemma Un_Inter: "A \ \B = (\C\B. A \ C)"
by blast
lemma Int_Union2: "\B \ A = (\C\B. C \ A)"
by blast
lemma INT_Int_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)"
by (rule sym) (rule INF_inf_distrib)
lemma UN_Un_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)"
by (rule sym) (rule SUP_sup_distrib)
lemma Int_Inter_image: "(\x\C. A x \ B x) = \(A ` C) \ \(B ` C)" (* FIXME drop *)
by (simp add: INT_Int_distrib)
lemma Int_Inter_eq: "A \ \\ = (if \={} then A else (\B\\. A \ B))"
"\\ \ A = (if \={} then A else (\B\\. B \ A))"
by auto
lemma Un_Union_image: "(\x\C. A x \ B x) = \(A ` C) \ \(B ` C)" (* FIXME drop *)
\<comment> \<open>Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:\<close>
\<comment> \<open>Union of a family of unions\<close>
by (simp add: UN_Un_distrib)
lemma Un_INT_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)"
by blast
lemma Int_UN_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)"
\<comment> \<open>Halmos, Naive Set Theory, page 35.\<close>
by blast
lemma Int_UN_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)"
by blast
lemma Un_INT_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)"
by blast
lemma Union_disjoint: "(\C \ A = {}) \ (\B\C. B \ A = {})"
by blast
lemma SUP_UNION: "(\x\(\y\A. g y). f x) = (\y\A. \x\g y. f x :: _ :: complete_lattice)"
by (rule order_antisym) (blast intro: SUP_least SUP_upper2)+
subsection \<open>Injections and bijections\<close>
lemma inj_on_Inter: "S \ {} \ (\A. A \ S \ inj_on f A) \ inj_on f (\S)"
unfolding inj_on_def by blast
lemma inj_on_INTER: "I \ {} \ (\i. i \ I \ inj_on f (A i)) \ inj_on f (\i \ I. A i)"
unfolding inj_on_def by safe simp
lemma inj_on_UNION_chain:
assumes chain: "\i j. i \ I \ j \ I \ A i \ A j \ A j \ A i"
and inj: "\i. i \ I \ inj_on f (A i)"
shows "inj_on f (\i \ I. A i)"
proof -
have "x = y"
if *: "i \ I" "j \ I"
and **: "x \ A i" "y \ A j"
and ***: "f x = f y"
for i j x y
using chain [OF *]
proof
assume "A i \ A j"
with ** have "x \ A j" by auto
with inj * ** *** show ?thesis
by (auto simp add: inj_on_def)
next
assume "A j \ A i"
with ** have "y \ A i" by auto
with inj * ** *** show ?thesis
by (auto simp add: inj_on_def)
qed
then show ?thesis
by (unfold inj_on_def UNION_eq) auto
qed
lemma bij_betw_UNION_chain:
assumes chain: "\i j. i \ I \ j \ I \ A i \ A j \ A j \ A i"
and bij: "\i. i \ I \ bij_betw f (A i) (A' i)"
shows "bij_betw f (\i \ I. A i) (\i \ I. A' i)"
unfolding bij_betw_def
proof safe
have "\i. i \ I \ inj_on f (A i)"
using bij bij_betw_def[of f] by auto
then show "inj_on f (\(A ` I))"
using chain inj_on_UNION_chain[of I A f] by auto
next
fix i x
assume *: "i \ I" "x \ A i"
with bij have "f x \ A' i"
by (auto simp: bij_betw_def)
with * show "f x \ \(A' ` I)" by blast
next
fix i x'
assume *: "i \ I" "x' \ A' i"
with bij have "\x \ A i. x' = f x"
unfolding bij_betw_def by blast
with * have "\j \ I. \x \ A j. x' = f x"
by blast
then show "x' \ f ` \(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 \ \x\A. B x \ C \ j \ A \ f ` (\(B ` A)) = (\x\A. f ` B x)"
by (auto simp add: inj_on_def) blast
lemma bij_image_INT: "bij f \ f ` (\(B ` A)) = (\x\A. f ` B x)"
by (auto simp: bij_def inj_def surj_def) blast
lemma UNION_fun_upd: "\(A(i := B) ` J) = \(A ` (J - {i})) \ (if i \ J then B else {})"
by (auto simp add: set_eq_iff)
lemma bij_betw_Pow:
assumes "bij_betw f A B"
shows "bij_betw (image f) (Pow A) (Pow B)"
proof -
from assms have "inj_on f A"
by (rule bij_betw_imp_inj_on)
then have "inj_on f (\(Pow A))"
by simp
then have "inj_on (image f) (Pow A)"
by (rule inj_on_image)
then have "bij_betw (image f) (Pow A) (image f ` Pow A)"
by (rule inj_on_imp_bij_betw)
moreover from assms have "f ` A = B"
by (rule bij_betw_imp_surj_on)
then have "image f ` Pow A = Pow B"
by (rule image_Pow_surj)
ultimately show ?thesis by simp
qed
subsubsection \<open>Complement\<close>
lemma Compl_INT [simp]: "- (\x\A. B x) = (\x\A. -B x)"
by blast
lemma Compl_UN [simp]: "- (\x\A. B x) = (\x\A. -B x)"
by blast
subsubsection \<open>Miniscoping and maxiscoping\<close>
text \<open>\<^medskip> Miniscoping: pushing in quantifiers and big Unions and Intersections.\<close>
lemma UN_simps [simp]:
"\a B C. (\x\C. insert a (B x)) = (if C={} then {} else insert a (\x\C. B x))"
"\A B C. (\x\C. A x \ B) = ((if C={} then {} else (\x\C. A x) \ B))"
"\A B C. (\x\C. A \ B x) = ((if C={} then {} else A \ (\x\C. B x)))"
"\A B C. (\x\C. A x \ B) = ((\x\C. A x) \ B)"
"\A B C. (\x\C. A \ B x) = (A \(\x\C. B x))"
"\A B C. (\x\C. A x - B) = ((\x\C. A x) - B)"
"\A B C. (\x\C. A - B x) = (A - (\x\C. B x))"
"\A B. (\x\\A. B x) = (\y\A. \x\y. B x)"
"\A B C. (\z\(\(B ` A)). C z) = (\x\A. \z\B x. C z)"
"\A B f. (\x\f`A. B x) = (\a\A. B (f a))"
by auto
lemma INT_simps [simp]:
"\A B C. (\x\C. A x \ B) = (if C={} then UNIV else (\x\C. A x) \ B)"
"\A B C. (\x\C. A \ B x) = (if C={} then UNIV else A \(\x\C. B x))"
"\A B C. (\x\C. A x - B) = (if C={} then UNIV else (\x\C. A x) - B)"
"\A B C. (\x\C. A - B x) = (if C={} then UNIV else A - (\x\C. B x))"
"\a B C. (\x\C. insert a (B x)) = insert a (\x\C. B x)"
"\A B C. (\x\C. A x \ B) = ((\x\C. A x) \ B)"
"\A B C. (\x\C. A \ B x) = (A \ (\x\C. B x))"
"\A B. (\x\\A. B x) = (\y\A. \x\y. B x)"
"\A B C. (\z\(\(B ` A)). C z) = (\x\A. \z\B x. C z)"
"\A B f. (\x\f`A. B x) = (\a\A. B (f a))"
by auto
lemma UN_ball_bex_simps [simp]:
"\A P. (\x\\A. P x) \ (\y\A. \x\y. P x)"
"\A B P. (\x\(\(B ` A)). P x) = (\a\A. \x\ B a. P x)"
"\A P. (\x\\A. P x) \ (\y\A. \x\y. P x)"
"\A B P. (\x\(\(B ` A)). P x) \ (\a\A. \x\B a. P x)"
by auto
text \<open>\<^medskip> Maxiscoping: pulling out big Unions and Intersections.\<close>
lemma UN_extend_simps:
"\a B C. insert a (\x\C. B x) = (if C={} then {a} else (\x\C. insert a (B x)))"
"\A B C. (\x\C. A x) \ B = (if C={} then B else (\x\C. A x \ B))"
"\A B C. A \ (\x\C. B x) = (if C={} then A else (\x\C. A \ B x))"
"\A B C. ((\x\C. A x) \ B) = (\x\C. A x \ B)"
"\A B C. (A \ (\x\C. B x)) = (\x\C. A \ B x)"
"\A B C. ((\x\C. A x) - B) = (\x\C. A x - B)"
"\A B C. (A - (\x\C. B x)) = (\x\C. A - B x)"
"\A B. (\y\A. \x\y. B x) = (\x\\A. B x)"
"\A B C. (\x\A. \z\B x. C z) = (\z\(\(B ` A)). C z)"
"\A B f. (\a\A. B (f a)) = (\x\f`A. B x)"
by auto
lemma INT_extend_simps:
"\A B C. (\x\C. A x) \ B = (if C={} then B else (\x\C. A x \ B))"
"\A B C. A \ (\x\C. B x) = (if C={} then A else (\x\C. A \ B x))"
"\A B C. (\x\C. A x) - B = (if C={} then UNIV - B else (\x\C. A x - B))"
"\A B C. A - (\x\C. B x) = (if C={} then A else (\x\C. A - B x))"
"\a B C. insert a (\x\C. B x) = (\x\C. insert a (B x))"
"\A B C. ((\x\C. A x) \ B) = (\x\C. A x \ B)"
"\A B C. A \ (\x\C. B x) = (\x\C. A \ B x)"
"\A B. (\y\A. \x\y. B x) = (\x\\A. B x)"
"\A B C. (\x\A. \z\B x. C z) = (\z\(\(B ` A)). C z)"
"\A B f. (\a\A. B (f a)) = (\x\f`A. B x)"
by auto
text \<open>Finally\<close>
lemmas mem_simps =
insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
\<comment> \<open>Each of these has ALREADY been added \<open>[simp]\<close> above.\<close>
end
¤ Dauer der Verarbeitung: 0.48 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
