src/HOL/Groebner_Basis.thy
changeset 23573 d85a277f90fd
parent 23477 f4b83f03cac9
child 25250 b3a485b98963
     1.1 --- a/src/HOL/Groebner_Basis.thy	Thu Jul 05 00:06:09 2007 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Jul 05 00:06:10 2007 +0200
     1.3 @@ -185,33 +185,39 @@
     1.4  lemmas semiring_norm = comp_arith
     1.5  
     1.6  ML {*
     1.7 -  fun numeral_is_const ct =
     1.8 -    can HOLogic.dest_number (Thm.term_of ct);
     1.9 +local
    1.10  
    1.11 -  val numeral_conv =
    1.12 -    Conv.then_conv (Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}),
    1.13 -   Simplifier.rewrite (HOL_basic_ss addsimps
    1.14 -  [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}));
    1.15 -*}
    1.16 +open Conv;
    1.17 +
    1.18 +fun numeral_is_const ct =
    1.19 +  can HOLogic.dest_number (Thm.term_of ct);
    1.20  
    1.21 -ML {*
    1.22 -  fun int_of_rat x =
    1.23 -    (case Rat.quotient_of_rat x of (i, 1) => i
    1.24 -    | _ => error "int_of_rat: bad int")
    1.25 -*}
    1.26 +fun int_of_rat x =
    1.27 +  (case Rat.quotient_of_rat x of (i, 1) => i
    1.28 +  | _ => error "int_of_rat: bad int");
    1.29  
    1.30 -declaration {*
    1.31 -  NormalizerData.funs @{thm class_semiring.axioms}
    1.32 +val numeral_conv =
    1.33 +  Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}) then_conv
    1.34 +  Simplifier.rewrite (HOL_basic_ss addsimps
    1.35 +    (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}));
    1.36 +
    1.37 +in
    1.38 +
    1.39 +fun normalizer_funs key =
    1.40 +  NormalizerData.funs key
    1.41     {is_const = fn phi => numeral_is_const,
    1.42      dest_const = fn phi => fn ct =>
    1.43        Rat.rat_of_int (snd
    1.44          (HOLogic.dest_number (Thm.term_of ct)
    1.45            handle TERM _ => error "ring_dest_const")),
    1.46 -    mk_const = fn phi => fn cT => fn x =>
    1.47 -      Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
    1.48 +    mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT (int_of_rat x),
    1.49      conv = fn phi => K numeral_conv}
    1.50 +
    1.51 +end
    1.52  *}
    1.53  
    1.54 +declaration {* normalizer_funs @{thm class_semiring.axioms} *}
    1.55 +
    1.56  
    1.57  locale gb_ring = gb_semiring +
    1.58    fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.59 @@ -241,17 +247,7 @@
    1.60    by unfold_locales simp_all
    1.61  
    1.62  
    1.63 -declaration {*
    1.64 -  NormalizerData.funs @{thm class_ring.axioms}
    1.65 -   {is_const = fn phi => numeral_is_const,
    1.66 -    dest_const = fn phi => fn ct =>
    1.67 -      Rat.rat_of_int (snd
    1.68 -        (HOLogic.dest_number (Thm.term_of ct)
    1.69 -          handle TERM _ => error "ring_dest_const")),
    1.70 -    mk_const = fn phi => fn cT => fn x =>
    1.71 -      Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
    1.72 -    conv = fn phi => K numeral_conv}
    1.73 -*}
    1.74 +declaration {* normalizer_funs @{thm class_ring.axioms} *}
    1.75  
    1.76  use "Tools/Groebner_Basis/normalizer.ML"
    1.77  
    1.78 @@ -354,17 +350,7 @@
    1.79  qed
    1.80  
    1.81  
    1.82 -declaration {*
    1.83 -  NormalizerData.funs @{thm class_ringb.axioms}
    1.84 -   {is_const = fn phi => numeral_is_const,
    1.85 -    dest_const = fn phi => fn ct =>
    1.86 -      Rat.rat_of_int (snd
    1.87 -        (HOLogic.dest_number (Thm.term_of ct)
    1.88 -          handle TERM _ => error "ring_dest_const")),
    1.89 -    mk_const = fn phi => fn cT => fn x =>
    1.90 -      Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
    1.91 -    conv = fn phi => K numeral_conv}
    1.92 -*}
    1.93 +declaration {* normalizer_funs @{thm class_ringb.axioms} *}
    1.94  
    1.95  interpretation natgb: semiringb
    1.96    ["op +" "op *" "op ^" "0::nat" "1"]
    1.97 @@ -388,17 +374,7 @@
    1.98    thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
    1.99  qed
   1.100  
   1.101 -declaration {*
   1.102 -  NormalizerData.funs @{thm natgb.axioms}
   1.103 -   {is_const = fn phi => numeral_is_const,
   1.104 -    dest_const = fn phi => fn ct =>
   1.105 -      Rat.rat_of_int (snd
   1.106 -        (HOLogic.dest_number (Thm.term_of ct)
   1.107 -          handle TERM _ => error "ring_dest_const")),
   1.108 -    mk_const = fn phi => fn cT => fn x =>
   1.109 -      Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
   1.110 -    conv = fn phi => K numeral_conv}
   1.111 -*}
   1.112 +declaration {* normalizer_funs @{thm natgb.axioms} *}
   1.113  
   1.114  locale fieldgb = ringb + gb_field
   1.115  begin
   1.116 @@ -448,7 +424,7 @@
   1.117      ((Scan.optional (keyword addN |-- thms) []) -- 
   1.118      (Scan.optional (keyword delN |-- thms) [])) src 
   1.119   #> (fn ((add_ths, del_ths), ctxt) => 
   1.120 -       Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
   1.121 +       Method.SIMPLE_METHOD' (Groebner.ring_tac add_ths del_ths ctxt))
   1.122  end
   1.123  *} "solve polynomial equations over (semi)rings using Groebner bases"
   1.124