(* 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‹Set intervals›
theory Set_Interval imports Parity 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)
lemma card_3_iff: "card S = 3 ⟷ (∃x y z. S = {x,y,z} ∧ x ≠ y ∧ y ≠ z ∧ x ≠ z)" by (fastforce simp: card_Suc_eq numeral_eq_Suc)
context ord begin
definition
lessThan :: "'a ==> 'a set" (‹(‹indent=1 notation=‹mixfix set interval›\›{..<_})›) where "{..
definition
atMost :: "'a ==> 'a set" (‹(‹indent=1 notation=‹mixfix set interval›\›{.._})›) where "{..u} == {x. x ≤ u}"
definition
greaterThan :: "'a ==> 'a set" (‹(‹indent=1 notation=‹mixfix set interval›\›{_<..})›) where "{l<..} == {x. l
definition
atLeast :: "'a ==> 'a set" (‹(‹indent=1 notation=‹mixfix set interval›\›{_..})›) where "{l..} == {x. l≤x}"
definition
greaterThanLessThan :: "'a ==> 'a ==> 'a set" (‹(‹indent=1 notation=‹mixfix set interval›\›{_/<..<_})›) where "{l<..∩ {..
definition
atLeastLessThan :: "'a ==> 'a ==> 'a set" (‹(‹indent=1 notation=‹mixfix set interval›\›{_/..<_})›) where "{l..∩ {..
definition
greaterThanAtMost :: "'a ==> 'a ==> 'a set" (‹(‹indent=1 notation=‹mixfix set interval›\›{_/<.._})›) where "{l<..u} == {l<..} ∩ {..u}"
definition
atLeastAtMost :: "'a ==> 'a ==> 'a set" (‹(‹indent=1 notation=‹mixfix set interval›\›{_/.._})›) where "{l..u} == {l..} ∩ {..u}"
end
text‹A note of warning when using 🍋‹{..🚫› on type 🍋‹nat›: it is equivalent to🍋‹{0::nat..🚫› but some lemmas involving 🍋‹{m..🚫› may not exist in🍋‹{..🚫›-form as well.›
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" by (metis Compl_greaterThan double_complement)
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 ∩ 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‹Logical Equivalences for Set Inclusion and Equality›
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‹Two-sided intervals›
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‹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.›
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‹Emptyness, singletons, subset›
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} ⟷ ((¬ a ≤ b) ∨ c ≤ a ∧ b ≤ d ∧ (c < a ∨ b < d)) ∧ c ≤ 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 (in linorder) Ico_eq_Ico: "{l..∧ h=h' ∨¬ l∧¬ l' by (metis atLeastLessThan_empty_iff2 nle_le not_less ord.atLeastLessThan_iff)
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‹{a..b} = {c}›have"c ≤ a ∧ b ≤ c"by auto with * show"a = b ∧ b = c"by auto qed simp
text‹Quantifiers›
lemma ex_interval_simps: "(∃x ∈ {..⟷ (∃x "(∃x ∈ {..u}. P x) ⟷ (∃x≤u. P x)" "(∃x ∈ {l<..}. P x) ⟷ (∃x>l. P x)" "(∃x ∈ {l..}. P x) ⟷ (∃x≥l. P x)" "(∃x ∈ {l<..⟷ (∃x. l∧ x∧ P x)" "(∃x ∈ {l..⟷ (∃x. l≤x ∧ x∧ P x)" "(∃x ∈ {l<..u}. P x) ⟷ (∃x. l∧ x≤u ∧ P x)" "(∃x ∈ {l..u}. P x) ⟷ (∃x. l≤x ∧ x≤u ∧ P x)" by auto
lemma all_interval_simps: "(∀x ∈ {..⟷ (∀x "(∀x ∈ {..u}. P x) ⟷ (∀x≤u. P x)" "(∀x ∈ {l<..}. P x) ⟷ (∀x>l. P x)" "(∀x ∈ {l..}. P x) ⟷ (∀x≥l. P x)" "(∀x ∈ {l<..⟷ (∀x. l⟶ x⟶ P x)" "(∀x ∈ {l..⟷ (∀x. l≤x ⟶ x⟶ P x)" "(∀x ∈ {l<..u}. P x) ⟷ (∀x. l⟶ x≤u ⟶ P x)" "(∀x ∈ {l..u}. P x) ⟷ (∀x. l≤x ⟶ x≤u ⟶ P x)" by auto
text‹The following results generalise their namesakes in @{theory HOL.Nat} to intervals›
lemma lift_Suc_mono_le_ivl: assumes mono: "∧n. n∈N ==> f n ≤ f (Suc n)" and"n ≤ n'"and subN: "{n..⊆ N" shows"f n ≤ f n'" proof (cases "n < n'") case True thenshow ?thesis using subN proof (induction n n' rule: less_Suc_induct) case (1 i) thenshow ?case by (simp add: mono subsetD) next case (2 i j k) have"f i ≤ f j""f j ≤ f k" using 2 by force+ thenshow ?caseby auto qed next case False with‹n ≤ n'›show ?thesis by auto qed
lemma lift_Suc_antimono_le_ivl: assumes mono: "∧n. n∈N ==> f n ≥ f (Suc n)" and"n ≤ n'"and subN: "{n..⊆ N" shows"f n ≥ f n'" proof (cases "n < n'") case True thenshow ?thesis using subN proof (induction n n' rule: less_Suc_induct) case (1 i) thenshow ?case by (simp add: mono subsetD) next case (2 i j k) have"f i ≥ f j""f j ≥ f k" using 2 by force+ thenshow ?caseby auto qed next case False with‹n ≤ n'›show ?thesis by auto qed
lemma lift_Suc_mono_less_ivl: assumes mono: "∧n. n∈N ==> f n < f (Suc n)" and"n < n'"and subN: "{n..⊆ N" shows"f n < f n'" using‹n 🚫'› using subN proof (induction n n' rule: less_Suc_induct) case (1 i) thenshow ?case by (simp add: mono subsetD) next case (2 i j k) have"f i < f j""f j < f k" using 2 by force+ thenshow ?caseby auto qed
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)
(* 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)
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" proof (cases "a < b") case True assume assm: "{a..⊆ {c.. thenhave 1: "c ≤ a ∧ a ≤ d" using True by (auto simp add: subset_eq Ball_def) thenhave 2: "b ≤ d" using assm by (auto simp add: subset_eq) from 1 2 show ?thesis by simp qed (auto)
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› (is‹?P ⟷ ?Q›) proof assume ?Q thenshow ?P by auto next assume ?P thenhave‹a 🚫∧ x ≤ b ⟷ c 🚫∧ x ≤ d›for x by (simp add: set_eq_iff) from this [of a] this [of b] this [of c] this [of d] show ?Q by auto qed
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 thenobtain k where"f k = m'""m ≤ k"by auto moreoverhave"m' ≤ f m"using f_img by auto ultimatelyshow"f m = m'" using f_mono by (auto elim: monoE[where x=m and y=k]) qed
subsection‹Infinite intervals›
context dense_linorder begin
lemma infinite_Ioo: assumes"a < b" shows"¬ finite {a<.. proof assume fin: "finite {a<.. moreoverhave ne: "{a<..≠ {}" using‹a 🚫›by auto ultimatelyhave"a < Max {a <..< b}""Max {a <..< b} < b" using Max_in[of "{a <..< b}"] by auto thenobtain x where"Max {a <..< b} < x""x < b" using dense[of "Max {a<.. b] by auto thenhave"x ∈ {a <..< b}" using‹a 🚫 {a 🚫🚫}›by auto thenhave"x ≤ Max {a <..< b}" using fin by auto with‹Max {a 🚫🚫} 🚫›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}" thenhave *: "∧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 alsohave"Min {..< a} ≤ x" using‹x 🚫›by fact alsonote‹x 🚫› finallyhave"Min {..< a} ≤ y" by fact with‹y 🚫 {..🚫}›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 <..}" thenhave *: "∧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 alsofrom x have"x ≤ Max {a <..}" by fact alsonote‹Max {a 🚫} 🚫› finallyhave"y ≤ Max { a <..}" by fact with‹Max {a 🚫} 🚫›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 ‹Intersection›
context linorder begin
lemma Icc_minus_Ico [simp]: assumes"a ≤ b" shows"{a..b'} - {a.. using assms by auto
lemma Icc_minus_Ioc [simp]: assumes"a ≤ b" shows"{a'..b} - {a<..b} = {a'..a}" using assms by auto
lemma Icc_minus_Ioo [simp]: assumes"a ≤ b" shows"{a..b} - {a<.. using assms by auto
lemma Int_atLeastAtMost[simp]: "{a..b} ∩ {c..d} = {max a c .. min b d}" by auto
lemma Int_atLeastAtMostR1[simp]: "{..b} ∩ {c..d} = {c .. min b d}" by auto
lemma Int_atLeastAtMostR2[simp]: "{a..} ∩ {c..d} = {max a c .. d}" by auto
lemma Int_atLeastAtMostL1[simp]: "{a..b} ∩ {..d} = {a .. min b d}" by auto
lemma Int_atLeastAtMostL2[simp]: "{a..b} ∩ {c..} = {max a c .. b}" by auto
lemma Int_atLeastLessThan[simp]: "{a..∩ {c.. by auto
lemma Int_greaterThanAtMost[simp]: "{a<..b} ∩ {c<..d} = {max a c <.. min b d}" by auto
lemma Int_greaterThanLessThan[simp]: "{a<..∩ {c<.. 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)
lemma UN_atMost_UNIV: "(∪m::nat. atMost m) = UNIV" by blast
subsubsection ‹The Constant 🍋‹atLeastLessThan›\›
text‹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.›
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‹The analogous result is useful on 🍋‹int›:› (* 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 ‹Intervals and numerals›
lemma lessThan_nat_numeral: 🍋‹Evaluation for specific numerals› "lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))" by (simp add: numeral_eq_Suc lessThan_Suc)
lemma atMost_nat_numeral: 🍋‹Evaluation for specific numerals› "atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))" by (simp add: numeral_eq_Suc atMost_Suc)
lemma atLeastLessThan_nat_numeral: 🍋‹Evaluation for specific numerals› "atLeastLessThan m (numeral k :: nat) = (if m ≤ (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k)) else {})" by (simp add: numeral_eq_Suc atLeastLessThanSuc)
subsubsection ‹Image›
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) thenshow"n = k + (n - k)" by (metis local.add_diff_cancel_left' add_assoc add_commute) qed thenshow ?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" thenhave"i ≤ n - k" by (simp add: add_le_imp_le_diff) have"n = n - k + k" proof - from‹n ∈ ?B›have"n = n - (i + k) + (i + k)" by simp alsohave"… = n - k - i + i + k" by (simp add: algebra_simps) alsohave"… = n - k + k" using‹i ≤ n - k›by simp finallyshow ?thesis . qed moreoverhave"n - k ∈ {i..j}" using‹n ∈ ?B› by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le) ultimatelyshow"n ∈ ?A" by (simp add: ac_simps) qed qed
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}" proof show"{d - b..d - a} ⊆ (-) d ` {a..b}" proof fix x assume"x ∈ {d - b..d - a}" thenhave"d - x ∈ {a..b}"and"x = d - (d - x)" by auto thenshow"x ∈ (-) d ` {a..b}" by (rule rev_image_eqI) qed qed(auto)
lemma image_diff_atLeastLessThan [simp]: fixes a b c::"'a::linordered_idom" shows"(-) c ` {a.. proof - have"(-) c ` {a.. unfolding image_image by simp alsohave"… = {c - b<..c - a}"by simp finallyshow ?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 alsohave"… = {c - b..by simp finallyshow ?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 alsohave"… = {..c - a}"by simp finallyshow ?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 alsohave"… = {c - b..}"by simp finallyshow ?thesis by simp qed
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 moreoverhave"(*) (inverse d) = (\c. c / d)" by (simp add: fun_eq_iff field_simps) ultimatelyshow ?thesis by simp qed
lemma image_mult_atLeastAtMost_if: "(*) c ` {x .. y} = (if c > 0 then {c * x .. c * y} else if x ≤ y then {c * y .. c * x} else {})" proof (cases "c = 0 ∨ x > y") case True thenshow ?thesis by auto next case False thenhave"x ≤ y" by auto from False consider "c < 0"| "c > 0" by (auto simp add: neq_iff) thenshow ?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) thenhave"d ∈ (*) c ` {x..y} ⟷ d / c ∈ (λz. z div c) ` (*) c ` {x..y}" by (subst inj_image_mem_iff) simp_all alsohave"…⟷ d / c ∈ {x..y}" using 1 by (simp add: image_image) alsohave"…⟷ d ∈ {c * y..c * x}" by (auto simp add: field_simps 1) finallyshow"d ∈ (*) c ` {x..y} ⟷ d ∈ {c * y..c * x}" . qed with‹x ≤ y›show ?thesis by auto qed (simp add: mult_left_mono_neg) qed
lemma image_mult_atLeastAtMost_if': "(λx. x * c) ` {x..y} = (if x ≤ 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 ≤ 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 ≤ 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 ≤ 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 ≤ 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.. by safe auto
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 ‹Finiteness›
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‹A bounded set of natural numbers is finite.› lemma bounded_nat_set_is_finite: "(∀i∈N. i < (n::nat)) ==> finite N" by (rule finite_subset [OF _ finite_lessThan]) auto
text‹A set of natural numbers is finite iff it is bounded.› lemma finite_nat_set_iff_bounded: "finite(N::nat set) = (∃m. ∀n∈N. n (is"?F = ?B") proof assume f:?F show ?B using Max_ge[OF ‹?F›, simplified less_Suc_eq_le[symmetric]] by blast next assume ?B show ?F using‹?B›by(blast intro:bounded_nat_set_is_finite) qed
lemma finite_less_ub: "∧f::nat==>nat. (!!n. n ≤ f n) ==> finite {n. f n ≤ u}" by (rule finite_subset[of _ "{..u}"])
(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 thenhave"Max {x. P x} ∈ {x. P x}" using Max_in x by auto thenshow ?thesis by (simp add: ‹finite {x. P x}› that) qed
text‹Any subset of an interval of natural numbers the size of the subset is exactly that interval.›
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 ?caseby auto next case (insert b A) hence *: "b ∉ A"by auto with insert have"A ≤ {k..and"b = k + card A" by fastforce+ with insert * show ?caseby auto qed next case False with assms show ?thesis by simp qed
subsubsection ‹Proving Inclusions and Equalities between Unions›
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" thenobtain 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" thenobtain 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: "(∪i∪i∈{k.. (is"?A = ?B") proof show"?B ⊆ ?A" proof fix x assume"x ∈ ?B" thenobtain i where i: "i ∈ {k.."x ∈ M(i)"by auto thenhave"i - k < n ∧ x ∈ M((i-k) + k)"by auto thenshow"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 subsetI) fix n and a from assms have"(∪i∈{0..⊆ (∪i∈{0.. . moreoverassume"a ∈ (∪i∈{0.. ultimatelyhave"a ∈ (∪i∈{0..by blast thenshow"a ∈ (∪i. B i)"by (auto simp add: UN_UN_finite_eq) qed
lemma UN_finite2_eq: assumes"(∧n::nat. (∪i∈{0..∪i∈{0.. shows"(∪n. A n) = (∪n. B n)" proof (rule subset_antisym [OF UN_finite_subset UN_finite2_subset]) fix n show"∪ (A ` {0..⊆ (∪n. B n)" using assms by auto next fix n show"∪ (B ` {0..⊆∪ (A ` {0.. using assms by (force simp add: atLeastLessThan_add_Un [of 0])+ qed
subsubsection ‹Cardinality›
lemma card_lessThan [simp]: "card {.. by (induct u, simp_all add: lessThan_Suc)
lemma card_atLeastLessThan [simp]: "card {l.. proof - have"(λx. x + l) ` {..⊆ {l.. by auto moreoverhave"{l..⊆ (λx. x + l) ` {.. proof fix x assume *: "x ∈ {l.. thenhave"x - l ∈ {..< u -l}" by auto thenhave"(x - l) + l ∈ (λx. x + l) ` {..< u -l}" by auto thenshow"x ∈ (λx. x + l) ` {.. using * by auto qed ultimatelyhave"{l.. by auto thenhave"card {l.. by (simp add: card_image inj_on_def) thenshow ?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 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" moreoverobtain f where"bij_betw f A {0 ..< card A}" using assms ex_bij_betw_finite_nat by blast moreoverobtain g where"bij_betw g {0 ..< card B} B" using assms ex_bij_betw_nat_finite by blast ultimatelyhave"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 thenshow ?thesis by simp qed
text‹Relational version of @{thm [source] card_inj_on_le}:› 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" unfolding inj_on_def proof safe 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 ‹a1 ∈ A›]] by blast have 2: "r a2 (?f a1)"using someI_ex[OF assms(2)[OF ‹a2 ∈ A›]] 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
lemma inj_on_funpow_least: 🍋‹contributor ‹Lars Noschinski›\‹inj_on (λk. (f ^^ k) s) {0..🚫› if‹(f ^^ n) s = s›‹∧m. 0 🚫==> m 🚫==> (f ^^ m) s ≠ s› proof -
{ fix k l assume A: "k < n""l < n""k ≠ l""(f ^^ k) s = (f ^^ l) s"
define k' l' where"k' = min k l"and"l' = max k l" with A have A': "k' < l'""(f ^^ k') s = (f ^^ l') s""l' < n" by (auto simp: min_def max_def)
have"s = (f ^^ ((n - l') + l')) s"using that ‹l' 🚫›by simp alsohave"… = (f ^^ (n - l')) ((f ^^ l') s)"by (simp add: funpow_add) alsohave"(f ^^ l') s = (f ^^ k') s"by (simp add: A') alsohave"(f ^^ (n - l')) … = (f ^^ (n - l' + k')) s"by (simp add: funpow_add) finallyhave"(f ^^ (n - l' + k')) s = s"by simp moreoverhave"n - l' + k' < n""0 < n - l' + k'"using A' by linarith+ ultimatelyhave False using that(2) by auto
} thenshow ?thesis by (intro inj_onI) auto qed
subsection‹Intervals of integers›
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l.. by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
lemma atLeastPlusOneLessThan_greaterThanLessThan_int: "{l+1.. by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
subsubsection ‹Finiteness›
lemma image_atLeastZeroLessThan_int: assumes"0 ≤ u" shows"{(0::int).. unfolding image_def lessThan_def proof show"{0..⊆ {y. ∃x∈{x. x < nat u}. y = int x}" proof fix x assume"x ∈ {0.. thenhave"x = int (nat x)"and"nat x < nat u" by (auto simp add: zless_nat_eq_int_zless [THEN sym]) thenhave"∃xa using exI[of _ "(nat x)"] by simp thenshow"x ∈ {y. ∃x∈{x. x < nat u}. y = int x}" by simp qed qed (auto)
lemma finite_atLeastZeroLessThan_int: "finite {(0::int).. proof (cases "0 ≤ u") case True thenshow ?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_M_bounded_by_nat: "finite {k. P k ∧ k < (i::nat)}" proof - have"{k. P k ∧ k < i} ⊆ {..by auto 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 alsohave"… = Suc (card {k ∈ M - {0}. k < Suc i})" apply (subst card_less_Suc2) using assms by auto alsohave"… = Suc (card ({k ∈ M. k < Suc i} - {0}))" by (force intro: arg_cong [where f=card]) alsohave"… = card (insert 0 ({k ∈ M. k < Suc i} - {0}))" by (simp add: card.insert_remove) alsohave"... = card {k ∈ M. k < Suc i}" using assms by (force simp add: intro: arg_cong [where f=card]) finallyshow ?thesis. qed
lemma card_le_Suc_Max: "finite S ==> card S ≤ Suc (Max S)" proof (rule classical) assume"finite S"and"¬ Suc (Max S) ≥ card S" thenhave"Suc (Max S) < card S" by simp with‹finite S›have"S ⊆ {0..Max S}" by auto hence"card S ≤ card {0..Max S}" by (intro card_mono; auto) thus"card S ≤ Suc (Max S)" by simp qed
lemma finite_countable_subset: assumes"finite A"and A: "A ⊆ (∪i::nat. B i)" obtains n where"A ⊆ (∪i proof - obtain f where f: "∧x. x ∈ A ==> x ∈ B(f x)" by (metis in_mono UN_iff A)
define n where"n = Suc (Max (f`A))" have"finite (f ` A)" by (simp add: ‹finite A›) thenhave"A ⊆ (∪i unfolding UN_iff f n_def subset_iff by (meson Max_ge f imageI le_imp_less_Suc lessThan_iff) thenshow ?thesis .. qed
lemma finite_countable_equals: assumes"finite A""A = (∪i::nat. B i)" obtains n where"A = (∪i proof - obtain n where"A ⊆ (∪i proof (rule finite_countable_subset) show"A ⊆∪ (range B)" by (force simp: assms) qed (use assms in auto) with that show ?thesis by (force simp: assms) qed
subsection‹Lemmas useful with the summation operator sum›
text‹For examples, see Algebra/poly/UnivPoly2.thy›
subsubsection ‹Disjoint Unions›
text‹Singletons and open intervals›
lemma ivl_disj_un_singleton: "{l::'a::linorder} ∪ {l<..} = {l..}" "{..∪ {u::'a::linorder} = {..u}" "(l::'a::linorder) < u ==> {l} ∪ {l<.. "(l::'a::linorder) < u ==> {l<..∪ {u} = {l<..u}" "(l::'a::linorder) ≤ u ==> {l} ∪ {l<..u} = {l..u}" "(l::'a::linorder) ≤ u ==> {l..∪ {u} = {l..u}" by auto
text‹One- and two-sided intervals›
lemma ivl_disj_un_one: "(l::'a::linorder) < u ==> {..l} ∪ {l<.. "(l::'a::linorder) ≤ u ==> {..∪ {l.. "(l::'a::linorder) ≤ u ==> {..l} ∪ {l<..u} = {..u}" "(l::'a::linorder) ≤ u ==> {..∪ {l..u} = {..u}" "(l::'a::linorder) ≤ u ==> {l<..u} ∪ {u<..} = {l<..}" "(l::'a::linorder) < u ==> {l<..∪ {u..} = {l<..}" "(l::'a::linorder) ≤ u ==> {l..u} ∪ {u<..} = {l..}" "(l::'a::linorder) ≤ u ==> {l..∪ {u..} = {l..}" by auto
text‹Two- and two-sided intervals›
lemma ivl_disj_un_two: "[(l::'a::linorder) < m; m ≤ u]==> {l<..∪ {m.. "[(l::'a::linorder) ≤ m; m < u]==> {l<..m} ∪ {m<.. "[(l::'a::linorder) ≤ m; m ≤ u]==> {l..∪ {m.. "[(l::'a::linorder) ≤ m; m < u]==> {l..m} ∪ {m<.. "[(l::'a::linorder) < m; m ≤ u]==> {l<..∪ {m..u} = {l<..u}" "[(l::'a::linorder) ≤ m; m ≤ u]==> {l<..m} ∪ {m<..u} = {l<..u}" "[(l::'a::linorder) ≤ m; m ≤ u]==> {l..∪ {m..u} = {l..u}" "[(l::'a::linorder) ≤ m; m ≤ u]==> {l..m} ∪ {m<..u} = {l..u}" by auto
lemma ivl_disj_un_two_touch: "[(l::'a::linorder) < m; m < u]==> {l<..m} ∪ {m.. "[(l::'a::linorder) ≤ m; m < u]==> {l..m} ∪ {m.. "[(l::'a::linorder) < m; m ≤ u]==> {l<..m} ∪ {m..u} = {l<..u}" "[(l::'a::linorder) ≤ m; m ≤ u]==> {l..m} ∪ {m..u} = {l..u}" by auto
lemma (in linorder) lessThan_minus_lessThan [simp]: "{..< n} - {..< m} = {m ..< n}" by auto
lemma (in linorder) atLeastAtMost_diff_ends: "{a..b} - {a, b} = {a<.. by auto
subsubsection ‹Some Subset Conditions›
lemma ivl_subset [simp]: "({i..⊆ {m..≤ i ∨ m ≤ i ∧ j ≤ (n::'a::linorder))" using linorder_class.le_less_linear[of i n] by safe (force intro: leI)+
subsection‹Generic big monoid operation over intervals›
context semiring_char_0 begin
lemma inj_on_of_nat [simp]: "inj_on of_nat N" by (rule inj_onI) simp
lemma bij_betw_of_nat [simp]: "bij_betw of_nat N A ⟷ of_nat ` N = A" by (simp add: bij_betw_def)
lemma Nats_infinite: "infinite (ℕ :: 'a set)" by (metis Nats_def finite_imageD infinite_UNIV_char_0 inj_on_of_nat)
end
context comm_monoid_set begin
lemma atLeastLessThan_reindex: "F g {h m..∘ h) {m.. if"bij_betw h {m..for m n ::nat proof - from that have"inj_on h {m..and"h ` {m.. by (simp_all add: bij_betw_def) thenshow ?thesis using reindex [of h "{m.. g] by simp qed
lemma atLeastAtMost_reindex: "F g {h m..h n} = F (g ∘ h) {m..n}" if"bij_betw h {m..n} {h m..h n}"for m n ::nat proof - from that have"inj_on h {m..n}"and"h ` {m..n} = {h m..h n}" by (simp_all add: bij_betw_def) thenshow ?thesis using reindex [of h "{m..n}" g] by simp qed
lemma atLeastLessThan_shift_bounds: "F g {m + k..∘ plus k) {m.. for m n k :: nat using atLeastLessThan_reindex [of "plus k" m n g] by (simp add: ac_simps)
lemma atLeastAtMost_shift_bounds: "F g {m + k..n + k} = F (g ∘ plus k) {m..n}" for m n k :: nat using atLeastAtMost_reindex [of "plus k" m n g] by (simp add: ac_simps)
lemma atLeast_Suc_lessThan_Suc_shift: "F g {Suc m..∘ Suc) {m.. using atLeastLessThan_shift_bounds [of _ _ 1] by (simp add: plus_1_eq_Suc)
lemma atLeast_Suc_atMost_Suc_shift: "F g {Suc m..Suc n} = F (g ∘ Suc) {m..n}" using atLeastAtMost_shift_bounds [of _ _ 1] by (simp add: plus_1_eq_Suc)
lemma atLeast_atMost_pred_shift: "F (g ∘ (λn. n - Suc 0)) {Suc m..Suc n} = F g {m..n}" unfolding atLeast_Suc_atMost_Suc_shift by simp
lemma atLeast_lessThan_pred_shift: "F (g ∘ (λn. n - Suc 0)) {Suc m.. unfolding atLeast_Suc_lessThan_Suc_shift by simp
lemma atLeast_int_lessThan_int_shift: "F g {int m..∘ int) {m.. by (rule atLeastLessThan_reindex)
(simp add: image_int_atLeastLessThan)
lemma atLeast_int_atMost_int_shift: "F g {int m..int n} = F (g ∘ int) {m..n}" by (rule atLeastAtMost_reindex)
(simp add: image_int_atLeastAtMost)
lemma atLeast0_lessThan_Suc: "F g {0..🪙* g n" by (simp add: atLeast0_lessThan_Suc ac_simps)
lemma atLeast0_atMost_Suc: "F g {0..Suc n} = F g {0..n} 🪙* g (Suc n)" by (simp add: atLeast0_atMost_Suc ac_simps)
lemma atLeast0_lessThan_Suc_shift: "F g {0..🪙* F (g ∘ Suc) {0.. by (simp add: atLeast0_lessThan_Suc_eq_insert_0 atLeast_Suc_lessThan_Suc_shift)
lemma atLeast0_atMost_Suc_shift: "F g {0..Suc n} = g 0 🪙* F (g ∘ Suc) {0..n}" by (simp add: atLeast0_atMost_Suc_eq_insert_0 atLeast_Suc_atMost_Suc_shift)
lemma atLeast_Suc_lessThan: "F g {m..🪙* F g {Suc m..if"m < n" proof - from that have"{m.. by auto thenshow ?thesis by simp qed
lemma atLeast_Suc_atMost: "F g {m..n} = g m 🪙* F g {Suc m..n}"if"m ≤ n" proof - from that have"{m..n} = insert m {Suc m..n}" by auto thenshow ?thesis by simp qed
lemma ivl_cong: "a = c ==> b = d ==> (∧x. c ≤ x ==> x < d ==> g x = h x) ==> F g {a.. by (rule cong) simp_all
lemma atLeastLessThan_shift_0: fixes m n p :: nat shows"F g {m..∘ plus m) {0.. using atLeastLessThan_shift_bounds [of g 0 m "n - m"] by (cases "m ≤ n") simp_all
lemma atLeastAtMost_shift_0: fixes m n p :: nat assumes"m ≤ n" shows"F g {m..n} = F (g ∘ plus m) {0..n - m}" using assms atLeastAtMost_shift_bounds [of g 0 m "n - m"] by simp
lemma atLeastLessThan_concat: fixes m n p :: nat shows"m ≤ n ==> n ≤ p ==> F g {m..🪙* F g {n.. by (simp add: union_disjoint [symmetric] ivl_disj_un)
lemma atLeastLessThan_rev: "F g {n.. by (rule reindex_bij_witness [where i="λi. m + n - Suc i"and j="λi. m + n - Suc i"], auto)
lemma atLeastAtMost_rev: fixes n m :: nat shows"F g {n..m} = F (λi. g (m + n - i)) {n..m}" by (rule reindex_bij_witness [where i="λi. m + n - i"and j="λi. m + n - i"]) auto
lemma atLeastLessThan_rev_at_least_Suc_atMost: "F g {n.. unfolding atLeastLessThan_rev [of g n m] by (cases m) (simp_all add: atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost)
syntax (latex_sum output) "_from_to_sum" :: "idt ==> 'a ==> 'a ==> 'b ==> 'b"
(‹(3🍋‹$\sum_{›_ = _🍋‹}^{›_🍋‹}$›_)› [0,0,0,10] 10) "_from_upto_sum" :: "idt ==> 'a ==> 'a ==> 'b ==> 'b"
(‹(3🍋‹$\sum_{›_ = _🍋‹}^{🚫close>_🍋‹}$›_)›[0,0,0,10] 10) "_upt_sum" :: "idt ==> 'a ==> 'b ==> 'b" (‹(3🍋‹$\sum_{›_🚫🍋‹}$›_)›[0,0,10] 10) "_upto_sum" :: "idt ==> 'a ==> 'b ==> 'b" (‹(3🍋‹$\sum_{›_≤ _🍋‹}$›_)›[0,0,10] 10) syntax "_from_to_sum" :: "idt ==> 'a ==> 'a ==> 'b ==> 'b" (‹(‹indent=3 notation=‹binder ∑›\›\∑_ = _.._./ _)›[0,0,0,10] 10) "_from_upto_sum" :: "idt ==> 'a ==> 'a ==> 'b ==> 'b" (‹(‹indent=3 notation=‹binder ∑›\›\∑_ = _..🚫/ _)› [0,0,0,10] 10) "_upt_sum" :: "idt ==> 'a ==> 'b ==> 'b" (‹(‹indent=3 notation=‹binder ∑›\›\∑_🚫/ _)› [0,0,10] 10) "_upto_sum" :: "idt ==> 'a ==> 'b ==> 'b" (‹(‹indent=3 notation=‹binder ∑›\›\∑_≤_./ _)› [0,0,10] 10) syntax_consts "_from_to_sum" "_from_upto_sum" "_upt_sum" "_upto_sum" == sum translations "∑x=a..b. t" == "CONST sum (λx. t) {a..b}" "∑x=a..🚫 t" == "CONST sum (λx. t) {a..🚫" "∑i≤n. t" == "CONST sum (λi. t) {..n}" "∑i🚫 t" == "CONST sum (λi. t) {..🚫" text‹The above introduces some pretty alternative syntaxes for summation over intervals: \begin{center} \begin{tabular}{lll} Old & New & \LaTeX\\ @{term[source]"∑x∈{a..b}. e"} & k='alert("undefinierte Formatierung term");' ontouchend='alert("undefinierte Formatierung term");' >🍋‹∑x=a..b. e›& @{term[mode=latex_sum]"∑x=a..b. e"}\\ @{term[source]"∑x∈{a..🚫. e"} & k='alert("undefinierte Formatierung term");' ontouchend='alert("undefinierte Formatierung term");' >🍋‹∑x=a..🚫 e›& @{term[mode=latex_sum]"∑x=a..🚫 e"}\\ @{term[source]"∑x∈{..b}. e"} & ='alert("undefinierte Formatierung term");' ontouchend='alert("undefinierte Formatierung term");' >🍋‹∑x≤b. e›& @{term[mode=latex_sum]"∑x≤b. e"}\\ @{term[source]"∑x∈{..🚫. e"} & ='alert("undefinierte Formatierung term");' ontouchend='alert("undefinierte Formatierung term");' >🍋‹∑x🚫 e›& @{term[mode=latex_sum]"∑x🚫 e"} \end{tabular} \end{center} The left column shows the term before introduction of the new syntax, the middle column shows the new (default) syntax, and the right column shows a special syntax. The latter is only meaningful for latex output and has to be activated explicitly by setting the print mode to ‹latex_sum›(e.g.\ via ‹mode = latex_sum› in antiquotations). It is not the default \LaTeX\ output because it only works well with italic-style formulae, not tt-style. Note that for uniformity on 🍋‹nat›it is better to use 🍋‹∑x::nat=0..🚫 e›rather than ‹∑x🚫 e›: ‹sum› may not provide all lemmas available for 🍋‹{m..🚫›also in the special form for 🍋‹{..🚫›.› text‹This congruence rule should be used for sums over intervals as the standard theorem @{text[source]sum.cong} does not work well with the simplifier who adds the unsimplified premise 🍋‹x∈B›to the context.› context comm_monoid_set begin lemma zero_middle: assumes "1 ≤ p" "k ≤ p" shows "F (λj. if j 🚫 then g j else if j = k then 🪙1 else h (j - Suc 0)) {..p} = F (λj. if j 🚫 then g j else h j) {..p - Suc 0}" (is "?lhs = ?rhs") proof - have [simp]: "{..p - Suc 0} ∩ {j. j 🚫} = {..🚫" "{..p - Suc 0} ∩ - {j. j 🚫} = {k..p - Suc 0}" using assms by auto have "?lhs = F g {..🚫🪙* F (λj. if j = k then 🪙1 else h (j - Suc 0)) {k..p}" using union_disjoint [of "{..🚫" "{k..p}"] assms by (simp add: ivl_disj_int_one ivl_disj_un_one) also have "… = F g {..🚫🪙* F (λj. h (j - Suc 0)) {Suc k..p}" by (simp add: atLeast_Suc_atMost [of k p] assms) also have "… = F g {..🚫🪙* F h {k .. p - Suc 0}" using reindex [of Suc "{k..p - Suc 0}"] assms by simp also have "… = ?rhs" by (simp add: If_cases) finally show ?thesis . qed lemma atMost_Suc [simp]: "F g {..Suc n} = F g {..n} 🪙* g (Suc n)" by (simp add: atMost_Suc ac_simps) lemma lessThan_Suc [simp]: "F g {..🚫n} = F g {..🚫🪙* g n" by (simp add: lessThan_Suc ac_simps) lemma cl_ivl_Suc [simp]: "F g {m..Suc n} = (if Suc n 🚫 then 🪙1 else F g {m..n} 🪙* g(Suc n))" by (auto simp: ac_simps atLeastAtMostSuc_conv) lemma op_ivl_Suc [simp]: "F g {m..🚫n} = (if n 🚫 then 🪙1 else F g {m..🚫🪙* g(n))" by (auto simp: ac_simps atLeastLessThanSuc) lemma head: fixes n :: nat assumes mn: "m ≤ n" shows "F g {m..n} = g m 🪙* F g {m🚫n}" (is "?lhs = ?rhs") proof - from mn have "{m..n} = {m} ∪ {m🚫n}" by (auto intro: ivl_disj_un_singleton) hence "?lhs = F g ({m} ∪ {m🚫n})" by (simp add: atLeast0LessThan) also have "… = ?rhs" by simp finally show ?thesis . qed lemma last_plus: fixes n::nat shows "m ≤ n ==> F g {m..n} = g n 🪙* F g {m..🚫" by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost commute) lemma head_if: fixes n :: nat shows "F g {m..n} = (if n 🚫 then 🪙1 else F g {m..🚫🪙* g(n))" by (simp add: commute last_plus) lemma ub_add_nat: assumes "(m::nat) ≤ n + 1" shows "F g {m..n + p} = F g {m..n} 🪙* F g {n + 1..n + p}" proof- have "{m .. n+p} = {m..n} ∪ {n+1..n+p}" using ‹m ≤ n+1›by auto thus ?thesis by (auto simp: ivl_disj_int union_disjoint atLeastSucAtMost_greaterThanAtMost) qed lemma nat_group: fixes k::nat shows "F (λm. F g {m * k ..🚫*k + k}) {..🚫 = F g {..🚫 * k}" proof (cases k) case (Suc l) then have "k > 0" by auto then show ?thesis by (induct n) (simp_all add: atLeastLessThan_concat add.commute atLeast0LessThan[symmetric]) qed auto lemma triangle_reindex: fixes n :: nat shows "F (λ(i,j). g i j) {(i,j). i+j 🚫} = F (λk. F (λi. g i (k - i)) {..k}) {..??" apply (simp add: Sigma) apply (rule reindex_bij_witness[where j="λ(i, j). (i+j, i)" and i="λ(k, i). (i, k - i)"]) apply auto done lemma triangle_reindex_eq: fixes n :: nat shows "F (λ(i,j). g i j) {(i,j). i+j ≤ n} = F (λk. F (λi. g i (k - i)) {..k}) {..n}" using triangle_reindex [of g "Suc n"] by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost) lemma nat_diff_reindex: "F (λi. g (n - Suc i)) {..🚫 = F g {..🚫" by (rule reindex_bij_witness[where i="λi. n - Suc i" and j="λi. n - Suc i"]) auto lemma shift_bounds_nat_ivl: "F g {m+k..🚫k} = F (λi. g(i + k)){m..🚫:nat}" by (induct "n", auto simp: atLeastLessThanSuc) lemma shift_bounds_cl_nat_ivl: "F g {m+k..n+k} = F (λi. g(i + k)){m..n::nat}" by (rule reindex_bij_witness[where i="λi. i + k" and j="λi. i - k"]) auto corollary shift_bounds_cl_Suc_ivl: "F g {Suc m..Suc n} = F (λi. g(Suc i)){m..n}" by (simp add: shift_bounds_cl_nat_ivl[where k="Suc 0", simplified]) corollary Suc_reindex_ivl: "m ≤ n ==> F g {m..n} 🪙* g (Suc n) = g m 🪙* F (λi. g (Suc i)) {m..n}" by (simp add: assoc atLeast_Suc_atMost flip: shift_bounds_cl_Suc_ivl) corollary shift_bounds_Suc_ivl: "F g {Suc m..🚫n} = F (λi. g(Suc i)){m..🚫" by (simp add: shift_bounds_nat_ivl[where k="Suc 0", simplified]) lemma atMost_Suc_shift: shows "F g {..Suc n} = g 0 🪙* F (λi. g (Suc i)) {..n}" proof (induct n) case 0 show ?case by simp next case (Suc n) note IH = this have "F g {..Suc (Suc n)} = F g {..Suc n} 🪙* g (Suc (Suc n))" by (rule atMost_Suc) also have "F g {..Suc n} = g 0 🪙* F (λi. g (Suc i)) {..n}" by (rule IH) also have "g 0 🪙* F (λi. g (Suc i)) {..n} 🪙* g (Suc (Suc n)) = g 0 🪙* (F (λi. g (Suc i)) {..n} 🪙* g (Suc (Suc n)))" by (rule assoc) also have "F (λi. g (Suc i)) {..n} 🪙* g (Suc (Suc n)) = F (λi. g (Suc i)) {..Suc n}" by (rule atMost_Suc [symmetric]) finally show ?case . qed lemma lessThan_Suc_shift: "F g {..🚫n} = g 0 🪙* F (λi. g (Suc i)) {..🚫" by (induction n) (simp_all add: ac_simps) lemma atMost_shift: "F g {..n} = g 0 🪙* F (λi. g (Suc i)) {..🚫" by (metis atLeast0AtMost atLeast0LessThan atLeastLessThanSuc_atLeastAtMost atLeastSucAtMost_greaterThanAtMost le0 head shift_bounds_Suc_ivl) lemma nested_swap: "F (λi. F (λj. a i j) {0..🚫) {0..n} = F (λj. F (λi. a i j) {Suc j..n}) {0..🚫" by (induction n) (auto simp: distrib) lemma nested_swap': "F (λi. F (λj. a i j) {..🚫) {..n} = F (λj. F (λi. a i j) {Suc j..n}) {..🚫" by (induction n) (auto simp: distrib) lemma atLeast1_atMost_eq: "F g {Suc 0..n} = F (λk. g (Suc k)) {..🚫" proof - have "F g {Suc 0..n} = F g (Suc ` {..🚫)" by (simp add: image_Suc_lessThan) also have "… = F (λk. g (Suc k)) {..🚫" by (simp add: reindex) finally show ?thesis . qed lemma atLeastLessThan_Suc: "a ≤ b ==> F g {a..🚫b} = F g {a..🚫🪙* g b" by (simp add: atLeastLessThanSuc commute) lemma nat_ivl_Suc': assumes "m ≤ Suc n" shows "F g {m..Suc n} = g (Suc n) 🪙* F g {m..n}" proof - from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto also have "F g … = g (Suc n) 🪙* F g {m..n}" by simp finally show ?thesis . qed lemma in_pairs: "F g {2*m..Suc(2*n)} = F (λi. g(2*i) 🪙* g(Suc(2*i))) {m..n}" proof (induction n) case 0 show ?case by (cases "m=0") auto next case (Suc n) then show ?case by (auto simp: assoc split: if_split_asm) qed lemma in_pairs_0: "F g {..Suc(2*n)} = F (λi. g(2*i) 🪙* g(Suc(2*i))) {..n}" using in_pairs [of _ 0 n] by (simp add: atLeast0AtMost) end lemma card_sum_le_nat_sum: "∑ {0..🚫S} ≤∑ S" proof (cases "finite S") case True then show ?thesis proof (induction "card S" arbitrary: S) case (Suc x) then have "Max S ≥ x" using card_le_Suc_Max by fastforce let ?S' = "S - {Max S}" from Suc have "Max S ∈ S" by (auto intro: Max_in) hence cards: "card S = Suc (card ?S')" using ‹finite S›by (intro card.remove; auto) hence "∑ {0..🚫?S'} ≤∑ ?S'" using Suc by (intro Suc; auto) hence "∑ {0..🚫?S'} + x ≤∑ ?S' + Max S" using ‹Max S ≥ x›by simp also have "... = ∑ S" using sum.remove[OF ‹finite S›‹Max S ∈ S›, where g="λx. x"] by simp finally show ?case using cards Suc by auto qed simp qed simp lemma sum_natinterval_diff: fixes f:: "nat ==> ('a::ab_group_add)" shows "sum (λk. f k - f(k + 1)) {(m::nat) .. n} = (if m ≤ n then f m - f(n + 1) else 0)" by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) lemma sum_diff_nat_ivl: fixes f :: "nat ==> 'a::ab_group_add" shows "[ m ≤ n; n ≤ p ]==> sum f {m..🚫 - sum f {m..🚫 = sum f {n..🚫" using sum.atLeastLessThan_concat [of m n p f,symmetric] by (simp add: ac_simps) lemma sum_diff_distrib: "∀x. Q x ≤ P x ==> (∑x🚫 P x) - (∑x🚫 Q x) = (∑x🚫 P x - Q x :: nat)" by (subst sum_subtractf_nat) auto subsubsection ‹Shifting bounds› context comm_monoid_add begin context fixes f :: "nat ==> 'a" assumes "f 0 = 0" begin lemma sum_shift_lb_Suc0_0_upt: "sum f {Suc 0..🚫 = sum f {0..🚫" proof (cases k) case 0 then show ?thesis by simp next case (Suc k) moreover have "{0..🚫k} = insert 0 {Suc 0..🚫k}" by auto ultimately show ?thesis using ‹f 0 = 0›by simp qed lemma sum_shift_lb_Suc0_0: "sum f {Suc 0..k} = sum f {0..k}" proof (cases k) case 0 with ‹f 0 = 0›show ?thesis by simp next case (Suc k) moreover have "{0..Suc k} = insert 0 {Suc 0..Suc k}" by auto ultimately show ?thesis using ‹f 0 = 0›by simp qed end end lemma sum_Suc_diff: fixes f :: "nat ==> 'a::ab_group_add" assumes "m ≤ Suc n" shows "(∑i = m..n. f(Suc i) - f i) = f (Suc n) - f m" using assms by (induct n) (auto simp: le_Suc_eq) lemma sum_Suc_diff': fixes f :: "nat ==> 'a::ab_group_add" assumes "m ≤ n" shows "(∑i = m..🚫 f (Suc i) - f i) = f n - f m" using assms by (induct n) (auto simp: le_Suc_eq) lemma sum_diff_split: fixes f:: "nat ==> 'a::ab_group_add" assumes "m ≤ n" shows "(∑i≤n. f i) - (∑i🚫 f i) = (∑i≤n - m. f(n - i))" proof - have "∧i. i ≤ n-m ==>∃k≥m. k ≤ n ∧ i = n-k" by (metis Nat.le_diff_conv2 add.commute ‹m≤n›diff_diff_cancel diff_le_self order.trans) then have eq: "{..n-m} = (-)n ` {m..n}" by force have inj: "inj_on ((-)n) {m..n}" by (auto simp: inj_on_def) have "(∑i≤n - m. f(n - i)) = (∑i=m..n. f i)" by (simp add: eq sum.reindex_cong [OF inj]) also have "… = (∑i≤n. f i) - (∑i🚫 f i)" using sum_diff_nat_ivl[of 0 "m" "Suc n" f] assms by (simp only: atLeast0AtMost atLeast0LessThan atLeastLessThanSuc_atLeastAtMost) finally show ?thesis by metis qed lemma prod_divide_nat_ivl: fixes f :: "nat ==> 'a::idom_divide" shows "[ m ≤ n; n ≤ p; prod f {m..🚫≠ 0]==> prod f {m..🚫 div prod f {m..🚫= prod f {n..🚫" using prod.atLeastLessThan_concat [of m n p f,symmetric] by (simp add: ac_simps) lemma prod_divide_split: (*FIXME: why is \<Prod> syntax not available?*) fixes f:: "nat ==> 'a::idom_divide" assumes"m ≤ n""prod f {..≠ 0" shows"(prod f {..n}) div (prod f {.. proof - have"∧i. i ≤ n-m ==>∃k≥m. k ≤ n ∧ i = n-k" by (metis Nat.le_diff_conv2 add.commute ‹m≤n› diff_diff_cancel diff_le_self order.trans) thenhave eq: "{..n-m} = (-)n ` {m..n}" by force have inj: "inj_on ((-)n) {m..n}" by (auto simp: inj_on_def) have"prod (λi. f(n - i)) {..n - m} = prod f {m..n}" by (simp add: eq prod.reindex_cong [OF inj]) alsohave"… = prod f {..n} div prod f {.. using prod_divide_nat_ivl[of 0 "m""Suc n" f] assms by (force simp: atLeast0AtMost atLeast0LessThan atLeastLessThanSuc_atLeastAtMost) finallyshow ?thesis by metis qed
subsubsection ‹Telescoping sums›
lemma sum_telescope: fixes f::"nat ==> 'a::ab_group_add" shows"sum (λi. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)" by (induct i) simp_all
lemma sum_telescope'': assumes"m ≤ n" shows"(∑k∈{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)" by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)
lemma sum_lessThan_telescope: "(∑n by (induction m) (simp_all add: algebra_simps)
lemma sum_lessThan_telescope': "(∑n by (induction m) (simp_all add: algebra_simps)
subsubsection ‹The formula for geometric sums›
lemma sum_power2: "(∑i=0.. by (induction k) (auto simp: mult_2)
lemma geometric_sum: assumes"x ≠ 1" shows"(∑i proof - from assms obtain y where"y = x - 1"and"y ≠ 0"by simp_all moreoverhave"(∑i by (induct n) (simp_all add: field_simps ‹y ≠ 0›) ultimatelyshow ?thesis by simp qed
lemma geometric_sum_less: assumes"0 < x""x < 1""finite S" shows"(∑i∈S. x ^ i) < 1 / (1 - x::'a::linordered_field)" proof -
define n where"n ≡ Suc (Max S)" have"(∑i∈S. x ^ i) ≤ (∑i unfolding n_def using assms by (fastforce intro!: sum_mono2 le_imp_less_Suc) alsohave"… = (1 - x ^ n) / (1 - x)" using assms by (simp add: geometric_sum field_simps) alsohave"… < 1 / (1-x)" using assms by (simp add: field_simps power_Suc_less) finallyshow ?thesis . qed
lemma diff_power_eq_sum: fixes y :: "'a::{comm_ring,monoid_mult}" shows "x ^ (Suc n) - y ^ (Suc n) = (x - y) * (∑p proof (induct n) case (Suc n) have"x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x^n) - y * (y * y ^ n)" by simp alsohave"... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)" by (simp add: algebra_simps) alsohave"... = y * ((x - y) * (∑p by (simp only: Suc) alsohave"... = (x - y) * (y * (∑p by (simp only: mult.left_commute) alsohave"... = (x - y) * (∑p by (simp add: field_simps Suc_diff_le sum_distrib_right sum_distrib_left) finallyshow ?case . qed simp
corollary power_diff_sumr2: 🍋‹‹COMPLEX_POLYFUN›in HOL Light› fixes x :: "'a::{comm_ring,monoid_mult}" shows"x^n - y^n = (x - y) * (∑i using diff_power_eq_sum[of x "n - 1" y] by (cases "n = 0") (simp_all add: field_simps)
lemma power_diff_1_eq: fixes x :: "'a::{comm_ring,monoid_mult}" shows"x^n - 1 = (x - 1) * (∑i using diff_power_eq_sum [of x _ 1] by (cases n) auto
lemma one_diff_power_eq': fixes x :: "'a::{comm_ring,monoid_mult}" shows"1 - x^n = (1 - x) * (∑i using diff_power_eq_sum [of 1 _ x] by (cases n) auto
lemma one_diff_power_eq: fixes x :: "'a::{comm_ring,monoid_mult}" shows"1 - x^n = (1 - x) * (∑i by (metis one_diff_power_eq' sum.nat_diff_reindex)
lemma sum_gp: fixes x :: "'a::{comm_ring,division_ring}" shows"(∑i=m..n. x^i) = (if n < m then 0 else if x = 1 then of_nat((n + 1) - m) else (x^m - x^Suc n) / (1 - x))" proof (cases "n < m") case False assume *: "¬ n < m" thenshow ?thesis proof (cases "x = 1") case False assume"x ≠ 1" thenhave not_zero: "1 - x ≠ 0" by auto have"(1 - x) * (∑i=m..n. x^i) = x ^ m - x * x ^ n" using sum_gp_multiplied [of m n x] * by auto thenhave"(∑i=m..n. x^i) = (x ^ m - x * x ^ n) / (1 - x) " using nonzero_divide_eq_eq mult.commute not_zero by metis thenshow ?thesis by auto qed (auto) qed (auto)
subsubsection‹Geometric progressions›
lemma sum_gp0: fixes x :: "'a::{comm_ring,division_ring}" shows"(∑i≤n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))" using sum_gp_basic[of x n] by (simp add: mult.commute field_split_simps)
lemma sum_power_add: fixes x :: "'a::{comm_ring,monoid_mult}" shows"(∑i∈I. x^(m+i)) = x^m * (∑i∈I. x^i)" by (simp add: sum_distrib_left power_add)
lemma sum_gp_offset: fixes x :: "'a::{comm_ring,division_ring}" shows"(∑i=m..m+n. x^i) = (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" using sum_gp [of x m "m+n"] by (auto simp: power_add algebra_simps)
lemma sum_gp_strict: fixes x :: "'a::{comm_ring,division_ring}" shows"(∑i by (induct n) (auto simp: algebra_simps field_split_simps)
subsubsection ‹The formulae for arithmetic sums›
context comm_semiring_1 begin
lemma double_gauss_sum: "2 * (∑i = 0..n. of_nat i) = of_nat n * (of_nat n + 1)" by (induct n) (simp_all add: sum.atLeast0_atMost_Suc algebra_simps left_add_twice)
lemma double_gauss_sum_from_Suc_0: "2 * (∑i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1)" proof - have"sum of_nat {Suc 0..n} = sum of_nat (insert 0 {Suc 0..n})" by simp alsohave"… = sum of_nat {0..n}" by (cases n) (simp_all add: atLeast0_atMost_Suc_eq_insert_0) finallyshow ?thesis by (simp add: double_gauss_sum) qed
lemma double_arith_series: "2 * (∑i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d)" proof - have"(∑i = 0..n. a + of_nat i * d) = ((∑i = 0..n. a) + (∑i = 0..n. of_nat i * d))" by (rule sum.distrib) alsohave"… = (of_nat (Suc n) * a + d * (∑i = 0..n. of_nat i))" by (simp add: sum_distrib_left algebra_simps) finallyshow ?thesis by (simp add: algebra_simps double_gauss_sum left_add_twice) qed
end
context linordered_euclidean_semiring begin
lemma gauss_sum: "(∑i = 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2" using double_gauss_sum [of n, symmetric] by simp
lemma gauss_sum_from_Suc_0: "(∑i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2" using double_gauss_sum_from_Suc_0 [of n, symmetric] by simp
lemma arith_series: "(∑i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d) div 2" using double_arith_series [of a d n, symmetric] by simp
end
lemma gauss_sum_nat: "∑{0..n} = (n * Suc n) div 2" using gauss_sum [of n, where ?'a = nat] by simp
lemma arith_series_nat: "(∑i = 0..n. a + i * d) = Suc n * (2 * a + n * d) div 2" using arith_series [of a d n] by simp
lemma Sum_Icc_int: "∑{m..n} = (n * (n + 1) - m * (m - 1)) div 2" if"m ≤ n"for m n :: int using that proof (induct i ≡"nat (n - m)" arbitrary: m n) case 0 thenhave"m = n" by arith thenshow ?case by (simp add: algebra_simps mult_2 [symmetric]) next case (Suc i) have 0: "i = nat((n-1) - m)""m ≤ n-1"using Suc(2,3) by arith+ have"∑ {m..n} = ∑ {m..1+(n-1)}"by simp alsohave"… = ∑ {m..n-1} + n"using‹m ≤ n› by(subst atLeastAtMostPlus1_int_conv) simp_all alsohave"… = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n" by(simp add: Suc(1)[OF 0]) alsohave"… = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2"by simp alsohave"… = (n*(n+1) - m*(m-1)) div 2" by (simp add: algebra_simps mult_2_right) finallyshow ?case . qed
lemma Sum_Icc_nat: "∑{m..n} = (n * (n + 1) - m * (m - 1)) div 2"for m n :: nat proof (cases "m ≤ n") case True thenhave *: "m * (m - 1) ≤ n * (n + 1)" by (meson diff_le_self order_trans le_add1 mult_le_mono) have"int (∑{m..n}) = (∑{int m..int n})" by (simp add: sum.atLeast_int_atMost_int_shift) alsohave"… = (int n * (int n + 1) - int m * (int m - 1)) div 2" using‹m ≤ n›by (simp add: Sum_Icc_int) alsohave"… = int ((n * (n + 1) - m * (m - 1)) div 2)" using le_square * by (simp add: algebra_simps of_nat_div of_nat_diff) finallyshow ?thesis by (simp only: of_nat_eq_iff) next case False thenshow ?thesis by (auto dest: less_imp_Suc_add simp add: not_le algebra_simps) qed
lemma Sum_Ico_nat: "∑{m..for m n :: nat by (cases n) (simp_all add: atLeastLessThanSuc_atLeastAtMost Sum_Icc_nat)
subsubsection ‹Division remainder›
lemma range_mod: fixes n :: nat assumes"n > 0" shows"range (λm. m mod n) = {0.. (is"?A = ?B") proof (rule set_eqI) fix m show"m ∈ ?A ⟷ m ∈ ?B" proof assume"m ∈ ?A" with assms show"m ∈ ?B" by auto next assume"m ∈ ?B" moreoverhave"m mod n ∈ ?A" by (rule rangeI) ultimatelyshow"m ∈ ?A" by simp qed qed
syntax (latex_prod output) "_from_to_prod" :: "idt ==> 'a ==> 'a ==> 'b ==> 'b"
(‹(3🍋‹$\prod_{›_ = _🍋‹}^{›_🍋‹}$› _)› [0,0,0,10] 10) "_from_upto_prod" :: "idt ==> 'a ==> 'a ==> 'b ==> 'b"
(‹(3🍋‹$\prod_{›_ = _🍋‹}^{🚫close>_🍋‹}$›_)› [0,0,0,10] 10) "_upt_prod" :: "idt ==> 'a ==> 'b ==> 'b" (‹(3🍋‹$\prod_{›_🚫🍋‹}$› _)› [0,0,10] 10) "_upto_prod" :: "idt ==> 'a ==> 'b ==> 'b" (‹(3🍋‹$\prod_{›_≤ _🍋‹}$› _)› [0,0,10] 10) syntax "_from_to_prod" :: "idt ==> 'a ==> 'a ==> 'b ==> 'b" (‹(‹indent=3 notation=‹binder ∏›\›\∏_ = _.._./ _)› [0,0,0,10] 10) "_from_upto_prod" :: "idt ==> 'a ==> 'a ==> 'b ==> 'b" (‹(‹indent=3 notation=‹binder ∏›\›\∏_ = _..🚫/ _)› [0,0,0,10] 10) "_upt_prod" :: "idt ==> 'a ==> 'b ==> 'b" (‹(‹indent=3 notation=‹binder ∏›\›\∏_🚫/ _)› [0,0,10] 10) "_upto_prod" :: "idt ==> 'a ==> 'b ==> 'b" (‹(‹indent=3 notation=‹binder ∏›\›\∏_≤_./ _)› [0,0,10] 10) syntax_consts "_from_to_prod" "_from_upto_prod" "_upt_prod" "_upto_prod" ⇌ prod translations "∏x=a..b. t" ⇌ "CONST prod (λx. t) {a..b}" "∏x=a..🚫 t" ⇌ "CONST prod (λx. t) {a..🚫" "∏i≤n. t" ⇌ "CONST prod (λi. t) {..n}" "∏i🚫 t" ⇌ "CONST prod (λi. t) {..🚫" lemma prod_int_plus_eq: "prod int {i..i+j} = ∏{int i..int (i+j)}" by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv) lemma prod_int_eq: "prod int {i..j} = ∏{int i..int j}" proof (cases "i ≤ j") case True then show ?thesis by (metis le_iff_add prod_int_plus_eq) next case False then show ?thesis by auto qed subsubsection ‹Telescoping products› lemma prod_telescope: fixes f::"nat ==> 'a::field" assumes "∧i. i≤n ==> f (Suc i) ≠ 0" shows "(∏i≤n. f i / f (Suc i)) = f 0 / f (Suc n)" using assms by (induction n) auto lemma prod_telescope'': fixes f::"nat ==> 'a::field" assumes "m ≤ n" assumes "∧i. i ∈ {m..n} ==> f i ≠ 0" shows "(∏i = Suc m..n. f i / f (i - 1)) = f n / f m" by (rule dec_induct[OF ‹m ≤ n›]) (auto simp add: assms) lemma prod_lessThan_telescope: fixes f::"nat ==> 'a::field" assumes "∧i. i≤n ==> f i ≠ 0" shows "(∏i🚫 f (Suc i) / f i) = f n / f 0" using assms by (induction n) auto lemma prod_lessThan_telescope': fixes f::"nat ==> 'a::field" assumes "∧i. i≤n ==> f i ≠ 0" shows "(∏i🚫 f i / f (Suc i)) = f 0 / f n" using assms by (induction n) auto subsection ‹Efficient folding over intervals› function fold_atLeastAtMost_nat where [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc = (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))" by pat_completeness auto termination by (relation "measure (λ(_,a,b,_). Suc b - a)") auto lemma fold_atLeastAtMost_nat: assumes "comp_fun_commute f" shows "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}" using assms proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases) case (1 f a b acc) interpret comp_fun_commute f by fact show ?case proof (cases "a > b") case True thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto next case False with 1 show ?thesis by (subst fold_atLeastAtMost_nat.simps) (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm) qed qed lemma sum_atLeastAtMost_code: "sum f {a..b} = fold_atLeastAtMost_nat (λa acc. f a + acc) a b 0" proof - have "comp_fun_commute (λa. (+) (f a))" by unfold_locales (auto simp: o_def add_ac) thus ?thesis by (simp add: sum.eq_fold fold_atLeastAtMost_nat o_def) qed lemma prod_atLeastAtMost_code: "prod f {a..b} = fold_atLeastAtMost_nat (λa acc. f a * acc) a b 1" proof - have "comp_fun_commute (\<lambda>a. (*) by unfold_locales (auto simp: o_def mult_ac) thus ?thesis by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def) qed
(* TODO: Add support for folding over more kinds of intervals here *)
lemma pairs_le_eq_Sigma: "{(i, j). i + j ≤ m} = Sigma (atMost m) (λr. atMost (m - r))" for m :: nat by auto
lemma sum_up_index_split: "(∑k≤m + n. f k) = (∑k≤m. f k) + (∑k = Suc m..m + n. f k)" by (metis atLeast0AtMost Suc_eq_plus1 le0 sum.ub_add_nat)
lemma Sigma_interval_disjoint: "(SIGMA i:A. {..v i}) ∩ (SIGMA i:A.{v i<..w}) = {}" for w :: "'a::order" by auto
lemma product_atMost_eq_Un: "A × {..m} = (SIGMA i:A.{..m - i}) ∪ (SIGMA i:A.{m - i<..m})" for m :: nat by auto
lemma polynomial_product: (*with thanks to Chaitanya Mangla*) fixes x :: "'a::idom" assumes m: "∧i. i > m ==> a i = 0" and n: "∧j. j > n ==> b j = 0" shows"(∑i≤m. (a i) * x ^ i) * (∑j≤n. (b j) * x ^ j) = (∑r≤m + n. (∑k≤r. (a k) * (b (r - k))) * x ^ r)" proof - have"∧i j. [m + n - i < j; a i ≠ 0]==> b j = 0" by (meson le_add_diff leI le_less_trans m n) thenhave🍋: "(∑(i,j)∈(SIGMA i:{..m+n}. {m+n - i<..m+n}). a i * x ^ i * (b j * x ^ j)) = 0" by (clarsimp simp add: sum_Un Sigma_interval_disjoint intro!: sum.neutral) have"(∑i≤m. (a i) * x ^ i) * (∑j≤n. (b j) * x ^ j) = (∑i≤m. ∑j≤n. (a i * x ^ i) * (b j * x ^ j))" by (rule sum_product) alsohave"… = (∑i≤m + n. ∑j≤n + m. a i * x ^ i * (b j * x ^ j))" using assms by (auto simp: sum_up_index_split) alsohave"… = (∑r≤m + n. ∑j≤m + n - r. a r * x ^ r * (b j * x ^ j))" by (simp add: add_ac sum.Sigma product_atMost_eq_Un sum_Un Sigma_interval_disjoint 🍋) alsohave"… = (∑(i,j)∈{(i,j). i+j ≤ m+n}. (a i * x ^ i) * (b j * x ^ j))" by (auto simp: pairs_le_eq_Sigma sum.Sigma) alsohave"... = (∑k≤m + n. ∑i≤k. a i * x ^ i * (b (k - i) * x ^ (k - i)))" by (rule sum.triangle_reindex_eq) alsohave"… = (∑r≤m + n. (∑k≤r. (a k) * (b (r - k))) * x ^ r)" by (auto simp: algebra_simps sum_distrib_left simp flip: power_add intro!: sum.cong) finallyshow ?thesis . qed
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.84 Sekunden
(vorverarbeitet am 2026-04-26)
¤
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 und die Messung sind noch experimentell.
