64 "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10) |
64 "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10) |
65 "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10) |
65 "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10) |
66 "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10) |
66 "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10) |
67 |
67 |
68 syntax (xsymbols) |
68 syntax (xsymbols) |
69 "@UNION_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10) |
69 "@UNION_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" 10) |
70 "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_ < _\<^esub>)/ _)" 10) |
70 "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" 10) |
71 "@INTER_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10) |
71 "@INTER_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" 10) |
72 "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_ < _\<^esub>)/ _)" 10) |
72 "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00_ < _)/ _)" 10) |
73 |
73 |
74 translations |
74 translations |
75 "UN i<=n. A" == "UN i:{..n}. A" |
75 "UN i<=n. A" == "UN i:{..n}. A" |
76 "UN i<n. A" == "UN i:{..<n}. A" |
76 "UN i<n. A" == "UN i:{..<n}. A" |
77 "INT i<=n. A" == "INT i:{..n}. A" |
77 "INT i<=n. A" == "INT i:{..n}. A" |
350 qed |
350 qed |
351 qed |
351 qed |
352 |
352 |
353 corollary image_Suc_atLeastAtMost[simp]: |
353 corollary image_Suc_atLeastAtMost[simp]: |
354 "Suc ` {i..j} = {Suc i..Suc j}" |
354 "Suc ` {i..j} = {Suc i..Suc j}" |
355 using image_add_atLeastAtMost[where k=1] by simp |
355 using image_add_atLeastAtMost[where k="Suc 0"] by simp |
356 |
356 |
357 corollary image_Suc_atLeastLessThan[simp]: |
357 corollary image_Suc_atLeastLessThan[simp]: |
358 "Suc ` {i..<j} = {Suc i..<Suc j}" |
358 "Suc ` {i..<j} = {Suc i..<Suc j}" |
359 using image_add_atLeastLessThan[where k=1] by simp |
359 using image_add_atLeastLessThan[where k="Suc 0"] by simp |
360 |
360 |
361 lemma image_add_int_atLeastLessThan: |
361 lemma image_add_int_atLeastLessThan: |
362 "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}" |
362 "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}" |
363 apply (auto simp add: image_def) |
363 apply (auto simp add: image_def) |
364 apply (rule_tac x = "x - l" in bexI) |
364 apply (rule_tac x = "x - l" in bexI) |
554 from zero_in_M have "{k \<in> M. k < Suc i} \<noteq> {}" by auto |
554 from zero_in_M have "{k \<in> M. k < Suc i} \<noteq> {}" by auto |
555 with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff) |
555 with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff) |
556 qed |
556 qed |
557 |
557 |
558 lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}" |
558 lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}" |
559 apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - 1"]) |
559 apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - Suc 0"]) |
560 apply simp |
560 apply simp |
561 apply fastsimp |
561 apply fastsimp |
562 apply auto |
562 apply auto |
563 apply (rule inj_on_diff_nat) |
563 apply (rule inj_on_diff_nat) |
564 apply auto |
564 apply auto |
801 "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}" |
801 "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}" |
802 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) |
802 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) |
803 |
803 |
804 lemma setsum_head_upt_Suc: |
804 lemma setsum_head_upt_Suc: |
805 "m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}" |
805 "m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}" |
806 apply(insert setsum_head_Suc[of m "n - 1" f]) |
806 apply(insert setsum_head_Suc[of m "n - Suc 0" f]) |
807 apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) |
807 apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) |
808 done |
808 done |
809 |
809 |
810 |
810 |
811 lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> |
811 lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> |
833 apply (simp add:image_add_atLeastAtMost o_def) |
833 apply (simp add:image_add_atLeastAtMost o_def) |
834 done |
834 done |
835 |
835 |
836 corollary setsum_shift_bounds_cl_Suc_ivl: |
836 corollary setsum_shift_bounds_cl_Suc_ivl: |
837 "setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}" |
837 "setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}" |
838 by (simp add:setsum_shift_bounds_cl_nat_ivl[where k=1,simplified]) |
838 by (simp add:setsum_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified]) |
839 |
839 |
840 corollary setsum_shift_bounds_Suc_ivl: |
840 corollary setsum_shift_bounds_Suc_ivl: |
841 "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}" |
841 "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}" |
842 by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified]) |
842 by (simp add:setsum_shift_bounds_nat_ivl[where k="Suc 0", simplified]) |
843 |
843 |
844 lemma setsum_shift_lb_Suc0_0: |
844 lemma setsum_shift_lb_Suc0_0: |
845 "f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}" |
845 "f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}" |
846 by(simp add:setsum_head_Suc) |
846 by(simp add:setsum_head_Suc) |
847 |
847 |
881 "(\<Sum>i\<in>{..<n}. a+?I i*d) = |
881 "(\<Sum>i\<in>{..<n}. a+?I i*d) = |
882 ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))" |
882 ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))" |
883 by (rule setsum_addf) |
883 by (rule setsum_addf) |
884 also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp |
884 also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp |
885 also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))" |
885 also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))" |
|
886 unfolding One_nat_def |
886 by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac) |
887 by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac) |
887 also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)" |
888 also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)" |
888 by (simp add: left_distrib right_distrib) |
889 by (simp add: left_distrib right_distrib) |
889 also from ngt1 have "{1..<n} = {1..n - 1}" |
890 also from ngt1 have "{1..<n} = {1..n - 1}" |
890 by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) |
891 by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) |
891 also from ngt1 |
892 also from ngt1 |
892 have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)" |
893 have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)" |
893 by (simp only: mult_ac gauss_sum [of "n - 1"]) |
894 by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def) |
894 (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]]) |
895 (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]]) |
895 finally show ?thesis by (simp add: algebra_simps) |
896 finally show ?thesis by (simp add: algebra_simps) |
896 next |
897 next |
897 assume "\<not>(n > 1)" |
898 assume "\<not>(n > 1)" |
898 hence "n = 1 \<or> n = 0" by auto |
899 hence "n = 1 \<or> n = 0" by auto |
904 proof - |
905 proof - |
905 have |
906 have |
906 "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) = |
907 "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) = |
907 of_nat(n) * (a + (a + of_nat(n - 1)*d))" |
908 of_nat(n) * (a + (a + of_nat(n - 1)*d))" |
908 by (rule arith_series_general) |
909 by (rule arith_series_general) |
909 thus ?thesis by (auto simp add: of_nat_id) |
910 thus ?thesis |
|
911 unfolding One_nat_def by (auto simp add: of_nat_id) |
910 qed |
912 qed |
911 |
913 |
912 lemma arith_series_int: |
914 lemma arith_series_int: |
913 "(2::int) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = |
915 "(2::int) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = |
914 of_nat n * (a + (a + of_nat(n - 1)*d))" |
916 of_nat n * (a + (a + of_nat(n - 1)*d))" |
944 (auto simp: diff_add_assoc2 intro: setsum_mono) |
946 (auto simp: diff_add_assoc2 intro: setsum_mono) |
945 ultimately |
947 ultimately |
946 show ?case by simp |
948 show ?case by simp |
947 qed |
949 qed |
948 |
950 |
|
951 subsection {* Products indexed over intervals *} |
|
952 |
|
953 syntax |
|
954 "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10) |
|
955 "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10) |
|
956 "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10) |
|
957 "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10) |
|
958 syntax (xsymbols) |
|
959 "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10) |
|
960 "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10) |
|
961 "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10) |
|
962 "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10) |
|
963 syntax (HTML output) |
|
964 "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10) |
|
965 "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10) |
|
966 "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10) |
|
967 "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10) |
|
968 syntax (latex_prod output) |
|
969 "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
970 ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) |
|
971 "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
972 ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) |
|
973 "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
974 ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10) |
|
975 "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
976 ("(3\<^raw:$\prod_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10) |
|
977 |
|
978 translations |
|
979 "\<Prod>x=a..b. t" == "CONST setprod (%x. t) {a..b}" |
|
980 "\<Prod>x=a..<b. t" == "CONST setprod (%x. t) {a..<b}" |
|
981 "\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}" |
|
982 "\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}" |
|
983 |
949 end |
984 end |