(* Title: HOL/SetInterval.thy Author: Tobias Nipkow and Clemens Ballarin Additions by Jeremy Avigad in March 2004 Copyright 2000 TU Muenchen lessThan, greaterThan, atLeast, atMost and two-sided intervals *) header {* Set intervals *} theory SetInterval imports Int begin context ord begin definition lessThan :: "'a => 'a set" ("(1{..<_})") where "{.. 'a set" ("(1{.._})") where "{..u} == {x. x \ u}" definition greaterThan :: "'a => 'a set" ("(1{_<..})") where "{l<..} == {x. l 'a set" ("(1{_..})") where "{l..} == {x. l\x}" definition greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where "{l<.. 'a => 'a set" ("(1{_..<_})") where "{l.. 'a => 'a set" ("(1{_<.._})") where "{l<..u} == {l<..} Int {..u}" definition atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where "{l..u} == {l..} Int {..u}" end text{* A note of warning when using @{term"{.. 'a => 'b set => 'b set" ("(3UN _<=_./ _)" 10) "@UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" 10) "@INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" 10) "@INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" 10) syntax (xsymbols) "@UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" 10) "@UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" 10) "@INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" 10) "@INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" 10) syntax (latex output) "@UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) "@UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10) "@INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) "@INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10) translations "UN i<=n. A" == "UN i:{..n}. A" "UN i atLeast y) = (y \ (x::'a::order))" by (blast intro: order_trans) lemma atLeast_eq_iff [iff]: "(atLeast x = atLeast y) = (x = (y::'a::linorder))" by (blast intro: order_antisym order_trans) lemma greaterThan_subset_iff [iff]: "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))" apply (auto simp add: greaterThan_def) apply (subst linorder_not_less [symmetric], blast) done lemma greaterThan_eq_iff [iff]: "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" apply (rule iffI) apply (erule equalityE) apply simp_all done lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))" by (blast intro: order_trans) lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" by (blast intro: order_antisym order_trans) lemma lessThan_subset_iff [iff]: "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))" apply (auto simp add: lessThan_def) apply (subst linorder_not_less [symmetric], blast) done lemma lessThan_eq_iff [iff]: "(lessThan x = lessThan y) = (x = (y::'a::linorder))" apply (rule iffI) apply (erule equalityE) apply simp_all done subsection {*Two-sided intervals*} context ord begin lemma greaterThanLessThan_iff [simp,noatp]: "(i : {l<.. {m..n} = {}"; by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) lemma atLeastLessThan_empty[simp]: "n \ m ==> {m.. k ==> {k<..l} = {}" by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}" by (auto simp add: atLeastAtMost_def) subsubsection {* Image *} lemma image_add_atLeastAtMost: "(%n::nat. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B") proof show "?A \ ?B" by auto next show "?B \ ?A" proof fix n assume a: "n : ?B" hence "n - k : {i..j}" by auto moreover have "n = (n - k) + k" using a by auto ultimately show "n : ?A" by blast qed qed lemma image_add_atLeastLessThan: "(%n::nat. n+k) ` {i.. ?B" by auto next show "?B \ ?A" proof fix n assume a: "n : ?B" hence "n - k : {i.. finite N" apply (rule finite_subset) apply (rule_tac [2] finite_lessThan, auto) done text {* A set of natural numbers is finite iff it is bounded. *} lemma finite_nat_set_iff_bounded: "finite(N::nat set) = (EX m. ALL n:N. nnat. (!!n. n \ f n) ==> finite {n. f n \ u}" by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) text{* Any subset of an interval of natural numbers the size of the subset is exactly that interval. *} lemma subset_card_intvl_is_intvl: "A <= {k.. A = {k.. \h. bij_betw h {0.. \h. bij_betw h M {0.. finite B \ card A = card B \ EX 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 subsection {* Intervals of integers *} lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l.. u ==> {(0::int).. u") apply (subst image_atLeastZeroLessThan_int, assumption) apply (rule finite_imageI) apply auto done lemma finite_atLeastLessThan_int [iff]: "finite {l.. u") apply (subst image_atLeastZeroLessThan_int, assumption) apply (subst card_image) apply (auto simp add: inj_on_def) done lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}" proof - have "{k. P k \ k < i} \ {.. 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: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}" apply (rule card_bij_eq [of "Suc" _ _ "\x. x - Suc 0"]) apply simp apply fastsimp apply auto apply (rule inj_on_diff_nat) apply auto apply (case_tac x) apply auto apply (case_tac xa) apply auto apply (case_tac xa) apply auto done lemma card_less_Suc: assumes zero_in_M: "0 \ M" shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}" proof - from assms have a: "0 \ {k \ M. k < Suc i}" by simp hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})" by (auto simp only: insert_Diff) have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto from finite_M_bounded_by_nat[of "\x. x \ M" "Suc i"] have "Suc (card {k. Suc k \ M \ k < i}) = card (insert 0 ({k \ M. k < Suc i} - {0}))" apply (subst card_insert) apply simp_all apply (subst b) apply (subst card_less_Suc2[symmetric]) apply simp_all done with c show ?thesis by simp qed subsection {*Lemmas useful with the summation operator setsum*} text {* For examples, see Algebra/poly/UnivPoly2.thy *} subsubsection {* Disjoint Unions *} text {* Singletons and open intervals *} lemma ivl_disj_un_singleton: "{l::'a::linorder} Un {l<..} = {l..}" "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}" "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}" "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}" "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}" "(l::'a::linorder) <= u ==> {l.. {l<.. {l<..m} Un {m<.. {l.. {l..m} Un {m<.. {l<.. {l<..m} Un {m<..u} = {l<..u}" "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}" by auto lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two subsubsection {* Disjoint Intersections *} text {* Singletons and open intervals *} lemma ivl_disj_int_singleton: "{l::'a::order} Int {l<..} = {}" "{.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))" apply(auto simp:linorder_not_le) apply(rule ccontr) apply(insert linorder_le_less_linear[of i n]) apply(clarsimp simp:linorder_not_le) apply(fastsimp) done subsection {* Summation indexed over intervals *} syntax "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10) "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10) syntax (xsymbols) "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) syntax (HTML output) "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) syntax (latex_sum output) "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10) "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10) translations "\x=a..b. t" == "CONST setsum (%x. t) {a..b}" "\x=a..i\n. t" == "CONST setsum (\i. t) {..n}" "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\ @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\ @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \ setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)" by (simp add:atMost_Suc add_ac) lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n" by (simp add:lessThan_Suc add_ac) lemma setsum_cl_ivl_Suc[simp]: "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))" by (auto simp:add_ac atLeastAtMostSuc_conv) lemma setsum_op_ivl_Suc[simp]: "setsum f {m.. (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)" by (auto simp:add_ac atLeastAtMostSuc_conv) *) lemma setsum_head: fixes n :: nat assumes mn: "m <= n" shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs") proof - from mn have "{m..n} = {m} \ {m<..n}" by (auto intro: ivl_disj_un_singleton) hence "?lhs = (\x\{m} \ {m<..n}. P x)" by (simp add: atLeast0LessThan) also have "\ = ?rhs" by simp finally show ?thesis . qed lemma setsum_head_Suc: "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}" by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) lemma setsum_head_upt_Suc: "m < n \ setsum f {m.. n + 1" shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {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 setsum_Un_disjoint atLeastSucAtMost_greaterThanAtMost) qed lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \ setsum f {m.. 'a::ab_group_add" shows "\ m \ n; n \ p \ \ setsum f {m.. ('a::ab_group_add)" shows "setsum (\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) lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] lemma setsum_setsum_restrict: "finite S \ finite T \ setsum (\x. setsum (\y. f x y) {y. y\ T \ R x y}) S = setsum (\y. setsum (\x. f x y) {x. x \ S \ R x y}) T" by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def) (rule setsum_commute) lemma setsum_image_gen: assumes fS: "finite S" shows "setsum g S = setsum (\y. setsum g {x. x \ S \ f x = y}) (f ` S)" proof- { fix x assume "x \ S" then have "{y. y\ f`S \ f x = y} = {f x}" by auto } hence "setsum g S = setsum (\x. setsum (\y. g x) {y. y\ f`S \ f x = y}) S" by simp also have "\ = setsum (\y. setsum g {x. x \ S \ f x = y}) (f ` S)" by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]]) finally show ?thesis . qed lemma setsum_multicount_gen: assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)" shows "setsum (\i. (card {j\t. R i j})) s = setsum k t" (is "?l = ?r") proof- have "?l = setsum (\i. setsum (\x.1) {j\t. R i j}) s" by auto also have "\ = ?r" unfolding setsum_setsum_restrict[OF assms(1-2)] using assms(3) by auto finally show ?thesis . qed lemma setsum_multicount: assumes "finite S" "finite T" "\j\T. (card {i\S. R i j} = k)" shows "setsum (\i. card {j\T. R i j}) S = k * card T" (is "?l = ?r") proof- have "?l = setsum (\i. k) T" by(rule setsum_multicount_gen)(auto simp:assms) also have "\ = ?r" by(simp add: setsum_constant mult_commute) finally show ?thesis by auto qed subsection{* Shifting bounds *} lemma setsum_shift_bounds_nat_ivl: "setsum f {m+k.. setsum f {Suc 0..k} = setsum f {0..k}" by(simp add:setsum_head_Suc) lemma setsum_shift_lb_Suc0_0_upt: "f(0::nat) = 0 \ setsum f {Suc 0.. (\i=0..i\{1..n}. of_nat i) = of_nat n*((of_nat n)+1)" proof (induct n) case 0 show ?case by simp next case (Suc n) then show ?case by (simp add: algebra_simps) qed theorem arith_series_general: "((1::'a::comm_semiring_1) + 1) * (\i\{.. 1" let ?I = "\i. of_nat i" and ?n = "of_nat n" have "(\i\{..i\{..i\{.. = ?n*a + (\i\{.. = (?n*a + d*(\i\{1.. = (1+1)*?n*a + d*(1+1)*(\i\{1..i\{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)" by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def) (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]]) finally show ?thesis by (simp add: algebra_simps) next assume "\(n > 1)" hence "n = 1 \ n = 0" by auto thus ?thesis by (auto simp: algebra_simps) qed lemma arith_series_nat: "Suc (Suc 0) * (\i\{..i\{..i\{..i\{..nat" shows "\x. Q x \ P x \ (\xxxxx 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10) "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10) "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10) "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10) syntax (xsymbols) "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) syntax (HTML output) "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) syntax (latex_prod output) "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10) "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10) translations "\x=a..b. t" == "CONST setprod (%x. t) {a..b}" "\x=a..i\n. t" == "CONST setprod (\i. t) {..n}" "\ii. t) {..