Export a wrapper for all semiring_normalizers
authorchaieb
Mon Jun 16 11:47:46 2008 +0200 (2008-06-16)
changeset 27222b08abdb8f499
parent 27221 31328dc30196
child 27223 8546e2407b31
Export a wrapper for all semiring_normalizers
src/HOL/Tools/Groebner_Basis/normalizer.ML
     1.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Sat Jun 14 23:52:51 2008 +0200
     1.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Mon Jun 16 11:47:46 2008 +0200
     1.3 @@ -9,6 +9,9 @@
     1.4   val semiring_normalize_ord_conv : Proof.context -> (cterm -> cterm -> bool) -> conv
     1.5   val semiring_normalize_tac : Proof.context -> int -> tactic
     1.6   val semiring_normalize_wrapper :  Proof.context -> NormalizerData.entry -> conv
     1.7 + val semiring_normalizers_ord_wrapper :  
     1.8 +     Proof.context -> NormalizerData.entry -> (cterm -> cterm -> bool) ->
     1.9 +      {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    1.10   val semiring_normalize_ord_wrapper :  Proof.context -> NormalizerData.entry ->
    1.11     (cterm -> cterm -> bool) -> conv
    1.12   val semiring_normalizers_conv :
    1.13 @@ -613,7 +616,8 @@
    1.14                                addsimps [Let_def, if_False, if_True, @{thm add_0}, @{thm add_Suc}];
    1.15  
    1.16  fun simple_cterm_ord t u = Term.term_ord (term_of t, term_of u) = LESS;
    1.17 -fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, 
    1.18 +
    1.19 +fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, 
    1.20                                       {conv, dest_const, mk_const, is_const}) ord =
    1.21    let
    1.22      val pow_conv =
    1.23 @@ -622,8 +626,10 @@
    1.24          (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
    1.25        then_conv conv ctxt
    1.26      val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
    1.27 -    val {main, ...} = semiring_normalizers_conv vars semiring ring dat ord
    1.28 -  in main end;
    1.29 +  in semiring_normalizers_conv vars semiring ring dat ord end;
    1.30 +
    1.31 +fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
    1.32 + #main (semiring_normalizers_ord_wrapper ctxt ({vars = vars, semiring = semiring, ring = ring, idom = idom, ideal = ideal},{conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord);
    1.33  
    1.34  fun semiring_normalize_wrapper ctxt data = 
    1.35    semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;