# HG changeset patch
# User huffman
# Date 1181521479 -7200
# Node ID 8ae6f7b0903b4ed96b5c1b6844ed504594cc3937
# Parent  83f3b6dc58b543cc58a3091812b6054f208bf607
add lemma of_nat_power

diff -r 83f3b6dc58b5 -r 8ae6f7b0903b src/HOL/Power.thy
--- a/src/HOL/Power.thy	Mon Jun 11 01:22:29 2007 +0200
+++ b/src/HOL/Power.thy	Mon Jun 11 02:24:39 2007 +0200
@@ -331,6 +331,10 @@
   show "z^(Suc n) = z * (z^n)" by simp
 qed
 
+lemma of_nat_power:
+  "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
+by (induct n, simp_all add: power_Suc)
+
 lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
 by (insert one_le_power [of i n], simp)