src/HOL/Groebner_Basis.thy
changeset 23330 01c09922ce59
parent 23327 1654013ec97c
child 23332 b91295432e6d
     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 = {*