dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
--- a/src/HOL/Groebner_Basis.thy Wed May 05 16:53:21 2010 +0200
+++ b/src/HOL/Groebner_Basis.thy Thu May 06 16:32:20 2010 +0200
@@ -7,14 +7,13 @@
theory Groebner_Basis
imports Numeral_Simprocs Nat_Transfer
uses
- "Tools/Groebner_Basis/normalizer_data.ML"
"Tools/Groebner_Basis/normalizer.ML"
("Tools/Groebner_Basis/groebner.ML")
begin
subsection {* Semiring normalization *}
-setup NormalizerData.setup
+setup Normalizer.setup
locale gb_semiring =
fixes add mul pwr r0 r1
@@ -203,7 +202,7 @@
in
fun normalizer_funs key =
- NormalizerData.funs key
+ Normalizer.funs key
{is_const = fn phi => numeral_is_const,
dest_const = fn phi => fn ct =>
Rat.rat_of_int (snd
@@ -217,7 +216,6 @@
declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms'} *}
-
locale gb_ring = gb_semiring +
fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
and neg :: "'a \<Rightarrow> 'a"
@@ -246,14 +244,6 @@
declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}
-use "Tools/Groebner_Basis/normalizer.ML"
-
-
-method_setup sring_norm = {*
- Scan.succeed (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
-*} "semiring normalizer"
-
-
locale gb_field = gb_ring +
fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
and inverse:: "'a \<Rightarrow> 'a"
@@ -421,6 +411,7 @@
"P \<equiv> False \<Longrightarrow> \<not> P"
"\<not> P \<Longrightarrow> (P \<equiv> False)"
by auto
+
use "Tools/Groebner_Basis/groebner.ML"
method_setup algebra =
@@ -674,7 +665,7 @@
in
val field_comp_conv = comp_conv;
val fieldgb_declaration =
- NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms'}
+ Normalizer.funs @{thm class_fieldgb.fieldgb_axioms'}
{is_const = K numeral_is_const,
dest_const = K dest_const,
mk_const = mk_const,
--- a/src/HOL/IsaMakefile Wed May 05 16:53:21 2010 +0200
+++ b/src/HOL/IsaMakefile Thu May 06 16:32:20 2010 +0200
@@ -284,9 +284,7 @@
Tools/ATP_Manager/atp_manager.ML \
Tools/ATP_Manager/atp_systems.ML \
Tools/Groebner_Basis/groebner.ML \
- Tools/Groebner_Basis/misc.ML \
Tools/Groebner_Basis/normalizer.ML \
- Tools/Groebner_Basis/normalizer_data.ML \
Tools/choice_specification.ML \
Tools/int_arith.ML \
Tools/list_code.ML \
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Wed May 05 16:53:21 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu May 06 16:32:20 2010 +0200
@@ -1195,7 +1195,7 @@
fun real_nonlinear_prover proof_method ctxt =
let
val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt
- (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+ (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main)
@@ -1310,7 +1310,7 @@
fun real_nonlinear_subst_prover prover ctxt =
let
val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt
- (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+ (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
--- a/src/HOL/Library/normarith.ML Wed May 05 16:53:21 2010 +0200
+++ b/src/HOL/Library/normarith.ML Thu May 06 16:32:20 2010 +0200
@@ -167,7 +167,7 @@
(* FIXME : Should be computed statically!! *)
val real_poly_conv =
Normalizer.semiring_normalize_wrapper ctxt
- (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+ (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv)))
end;
@@ -278,7 +278,7 @@
(* FIXME: Should be computed statically!!*)
val real_poly_conv =
Normalizer.semiring_normalize_wrapper ctxt
- (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+ (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs
val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) []
val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check"
@@ -384,7 +384,7 @@
let
val real_poly_neg_conv = #neg
(Normalizer.semiring_normalizers_ord_wrapper ctxt
- (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
+ (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
val (th1,th2) = conj_pair(rawrule th)
in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc
end
--- a/src/HOL/Library/positivstellensatz.ML Wed May 05 16:53:21 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Thu May 06 16:32:20 2010 +0200
@@ -748,7 +748,7 @@
fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
val {add,mul,neg,pow,sub,main} =
Normalizer.semiring_normalizers_ord_wrapper ctxt
- (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+ (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
in gen_real_arith ctxt
(cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv,
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Wed May 05 16:53:21 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Thu May 06 16:32:20 2010 +0200
@@ -947,7 +947,7 @@
case try (find_term 0) form of
NONE => NONE
| SOME tm =>
- (case NormalizerData.match ctxt tm of
+ (case Normalizer.match ctxt tm of
NONE => NONE
| SOME (res as (theory, {is_const, dest_const,
mk_const, conv = ring_eq_conv})) =>
@@ -959,7 +959,7 @@
(case try (find_term 0 (* FIXME !? *)) form of
NONE => reflexive form
| SOME tm =>
- (case NormalizerData.match ctxt tm of
+ (case Normalizer.match ctxt tm of
NONE => reflexive form
| SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) =>
#ring_conv (ring_and_ideal_conv theory
@@ -969,7 +969,7 @@
fun ring_tac add_ths del_ths ctxt =
Object_Logic.full_atomize_tac
THEN' asm_full_simp_tac
- (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
+ (Simplifier.context ctxt (fst (Normalizer.get ctxt)) delsimps del_ths addsimps add_ths)
THEN' CSUBGOAL (fn (p, i) =>
rtac (let val form = Object_Logic.dest_judgment p
in case get_ring_ideal_convs ctxt form of
@@ -989,7 +989,7 @@
in
fun ideal_tac add_ths del_ths ctxt =
asm_full_simp_tac
- (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
+ (Simplifier.context ctxt (fst (Normalizer.get ctxt)) delsimps del_ths addsimps add_ths)
THEN'
CSUBGOAL (fn (p, i) =>
case get_ring_ideal_convs ctxt p of
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Wed May 05 16:53:21 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Thu May 06 16:32:20 2010 +0200
@@ -1,27 +1,235 @@
(* Title: HOL/Tools/Groebner_Basis/normalizer.ML
Author: Amine Chaieb, TU Muenchen
+
+Normalization of expressions in semirings.
*)
signature NORMALIZER =
sig
- val semiring_normalize_conv : Proof.context -> conv
- val semiring_normalize_ord_conv : Proof.context -> (cterm -> cterm -> bool) -> conv
- val semiring_normalize_tac : Proof.context -> int -> tactic
- val semiring_normalize_wrapper : Proof.context -> NormalizerData.entry -> conv
- val semiring_normalizers_ord_wrapper :
- Proof.context -> NormalizerData.entry -> (cterm -> cterm -> bool) ->
+ type entry
+ 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, 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,
+ mk_const: morphism -> ctyp -> Rat.rat -> cterm,
+ conv: morphism -> Proof.context -> cterm -> thm} -> declaration
+
+ val semiring_normalize_conv : Proof.context -> conv
+ val semiring_normalize_ord_conv : Proof.context -> (cterm -> cterm -> bool) -> conv
+ val semiring_normalize_wrapper : Proof.context -> entry -> conv
+ val semiring_normalize_ord_wrapper : Proof.context -> entry ->
+ (cterm -> cterm -> bool) -> conv
+ val semiring_normalizers_conv :
+ 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}
+ val semiring_normalizers_ord_wrapper :
+ Proof.context -> entry -> (cterm -> cterm -> bool) ->
{add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
- 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 * thm list ->
- (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
- {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
+
+ val setup: theory -> theory
end
structure Normalizer: NORMALIZER =
struct
+(* data *)
+
+type entry =
+ {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,
+ dest_const: cterm -> Rat.rat,
+ mk_const: ctyp -> Rat.rat -> cterm,
+ conv: Proof.context -> cterm -> thm};
+
+val eq_key = Thm.eq_thm;
+fun eq_data arg = eq_fst eq_key arg;
+
+structure Data = Generic_Data
+(
+ type T = simpset * (thm * entry) list;
+ val empty = (HOL_basic_ss, []);
+ val extend = I;
+ fun merge ((ss, e), (ss', e')) : T =
+ (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
+);
+
+val get = Data.get o Context.Proof;
+
+
+(* match data *)
+
+fun match ctxt tm =
+ let
+ fun match_inst
+ ({vars, semiring = (sr_ops, sr_rules),
+ 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 =
+ let
+ val substT = Thm.instantiate (instT, []);
+ val substT_cterm = Drule.cterm_rule substT;
+
+ 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', field = field', idom = idom', ideal = ideal'}, fns);
+ in SOME result end
+ in (case try Thm.match (pat, tm) of
+ NONE => NONE
+ | SOME (instT, _) => h instT)
+ end;
+
+ fun match_struct (_,
+ 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;
+
+
+(* logical content *)
+
+val semiringN = "semiring";
+val ringN = "ring";
+val idomN = "idom";
+val idealN = "ideal";
+val fieldN = "field";
+
+fun undefined _ = raise Match;
+
+fun del_data key = apsnd (remove eq_data (key, []));
+
+val del = Thm.declaration_attribute (Data.map o del_data);
+val add_ss = Thm.declaration_attribute
+ (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
+
+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),
+ field = (f_ops, f_rules), idom, ideal} =
+ Thm.declaration_attribute (fn key => fn context => context |> Data.map
+ let
+ val ctxt = Context.proof_of context;
+
+ fun check kind name xs n =
+ null xs orelse length xs = n orelse
+ error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
+ val check_ops = check "operations";
+ val check_rules = check "rules";
+
+ val _ =
+ check_ops semiringN sr_ops 5 andalso
+ 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 = Local_Defs.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);
+
+ val (cx, cy) = Thm.dest_binop (hd sr_ops);
+ val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
+ val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
+ val ((clx, crx), (cly, cry)) =
+ rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
+ val ((ca, cb), (cc, cd)) =
+ rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
+ val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
+ val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
+
+ 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, field = field, idom = idom, ideal = ideal'},
+ {is_const = undefined, dest_const = undefined, mk_const = undefined,
+ conv = undefined})))
+ end);
+
+
+(* extra-logical functions *)
+
+fun funs raw_key {is_const, dest_const, mk_const, conv} phi =
+ (Data.map o apsnd) (fn data =>
+ let
+ val key = Morphism.thm phi raw_key;
+ val _ = AList.defined eq_key data key orelse
+ raise THM ("No data entry for structure key", 0, [key]);
+ val fns = {is_const = is_const phi, dest_const = dest_const phi,
+ mk_const = mk_const phi, conv = conv phi};
+ in AList.map_entry eq_key key (apsnd (K fns)) data end);
+
+
+(* concrete syntax *)
+
+local
+
+fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
+fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
+fun keyword3 k1 k2 k3 =
+ Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
+
+val opsN = "ops";
+val rulesN = "rules";
+
+val normN = "norm";
+val constN = "const";
+val delN = "del";
+
+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;
+val terms = thms >> map Drule.dest_term;
+
+fun optional scan = Scan.optional scan [];
+
+in
+
+val normalizer_setup =
+ Attrib.setup @{binding normalizer}
+ (Scan.lift (Args.$$$ delN >> K del) ||
+ ((keyword2 semiringN opsN |-- terms) --
+ (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), f), id), idl) =>
+ add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
+ "semiring normalizer data";
+
+end;
+
open Conv;
(* Very basic stuff for terms *)
@@ -55,6 +263,7 @@
val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
@{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"},
@{thm "less_nat_number_of"}];
+
val nat_add_conv =
zerone_conv
(Simplifier.rewrite
@@ -64,7 +273,6 @@
@{thm add_number_of_left}, @{thm Suc_eq_plus1}]
@ map (fn th => th RS sym) @{thms numerals}));
-val nat_mul_conv = nat_add_conv;
val zeron_tm = @{cterm "0::nat"};
val onen_tm = @{cterm "1::nat"};
val true_tm = @{cterm "True"};
@@ -182,7 +390,7 @@
then
let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
val (l,r) = Thm.dest_comb(concl th1)
- in transitive th1 (Drule.arg_cong_rule l (nat_mul_conv r))
+ in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
end
else
if opr aconvc mul_tm
@@ -656,14 +864,16 @@
semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
fun semiring_normalize_ord_conv ctxt ord tm =
- (case NormalizerData.match ctxt tm of
+ (case match ctxt tm of
NONE => reflexive tm
| SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
-
fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
-fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) =>
- rtac (semiring_normalize_conv ctxt
- (cterm_of (ProofContext.theory_of ctxt) (fst (Logic.dest_equals goal)))) i);
+(* theory setup *)
+
+val setup =
+ normalizer_setup #>
+ Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
+
end;
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Wed May 05 16:53:21 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,226 +0,0 @@
-(* Title: HOL/Tools/Groebner_Basis/normalizer_data.ML
- Author: Amine Chaieb, TU Muenchen
-
-Ring normalization data.
-*)
-
-signature NORMALIZER_DATA =
-sig
- type entry
- 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, 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,
- mk_const: morphism -> ctyp -> Rat.rat -> cterm,
- conv: morphism -> Proof.context -> cterm -> thm} -> declaration
- val setup: theory -> theory
-end;
-
-structure NormalizerData: NORMALIZER_DATA =
-struct
-
-(* data *)
-
-type entry =
- {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,
- dest_const: cterm -> Rat.rat,
- mk_const: ctyp -> Rat.rat -> cterm,
- conv: Proof.context -> cterm -> thm};
-
-val eq_key = Thm.eq_thm;
-fun eq_data arg = eq_fst eq_key arg;
-
-structure Data = Generic_Data
-(
- type T = simpset * (thm * entry) list;
- val empty = (HOL_basic_ss, []);
- val extend = I;
- fun merge ((ss, e), (ss', e')) : T =
- (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
-);
-
-val get = Data.get o Context.Proof;
-
-
-(* match data *)
-
-fun match ctxt tm =
- let
- fun match_inst
- ({vars, semiring = (sr_ops, sr_rules),
- 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 =
- let
- val substT = Thm.instantiate (instT, []);
- val substT_cterm = Drule.cterm_rule substT;
-
- 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', field = field', idom = idom', ideal = ideal'}, fns);
- in SOME result end
- in (case try Thm.match (pat, tm) of
- NONE => NONE
- | SOME (instT, _) => h instT)
- end;
-
- fun match_struct (_,
- 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;
-
-
-(* logical content *)
-
-val semiringN = "semiring";
-val ringN = "ring";
-val idomN = "idom";
-val idealN = "ideal";
-val fieldN = "field";
-
-fun undefined _ = raise Match;
-
-fun del_data key = apsnd (remove eq_data (key, []));
-
-val del = Thm.declaration_attribute (Data.map o del_data);
-val add_ss = Thm.declaration_attribute
- (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
-
-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),
- field = (f_ops, f_rules), idom, ideal} =
- Thm.declaration_attribute (fn key => fn context => context |> Data.map
- let
- val ctxt = Context.proof_of context;
-
- fun check kind name xs n =
- null xs orelse length xs = n orelse
- error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
- val check_ops = check "operations";
- val check_rules = check "rules";
-
- val _ =
- check_ops semiringN sr_ops 5 andalso
- 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 = Local_Defs.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);
-
- val (cx, cy) = Thm.dest_binop (hd sr_ops);
- val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
- val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
- val ((clx, crx), (cly, cry)) =
- rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
- val ((ca, cb), (cc, cd)) =
- rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
- val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
- val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
-
- 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, field = field, idom = idom, ideal = ideal'},
- {is_const = undefined, dest_const = undefined, mk_const = undefined,
- conv = undefined})))
- end);
-
-
-(* extra-logical functions *)
-
-fun funs raw_key {is_const, dest_const, mk_const, conv} phi =
- (Data.map o apsnd) (fn data =>
- let
- val key = Morphism.thm phi raw_key;
- val _ = AList.defined eq_key data key orelse
- raise THM ("No data entry for structure key", 0, [key]);
- val fns = {is_const = is_const phi, dest_const = dest_const phi,
- mk_const = mk_const phi, conv = conv phi};
- in AList.map_entry eq_key key (apsnd (K fns)) data end);
-
-
-(* concrete syntax *)
-
-local
-
-fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
-fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
-fun keyword3 k1 k2 k3 =
- Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
-
-val opsN = "ops";
-val rulesN = "rules";
-
-val normN = "norm";
-val constN = "const";
-val delN = "del";
-
-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;
-val terms = thms >> map Drule.dest_term;
-
-fun optional scan = Scan.optional scan [];
-
-in
-
-val normalizer_setup =
- Attrib.setup @{binding normalizer}
- (Scan.lift (Args.$$$ delN >> K del) ||
- ((keyword2 semiringN opsN |-- terms) --
- (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), f), id), idl) =>
- add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
- "semiring normalizer data";
-
-end;
-
-
-(* theory setup *)
-
-val setup =
- normalizer_setup #>
- Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
-
-end;
--- a/src/HOL/ex/Groebner_Examples.thy Wed May 05 16:53:21 2010 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy Thu May 06 16:32:20 2010 +0200
@@ -10,14 +10,26 @@
subsection {* Basic examples *}
-schematic_lemma "3 ^ 3 == (?X::'a::{number_ring})"
- by sring_norm
+lemma
+ fixes x :: int
+ shows "x ^ 3 = x ^ 3"
+ apply (tactic {* ALLGOALS (CONVERSION
+ (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
+ by (rule refl)
-schematic_lemma "(x - (-2))^5 == ?X::int"
- by sring_norm
+lemma
+ fixes x :: int
+ shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x² + (80 * x + 32))))"
+ apply (tactic {* ALLGOALS (CONVERSION
+ (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
+ by (rule refl)
-schematic_lemma "(x - (-2))^5 * (y - 78) ^ 8 == ?X::int"
- by sring_norm
+schematic_lemma
+ fixes x :: int
+ shows "(x - (-2))^5 * (y - 78) ^ 8 = ?X"
+ apply (tactic {* ALLGOALS (CONVERSION
+ (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
+ by (rule refl)
lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
apply (simp only: power_Suc power_0)