author chaieb Sun Apr 05 19:21:51 2009 +0100 (2009-04-05) changeset 30869 71fde5b7b43c parent 30868 1040425c86a2 child 30872 0a667739d175
More precise treatement of rational constants by the normalizer for fields
```     1.1 --- a/src/HOL/Groebner_Basis.thy	Sun Apr 05 19:21:51 2009 +0100
1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Apr 05 19:21:51 2009 +0100
1.3 @@ -489,8 +489,7 @@
1.5  lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
1.7 -
1.8 -
1.9 +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*}
1.10  ML{*
1.11  local
1.12   val zr = @{cpat "0"}
1.13 @@ -616,6 +615,10 @@
1.14               @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
1.15               name = "ord_frac_simproc", proc = proc3, identifier = []}
1.16
1.17 +local
1.18 +open Conv
1.19 +in
1.20 +
1.21  val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
1.22             @{thm "divide_Numeral1"},
1.23             @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
1.24 @@ -624,11 +627,11 @@
1.25             @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
1.26             @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
1.27             @{thm "diff_def"}, @{thm "minus_divide_left"},
1.28 -           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym]
1.29 +           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
1.30 +           @{thm divide_inverse} RS sym, @{thm inverse_divide},
1.31 +           fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))
1.32 +           (@{thm divide_inverse} RS sym)]
1.33
1.34 -local
1.35 -open Conv
1.36 -in
1.37  val comp_conv = (Simplifier.rewrite