src/HOL/Groebner_Basis.thy
changeset 30869 71fde5b7b43c
parent 30866 dd5117e2d73e
child 30925 c38cbc0ac8d1
     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.4    by (simp add: add_divide_distrib)
     1.5  lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
     1.6    by (simp add: add_divide_distrib)
     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
    1.38  (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
    1.39                addsimps ths addsimps simp_thms
    1.40 @@ -650,6 +653,8 @@
    1.41  fun dest_const ct = ((case term_of ct of
    1.42     Const (@{const_name "HOL.divide"},_) $ a $ b=>
    1.43      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
    1.44 + | Const (@{const_name "HOL.inverse"},_)$t => 
    1.45 +               Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
    1.46   | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
    1.47     handle TERM _ => error "ring_dest_const")
    1.48