# HG changeset patch
# User paulson
# Date 1072187168 -3600
# Node ID 55c688d2eefaf96806d08158a645eb8c3bc1d361
# Parent  fb7a114826be4ffc612b3755b1a8604d85ce05ad
new theorems

diff -r fb7a114826be -r 55c688d2eefa src/HOL/Real/RealArith.thy
--- a/src/HOL/Real/RealArith.thy	Tue Dec 23 14:45:47 2003 +0100
+++ b/src/HOL/Real/RealArith.thy	Tue Dec 23 14:46:08 2003 +0100
@@ -47,7 +47,7 @@
 Addsimps [symmetric real_diff_def]
 *)
 
-subsubsection{*Division By @{term 1} and @{term "-1"}*}
+subsubsection{*Division By @{term "-1"}*}
 
 lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)"
 by simp
diff -r fb7a114826be -r 55c688d2eefa src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Tue Dec 23 14:45:47 2003 +0100
+++ b/src/HOL/Real/real_arith.ML	Tue Dec 23 14:46:08 2003 +0100
@@ -7,26 +7,6 @@
 *)
 
 
-(** Misc ML bindings **)
-
-val inverse_less_iff_less = thm"Ring_and_Field.inverse_less_iff_less";
-val add_right_mono = thm"Ring_and_Field.add_right_mono";
-val times_divide_eq_left = thm "times_divide_eq_left";
-val times_divide_eq_right = thm "times_divide_eq_right";
-val inverse_mult_distrib = thm "inverse_mult_distrib";
-val minus_minus = thm "minus_minus";
-val left_inverse = thm "left_inverse";
-val right_inverse = thm "right_inverse";
-val inverse_minus_eq = thm "inverse_minus_eq";
-val minus_mult_left = thm "minus_mult_left";
-val minus_mult_right = thm "minus_mult_right";
-
-val pos_real_less_divide_eq = thm"pos_less_divide_eq";
-val pos_real_divide_less_eq = thm"pos_divide_less_eq";
-val pos_real_le_divide_eq = thm"pos_le_divide_eq";
-val pos_real_divide_le_eq = thm"pos_divide_le_eq";
-
-
 (****Common factor cancellation****)
 
 (*To quote from Provers/Arith/cancel_numeral_factor.ML:
@@ -39,19 +19,6 @@
 and d = gcd(m,m') and n=m/d and n'=m'/d.
 *)
 
-val inverse_eq_divide = thm"Ring_and_Field.inverse_eq_divide";
-
-val mult_less_cancel_left = thm"Ring_and_Field.mult_less_cancel_left";
-val mult_le_cancel_left = thm"Ring_and_Field.mult_le_cancel_left";
-val mult_less_cancel_right = thm"Ring_and_Field.mult_less_cancel_right";
-val mult_le_cancel_right = thm"Ring_and_Field.mult_le_cancel_right";
-val mult_cancel_left = thm"Ring_and_Field.mult_cancel_left";
-val mult_cancel_right = thm"Ring_and_Field.mult_cancel_right";
-
-val mult_divide_cancel_left = thm"Ring_and_Field.mult_divide_cancel_left";
-val mult_divide_cancel_eq_if = thm"Ring_and_Field.mult_divide_cancel_eq_if";
-
-
 local
   open Real_Numeral_Simprocs
 in
diff -r fb7a114826be -r 55c688d2eefa src/HOL/Real/real_arith0.ML
--- a/src/HOL/Real/real_arith0.ML	Tue Dec 23 14:45:47 2003 +0100
+++ b/src/HOL/Real/real_arith0.ML	Tue Dec 23 14:46:08 2003 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Real/real_arith.ML
+(*  Title:      HOL/Real/real_arith0.ML
     ID:         $Id$
     Author:     Tobias Nipkow, TU Muenchen
     Copyright   1999 TU Muenchen
@@ -6,6 +6,45 @@
 Instantiation of the generic linear arithmetic package for type real.
 *)
 
+(** Misc ML bindings **)
+(*FIXME: move to Integ or earlier*)
+
+val left_inverse = thm "left_inverse";
+val right_inverse = thm "right_inverse";
+val inverse_less_iff_less = thm"Ring_and_Field.inverse_less_iff_less";
+val inverse_eq_divide = thm"Ring_and_Field.inverse_eq_divide";
+val inverse_minus_eq = thm "inverse_minus_eq";
+val inverse_mult_distrib = thm "inverse_mult_distrib";
+val inverse_add = thm "inverse_add";
+
+val add_right_mono = thm"Ring_and_Field.add_right_mono";
+val times_divide_eq_left = thm "times_divide_eq_left";
+val times_divide_eq_right = thm "times_divide_eq_right";
+val minus_minus = thm "minus_minus";
+val minus_mult_left = thm "minus_mult_left";
+val minus_mult_right = thm "minus_mult_right";
+
+val pos_real_less_divide_eq = thm"pos_less_divide_eq";
+val pos_real_divide_less_eq = thm"pos_divide_less_eq";
+val pos_real_le_divide_eq = thm"pos_le_divide_eq";
+val pos_real_divide_le_eq = thm"pos_divide_le_eq";
+
+val mult_less_cancel_left = thm"Ring_and_Field.mult_less_cancel_left";
+val mult_le_cancel_left = thm"Ring_and_Field.mult_le_cancel_left";
+val mult_less_cancel_right = thm"Ring_and_Field.mult_less_cancel_right";
+val mult_le_cancel_right = thm"Ring_and_Field.mult_le_cancel_right";
+val mult_cancel_left = thm"Ring_and_Field.mult_cancel_left";
+val mult_cancel_right = thm"Ring_and_Field.mult_cancel_right";
+
+val field_mult_cancel_left = thm "field_mult_cancel_left";
+val field_mult_cancel_right = thm "field_mult_cancel_right";
+
+val mult_divide_cancel_left = thm"Ring_and_Field.mult_divide_cancel_left";
+val mult_divide_cancel_right = thm "Ring_and_Field.mult_divide_cancel_right";
+val mult_divide_cancel_eq_if = thm"Ring_and_Field.mult_divide_cancel_eq_if";
+
+
+
 local
 
 (* reduce contradictory <= to False *)
diff -r fb7a114826be -r 55c688d2eefa src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Dec 23 14:45:47 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy	Tue Dec 23 14:46:08 2003 +0100
@@ -882,6 +882,16 @@
 apply (simp_all add: nonzero_mult_divide_cancel_left)
 done
 
+lemma nonzero_mult_divide_cancel_right:
+     "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
+by (simp add: mult_commute [of _ c] nonzero_mult_divide_cancel_left) 
+
+lemma mult_divide_cancel_right:
+     "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
+apply (case_tac "b = 0")
+apply (simp_all add: nonzero_mult_divide_cancel_right)
+done
+
 (*For ExtractCommonTerm*)
 lemma mult_divide_cancel_eq_if:
      "(c*a) / (c*b) =