author chaieb Sun Apr 05 05:07:10 2009 +0100 (2009-04-05) changeset 30866 dd5117e2d73e parent 30865 5106e13d400f child 30867 6fff6030338b
now deals with devision in fields
```     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Apr 03 18:03:29 2009 +0200
1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Apr 05 05:07:10 2009 +0100
1.3 @@ -191,8 +191,7 @@
1.4
1.5  open Conv;
1.6
1.7 -fun numeral_is_const ct =
1.8 -  can HOLogic.dest_number (Thm.term_of ct);
1.9 +fun numeral_is_const ct = can HOLogic.dest_number (Thm.term_of ct);
1.10
1.11  fun int_of_rat x =
1.12    (case Rat.quotient_of_rat x of (i, 1) => i
1.13 @@ -260,16 +259,22 @@
1.14  locale gb_field = gb_ring +
1.15    fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.16      and inverse:: "'a \<Rightarrow> 'a"
1.17 -  assumes divide: "divide x y = mul x (inverse y)"
1.18 -     and inverse: "inverse x = divide r1 x"
1.19 +  assumes divide_inverse: "divide x y = mul x (inverse y)"
1.20 +     and inverse_divide: "inverse x = divide r1 x"
1.21  begin
1.22
1.23 +lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" .
1.24 +
1.25 +lemmas field_rules = divide_inverse inverse_divide
1.26 +
1.27  lemmas gb_field_axioms' =
1.28    gb_field_axioms [normalizer
1.29      semiring ops: semiring_ops
1.30      semiring rules: semiring_rules
1.31      ring ops: ring_ops
1.32 -    ring rules: ring_rules]
1.33 +    ring rules: ring_rules
1.34 +    field ops: field_ops
1.35 +    field rules: field_rules]
1.36
1.37  end
1.38
1.39 @@ -393,6 +398,8 @@
1.40    semiring rules: semiring_rules
1.41    ring ops: ring_ops
1.42    ring rules: ring_rules
1.43 +  field ops: field_ops
1.44 +  field rules: field_rules
1.47
1.48 @@ -636,8 +643,8 @@
1.49  fun numeral_is_const ct =
1.50    case term_of ct of
1.51     Const (@{const_name "HOL.divide"},_) \$ a \$ b =>
1.52 -     numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct)
1.53 - | Const (@{const_name "HOL.uminus"},_)\$t => numeral_is_const (Thm.dest_arg ct)
1.54 +     can HOLogic.dest_number a andalso can HOLogic.dest_number b
1.55 + | Const (@{const_name "HOL.inverse"},_)\$t => can HOLogic.dest_number t
1.56   | t => can HOLogic.dest_number t
1.57
1.58  fun dest_const ct = ((case term_of ct of
```
```     2.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Fri Apr 03 18:03:29 2009 +0200
2.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Sun Apr 05 05:07:10 2009 +0100
2.3 @@ -5,8 +5,8 @@
2.4  signature GROEBNER =
2.5  sig
2.6    val ring_and_ideal_conv :
2.7 -    {idom: thm list, ring: cterm list * thm list, vars: cterm list,
2.8 -     semiring: cterm list * thm list, ideal : thm list} ->
2.9 +    {idom: thm list, ring: cterm list * thm list, field: cterm list * thm list,
2.10 +     vars: cterm list, semiring: cterm list * thm list, ideal : thm list} ->
2.11      (cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
2.12      conv ->  conv ->
2.13   {ring_conv : conv,
2.14 @@ -581,7 +581,8 @@
2.15  (** main **)
2.16
2.17  fun ring_and_ideal_conv
2.18 -  {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom, ideal}
2.19 +  {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
2.20 +   field = (f_ops, f_rules), idom, ideal}
2.21    dest_const mk_const ring_eq_conv ring_normalize_conv =
2.22  let
2.23    val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
2.24 @@ -590,32 +591,37 @@
2.25
2.26    val (ring_sub_tm, ring_neg_tm) =
2.27      (case r_ops of
2.28 -      [] => (@{cterm "True"}, @{cterm "True"})
2.29 -    | [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat));
2.30 +     [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat)
2.31 +    |_  => (@{cterm "True"}, @{cterm "True"}));
2.32 +
2.33 +  val (field_div_tm, field_inv_tm) =
2.34 +    (case f_ops of
2.35 +       [div_pat, inv_pat] => (dest_fun2 div_pat, dest_fun inv_pat)
2.36 +     | _ => (@{cterm "True"}, @{cterm "True"}));
2.37
2.38    val [idom_thm, neq_thm] = idom;
2.40       if length ideal = 2 then ideal else [eq_commute, eq_commute]
2.41 -  val ring_dest_neg =
2.42 -    fn t => let val (l,r) = dest_comb t in
2.43 -        if Term.could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t])
2.44 -      end
2.45 +  fun ring_dest_neg t =
2.46 +    let val (l,r) = dest_comb t
2.47 +    in if Term.could_unify(term_of l,term_of ring_neg_tm) then r
2.48 +       else raise CTERM ("ring_dest_neg", [t])
2.49 +    end
2.50
2.51   val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
2.52 -(*
2.53 - fun ring_dest_inv t =
2.54 + fun field_dest_inv t =
2.55      let val (l,r) = dest_comb t in
2.56 -        if Term.could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv"
2.57 +        if Term.could_unify(term_of l, term_of field_inv_tm) then r
2.58 +        else raise CTERM ("field_dest_inv", [t])
2.59      end
2.60 -*)
2.63   val ring_dest_sub = dest_binary ring_sub_tm;
2.64   val ring_mk_sub = mk_binop ring_sub_tm;
2.65   val ring_dest_mul = dest_binary ring_mul_tm;
2.66   val ring_mk_mul = mk_binop ring_mul_tm;
2.67 -(* val ring_dest_div = dest_binary ring_div_tm;
2.68 - val ring_mk_div = mk_binop ring_div_tm;*)
2.69 + val field_dest_div = dest_binary field_div_tm;
2.70 + val field_mk_div = mk_binop field_div_tm;
2.71   val ring_dest_pow = dest_binary ring_pow_tm;
2.72   val ring_mk_pow = mk_binop ring_pow_tm ;
2.73   fun grobvars tm acc =
2.74 @@ -625,16 +631,16 @@
2.75      else if can ring_dest_add tm orelse can ring_dest_sub tm
2.76              orelse can ring_dest_mul tm
2.77      then grobvars (dest_arg1 tm) (grobvars (dest_arg tm) acc)
2.78 -(*    else if can ring_dest_inv tm
2.79 -       then
2.80 -             let val gvs = grobvars (dest_arg tm) [] in
2.81 -             if gvs = [] then acc else tm::acc
2.82 -             end
2.83 -    else if can ring_dest_div tm then
2.84 -              let val lvs = grobvars (dest_arg1 tm) acc
2.85 -                val gvs = grobvars (dest_arg tm) []
2.86 -              in if gvs = [] then lvs else tm::acc
2.87 -             end *)
2.88 +    else if can field_dest_inv tm
2.89 +         then
2.90 +          let val gvs = grobvars (dest_arg tm) []
2.91 +          in if null gvs then acc else tm::acc
2.92 +          end
2.93 +    else if can field_dest_div tm then
2.94 +         let val lvs = grobvars (dest_arg1 tm) acc
2.95 +             val gvs = grobvars (dest_arg tm) []
2.96 +          in if null gvs then lvs else tm::acc
2.97 +          end
2.98      else tm::acc ;
2.99
2.100  fun grobify_term vars tm =
2.101 @@ -648,8 +654,8 @@
2.102    ((grob_neg(grobify_term vars (ring_dest_neg tm)))
2.103    handle CTERM _ =>
2.104     (
2.105 -(*   (grob_inv(grobify_term vars (ring_dest_inv tm)))
2.106 -   handle CTERM _ => *)
2.107 +   (grob_inv(grobify_term vars (field_dest_inv tm)))
2.108 +   handle CTERM _ =>
2.109      ((let val (l,r) = ring_dest_add tm
2.110      in grob_add (grobify_term vars l) (grobify_term vars r)
2.111      end)
2.112 @@ -662,18 +668,15 @@
2.113        in grob_mul (grobify_term vars l) (grobify_term vars r)
2.114        end)
2.115         handle CTERM _ =>
2.116 -        (
2.117 -(*  (let val (l,r) = ring_dest_div tm
2.118 +        (  (let val (l,r) = field_dest_div tm
2.119            in grob_div (grobify_term vars l) (grobify_term vars r)
2.120            end)
2.121 -         handle CTERM _ => *)
2.122 +         handle CTERM _ =>
2.123            ((let val (l,r) = ring_dest_pow tm
2.124            in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r)
2.125            end)
2.126             handle CTERM _ => error "grobify_term: unknown or invalid term")))))))));
2.127  val eq_tm = idom_thm |> concl |> dest_arg |> dest_arg |> dest_fun2;
2.128 -(*ring_integral |> hd |> concl |> dest_arg
2.129 -                          |> dest_abs NONE |> snd |> dest_fun |> dest_fun; *)
2.130  val dest_eq = dest_binary eq_tm;
2.131
2.132  fun grobify_equation vars tm =
```
```     3.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Fri Apr 03 18:03:29 2009 +0200
3.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Sun Apr 05 05:07:10 2009 +0100
3.3 @@ -14,7 +14,7 @@
3.4   val semiring_normalize_ord_wrapper :  Proof.context -> NormalizerData.entry ->
3.5     (cterm -> cterm -> bool) -> conv
3.6   val semiring_normalizers_conv :
3.7 -     cterm list -> cterm list * thm list -> cterm list * thm list ->
3.8 +     cterm list -> cterm list * thm list -> cterm list * thm list -> cterm list * thm list ->
3.9       (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
3.10         {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
3.11  end
3.12 @@ -71,7 +71,7 @@
3.13
3.14
3.15  (* The main function! *)
3.16 -fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules)
3.17 +fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
3.18    (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
3.19  let
3.20
3.21 @@ -97,8 +97,7 @@
3.22
3.24    (case (r_ops, r_rules) of
3.25 -    ([], []) => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)
3.26 -  | ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
3.27 +    ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
3.28        let
3.29          val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
3.30          val neg_tm = Thm.dest_fun neg_pat
3.31 @@ -106,7 +105,18 @@
3.32          val is_sub = is_binop sub_tm
3.33        in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
3.34            sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
3.35 -      end);
3.36 +      end
3.37 +    | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm));
3.38 +
3.39 +val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) =
3.40 +  (case (f_ops, f_rules) of
3.41 +   ([divide_pat, inverse_pat], [div_inv, inv_div]) =>
3.42 +     let val div_tm = funpow 2 Thm.dest_fun divide_pat
3.43 +         val inv_tm = Thm.dest_fun inverse_pat
3.44 +     in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm)
3.45 +     end
3.46 +   | _ => (TrueI, TrueI, true_tm, true_tm, K false));
3.47 +
3.48  in fn variable_order =>
3.49   let
3.50
3.51 @@ -579,6 +589,10 @@
3.52         let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
3.53         in transitive th1 (polynomial_neg_conv (concl th1))
3.54         end
3.55 +     else if lopr aconvc inverse_tm then
3.56 +       let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
3.57 +       in transitive th1 (semiring_mul_conv (concl th1))
3.58 +       end
3.59       else
3.60         if not(is_comb lopr) then reflexive tm
3.61         else
3.62 @@ -588,6 +602,14 @@
3.63                let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
3.64                in transitive th1 (polynomial_pow_conv (concl th1))
3.65                end
3.66 +         else if opr aconvc divide_tm
3.67 +            then
3.68 +              let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l))
3.69 +                                        (polynomial_conv r)
3.70 +                  val th2 = (rewr_conv divide_inverse then_conv polynomial_mul_conv)
3.71 +                              (Thm.rhs_of th1)
3.72 +              in transitive th1 th2
3.73 +              end
3.74              else
3.75                if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
3.76                then
3.77 @@ -616,7 +638,7 @@
3.78
3.79  fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
3.80
3.81 -fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal},
3.82 +fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal},
3.83                                       {conv, dest_const, mk_const, is_const}) ord =
3.84    let
3.85      val pow_conv =
3.86 @@ -625,10 +647,10 @@
3.87          (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
3.88        then_conv conv ctxt
3.89      val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
3.90 -  in semiring_normalizers_conv vars semiring ring dat ord end;
3.91 +  in semiring_normalizers_conv vars semiring ring field dat ord end;
3.92
3.93 -fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
3.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);
3.95 +fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
3.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);
3.97
3.98  fun semiring_normalize_wrapper ctxt data =
3.99    semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
```
```     4.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Fri Apr 03 18:03:29 2009 +0200
4.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sun Apr 05 05:07:10 2009 +0100
4.3 @@ -11,7 +11,7 @@
4.4    val get: Proof.context -> simpset * (thm * entry) list
4.5    val match: Proof.context -> cterm -> entry option
4.6    val del: attribute
4.7 -  val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list, ideal: thm list}
4.8 +  val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list}
4.9      -> attribute
4.10    val funs: thm -> {is_const: morphism -> cterm -> bool,
4.11      dest_const: morphism -> cterm -> Rat.rat,
4.12 @@ -29,6 +29,7 @@
4.13   {vars: cterm list,
4.14    semiring: cterm list * thm list,
4.15    ring: cterm list * thm list,
4.16 +  field: cterm list * thm list,
4.17    idom: thm list,
4.18    ideal: thm list} *
4.19   {is_const: cterm -> bool,
4.20 @@ -57,7 +58,7 @@
4.21    let
4.22      fun match_inst
4.23          ({vars, semiring = (sr_ops, sr_rules),
4.24 -          ring = (r_ops, r_rules), idom, ideal},
4.25 +          ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
4.26           fns as {is_const, dest_const, mk_const, conv}) pat =
4.27         let
4.28          fun h instT =
4.29 @@ -68,11 +69,12 @@
4.30              val vars' = map substT_cterm vars;
4.31              val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
4.32              val ring' = (map substT_cterm r_ops, map substT r_rules);
4.33 +            val field' = (map substT_cterm f_ops, map substT f_rules);
4.34              val idom' = map substT idom;
4.35              val ideal' = map substT ideal;
4.36
4.37              val result = ({vars = vars', semiring = semiring',
4.38 -                           ring = ring', idom = idom', ideal = ideal'}, fns);
4.39 +                           ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
4.40            in SOME result end
4.41        in (case try Thm.match (pat, tm) of
4.42             NONE => NONE
4.43 @@ -80,8 +82,8 @@
4.44        end;
4.45
4.46      fun match_struct (_,
4.47 -        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), ...}, _): entry) =
4.48 -      get_first (match_inst entry) (sr_ops @ r_ops);
4.49 +        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
4.50 +      get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
4.51    in get_first match_struct (snd (get ctxt)) end;
4.52
4.53
4.54 @@ -91,6 +93,7 @@
4.55  val ringN = "ring";
4.56  val idomN = "idom";
4.57  val idealN = "ideal";
4.58 +val fieldN = "field";
4.59
4.60  fun undefined _ = raise Match;
4.61
4.62 @@ -103,7 +106,8 @@
4.63  val del_ss = Thm.declaration_attribute
4.64     (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
4.65
4.66 -fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom, ideal} =
4.67 +fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
4.68 +         field = (f_ops, f_rules), idom, ideal} =
4.69    Thm.declaration_attribute (fn key => fn context => context |> Data.map
4.70      let
4.71        val ctxt = Context.proof_of context;
4.72 @@ -119,11 +123,14 @@
4.73          check_rules semiringN sr_rules 37 andalso
4.74          check_ops ringN r_ops 2 andalso
4.75          check_rules ringN r_rules 2 andalso
4.76 +        check_ops fieldN f_ops 2 andalso
4.77 +        check_rules fieldN f_rules 2 andalso
4.78          check_rules idomN idom 2;
4.79
4.80        val mk_meta = LocalDefs.meta_rewrite_rule ctxt;
4.81        val sr_rules' = map mk_meta sr_rules;
4.82        val r_rules' = map mk_meta r_rules;
4.83 +      val f_rules' = map mk_meta f_rules;
4.84
4.85        fun rule i = nth sr_rules' (i - 1);
4.86
4.87 @@ -140,11 +147,12 @@
4.88        val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
4.89        val semiring = (sr_ops, sr_rules');
4.90        val ring = (r_ops, r_rules');
4.91 +      val field = (f_ops, f_rules');
4.92        val ideal' = map (symmetric o mk_meta) ideal
4.93      in
4.94        del_data key #>
4.95        apsnd (cons (key, ({vars = vars, semiring = semiring,
4.96 -                          ring = ring, idom = idom, ideal = ideal'},
4.97 +                          ring = ring, field = field, idom = idom, ideal = ideal'},
4.98               {is_const = undefined, dest_const = undefined, mk_const = undefined,
4.99               conv = undefined})))
4.100      end);
4.101 @@ -182,6 +190,7 @@
4.102  val any_keyword =
4.103    keyword2 semiringN opsN || keyword2 semiringN rulesN ||
4.104    keyword2 ringN opsN || keyword2 ringN rulesN ||
4.105 +  keyword2 fieldN opsN || keyword2 fieldN rulesN ||
4.106    keyword2 idomN rulesN || keyword2 idealN rulesN;
4.107
4.108  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
4.109 @@ -198,9 +207,12 @@
4.110         (keyword2 semiringN rulesN |-- thms)) --
4.111        (optional (keyword2 ringN opsN |-- terms) --
4.112         optional (keyword2 ringN rulesN |-- thms)) --
4.113 +      (optional (keyword2 fieldN opsN |-- terms) --
4.114 +       optional (keyword2 fieldN rulesN |-- thms)) --
4.115        optional (keyword2 idomN rulesN |-- thms) --
4.116        optional (keyword2 idealN rulesN |-- thms)
4.117 -      >> (fn (((sr, r), id), idl) => add {semiring = sr, ring = r, idom = id, ideal = idl}))
4.118 +      >> (fn ((((sr, r), f), id), idl) =>
4.119 +             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
4.120      "semiring normalizer data";
4.121
4.122  end;
```