Commit be2bf69d authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

renamings to use generic sum/prod lemmas from their locale

parent 8d513a937b50
......@@ -391,7 +391,7 @@ next
apply (unfold poly_y_x_def)
apply (unfold degree_monom_eq)
apply (subst(2) lessThan_Suc_atMost[symmetric])
apply (unfold sum_lessThan_Suc)
apply (unfold sum.lessThan_Suc)
apply (subst sum.neutral,force)
apply (subst(14) poly_as_sum_of_monoms[symmetric])
apply (unfold smult_as_map_poly)
......
......@@ -39,7 +39,7 @@ proof(intro antisym[OF degree_mult_le] le_degree, unfold coeff_mult)
then show ?thesis by (intro sum.neutral, auto)
qed
also have "sum ?f {..degree p} = sum ?f {..<degree p} + ?f (degree p)"
by(fold lessThan_Suc_atMost, unfold sum_lessThan_Suc, auto)
by(fold lessThan_Suc_atMost, unfold sum.lessThan_Suc, auto)
also have "sum ?f {..<degree p} = 0"
proof-
{fix x assume "x < degree p"
......
......@@ -139,7 +139,7 @@ proof -
also have "\<dots> = (\<Sum>i = Suc 0..n. (n choose i) * Stirling i m)"
by (intro sum.mono_neutral_right) auto
also have "\<dots> = real (\<Sum>i = 0..n. Stirling i m * (n choose i)) - real (Stirling 0 m)"
by (simp add: sum_head_Suc mult_ac)
by (simp add: sum.atLeast_Suc_atMost mult_ac)
also have "real (\<Sum>i = 0..n. Stirling i m * (n choose i)) = real (Stirling (Suc n) (Suc m))"
by (rule Suc.IH [symmetric])
also have "real (\<Sum>i = 0..n. (n choose i) * Stirling (Suc i) m) =
......
......@@ -1093,10 +1093,10 @@ proof -
from psi_odd_def have "psi_odd n = (\<Sum>d=1..n. mangoldt_odd d)"
by simp
also from * have "\<dots> = psi_odd_2 n"
by (cases "n \<ge> 1") (simp_all add: eval_nat_numeral sum_head_Suc)
by (cases "n \<ge> 1") (simp_all add: eval_nat_numeral sum.atLeast_Suc_atMost)
also from psi_residues_compare_2 have "\<dots> \<le> psi_even_2 n" .
also from ** have "\<dots> = psi_even n"
by (cases "n \<ge> 1") (simp_all add: eval_nat_numeral sum_head_Suc psi_even_def)
by (cases "n \<ge> 1") (simp_all add: eval_nat_numeral sum.atLeast_Suc_atMost psi_even_def)
finally show ?thesis .
qed
......@@ -1436,7 +1436,7 @@ next
\<le> (\<Sum>d = 1..3. (- 1) ^ (d + 1) * psi (n div d))"
by simp
also have "\<dots> = psi n - psi (n div 2) + psi (n div 3)"
by (simp add: sum_head_Suc numeral_2_eq_2)
by (simp add: sum.atLeast_Suc_atMost numeral_2_eq_2)
finally show "ln (fact n) - 2 * ln (fact (n div 2)) \<le> psi n - psi (n div 2) + psi (n div 3)" .
qed
......@@ -1742,7 +1742,7 @@ next
also have "\<dots> = (\<Sum>p | prime p \<and> p \<in> {1..n}. (\<Sum>k = 1..n. ln p / p^k))"
by (subst sum.Sigma) auto
also have "\<dots> = ?L + (\<Sum>p | prime p \<and> p \<in> {1..n}. (\<Sum>k = 2..n. ln p / p^k))"
by (simp add: comm_monoid_add_class.sum.distrib sum_head_Suc numeral_2_eq_2)
by (simp add: comm_monoid_add_class.sum.distrib sum.atLeast_Suc_atMost numeral_2_eq_2)
finally have "?M - ?L \<le> (\<Sum>p | prime p \<and> p \<in> {1..n}. (\<Sum>k = 2..n. ln p / p^k))"
by (simp add: algebra_simps)
also have "\<dots> = (\<Sum>p | prime p \<and> p \<in> {1..n}. ln p * (\<Sum>k = 2..n. inverse p ^ k))"
......@@ -1826,7 +1826,7 @@ next
also have "\<dots> \<le> 3 - ln 2"
using ln_2_less_1 by (simp add: algebra_simps)
finally show ?thesis
using True by (simp add: algebra_simps sum_head_Suc [of 2 n])
using True by (simp add: algebra_simps sum.atLeast_Suc_atMost [of 2 n])
qed
finally show ?thesis .
qed
......
......@@ -4502,7 +4502,7 @@ next
(auto simp add: LCons image_iff less_Suc_eq_0_disj)
also have "llength xs + \<dots> = (\<Sum>i<Suc n. llength (lnth xss i))"
unfolding atLeast0LessThan[symmetric] LCons
by(subst (2) sum_head_upt_Suc) simp_all
by(subst (2) sum.atLeast_Suc_lessThan) simp_all
finally show ?thesis using LCons by simp
qed
qed
......@@ -4603,7 +4603,7 @@ next
{ have "(\<Sum>i < m + length xss'. llength (lnth xss i)) =
(\<Sum>i < length xss'. llength (lnth xss i)) +
(\<Sum>i = length xss'..<m + length xss'. llength (lnth xss i))"
by(subst (1 2) atLeast0LessThan[symmetric])(subst sum_add_nat_ivl, simp_all)
by(subst (1 2) atLeast0LessThan[symmetric])(subst sum.atLeastLessThan_concat, simp_all)
also from lnth_prefix have "(\<Sum>i < length xss'. llength (lnth xss i)) = 0" by simp
also have "{length xss'..<m + length xss'} = {0+length xss'..<m+length xss'}" by auto
also have "(\<Sum>i = 0 + length xss'..<m + length xss'. llength (lnth xss i)) =
......@@ -4612,7 +4612,7 @@ next
also have "\<dots> = (\<Sum>i = 0..<m. llength (lnth (LCons (LCons x xs') xss'') i))"
unfolding xss by(subst lnth_lappend2) simp+
also have "\<dots> = eSuc (llength xs') + (\<Sum>i = Suc 0..<m. llength (lnth (LCons (LCons x xs') xss'') i))"
by(subst sum_head_upt_Suc) simp_all
by(subst sum.atLeast_Suc_lessThan) simp_all
also {
fix i
assume "i \<in> {Suc 0..<m}"
......@@ -4623,7 +4623,7 @@ next
(\<Sum>i = Suc 0..<m. llength (lnth (LCons xs' xss'') i))" by(simp)
also have "eSuc (llength xs') + \<dots> = 1 + (llength (lnth (LCons xs' xss'') 0) + \<dots>)"
by(simp add: eSuc_plus_1 ac_simps)
also note sum_head_upt_Suc[symmetric, OF \<open>0 < m\<close>]
also note sum.atLeast_Suc_lessThan[symmetric, OF \<open>0 < m\<close>]
finally have "enat (Suc n) = (\<Sum>i<m + length xss'. llength (lnth xss i)) + enat n'"
unfolding eSuc_enat[symmetric] n_eq by(simp add: eSuc_plus_1 ac_simps atLeast0LessThan) }
ultimately show ?thesis by blast
......
......@@ -54,10 +54,10 @@ lemma all1_vec_scalar_prod:
shows "all1_vec (length xs) \<bullet> (vec_of_list xs) = sum_list xs"
proof -
have "all1_vec (length xs) \<bullet> (vec_of_list xs) = (\<Sum>i = 0..<dim_vec (vec_of_list xs). vec_of_list xs $ i)"
unfolding scalar_prod_def by (metis (no_types, lifting) all1_vec_def mult_cancel_right1 sum_ivl_cong
unfolding scalar_prod_def by (metis (no_types, lifting) all1_vec_def mult_cancel_right1 sum.ivl_cong
vec.abs_eq dim_vec index_vec vec_of_list.abs_eq)
also have "... = (\<Sum>i = 0..<length xs. xs ! i)" using vec.abs_eq dim_vec vec_of_list.abs_eq
by (metis sum_ivl_cong index_vec)
by (metis sum.ivl_cong index_vec)
also have "... = sum_list xs" by (simp add: sum_list_sum_nth)
finally show ?thesis by auto
qed
......
......@@ -128,11 +128,11 @@ proof (induction xs arbitrary: n rule: psums.induct[case_names Nil sng rec])
also from rec.prems Suc have "\<dots> = (\<Sum>i\<le>m. ((x+y) # xs) ! i)"
by (intro rec.IH) simp_all
also have "\<dots> = x + y + (\<Sum>i=1..m. (y#xs) ! i)"
by (auto simp: atLeast0AtMost [symmetric] sum_head_Suc[of 0])
by (auto simp: atLeast0AtMost [symmetric] sum.atLeast_Suc_atMost[of 0])
also have "(\<Sum>i=1..m. (y#xs) ! i) = (\<Sum>i=Suc 1..Suc m. (x#y#xs) ! i)"
by (subst sum_shift_bounds_cl_Suc_ivl) simp
also from Suc have "x + y + \<dots> = (\<Sum>i\<le>n. (x#y#xs) ! i)"
by (auto simp: atLeast0AtMost [symmetric] sum_head_Suc add_ac)
by (auto simp: atLeast0AtMost [symmetric] sum.atLeast_Suc_atMost add_ac)
finally show ?thesis .
qed simp
qed simp_all
......
......@@ -265,7 +265,7 @@ next
have "(\<Sum>k = 0..n. of_nat (Stirling n k) * (of_nat k * ffact k a)) =
(\<Sum>k = 0..n+2. of_nat (Stirling n k) * (of_nat k * ffact k a))" by simp
also have "\<dots> = (\<Sum>k = Suc 0 .. Suc (Suc n). of_nat (Stirling n k) * (of_nat k * ffact k a)) "
by (simp only: sum_head_Suc [of 0 "n + 2"]) simp
by (simp only: sum.atLeast_Suc_atMost [of 0 "n + 2"]) simp
also have "\<dots> = (\<Sum>k = 0 .. Suc n. of_nat (Stirling n (Suc k)) * (of_nat (Suc k) * ffact (Suc k) a))"
by (simp only: image_Suc_atLeastAtMost sum_shift_bounds_cl_Suc_ivl)
also have "\<dots> = (\<Sum>k = 0 .. Suc n. of_nat ((Suc k) * Stirling n (Suc k)) * ffact (Suc k) a)"
......@@ -280,7 +280,7 @@ next
also have "\<dots> = (\<Sum>k = Suc 0..Suc n. of_nat (Stirling (Suc n) k) * ffact k a)"
by (simp only: image_Suc_atLeastAtMost sum_shift_bounds_cl_Suc_ivl)
also have "\<dots> = (\<Sum>k = 0..Suc n. of_nat (Stirling (Suc n) k) * ffact k a)"
by (simp only: sum_head_Suc [of "0" "Suc n"]) simp
by (simp only: sum.atLeast_Suc_atMost [of "0" "Suc n"]) simp
finally show ?case by simp
qed
......@@ -303,7 +303,7 @@ next
(\<Sum>k = 0..n. (- 1) ^ (Suc n - k) * of_nat (n * stirling n k) * a ^ k)"
by (simp add: Suc_diff_le)
also have "\<dots> = (\<Sum>k = Suc 0..Suc n. (- 1) ^ (Suc n - k) * of_nat (n * stirling n k) * a ^ k)"
by (simp add: sum_head_Suc) (cases n; simp)
by (simp add: sum.atLeast_Suc_atMost) (cases n; simp)
also have "\<dots> = (\<Sum>k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (n * stirling n (Suc k)) * a ^ Suc k)"
by (simp only: sum_shift_bounds_cl_Suc_ivl)
finally show ?thesis by simp
......@@ -315,7 +315,7 @@ next
also have "\<dots> = (\<Sum>k = Suc 0..Suc n. (- 1) ^ (Suc n - k) * of_nat (stirling (Suc n) k) * a ^ k)"
by (simp only: sum_shift_bounds_cl_Suc_ivl)
also have "\<dots> = (\<Sum>k = 0..Suc n. (- 1) ^ (Suc n - k) * of_nat (stirling (Suc n) k) * a ^ k)"
by (simp add: sum_head_Suc)
by (simp add: sum.atLeast_Suc_atMost)
finally show ?case .
qed
......
......@@ -336,11 +336,11 @@ proof -
also have "(\<Sum>j=0..m. poly (df (Suc j)) 0) = (\<Sum>j=Suc 0..Suc m. poly (df j) 0)"
by (rule sum_shift_bounds_cl_Suc_ivl [symmetric])
also have "\<dots> = (\<Sum>j=0..Suc m. poly (df j) 0) - poly f 0"
by (subst (2) sum_head_Suc) (simp_all add: df_def)
by (subst (2) sum.atLeast_Suc_atMost) (simp_all add: df_def)
also have "(\<Sum>j=0..m. poly (df (Suc j)) u) = (\<Sum>j=Suc 0..Suc m. poly (df j) u)"
by (rule sum_shift_bounds_cl_Suc_ivl [symmetric])
also have "\<dots> = (\<Sum>j=0..Suc m. poly (df j) u) - poly f u"
by (subst (2) sum_head_Suc) (simp_all add: df_def)
by (subst (2) sum.atLeast_Suc_atMost) (simp_all add: df_def)
finally have "((\<lambda>t. - (exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u))) has_integral
-(exp u * ((\<Sum>j = 0..Suc m. poly (df j) 0) - poly f 0) -
((\<Sum>j = 0..Suc m. poly (df j) u) - poly f u))) {0..1}"
......
......@@ -439,7 +439,7 @@ proof -
have "(\<Sum>i<n-1. abs(u s ((T^^(i * s+t))x))) + u s ((T^^((n-1) * s+t)) x)
\<le> (\<Sum>i<n-1. abs(u s ((T^^(i * s+t))x))) + abs(u s ((T^^((n-1) * s+t)) x))" by auto
also have "... \<le> (\<Sum>i<n. abs(u s ((T^^(i* s+t))x)))"
using \<open>n\<ge>1\<close> lessThan_Suc_atMost sum_lessThan_Suc[where ?n = "n-1" and ?f = "\<lambda>i. abs(u s ((T^^(i* s+t))x))" , symmetric] by auto
using \<open>n\<ge>1\<close> lessThan_Suc_atMost sum.lessThan_Suc[where ?n = "n-1" and ?f = "\<lambda>i. abs(u s ((T^^(i* s+t))x))" , symmetric] by auto
finally have ***: "(\<Sum>i<n-1. abs(u s ((T^^(i* s+t))x))) + u s ((T^^((n-1) * s+t)) x) \<le> (\<Sum>i<n. abs(u s ((T^^(i* s+t))x)))"
by simp
......@@ -502,7 +502,7 @@ proof -
also have "... \<le> (\<Sum>j \<in> {(n-1) * s+t..<m}. abs(u 1 ((T^^j) x))) + (\<Sum>j \<in> {m..<n * s+t}. abs(u 1 ((T^^j) x)))"
by auto
also have "... = (\<Sum>j \<in> {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^j) x)))"
apply (rule sum_add_nat_ivl) using m2 by auto
apply (rule sum.atLeastLessThan_concat) using m2 by auto
finally have *: "birkhoff_sum (u 1) (n * s+t-m) ((T^^m) x) \<le> (\<Sum>j \<in> {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^j) x)))"
by auto
......@@ -535,7 +535,7 @@ proof -
also have "... \<le> (\<Sum>j \<in> {p* s+t..<m-l}. abs(u 1 ((T^^j) x))) + (\<Sum>j \<in> {m-l..<(p+1)* s+t}. abs(u 1 ((T^^j) x)))"
by auto
also have "... = (\<Sum>j \<in> {p* s+t..<(p+1)* s+t}. abs(u 1 ((T^^j) x)))"
apply (rule sum_add_nat_ivl) using p1 p2 by auto
apply (rule sum.atLeastLessThan_concat) using p1 p2 by auto
finally have *: "birkhoff_sum (u 1) (m-l - (p* s+t)) ((T^^(p* s+t)) x)
\<le> (\<Sum>j \<in> {p* s+t..<(p+1)* s+t}. abs(u 1 ((T^^j) x)))"
by auto
......@@ -559,7 +559,7 @@ proof -
also have "... \<le> 2* K * s + (\<Sum>i \<in> {p* s+t..<(n-1) * s+t}. F ((T^^i) x)) + (\<Sum>i \<in>{(n-1) * s+t..<n * s+t}. F ((T^^i) x))"
apply (auto, rule sum_mono2) using \<open>(p+1)* s+t\<le>(n-1) * s+t\<close> F_pos by auto
also have "... = 2* K * s + (\<Sum>i \<in> {p* s+t..<n * s+t}. F ((T^^i) x))"
apply (auto, rule sum_add_nat_ivl) using \<open>p\<le>n-1\<close> by auto
apply (auto, rule sum.atLeastLessThan_concat) using \<open>p\<le>n-1\<close> by auto
finally have A0: "(\<Sum>i \<in> {p* s+t..<(p+1)* s+t}. abs(u 1 ((T^^i) x))) + (\<Sum>i \<in> {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^i) x)))
\<le> 2* K * s + (\<Sum>i \<in> {p* s+t..<n * s+t}. F ((T^^i) x))"
by simp
......@@ -595,7 +595,7 @@ proof -
apply (rule sum_mono2) using \<open>p\<le>n-1\<close> by auto
have A4: "birkhoff_sum F (p * s + t) x + (\<Sum>i \<in> {p* s+t..<n * s+t}. F ((T^^i) x)) = birkhoff_sum F (n * s + t) x"
unfolding birkhoff_sum_def apply (subst atLeast0LessThan[symmetric])+ apply (rule sum_add_nat_ivl)
unfolding birkhoff_sum_def apply (subst atLeast0LessThan[symmetric])+ apply (rule sum.atLeastLessThan_concat)
using \<open>p\<le>n-1\<close> by auto
have "u (n * s+t) x \<le> u m x + (\<Sum>i \<in> {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^i) x)))"
......
......@@ -236,7 +236,7 @@ proof -
finally show ?thesis by auto
qed
have "(\<Sum>j<a*N. u N ((T^^j) x)) - (\<Sum>j<n-2*N. u N ((T^^j) x)) = (\<Sum>j\<in>{n-2*N..<a*N}. u N ((T^^j) x))"
using sum_add_nat_ivl[OF _ \<open>a*N \<ge> n - 2*N\<close>, of 0 "\<lambda>j. u N ((T^^j) x)", symmetric] atLeast0LessThan by simp
using sum.atLeastLessThan_concat[OF _ \<open>a*N \<ge> n - 2*N\<close>, of 0 "\<lambda>j. u N ((T^^j) x)", symmetric] atLeast0LessThan by simp
also have "... \<le> (\<Sum>j\<in>{n-2*N..<a*N}. E2)" by (rule sum_mono[OF I])
also have "... = (a*N - (n-2*N)) * E2" by simp
also have "... \<le> N * E2" using \<open>(a*N - (n-2*N)) \<le> N\<close> \<open>E2 \<ge> 0\<close> by (simp add: mult_right_mono)
......
......@@ -835,7 +835,7 @@ proof -
add.commute add.left_neutral by auto
finally have *: "birkhoff_sum f m ((T^^n)x) = (\<Sum>j\<in>{n..< m+n}. f ((T ^^j) x))" unfolding birkhoff_sum_def by auto
have "birkhoff_sum f (n+m) x = (\<Sum>i<n. f((T^^i)x)) + (\<Sum>i\<in>{n..<m+n}. f((T^^i)x))"
unfolding birkhoff_sum_def by (metis add.commute add.right_neutral atLeast0LessThan le_add2 sum_add_nat_ivl)
unfolding birkhoff_sum_def by (metis add.commute add.right_neutral atLeast0LessThan le_add2 sum.atLeastLessThan_concat)
also have "... = birkhoff_sum f n x + (\<Sum>i\<in>{n..<m+n}. f((T^^i)x))" unfolding birkhoff_sum_def by simp
finally show ?thesis using * by simp
qed
......
......@@ -256,7 +256,7 @@ proof (unfold_locales)
then have "finite (range u)" using finite_nat_iff_bounded by auto
then have "\<exists>i j. (i<j) \<and> (u i = u j)" by (metis finite_imageD infinite_UNIV_nat injI less_linear)
then obtain i k where "k>0" "u i = u (i+k)" using less_imp_add_positive by blast
moreover have "s 0 (i+k) = s 0 i + s i k" unfolding s_def by (simp add: sum_add_nat_ivl)
moreover have "s 0 (i+k) = s 0 i + s i k" unfolding s_def by (simp add: sum.atLeastLessThan_concat)
ultimately have "(s i k) mod n = 0" using u_def nat_mod_cong by metis
then obtain r where "s i k = n * r" by auto
moreover have "s i k > 0" unfolding s_def
......@@ -1261,7 +1261,7 @@ proof
ultimately have "n = (\<Sum>i\<in>{0..<1}. return_time_function A (((induced_map A)^^i) y))
+ (\<Sum>i \<in> {1..<N0+1}. return_time_function A (((induced_map A)^^i) y))" using \<open>n \<ge> m\<close> by simp
then have "n = (\<Sum>i\<in>{0..<N0+1}. return_time_function A (((induced_map A)^^i) y))"
using le_add2 sum_add_nat_ivl by blast
using le_add2 sum.atLeastLessThan_concat by blast
moreover have "N0 + 1 \<le> n" using \<open>N0 \<le> n-m\<close> \<open>n - m < n\<close> by linarith
ultimately show ?thesis by (metis atLeast0LessThan)
qed
......
......@@ -242,7 +242,7 @@ proof (induction n)
exp (- x\<^sup>2) / sqrt pi *
(\<Sum>i<Suc n. (- 1) ^ i * fact (2 * i) / (4 ^ i * fact i) / x ^ (2 * i + 1)) +
erf_remainder (Suc n) x"
by (subst sum_lessThan_Suc) (simp add: algebra_simps)
by (subst sum.lessThan_Suc) (simp add: algebra_simps)
finally show ?case .
qed (auto simp: assms erf_remainder_0_conv_erfc)
......
......@@ -65,7 +65,7 @@ lemma sum_add_split_nat_ivl:
and g: "!!i. [| m <= i; i < k |] ==> g i = f i"
and h: "!!i. [| k <= i; i < n |] ==> h i = f i"
shows "sum g {m..<k} + sum h {k..<n} = sum f {m..<n}"
using le g h by (simp add: sum_add_nat_ivl cong: sum.cong_simp)
using le g h by (simp add: sum.atLeastLessThan_concat cong: sum.cong_simp)
lemma ivl_splice_Un:
"{0..<2*n::nat} = ((*) 2 ` {0..<n}) \<union> ((%i. Suc (2*i)) ` {0..<n})"
......
......@@ -51,7 +51,7 @@ next
finally show ?thesis .
qed
from this show ?thesis
by (simp add: sum_head_Suc[of _ _ "\<lambda>k. (n choose k) * ?t k"])
by (simp add: sum.atLeast_Suc_atMost[of _ _ "\<lambda>k. (n choose k) * ?t k"])
qed
also have "\<dots> = ?t 0 + (\<Sum>k = 0..n. (n choose k + (n choose Suc k)) * ?u k)"
by (simp add: distrib_right sum.distrib)
......@@ -65,7 +65,7 @@ next
also have "\<dots> = ?v 0 + (\<Sum>k = Suc 0..Suc n. ?v k)"
by (simp only: sum_shift_bounds_cl_Suc_ivl diff_Suc_Suc mult.assoc)
also have "\<dots> = (\<Sum>k = 0..Suc n. (Suc n choose k) * ffact k x * ffact (Suc n - k) y)"
by (simp add: sum_head_Suc)
by (simp add: sum.atLeast_Suc_atMost)
finally show ?thesis .
qed
finally show ?case .
......@@ -123,7 +123,7 @@ next
finally show ?thesis .
qed
from this show ?thesis
by (simp add: sum_head_Suc[of _ _ "\<lambda>k. of_nat (n choose k) * ?t k"])
by (simp add: sum.atLeast_Suc_atMost[of _ _ "\<lambda>k. of_nat (n choose k) * ?t k"])
qed
also have "\<dots> = ?t 0 + (\<Sum>k = 0..n. of_nat (n choose k + (n choose Suc k)) * ?u k)"
by (simp add: distrib_right sum.distrib)
......@@ -137,7 +137,7 @@ next
also have "\<dots> = ?v 0 + (\<Sum>k = Suc 0..Suc n. ?v k)"
by (simp only: sum_shift_bounds_cl_Suc_ivl diff_Suc_Suc mult.assoc)
also have "\<dots> = (\<Sum>k = 0..Suc n. of_nat (Suc n choose k) * ffact k x * ffact (Suc n - k) y)"
by (simp add: sum_head_Suc)
by (simp add: sum.atLeast_Suc_atMost)
finally show ?thesis .
qed
finally show ?case .
......
......@@ -192,7 +192,7 @@ proof -
proof (cases "S = 0")
case True
have "(\<Sum>i = Suc 0..<n. f (u i) (u (Suc i))) = (\<Sum>i = 0..<n. f (u i) (u (Suc i))) - f(u 0) (u (Suc 0))"
using sum_head_upt_Suc[OF \<open>n > 0\<close>, of "\<lambda>i. f (u i) (u (Suc i))"] by simp
using sum.atLeast_Suc_lessThan[OF \<open>n > 0\<close>, of "\<lambda>i. f (u i) (u (Suc i))"] by simp
also have "... \<le> S/2" using True S_def nonneg by auto
finally have "0 < n \<and> (\<Sum>i = 0..<0. f (u i) (u (Suc i))) \<le> S/2 \<and> (\<Sum>i = Suc 0..<n. f (u i) (u (Suc i))) \<le> S/2"
using \<open>n > 0\<close> \<open>S = 0\<close> by auto
......
......@@ -507,7 +507,7 @@ qed
lemma sum_upto_add_nat:
"a \<le> b \<Longrightarrow> sum f {..<(a :: nat)} + sum f {a..<b} = sum f {..<b}"
by (metis atLeast0LessThan le0 sum_add_nat_ivl)
by (metis atLeast0LessThan le0 sum.atLeastLessThan_concat)
lemma nat_fun_sum_eq_conv:
fixes f :: "'a \<Rightarrow> nat"
......
......@@ -636,7 +636,7 @@ proof(rule thread_start_actions_okI)
let ?i = "length ?start_heap_obs + ?i'"
from \<open>i < m\<close> have "(\<Sum>i<m. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>) = ?i' + (\<Sum>i=i..<m. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>)"
unfolding atLeast0LessThan[symmetric] by(subst sum_add_nat_ivl) simp_all
unfolding atLeast0LessThan[symmetric] by(subst sum.atLeastLessThan_concat) simp_all
hence "?i' \<le> ?a" unfolding a_conv by simp
hence "?i \<le> a" using \<open>a \<ge> length ?start_heap_obs\<close> by arith
......@@ -666,18 +666,18 @@ proof(rule thread_start_actions_okI)
assume "i < k"
hence "(\<Sum>i<k. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>) =
(\<Sum>i<i. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>) + (\<Sum>i=i..<k. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>)"
unfolding atLeast0LessThan[symmetric] by(subst sum_add_nat_ivl) simp_all
unfolding atLeast0LessThan[symmetric] by(subst sum.atLeastLessThan_concat) simp_all
with i_conv have "(\<Sum>i=i..<k. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>) = l" "l = 0" by simp_all
moreover have "(\<Sum>i=i..<k. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>) \<ge> length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>"
by(subst sum_head_upt_Suc[OF \<open>i < k\<close>]) simp
by(subst sum.atLeast_Suc_lessThan[OF \<open>i < k\<close>]) simp
ultimately show False using nth_i by simp
next
assume "k < i"
hence "?i' = (\<Sum>i<k. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>) + (\<Sum>i=k..<i. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>)"
unfolding atLeast0LessThan[symmetric] by(subst sum_add_nat_ivl) simp_all
unfolding atLeast0LessThan[symmetric] by(subst sum.atLeastLessThan_concat) simp_all
with i_conv have "(\<Sum>i=k..<i. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>) = l" by simp
moreover have "(\<Sum>i=k..<i. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>) \<ge> length \<lbrace>snd (lnth E' k)\<rbrace>\<^bsub>o\<^esub>"
by(subst sum_head_upt_Suc[OF \<open>k < i\<close>]) simp
by(subst sum.atLeast_Suc_lessThan[OF \<open>k < i\<close>]) simp
ultimately show False using l by simp
qed
qed
......@@ -1021,7 +1021,7 @@ next
hence "(\<Sum>i<a_m. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>) = (\<Sum>i<a'_m. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>) + (\<Sum>i = a'_m..<a_m. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>)"
by(simp add: sum_upto_add_nat)
hence "a' - n < a - n" using \<open>a'_m < a_m\<close> a'_n E'_a'_m unfolding a_conv a'_conv
by(subst (asm) sum_head_upt_Suc) simp_all
by(subst (asm) sum.atLeast_Suc_lessThan) simp_all
with a_a' show False by simp
qed
......@@ -1090,7 +1090,7 @@ next
hence "(\<Sum>i<a'_m. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>) = (\<Sum>i<a_m. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>) + (\<Sum>i = a_m..<a'_m. length \<lbrace>snd (lnth E' i)\<rbrace>\<^bsub>o\<^esub>)"
by(simp add: sum_upto_add_nat)
with a'_less \<open>a_m < a'_m\<close> E'_a_m a_n a'_n show False
unfolding a'_conv a_conv by(subst (asm) sum_head_upt_Suc) simp_all
unfolding a'_conv a_conv by(subst (asm) sum.atLeast_Suc_lessThan) simp_all
qed
qed
with E'_a_m E'_a'_m have [simp]: "t_a' = t_a" "ta_a' = ta_a" by simp_all
......
......@@ -101,7 +101,7 @@ lemma vec_conjugate_sprod_comm:
fixes v w :: "'a :: {conjugatable_ring, comm_ring} vec"
assumes "v : carrier_vec n" and "w : carrier_vec n"
shows "v \<bullet>c w = (conjugate\<^sub>v w \<bullet> v)"
unfolding scalar_prod_def using assms by(subst sum_ivl_cong, auto simp: ac_simps)
unfolding scalar_prod_def using assms by(subst sum.ivl_cong, auto simp: ac_simps)
lemma vec_conjugate_square_zero:
fixes v :: "'a :: {conjugatable_ordered_ring,semiring_no_zero_divisors} vec"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment