# HG changeset patch # User chaieb # Date 1181579296 -7200 # Node ID 01c09922ce59affdef2fc80e18a972fdef8344a1 # Parent 0dbb303022596c0851be2c0a123f7c3bf7b449a4 Conversion for computation on constants now depends on the context diff -r 0dbb30302259 -r 01c09922ce59 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Mon Jun 11 18:28:15 2007 +0200 +++ b/src/HOL/Groebner_Basis.thy Mon Jun 11 18:28:16 2007 +0200 @@ -209,7 +209,7 @@ handle TERM _ => error "ring_dest_const")), mk_const = fn phi => fn cT => fn x => Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)), - conv = fn phi => numeral_conv} + conv = fn phi => K numeral_conv} *} @@ -250,7 +250,7 @@ handle TERM _ => error "ring_dest_const")), mk_const = fn phi => fn cT => fn x => Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)), - conv = fn phi => numeral_conv} + conv = fn phi => K numeral_conv} *} use "Tools/Groebner_Basis/normalizer.ML" @@ -362,7 +362,7 @@ handle TERM _ => error "ring_dest_const")), mk_const = fn phi => fn cT => fn x => Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)), - conv = fn phi => numeral_conv} + conv = fn phi => K numeral_conv} *} @@ -397,7 +397,7 @@ handle TERM _ => error "ring_dest_const")), mk_const = fn phi => fn cT => fn x => Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)), - conv = fn phi => numeral_conv} + conv = fn phi => K numeral_conv} *} locale fieldgb = ringb + gb_field @@ -437,8 +437,16 @@ use "Tools/Groebner_Basis/groebner.ML" ML {* - fun algebra_tac ctxt i = ObjectLogic.full_atomize_tac i THEN (fn st => - rtac (Groebner.ring_conv ctxt (Thm.dest_arg (nth (cprems_of st) (i - 1)))) i st); + fun algebra_tac ctxt i = ObjectLogic.full_atomize_tac i + THEN (fn st => + case try (nth (cprems_of st)) (i - 1) of + NONE => no_tac st + | SOME p => let val th = Groebner.ring_conv ctxt (Thm.dest_arg p) + in rtac th i st end + handle TERM _ => no_tac st + handle THM _ => no_tac st + handle ERROR _ => no_tac st + handle CTERM _ => no_tac st); *} method_setup algebra = {* diff -r 0dbb30302259 -r 01c09922ce59 src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Mon Jun 11 18:28:15 2007 +0200 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Mon Jun 11 18:28:16 2007 +0200 @@ -739,7 +739,7 @@ NONE => reflexive form | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) => fst (ring_and_ideal_conv theory - dest_const (mk_const (Thm.ctyp_of_term tm)) ring_eq_conv - (semiring_normalize_wrapper res)) form)); + dest_const (mk_const (Thm.ctyp_of_term tm)) (ring_eq_conv ctxt) + (semiring_normalize_wrapper ctxt res)) form)); end; diff -r 0dbb30302259 -r 01c09922ce59 src/HOL/Tools/Groebner_Basis/normalizer.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Mon Jun 11 18:28:15 2007 +0200 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Mon Jun 11 18:28:16 2007 +0200 @@ -9,7 +9,7 @@ val mk_cnumeral : integer -> cterm val semiring_normalize_conv : Proof.context -> Conv.conv val semiring_normalize_tac : Proof.context -> int -> tactic - val semiring_normalize_wrapper : NormalizerData.entry -> Conv.conv + val semiring_normalize_wrapper : Proof.context -> NormalizerData.entry -> Conv.conv val semiring_normalizers_conv : cterm list -> cterm list * thm list -> cterm list * thm list -> (cterm -> bool) * Conv.conv * Conv.conv * Conv.conv -> (cterm -> Thm.cterm -> bool) -> @@ -622,7 +622,7 @@ val nat_exp_ss = HOL_basic_ss addsimps (nat_number @ nat_arith @ arith_simps @ rel_simps) addsimps [Let_def, if_False, if_True, add_0, add_Suc]; -fun semiring_normalize_wrapper ({vars, semiring, ring, idom}, +fun semiring_normalize_wrapper ctxt ({vars, semiring, ring, idom}, {conv, dest_const, mk_const, is_const}) = let fun ord t u = Term.term_ord (term_of t, term_of u) = LESS @@ -631,15 +631,15 @@ arg_conv (Simplifier.rewrite nat_exp_ss) then_conv Simplifier.rewrite (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34]) - then_conv conv - val dat = (is_const, conv, conv, pow_conv) + then_conv conv ctxt + val dat = (is_const, conv ctxt, conv ctxt, pow_conv) val {main, ...} = semiring_normalizers_conv vars semiring ring dat ord in main end; fun semiring_normalize_conv ctxt tm = (case NormalizerData.match ctxt tm of NONE => reflexive tm - | SOME res => semiring_normalize_wrapper res tm); + | SOME res => semiring_normalize_wrapper ctxt res tm); fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) => diff -r 0dbb30302259 -r 01c09922ce59 src/HOL/Tools/Groebner_Basis/normalizer_data.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Mon Jun 11 18:28:15 2007 +0200 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Mon Jun 11 18:28:16 2007 +0200 @@ -16,7 +16,7 @@ val funs: thm -> {is_const: morphism -> cterm -> bool, dest_const: morphism -> cterm -> Rat.rat, mk_const: morphism -> ctyp -> Rat.rat -> cterm, - conv: morphism -> cterm -> thm} -> morphism -> Context.generic -> Context.generic + conv: morphism -> Proof.context -> cterm -> thm} -> morphism -> Context.generic -> Context.generic val setup: theory -> theory end; @@ -33,7 +33,7 @@ {is_const: cterm -> bool, dest_const: cterm -> Rat.rat, mk_const: ctyp -> Rat.rat -> cterm, - conv: cterm -> thm}; + conv: Proof.context -> cterm -> thm}; val eq_key = Thm.eq_thm; fun eq_data arg = eq_fst eq_key arg;