src/HOL/Power.thy
changeset 62481 b5d8e57826df
parent 62366 95c6cf433c91
child 63040 eb4ddd18d635
     1.1 --- a/src/HOL/Power.thy	Tue Mar 01 10:32:55 2016 +0100
     1.2 +++ b/src/HOL/Power.thy	Tue Mar 01 10:36:19 2016 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  section \<open>Exponentiation\<close>
     1.5  
     1.6  theory Power
     1.7 -imports Num Equiv_Relations
     1.8 +imports Num
     1.9  begin
    1.10  
    1.11  subsection \<open>Powers for Arbitrary Monoids\<close>
    1.12 @@ -232,7 +232,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
    1.17 +context semiring_1_no_zero_divisors
    1.18  begin
    1.19  
    1.20  subclass power .
    1.21 @@ -251,13 +251,6 @@
    1.22  
    1.23  end
    1.24  
    1.25 -context semidom
    1.26 -begin
    1.27 -
    1.28 -subclass semiring_1_no_zero_divisors ..
    1.29 -
    1.30 -end
    1.31 -
    1.32  context ring_1
    1.33  begin
    1.34  
    1.35 @@ -307,8 +300,6 @@
    1.36  context ring_1_no_zero_divisors
    1.37  begin
    1.38  
    1.39 -subclass semiring_1_no_zero_divisors ..
    1.40 -
    1.41  lemma power2_eq_1_iff:
    1.42    "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
    1.43    using square_eq_1_iff [of a] by (simp add: power2_eq_square)
    1.44 @@ -851,70 +842,6 @@
    1.45  qed
    1.46  
    1.47  
    1.48 -subsubsection \<open>Generalized sum over a set\<close>
    1.49 -
    1.50 -lemma setsum_zero_power [simp]:
    1.51 -  fixes c :: "nat \<Rightarrow> 'a::division_ring"
    1.52 -  shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
    1.53 -apply (cases "finite A")
    1.54 -  by (induction A rule: finite_induct) auto
    1.55 -
    1.56 -lemma setsum_zero_power' [simp]:
    1.57 -  fixes c :: "nat \<Rightarrow> 'a::field"
    1.58 -  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)"
    1.59 -  using setsum_zero_power [of "\<lambda>i. c i / d i" A]
    1.60 -  by auto
    1.61 -
    1.62 -
    1.63 -subsubsection \<open>Generalized product over a set\<close>
    1.64 -
    1.65 -lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
    1.66 -apply (erule finite_induct)
    1.67 -apply auto
    1.68 -done
    1.69 -
    1.70 -lemma setprod_power_distrib:
    1.71 -  fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
    1.72 -  shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A"
    1.73 -proof (cases "finite A")
    1.74 -  case True then show ?thesis
    1.75 -    by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
    1.76 -next
    1.77 -  case False then show ?thesis
    1.78 -    by simp
    1.79 -qed
    1.80 -
    1.81 -lemma power_setsum:
    1.82 -  "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
    1.83 -  by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
    1.84 -
    1.85 -lemma setprod_gen_delta:
    1.86 -  assumes fS: "finite S"
    1.87 -  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)"
    1.88 -proof-
    1.89 -  let ?f = "(\<lambda>k. if k=a then b k else c)"
    1.90 -  {assume a: "a \<notin> S"
    1.91 -    hence "\<forall> k\<in> S. ?f k = c" by simp
    1.92 -    hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
    1.93 -  moreover
    1.94 -  {assume a: "a \<in> S"
    1.95 -    let ?A = "S - {a}"
    1.96 -    let ?B = "{a}"
    1.97 -    have eq: "S = ?A \<union> ?B" using a by blast
    1.98 -    have dj: "?A \<inter> ?B = {}" by simp
    1.99 -    from fS have fAB: "finite ?A" "finite ?B" by auto
   1.100 -    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
   1.101 -      apply (rule setprod.cong) by auto
   1.102 -    have cA: "card ?A = card S - 1" using fS a by auto
   1.103 -    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
   1.104 -    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
   1.105 -      using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
   1.106 -      by simp
   1.107 -    then have ?thesis using a cA
   1.108 -      by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)}
   1.109 -  ultimately show ?thesis by blast
   1.110 -qed
   1.111 -
   1.112  subsection \<open>Code generator tweak\<close>
   1.113  
   1.114  code_identifier