# HG changeset patch
# User chaieb
# Date 1182080365 -7200
# Node ID 8659acd81f9d0491a5ad8e4defd447fe18491569
# Parent  9e1edc15ef52e2353ddecdf1a9bdb54b3e2ccf7a
Tuned instantiation of Groebner bases to fields

diff -r 9e1edc15ef52 -r 8659acd81f9d src/HOL/NatSimprocs.thy
--- a/src/HOL/NatSimprocs.thy	Sun Jun 17 13:39:22 2007 +0200
+++ b/src/HOL/NatSimprocs.thy	Sun Jun 17 13:39:25 2007 +0200
@@ -561,20 +561,25 @@
            @{thm "diff_def"}, @{thm "minus_divide_left"}, 
            @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym]
 
-
-fun comp_conv ctxt = Simplifier.rewrite  
+local
+open Conv
+in
+fun comp_conv ctxt = (Simplifier.rewrite  
 (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} 
               addsimps ths addsimps comp_arith addsimps simp_thms
               addsimprocs field_cancel_numeral_factors
                addsimprocs [add_frac_frac_simproc ctxt, add_frac_num_simproc ctxt,
                             ord_frac_simproc]
-                addcongs [@{thm "if_weak_cong"}])
-
+                addcongs [@{thm "if_weak_cong"}]))
+then_conv (Simplifier.rewrite (HOL_basic_ss addsimps
+  [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}))
+end
 
 fun numeral_is_const ct = 
   case term_of ct of 
    Const (@{const_name "HOL.divide"},_) $ a $ b => 
-     can HOLogic.dest_number a andalso can HOLogic.dest_number b
+     numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct)
+ | Const (@{const_name "HOL.uminus"},_)$t => numeral_is_const (Thm.dest_arg ct)
  | t => can HOLogic.dest_number t
 
 fun dest_const ct = case term_of ct of