diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Quotient_Rat.thy
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -32,28 +32,29 @@
 begin
 
 quotient_definition
-  "0 \<Colon> rat" is "(0\<Colon>int, 1\<Colon>int)"
+  "0 \<Colon> rat" is "(0\<Colon>int, 1\<Colon>int)" by simp
 
 quotient_definition
-  "1 \<Colon> rat" is "(1\<Colon>int, 1\<Colon>int)"
+  "1 \<Colon> rat" is "(1\<Colon>int, 1\<Colon>int)" by simp
 
 fun times_rat_raw where
   "times_rat_raw (a :: int, b :: int) (c, d) = (a * c, b * d)"
 
 quotient_definition
-  "(op *) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw
+  "(op *) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult_assoc mult_left_commute)
 
 fun plus_rat_raw where
   "plus_rat_raw (a :: int, b :: int) (c, d) = (a * d + c * b, b * d)"
 
 quotient_definition
-  "(op +) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is plus_rat_raw
+  "(op +) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is plus_rat_raw 
+  by (auto simp add: mult_commute mult_left_commute int_distrib(2))
 
 fun uminus_rat_raw where
   "uminus_rat_raw (a :: int, b :: int) = (-a, b)"
 
 quotient_definition
-  "(uminus \<Colon> (rat \<Rightarrow> rat))" is "uminus_rat_raw"
+  "(uminus \<Colon> (rat \<Rightarrow> rat))" is "uminus_rat_raw" by fastforce
 
 definition
   minus_rat_def: "a - b = a + (-b\<Colon>rat)"
@@ -63,6 +64,32 @@
 
 quotient_definition
   "(op \<le>) :: rat \<Rightarrow> rat \<Rightarrow> bool" is "le_rat_raw"
+proof -
+  {
+    fix a b c d e f g h :: int
+    assume "a * f * (b * f) \<le> e * b * (b * f)"
+    then have le: "a * f * b * f \<le> e * b * b * f" by simp
+    assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" "h \<noteq> 0"
+    then have b2: "b * b > 0"
+      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
+    have f2: "f * f > 0" using nz(3)
+      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
+    assume eq: "a * d = c * b" "e * h = g * f"
+    have "a * f * b * f * d * d \<le> e * b * b * f * d * d" using le nz(2)
+      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
+    then have "c * f * f * d * (b * b) \<le> e * f * d * d * (b * b)" using eq
+      by (metis (no_types) mult_assoc mult_commute)
+    then have "c * f * f * d \<le> e * f * d * d" using b2
+      by (metis leD linorder_le_less_linear mult_strict_right_mono)
+    then have "c * f * f * d * h * h \<le> e * f * d * d * h * h" using nz(4)
+      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
+    then have "c * h * (d * h) * (f * f) \<le> g * d * (d * h) * (f * f)" using eq
+      by (metis (no_types) mult_assoc mult_commute)
+    then have "c * h * (d * h) \<le> g * d * (d * h)" using f2
+      by (metis leD linorder_le_less_linear mult_strict_right_mono)
+  }
+  then show "\<And>x y xa ya. x \<approx> y \<Longrightarrow> xa \<approx> ya \<Longrightarrow> le_rat_raw x xa = le_rat_raw y ya" by auto
+qed
 
 definition
   less_rat_def: "(z\<Colon>rat) < w = (z \<le> w \<and> z \<noteq> w)"
@@ -83,14 +110,7 @@
 where [simp]: "Fract_raw a b = (if b = 0 then (0, 1) else (a, b))"
 
 quotient_definition "Fract :: int \<Rightarrow> int \<Rightarrow> rat" is
-  Fract_raw
-
-lemma [quot_respect]:
-  "(op \<approx> ===> op \<approx> ===> op \<approx>) times_rat_raw times_rat_raw"
-  "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_rat_raw plus_rat_raw"
-  "(op \<approx> ===> op \<approx>) uminus_rat_raw uminus_rat_raw"
-  "(op = ===> op = ===> op \<approx>) Fract_raw Fract_raw"
-  by (auto intro!: fun_relI simp add: mult_assoc mult_commute mult_left_commute int_distrib(2))
+  Fract_raw by simp
 
 lemmas [simp] = Respects_def
 
@@ -156,15 +176,11 @@
   "rat_inverse_raw (a :: int, b :: int) = (if a = 0 then (0, 1) else (b, a))"
 
 quotient_definition
-  "inverse :: rat \<Rightarrow> rat" is rat_inverse_raw
+  "inverse :: rat \<Rightarrow> rat" is rat_inverse_raw by (force simp add: mult_commute)
 
 definition
   divide_rat_def: "q / r = q * inverse (r::rat)"
 
-lemma [quot_respect]:
-  "(op \<approx> ===> op \<approx>) rat_inverse_raw rat_inverse_raw"
-  by (auto intro!: fun_relI simp add: mult_commute)
-
 instance proof
   fix q :: rat
   assume "q \<noteq> 0"
@@ -179,34 +195,6 @@
 
 end
 
-lemma [quot_respect]: "(op \<approx> ===> op \<approx> ===> op =) le_rat_raw le_rat_raw"
-proof -
-  {
-    fix a b c d e f g h :: int
-    assume "a * f * (b * f) \<le> e * b * (b * f)"
-    then have le: "a * f * b * f \<le> e * b * b * f" by simp
-    assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" "h \<noteq> 0"
-    then have b2: "b * b > 0"
-      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
-    have f2: "f * f > 0" using nz(3)
-      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
-    assume eq: "a * d = c * b" "e * h = g * f"
-    have "a * f * b * f * d * d \<le> e * b * b * f * d * d" using le nz(2)
-      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
-    then have "c * f * f * d * (b * b) \<le> e * f * d * d * (b * b)" using eq
-      by (metis (no_types) mult_assoc mult_commute)
-    then have "c * f * f * d \<le> e * f * d * d" using b2
-      by (metis leD linorder_le_less_linear mult_strict_right_mono)
-    then have "c * f * f * d * h * h \<le> e * f * d * d * h * h" using nz(4)
-      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
-    then have "c * h * (d * h) * (f * f) \<le> g * d * (d * h) * (f * f)" using eq
-      by (metis (no_types) mult_assoc mult_commute)
-    then have "c * h * (d * h) \<le> g * d * (d * h)" using f2
-      by (metis leD linorder_le_less_linear mult_strict_right_mono)
-  }
-  then show ?thesis by (auto intro!: fun_relI)
-qed
-
 instantiation rat :: linorder
 begin