--- 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 *}