(* Title: HOL/Set_Interval.thy
Author: Tobias Nipkow, Clemens Ballarin, Jeremy Avigad
lessThan, greaterThan, atLeast, atMost and two-sided intervals
Modern convention: Ixy stands for an interval where x and y
describe the lower and upper bound and x,y : {c,o,i}
where c = closed, o = open, i = infinite.
Examples: Ico = {_ ..< _} and Ici = {_ ..}
*)
section \<open>Set intervals\<close>
theory Set_Interval
imports Divides
begin
(* Belongs in Finite_Set but 2 is not available there *)
lemma card_2_iff: "card S = 2 \ (\x y. S = {x,y} \ x \ y)"
by (auto simp: card_Suc_eq numeral_eq_Suc)
lemma card_2_iff': "card S = 2 \ (\x\S. \y\S. x \ y \ (\z\S. z = x \ z = y))"
by (auto simp: card_Suc_eq numeral_eq_Suc)
context ord
begin
definition
lessThan :: "'a => 'a set" ("(1{..<_})") where
"{..
definition
atMost :: "'a => 'a set" ("(1{.._})") where
"{..u} == {x. x \ u}"
definition
greaterThan :: "'a => 'a set" ("(1{_<..})") where
"{l<..} == {x. l
definition
atLeast :: "'a => 'a set" ("(1{_..})") where
"{l..} == {x. l\x}"
definition
greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where
"{l<..
definition
atLeastLessThan :: "'a => 'a => 'a set" ("(1{_..<_})") where
"{l..
definition
greaterThanAtMost :: "'a => 'a => 'a set" ("(1{_<.._})") where
"{l<..u} == {l<..} Int {..u}"
definition
atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where
"{l..u} == {l..} Int {..u}"
end
text\<open>A note of warning when using \<^term>\<open>{..<n}\<close> on type \<^typ>\<open>nat\<close>: it is equivalent to \<^term>\<open>{0::nat..<n}\<close> but some lemmas involving
\<^term>\<open>{m..<n}\<close> may not exist in \<^term>\<open>{..<n}\<close>-form as well.\<close>
syntax (ASCII)
"_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10)
"_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10)
"_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10)
"_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10)
syntax (latex output)
"_UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ \ _)/ _)" [0, 0, 10] 10)
"_UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ < _)/ _)" [0, 0, 10] 10)
"_INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ \ _)/ _)" [0, 0, 10] 10)
"_INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ < _)/ _)" [0, 0, 10] 10)
syntax
"_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10)
"_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\_<_./ _)" [0, 0, 10] 10)
"_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10)
"_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\_<_./ _)" [0, 0, 10] 10)
translations
"\i\n. A" \ "\i\{..n}. A"
"\i "\i\{..
"\i\n. A" \ "\i\{..n}. A"
"\i "\i\{..
subsection \<open>Various equivalences\<close>
lemma (in ord) lessThan_iff [iff]: "(i \ lessThan k) = (i
by (simp add: lessThan_def)
lemma Compl_lessThan [simp]:
"!!k:: 'a::linorder. -lessThan k = atLeast k"
by (auto simp add: lessThan_def atLeast_def)
lemma single_Diff_lessThan [simp]: "!!k:: 'a::preorder. {k} - lessThan k = {k}"
by auto
lemma (in ord) greaterThan_iff [iff]: "(i \ greaterThan k) = (k
by (simp add: greaterThan_def)
lemma Compl_greaterThan [simp]:
"!!k:: 'a::linorder. -greaterThan k = atMost k"
by (auto simp add: greaterThan_def atMost_def)
lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
apply (subst Compl_greaterThan [symmetric])
apply (rule double_complement)
done
lemma (in ord) atLeast_iff [iff]: "(i \ atLeast k) = (k<=i)"
by (simp add: atLeast_def)
lemma Compl_atLeast [simp]: "!!k:: 'a::linorder. -atLeast k = lessThan k"
by (auto simp add: lessThan_def atLeast_def)
lemma (in ord) atMost_iff [iff]: "(i \ atMost k) = (i<=k)"
by (simp add: atMost_def)
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
by (blast intro: order_antisym)
lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \ { b <..} = { max a b <..}"
by auto
lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \ {..< b} = {..< min a b}"
by auto
subsection \<open>Logical Equivalences for Set Inclusion and Equality\<close>
lemma atLeast_empty_triv [simp]: "{{}..} = UNIV"
by auto
lemma atMost_UNIV_triv [simp]: "{..UNIV} = UNIV"
by auto
lemma atLeast_subset_iff [iff]:
"(atLeast x \ atLeast y) = (y \ (x::'a::preorder))"
by (blast intro: order_trans)
lemma atLeast_eq_iff [iff]:
"(atLeast x = atLeast y) = (x = (y::'a::order))"
by (blast intro: order_antisym order_trans)
lemma greaterThan_subset_iff [iff]:
"(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))"
unfolding greaterThan_def by (auto simp: linorder_not_less [symmetric])
lemma greaterThan_eq_iff [iff]:
"(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"
by (auto simp: elim!: equalityE)
lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::preorder))"
by (blast intro: order_trans)
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::order))"
by (blast intro: order_antisym order_trans)
lemma lessThan_subset_iff [iff]:
"(lessThan x \ lessThan y) = (x \ (y::'a::linorder))"
unfolding lessThan_def by (auto simp: linorder_not_less [symmetric])
lemma lessThan_eq_iff [iff]:
"(lessThan x = lessThan y) = (x = (y::'a::linorder))"
by (auto simp: elim!: equalityE)
lemma lessThan_strict_subset_iff:
fixes m n :: "'a::linorder"
shows "{.. m < n"
by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)
lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \ {b <..} \ b < a"
by auto
lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \ {..< b} \ a < b"
by auto
lemma (in preorder) Ioi_le_Ico: "{a <..} \ {a ..}"
by (auto intro: less_imp_le)
subsection \<open>Two-sided intervals\<close>
context ord
begin
lemma greaterThanLessThan_iff [simp]: "(i \ {l<.. i < u)"
by (simp add: greaterThanLessThan_def)
lemma atLeastLessThan_iff [simp]: "(i \ {l.. i \ i < u)"
by (simp add: atLeastLessThan_def)
lemma greaterThanAtMost_iff [simp]: "(i \ {l<..u}) = (l < i \ i \ u)"
by (simp add: greaterThanAtMost_def)
lemma atLeastAtMost_iff [simp]: "(i \ {l..u}) = (l \ i \ i \ u)"
by (simp add: atLeastAtMost_def)
text \<open>The above four lemmas could be declared as iffs. Unfortunately this
breaks many proofs. Since it only helps blast, it is better to leave them
alone.\<close>
lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \ {..< b }"
by auto
lemma (in order) atLeastLessThan_eq_atLeastAtMost_diff:
"{a..
by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
lemma (in order) greaterThanAtMost_eq_atLeastAtMost_diff:
"{a<..b} = {a..b} - {a}"
by (auto simp add: greaterThanAtMost_def atLeastAtMost_def)
end
subsubsection\<open>Emptyness, singletons, subset\<close>
context preorder
begin
lemma atLeastatMost_empty_iff[simp]:
"{a..b} = {} \ (\ a \ b)"
by auto (blast intro: order_trans)
lemma atLeastatMost_empty_iff2[simp]:
"{} = {a..b} \ (\ a \ b)"
by auto (blast intro: order_trans)
lemma atLeastLessThan_empty_iff[simp]:
"{a.. (\ a < b)"
by auto (blast intro: le_less_trans)
lemma atLeastLessThan_empty_iff2[simp]:
"{} = {a.. (\ a < b)"
by auto (blast intro: le_less_trans)
lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ \ k < l"
by auto (blast intro: less_le_trans)
lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ \ k < l"
by auto (blast intro: less_le_trans)
lemma atLeastatMost_subset_iff[simp]:
"{a..b} \ {c..d} \ (\ a \ b) \ c \ a \ b \ d"
unfolding atLeastAtMost_def atLeast_def atMost_def
by (blast intro: order_trans)
lemma atLeastatMost_psubset_iff:
"{a..b} < {c..d} \
((\<not> a \<le> b) \<or> c \<le> a \<and> b \<le> d \<and> (c < a \<or> b < d)) \<and> c \<le> d"
by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)
lemma atLeastAtMost_subseteq_atLeastLessThan_iff:
"{a..b} \ {c ..< d} \ (a \ b \ c \ a \ b < d)"
by auto (blast intro: local.order_trans local.le_less_trans elim: )+
lemma Icc_subset_Ici_iff[simp]:
"{l..h} \ {l'..} = (\ l\h \ l\l')"
by(auto simp: subset_eq intro: order_trans)
lemma Icc_subset_Iic_iff[simp]:
"{l..h} \ {..h'} = (\ l\h \ h\h')"
by(auto simp: subset_eq intro: order_trans)
lemma not_Ici_eq_empty[simp]: "{l..} \ {}"
by(auto simp: set_eq_iff)
lemma not_Iic_eq_empty[simp]: "{..h} \ {}"
by(auto simp: set_eq_iff)
lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]
lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric]
end
context order
begin
lemma atLeastatMost_empty[simp]:
"b < a \ {a..b} = {}"
by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
lemma atLeastLessThan_empty[simp]:
"b \ a \ {a..
by(auto simp: atLeastLessThan_def)
lemma greaterThanAtMost_empty[simp]: "l \ k ==> {k<..l} = {}"
by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<..
by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
lemma atLeastAtMost_singleton': "a = b \ {a .. b} = {a}" by simp
lemma Icc_eq_Icc[simp]:
"{l..h} = {l'..h'} = (l=l' \ h=h' \ \ l\h \ \ l'\h')"
by(simp add: order_class.eq_iff)(auto intro: order_trans)
lemma atLeastAtMost_singleton_iff[simp]:
"{a .. b} = {c} \ a = b \ b = c"
proof
assume "{a..b} = {c}"
hence *: "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
with \<open>{a..b} = {c}\<close> have "c \<le> a \<and> b \<le> c" by auto
with * show "a = b \ b = c" by auto
qed simp
end
context no_top
begin
(* also holds for no_bot but no_top should suffice *)
lemma not_UNIV_le_Icc[simp]: "\ UNIV \ {l..h}"
using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)
lemma not_UNIV_le_Iic[simp]: "\ UNIV \ {..h}"
using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)
lemma not_Ici_le_Icc[simp]: "\ {l..} \ {l'..h'}"
using gt_ex[of h']
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)
lemma not_Ici_le_Iic[simp]: "\ {l..} \ {..h'}"
using gt_ex[of h']
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)
end
context no_bot
begin
lemma not_UNIV_le_Ici[simp]: "\ UNIV \ {l..}"
using lt_ex[of l] by(auto simp: subset_eq less_le_not_le)
lemma not_Iic_le_Icc[simp]: "\ {..h} \ {l'..h'}"
using lt_ex[of l']
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)
lemma not_Iic_le_Ici[simp]: "\ {..h} \ {l'..}"
using lt_ex[of l']
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)
end
context no_top
begin
(* also holds for no_bot but no_top should suffice *)
lemma not_UNIV_eq_Icc[simp]: "\ UNIV = {l'..h'}"
using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le)
lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric]
lemma not_UNIV_eq_Iic[simp]: "\ UNIV = {..h'}"
using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le)
lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric]
lemma not_Icc_eq_Ici[simp]: "\ {l..h} = {l'..}"
unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast
lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric]
(* also holds for no_bot but no_top should suffice *)
lemma not_Iic_eq_Ici[simp]: "\ {..h} = {l'..}"
using not_Ici_le_Iic[of l' h] by blast
lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric]
end
context no_bot
begin
lemma not_UNIV_eq_Ici[simp]: "\ UNIV = {l'..}"
using lt_ex[of l'] by(auto simp: set_eq_iff less_le_not_le)
lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric]
lemma not_Icc_eq_Iic[simp]: "\ {l..h} = {..h'}"
unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast
lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric]
end
context dense_linorder
begin
lemma greaterThanLessThan_empty_iff[simp]:
"{ a <..< b } = {} \ b \ a"
using dense[of a b] by (cases "a < b") auto
lemma greaterThanLessThan_empty_iff2[simp]:
"{} = { a <..< b } \ b \ a"
using dense[of a b] by (cases "a < b") auto
lemma atLeastLessThan_subseteq_atLeastAtMost_iff:
"{a ..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"
using dense[of "max a d" "b"]
by (force simp: subset_eq Ball_def not_less[symmetric])
lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:
"{a <.. b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"
using dense[of "a" "min c b"]
by (force simp: subset_eq Ball_def not_less[symmetric])
lemma greaterThanLessThan_subseteq_atLeastAtMost_iff:
"{a <..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"
using dense[of "a" "min c b"] dense[of "max a d" "b"]
by (force simp: subset_eq Ball_def not_less[symmetric])
lemma greaterThanLessThan_subseteq_greaterThanLessThan:
"{a <..< b} \ {c <..< d} \ (a < b \ a \ c \ b \ d)"
using dense[of "a" "min c b"] dense[of "max a d" "b"]
by (force simp: subset_eq Ball_def not_less[symmetric])
lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:
"{a <.. b} \ { c ..< d } \ (a < b \ c \ a \ b < d)"
using dense[of "a" "min c b"]
by (force simp: subset_eq Ball_def not_less[symmetric])
lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:
"{a <..< b} \ { c ..< d } \ (a < b \ c \ a \ b \ d)"
using dense[of "a" "min c b"] dense[of "max a d" "b"]
by (force simp: subset_eq Ball_def not_less[symmetric])
lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff:
"{a <..< b} \ { c <.. d } \ (a < b \ c \ a \ b \ d)"
using dense[of "a" "min c b"] dense[of "max a d" "b"]
by (force simp: subset_eq Ball_def not_less[symmetric])
end
context no_top
begin
lemma greaterThan_non_empty[simp]: "{x <..} \ {}"
using gt_ex[of x] by auto
end
context no_bot
begin
lemma lessThan_non_empty[simp]: "{..< x} \ {}"
using lt_ex[of x] by auto
end
lemma (in linorder) atLeastLessThan_subset_iff:
"{a.. {c.. b \ a \ c\a \ b\d"
apply (auto simp:subset_eq Ball_def not_le)
apply(frule_tac x=a in spec)
apply(erule_tac x=d in allE)
apply (auto simp: )
done
lemma atLeastLessThan_inj:
fixes a b c d :: "'a::linorder"
assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"
shows "a = c" "b = d"
using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le antisym_conv2 subset_refl)+
lemma atLeastLessThan_eq_iff:
fixes a b c d :: "'a::linorder"
assumes "a < b" "c < d"
shows "{a ..< b} = {c ..< d} \ a = c \ b = d"
using atLeastLessThan_inj assms by auto
lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \ (b \ a \ d \ c) \ a = c \ b = d"
by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le)
lemma (in order) Iio_Int_singleton: "{.. {x} = (if x < k then {x} else {})"
by auto
lemma (in linorder) Ioc_subset_iff: "{a<..b} \ {c<..d} \ (b \ a \ c \ a \ b \ d)"
by (auto simp: subset_eq Ball_def) (metis less_le not_less)
lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot"
by (auto simp: set_eq_iff intro: le_bot)
lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \ x = top"
by (auto simp: set_eq_iff intro: top_le)
lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff:
"{x..y} = UNIV \ (x = bot \ y = top)"
by (auto simp: set_eq_iff intro: top_le le_bot)
lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \ n = bot"
by (auto simp: set_eq_iff not_less le_bot)
lemma lessThan_empty_iff: "{..< n::nat} = {} \ n = 0"
by (simp add: Iio_eq_empty_iff bot_nat_def)
lemma mono_image_least:
assumes f_mono: "mono f" and f_img: "f ` {m ..< n} = {m' ..< n'}" "m < n"
shows "f m = m'"
proof -
from f_img have "{m' ..< n'} \ {}"
by (metis atLeastLessThan_empty_iff image_is_empty)
with f_img have "m' \ f ` {m ..< n}" by auto
then obtain k where "f k = m'" "m \ k" by auto
moreover have "m' \ f m" using f_img by auto
ultimately show "f m = m'"
using f_mono by (auto elim: monoE[where x=m and y=k])
qed
subsection \<open>Infinite intervals\<close>
context dense_linorder
begin
lemma infinite_Ioo:
assumes "a < b"
shows "\ finite {a<..
proof
assume fin: "finite {a<..
moreover have ne: "{a<.. {}"
using \<open>a < b\<close> by auto
ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b"
using Max_in[of "{a <..< b}"] by auto
then obtain x where "Max {a <..< b} < x" "x < b"
using dense[of "Max {a<.. b] by auto
then have "x \ {a <..< b}"
using \<open>a < Max {a <..< b}\<close> by auto
then have "x \ Max {a <..< b}"
using fin by auto
with \<open>Max {a <..< b} < x\<close> show False by auto
qed
lemma infinite_Icc: "a < b \ \ finite {a .. b}"
using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b]
by (auto dest: finite_subset)
lemma infinite_Ico: "a < b \ \ finite {a ..< b}"
using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b]
by (auto dest: finite_subset)
lemma infinite_Ioc: "a < b \ \ finite {a <.. b}"
using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b]
by (auto dest: finite_subset)
lemma infinite_Ioo_iff [simp]: "infinite {a<.. a < b"
using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioo)
lemma infinite_Icc_iff [simp]: "infinite {a .. b} \ a < b"
using not_less_iff_gr_or_eq by (fastforce simp: infinite_Icc)
lemma infinite_Ico_iff [simp]: "infinite {a.. a < b"
using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ico)
lemma infinite_Ioc_iff [simp]: "infinite {a<..b} \ a < b"
using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioc)
end
lemma infinite_Iio: "\ finite {..< a :: 'a :: {no_bot, linorder}}"
proof
assume "finite {..< a}"
then have *: "\x. x < a \ Min {..< a} \ x"
by auto
obtain x where "x < a"
using lt_ex by auto
obtain y where "y < Min {..< a}"
using lt_ex by auto
also have "Min {..< a} \ x"
using \<open>x < a\<close> by fact
also note \<open>x < a\<close>
finally have "Min {..< a} \ y"
by fact
with \<open>y < Min {..< a}\<close> show False by auto
qed
lemma infinite_Iic: "\ finite {.. a :: 'a :: {no_bot, linorder}}"
using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"]
by (auto simp: subset_eq less_imp_le)
lemma infinite_Ioi: "\ finite {a :: 'a :: {no_top, linorder} <..}"
proof
assume "finite {a <..}"
then have *: "\x. a < x \ x \ Max {a <..}"
by auto
obtain y where "Max {a <..} < y"
using gt_ex by auto
obtain x where x: "a < x"
using gt_ex by auto
also from x have "x \ Max {a <..}"
by fact
also note \<open>Max {a <..} < y\<close>
finally have "y \ Max { a <..}"
by fact
with \<open>Max {a <..} < y\<close> show False by auto
qed
lemma infinite_Ici: "\ finite {a :: 'a :: {no_top, linorder} ..}"
using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"]
by (auto simp: subset_eq less_imp_le)
subsubsection \<open>Intersection\<close>
context linorder
begin
lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"
by auto
lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"
by auto
lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"
by auto
lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"
by auto
lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"
by auto
lemma Int_atLeastLessThan[simp]: "{a..
by auto
lemma Int_greaterThanAtMost[simp]: "{a<..b} Int {c<..d} = {max a c <.. min b d}"
by auto
lemma Int_greaterThanLessThan[simp]: "{a<..
by auto
lemma Int_atMost[simp]: "{..a} \ {..b} = {.. min a b}"
by (auto simp: min_def)
lemma Ioc_disjoint: "{a<..b} \ {c<..d} = {} \ b \ a \ d \ c \ b \ c \ d \ a"
by auto
end
context complete_lattice
begin
lemma
shows Sup_atLeast[simp]: "Sup {x ..} = top"
and Sup_greaterThanAtLeast[simp]: "x < top \ Sup {x <..} = top"
and Sup_atMost[simp]: "Sup {.. y} = y"
and Sup_atLeastAtMost[simp]: "x \ y \ Sup { x .. y} = y"
and Sup_greaterThanAtMost[simp]: "x < y \ Sup { x <.. y} = y"
by (auto intro!: Sup_eqI)
lemma
shows Inf_atMost[simp]: "Inf {.. x} = bot"
and Inf_atMostLessThan[simp]: "top < x \ Inf {..< x} = bot"
and Inf_atLeast[simp]: "Inf {x ..} = x"
and Inf_atLeastAtMost[simp]: "x \ y \ Inf { x .. y} = x"
and Inf_atLeastLessThan[simp]: "x < y \ Inf { x ..< y} = x"
by (auto intro!: Inf_eqI)
end
lemma
fixes x y :: "'a :: {complete_lattice, dense_linorder}"
shows Sup_lessThan[simp]: "Sup {..< y} = y"
and Sup_atLeastLessThan[simp]: "x < y \ Sup { x ..< y} = y"
and Sup_greaterThanLessThan[simp]: "x < y \ Sup { x <..< y} = y"
and Inf_greaterThan[simp]: "Inf {x <..} = x"
and Inf_greaterThanAtMost[simp]: "x < y \ Inf { x <.. y} = x"
and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x"
by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded)
subsection \<open>Intervals of natural numbers\<close>
subsubsection \<open>The Constant \<^term>\<open>lessThan\<close>\<close>
lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
by (simp add: lessThan_def)
lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
by (simp add: lessThan_def less_Suc_eq, blast)
text \<open>The following proof is convenient in induction proofs where
new elements get indices at the beginning. So it is used to transform
\<^term>\<open>{..<Suc n}\<close> to \<^term>\<open>0::nat\<close> and \<^term>\<open>{..< n}\<close>.\<close>
lemma zero_notin_Suc_image [simp]: "0 \ Suc ` A"
by auto
lemma lessThan_Suc_eq_insert_0: "{..
by (auto simp: image_iff less_Suc_eq_0_disj)
lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
by (simp add: lessThan_def atMost_def less_Suc_eq_le)
lemma atMost_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})"
unfolding lessThan_Suc_atMost[symmetric] lessThan_Suc_eq_insert_0[of "Suc n"] ..
lemma UN_lessThan_UNIV: "(\m::nat. lessThan m) = UNIV"
by blast
subsubsection \<open>The Constant \<^term>\<open>greaterThan\<close>\<close>
lemma greaterThan_0: "greaterThan 0 = range Suc"
unfolding greaterThan_def
by (blast dest: gr0_conv_Suc [THEN iffD1])
lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
unfolding greaterThan_def
by (auto elim: linorder_neqE)
lemma INT_greaterThan_UNIV: "(\m::nat. greaterThan m) = {}"
by blast
subsubsection \<open>The Constant \<^term>\<open>atLeast\<close>\<close>
lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
by (unfold atLeast_def UNIV_def, simp)
lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
unfolding atLeast_def by (auto simp: order_le_less Suc_le_eq)
lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)
lemma UN_atLeast_UNIV: "(\m::nat. atLeast m) = UNIV"
by blast
subsubsection \<open>The Constant \<^term>\<open>atMost\<close>\<close>
lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
by (simp add: atMost_def)
lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
unfolding atMost_def by (auto simp add: less_Suc_eq order_le_less)
lemma UN_atMost_UNIV: "(\m::nat. atMost m) = UNIV"
by blast
subsubsection \<open>The Constant \<^term>\<open>atLeastLessThan\<close>\<close>
text\<open>The orientation of the following 2 rules is tricky. The lhs is
defined in terms of the rhs. Hence the chosen orientation makes sense
in this theory --- the reverse orientation complicates proofs (eg
nontermination). But outside, when the definition of the lhs is rarely
used, the opposite orientation seems preferable because it reduces a
specific concept to a more general one.\<close>
lemma atLeast0LessThan [code_abbrev]: "{0::nat..
by(simp add:lessThan_def atLeastLessThan_def)
lemma atLeast0AtMost [code_abbrev]: "{0..n::nat} = {..n}"
by(simp add:atMost_def atLeastAtMost_def)
lemma lessThan_atLeast0: "{..
by (simp add: atLeast0LessThan)
lemma atMost_atLeast0: "{..n} = {0::nat..n}"
by (simp add: atLeast0AtMost)
lemma atLeastLessThan0: "{m..<0::nat} = {}"
by (simp add: atLeastLessThan_def)
lemma atLeast0_lessThan_Suc: "{0..
by (simp add: atLeast0LessThan lessThan_Suc)
lemma atLeast0_lessThan_Suc_eq_insert_0: "{0..
by (simp add: atLeast0LessThan lessThan_Suc_eq_insert_0)
subsubsection \<open>The Constant \<^term>\<open>atLeastAtMost\<close>\<close>
lemma Icc_eq_insert_lb_nat: "m \ n \ {m..n} = insert m {Suc m..n}"
by auto
lemma atLeast0_atMost_Suc:
"{0..Suc n} = insert (Suc n) {0..n}"
by (simp add: atLeast0AtMost atMost_Suc)
lemma atLeast0_atMost_Suc_eq_insert_0:
"{0..Suc n} = insert 0 (Suc ` {0..n})"
by (simp add: atLeast0AtMost atMost_Suc_eq_insert_0)
subsubsection \<open>Intervals of nats with \<^term>\<open>Suc\<close>\<close>
text\<open>Not a simprule because the RHS is too messy.\<close>
lemma atLeastLessThanSuc:
"{m.. n then insert n {m..
by (auto simp add: atLeastLessThan_def)
lemma atLeastLessThan_singleton [simp]: "{m..
by (auto simp add: atLeastLessThan_def)
lemma atLeastLessThanSuc_atLeastAtMost: "{l..
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}"
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def
greaterThanAtMost_def)
lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
greaterThanLessThan_def)
lemma atLeastAtMostSuc_conv: "m \ Suc n \ {m..Suc n} = insert (Suc n) {m..n}"
by auto
lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}"
by auto
text \<open>The analogous result is useful on \<^typ>\<open>int\<close>:\<close>
(* here, because we don't have an own int section *)
lemma atLeastAtMostPlus1_int_conv:
"m \ 1+n \ {m..1+n} = insert (1+n) {m..n::int}"
by (auto intro: set_eqI)
lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j..
by (induct k) (simp_all add: atLeastLessThanSuc)
subsubsection \<open>Intervals and numerals\<close>
lemma lessThan_nat_numeral: \<comment> \<open>Evaluation for specific numerals\<close>
"lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))"
by (simp add: numeral_eq_Suc lessThan_Suc)
lemma atMost_nat_numeral: \<comment> \<open>Evaluation for specific numerals\<close>
"atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))"
by (simp add: numeral_eq_Suc atMost_Suc)
lemma atLeastLessThan_nat_numeral: \<comment> \<open>Evaluation for specific numerals\<close>
"atLeastLessThan m (numeral k :: nat) =
(if m \<le> (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k))
else {})"
by (simp add: numeral_eq_Suc atLeastLessThanSuc)
subsubsection \<open>Image\<close>
context linordered_semidom
begin
lemma image_add_atLeast[simp]: "plus k ` {i..} = {k + i..}"
proof -
have "n = k + (n - k)" if "i + k \ n" for n
proof -
have "n = (n - (k + i)) + (k + i)" using that
by (metis add_commute le_add_diff_inverse)
then show "n = k + (n - k)"
by (metis local.add_diff_cancel_left' add_assoc add_commute)
qed
then show ?thesis
by (fastforce simp: add_le_imp_le_diff add.commute)
qed
lemma image_add_atLeastAtMost [simp]:
"plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B")
proof
show "?A \ ?B"
by (auto simp add: ac_simps)
next
show "?B \ ?A"
proof
fix n
assume "n \ ?B"
then have "i \ n - k"
by (simp add: add_le_imp_le_diff)
have "n = n - k + k"
proof -
from \<open>n \<in> ?B\<close> have "n = n - (i + k) + (i + k)"
by simp
also have "\ = n - k - i + i + k"
by (simp add: algebra_simps)
also have "\ = n - k + k"
using \<open>i \<le> n - k\<close> by simp
finally show ?thesis .
qed
moreover have "n - k \ {i..j}"
using \<open>n \<in> ?B\<close>
by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le)
ultimately show "n \ ?A"
by (simp add: ac_simps)
qed
qed
lemma image_add_atLeastAtMost' [simp]:
"(\n. n + k) ` {i..j} = {i + k..j + k}"
by (simp add: add.commute [of _ k])
lemma image_add_atLeastLessThan [simp]:
"plus k ` {i..
by (simp add: image_set_diff atLeastLessThan_eq_atLeastAtMost_diff ac_simps)
lemma image_add_atLeastLessThan' [simp]:
"(\n. n + k) ` {i..
by (simp add: add.commute [of _ k])
lemma image_add_greaterThanAtMost[simp]: "(+) c ` {a<..b} = {c + a<..c + b}"
by (simp add: image_set_diff greaterThanAtMost_eq_atLeastAtMost_diff ac_simps)
end
context ordered_ab_group_add
begin
lemma
fixes x :: 'a
shows image_uminus_greaterThan[simp]: "uminus ` {x<..} = {..<-x}"
and image_uminus_atLeast[simp]: "uminus ` {x..} = {..-x}"
proof safe
fix y assume "y < -x"
hence *: "x < -y" using neg_less_iff_less[of "-y" x] by simp
have "- (-y) \ uminus ` {x<..}"
by (rule imageI) (simp add: *)
thus "y \ uminus ` {x<..}" by simp
next
fix y assume "y \ -x"
have "- (-y) \ uminus ` {x..}"
by (rule imageI) (insert \<open>y \<le> -x\<close>[THEN le_imp_neg_le], simp)
thus "y \ uminus ` {x..}" by simp
qed simp_all
lemma
fixes x :: 'a
shows image_uminus_lessThan[simp]: "uminus ` {..
and image_uminus_atMost[simp]: "uminus ` {..x} = {-x..}"
proof -
have "uminus ` {..
and "uminus ` {..x} = uminus ` uminus ` {-x..}" by simp_all
thus "uminus ` {.. and "uminus ` {..x} = {-x..}"
by (simp_all add: image_image
del: image_uminus_greaterThan image_uminus_atLeast)
qed
lemma
fixes x :: 'a
shows image_uminus_atLeastAtMost[simp]: "uminus ` {x..y} = {-y..-x}"
and image_uminus_greaterThanAtMost[simp]: "uminus ` {x<..y} = {-y..<-x}"
and image_uminus_atLeastLessThan[simp]: "uminus ` {x..
and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute)
lemma image_add_atMost[simp]: "(+) c ` {..a} = {..c + a}"
by (auto intro!: image_eqI[where x="x - c" for x] simp: algebra_simps)
end
lemma image_Suc_atLeastAtMost [simp]:
"Suc ` {i..j} = {Suc i..Suc j}"
using image_add_atLeastAtMost [of 1 i j]
by (simp only: plus_1_eq_Suc) simp
lemma image_Suc_atLeastLessThan [simp]:
"Suc ` {i..
using image_add_atLeastLessThan [of 1 i j]
by (simp only: plus_1_eq_Suc) simp
corollary image_Suc_atMost:
"Suc ` {..n} = {1..Suc n}"
by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
corollary image_Suc_lessThan:
"Suc ` {..
by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
lemma image_diff_atLeastAtMost [simp]:
fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
apply auto
apply (rule_tac x="d-x" in rev_image_eqI, auto)
done
lemma image_diff_atLeastLessThan [simp]:
fixes a b c::"'a::linordered_idom"
shows "(-) c ` {a..
proof -
have "(-) c ` {a..
unfolding image_image by simp
also have "\ = {c - b<..c - a}" by simp
finally show ?thesis by simp
qed
lemma image_minus_const_greaterThanAtMost[simp]:
fixes a b c::"'a::linordered_idom"
shows "(-) c ` {a<..b} = {c - b..
proof -
have "(-) c ` {a<..b} = (+) c ` uminus ` {a<..b}"
unfolding image_image by simp
also have "\ = {c - b..
finally show ?thesis by simp
qed
lemma image_minus_const_atLeast[simp]:
fixes a c::"'a::linordered_idom"
shows "(-) c ` {a..} = {..c - a}"
proof -
have "(-) c ` {a..} = (+) c ` uminus ` {a ..}"
unfolding image_image by simp
also have "\ = {..c - a}" by simp
finally show ?thesis by simp
qed
lemma image_minus_const_AtMost[simp]:
fixes b c::"'a::linordered_idom"
shows "(-) c ` {..b} = {c - b..}"
proof -
have "(-) c ` {..b} = (+) c ` uminus ` {..b}"
unfolding image_image by simp
also have "\ = {c - b..}" by simp
finally show ?thesis by simp
qed
lemma image_minus_const_atLeastAtMost' [simp]:
"(\t. t-d)`{a..b} = {a-d..b-d}" for d::"'a::linordered_idom"
by (metis (no_types, lifting) diff_conv_add_uminus image_add_atLeastAtMost' image_cong)
context linordered_field
begin
lemma image_mult_atLeastAtMost [simp]:
"((*) d ` {a..b}) = {d*a..d*b}" if "d>0"
using that
by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
lemma image_divide_atLeastAtMost [simp]:
"((\c. c / d) ` {a..b}) = {a/d..b/d}" if "d>0"
proof -
from that have "inverse d > 0"
by simp
with image_mult_atLeastAtMost [of "inverse d" a b]
have "(*) (inverse d) ` {a..b} = {inverse d * a..inverse d * b}"
by blast
moreover have "(*) (inverse d) = (\c. c / d)"
by (simp add: fun_eq_iff field_simps)
ultimately show ?thesis
by simp
qed
lemma image_mult_atLeastAtMost_if:
"(*) c ` {x .. y} =
(if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"
proof (cases "c = 0 \ x > y")
case True
then show ?thesis
by auto
next
case False
then have "x \ y"
by auto
from False consider "c < 0"| "c > 0"
by (auto simp add: neq_iff)
then show ?thesis
proof cases
case 1
have "(*) c ` {x..y} = {c * y..c * x}"
proof (rule set_eqI)
fix d
from 1 have "inj (\z. z / c)"
by (auto intro: injI)
then have "d \ (*) c ` {x..y} \ d / c \ (\z. z div c) ` (*) c ` {x..y}"
by (subst inj_image_mem_iff) simp_all
also have "\ \ d / c \ {x..y}"
using 1 by (simp add: image_image)
also have "\ \ d \ {c * y..c * x}"
by (auto simp add: field_simps 1)
finally show "d \ (*) c ` {x..y} \ d \ {c * y..c * x}" .
qed
with \<open>x \<le> y\<close> show ?thesis
by auto
qed (simp add: mult_left_mono_neg)
qed
lemma image_mult_atLeastAtMost_if':
"(\x. x * c) ` {x..y} =
(if x \<le> y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})"
using image_mult_atLeastAtMost_if [of c x y] by (auto simp add: ac_simps)
lemma image_affinity_atLeastAtMost:
"((\x. m * x + c) ` {a..b}) = (if {a..b} = {} then {}
else if 0 \<le> m then {m * a + c .. m * b + c}
else {m * b + c .. m * a + c})"
proof -
have *: "(\x. m * x + c) = ((\x. x + c) \ (*) m)"
by (simp add: fun_eq_iff)
show ?thesis by (simp only: * image_comp [symmetric] image_mult_atLeastAtMost_if)
(auto simp add: mult_le_cancel_left)
qed
lemma image_affinity_atLeastAtMost_diff:
"((\x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
else if 0 \<le> m then {m*a - c .. m*b - c}
else {m*b - c .. m*a - c})"
using image_affinity_atLeastAtMost [of m "-c" a b]
by simp
lemma image_affinity_atLeastAtMost_div:
"((\x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
else if 0 \<le> m then {a/m + c .. b/m + c}
else {b/m + c .. a/m + c})"
using image_affinity_atLeastAtMost [of "inverse m" c a b]
by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
lemma image_affinity_atLeastAtMost_div_diff:
"((\x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
else if 0 \<le> m then {a/m - c .. b/m - c}
else {b/m - c .. a/m - c})"
using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
end
lemma atLeast1_lessThan_eq_remove0:
"{Suc 0..
by auto
lemma atLeast1_atMost_eq_remove0:
"{Suc 0..n} = {..n} - {0}"
by auto
lemma image_add_int_atLeastLessThan:
"(\x. x + (l::int)) ` {0..
apply (auto simp add: image_def)
apply (rule_tac x = "x - l" in bexI)
apply auto
done
lemma image_minus_const_atLeastLessThan_nat:
fixes c :: nat
shows "(\i. i - c) ` {x ..< y} =
(if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
(is "_ = ?right")
proof safe
fix a assume a: "a \ ?right"
show "a \ (\i. i - c) ` {x ..< y}"
proof cases
assume "c < y" with a show ?thesis
by (auto intro!: image_eqI[of _ _ "a + c"])
next
assume "\ c < y" with a show ?thesis
by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
qed
qed auto
lemma image_int_atLeastLessThan:
"int ` {a..
by (auto intro!: image_eqI [where x = "nat x" for x])
lemma image_int_atLeastAtMost:
"int ` {a..b} = {int a..int b}"
by (auto intro!: image_eqI [where x = "nat x" for x])
subsubsection \<open>Finiteness\<close>
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..
by (induct k) (simp_all add: lessThan_Suc)
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
by (induct k) (simp_all add: atMost_Suc)
lemma finite_greaterThanLessThan [iff]:
fixes l :: nat shows "finite {l<..
by (simp add: greaterThanLessThan_def)
lemma finite_atLeastLessThan [iff]:
fixes l :: nat shows "finite {l..
by (simp add: atLeastLessThan_def)
lemma finite_greaterThanAtMost [iff]:
fixes l :: nat shows "finite {l<..u}"
by (simp add: greaterThanAtMost_def)
lemma finite_atLeastAtMost [iff]:
fixes l :: nat shows "finite {l..u}"
by (simp add: atLeastAtMost_def)
text \<open>A bounded set of natural numbers is finite.\<close>
lemma bounded_nat_set_is_finite: "(\i\N. i < (n::nat)) \ finite N"
by (rule finite_subset [OF _ finite_lessThan]) auto
text \<open>A set of natural numbers is finite iff it is bounded.\<close>
lemma finite_nat_set_iff_bounded:
"finite(N::nat set) = (\m. \n\N. n
proof
assume f:?F show ?B
using Max_ge[OF \<open>?F\<close>, simplified less_Suc_eq_le[symmetric]] by blast
next
assume ?B show ?F using \<open>?B\<close> by(blast intro:bounded_nat_set_is_finite)
qed
lemma finite_nat_set_iff_bounded_le: "finite(N::nat set) = (\m. \n\N. n\m)"
unfolding finite_nat_set_iff_bounded
by (blast dest:less_imp_le_nat le_imp_less_Suc)
lemma finite_less_ub:
"!!f::nat=>nat. (!!n. n \ f n) ==> finite {n. f n \ u}"
by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
lemma bounded_Max_nat:
fixes P :: "nat \ bool"
assumes x: "P x" and M: "\x. P x \ x \ M"
obtains m where "P m" "\x. P x \ x \ m"
proof -
have "finite {x. P x}"
using M finite_nat_set_iff_bounded_le by auto
then have "Max {x. P x} \ {x. P x}"
using Max_in x by auto
then show ?thesis
by (simp add: \<open>finite {x. P x}\<close> that)
qed
text\<open>Any subset of an interval of natural numbers the size of the
subset is exactly that interval.\<close>
lemma subset_card_intvl_is_intvl:
assumes "A \ {k..
shows "A = {k..
proof (cases "finite A")
case True
from this and assms show ?thesis
proof (induct A rule: finite_linorder_max_induct)
case empty thus ?case by auto
next
case (insert b A)
hence *: "b \ A" by auto
with insert have "A \ {k..
by fastforce+
with insert * show ?case by auto
qed
next
case False
with assms show ?thesis by simp
qed
subsubsection \<open>Proving Inclusions and Equalities between Unions\<close>
lemma UN_le_eq_Un0:
"(\i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B")
proof
show "?A \ ?B"
proof
fix x assume "x \ ?A"
then obtain i where i: "i\n" "x \ M i" by auto
show "x \ ?B"
proof(cases i)
case 0 with i show ?thesis by simp
next
case (Suc j) with i show ?thesis by auto
qed
qed
next
show "?B \ ?A" by fastforce
qed
lemma UN_le_add_shift:
"(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B")
proof
show "?A \ ?B" by fastforce
next
show "?B \ ?A"
proof
fix x assume "x \ ?B"
then obtain i where i: "i \ {k..n+k}" "x \ M(i)" by auto
hence "i-k\n \ x \ M((i-k)+k)" by auto
thus "x \ ?A" by blast
qed
qed
lemma UN_le_add_shift_strict:
"(\ii\{k..
proof
show "?B \ ?A"
proof
fix x assume "x \ ?B"
then obtain i where i: "i \ {k.. M(i)" by auto
then have "i - k < n \ x \ M((i-k) + k)" by auto
then show "x \ ?A" using UN_le_add_shift by blast
qed
qed (fastforce)
lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)"
by (auto simp add: atLeast0LessThan)
lemma UN_finite_subset:
"(\n::nat. (\i\{0.. C) \ (\n. A n) \ C"
by (subst UN_UN_finite_eq [symmetric]) blast
lemma UN_finite2_subset:
assumes "\n::nat. (\i\{0.. (\i\{0..
shows "(\n. A n) \ (\n. B n)"
proof (rule UN_finite_subset, rule)
fix n and a
from assms have "(\i\{0.. (\i\{0..
moreover assume "a \ (\i\{0..
ultimately have "a \ (\i\{0..
then show "a \ (\i. B i)" by (auto simp add: UN_UN_finite_eq)
qed
lemma UN_finite2_eq:
"(\n::nat. (\i\{0..i\{0..
(\<Union>n. A n) = (\<Union>n. B n)"
apply (rule subset_antisym [OF UN_finite_subset UN_finite2_subset])
apply auto
apply (force simp add: atLeastLessThan_add_Un [of 0])+
done
subsubsection \<open>Cardinality\<close>
lemma card_lessThan [simp]: "card {..
by (induct u, simp_all add: lessThan_Suc)
lemma card_atMost [simp]: "card {..u} = Suc u"
by (simp add: lessThan_Suc_atMost [THEN sym])
lemma card_atLeastLessThan [simp]: "card {l..
proof -
have "{l..x. x + l) ` {..
apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
apply (rule_tac x = "x - l" in exI)
apply arith
done
then have "card {l..
by (simp add: card_image inj_on_def)
then show ?thesis
by simp
qed
lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l"
by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
lemma card_greaterThanLessThan [simp]: "card {l<..
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
lemma subset_eq_atLeast0_lessThan_finite:
fixes n :: nat
assumes "N \ {0..
shows "finite N"
using assms finite_atLeastLessThan by (rule finite_subset)
lemma subset_eq_atLeast0_atMost_finite:
fixes n :: nat
assumes "N \ {0..n}"
shows "finite N"
using assms finite_atLeastAtMost by (rule finite_subset)
lemma ex_bij_betw_nat_finite:
"finite M \ \h. bij_betw h {0..
apply(drule finite_imp_nat_seg_image_inj_on)
apply(auto simp:atLeast0LessThan[symmetric] lessThan_def[symmetric] card_image bij_betw_def)
done
lemma ex_bij_betw_finite_nat:
"finite M \ \h. bij_betw h M {0..
by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
lemma finite_same_card_bij:
"finite A \ finite B \ card A = card B \ \h. bij_betw h A B"
apply(drule ex_bij_betw_finite_nat)
apply(drule ex_bij_betw_nat_finite)
apply(auto intro!:bij_betw_trans)
done
lemma ex_bij_betw_nat_finite_1:
"finite M \ \h. bij_betw h {1 .. card M} M"
by (rule finite_same_card_bij) auto
lemma bij_betw_iff_card:
assumes "finite A" "finite B"
shows "(\f. bij_betw f A B) \ (card A = card B)"
proof
assume "card A = card B"
moreover obtain f where "bij_betw f A {0 ..< card A}"
using assms ex_bij_betw_finite_nat by blast
moreover obtain g where "bij_betw g {0 ..< card B} B"
using assms ex_bij_betw_nat_finite by blast
ultimately have "bij_betw (g \ f) A B"
by (auto simp: bij_betw_trans)
thus "(\f. bij_betw f A B)" by blast
qed (auto simp: bij_betw_same_card)
lemma subset_eq_atLeast0_lessThan_card:
fixes n :: nat
assumes "N \ {0..
shows "card N \ n"
proof -
from assms finite_lessThan have "card N \ card {0..
using card_mono by blast
then show ?thesis by simp
qed
text \<open>Relational version of @{thm [source] card_inj_on_le}:\<close>
lemma card_le_if_inj_on_rel:
assumes "finite B"
"\a. a \ A \ \b. b\B \ r a b"
"\a1 a2 b. \ a1 \ A; a2 \ A; b \ B; r a1 b; r a2 b \ \ a1 = a2"
shows "card A \ card B"
proof -
let ?P = "\a b. b \ B \ r a b"
let ?f = "\a. SOME b. ?P a b"
have 1: "?f ` A \ B" by (auto intro: someI2_ex[OF assms(2)])
have "inj_on ?f A"
proof (auto simp: inj_on_def)
fix a1 a2 assume asms: "a1 \ A" "a2 \ A" "?f a1 = ?f a2"
have 0: "?f a1 \ B" using "1" \a1 \ A\ by blast
have 1: "r a1 (?f a1)" using someI_ex[OF assms(2)[OF \<open>a1 \<in> A\<close>]] by blast
have 2: "r a2 (?f a1)" using someI_ex[OF assms(2)[OF \<open>a2 \<in> A\<close>]] asms(3) by auto
show "a1 = a2" using assms(3)[OF asms(1,2) 0 1 2] .
qed
with 1 show ?thesis using card_inj_on_le[of ?f A B] assms(1) by simp
qed
subsection \<open>Intervals of integers\<close>
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..
by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}"
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
lemma atLeastPlusOneLessThan_greaterThanLessThan_int:
"{l+1..
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
subsubsection \<open>Finiteness\<close>
lemma image_atLeastZeroLessThan_int: "0 \ u ==>
{(0::int)..<u} = int ` {..<nat u}"
unfolding image_def lessThan_def
apply auto
apply (rule_tac x = "nat x" in exI)
apply (auto simp add: zless_nat_eq_int_zless [THEN sym])
done
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..
proof (cases "0 \ u")
case True
then show ?thesis
by (auto simp: image_atLeastZeroLessThan_int)
qed auto
lemma finite_atLeastLessThan_int [iff]: "finite {l..
by (simp only: image_add_int_atLeastLessThan [symmetric, of l] finite_imageI finite_atLeastZeroLessThan_int)
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}"
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
lemma finite_greaterThanLessThan_int [iff]: "finite {l<..
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
subsubsection \<open>Cardinality\<close>
lemma card_atLeastZeroLessThan_int: "card {(0::int)..
proof (cases "0 \ u")
case True
then show ?thesis
by (auto simp: image_atLeastZeroLessThan_int card_image inj_on_def)
qed auto
lemma card_atLeastLessThan_int [simp]: "card {l..
proof -
have "card {l..
apply (subst image_add_int_atLeastLessThan [symmetric])
apply (rule card_image)
apply (simp add: inj_on_def)
done
then show ?thesis
by (simp add: card_atLeastZeroLessThan_int)
qed
lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym])
apply (auto simp add: algebra_simps)
done
lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)"
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
lemma card_greaterThanLessThan_int [simp]: "card {l<..
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
lemma finite_M_bounded_by_nat: "finite {k. P k \ k < (i::nat)}"
proof -
have "{k. P k \ k < i} \ {..
with finite_lessThan[of "i"] show ?thesis by (simp add: finite_subset)
qed
lemma card_less:
assumes zero_in_M: "0 \ M"
shows "card {k \ M. k < Suc i} \ 0"
proof -
from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto
with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)
qed
lemma card_less_Suc2:
assumes "0 \ M" shows "card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"
proof -
have *: "\j \ M; j < Suc i\ \ j - Suc 0 < i \ Suc (j - Suc 0) \ M \ Suc 0 \ j" for j
by (cases j) (use assms in auto)
show ?thesis
proof (rule card_bij_eq)
show "inj_on Suc {k. Suc k \ M \ k < i}"
by force
show "inj_on (\x. x - Suc 0) {k \ M. k < Suc i}"
by (rule inj_on_diff_nat) (use * in blast)
qed (use * in auto)
qed
lemma card_less_Suc:
assumes "0 \ M"
shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"
proof -
have "Suc (card {k. Suc k \ M \ k < i}) = Suc (card {k. Suc k \ M - {0} \ k < i})"
by simp
also have "\ = Suc (card {k \ M - {0}. k < Suc i})"
apply (subst card_less_Suc2)
using assms by auto
also have "\ = Suc (card ({k \ M. k < Suc i} - {0}))"
by (force intro: arg_cong [where f=card])
also have "\ = card (insert 0 ({k \ M. k < Suc i} - {0}))"
by (simp add: card.insert_remove)
also have "... = card {k \ M. k < Suc i}"
using assms
by (force simp add: intro: arg_cong [where f=card])
finally show ?thesis.
qed
subsection \<open>Lemmas useful with the summation operator sum\<close>
text \<open>For examples, see Algebra/poly/UnivPoly2.thy\<close>
subsubsection \<open>Disjoint Unions\<close>
text \<open>Singletons and open intervals\<close>
lemma ivl_disj_un_singleton:
"{l::'a::linorder} Un {l<..} = {l..}"
"{..
"(l::'a::linorder) < u ==> {l} Un {l<..
"(l::'a::linorder) < u ==> {l<..
"(l::'a::linorder) \ u ==> {l} Un {l<..u} = {l..u}"
"(l::'a::linorder) \ u ==> {l..
by auto
text \<open>One- and two-sided intervals\<close>
lemma ivl_disj_un_one:
"(l::'a::linorder) < u ==> {..l} Un {l<..
"(l::'a::linorder) \ u ==> {..
"(l::'a::linorder) \ u ==> {..l} Un {l<..u} = {..u}"
"(l::'a::linorder) \ u ==> {..
"(l::'a::linorder) \ u ==> {l<..u} Un {u<..} = {l<..}"
"(l::'a::linorder) < u ==> {l<..
"(l::'a::linorder) \ u ==> {l..u} Un {u<..} = {l..}"
"(l::'a::linorder) \ u ==> {l..
by auto
text \<open>Two- and two-sided intervals\<close>
lemma ivl_disj_un_two:
"[| (l::'a::linorder) < m; m \ u |] ==> {l<..
"[| (l::'a::linorder) \ m; m < u |] ==> {l<..m} Un {m<..
"[| (l::'a::linorder) \ m; m \ u |] ==> {l..
"[| (l::'a::linorder) \ m; m < u |] ==> {l..m} Un {m<.. |
