src/HOL/Power.thy
changeset 23183 af27d3ad9baf
parent 22991 b9e2a133e84e
child 23305 8ae6f7b0903b
     1.1 --- a/src/HOL/Power.thy	Fri Jun 01 10:44:28 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Fri Jun 01 10:44:30 2007 +0200
     1.3 @@ -18,37 +18,29 @@
     1.4    assumes power_Suc:      "a \<^loc>^ Suc n = a \<^loc>* (a \<^loc>^ n)"
     1.5  
     1.6  lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
     1.7 -by (simp add: power_Suc)
     1.8 +  by (simp add: power_Suc)
     1.9  
    1.10  text{*It looks plausible as a simprule, but its effect can be strange.*}
    1.11  lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::{recpower,semiring_0}))"
    1.12 -by (induct "n", auto)
    1.13 +  by (induct n) simp_all
    1.14  
    1.15  lemma power_one [simp]: "1^n = (1::'a::recpower)"
    1.16 -apply (induct "n")
    1.17 -apply (auto simp add: power_Suc)
    1.18 -done
    1.19 +  by (induct n) (simp_all add: power_Suc)
    1.20  
    1.21  lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
    1.22 -by (simp add: power_Suc)
    1.23 +  by (simp add: power_Suc)
    1.24  
    1.25  lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
    1.26 -by (induct "n") (simp_all add:power_Suc mult_assoc)
    1.27 +  by (induct n) (simp_all add: power_Suc mult_assoc)
    1.28  
    1.29  lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)"
    1.30 -apply (induct "m")
    1.31 -apply (simp_all add: power_Suc mult_ac)
    1.32 -done
    1.33 +  by (induct m) (simp_all add: power_Suc mult_ac)
    1.34  
    1.35  lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n"
    1.36 -apply (induct "n") 
    1.37 -apply (simp_all add: power_Suc power_add)
    1.38 -done
    1.39 +  by (induct n) (simp_all add: power_Suc power_add)
    1.40  
    1.41  lemma power_mult_distrib: "((a::'a::{recpower,comm_monoid_mult}) * b) ^ n = (a^n) * (b^n)"
    1.42 -apply (induct "n")
    1.43 -apply (auto simp add: power_Suc mult_ac)
    1.44 -done
    1.45 +  by (induct n) (simp_all add: power_Suc mult_ac)
    1.46  
    1.47  lemma zero_less_power:
    1.48       "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n"