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.11 -header{*Exponentiation*}
    1.12 +header {* Exponentiation *}
    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