Conversion for computation on constants now depends on the context
authorchaieb
Mon Jun 11 18:28:16 2007 +0200 (2007-06-11)
changeset 2333001c09922ce59
parent 23329 0dbb30302259
child 23331 da040caa0596
Conversion for computation on constants now depends on the context
src/HOL/Groebner_Basis.thy
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Groebner_Basis/normalizer.ML
src/HOL/Tools/Groebner_Basis/normalizer_data.ML
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Jun 11 18:28:15 2007 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Jun 11 18:28:16 2007 +0200
     1.3 @@ -209,7 +209,7 @@
     1.4            handle TERM _ => error "ring_dest_const")),
     1.5      mk_const = fn phi => fn cT => fn x =>
     1.6        Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
     1.7 -    conv = fn phi => numeral_conv}
     1.8 +    conv = fn phi => K numeral_conv}
     1.9  *}
    1.10  
    1.11  
    1.12 @@ -250,7 +250,7 @@
    1.13            handle TERM _ => error "ring_dest_const")),
    1.14      mk_const = fn phi => fn cT => fn x =>
    1.15        Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
    1.16 -    conv = fn phi => numeral_conv}
    1.17 +    conv = fn phi => K numeral_conv}
    1.18  *}
    1.19  
    1.20  use "Tools/Groebner_Basis/normalizer.ML"
    1.21 @@ -362,7 +362,7 @@
    1.22            handle TERM _ => error "ring_dest_const")),
    1.23      mk_const = fn phi => fn cT => fn x =>
    1.24        Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
    1.25 -    conv = fn phi => numeral_conv}
    1.26 +    conv = fn phi => K numeral_conv}
    1.27  *}
    1.28  
    1.29  
    1.30 @@ -397,7 +397,7 @@
    1.31            handle TERM _ => error "ring_dest_const")),
    1.32      mk_const = fn phi => fn cT => fn x =>
    1.33        Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
    1.34 -    conv = fn phi => numeral_conv}
    1.35 +    conv = fn phi => K numeral_conv}
    1.36  *}
    1.37  
    1.38  locale fieldgb = ringb + gb_field
    1.39 @@ -437,8 +437,16 @@
    1.40  use "Tools/Groebner_Basis/groebner.ML"
    1.41  
    1.42  ML {*
    1.43 -  fun algebra_tac ctxt i = ObjectLogic.full_atomize_tac i THEN (fn st =>
    1.44 -  rtac (Groebner.ring_conv ctxt (Thm.dest_arg (nth (cprems_of st) (i - 1)))) i st);
    1.45 +  fun algebra_tac ctxt i = ObjectLogic.full_atomize_tac i 
    1.46 +  THEN (fn st =>
    1.47 +   case try (nth (cprems_of st)) (i - 1) of
    1.48 +    NONE => no_tac st
    1.49 +  | SOME p => let val th = Groebner.ring_conv ctxt (Thm.dest_arg p)
    1.50 +              in rtac th i st end
    1.51 +              handle TERM _ => no_tac st
    1.52 +              handle THM _ => no_tac st
    1.53 +              handle ERROR _ => no_tac st
    1.54 +              handle CTERM _ => no_tac st);
    1.55  *}
    1.56  
    1.57  method_setup algebra = {*
     2.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Mon Jun 11 18:28:15 2007 +0200
     2.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Mon Jun 11 18:28:16 2007 +0200
     2.3 @@ -739,7 +739,7 @@
     2.4          NONE => reflexive form
     2.5        | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) =>
     2.6          fst (ring_and_ideal_conv theory
     2.7 -          dest_const (mk_const (Thm.ctyp_of_term tm)) ring_eq_conv
     2.8 -          (semiring_normalize_wrapper res)) form));
     2.9 +          dest_const (mk_const (Thm.ctyp_of_term tm)) (ring_eq_conv ctxt)
    2.10 +          (semiring_normalize_wrapper ctxt res)) form));
    2.11  
    2.12  end;
     3.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Mon Jun 11 18:28:15 2007 +0200
     3.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Mon Jun 11 18:28:16 2007 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4   val mk_cnumeral : integer -> cterm
     3.5   val semiring_normalize_conv : Proof.context -> Conv.conv
     3.6   val semiring_normalize_tac : Proof.context -> int -> tactic
     3.7 - val semiring_normalize_wrapper :  NormalizerData.entry -> Conv.conv
     3.8 + val semiring_normalize_wrapper :  Proof.context -> NormalizerData.entry -> Conv.conv
     3.9   val semiring_normalizers_conv :
    3.10       cterm list -> cterm list * thm list -> cterm list * thm list ->
    3.11       (cterm -> bool) * Conv.conv * Conv.conv * Conv.conv -> (cterm -> Thm.cterm -> bool) ->
    3.12 @@ -622,7 +622,7 @@
    3.13  val nat_exp_ss = HOL_basic_ss addsimps (nat_number @ nat_arith @ arith_simps @ rel_simps)
    3.14                                addsimps [Let_def, if_False, if_True, add_0, add_Suc];
    3.15  
    3.16 -fun semiring_normalize_wrapper ({vars, semiring, ring, idom}, 
    3.17 +fun semiring_normalize_wrapper ctxt ({vars, semiring, ring, idom}, 
    3.18                                       {conv, dest_const, mk_const, is_const}) =
    3.19    let
    3.20      fun ord t u = Term.term_ord (term_of t, term_of u) = LESS
    3.21 @@ -631,15 +631,15 @@
    3.22        arg_conv (Simplifier.rewrite nat_exp_ss)
    3.23        then_conv Simplifier.rewrite
    3.24          (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
    3.25 -      then_conv conv
    3.26 -    val dat = (is_const, conv, conv, pow_conv)
    3.27 +      then_conv conv ctxt
    3.28 +    val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
    3.29      val {main, ...} = semiring_normalizers_conv vars semiring ring dat ord
    3.30    in main end;
    3.31  
    3.32  fun semiring_normalize_conv ctxt tm =
    3.33    (case NormalizerData.match ctxt tm of
    3.34      NONE => reflexive tm
    3.35 -  | SOME res => semiring_normalize_wrapper res tm);
    3.36 +  | SOME res => semiring_normalize_wrapper ctxt res tm);
    3.37  
    3.38  
    3.39  fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) =>
     4.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Mon Jun 11 18:28:15 2007 +0200
     4.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Mon Jun 11 18:28:16 2007 +0200
     4.3 @@ -16,7 +16,7 @@
     4.4    val funs: thm -> {is_const: morphism -> cterm -> bool,
     4.5      dest_const: morphism -> cterm -> Rat.rat,
     4.6      mk_const: morphism -> ctyp -> Rat.rat -> cterm,
     4.7 -    conv: morphism -> cterm -> thm} -> morphism -> Context.generic -> Context.generic
     4.8 +    conv: morphism -> Proof.context -> cterm -> thm} -> morphism -> Context.generic -> Context.generic
     4.9    val setup: theory -> theory
    4.10  end;
    4.11  
    4.12 @@ -33,7 +33,7 @@
    4.13   {is_const: cterm -> bool,
    4.14    dest_const: cterm -> Rat.rat,
    4.15    mk_const: ctyp -> Rat.rat -> cterm,
    4.16 -  conv: cterm -> thm};
    4.17 +  conv: Proof.context -> cterm -> thm};
    4.18  
    4.19  val eq_key = Thm.eq_thm;
    4.20  fun eq_data arg = eq_fst eq_key arg;