Lemmas on dvd, power and finite summation added or strengthened.
authorballarin
Fri Aug 26 10:01:06 2005 +0200 (2005-08-26)
changeset 17149e2b19c92ef51
parent 17148 858cab621db2
child 17150 ce2a1aeb42aa
Lemmas on dvd, power and finite summation added or strengthened.
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Integ/NatSimprocs.thy
src/HOL/Power.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Aug 26 08:42:52 2005 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Aug 26 10:01:06 2005 +0200
     1.3 @@ -1144,6 +1144,7 @@
     1.4  done
     1.5  
     1.6  (* FIXME: this is distributitivty, name as such! *)
     1.7 +(* suggested name: setsum_right_distrib (CB) *)
     1.8  
     1.9  lemma setsum_mult: 
    1.10    fixes f :: "'a => ('b::semiring_0_cancel)"
    1.11 @@ -1160,6 +1161,34 @@
    1.12    case False thus ?thesis by (simp add: setsum_def)
    1.13  qed
    1.14  
    1.15 +lemma setsum_left_distrib:
    1.16 +  "setsum f A * (r::'a::semiring_0_cancel) = (\<Sum>n\<in>A. f n * r)"
    1.17 +proof (cases "finite A")
    1.18 +  case True
    1.19 +  then show ?thesis
    1.20 +  proof induct
    1.21 +    case empty thus ?case by simp
    1.22 +  next
    1.23 +    case (insert x A) thus ?case by (simp add: left_distrib)
    1.24 +  qed
    1.25 +next
    1.26 +  case False thus ?thesis by (simp add: setsum_def)
    1.27 +qed
    1.28 +
    1.29 +lemma setsum_divide_distrib:
    1.30 +  "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
    1.31 +proof (cases "finite A")
    1.32 +  case True
    1.33 +  then show ?thesis
    1.34 +  proof induct
    1.35 +    case empty thus ?case by simp
    1.36 +  next
    1.37 +    case (insert x A) thus ?case by (simp add: add_divide_distrib)
    1.38 +  qed
    1.39 +next
    1.40 +  case False thus ?thesis by (simp add: setsum_def)
    1.41 +qed
    1.42 +
    1.43  lemma setsum_abs[iff]: 
    1.44    fixes f :: "'a => ('b::lordered_ab_group_abs)"
    1.45    shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
    1.46 @@ -1213,6 +1242,33 @@
    1.47  qed
    1.48  
    1.49  
    1.50 +text {* Commuting outer and inner summation *}
    1.51 +
    1.52 +lemma swap_inj_on:
    1.53 +  "inj_on (%(i, j). (j, i)) (A \<times> B)"
    1.54 +  by (unfold inj_on_def) fast
    1.55 +
    1.56 +lemma swap_product:
    1.57 +  "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
    1.58 +  by (simp add: split_def image_def) blast
    1.59 +
    1.60 +lemma setsum_commute:
    1.61 +  "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
    1.62 +proof (simp add: setsum_cartesian_product)
    1.63 +  have "(\<Sum>z\<in>A \<times> B. f (fst z) (snd z)) =
    1.64 +    (\<Sum>z\<in>(%(i, j). (j, i)) ` (A \<times> B). f (snd z) (fst z))"
    1.65 +    (is "?s = _")
    1.66 +    apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
    1.67 +    apply (simp add: split_def)
    1.68 +    done
    1.69 +  also have "... = (\<Sum>z\<in>B \<times> A. f (snd z) (fst z))"
    1.70 +    (is "_ = ?t")
    1.71 +    apply (simp add: swap_product)
    1.72 +    done
    1.73 +  finally show "?s = ?t" .
    1.74 +qed
    1.75 +
    1.76 +
    1.77  subsection {* Generalized product over a set *}
    1.78  
    1.79  constdefs
     2.1 --- a/src/HOL/Hyperreal/Series.thy	Fri Aug 26 08:42:52 2005 +0200
     2.2 +++ b/src/HOL/Hyperreal/Series.thy	Fri Aug 26 10:01:06 2005 +0200
     2.3 @@ -334,13 +334,7 @@
     2.4  
     2.5  text{*Sum of a geometric progression.*}
     2.6  
     2.7 -lemma sumr_geometric:
     2.8 - "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::real)"
     2.9 -apply (induct "n", auto)
    2.10 -apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1])
    2.11 -apply (auto simp add: mult_assoc left_distrib)
    2.12 -apply (simp add: right_distrib diff_minus mult_commute)
    2.13 -done
    2.14 +lemmas sumr_geometric = geometric_sum [where 'a = real]
    2.15  
    2.16  lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"
    2.17  apply (case_tac "x = 1")
     3.1 --- a/src/HOL/Integ/NatSimprocs.thy	Fri Aug 26 08:42:52 2005 +0200
     3.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Fri Aug 26 10:01:06 2005 +0200
     3.3 @@ -362,6 +362,13 @@
     3.4  
     3.5  lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, simp]
     3.6  
     3.7 +(* The following lemma should appear in Divides.thy, but there the proof
     3.8 +   doesn't work. *)
     3.9 +
    3.10 +lemma nat_dvd_not_less:
    3.11 +  "[| 0 < m; m < n |] ==> \<not> n dvd (m::nat)"
    3.12 +  by (unfold dvd_def) auto
    3.13 +
    3.14  ML
    3.15  {*
    3.16  val divide_minus1 = thm "divide_minus1";
     4.1 --- a/src/HOL/Power.thy	Fri Aug 26 08:42:52 2005 +0200
     4.2 +++ b/src/HOL/Power.thy	Fri Aug 26 10:01:06 2005 +0200
     4.3 @@ -351,6 +351,13 @@
     4.4  apply (erule dvd_imp_le, simp)
     4.5  done
     4.6  
     4.7 +lemma power_diff:
     4.8 +  assumes nz: "a ~= 0"
     4.9 +  shows "n <= m ==> (a::'a::{recpower, field}) ^ (m-n) = (a^m) / (a^n)"
    4.10 +  by (induct m n rule: diff_induct)
    4.11 +    (simp_all add: power_Suc nonzero_mult_divide_cancel_left nz)
    4.12 +
    4.13 +
    4.14  text{*ML bindings for the general exponentiation theorems*}
    4.15  ML
    4.16  {*
     5.1 --- a/src/HOL/SetInterval.thy	Fri Aug 26 08:42:52 2005 +0200
     5.2 +++ b/src/HOL/SetInterval.thy	Fri Aug 26 10:01:06 2005 +0200
     5.3 @@ -709,6 +709,18 @@
     5.4    "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
     5.5  by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
     5.6  
     5.7 +subsection {* The formula for geometric sums *}
     5.8 +
     5.9 +lemma geometric_sum:
    5.10 +  "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
    5.11 +  (x ^ n - 1) / (x - 1::'a::{field, recpower, division_by_zero})"
    5.12 +  apply (induct "n", auto)
    5.13 +  apply (rule_tac c = "x - 1" in field_mult_cancel_right_lemma)
    5.14 +  apply (auto simp add: mult_assoc left_distrib)
    5.15 +  apply (simp add: right_distrib diff_minus mult_commute power_Suc)
    5.16 +  done
    5.17 +
    5.18 +
    5.19  
    5.20  ML
    5.21  {*