# HG changeset patch # User paulson # Date 1443629352 -3600 # Node ID dcf7be51bf5ddda27a36d6911520e0235298a712 # Parent f49644098959b0f2e6410234c4b4a1b38b99ccce Dead wood removal diff -r f49644098959 -r dcf7be51bf5d src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Fri Sep 25 23:01:34 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Wed Sep 30 17:09:12 2015 +0100 @@ -10,74 +10,6 @@ "~~/src/HOL/Library/Permutations" begin -subsection\First some facts about products\ - -lemma setprod_add_split: - fixes m n :: nat - assumes mn: "m \ n + 1" - shows "setprod f {m..n+p} = setprod f {m .. n} * setprod f {n+1..n+p}" -proof - - let ?A = "{m..n+p}" - let ?B = "{m..n}" - let ?C = "{n+1..n+p}" - from mn have un: "?B \ ?C = ?A" - by auto - from mn have dj: "?B \ ?C = {}" - by auto - have f: "finite ?B" "finite ?C" - by simp_all - from setprod.union_disjoint[OF f dj, of f, unfolded un] show ?thesis . -qed - - -lemma setprod_offset: - fixes m n :: nat - shows "setprod f {m + p .. n + p} = setprod (\i. f (i + p)) {m..n}" - by (rule setprod.reindex_bij_witness[where i="op + p" and j="\i. i - p"]) auto - -lemma setprod_singleton: "setprod f {x} = f x" - by simp - -lemma setprod_singleton_nat_seg: - fixes n :: "'a::order" - shows "setprod f {n..n} = f n" - by simp - -lemma setprod_numseg: - "setprod f {m..0} = (if m = 0 then f 0 else 1)" - "setprod f {m .. Suc n} = - (if m \ Suc n then f (Suc n) * setprod f {m..n} else setprod f {m..n})" - by (auto simp add: atLeastAtMostSuc_conv) - -lemma setprod_le: - fixes f g :: "'b \ 'a::linordered_idom" - assumes fS: "finite S" - and fg: "\x\S. f x \ 0 \ f x \ g x" - shows "setprod f S \ setprod g S" - using fS fg - apply (induct S) - apply simp - apply auto - apply (rule mult_mono) - apply (auto intro: setprod_nonneg) - done - -(* FIXME: In Finite_Set there is a useless further assumption *) -lemma setprod_inversef: - "finite A \ setprod (inverse \ f) A = (inverse (setprod f A) :: 'a:: field)" - apply (erule finite_induct) - apply (simp) - apply simp - done - -lemma setprod_le_1: - fixes f :: "'b \ 'a::linordered_idom" - assumes fS: "finite S" - and f: "\x\S. f x \ 0 \ f x \ 1" - shows "setprod f S \ 1" - using setprod_le[OF fS f] unfolding setprod.neutral_const . - - subsection \Trace\ definition trace :: "'a::semiring_1^'n^'n \ 'a" @@ -1275,16 +1207,16 @@ text \Explicit formulas for low dimensions.\ lemma setprod_neutral_const: "setprod f {(1::nat)..1} = f 1" - by (fact setprod_singleton_nat_seg) + by simp lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2" - by (simp add: eval_nat_numeral setprod_numseg mult.commute) + by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute) lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3" - by (simp add: eval_nat_numeral setprod_numseg mult.commute) + by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute) lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1" - by (simp add: det_def sign_id) + by (simp add: det_def of_nat_Suc sign_id) lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1" proof - diff -r f49644098959 -r dcf7be51bf5d src/HOL/Multivariate_Analysis/ex/Approximations.thy --- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy Fri Sep 25 23:01:34 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy Wed Sep 30 17:09:12 2015 +0100 @@ -27,9 +27,9 @@ lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \ inverse(2 ^ 32)" apply (simp only: abs_diff_le_iff) apply (rule sin_pi6_straddle, simp_all) - using Taylor_sin [of "1686629713/3221225472" 11] + using Taylor_sin [of "1686629713/3221225472" 11] apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) - apply (simp only: pos_le_divide_eq [symmetric]) + apply (simp only: pos_le_divide_eq [symmetric]) using Taylor_sin [of "6746518853/12884901888" 11] apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric]) diff -r f49644098959 -r dcf7be51bf5d src/HOL/Old_Number_Theory/Finite2.thy --- a/src/HOL/Old_Number_Theory/Finite2.thy Fri Sep 25 23:01:34 2015 +0200 +++ b/src/HOL/Old_Number_Theory/Finite2.thy Wed Sep 30 17:09:12 2015 +0100 @@ -37,15 +37,11 @@ qed lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)" - apply (induct set: finite) - apply (auto simp add: distrib_right distrib_left) - done +by (simp add: of_nat_mult) lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = int(c) * int(card X)" - apply (induct set: finite) - apply (auto simp add: distrib_left) - done +by (simp add: of_nat_mult) lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = c * setsum f A"