(* 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 "{..<u} == {x. x < u}"
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<x}"
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<..<u} == {l<..} ∩ {..<u}"
definition
atLeastLessThan :: "'a ==> 'a ==> 'a set" (‹(‹indent=1 notation=‹mixfix set interval››{_/..<_})›) where "{l..<u} == {l..} ∩ {..<u}"
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 term‹{..<n}› on type 🍋‹nat›: it is equivalent to term‹{0::nat..<n}› but some lemmas involving term‹{m..<n}› may not exist in term‹{..<n}›-form as well.›
lemma (in ord) lessThan_iff [iff]: "(i ∈ lessThan k) = (i<k)" 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<i)" 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} ⟷ 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<..<u}) = (l < i ∧ i < u)" by (simp add: greaterThanLessThan_def)
lemma atLeastLessThan_iff [simp]: "(i ∈ {l..<u}) = (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
many proofs. Since it only helps blast, it is better to leave them
.›
lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} ∩ {..< b }" by auto
lemma (in order) atLeastLessThan_eq_atLeastAtMost_diff: "{a..<b} = {a..b} - {b}" 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..<b} = {} ⟷ (¬ a < b)" by auto (blast intro: le_less_trans)
lemma atLeastLessThan_empty_iff2[simp]: "{} = {a..<b} ⟷ (¬ 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 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 ∈ {..<u}. P x) ⟷ (∃x<u. P 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<..<u}. P x) ⟷ (∃x. l<x ∧ x<u ∧ P x)" "(∃x ∈ {l..<u}. P x) ⟷ (∃x. l≤x ∧ x<u ∧ P x)" "(∃x ∈ {l<..u}. P x) ⟷ (∃x. l<x ∧ x≤u ∧ P x)" "(∃x ∈ {l..u}. P x) ⟷ (∃x. l≤x ∧ x≤u ∧ P x)" by auto
lemma all_interval_simps: "(∀x ∈ {..<u}. P x) ⟷ (∀x<u. P 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<..<u}. P x) ⟷ (∀x. l<x ⟶ x<u ⟶ P x)" "(∀x ∈ {l..<u}. P x) ⟷ (∀x. l≤x ⟶ x<u ⟶ P x)" "(∀x ∈ {l<..u}. P x) ⟷ (∀x. l<x ⟶ 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'} ⊆ 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" using2by 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'} ⊆ 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" using2by 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'} ⊆ N" shows"f n < f n'" using‹n < 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" using2by 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..<b} ⊆ {c..<d} ==> b ≤ a ∨ c≤a ∧ b≤d" proof (cases "a < b") case True assume assm: "{a..<b} ⊆ {c..<d}" thenhave1: "c ≤ a ∧ a ≤ d" using True by (auto simp add: subset_eq Ball_def) thenhave2: "b ≤ d" using assm by (auto simp add: subset_eq) from12show ?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 ∧ x ≤ b ⟷ c < x ∧ 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: "{..<k} ∩ {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<..<b}" proof assume fin: "finite {a<..<b}" moreoverhave ne: "{a<..<b} ≠ {}" using‹a < b›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}" b] by auto thenhave"x ∈ {a <..< b}" using‹a < Max {a <..< b}›by auto thenhave"x ≤ Max {a <..< b}" using fin by auto with‹Max {a <..< b} < x›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<..<b} ⟷ 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..<b} ⟷ 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 < a›by fact alsonote‹x < a› finallyhave"Min {..< a} ≤ y" by fact with‹y < Min {..< a}›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 <..} < y› finallyhave"y ≤ Max { a <..}" by fact with‹Max {a <..} < y›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..<b} = {b..b'}" 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<..<b} = {a,b}" 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..<b} ∩ {c..<d} = {max a c ..< min b d}" by auto
lemma Int_greaterThanAtMost[simp]: "{a<..b} ∩ {c<..d} = {max a c <.. min b d}" by auto
lemma Int_greaterThanLessThan[simp]: "{a<..<b} ∩ {c<..<d} = {max a c <..< min b d}" 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 lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" by (simp add: lessThan_def less_Suc_eq, blast)
text‹The following proof is convenient in induction proofs where
elements get indices at the beginning. So it is used to transform term‹{..<Suc n}› to term‹0::nat› and term‹{..< n}›.›
lemma zero_notin_Suc_image [simp]: "0 ∉ Suc ` A" by auto
lemma UN_atMost_UNIV: "(∪m::nat. atMost m) = UNIV" by blast
subsubsection‹The Constant term‹atLeastLessThan››
text‹The orientation of the following 2 rules is tricky. The lhs is
in terms of the rhs. Hence the chosen orientation makes sense
this theory --- the reverse orientation complicates proofs (eg
). But outside, when the definition of the lhs is rarely
, the opposite orientation seems preferable because it reduces a
concept to a more general one.›
text‹Not a simprule because the RHS is too messy.› lemma atLeastLessThanSuc: "{m..<Suc n} = (if m ≤ n then insert n {m..<n} else {})" by (auto simp add: atLeastLessThan_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+k} = {i..<j} ∪ {j..<j+k::nat}" 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
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 case1 have"(*) c ` {x..y} = {c * y..c * x}" proof (rule set_eqI) fix d from1have"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}" using1by (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..<n} = {..<n} - {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..<u-l} = {l..<u}" 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..<b} = {int a..<int b}" 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 {..<k}" 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<..<u}" by (simp add: greaterThanLessThan_def)
lemma finite_atLeastLessThan [iff]: fixes l :: nat shows"finite {l..<u}" 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<m)" (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
is exactly that interval.›
lemma subset_card_intvl_is_intvl: assumes"A ⊆ {k..<k + card A}" shows"A = {k..<k + card A}" 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..<k + card A}"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) case0with 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<n::nat. M(i+k)) = (∪i∈{k..<n+k}. M i)" (is"?A = ?B") proof show"?B ⊆ ?A" proof fix x assume"x ∈ ?B" thenobtain i where i: "i ∈ {k..<n+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 i) = (∪n. A n)" by (auto simp add: atLeast0LessThan)
lemma UN_finite_subset: "(∧n::nat. (∪i∈{0..<n}. A i) ⊆ C) ==> (∪n. A n) ⊆ C" by (subst UN_UN_finite_eq [symmetric]) blast
lemma UN_finite2_subset: assumes"∧n::nat. (∪i∈{0..<n}. A i) ⊆ (∪i∈{0..<n + k}. B i)" shows"(∪n. A n) ⊆ (∪n. B n)" proof (rule UN_finite_subset, rule subsetI) fix n and a from assms have"(∪i∈{0..<n}. A i) ⊆ (∪i∈{0..<n + k}. B i)" . moreoverassume"a ∈ (∪i∈{0..<n}. A i)" ultimatelyhave"a ∈ (∪i∈{0..<n + k}. B i)"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..<n}. A i) = (∪i∈{0..<n + k}. B i))" shows"(∪n. A n) = (∪n. B n)" proof (rule subset_antisym [OF UN_finite_subset UN_finite2_subset]) fix n show"∪ (A ` {0..<n}) ⊆ (∪n. B n)" using assms by auto next fix n show"∪ (B ` {0..<n}) ⊆∪ (A ` {0..<n + k})" using assms by (force simp add: atLeastLessThan_add_Un [of 0])+ qed
subsubsection‹Cardinality›
lemma card_lessThan [simp]: "card {..<u} = u" by (induct u, simp_all add: lessThan_Suc)
lemma card_atLeastLessThan [simp]: "card {l..<u} = u - l" proof - have"(λx. x + l) ` {..<u - l} ⊆ {l..<u}" by auto moreoverhave"{l..<u} ⊆ (λx. x + l) ` {..<u-l}" proof fix x assume *: "x ∈ {l..<u}" thenhave"x - l ∈ {..< u -l}" by auto thenhave"(x - l) + l ∈ (λx. x + l) ` {..< u -l}" by auto thenshow"x ∈ (λx. x + l) ` {..<u - l}" using * by auto qed ultimatelyhave"{l..<u} = (λx. x + l) ` {..<u-l}" by auto thenhave"card {l..<u} = card {..<u-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 card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l" by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
lemma subset_eq_atLeast0_lessThan_finite: fixes n :: nat assumes"N ⊆ {0..<n}" 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..<card M} M" 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..<card M}" 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..<n}" shows"card N ≤ n" proof - from assms finite_lessThan have"card N ≤ card {0..<n}" 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" have1: "?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" have0: "?f a1 ∈ B"using"1"‹a1 ∈ A›by blast have1: "r a1 (?f a1)"using someI_ex[OF assms(2)[OF ‹a1 ∈ A›]] by blast have2: "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) 012] . qed with1show ?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..<n}› if‹(f ^^ n) s = s›‹∧m. 0 < m ==> m < n ==> (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' < n›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
lemma image_atLeastZeroLessThan_int: assumes"0 ≤ u" shows"{(0::int)..<u} = int ` {..<nat u}" unfolding image_def lessThan_def proof show"{0..<u} ⊆ {y. ∃x∈{x. x < nat u}. y = int x}" proof fix x assume"x ∈ {0..<u}" thenhave"x = int (nat x)"and"nat x < nat u" by (auto simp add: zless_nat_eq_int_zless [THEN sym]) thenhave"∃xa<nat u. x = int 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)..<u}" proof (cases "0 ≤ u") case True thenshow ?thesis by (auto simp: image_atLeastZeroLessThan_int) qed auto
lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}" by (simp only: image_add_int_atLeastLessThan [symmetric, of l] finite_imageI finite_atLeastZeroLessThan_int)
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<..<u} = nat (u - (l + 1))" 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} ⊆ {..<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<n. B 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<n. B 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<n. B i)" proof - obtain n where"A ⊆ (∪i<n. B 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} ∪ {u::'a::linorder} = {..u}" "(l::'a::linorder) < u ==> {l} ∪ {l<..<u} = {l..<u}" "(l::'a::linorder) < u ==> {l<..<u} ∪ {u} = {l<..u}" "(l::'a::linorder) ≤ u ==> {l} ∪ {l<..u} = {l..u}" "(l::'a::linorder) ≤ u ==> {l..<u} ∪ {u} = {l..u}" by auto
text‹One- and two-sided intervals›
lemma ivl_disj_un_one: "(l::'a::linorder) < u ==> {..l} ∪ {l<..<u} = {..<u}" "(l::'a::linorder) ≤ u ==> {..<l} ∪ {l..<u} = {..<u}" "(l::'a::linorder) ≤ u ==> {..l} ∪ {l<..u} = {..u}" "(l::'a::linorder) ≤ u ==> {..<l} ∪ {l..u} = {..u}" "(l::'a::linorder) ≤ u ==> {l<..u} ∪ {u<..} = {l<..}" "(l::'a::linorder) < u ==> {l<..<u} ∪ {u..} = {l<..}" "(l::'a::linorder) ≤ u ==> {l..u} ∪ {u<..} = {l..}" "(l::'a::linorder) ≤ u ==> {l..<u} ∪ {u..} = {l..}" by auto
text‹Two- and two-sided intervals›
lemma ivl_disj_un_two: "[(l::'a::linorder) < m; m ≤ u]==> {l<..<m} ∪ {m..<u} = {l<..<u}" "[(l::'a::linorder) ≤ m; m < u]==> {l<..m} ∪ {m<..<u} = {l<..<u}" "[(l::'a::linorder) ≤ m; m ≤ u]==> {l..<m} ∪ {m..<u} = {l..<u}" "[(l::'a::linorder) ≤ m; m < u]==> {l..m} ∪ {m<..<u} = {l..<u}" "[(l::'a::linorder) < m; m ≤ u]==> {l<..<m} ∪ {m..u} = {l<..u}" "[(l::'a::linorder) ≤ m; m ≤ u]==> {l<..m} ∪ {m<..u} = {l<..u}" "[(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 ivl_disj_un_two_touch: "[(l::'a::linorder) < m; m < u]==> {l<..m} ∪ {m..<u} = {l<..<u}" "[(l::'a::linorder) ≤ m; m < u]==> {l..m} ∪ {m..<u} = {l..<u}" "[(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 ivl_diff[simp]: "i ≤ n ==> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}" 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<..<b}" by auto
subsubsection‹Some Subset Conditions›
lemma ivl_subset [simp]: "({i..<j} ⊆ {m..<n}) = (j ≤ 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 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 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..<n + k} = F (g ∘ plus k) {m..<n}" 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 n} = F (g ∘ Suc) {m..<n}" 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..<Suc n} = F g {m..<n}" unfolding atLeast_Suc_lessThan_Suc_shift by simp
lemma atLeast_int_lessThan_int_shift: "F g {int m..<int n} = F (g ∘ int) {m..<n}" 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..<Suc n} = F g {0..<n} * 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..<Suc n} = g 0 * F (g ∘ Suc) {0..<n}" 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..<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 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..<b} = F h {c..<d}" by (rule cong) simp_all
lemma atLeastLessThan_shift_0: fixes m n p :: nat shows"F g {m..<n} = F (g ∘ plus m) {0..<n - m}" 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..<n} * F g {n..<p} = F g {m..<p}" by (simp add: union_disjoint [symmetric] ivl_disj_un)
lemma atLeastLessThan_rev: "F g {n..<m} = F (λi. g (m + n - Suc i)) {n..<m}" 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..<m} = F (λi. g (m + n - i)) {Suc n..m}" unfolding atLeastLessThan_rev [of g n m] by (cases m) (simp_all add: atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost)
"_from_to_sum" "_from_upto_sum" "_upt_sum" "_upto_sum" == sum
"∑x=a..b. t" == "CONST sum (λx. t) {a..b}"
"∑x=a..<b. t" == "CONST sum (λx. t) {a..<b}"
"∑i≤n. t" == "CONST sum (λi. t) {..n}"
"∑i<n. t" == "CONST sum (λi. t) {..<n}"
‹The above introduces some pretty alternative syntaxes for
over intervals:
begin{center}
begin{tabular}{lll}
& New & \LaTeX\\
{term[source]"∑x∈{a..b}. e"} & term‹∑x=a..b. e› & @{term[mode=latex_sum]"∑x=a..b. e"}\\
{term[source]"∑x∈{a..<b}. e"} & term‹∑x=a..<b. e› & @{term[mode=latex_sum]"∑x=a..<b. e"}\\
{term[source]"∑x∈{..b}. e"} & term‹∑x≤b. e› & @{term[mode=latex_sum]"∑x≤b. e"}\\
{term[source]"∑x∈{..<b}. e"} & term‹∑x<b. e› & @{term[mode=latex_sum]"∑x<b. e"}
end{tabular}
end{center}
left column shows the term before introduction of the new syntax,
middle column shows the new (default) syntax, and the right column
a special syntax. The latter is only meaningful for latex output
has to be activated explicitly by setting the print mode to ‹latex_sum› (e.g.\ via ‹mode = latex_sum› in
). It is not the default \LaTeX\ output because it only
well with italic-style formulae, not tt-style.
that for uniformity on 🍋‹nat› it is better to use term‹∑x::nat=0..<n. e› rather than ‹∑x<n. e›: ‹sum› may
provide all lemmas available for term‹{m..<n}› also in the
form for term‹{..<n}›.›
‹This congruence rule should be used for sums over intervals as
standard theorem @{text[source]sum.cong} does not work well
the simplifier who adds the unsimplified premise term‹x∈B› to
context.›
comm_monoid_set
zero_middle:
assumes "1 ≤ p" "k ≤ p"
shows "F (λj. if j < k then g j else if j = k then 1 else h (j - Suc 0)) {..p}
= F (λj. if j < k then g j else h j) {..p - Suc 0}" (is "?lhs = ?rhs")
-
have [simp]: "{..p - Suc 0} ∩ {j. j < k} = {..<k}" "{..p - Suc 0} ∩ - {j. j < k} = {k..p - Suc 0}"
using assms by auto
have "?lhs = F g {..<k} * F (λj. if j = k then 1 else h (j - Suc 0)) {k..p}"
using union_disjoint [of "{..<k}" "{k..p}"] assms
by (simp add: ivl_disj_int_one ivl_disj_un_one)
also have "… = F g {..<k} * F (λj. h (j - Suc 0)) {Suc k..p}"
by (simp add: atLeast_Suc_atMost [of k p] assms)
also have "… = F g {..<k} * 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 .
atMost_Suc [simp]:
"F g {..Suc n} = F g {..n} * g (Suc n)"
by (simp add: atMost_Suc ac_simps)
lessThan_Suc [simp]:
"F g {..<Suc n} = F g {..<n} * g n"
by (simp add: lessThan_Suc ac_simps)
cl_ivl_Suc [simp]:
"F g {m..Suc n} = (if Suc n < m then 1 else F g {m..n} * g(Suc n))"
by (auto simp: ac_simps atLeastAtMostSuc_conv)
op_ivl_Suc [simp]:
"F g {m..<Suc n} = (if n < m then 1 else F g {m..<n} * g(n))"
by (auto simp: ac_simps atLeastLessThanSuc)
head:
fixes n :: nat
assumes mn: "m ≤ n"
shows "F g {m..n} = g m * F g {m<..n}" (is "?lhs = ?rhs")
-
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 .
last_plus:
fixes n::nat shows "m ≤ n ==> F g {m..n} = g n * F g {m..<n}"
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost commute)
head_if:
fixes n :: nat
shows "F g {m..n} = (if n < m then 1 else F g {m..<n} * g(n))"
by (simp add: commute last_plus)
ub_add_nat:
assumes "(m::nat) ≤ n + 1"
shows "F g {m..n + p} = F g {m..n} * F g {n + 1..n + p}"
-
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)
nat_group:
fixes k::nat shows "F (λm. F g {m * k ..< m*k + k}) {..<n} = F g {..< n * k}"
(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])
auto
triangle_reindex:
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}"
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
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}"
triangle_reindex [of g "Suc n"]
(simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)
nat_diff_reindex: "F (λi. g (n - Suc i)) {..<n} = F g {..<n}"
by (rule reindex_bij_witness[where i="λi. n - Suc i" and j="λi. n - Suc i"]) auto
shift_bounds_nat_ivl:
"F g {m+k..<n+k} = F (λi. g(i + k)){m..<n::nat}"
(induct "n", auto simp: atLeastLessThanSuc)
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
shift_bounds_cl_Suc_ivl:
"F g {Suc m..Suc n} = F (λi. g(Suc i)){m..n}"
(simp add: shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
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)
shift_bounds_Suc_ivl:
"F g {Suc m..<Suc n} = F (λi. g(Suc i)){m..<n}"
(simp add: shift_bounds_nat_ivl[where k="Suc 0", simplified])
atMost_Suc_shift:
shows "F g {..Suc n} = g 0 * F (λi. g (Suc i)) {..n}"
(induct n)
case 0 show ?case by simp
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 .
lessThan_Suc_shift:
"F g {..<Suc n} = g 0 * F (λi. g (Suc i)) {..<n}"
by (induction n) (simp_all add: ac_simps)
atMost_shift:
"F g {..n} = g 0 * F (λi. g (Suc i)) {..<n}"
by (metis atLeast0AtMost atLeast0LessThan atLeastLessThanSuc_atLeastAtMost
atLeastSucAtMost_greaterThanAtMost le0 head shift_bounds_Suc_ivl)
nested_swap:
"F (λi. F (λj. a i j) {0..<i}) {0..n} = F (λj. F (λi. a i j) {Suc j..n}) {0..<n}"
by (induction n) (auto simp: distrib)
nested_swap':
"F (λi. F (λj. a i j) {..<i}) {..n} = F (λj. F (λi. a i j) {Suc j..n}) {..<n}"
by (induction n) (auto simp: distrib)
atLeast1_atMost_eq:
"F g {Suc 0..n} = F (λk. g (Suc k)) {..<n}"
-
have "F g {Suc 0..n} = F g (Suc ` {..<n})"
by (simp add: image_Suc_lessThan)
also have "… = F (λk. g (Suc k)) {..<n}"
by (simp add: reindex)
finally show ?thesis .
atLeastLessThan_Suc: "a ≤ b ==> F g {a..<Suc b} = F g {a..<b} * g b"
by (simp add: atLeastLessThanSuc commute)
nat_ivl_Suc':
assumes "m ≤ Suc n"
shows "F g {m..Suc n} = g (Suc n) * F g {m..n}"
-
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 .
in_pairs: "F g {2*m..Suc(2*n)} = F (λi. g(2*i) * g(Suc(2*i))) {m..n}"
(induction n)
case 0
show ?case
by (cases "m=0") auto
case (Suc n)
then show ?case
by (auto simp: assoc split: if_split_asm)
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)
card_sum_le_nat_sum: "∑ {0..<card S} ≤∑ S"
(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..<card ?S'} ≤∑ ?S'"
using Suc by (intro Suc; auto)
hence "∑ {0..<card ?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
simp
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)"
(induct n, auto simp add: algebra_simps not_le le_Suc_eq)
sum_diff_nat_ivl:
fixes f :: "nat ==> 'a::ab_group_add"
shows "[ m ≤ n; n ≤ p ]==> sum f {m..<p} - sum f {m..<n} = sum f {n..<p}"
using sum.atLeastLessThan_concat [of m n p f,symmetric]
by (simp add: ac_simps)
sum_diff_distrib: "∀x. Q x ≤ P x ==> (∑x<n. P x) - (∑x<n. Q x) = (∑x<n. P x - Q x :: nat)"
by (subst sum_subtractf_nat) auto
‹Shifting bounds›
comm_monoid_add
fixes f :: "nat ==> 'a"
assumes "f 0 = 0"
sum_shift_lb_Suc0_0_upt:
"sum f {Suc 0..<k} = sum f {0..<k}"
(cases k)
case 0
then show ?thesis
by simp
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
sum_shift_lb_Suc0_0: "sum f {Suc 0..k} = sum f {0..k}"
(cases k)
case 0
with ‹f 0 = 0› show ?thesis
by simp
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
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"
assms by (induct n) (auto simp: le_Suc_eq)
sum_Suc_diff':
fixes f :: "nat ==> 'a::ab_group_add"
assumes "m ≤ n"
shows "(∑i = m..<n. f (Suc i) - f i) = f n - f m"
assms by (induct n) (auto simp: le_Suc_eq)
sum_diff_split:
fixes f:: "nat ==> 'a::ab_group_add"
assumes "m ≤ n"
shows "(∑i≤n. f i) - (∑i<m. f i) = (∑i≤n - m. f(n - i))"
-
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<m. 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
prod_divide_nat_ivl:
fixes f :: "nat ==> 'a::idom_divide"
shows "[ m ≤ n; n ≤ p; prod f {m..<n} ≠ 0]==> prod f {m..<p} div prod f {m..<n} = prod f {n..<p}"
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 {..<m} ≠ 0" shows"(prod f {..n}) div (prod f {..<m}) = prod (λi. f(n - i)) {..n - m}" 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 {..<m}" 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<m. f (Suc n) - f n :: 'a :: ab_group_add) = f m - f 0" by (induction m) (simp_all add: algebra_simps)
lemma sum_lessThan_telescope': "(∑n<m. f n - f (Suc n) :: 'a :: ab_group_add) = f 0 - f m" by (induction m) (simp_all add: algebra_simps)
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<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))" 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) case0 thenhave"m = n" by arith thenshow ?case by (simp add: algebra_simps mult_2 [symmetric]) next case (Suc i) have0: "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..<n} = (n * (n - 1) - m * (m - 1)) div 2"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..<n}" (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
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)
prod_int_eq: "prod int {i..j} = ∏{int i..int j}"
(cases "i ≤ j")
case True
then show ?thesis
by (metis le_iff_add prod_int_plus_eq)
case False
then show ?thesis
by auto
‹Telescoping products›
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
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)
prod_lessThan_telescope:
fixes f::"nat ==> 'a::field"
assumes "∧i. i≤n ==> f i ≠ 0"
shows "(∏i<n. f (Suc i) / f i) = f n / f 0"
using assms by (induction n) auto
prod_lessThan_telescope':
fixes f::"nat ==> 'a::field"
assumes "∧i. i≤n ==> f i ≠ 0"
shows "(∏i<n. f i / f (Suc i)) = f 0 / f n"
using assms by (induction n) auto
‹Efficient folding over intervals›
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))"
pat_completeness auto
by (relation "measure (λ(_,a,b,_). Suc b - a)") auto
fold_atLeastAtMost_nat:
assumes "comp_fun_commute f"
shows "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}"
assms
(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
sum_atLeastAtMost_code:
"sum f {a..b} = fold_atLeastAtMost_nat (λa acc. f a + acc) a b 0"
-
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)
prod_atLeastAtMost_code:
"prod f {a..b} = fold_atLeastAtMost_nat (λa acc. f a * acc) a b 1"
-
have "comp_fun_commute (\<lambda>a. (*) (f 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) then have 🍋: "(∑(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) also have "… = (∑i≤m + n. ∑j≤n + m. a i * x ^ i * (b j * x ^ j))" using assms by (auto simp: sum_up_index_split) also have "… = (∑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 🍋) also have "… = (∑(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) also have "... = (∑k≤m + n. ∑i≤k. a i * x ^ i * (b (k - i) * x ^ (k - i)))" by (rule sum.triangle_reindex_eq) also have "… = (∑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) finally show ?thesis . qed
end
Messung V0.5 in Prozent
¤ 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.0.96Bemerkung:
(vorverarbeitet am 2026-06-09)
¤
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.
