1.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Fri Apr 03 18:03:29 2009 +0200
1.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Apr 05 05:07:10 2009 +0100
1.3 @@ -11,7 +11,7 @@
1.4 val get: Proof.context -> simpset * (thm * entry) list
1.5 val match: Proof.context -> cterm -> entry option
1.6 val del: attribute
1.7 - val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list, ideal: thm list}
1.8 + val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list}
1.9 -> attribute
1.10 val funs: thm -> {is_const: morphism -> cterm -> bool,
1.11 dest_const: morphism -> cterm -> Rat.rat,
1.12 @@ -29,6 +29,7 @@
1.13 {vars: cterm list,
1.14 semiring: cterm list * thm list,
1.15 ring: cterm list * thm list,
1.16 + field: cterm list * thm list,
1.17 idom: thm list,
1.18 ideal: thm list} *
1.19 {is_const: cterm -> bool,
1.20 @@ -57,7 +58,7 @@
1.21 let
1.22 fun match_inst
1.23 ({vars, semiring = (sr_ops, sr_rules),
1.24 - ring = (r_ops, r_rules), idom, ideal},
1.25 + ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
1.26 fns as {is_const, dest_const, mk_const, conv}) pat =
1.27 let
1.28 fun h instT =
1.29 @@ -68,11 +69,12 @@
1.30 val vars' = map substT_cterm vars;
1.31 val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
1.32 val ring' = (map substT_cterm r_ops, map substT r_rules);
1.33 + val field' = (map substT_cterm f_ops, map substT f_rules);
1.34 val idom' = map substT idom;
1.35 val ideal' = map substT ideal;
1.36
1.37 val result = ({vars = vars', semiring = semiring',
1.38 - ring = ring', idom = idom', ideal = ideal'}, fns);
1.39 + ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
1.40 in SOME result end
1.41 in (case try Thm.match (pat, tm) of
1.42 NONE => NONE
1.43 @@ -80,8 +82,8 @@
1.44 end;
1.45
1.46 fun match_struct (_,
1.47 - entry as ({semiring = (sr_ops, _), ring = (r_ops, _), ...}, _): entry) =
1.48 - get_first (match_inst entry) (sr_ops @ r_ops);
1.49 + entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
1.50 + get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
1.51 in get_first match_struct (snd (get ctxt)) end;
1.52
1.53
1.54 @@ -91,6 +93,7 @@
1.55 val ringN = "ring";
1.56 val idomN = "idom";
1.57 val idealN = "ideal";
1.58 +val fieldN = "field";
1.59
1.60 fun undefined _ = raise Match;
1.61
1.62 @@ -103,7 +106,8 @@
1.63 val del_ss = Thm.declaration_attribute
1.64 (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
1.65
1.66 -fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom, ideal} =
1.67 +fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
1.68 + field = (f_ops, f_rules), idom, ideal} =
1.69 Thm.declaration_attribute (fn key => fn context => context |> Data.map
1.70 let
1.71 val ctxt = Context.proof_of context;
1.72 @@ -119,11 +123,14 @@
1.73 check_rules semiringN sr_rules 37 andalso
1.74 check_ops ringN r_ops 2 andalso
1.75 check_rules ringN r_rules 2 andalso
1.76 + check_ops fieldN f_ops 2 andalso
1.77 + check_rules fieldN f_rules 2 andalso
1.78 check_rules idomN idom 2;
1.79
1.80 val mk_meta = LocalDefs.meta_rewrite_rule ctxt;
1.81 val sr_rules' = map mk_meta sr_rules;
1.82 val r_rules' = map mk_meta r_rules;
1.83 + val f_rules' = map mk_meta f_rules;
1.84
1.85 fun rule i = nth sr_rules' (i - 1);
1.86
1.87 @@ -140,11 +147,12 @@
1.88 val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
1.89 val semiring = (sr_ops, sr_rules');
1.90 val ring = (r_ops, r_rules');
1.91 + val field = (f_ops, f_rules');
1.92 val ideal' = map (symmetric o mk_meta) ideal
1.93 in
1.94 del_data key #>
1.95 apsnd (cons (key, ({vars = vars, semiring = semiring,
1.96 - ring = ring, idom = idom, ideal = ideal'},
1.97 + ring = ring, field = field, idom = idom, ideal = ideal'},
1.98 {is_const = undefined, dest_const = undefined, mk_const = undefined,
1.99 conv = undefined})))
1.100 end);
1.101 @@ -182,6 +190,7 @@
1.102 val any_keyword =
1.103 keyword2 semiringN opsN || keyword2 semiringN rulesN ||
1.104 keyword2 ringN opsN || keyword2 ringN rulesN ||
1.105 + keyword2 fieldN opsN || keyword2 fieldN rulesN ||
1.106 keyword2 idomN rulesN || keyword2 idealN rulesN;
1.107
1.108 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
1.109 @@ -198,9 +207,12 @@
1.110 (keyword2 semiringN rulesN |-- thms)) --
1.111 (optional (keyword2 ringN opsN |-- terms) --
1.112 optional (keyword2 ringN rulesN |-- thms)) --
1.113 + (optional (keyword2 fieldN opsN |-- terms) --
1.114 + optional (keyword2 fieldN rulesN |-- thms)) --
1.115 optional (keyword2 idomN rulesN |-- thms) --
1.116 optional (keyword2 idealN rulesN |-- thms)
1.117 - >> (fn (((sr, r), id), idl) => add {semiring = sr, ring = r, idom = id, ideal = idl}))
1.118 + >> (fn ((((sr, r), f), id), idl) =>
1.119 + add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
1.120 "semiring normalizer data";
1.121
1.122 end;