--- a/Admin/makedist Sat Apr 04 20:22:39 2009 +0200
+++ b/Admin/makedist Sun Apr 05 23:19:39 2009 +0200
@@ -125,17 +125,6 @@
cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
-# website
-
-mkdir -p ../website
-cat > ../website/config <<EOF
-DISTNAME="$DISTNAME"
-DISTBASE="$DISTBASE"
-EOF
-
-cp lib/html/library_index_content.template ../website/
-
-
# prepare dist for release
echo "###"
--- a/doc-src/pdfsetup.sty Sat Apr 04 20:22:39 2009 +0200
+++ b/doc-src/pdfsetup.sty Sun Apr 05 23:19:39 2009 +0200
@@ -1,9 +1,8 @@
-%% $Id$
%%
%% hyperref setup -- special version for Isabelle documentation
%%
-\message{pdfsetup.sty v0.4 2008-05-15}
+\usepackage{ifpdf}
\usepackage{color}
\definecolor{linkcolor}{rgb}{0,0,0}
@@ -14,3 +13,5 @@
\gdef\bold#1{\textbf{\hyperpage{#1}}}
\urlstyle{rm}
+
+\ifpdf\relax\else\renewcommand{\url}[1]{\nolinkurl{#1}}\fi
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sat Apr 04 20:22:39 2009 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Apr 05 23:19:39 2009 +0200
@@ -657,6 +657,7 @@
fun dest_frac ct = case term_of ct of
Const (@{const_name "HOL.divide"},_) $ a $ b=>
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
+ | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
| t => Rat.rat_of_int (snd (HOLogic.dest_number t))
fun mk_frac phi cT x =
--- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Sat Apr 04 20:22:39 2009 +0200
+++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Sun Apr 05 23:19:39 2009 +0200
@@ -3,7 +3,7 @@
header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *}
theory Dense_Linear_Order_Ex
-imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
begin
lemma
--- a/src/HOL/Groebner_Basis.thy Sat Apr 04 20:22:39 2009 +0200
+++ b/src/HOL/Groebner_Basis.thy Sun Apr 05 23:19:39 2009 +0200
@@ -191,8 +191,7 @@
open Conv;
-fun numeral_is_const ct =
- can HOLogic.dest_number (Thm.term_of ct);
+fun numeral_is_const ct = can HOLogic.dest_number (Thm.term_of ct);
fun int_of_rat x =
(case Rat.quotient_of_rat x of (i, 1) => i
@@ -260,16 +259,22 @@
locale gb_field = gb_ring +
fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
and inverse:: "'a \<Rightarrow> 'a"
- assumes divide: "divide x y = mul x (inverse y)"
- and inverse: "inverse x = divide r1 x"
+ assumes divide_inverse: "divide x y = mul x (inverse y)"
+ and inverse_divide: "inverse x = divide r1 x"
begin
+lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" .
+
+lemmas field_rules = divide_inverse inverse_divide
+
lemmas gb_field_axioms' =
gb_field_axioms [normalizer
semiring ops: semiring_ops
semiring rules: semiring_rules
ring ops: ring_ops
- ring rules: ring_rules]
+ ring rules: ring_rules
+ field ops: field_ops
+ field rules: field_rules]
end
@@ -393,6 +398,8 @@
semiring rules: semiring_rules
ring ops: ring_ops
ring rules: ring_rules
+ field ops: field_ops
+ field rules: field_rules
idom rules: noteq_reduce add_scale_eq_noteq
ideal rules: subr0_iff add_r0_iff]
@@ -482,8 +489,7 @@
by (simp add: add_divide_distrib)
lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
by (simp add: add_divide_distrib)
-
-
+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*}
ML{*
local
val zr = @{cpat "0"}
@@ -609,6 +615,10 @@
@{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
name = "ord_frac_simproc", proc = proc3, identifier = []}
+local
+open Conv
+in
+
val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
@{thm "divide_Numeral1"},
@{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
@@ -617,11 +627,11 @@
@{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
@{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
@{thm "diff_def"}, @{thm "minus_divide_left"},
- @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym]
+ @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
+ @{thm divide_inverse} RS sym, @{thm inverse_divide},
+ fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))
+ (@{thm divide_inverse} RS sym)]
-local
-open Conv
-in
val comp_conv = (Simplifier.rewrite
(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
addsimps ths addsimps simp_thms
@@ -636,13 +646,15 @@
fun numeral_is_const ct =
case term_of ct of
Const (@{const_name "HOL.divide"},_) $ a $ b =>
- numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct)
- | Const (@{const_name "HOL.uminus"},_)$t => numeral_is_const (Thm.dest_arg ct)
+ can HOLogic.dest_number a andalso can HOLogic.dest_number b
+ | Const (@{const_name "HOL.inverse"},_)$t => can HOLogic.dest_number t
| t => can HOLogic.dest_number t
fun dest_const ct = ((case term_of ct of
Const (@{const_name "HOL.divide"},_) $ a $ b=>
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
+ | Const (@{const_name "HOL.inverse"},_)$t =>
+ Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
| t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
handle TERM _ => error "ring_dest_const")
--- a/src/HOL/Library/normarith.ML Sat Apr 04 20:22:39 2009 +0200
+++ b/src/HOL/Library/normarith.ML Sun Apr 05 23:19:39 2009 +0200
@@ -369,6 +369,7 @@
fun dest_ratconst t = case term_of t of
Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+ | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
| _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
fun is_ratconst t = can dest_ratconst t
@@ -795,8 +796,9 @@
open Conv Thm Conv2;
val bool_eq = op = : bool *bool -> bool
- fun dest_ratconst t = case term_of t of
+ fun dest_ratconst t = case term_of t of
Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+ | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
| _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
fun is_ratconst t = can dest_ratconst t
fun augment_norm b t acc = case term_of t of
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Sat Apr 04 20:22:39 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Sun Apr 05 23:19:39 2009 +0200
@@ -5,8 +5,8 @@
signature GROEBNER =
sig
val ring_and_ideal_conv :
- {idom: thm list, ring: cterm list * thm list, vars: cterm list,
- semiring: cterm list * thm list, ideal : thm list} ->
+ {idom: thm list, ring: cterm list * thm list, field: cterm list * thm list,
+ vars: cterm list, semiring: cterm list * thm list, ideal : thm list} ->
(cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
conv -> conv ->
{ring_conv : conv,
@@ -581,7 +581,8 @@
(** main **)
fun ring_and_ideal_conv
- {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom, ideal}
+ {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
+ field = (f_ops, f_rules), idom, ideal}
dest_const mk_const ring_eq_conv ring_normalize_conv =
let
val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
@@ -590,32 +591,37 @@
val (ring_sub_tm, ring_neg_tm) =
(case r_ops of
- [] => (@{cterm "True"}, @{cterm "True"})
- | [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat));
+ [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat)
+ |_ => (@{cterm "True"}, @{cterm "True"}));
+
+ val (field_div_tm, field_inv_tm) =
+ (case f_ops of
+ [div_pat, inv_pat] => (dest_fun2 div_pat, dest_fun inv_pat)
+ | _ => (@{cterm "True"}, @{cterm "True"}));
val [idom_thm, neq_thm] = idom;
val [idl_sub, idl_add0] =
if length ideal = 2 then ideal else [eq_commute, eq_commute]
- val ring_dest_neg =
- fn t => let val (l,r) = dest_comb t in
- if Term.could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t])
- end
+ fun ring_dest_neg t =
+ let val (l,r) = dest_comb t
+ in if Term.could_unify(term_of l,term_of ring_neg_tm) then r
+ else raise CTERM ("ring_dest_neg", [t])
+ end
val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
-(*
- fun ring_dest_inv t =
+ fun field_dest_inv t =
let val (l,r) = dest_comb t in
- if Term.could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv"
+ if Term.could_unify(term_of l, term_of field_inv_tm) then r
+ else raise CTERM ("field_dest_inv", [t])
end
-*)
val ring_dest_add = dest_binary ring_add_tm;
val ring_mk_add = mk_binop ring_add_tm;
val ring_dest_sub = dest_binary ring_sub_tm;
val ring_mk_sub = mk_binop ring_sub_tm;
val ring_dest_mul = dest_binary ring_mul_tm;
val ring_mk_mul = mk_binop ring_mul_tm;
-(* val ring_dest_div = dest_binary ring_div_tm;
- val ring_mk_div = mk_binop ring_div_tm;*)
+ val field_dest_div = dest_binary field_div_tm;
+ val field_mk_div = mk_binop field_div_tm;
val ring_dest_pow = dest_binary ring_pow_tm;
val ring_mk_pow = mk_binop ring_pow_tm ;
fun grobvars tm acc =
@@ -625,16 +631,16 @@
else if can ring_dest_add tm orelse can ring_dest_sub tm
orelse can ring_dest_mul tm
then grobvars (dest_arg1 tm) (grobvars (dest_arg tm) acc)
-(* else if can ring_dest_inv tm
- then
- let val gvs = grobvars (dest_arg tm) [] in
- if gvs = [] then acc else tm::acc
- end
- else if can ring_dest_div tm then
- let val lvs = grobvars (dest_arg1 tm) acc
- val gvs = grobvars (dest_arg tm) []
- in if gvs = [] then lvs else tm::acc
- end *)
+ else if can field_dest_inv tm
+ then
+ let val gvs = grobvars (dest_arg tm) []
+ in if null gvs then acc else tm::acc
+ end
+ else if can field_dest_div tm then
+ let val lvs = grobvars (dest_arg1 tm) acc
+ val gvs = grobvars (dest_arg tm) []
+ in if null gvs then lvs else tm::acc
+ end
else tm::acc ;
fun grobify_term vars tm =
@@ -648,8 +654,8 @@
((grob_neg(grobify_term vars (ring_dest_neg tm)))
handle CTERM _ =>
(
-(* (grob_inv(grobify_term vars (ring_dest_inv tm)))
- handle CTERM _ => *)
+ (grob_inv(grobify_term vars (field_dest_inv tm)))
+ handle CTERM _ =>
((let val (l,r) = ring_dest_add tm
in grob_add (grobify_term vars l) (grobify_term vars r)
end)
@@ -662,18 +668,15 @@
in grob_mul (grobify_term vars l) (grobify_term vars r)
end)
handle CTERM _ =>
- (
-(* (let val (l,r) = ring_dest_div tm
+ ( (let val (l,r) = field_dest_div tm
in grob_div (grobify_term vars l) (grobify_term vars r)
end)
- handle CTERM _ => *)
+ handle CTERM _ =>
((let val (l,r) = ring_dest_pow tm
in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r)
end)
handle CTERM _ => error "grobify_term: unknown or invalid term")))))))));
val eq_tm = idom_thm |> concl |> dest_arg |> dest_arg |> dest_fun2;
-(*ring_integral |> hd |> concl |> dest_arg
- |> dest_abs NONE |> snd |> dest_fun |> dest_fun; *)
val dest_eq = dest_binary eq_tm;
fun grobify_equation vars tm =
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Sat Apr 04 20:22:39 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Sun Apr 05 23:19:39 2009 +0200
@@ -14,7 +14,7 @@
val semiring_normalize_ord_wrapper : Proof.context -> NormalizerData.entry ->
(cterm -> cterm -> bool) -> conv
val semiring_normalizers_conv :
- cterm list -> cterm list * thm list -> cterm list * thm list ->
+ cterm list -> cterm list * thm list -> cterm list * thm list -> cterm list * thm list ->
(cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
{add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
end
@@ -71,7 +71,7 @@
(* The main function! *)
-fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules)
+fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
(is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
let
@@ -97,8 +97,7 @@
val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
(case (r_ops, r_rules) of
- ([], []) => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)
- | ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
+ ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
let
val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
val neg_tm = Thm.dest_fun neg_pat
@@ -106,7 +105,18 @@
val is_sub = is_binop sub_tm
in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
- end);
+ end
+ | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm));
+
+val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) =
+ (case (f_ops, f_rules) of
+ ([divide_pat, inverse_pat], [div_inv, inv_div]) =>
+ let val div_tm = funpow 2 Thm.dest_fun divide_pat
+ val inv_tm = Thm.dest_fun inverse_pat
+ in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm)
+ end
+ | _ => (TrueI, TrueI, true_tm, true_tm, K false));
+
in fn variable_order =>
let
@@ -579,6 +589,10 @@
let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
in transitive th1 (polynomial_neg_conv (concl th1))
end
+ else if lopr aconvc inverse_tm then
+ let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
+ in transitive th1 (semiring_mul_conv (concl th1))
+ end
else
if not(is_comb lopr) then reflexive tm
else
@@ -588,6 +602,14 @@
let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
in transitive th1 (polynomial_pow_conv (concl th1))
end
+ else if opr aconvc divide_tm
+ then
+ let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l))
+ (polynomial_conv r)
+ val th2 = (rewr_conv divide_inverse then_conv polynomial_mul_conv)
+ (Thm.rhs_of th1)
+ in transitive th1 th2
+ end
else
if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
then
@@ -616,7 +638,7 @@
fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
-fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal},
+fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal},
{conv, dest_const, mk_const, is_const}) ord =
let
val pow_conv =
@@ -625,10 +647,10 @@
(HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
then_conv conv ctxt
val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
- in semiring_normalizers_conv vars semiring ring dat ord end;
+ in semiring_normalizers_conv vars semiring ring field dat ord end;
-fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
- #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);
+fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
+ #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);
fun semiring_normalize_wrapper ctxt data =
semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sat Apr 04 20:22:39 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Apr 05 23:19:39 2009 +0200
@@ -11,7 +11,7 @@
val get: Proof.context -> simpset * (thm * entry) list
val match: Proof.context -> cterm -> entry option
val del: attribute
- val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list, ideal: thm list}
+ val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list}
-> attribute
val funs: thm -> {is_const: morphism -> cterm -> bool,
dest_const: morphism -> cterm -> Rat.rat,
@@ -29,6 +29,7 @@
{vars: cterm list,
semiring: cterm list * thm list,
ring: cterm list * thm list,
+ field: cterm list * thm list,
idom: thm list,
ideal: thm list} *
{is_const: cterm -> bool,
@@ -57,7 +58,7 @@
let
fun match_inst
({vars, semiring = (sr_ops, sr_rules),
- ring = (r_ops, r_rules), idom, ideal},
+ ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
fns as {is_const, dest_const, mk_const, conv}) pat =
let
fun h instT =
@@ -68,11 +69,12 @@
val vars' = map substT_cterm vars;
val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
val ring' = (map substT_cterm r_ops, map substT r_rules);
+ val field' = (map substT_cterm f_ops, map substT f_rules);
val idom' = map substT idom;
val ideal' = map substT ideal;
val result = ({vars = vars', semiring = semiring',
- ring = ring', idom = idom', ideal = ideal'}, fns);
+ ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
in SOME result end
in (case try Thm.match (pat, tm) of
NONE => NONE
@@ -80,8 +82,8 @@
end;
fun match_struct (_,
- entry as ({semiring = (sr_ops, _), ring = (r_ops, _), ...}, _): entry) =
- get_first (match_inst entry) (sr_ops @ r_ops);
+ entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
+ get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
in get_first match_struct (snd (get ctxt)) end;
@@ -91,6 +93,7 @@
val ringN = "ring";
val idomN = "idom";
val idealN = "ideal";
+val fieldN = "field";
fun undefined _ = raise Match;
@@ -103,7 +106,8 @@
val del_ss = Thm.declaration_attribute
(fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
-fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom, ideal} =
+fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
+ field = (f_ops, f_rules), idom, ideal} =
Thm.declaration_attribute (fn key => fn context => context |> Data.map
let
val ctxt = Context.proof_of context;
@@ -119,11 +123,14 @@
check_rules semiringN sr_rules 37 andalso
check_ops ringN r_ops 2 andalso
check_rules ringN r_rules 2 andalso
+ check_ops fieldN f_ops 2 andalso
+ check_rules fieldN f_rules 2 andalso
check_rules idomN idom 2;
val mk_meta = LocalDefs.meta_rewrite_rule ctxt;
val sr_rules' = map mk_meta sr_rules;
val r_rules' = map mk_meta r_rules;
+ val f_rules' = map mk_meta f_rules;
fun rule i = nth sr_rules' (i - 1);
@@ -140,11 +147,12 @@
val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
val semiring = (sr_ops, sr_rules');
val ring = (r_ops, r_rules');
+ val field = (f_ops, f_rules');
val ideal' = map (symmetric o mk_meta) ideal
in
del_data key #>
apsnd (cons (key, ({vars = vars, semiring = semiring,
- ring = ring, idom = idom, ideal = ideal'},
+ ring = ring, field = field, idom = idom, ideal = ideal'},
{is_const = undefined, dest_const = undefined, mk_const = undefined,
conv = undefined})))
end);
@@ -182,6 +190,7 @@
val any_keyword =
keyword2 semiringN opsN || keyword2 semiringN rulesN ||
keyword2 ringN opsN || keyword2 ringN rulesN ||
+ keyword2 fieldN opsN || keyword2 fieldN rulesN ||
keyword2 idomN rulesN || keyword2 idealN rulesN;
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
@@ -198,9 +207,12 @@
(keyword2 semiringN rulesN |-- thms)) --
(optional (keyword2 ringN opsN |-- terms) --
optional (keyword2 ringN rulesN |-- thms)) --
+ (optional (keyword2 fieldN opsN |-- terms) --
+ optional (keyword2 fieldN rulesN |-- thms)) --
optional (keyword2 idomN rulesN |-- thms) --
optional (keyword2 idealN rulesN |-- thms)
- >> (fn (((sr, r), id), idl) => add {semiring = sr, ring = r, idom = id, ideal = idl}))
+ >> (fn ((((sr, r), f), id), idl) =>
+ add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
"semiring normalizer data";
end;