# HG changeset patch
# User nipkow
# Date 1401466420 -7200
# Node ID 653e56c6c963b096c294f90421a839dd8f77db0a
# Parent  161cf68af30053977d14e094c848b69385ae5c8b
must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure

diff -r 161cf68af300 -r 653e56c6c963 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri May 30 16:10:57 2014 +0200
+++ b/src/HOL/Rat.thy	Fri May 30 18:13:40 2014 +0200
@@ -629,7 +629,7 @@
       @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
       @{thm of_int_minus}, @{thm of_int_diff},
       @{thm of_int_of_nat_eq}]
-  #> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors
+  #> Lin_Arith.add_simprocs Numeral_Simprocs.field_divide_cancel_numeral_factor
   #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"})
   #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"}))
 *}
diff -r 161cf68af300 -r 653e56c6c963 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Fri May 30 16:10:57 2014 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Fri May 30 18:13:40 2014 +0200
@@ -37,7 +37,7 @@
   val div_cancel_numeral_factor: Proof.context -> cterm -> thm option
   val divide_cancel_numeral_factor: Proof.context -> cterm -> thm option
   val field_combine_numerals: Proof.context -> cterm -> thm option
-  val field_cancel_numeral_factors: simproc list
+  val field_divide_cancel_numeral_factor: simproc list
   val num_ss: simpset
   val field_comp_conv: Proof.context -> conv
 end;
@@ -446,20 +446,24 @@
 fun div_cancel_numeral_factor ctxt ct = DivCancelNumeralFactor.proc ctxt (term_of ct)
 fun divide_cancel_numeral_factor ctxt ct = DivideCancelNumeralFactor.proc ctxt (term_of ct)
 
-val field_cancel_numeral_factors =
-  map (prep_simproc @{theory})
-   [("field_eq_cancel_numeral_factor",
-     ["(l::'a::field) * m = n",
-      "(l::'a::field) = m * n"],
-     EqCancelNumeralFactor.proc),
-    ("field_cancel_numeral_factor",
+val field_divide_cancel_numeral_factor =
+  [prep_simproc @{theory}
+    ("field_divide_cancel_numeral_factor",
      ["((l::'a::field_inverse_zero) * m) / n",
       "(l::'a::field_inverse_zero) / (m * n)",
       "((numeral v)::'a::field_inverse_zero) / (numeral w)",
       "((numeral v)::'a::field_inverse_zero) / (- numeral w)",
       "((- numeral v)::'a::field_inverse_zero) / (numeral w)",
       "((- numeral v)::'a::field_inverse_zero) / (- numeral w)"],
-     DivideCancelNumeralFactor.proc)]
+     DivideCancelNumeralFactor.proc)];
+
+val field_cancel_numeral_factors =
+  prep_simproc @{theory}
+    ("field_eq_cancel_numeral_factor",
+     ["(l::'a::field) * m = n",
+      "(l::'a::field) = m * n"],
+     EqCancelNumeralFactor.proc)
+   :: field_divide_cancel_numeral_factor;
 
 
 (** Declarations for ExtractCommonTerm **)