1.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Fri Apr 03 18:03:29 2009 +0200
     1.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Sun Apr 05 05:07:10 2009 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4   val semiring_normalize_ord_wrapper :  Proof.context -> NormalizerData.entry ->
     1.5     (cterm -> cterm -> bool) -> conv
     1.6   val semiring_normalizers_conv :
     1.7 -     cterm list -> cterm list * thm list -> cterm list * thm list ->
     1.8 +     cterm list -> cterm list * thm list -> cterm list * thm list -> cterm list * thm list ->
     1.9       (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
    1.10         {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    1.11  end
    1.12 @@ -71,7 +71,7 @@
    1.13  
    1.14  
    1.15  (* The main function! *)
    1.16 -fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules)
    1.17 +fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
    1.18    (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
    1.19  let
    1.20  
    1.21 @@ -97,8 +97,7 @@
    1.22  
    1.23  val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
    1.24    (case (r_ops, r_rules) of
    1.25 -    ([], []) => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)
    1.26 -  | ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
    1.27 +    ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
    1.28        let
    1.29          val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
    1.30          val neg_tm = Thm.dest_fun neg_pat
    1.31 @@ -106,7 +105,18 @@
    1.32          val is_sub = is_binop sub_tm
    1.33        in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
    1.34            sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
    1.35 -      end);
    1.36 +      end
    1.37 +    | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm));
    1.38 +
    1.39 +val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = 
    1.40 +  (case (f_ops, f_rules) of 
    1.41 +   ([divide_pat, inverse_pat], [div_inv, inv_div]) => 
    1.42 +     let val div_tm = funpow 2 Thm.dest_fun divide_pat
    1.43 +         val inv_tm = Thm.dest_fun inverse_pat
    1.44 +     in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm)
    1.45 +     end
    1.46 +   | _ => (TrueI, TrueI, true_tm, true_tm, K false));
    1.47 +
    1.48  in fn variable_order =>
    1.49   let
    1.50  
    1.51 @@ -579,6 +589,10 @@
    1.52         let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
    1.53         in transitive th1 (polynomial_neg_conv (concl th1))
    1.54         end
    1.55 +     else if lopr aconvc inverse_tm then
    1.56 +       let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
    1.57 +       in transitive th1 (semiring_mul_conv (concl th1))
    1.58 +       end
    1.59       else
    1.60         if not(is_comb lopr) then reflexive tm
    1.61         else
    1.62 @@ -588,6 +602,14 @@
    1.63                let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
    1.64                in transitive th1 (polynomial_pow_conv (concl th1))
    1.65                end
    1.66 +         else if opr aconvc divide_tm 
    1.67 +            then
    1.68 +              let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
    1.69 +                                        (polynomial_conv r)
    1.70 +                  val th2 = (rewr_conv divide_inverse then_conv polynomial_mul_conv) 
    1.71 +                              (Thm.rhs_of th1)
    1.72 +              in transitive th1 th2
    1.73 +              end
    1.74              else
    1.75                if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
    1.76                then
    1.77 @@ -616,7 +638,7 @@
    1.78  
    1.79  fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
    1.80  
    1.81 -fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, 
    1.82 +fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, 
    1.83                                       {conv, dest_const, mk_const, is_const}) ord =
    1.84    let
    1.85      val pow_conv =
    1.86 @@ -625,10 +647,10 @@
    1.87          (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
    1.88        then_conv conv ctxt
    1.89      val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
    1.90 -  in semiring_normalizers_conv vars semiring ring dat ord end;
    1.91 +  in semiring_normalizers_conv vars semiring ring field dat ord end;
    1.92  
    1.93 -fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
    1.94 - #main (semiring_normalizers_ord_wrapper ctxt ({vars = vars, semiring = semiring, ring = ring, idom = idom, ideal = ideal},{conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord);
    1.95 +fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
    1.96 + #main (semiring_normalizers_ord_wrapper ctxt ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal},{conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord);
    1.97  
    1.98  fun semiring_normalize_wrapper ctxt data = 
    1.99    semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;