# HG changeset patch
# User chaieb
# Date 1238955711 -3600
# Node ID 71fde5b7b43c421bd38cd081152865750f693653
# Parent  1040425c86a22a16f4e34015ece8992fb7fd4073
More precise treatement of rational constants by the normalizer for fields

diff -r 1040425c86a2 -r 71fde5b7b43c src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sun Apr 05 19:21:51 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy	Sun Apr 05 19:21:51 2009 +0100
@@ -489,8 +489,7 @@
   by (simp add: add_divide_distrib)
 lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
   by (simp add: add_divide_distrib)
-
-
+ML{* let open Conv in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))   (@{thm divide_inverse} RS sym)end*}
 ML{* 
 local
  val zr = @{cpat "0"}
@@ -616,6 +615,10 @@
              @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
              name = "ord_frac_simproc", proc = proc3, identifier = []}
 
+local
+open Conv
+in
+
 val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
            @{thm "divide_Numeral1"},
            @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
@@ -624,11 +627,11 @@
            @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
            @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
            @{thm "diff_def"}, @{thm "minus_divide_left"},
-           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym]
+           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
+           @{thm divide_inverse} RS sym, @{thm inverse_divide}, 
+           fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))   
+           (@{thm divide_inverse} RS sym)]
 
-local
-open Conv
-in
 val comp_conv = (Simplifier.rewrite
 (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
               addsimps ths addsimps simp_thms
@@ -650,6 +653,8 @@
 fun dest_const ct = ((case term_of ct of
    Const (@{const_name "HOL.divide"},_) $ a $ b=>
     Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
+ | Const (@{const_name "HOL.inverse"},_)$t => 
+               Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
  | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
    handle TERM _ => error "ring_dest_const")