1.1 --- a/Admin/makedist Sat Apr 04 20:22:39 2009 +0200
1.2 +++ b/Admin/makedist Sun Apr 05 23:19:39 2009 +0200
1.3 @@ -125,17 +125,6 @@
1.4 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
1.5
1.6
1.7 -# website
1.8 -
1.9 -mkdir -p ../website
1.10 -cat > ../website/config <<EOF
1.11 -DISTNAME="$DISTNAME"
1.12 -DISTBASE="$DISTBASE"
1.13 -EOF
1.14 -
1.15 -cp lib/html/library_index_content.template ../website/
1.16 -
1.17 -
1.18 # prepare dist for release
1.19
1.20 echo "###"
2.1 --- a/doc-src/pdfsetup.sty Sat Apr 04 20:22:39 2009 +0200
2.2 +++ b/doc-src/pdfsetup.sty Sun Apr 05 23:19:39 2009 +0200
2.3 @@ -1,9 +1,8 @@
2.4 -%% $Id$
2.5 %%
2.6 %% hyperref setup -- special version for Isabelle documentation
2.7 %%
2.8
2.9 -\message{pdfsetup.sty v0.4 2008-05-15}
2.10 +\usepackage{ifpdf}
2.11
2.12 \usepackage{color}
2.13 \definecolor{linkcolor}{rgb}{0,0,0}
2.14 @@ -14,3 +13,5 @@
2.15 \gdef\bold#1{\textbf{\hyperpage{#1}}}
2.16
2.17 \urlstyle{rm}
2.18 +
2.19 +\ifpdf\relax\else\renewcommand{\url}[1]{\nolinkurl{#1}}\fi
3.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sat Apr 04 20:22:39 2009 +0200
3.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Apr 05 23:19:39 2009 +0200
3.3 @@ -657,6 +657,7 @@
3.4 fun dest_frac ct = case term_of ct of
3.5 Const (@{const_name "HOL.divide"},_) $ a $ b=>
3.6 Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
3.7 + | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
3.8 | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
3.9
3.10 fun mk_frac phi cT x =
4.1 --- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Sat Apr 04 20:22:39 2009 +0200
4.2 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Sun Apr 05 23:19:39 2009 +0200
4.3 @@ -3,7 +3,7 @@
4.4 header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *}
4.5
4.6 theory Dense_Linear_Order_Ex
4.7 -imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
4.8 +imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
4.9 begin
4.10
4.11 lemma
5.1 --- a/src/HOL/Groebner_Basis.thy Sat Apr 04 20:22:39 2009 +0200
5.2 +++ b/src/HOL/Groebner_Basis.thy Sun Apr 05 23:19:39 2009 +0200
5.3 @@ -191,8 +191,7 @@
5.4
5.5 open Conv;
5.6
5.7 -fun numeral_is_const ct =
5.8 - can HOLogic.dest_number (Thm.term_of ct);
5.9 +fun numeral_is_const ct = can HOLogic.dest_number (Thm.term_of ct);
5.10
5.11 fun int_of_rat x =
5.12 (case Rat.quotient_of_rat x of (i, 1) => i
5.13 @@ -260,16 +259,22 @@
5.14 locale gb_field = gb_ring +
5.15 fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
5.16 and inverse:: "'a \<Rightarrow> 'a"
5.17 - assumes divide: "divide x y = mul x (inverse y)"
5.18 - and inverse: "inverse x = divide r1 x"
5.19 + assumes divide_inverse: "divide x y = mul x (inverse y)"
5.20 + and inverse_divide: "inverse x = divide r1 x"
5.21 begin
5.22
5.23 +lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" .
5.24 +
5.25 +lemmas field_rules = divide_inverse inverse_divide
5.26 +
5.27 lemmas gb_field_axioms' =
5.28 gb_field_axioms [normalizer
5.29 semiring ops: semiring_ops
5.30 semiring rules: semiring_rules
5.31 ring ops: ring_ops
5.32 - ring rules: ring_rules]
5.33 + ring rules: ring_rules
5.34 + field ops: field_ops
5.35 + field rules: field_rules]
5.36
5.37 end
5.38
5.39 @@ -393,6 +398,8 @@
5.40 semiring rules: semiring_rules
5.41 ring ops: ring_ops
5.42 ring rules: ring_rules
5.43 + field ops: field_ops
5.44 + field rules: field_rules
5.45 idom rules: noteq_reduce add_scale_eq_noteq
5.46 ideal rules: subr0_iff add_r0_iff]
5.47
5.48 @@ -482,8 +489,7 @@
5.49 by (simp add: add_divide_distrib)
5.50 lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
5.51 by (simp add: add_divide_distrib)
5.52 -
5.53 -
5.54 +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*}
5.55 ML{*
5.56 local
5.57 val zr = @{cpat "0"}
5.58 @@ -609,6 +615,10 @@
5.59 @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
5.60 name = "ord_frac_simproc", proc = proc3, identifier = []}
5.61
5.62 +local
5.63 +open Conv
5.64 +in
5.65 +
5.66 val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
5.67 @{thm "divide_Numeral1"},
5.68 @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
5.69 @@ -617,11 +627,11 @@
5.70 @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
5.71 @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
5.72 @{thm "diff_def"}, @{thm "minus_divide_left"},
5.73 - @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym]
5.74 + @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
5.75 + @{thm divide_inverse} RS sym, @{thm inverse_divide},
5.76 + fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))
5.77 + (@{thm divide_inverse} RS sym)]
5.78
5.79 -local
5.80 -open Conv
5.81 -in
5.82 val comp_conv = (Simplifier.rewrite
5.83 (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
5.84 addsimps ths addsimps simp_thms
5.85 @@ -636,13 +646,15 @@
5.86 fun numeral_is_const ct =
5.87 case term_of ct of
5.88 Const (@{const_name "HOL.divide"},_) $ a $ b =>
5.89 - numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct)
5.90 - | Const (@{const_name "HOL.uminus"},_)$t => numeral_is_const (Thm.dest_arg ct)
5.91 + can HOLogic.dest_number a andalso can HOLogic.dest_number b
5.92 + | Const (@{const_name "HOL.inverse"},_)$t => can HOLogic.dest_number t
5.93 | t => can HOLogic.dest_number t
5.94
5.95 fun dest_const ct = ((case term_of ct of
5.96 Const (@{const_name "HOL.divide"},_) $ a $ b=>
5.97 Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
5.98 + | Const (@{const_name "HOL.inverse"},_)$t =>
5.99 + Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
5.100 | t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
5.101 handle TERM _ => error "ring_dest_const")
5.102
6.1 --- a/src/HOL/Library/normarith.ML Sat Apr 04 20:22:39 2009 +0200
6.2 +++ b/src/HOL/Library/normarith.ML Sun Apr 05 23:19:39 2009 +0200
6.3 @@ -369,6 +369,7 @@
6.4
6.5 fun dest_ratconst t = case term_of t of
6.6 Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
6.7 + | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
6.8 | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
6.9 fun is_ratconst t = can dest_ratconst t
6.10
6.11 @@ -795,8 +796,9 @@
6.12
6.13 open Conv Thm Conv2;
6.14 val bool_eq = op = : bool *bool -> bool
6.15 - fun dest_ratconst t = case term_of t of
6.16 + fun dest_ratconst t = case term_of t of
6.17 Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
6.18 + | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
6.19 | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
6.20 fun is_ratconst t = can dest_ratconst t
6.21 fun augment_norm b t acc = case term_of t of
7.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Sat Apr 04 20:22:39 2009 +0200
7.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Sun Apr 05 23:19:39 2009 +0200
7.3 @@ -5,8 +5,8 @@
7.4 signature GROEBNER =
7.5 sig
7.6 val ring_and_ideal_conv :
7.7 - {idom: thm list, ring: cterm list * thm list, vars: cterm list,
7.8 - semiring: cterm list * thm list, ideal : thm list} ->
7.9 + {idom: thm list, ring: cterm list * thm list, field: cterm list * thm list,
7.10 + vars: cterm list, semiring: cterm list * thm list, ideal : thm list} ->
7.11 (cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
7.12 conv -> conv ->
7.13 {ring_conv : conv,
7.14 @@ -581,7 +581,8 @@
7.15 (** main **)
7.16
7.17 fun ring_and_ideal_conv
7.18 - {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom, ideal}
7.19 + {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
7.20 + field = (f_ops, f_rules), idom, ideal}
7.21 dest_const mk_const ring_eq_conv ring_normalize_conv =
7.22 let
7.23 val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
7.24 @@ -590,32 +591,37 @@
7.25
7.26 val (ring_sub_tm, ring_neg_tm) =
7.27 (case r_ops of
7.28 - [] => (@{cterm "True"}, @{cterm "True"})
7.29 - | [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat));
7.30 + [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat)
7.31 + |_ => (@{cterm "True"}, @{cterm "True"}));
7.32 +
7.33 + val (field_div_tm, field_inv_tm) =
7.34 + (case f_ops of
7.35 + [div_pat, inv_pat] => (dest_fun2 div_pat, dest_fun inv_pat)
7.36 + | _ => (@{cterm "True"}, @{cterm "True"}));
7.37
7.38 val [idom_thm, neq_thm] = idom;
7.39 val [idl_sub, idl_add0] =
7.40 if length ideal = 2 then ideal else [eq_commute, eq_commute]
7.41 - val ring_dest_neg =
7.42 - fn t => let val (l,r) = dest_comb t in
7.43 - if Term.could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t])
7.44 - end
7.45 + fun ring_dest_neg t =
7.46 + let val (l,r) = dest_comb t
7.47 + in if Term.could_unify(term_of l,term_of ring_neg_tm) then r
7.48 + else raise CTERM ("ring_dest_neg", [t])
7.49 + end
7.50
7.51 val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
7.52 -(*
7.53 - fun ring_dest_inv t =
7.54 + fun field_dest_inv t =
7.55 let val (l,r) = dest_comb t in
7.56 - if Term.could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv"
7.57 + if Term.could_unify(term_of l, term_of field_inv_tm) then r
7.58 + else raise CTERM ("field_dest_inv", [t])
7.59 end
7.60 -*)
7.61 val ring_dest_add = dest_binary ring_add_tm;
7.62 val ring_mk_add = mk_binop ring_add_tm;
7.63 val ring_dest_sub = dest_binary ring_sub_tm;
7.64 val ring_mk_sub = mk_binop ring_sub_tm;
7.65 val ring_dest_mul = dest_binary ring_mul_tm;
7.66 val ring_mk_mul = mk_binop ring_mul_tm;
7.67 -(* val ring_dest_div = dest_binary ring_div_tm;
7.68 - val ring_mk_div = mk_binop ring_div_tm;*)
7.69 + val field_dest_div = dest_binary field_div_tm;
7.70 + val field_mk_div = mk_binop field_div_tm;
7.71 val ring_dest_pow = dest_binary ring_pow_tm;
7.72 val ring_mk_pow = mk_binop ring_pow_tm ;
7.73 fun grobvars tm acc =
7.74 @@ -625,16 +631,16 @@
7.75 else if can ring_dest_add tm orelse can ring_dest_sub tm
7.76 orelse can ring_dest_mul tm
7.77 then grobvars (dest_arg1 tm) (grobvars (dest_arg tm) acc)
7.78 -(* else if can ring_dest_inv tm
7.79 - then
7.80 - let val gvs = grobvars (dest_arg tm) [] in
7.81 - if gvs = [] then acc else tm::acc
7.82 - end
7.83 - else if can ring_dest_div tm then
7.84 - let val lvs = grobvars (dest_arg1 tm) acc
7.85 - val gvs = grobvars (dest_arg tm) []
7.86 - in if gvs = [] then lvs else tm::acc
7.87 - end *)
7.88 + else if can field_dest_inv tm
7.89 + then
7.90 + let val gvs = grobvars (dest_arg tm) []
7.91 + in if null gvs then acc else tm::acc
7.92 + end
7.93 + else if can field_dest_div tm then
7.94 + let val lvs = grobvars (dest_arg1 tm) acc
7.95 + val gvs = grobvars (dest_arg tm) []
7.96 + in if null gvs then lvs else tm::acc
7.97 + end
7.98 else tm::acc ;
7.99
7.100 fun grobify_term vars tm =
7.101 @@ -648,8 +654,8 @@
7.102 ((grob_neg(grobify_term vars (ring_dest_neg tm)))
7.103 handle CTERM _ =>
7.104 (
7.105 -(* (grob_inv(grobify_term vars (ring_dest_inv tm)))
7.106 - handle CTERM _ => *)
7.107 + (grob_inv(grobify_term vars (field_dest_inv tm)))
7.108 + handle CTERM _ =>
7.109 ((let val (l,r) = ring_dest_add tm
7.110 in grob_add (grobify_term vars l) (grobify_term vars r)
7.111 end)
7.112 @@ -662,18 +668,15 @@
7.113 in grob_mul (grobify_term vars l) (grobify_term vars r)
7.114 end)
7.115 handle CTERM _ =>
7.116 - (
7.117 -(* (let val (l,r) = ring_dest_div tm
7.118 + ( (let val (l,r) = field_dest_div tm
7.119 in grob_div (grobify_term vars l) (grobify_term vars r)
7.120 end)
7.121 - handle CTERM _ => *)
7.122 + handle CTERM _ =>
7.123 ((let val (l,r) = ring_dest_pow tm
7.124 in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r)
7.125 end)
7.126 handle CTERM _ => error "grobify_term: unknown or invalid term")))))))));
7.127 val eq_tm = idom_thm |> concl |> dest_arg |> dest_arg |> dest_fun2;
7.128 -(*ring_integral |> hd |> concl |> dest_arg
7.129 - |> dest_abs NONE |> snd |> dest_fun |> dest_fun; *)
7.130 val dest_eq = dest_binary eq_tm;
7.131
7.132 fun grobify_equation vars tm =
8.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Sat Apr 04 20:22:39 2009 +0200
8.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Sun Apr 05 23:19:39 2009 +0200
8.3 @@ -14,7 +14,7 @@
8.4 val semiring_normalize_ord_wrapper : Proof.context -> NormalizerData.entry ->
8.5 (cterm -> cterm -> bool) -> conv
8.6 val semiring_normalizers_conv :
8.7 - cterm list -> cterm list * thm list -> cterm list * thm list ->
8.8 + cterm list -> cterm list * thm list -> cterm list * thm list -> cterm list * thm list ->
8.9 (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
8.10 {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
8.11 end
8.12 @@ -71,7 +71,7 @@
8.13
8.14
8.15 (* The main function! *)
8.16 -fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules)
8.17 +fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
8.18 (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
8.19 let
8.20
8.21 @@ -97,8 +97,7 @@
8.22
8.23 val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
8.24 (case (r_ops, r_rules) of
8.25 - ([], []) => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)
8.26 - | ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
8.27 + ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
8.28 let
8.29 val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
8.30 val neg_tm = Thm.dest_fun neg_pat
8.31 @@ -106,7 +105,18 @@
8.32 val is_sub = is_binop sub_tm
8.33 in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
8.34 sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
8.35 - end);
8.36 + end
8.37 + | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm));
8.38 +
8.39 +val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) =
8.40 + (case (f_ops, f_rules) of
8.41 + ([divide_pat, inverse_pat], [div_inv, inv_div]) =>
8.42 + let val div_tm = funpow 2 Thm.dest_fun divide_pat
8.43 + val inv_tm = Thm.dest_fun inverse_pat
8.44 + in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm)
8.45 + end
8.46 + | _ => (TrueI, TrueI, true_tm, true_tm, K false));
8.47 +
8.48 in fn variable_order =>
8.49 let
8.50
8.51 @@ -579,6 +589,10 @@
8.52 let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
8.53 in transitive th1 (polynomial_neg_conv (concl th1))
8.54 end
8.55 + else if lopr aconvc inverse_tm then
8.56 + let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
8.57 + in transitive th1 (semiring_mul_conv (concl th1))
8.58 + end
8.59 else
8.60 if not(is_comb lopr) then reflexive tm
8.61 else
8.62 @@ -588,6 +602,14 @@
8.63 let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
8.64 in transitive th1 (polynomial_pow_conv (concl th1))
8.65 end
8.66 + else if opr aconvc divide_tm
8.67 + then
8.68 + let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l))
8.69 + (polynomial_conv r)
8.70 + val th2 = (rewr_conv divide_inverse then_conv polynomial_mul_conv)
8.71 + (Thm.rhs_of th1)
8.72 + in transitive th1 th2
8.73 + end
8.74 else
8.75 if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
8.76 then
8.77 @@ -616,7 +638,7 @@
8.78
8.79 fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
8.80
8.81 -fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal},
8.82 +fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal},
8.83 {conv, dest_const, mk_const, is_const}) ord =
8.84 let
8.85 val pow_conv =
8.86 @@ -625,10 +647,10 @@
8.87 (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
8.88 then_conv conv ctxt
8.89 val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
8.90 - in semiring_normalizers_conv vars semiring ring dat ord end;
8.91 + in semiring_normalizers_conv vars semiring ring field dat ord end;
8.92
8.93 -fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
8.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);
8.95 +fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
8.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);
8.97
8.98 fun semiring_normalize_wrapper ctxt data =
8.99 semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
9.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sat Apr 04 20:22:39 2009 +0200
9.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Apr 05 23:19:39 2009 +0200
9.3 @@ -11,7 +11,7 @@
9.4 val get: Proof.context -> simpset * (thm * entry) list
9.5 val match: Proof.context -> cterm -> entry option
9.6 val del: attribute
9.7 - val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list, ideal: thm list}
9.8 + val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list}
9.9 -> attribute
9.10 val funs: thm -> {is_const: morphism -> cterm -> bool,
9.11 dest_const: morphism -> cterm -> Rat.rat,
9.12 @@ -29,6 +29,7 @@
9.13 {vars: cterm list,
9.14 semiring: cterm list * thm list,
9.15 ring: cterm list * thm list,
9.16 + field: cterm list * thm list,
9.17 idom: thm list,
9.18 ideal: thm list} *
9.19 {is_const: cterm -> bool,
9.20 @@ -57,7 +58,7 @@
9.21 let
9.22 fun match_inst
9.23 ({vars, semiring = (sr_ops, sr_rules),
9.24 - ring = (r_ops, r_rules), idom, ideal},
9.25 + ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
9.26 fns as {is_const, dest_const, mk_const, conv}) pat =
9.27 let
9.28 fun h instT =
9.29 @@ -68,11 +69,12 @@
9.30 val vars' = map substT_cterm vars;
9.31 val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
9.32 val ring' = (map substT_cterm r_ops, map substT r_rules);
9.33 + val field' = (map substT_cterm f_ops, map substT f_rules);
9.34 val idom' = map substT idom;
9.35 val ideal' = map substT ideal;
9.36
9.37 val result = ({vars = vars', semiring = semiring',
9.38 - ring = ring', idom = idom', ideal = ideal'}, fns);
9.39 + ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
9.40 in SOME result end
9.41 in (case try Thm.match (pat, tm) of
9.42 NONE => NONE
9.43 @@ -80,8 +82,8 @@
9.44 end;
9.45
9.46 fun match_struct (_,
9.47 - entry as ({semiring = (sr_ops, _), ring = (r_ops, _), ...}, _): entry) =
9.48 - get_first (match_inst entry) (sr_ops @ r_ops);
9.49 + entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
9.50 + get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
9.51 in get_first match_struct (snd (get ctxt)) end;
9.52
9.53
9.54 @@ -91,6 +93,7 @@
9.55 val ringN = "ring";
9.56 val idomN = "idom";
9.57 val idealN = "ideal";
9.58 +val fieldN = "field";
9.59
9.60 fun undefined _ = raise Match;
9.61
9.62 @@ -103,7 +106,8 @@
9.63 val del_ss = Thm.declaration_attribute
9.64 (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
9.65
9.66 -fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom, ideal} =
9.67 +fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
9.68 + field = (f_ops, f_rules), idom, ideal} =
9.69 Thm.declaration_attribute (fn key => fn context => context |> Data.map
9.70 let
9.71 val ctxt = Context.proof_of context;
9.72 @@ -119,11 +123,14 @@
9.73 check_rules semiringN sr_rules 37 andalso
9.74 check_ops ringN r_ops 2 andalso
9.75 check_rules ringN r_rules 2 andalso
9.76 + check_ops fieldN f_ops 2 andalso
9.77 + check_rules fieldN f_rules 2 andalso
9.78 check_rules idomN idom 2;
9.79
9.80 val mk_meta = LocalDefs.meta_rewrite_rule ctxt;
9.81 val sr_rules' = map mk_meta sr_rules;
9.82 val r_rules' = map mk_meta r_rules;
9.83 + val f_rules' = map mk_meta f_rules;
9.84
9.85 fun rule i = nth sr_rules' (i - 1);
9.86
9.87 @@ -140,11 +147,12 @@
9.88 val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
9.89 val semiring = (sr_ops, sr_rules');
9.90 val ring = (r_ops, r_rules');
9.91 + val field = (f_ops, f_rules');
9.92 val ideal' = map (symmetric o mk_meta) ideal
9.93 in
9.94 del_data key #>
9.95 apsnd (cons (key, ({vars = vars, semiring = semiring,
9.96 - ring = ring, idom = idom, ideal = ideal'},
9.97 + ring = ring, field = field, idom = idom, ideal = ideal'},
9.98 {is_const = undefined, dest_const = undefined, mk_const = undefined,
9.99 conv = undefined})))
9.100 end);
9.101 @@ -182,6 +190,7 @@
9.102 val any_keyword =
9.103 keyword2 semiringN opsN || keyword2 semiringN rulesN ||
9.104 keyword2 ringN opsN || keyword2 ringN rulesN ||
9.105 + keyword2 fieldN opsN || keyword2 fieldN rulesN ||
9.106 keyword2 idomN rulesN || keyword2 idealN rulesN;
9.107
9.108 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
9.109 @@ -198,9 +207,12 @@
9.110 (keyword2 semiringN rulesN |-- thms)) --
9.111 (optional (keyword2 ringN opsN |-- terms) --
9.112 optional (keyword2 ringN rulesN |-- thms)) --
9.113 + (optional (keyword2 fieldN opsN |-- terms) --
9.114 + optional (keyword2 fieldN rulesN |-- thms)) --
9.115 optional (keyword2 idomN rulesN |-- thms) --
9.116 optional (keyword2 idealN rulesN |-- thms)
9.117 - >> (fn (((sr, r), id), idl) => add {semiring = sr, ring = r, idom = id, ideal = idl}))
9.118 + >> (fn ((((sr, r), f), id), idl) =>
9.119 + add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
9.120 "semiring normalizer data";
9.121
9.122 end;