diff -r d1b341c3aabc -r 673d7bc6b9db src/HOL/Library/Rational_Numbers.thy
--- a/src/HOL/Library/Rational_Numbers.thy	Tue Oct 23 22:56:55 2001 +0200
+++ b/src/HOL/Library/Rational_Numbers.thy	Tue Oct 23 22:57:52 2001 +0200
@@ -17,7 +17,7 @@
 
 typedef fraction = "{(a, b) :: int \<times> int | a b. b \<noteq> 0}"
 proof
-  show "(0, Numeral1) \<in> ?fraction" by simp
+  show "(0, 1) \<in> ?fraction" by simp
 qed
 
 constdefs
@@ -55,18 +55,10 @@
 defs (overloaded)
   equiv_fraction_def: "Q \<sim> R == num Q * den R = num R * den Q"
 
-lemma equiv_fraction_iff:
+lemma equiv_fraction_iff [iff]:
     "b \<noteq> 0 ==> b' \<noteq> 0 ==> (fract a b \<sim> fract a' b') = (a * b' = a' * b)"
   by (simp add: equiv_fraction_def)
 
-lemma equiv_fractionI [intro]:
-    "a * b' = a' * b ==> b \<noteq> 0 ==> b' \<noteq> 0 ==> fract a b \<sim> fract a' b'"
-  by (insert equiv_fraction_iff) blast
-
-lemma equiv_fractionD [dest]:
-    "fract a b \<sim> fract a' b' ==> b \<noteq> 0 ==> b' \<noteq> 0 ==> a * b' = a' * b"
-  by (insert equiv_fraction_iff) blast
-
 instance fraction :: equiv
 proof
   fix Q R S :: fraction
@@ -111,18 +103,10 @@
   }
 qed
 
-lemma eq_fraction_iff:
+lemma eq_fraction_iff [iff]:
     "b \<noteq> 0 ==> b' \<noteq> 0 ==> (\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor>) = (a * b' = a' * b)"
   by (simp add: equiv_fraction_iff quot_equality)
 
-lemma eq_fractionI [intro]:
-    "a * b' = a' * b ==> b \<noteq> 0 ==> b' \<noteq> 0 ==> \<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor>"
-  by (insert eq_fraction_iff) blast
-
-lemma eq_fractionD [dest]:
-    "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> b \<noteq> 0 ==> b' \<noteq> 0 ==> a * b' = a' * b"
-  by (insert eq_fraction_iff) blast
-
 
 subsubsection {* Operations on fractions *}
 
@@ -133,6 +117,7 @@
 *}
 
 instance fraction :: zero ..
+instance fraction :: one ..
 instance fraction :: plus ..
 instance fraction :: minus ..
 instance fraction :: times ..
@@ -140,7 +125,8 @@
 instance fraction :: ord ..
 
 defs (overloaded)
-  zero_fraction_def: "0 == fract 0 Numeral1"
+  zero_fraction_def: "0 == fract 0 1"
+  one_fraction_def: "1 == fract 1 1"
   add_fraction_def: "Q + R ==
     fract (num Q * den R + num R * den Q) (den Q * den R)"
   minus_fraction_def: "-Q == fract (-(num Q)) (den Q)"
@@ -368,6 +354,7 @@
 subsubsection {* Standard operations on rational numbers *}
 
 instance rat :: zero ..
+instance rat :: one ..
 instance rat :: plus ..
 instance rat :: minus ..
 instance rat :: times ..
@@ -377,6 +364,7 @@
 
 defs (overloaded)
   zero_rat_def: "0 == rat_of 0"
+  one_rat_def: "1 == rat_of 1"
   add_rat_def: "q + r == rat_of (fraction_of q + fraction_of r)"
   minus_rat_def: "-q == rat_of (-(fraction_of q))"
   diff_rat_def: "q - r == q + (-(r::rat))"
@@ -386,10 +374,13 @@
   le_rat_def: "q \<le> r == fraction_of q \<le> fraction_of r"
   less_rat_def: "q < r == q \<le> r \<and> q \<noteq> (r::rat)"
   abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)"
-  number_of_rat_def: "number_of b == Fract (number_of b) Numeral1"
+  number_of_rat_def: "number_of b == Fract (number_of b) 1"
 
-theorem zero_rat: "0 = Fract 0 Numeral1"
-  by (simp add: zero_rat_def zero_fraction_def rat_of_def Fract_def)
+theorem zero_rat: "0 = Fract 0 1"
+  by (simp add: zero_rat_def zero_fraction_def rat_of_def Fract_def)        
+
+theorem one_rat: "1 = Fract 1 1"
+  by (simp add: one_rat_def one_fraction_def rat_of_def Fract_def)
 
 theorem add_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
   Fract a b + Fract c d = Fract (a * d + c * b) (b * d)"
@@ -497,18 +488,16 @@
     by (induct q) (simp add: zero_rat minus_rat add_rat eq_rat)
   show "q - r = q + (-r)"
     by (induct q, induct r) (simp add: add_rat minus_rat diff_rat)
-  show "(0::rat) = Numeral0"
-    by (simp add: zero_rat number_of_rat_def)
   show "(q * r) * s = q * (r * s)"
     by (induct q, induct r, induct s) (simp add: mult_rat zmult_ac)
   show "q * r = r * q"
     by (induct q, induct r) (simp add: mult_rat zmult_ac)
-  show "Numeral1 * q = q"
-    by (induct q) (simp add: number_of_rat_def mult_rat)
+  show "1 * q = q"
+    by (induct q) (simp add: one_rat mult_rat)
   show "(q + r) * s = q * s + r * s"
     by (induct q, induct r, induct s) (simp add: add_rat mult_rat eq_rat int_distrib)
-  show "q \<noteq> 0 ==> inverse q * q = Numeral1"
-    by (induct q) (simp add: inverse_rat mult_rat number_of_rat_def zero_rat eq_rat)
+  show "q \<noteq> 0 ==> inverse q * q = 1"
+    by (induct q) (simp add: inverse_rat mult_rat one_rat zero_rat eq_rat)
   show "r \<noteq> 0 ==> q / r = q * inverse r"
     by (induct q, induct r) (simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat)
 qed
@@ -629,16 +618,16 @@
 subsection {* Embedding integers *}
 
 constdefs
-  rat :: "int => rat"    (* FIXME generalize int to any numeric subtype *)
-  "rat z == Fract z Numeral1"
-  int_set :: "rat set"    ("\<int>")    (* FIXME generalize rat to any numeric supertype *)
+  rat :: "int => rat"    (* FIXME generalize int to any numeric subtype (?) *)
+  "rat z == Fract z 1"
+  int_set :: "rat set"    ("\<int>")    (* FIXME generalize rat to any numeric supertype (?) *)
   "\<int> == range rat"
 
 lemma rat_inject: "(rat z = rat w) = (z = w)"
 proof
   assume "rat z = rat w"
-  hence "Fract z Numeral1 = Fract w Numeral1" by (unfold rat_def)
-  hence "\<lfloor>fract z Numeral1\<rfloor> = \<lfloor>fract w Numeral1\<rfloor>" ..
+  hence "Fract z 1 = Fract w 1" by (unfold rat_def)
+  hence "\<lfloor>fract z 1\<rfloor> = \<lfloor>fract w 1\<rfloor>" ..
   thus "z = w" by auto
 next
   assume "z = w"
@@ -657,6 +646,6 @@
   by (rule int_set_cases) auto
 
 theorem number_of_rat: "number_of b = rat (number_of b)"
-  by (simp only: number_of_rat_def rat_def)
+  by (simp add: number_of_rat_def rat_def)
 
 end