src/HOL/Power.thy
 changeset 62481 b5d8e57826df parent 62366 95c6cf433c91 child 63040 eb4ddd18d635
```--- 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 \<open>Exponentiation\<close>

theory Power
-imports Num Equiv_Relations
+imports Num
begin

subsection \<open>Powers for Arbitrary Monoids\<close>
@@ -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 \<longleftrightarrow> a = 1 \<or> a = - 1"
using square_eq_1_iff [of a] by (simp add: power2_eq_square)
@@ -851,70 +842,6 @@
qed

-subsubsection \<open>Generalized sum over a set\<close>
-
-lemma setsum_zero_power [simp]:
-  fixes c :: "nat \<Rightarrow> 'a::division_ring"
-  shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> 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 \<Rightarrow> 'a::field"
-  shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)"
-  using setsum_zero_power [of "\<lambda>i. c i / d i" A]
-  by auto
-
-
-subsubsection \<open>Generalized product over a set\<close>
-
-lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
-apply (erule finite_induct)
-apply auto
-done
-
-lemma setprod_power_distrib:
-  fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
-  shows "setprod f A ^ n = setprod (\<lambda>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 ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
-
-lemma setprod_gen_delta:
-  assumes fS: "finite S"
-  shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"
-proof-
-  let ?f = "(\<lambda>k. if k=a then b k else c)"
-  {assume a: "a \<notin> S"
-    hence "\<forall> k\<in> S. ?f k = c" by simp
-    hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
-  moreover
-  {assume a: "a \<in> S"
-    let ?A = "S - {a}"
-    let ?B = "{a}"
-    have eq: "S = ?A \<union> ?B" using a by blast
-    have dj: "?A \<inter> ?B = {}" by simp
-    from fS have fAB: "finite ?A" "finite ?B" by auto
-    have fA0:"setprod ?f ?A = setprod (\<lambda>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 \<open>Code generator tweak\<close>

code_identifier```