--- 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
--- 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
--- 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 *)
--- 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) =