--- 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")