# HG changeset patch
# User nipkow
# Date 1115196163 -7200
# Node ID 01d5d0c1c078f22cc3dc6c7e75910b9fdd68e11d
# Parent  7ef183f3fc9804772143cb9001a3a1c4069c6ac3
fixed lin.arith

diff -r 7ef183f3fc98 -r 01d5d0c1c078 src/HOL/Hyperreal/hypreal_arith.ML
--- a/src/HOL/Hyperreal/hypreal_arith.ML	Wed May 04 08:37:45 2005 +0200
+++ b/src/HOL/Hyperreal/hypreal_arith.ML	Wed May 04 10:42:43 2005 +0200
@@ -28,11 +28,12 @@
     Fast_Arith.lin_arith_prover;
 
 val hypreal_arith_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
+ [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = mult_mono_thms,
     inj_thms = inj_thms @ real_inj_thms, 
     lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*)
+    neqE = neqE,
     simpset = simpset}),
   arith_inj_const ("HyperDef.hypreal_of_real", HOLogic.realT --> hyprealT),
   Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]];
diff -r 7ef183f3fc98 -r 01d5d0c1c078 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Wed May 04 08:37:45 2005 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed May 04 10:42:43 2005 +0200
@@ -587,8 +587,7 @@
 done
 
 lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
-  by (force elim: order_less_asym
-            simp add: Ring_and_Field.mult_le_cancel_left)
+by(simp add:mult_commute)
 
 text{*Only two uses?*}
 lemma real_mult_less_mono':
diff -r 7ef183f3fc98 -r 01d5d0c1c078 src/HOL/Real/rat_arith.ML
--- a/src/HOL/Real/rat_arith.ML	Wed May 04 08:37:45 2005 +0200
+++ b/src/HOL/Real/rat_arith.ML	Wed May 04 10:42:43 2005 +0200
@@ -38,11 +38,13 @@
 val ratT = Type("Rational.rat", []);
 
 val rat_arith_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
+ [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD,
+ neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = mult_mono_thms,
     inj_thms = int_inj_thms @ inj_thms,
     lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the rats are dense!*)
+    neqE =  neqE,
     simpset = simpset addsimps simps
                       addsimprocs simprocs}),
   arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT),
diff -r 7ef183f3fc98 -r 01d5d0c1c078 src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Wed May 04 08:37:45 2005 +0200
+++ b/src/HOL/Real/real_arith.ML	Wed May 04 10:42:43 2005 +0200
@@ -118,11 +118,12 @@
   Fast_Arith.lin_arith_prover;
 
 val real_arith_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
+ [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = mult_mono_thms,
     inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
     lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the reals are dense!*)
+    neqE = neqE,
     simpset = simpset addsimps simps}),
   arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT),
   arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT),
diff -r 7ef183f3fc98 -r 01d5d0c1c078 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Wed May 04 08:37:45 2005 +0200
+++ b/src/HOL/Ring_and_Field.thy	Wed May 04 10:42:43 2005 +0200
@@ -245,6 +245,9 @@
 
 axclass ordered_field \<subseteq> field, ordered_idom
 
+lemmas linorder_neqE_ordered_idom =
+ linorder_neqE[where 'a = "?'b::ordered_idom"]
+
 lemma eq_add_iff1:
      "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"
 apply (simp add: diff_minus left_distrib)
diff -r 7ef183f3fc98 -r 01d5d0c1c078 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed May 04 08:37:45 2005 +0200
+++ b/src/HOL/arith_data.ML	Wed May 04 10:42:43 2005 +0200
@@ -423,7 +423,8 @@
     mult_mono_thms = mult_mono_thms,
     inj_thms = inj_thms,
     lessD = lessD @ [Suc_leI],
-    neqE = [linorder_neqE_nat],
+    neqE = [linorder_neqE_nat,
+      Goals.get_thm (theory "Ring_and_Field") "linorder_neqE_ordered_idom"],
     simpset = HOL_basic_ss addsimps add_rules
                    addsimprocs [ab_group_add_cancel.sum_conv, 
                                 ab_group_add_cancel.rel_conv]