src/HOL/Rational.thy

   shows "\<And>a b c d. b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b = Fract c d \<longleftrightarrow> a * d = c * b"
   and "\<And>a. Fract a 0 = Fract 0 1"
   and "\<And>a c. Fract 0 a = Fract 0 c"
   by (simp_all add: Fract_def)
 
-instantiation rat :: "{comm_ring_1, recpower}"
+instantiation rat :: comm_ring_1
 begin
 
 definition
   Zero_rat_def [code, code unfold]: "0 = Fract 0 1"
 

 next
   fix q r s :: rat show "(q + r) * s = q * s + r * s"
     by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps)
 next
   show "(0::rat) \<noteq> 1" by (simp add: Zero_rat_def One_rat_def eq_rat)
-next
-  fix q :: rat show "q * 1 = q"
-    by (cases q) (simp add: One_rat_def eq_rat)
 qed
 
 end
 
 lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"

   "(of_rat (a / b)::'a::{field_char_0,division_by_zero})
    = of_rat a / of_rat b"
 by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
 
 lemma of_rat_power:
-  "(of_rat (a ^ n)::'a::{field_char_0,recpower}) = of_rat a ^ n"
+  "(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n"
 by (induct n) (simp_all add: of_rat_mult)
 
 lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)"
 apply (induct a, induct b)
 apply (simp add: of_rat_rat eq_rat)

 apply (rule range_eqI)
 apply (rule of_rat_divide [symmetric])
 done
 
 lemma Rats_power [simp]:
-  fixes a :: "'a::{field_char_0,recpower}"
+  fixes a :: "'a::field_char_0"
   shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
 apply (rule of_rat_power [symmetric])
 done

 qed
 
 lemma Rats_induct [case_names of_rat, induct set: Rats]:
   "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
   by (rule Rats_cases) auto
+
+instance rat :: recpower ..
 
 
 subsection {* Implementation of rational numbers as pairs of integers *}
 
 lemma Fract_norm: "Fract (a div zgcd a b) (b div zgcd a b) = Fract a b"