# HG changeset patch # User ballarin # Date 1125043266 -7200 # Node ID e2b19c92ef51ce665e4462c1b86125d05af172d6 # Parent 858cab621db2139227534a2d9a731753fe6127e3 Lemmas on dvd, power and finite summation added or strengthened. diff -r 858cab621db2 -r e2b19c92ef51 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Aug 26 08:42:52 2005 +0200 +++ b/src/HOL/Finite_Set.thy Fri Aug 26 10:01:06 2005 +0200 @@ -1144,6 +1144,7 @@ done (* FIXME: this is distributitivty, name as such! *) +(* suggested name: setsum_right_distrib (CB) *) lemma setsum_mult: fixes f :: "'a => ('b::semiring_0_cancel)" @@ -1160,6 +1161,34 @@ case False thus ?thesis by (simp add: setsum_def) qed +lemma setsum_left_distrib: + "setsum f A * (r::'a::semiring_0_cancel) = (\n\A. f n * r)" +proof (cases "finite A") + case True + then show ?thesis + proof induct + case empty thus ?case by simp + next + case (insert x A) thus ?case by (simp add: left_distrib) + qed +next + case False thus ?thesis by (simp add: setsum_def) +qed + +lemma setsum_divide_distrib: + "setsum f A / (r::'a::field) = (\n\A. f n / r)" +proof (cases "finite A") + case True + then show ?thesis + proof induct + case empty thus ?case by simp + next + case (insert x A) thus ?case by (simp add: add_divide_distrib) + qed +next + case False thus ?thesis by (simp add: setsum_def) +qed + lemma setsum_abs[iff]: fixes f :: "'a => ('b::lordered_ab_group_abs)" shows "abs (setsum f A) \ setsum (%i. abs(f i)) A" @@ -1213,6 +1242,33 @@ qed +text {* Commuting outer and inner summation *} + +lemma swap_inj_on: + "inj_on (%(i, j). (j, i)) (A \ B)" + by (unfold inj_on_def) fast + +lemma swap_product: + "(%(i, j). (j, i)) ` (A \ B) = B \ A" + by (simp add: split_def image_def) blast + +lemma setsum_commute: + "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)" +proof (simp add: setsum_cartesian_product) + have "(\z\A \ B. f (fst z) (snd z)) = + (\z\(%(i, j). (j, i)) ` (A \ B). f (snd z) (fst z))" + (is "?s = _") + apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on) + apply (simp add: split_def) + done + also have "... = (\z\B \ A. f (snd z) (fst z))" + (is "_ = ?t") + apply (simp add: swap_product) + done + finally show "?s = ?t" . +qed + + subsection {* Generalized product over a set *} constdefs diff -r 858cab621db2 -r e2b19c92ef51 src/HOL/Hyperreal/Series.thy --- a/src/HOL/Hyperreal/Series.thy Fri Aug 26 08:42:52 2005 +0200 +++ b/src/HOL/Hyperreal/Series.thy Fri Aug 26 10:01:06 2005 +0200 @@ -334,13 +334,7 @@ text{*Sum of a geometric progression.*} -lemma sumr_geometric: - "x ~= 1 ==> (\i=0.. (%n. x ^ n) sums (1/(1 - x))" apply (case_tac "x = 1") diff -r 858cab621db2 -r e2b19c92ef51 src/HOL/Integ/NatSimprocs.thy --- a/src/HOL/Integ/NatSimprocs.thy Fri Aug 26 08:42:52 2005 +0200 +++ b/src/HOL/Integ/NatSimprocs.thy Fri Aug 26 10:01:06 2005 +0200 @@ -362,6 +362,13 @@ lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, simp] +(* The following lemma should appear in Divides.thy, but there the proof + doesn't work. *) + +lemma nat_dvd_not_less: + "[| 0 < m; m < n |] ==> \ n dvd (m::nat)" + by (unfold dvd_def) auto + ML {* val divide_minus1 = thm "divide_minus1"; diff -r 858cab621db2 -r e2b19c92ef51 src/HOL/Power.thy --- a/src/HOL/Power.thy Fri Aug 26 08:42:52 2005 +0200 +++ b/src/HOL/Power.thy Fri Aug 26 10:01:06 2005 +0200 @@ -351,6 +351,13 @@ apply (erule dvd_imp_le, simp) done +lemma power_diff: + assumes nz: "a ~= 0" + shows "n <= m ==> (a::'a::{recpower, field}) ^ (m-n) = (a^m) / (a^n)" + by (induct m n rule: diff_induct) + (simp_all add: power_Suc nonzero_mult_divide_cancel_left nz) + + text{*ML bindings for the general exponentiation theorems*} ML {* diff -r 858cab621db2 -r e2b19c92ef51 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Fri Aug 26 08:42:52 2005 +0200 +++ b/src/HOL/SetInterval.thy Fri Aug 26 10:01:06 2005 +0200 @@ -709,6 +709,18 @@ "setsum f {Suc m.. (\i=0..