src/HOL/Real/Rational.thy

 lemma [code]:
   "of_rat (Rational (k, l)) = (if l \<noteq> 0 then of_int k / of_int l else 0)"
   by (cases "l = 0")
     (auto simp add: Rational_simp of_rat_rat [simplified Fract_of_int_quotient [of k l], symmetric])
 
-instance rat :: eq ..
-
-lemma rat_eq_code [code]: "Rational x = Rational y \<longleftrightarrow> normNum x = normNum y"
-  unfolding Rational_def INum_normNum_iff ..
+instantiation rat :: eq
+begin
+
+definition [code func del]: "eq (r\<Colon>rat) s \<longleftrightarrow> r = s"
+
+instance by default (simp add: eq_rat_def)
+
+lemma rat_eq_code [code]: "eq (Rational x) (Rational y) \<longleftrightarrow> eq (normNum x) (normNum y)"
+  unfolding Rational_def INum_normNum_iff eq ..
+
+end
 
 lemma rat_less_eq_code [code]: "Rational x \<le> Rational y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
 proof -
   have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> Rational (normNum x) \<le> Rational (normNum y)" 
     by (simp add: Rational_def del: normNum)