# 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;