src/HOL/Power.thy
 changeset 30960 fec1a04b7220 parent 30730 4d3565f2cb0e child 30996 648d02b124d8
```     1.1 --- a/src/HOL/Power.thy	Wed Apr 22 19:09:19 2009 +0200
1.2 +++ b/src/HOL/Power.thy	Wed Apr 22 19:09:21 2009 +0200
1.3 @@ -1,24 +1,24 @@
1.4  (*  Title:      HOL/Power.thy
1.5 -    ID:         \$Id\$
1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7      Copyright   1997  University of Cambridge
1.8 -
1.9  *)
1.10
1.13
1.14  theory Power
1.15  imports Nat
1.16  begin
1.17
1.18 -class power =
1.19 -  fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "^" 80)
1.20 +subsection {* Powers for Arbitrary Monoids *}
1.21 +
1.22 +class recpower = monoid_mult
1.23 +begin
1.24
1.25 -subsection{*Powers for Arbitrary Monoids*}
1.26 +primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) where
1.27 +    power_0: "a ^ 0 = 1"
1.28 +  | power_Suc: "a ^ Suc n = a * a ^ n"
1.29
1.30 -class recpower = monoid_mult + power +
1.31 -  assumes power_0 [simp]: "a ^ 0       = 1"
1.32 -  assumes power_Suc [simp]: "a ^ Suc n = a * (a ^ n)"
1.33 +end
1.34
1.35  lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
1.36    by simp
1.37 @@ -360,24 +360,9 @@
1.38  done
1.39
1.40
1.41 -subsection{*Exponentiation for the Natural Numbers*}
1.42 -
1.43 -instantiation nat :: recpower
1.44 -begin
1.45 -
1.46 -primrec power_nat where
1.47 -  "p ^ 0 = (1\<Colon>nat)"
1.48 -  | "p ^ (Suc n) = (p\<Colon>nat) * (p ^ n)"
1.49 +subsection {* Exponentiation for the Natural Numbers *}
1.50
1.51 -instance proof
1.52 -  fix z n :: nat
1.53 -  show "z^0 = 1" by simp
1.54 -  show "z^(Suc n) = z * (z^n)" by simp
1.55 -qed
1.56 -
1.57 -declare power_nat.simps [simp del]
1.58 -
1.59 -end
1.60 +instance nat :: recpower ..
1.61
1.62  lemma of_nat_power:
1.63    "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
1.64 @@ -391,7 +376,7 @@
1.65
1.66  lemma nat_power_eq_Suc_0_iff [simp]:
1.67    "((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)"
1.68 -by (induct_tac m, auto)
1.69 +by (induct m, auto)
1.70
1.71  lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0"
1.72  by simp
```