src/HOL/Power.thy
changeset 62481 b5d8e57826df
parent 62366 95c6cf433c91
child 63040 eb4ddd18d635
equal deleted inserted replaced
62480:f2e8984adef7 62481:b5d8e57826df
     4 *)
     4 *)
     5 
     5 
     6 section \<open>Exponentiation\<close>
     6 section \<open>Exponentiation\<close>
     7 
     7 
     8 theory Power
     8 theory Power
     9 imports Num Equiv_Relations
     9 imports Num
    10 begin
    10 begin
    11 
    11 
    12 subsection \<open>Powers for Arbitrary Monoids\<close>
    12 subsection \<open>Powers for Arbitrary Monoids\<close>
    13 
    13 
    14 class power = one + times
    14 class power = one + times
   230   then show "x dvd (x ^ n)" by simp
   230   then show "x dvd (x ^ n)" by simp
   231 qed
   231 qed
   232 
   232 
   233 end
   233 end
   234 
   234 
   235 class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
   235 context semiring_1_no_zero_divisors
   236 begin
   236 begin
   237 
   237 
   238 subclass power .
   238 subclass power .
   239 
   239 
   240 lemma power_eq_0_iff [simp]:
   240 lemma power_eq_0_iff [simp]:
   246   by (induct n) auto
   246   by (induct n) auto
   247 
   247 
   248 lemma zero_eq_power2 [simp]:
   248 lemma zero_eq_power2 [simp]:
   249   "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"
   249   "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"
   250   unfolding power2_eq_square by simp
   250   unfolding power2_eq_square by simp
   251 
       
   252 end
       
   253 
       
   254 context semidom
       
   255 begin
       
   256 
       
   257 subclass semiring_1_no_zero_divisors ..
       
   258 
   251 
   259 end
   252 end
   260 
   253 
   261 context ring_1
   254 context ring_1
   262 begin
   255 begin
   304 
   297 
   305 end
   298 end
   306 
   299 
   307 context ring_1_no_zero_divisors
   300 context ring_1_no_zero_divisors
   308 begin
   301 begin
   309 
       
   310 subclass semiring_1_no_zero_divisors ..
       
   311 
   302 
   312 lemma power2_eq_1_iff:
   303 lemma power2_eq_1_iff:
   313   "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
   304   "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
   314   using square_eq_1_iff [of a] by (simp add: power2_eq_square)
   305   using square_eq_1_iff [of a] by (simp add: power2_eq_square)
   315 
   306 
   849     apply (subst card_Un_disjoint, auto)
   840     apply (subst card_Un_disjoint, auto)
   850     done
   841     done
   851 qed
   842 qed
   852 
   843 
   853 
   844 
   854 subsubsection \<open>Generalized sum over a set\<close>
       
   855 
       
   856 lemma setsum_zero_power [simp]:
       
   857   fixes c :: "nat \<Rightarrow> 'a::division_ring"
       
   858   shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
       
   859 apply (cases "finite A")
       
   860   by (induction A rule: finite_induct) auto
       
   861 
       
   862 lemma setsum_zero_power' [simp]:
       
   863   fixes c :: "nat \<Rightarrow> 'a::field"
       
   864   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)"
       
   865   using setsum_zero_power [of "\<lambda>i. c i / d i" A]
       
   866   by auto
       
   867 
       
   868 
       
   869 subsubsection \<open>Generalized product over a set\<close>
       
   870 
       
   871 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
       
   872 apply (erule finite_induct)
       
   873 apply auto
       
   874 done
       
   875 
       
   876 lemma setprod_power_distrib:
       
   877   fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
       
   878   shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A"
       
   879 proof (cases "finite A")
       
   880   case True then show ?thesis
       
   881     by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
       
   882 next
       
   883   case False then show ?thesis
       
   884     by simp
       
   885 qed
       
   886 
       
   887 lemma power_setsum:
       
   888   "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
       
   889   by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
       
   890 
       
   891 lemma setprod_gen_delta:
       
   892   assumes fS: "finite S"
       
   893   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)"
       
   894 proof-
       
   895   let ?f = "(\<lambda>k. if k=a then b k else c)"
       
   896   {assume a: "a \<notin> S"
       
   897     hence "\<forall> k\<in> S. ?f k = c" by simp
       
   898     hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
       
   899   moreover
       
   900   {assume a: "a \<in> S"
       
   901     let ?A = "S - {a}"
       
   902     let ?B = "{a}"
       
   903     have eq: "S = ?A \<union> ?B" using a by blast
       
   904     have dj: "?A \<inter> ?B = {}" by simp
       
   905     from fS have fAB: "finite ?A" "finite ?B" by auto
       
   906     have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
       
   907       apply (rule setprod.cong) by auto
       
   908     have cA: "card ?A = card S - 1" using fS a by auto
       
   909     have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
       
   910     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
       
   911       using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
       
   912       by simp
       
   913     then have ?thesis using a cA
       
   914       by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)}
       
   915   ultimately show ?thesis by blast
       
   916 qed
       
   917 
       
   918 subsection \<open>Code generator tweak\<close>
   845 subsection \<open>Code generator tweak\<close>
   919 
   846 
   920 code_identifier
   847 code_identifier
   921   code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   848   code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   922 
   849