# HG changeset patch # User haftmann # Date 1273156340 -7200 # Node ID 9b85b9d74b8319dcd33dc6b2c82304f19bafc2d3 # Parent 816da1023508529729e1b450863236f29139ab6f dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML diff -r 816da1023508 -r 9b85b9d74b83 src/HOL/Groebner_Basis.thy --- 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 \ 'a \ 'a" and neg :: "'a \ '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 \ 'a \ 'a" and inverse:: "'a \ 'a" @@ -421,6 +411,7 @@ "P \ False \ \ P" "\ P \ (P \ 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, diff -r 816da1023508 -r 9b85b9d74b83 src/HOL/IsaMakefile --- 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 \ diff -r 816da1023508 -r 9b85b9d74b83 src/HOL/Library/Sum_Of_Squares/sum_of_squares.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, diff -r 816da1023508 -r 9b85b9d74b83 src/HOL/Library/normarith.ML --- 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 diff -r 816da1023508 -r 9b85b9d74b83 src/HOL/Library/positivstellensatz.ML --- 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, diff -r 816da1023508 -r 9b85b9d74b83 src/HOL/Tools/Groebner_Basis/groebner.ML --- 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 diff -r 816da1023508 -r 9b85b9d74b83 src/HOL/Tools/Groebner_Basis/normalizer.ML --- 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; diff -r 816da1023508 -r 9b85b9d74b83 src/HOL/Tools/Groebner_Basis/normalizer_data.ML --- 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; diff -r 816da1023508 -r 9b85b9d74b83 src/HOL/ex/Groebner_Examples.thy --- 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)