# HG changeset patch
# User huffman
# Date 1158100718 -7200
# Node ID 05072ae0d4351678d539ebd0c37c28727671b94e
# Parent  189811b398695e85b679f0fc29453ac97db141e1
added instance rat :: recpower

diff -r 189811b39869 -r 05072ae0d435 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Tue Sep 12 21:05:39 2006 +0200
+++ b/src/HOL/Real/Rational.thy	Wed Sep 13 00:38:38 2006 +0200
@@ -158,7 +158,7 @@
 
 subsubsection {* Standard operations on rational numbers *}
 
-instance rat :: "{ord, zero, one, plus, times, minus, inverse}" ..
+instance rat :: "{ord, zero, one, plus, times, minus, inverse, power}" ..
 
 defs (overloaded)
   Zero_rat_def:  "0 == Fract 0 1"
@@ -194,6 +194,10 @@
 
   abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)"
 
+primrec (rat)
+  rat_power_0:   "q ^ 0       = 1"
+  rat_power_Suc: "q ^ (Suc n) = (q::rat) * (q ^ n)"
+
 lemma zero_rat: "0 = Fract 0 1"
 by (simp add: Zero_rat_def)
 
@@ -394,6 +398,14 @@
                   inverse_congruent UN_ratrel)
 qed
 
+instance rat :: recpower
+proof
+  fix q :: rat
+  fix n :: nat
+  show "q ^ 0 = 1" by simp
+  show "q ^ (Suc n) = q * (q ^ n)" by simp
+qed
+
 
 subsection {* Various Other Results *}