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.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.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")