diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Power.thy --- a/src/HOL/Power.thy Tue Mar 01 10:32:55 2016 +0100 +++ b/src/HOL/Power.thy Tue Mar 01 10:36:19 2016 +0100 @@ -6,7 +6,7 @@ section \Exponentiation\ theory Power -imports Num Equiv_Relations +imports Num begin subsection \Powers for Arbitrary Monoids\ @@ -232,7 +232,7 @@ end -class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors +context semiring_1_no_zero_divisors begin subclass power . @@ -251,13 +251,6 @@ end -context semidom -begin - -subclass semiring_1_no_zero_divisors .. - -end - context ring_1 begin @@ -307,8 +300,6 @@ context ring_1_no_zero_divisors begin -subclass semiring_1_no_zero_divisors .. - lemma power2_eq_1_iff: "a\<^sup>2 = 1 \ a = 1 \ a = - 1" using square_eq_1_iff [of a] by (simp add: power2_eq_square) @@ -851,70 +842,6 @@ qed -subsubsection \Generalized sum over a set\ - -lemma setsum_zero_power [simp]: - fixes c :: "nat \ 'a::division_ring" - shows "(\i\A. c i * 0^i) = (if finite A \ 0 \ A then c 0 else 0)" -apply (cases "finite A") - by (induction A rule: finite_induct) auto - -lemma setsum_zero_power' [simp]: - fixes c :: "nat \ 'a::field" - shows "(\i\A. c i * 0^i / d i) = (if finite A \ 0 \ A then c 0 / d 0 else 0)" - using setsum_zero_power [of "\i. c i / d i" A] - by auto - - -subsubsection \Generalized product over a set\ - -lemma setprod_constant: "finite A ==> (\x\ A. (y::'a::{comm_monoid_mult})) = y^(card A)" -apply (erule finite_induct) -apply auto -done - -lemma setprod_power_distrib: - fixes f :: "'a \ 'b::comm_semiring_1" - shows "setprod f A ^ n = setprod (\x. (f x) ^ n) A" -proof (cases "finite A") - case True then show ?thesis - by (induct A rule: finite_induct) (auto simp add: power_mult_distrib) -next - case False then show ?thesis - by simp -qed - -lemma power_setsum: - "c ^ (\a\A. f a) = (\a\A. c ^ f a)" - by (induct A rule: infinite_finite_induct) (simp_all add: power_add) - -lemma setprod_gen_delta: - assumes fS: "finite S" - shows "setprod (\k. if k=a then b k else c) S = (if a \ S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)" -proof- - let ?f = "(\k. if k=a then b k else c)" - {assume a: "a \ S" - hence "\ k\ S. ?f k = c" by simp - hence ?thesis using a setprod_constant[OF fS, of c] by simp } - moreover - {assume a: "a \ S" - let ?A = "S - {a}" - let ?B = "{a}" - have eq: "S = ?A \ ?B" using a by blast - have dj: "?A \ ?B = {}" by simp - from fS have fAB: "finite ?A" "finite ?B" by auto - have fA0:"setprod ?f ?A = setprod (\i. c) ?A" - apply (rule setprod.cong) by auto - have cA: "card ?A = card S - 1" using fS a by auto - have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto - have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" - using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] - by simp - then have ?thesis using a cA - by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)} - ultimately show ?thesis by blast -qed - subsection \Code generator tweak\ code_identifier