Semiring normalization and Groebner Bases.
authorwenzelm
Tue Jun 05 16:26:04 2007 +0200 (2007-06-05)
changeset 2325267268bb40b21
parent 23251 471b576aad25
child 23253 b1f3f53c60b5
Semiring normalization and Groebner Bases.
CONTRIBUTORS
src/HOL/Groebner_Basis.thy
src/HOL/IsaMakefile
src/HOL/NatSimprocs.thy
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Groebner_Basis/misc.ML
src/HOL/Tools/Groebner_Basis/normalizer.ML
src/HOL/Tools/Groebner_Basis/normalizer_data.ML
     1.1 --- a/CONTRIBUTORS	Tue Jun 05 15:17:02 2007 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Jun 05 16:26:04 2007 +0200
     1.3 @@ -1,6 +1,9 @@
     1.4  
     1.5 -Contributions to Isabelle
     1.6 --------------------------
     1.7 +Contributions to Isabelle 2007
     1.8 +------------------------------
     1.9 +
    1.10 +* June 2007: Amine Chaieb, TUM
    1.11 +  Semiring normalization and Groebner Bases
    1.12  
    1.13  * 2006/2007: Florian Haftmann, TUM
    1.14    Pure: generic code generator framework.
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Jun 05 16:26:04 2007 +0200
     2.3 @@ -0,0 +1,416 @@
     2.4 +(*  Title:      HOL/Groebner_Basis.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Amine Chaieb, TU Muenchen
     2.7 +*)
     2.8 +
     2.9 +header {* Semiring normalization and Groebner Bases *}
    2.10 +
    2.11 +theory Groebner_Basis
    2.12 +imports NatBin
    2.13 +uses
    2.14 +  "Tools/Groebner_Basis/misc.ML"
    2.15 +  "Tools/Groebner_Basis/normalizer_data.ML"
    2.16 +  ("Tools/Groebner_Basis/normalizer.ML")
    2.17 +begin
    2.18 +
    2.19 +subsection {* Semiring normalization *}
    2.20 +
    2.21 +setup NormalizerData.setup
    2.22 +
    2.23 +
    2.24 +locale semiring =
    2.25 +  fixes add mul pwr r0 r1
    2.26 +  assumes add_a:"(add x (add y z) = add (add x y) z)"
    2.27 +    and add_c: "add x y = add y x" and add_0:"add r0 x = x"
    2.28 +    and mul_a:"mul x (mul y z) = mul (mul x y) z" and mul_c:"mul x y = mul y x"
    2.29 +    and mul_1:"mul r1 x = x" and  mul_0:"mul r0 x = r0"
    2.30 +    and mul_d:"mul x (add y z) = add (mul x y) (mul x z)"
    2.31 +    and pwr_0:"pwr x 0 = r1" and pwr_Suc:"pwr x (Suc n) = mul x (pwr x n)"
    2.32 +begin
    2.33 +
    2.34 +lemma mul_pwr:"mul (pwr x p) (pwr x q) = pwr x (p + q)"
    2.35 +proof (induct p)
    2.36 +  case 0
    2.37 +  then show ?case by (auto simp add: pwr_0 mul_1)
    2.38 +next
    2.39 +  case Suc
    2.40 +  from this [symmetric] show ?case
    2.41 +    by (auto simp add: pwr_Suc mul_1 mul_a)
    2.42 +qed
    2.43 +
    2.44 +lemma pwr_mul: "pwr (mul x y) q = mul (pwr x q) (pwr y q)"
    2.45 +proof (induct q arbitrary: x y, auto simp add:pwr_0 pwr_Suc mul_1)
    2.46 +  fix q x y
    2.47 +  assume "\<And>x y. pwr (mul x y) q = mul (pwr x q) (pwr y q)"
    2.48 +  have "mul (mul x y) (mul (pwr x q) (pwr y q)) = mul x (mul y (mul (pwr x q) (pwr y q)))"
    2.49 +    by (simp add: mul_a)
    2.50 +  also have "\<dots> = (mul (mul y (mul (pwr y q) (pwr x q))) x)" by (simp add: mul_c)
    2.51 +  also have "\<dots> = (mul (mul y (pwr y q)) (mul (pwr x q) x))" by (simp add: mul_a)
    2.52 +  finally show "mul (mul x y) (mul (pwr x q) (pwr y q)) =
    2.53 +    mul (mul x (pwr x q)) (mul y (pwr y q))" by (simp add: mul_c)
    2.54 +qed
    2.55 +
    2.56 +lemma pwr_pwr: "pwr (pwr x p) q = pwr x (p * q)"
    2.57 +proof (induct p arbitrary: q)
    2.58 +  case 0
    2.59 +  show ?case using pwr_Suc mul_1 pwr_0 by (induct q) auto
    2.60 +next
    2.61 +  case Suc
    2.62 +  thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc)
    2.63 +qed
    2.64 +
    2.65 +
    2.66 +subsubsection {* Declaring the abstract theory *}
    2.67 +
    2.68 +lemma semiring_ops:
    2.69 +  includes meta_term_syntax
    2.70 +  shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
    2.71 +    and "TERM r0" and "TERM r1"
    2.72 +  by rule+
    2.73 +
    2.74 +lemma semiring_rules:
    2.75 +  "add (mul a m) (mul b m) = mul (add a b) m"
    2.76 +  "add (mul a m) m = mul (add a r1) m"
    2.77 +  "add m (mul a m) = mul (add a r1) m"
    2.78 +  "add m m = mul (add r1 r1) m"
    2.79 +  "add r0 a = a"
    2.80 +  "add a r0 = a"
    2.81 +  "mul a b = mul b a"
    2.82 +  "mul (add a b) c = add (mul a c) (mul b c)"
    2.83 +  "mul r0 a = r0"
    2.84 +  "mul a r0 = r0"
    2.85 +  "mul r1 a = a"
    2.86 +  "mul a r1 = a"
    2.87 +  "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)"
    2.88 +  "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))"
    2.89 +  "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)"
    2.90 +  "mul (mul lx ly) rx = mul (mul lx rx) ly"
    2.91 +  "mul (mul lx ly) rx = mul lx (mul ly rx)"
    2.92 +  "mul lx (mul rx ry) = mul (mul lx rx) ry"
    2.93 +  "mul lx (mul rx ry) = mul rx (mul lx ry)"
    2.94 +  "add (add a b) (add c d) = add (add a c) (add b d)"
    2.95 +  "add (add a b) c = add a (add b c)"
    2.96 +  "add a (add c d) = add c (add a d)"
    2.97 +  "add (add a b) c = add (add a c) b"
    2.98 +  "add a c = add c a"
    2.99 +  "add a (add c d) = add (add a c) d"
   2.100 +  "mul (pwr x p) (pwr x q) = pwr x (p + q)"
   2.101 +  "mul x (pwr x q) = pwr x (Suc q)"
   2.102 +  "mul (pwr x q) x = pwr x (Suc q)"
   2.103 +  "mul x x = pwr x 2"
   2.104 +  "pwr (mul x y) q = mul (pwr x q) (pwr y q)"
   2.105 +  "pwr (pwr x p) q = pwr x (p * q)"
   2.106 +  "pwr x 0 = r1"
   2.107 +  "pwr x 1 = x"
   2.108 +  "mul x (add y z) = add (mul x y) (mul x z)"
   2.109 +  "pwr x (Suc q) = mul x (pwr x q)"
   2.110 +  "pwr x (2*n) = mul (pwr x n) (pwr x n)"
   2.111 +  "pwr x (Suc (2*n)) = mul x (mul (pwr x n) (pwr x n))"
   2.112 +proof -
   2.113 +  show "add (mul a m) (mul b m) = mul (add a b) m" using mul_d mul_c by simp
   2.114 +next show"add (mul a m) m = mul (add a r1) m" using mul_d mul_c mul_1 by simp
   2.115 +next show "add m (mul a m) = mul (add a r1) m" using mul_c mul_d mul_1 add_c by simp
   2.116 +next show "add m m = mul (add r1 r1) m" using mul_c mul_d mul_1 by simp
   2.117 +next show "add r0 a = a" using add_0 by simp
   2.118 +next show "add a r0 = a" using add_0 add_c by simp
   2.119 +next show "mul a b = mul b a" using mul_c by simp
   2.120 +next show "mul (add a b) c = add (mul a c) (mul b c)" using mul_c mul_d by simp
   2.121 +next show "mul r0 a = r0" using mul_0 by simp
   2.122 +next show "mul a r0 = r0" using mul_0 mul_c by simp
   2.123 +next show "mul r1 a = a" using mul_1 by simp
   2.124 +next show "mul a r1 = a" using mul_1 mul_c by simp
   2.125 +next show "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)"
   2.126 +    using mul_c mul_a by simp
   2.127 +next show "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))"
   2.128 +    using mul_a by simp
   2.129 +next
   2.130 +  have "mul (mul lx ly) (mul rx ry) = mul (mul rx ry) (mul lx ly)" by (rule mul_c)
   2.131 +  also have "\<dots> = mul rx (mul ry (mul lx ly))" using mul_a by simp
   2.132 +  finally
   2.133 +  show "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)"
   2.134 +    using mul_c by simp
   2.135 +next show "mul (mul lx ly) rx = mul (mul lx rx) ly" using mul_c mul_a by simp
   2.136 +next
   2.137 +  show "mul (mul lx ly) rx = mul lx (mul ly rx)" by (simp add: mul_a)
   2.138 +next show "mul lx (mul rx ry) = mul (mul lx rx) ry" by (simp add: mul_a )
   2.139 +next show "mul lx (mul rx ry) = mul rx (mul lx ry)" by (simp add: mul_a,simp add: mul_c)
   2.140 +next show "add (add a b) (add c d) = add (add a c) (add b d)"
   2.141 +    using add_c add_a by simp
   2.142 +next show "add (add a b) c = add a (add b c)" using add_a by simp
   2.143 +next show "add a (add c d) = add c (add a d)"
   2.144 +    apply (simp add: add_a) by (simp only: add_c)
   2.145 +next show "add (add a b) c = add (add a c) b" using add_a add_c by simp
   2.146 +next show "add a c = add c a" by (rule add_c)
   2.147 +next show "add a (add c d) = add (add a c) d" using add_a by simp
   2.148 +next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr)
   2.149 +next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp
   2.150 +next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp
   2.151 +next show "mul x x = pwr x 2" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
   2.152 +next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
   2.153 +next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
   2.154 +next show "pwr x 0 = r1" using pwr_0 .
   2.155 +next show "pwr x 1 = x" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
   2.156 +next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
   2.157 +next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
   2.158 +next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number mul_pwr)
   2.159 +next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))"
   2.160 +    by (simp add: nat_number pwr_Suc mul_pwr)
   2.161 +qed
   2.162 +
   2.163 +
   2.164 +lemma "axioms" [normalizer
   2.165 +    semiring ops: semiring_ops
   2.166 +    semiring rules: semiring_rules]:
   2.167 +  "semiring add mul pwr r0 r1" .
   2.168 +
   2.169 +end
   2.170 +
   2.171 +interpretation class_semiring: semiring
   2.172 +    ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
   2.173 +  by unfold_locales (auto simp add: ring_eq_simps power_Suc)
   2.174 +
   2.175 +lemmas nat_arith =
   2.176 +  add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
   2.177 +
   2.178 +lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
   2.179 +  by (simp add: numeral_1_eq_1)
   2.180 +lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False
   2.181 +  if_True add_0 add_Suc add_number_of_left mult_number_of_left
   2.182 +  numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
   2.183 +  numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1
   2.184 +  iszero_number_of_1 iszero_number_of_0 nonzero_number_of_Min
   2.185 +  iszero_number_of_Pls iszero_0 not_iszero_Numeral1
   2.186 +
   2.187 +lemmas semiring_norm = comp_arith
   2.188 +
   2.189 +ML {*
   2.190 +  fun numeral_is_const ct =
   2.191 +    can HOLogic.dest_number (Thm.term_of ct);
   2.192 +
   2.193 +  val numeral_conv =
   2.194 +    Conv.then_conv (Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}),
   2.195 +   Simplifier.rewrite (HOL_basic_ss addsimps
   2.196 +  [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}));
   2.197 +*}
   2.198 +
   2.199 +ML {*
   2.200 +  fun int_of_rat x =
   2.201 +    (case Rat.quotient_of_rat x of (i, 1) => i
   2.202 +    | _ => error "int_of_rat: bad int")
   2.203 +*}
   2.204 +
   2.205 +declaration {*
   2.206 +  NormalizerData.funs @{thm class_semiring.axioms}
   2.207 +   {is_const = fn phi => numeral_is_const,
   2.208 +    dest_const = fn phi => fn ct =>
   2.209 +      Rat.rat_of_int (snd
   2.210 +        (HOLogic.dest_number (Thm.term_of ct)
   2.211 +          handle TERM _ => error "ring_dest_const")),
   2.212 +    mk_const = fn phi => fn cT => fn x =>
   2.213 +      Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
   2.214 +    conv = fn phi => numeral_conv}
   2.215 +*}
   2.216 +
   2.217 +
   2.218 +locale ring = semiring +
   2.219 +  fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   2.220 +    and neg :: "'a \<Rightarrow> 'a"
   2.221 +  assumes neg_mul: "neg x = mul (neg r1) x"
   2.222 +    and sub_add: "sub x y = add x (neg y)"
   2.223 +begin
   2.224 +
   2.225 +lemma ring_ops:
   2.226 +  includes meta_term_syntax
   2.227 +  shows "TERM (sub x y)" and "TERM (neg x)" .
   2.228 +
   2.229 +lemmas ring_rules = neg_mul sub_add
   2.230 +
   2.231 +lemma "axioms" [normalizer
   2.232 +  semiring ops: semiring_ops
   2.233 +  semiring rules: semiring_rules
   2.234 +  ring ops: ring_ops
   2.235 +  ring rules: ring_rules]:
   2.236 +  "ring add mul pwr r0 r1 sub neg" .
   2.237 +
   2.238 +end
   2.239 +
   2.240 +
   2.241 +interpretation class_ring: ring ["op +" "op *" "op ^"
   2.242 +    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
   2.243 +  by unfold_locales simp_all
   2.244 +
   2.245 +
   2.246 +declaration {*
   2.247 +  NormalizerData.funs @{thm class_ring.axioms}
   2.248 +   {is_const = fn phi => numeral_is_const,
   2.249 +    dest_const = fn phi => fn ct =>
   2.250 +      Rat.rat_of_int (snd
   2.251 +        (HOLogic.dest_number (Thm.term_of ct)
   2.252 +          handle TERM _ => error "ring_dest_const")),
   2.253 +    mk_const = fn phi => fn cT => fn x =>
   2.254 +      Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
   2.255 +    conv = fn phi => numeral_conv}
   2.256 +*}
   2.257 +
   2.258 +use "Tools/Groebner_Basis/normalizer.ML"
   2.259 +
   2.260 +method_setup sring_norm = {*
   2.261 +  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt))
   2.262 +*} "Semiring_normalizer"
   2.263 +
   2.264 +
   2.265 +subsection {* Gröbner Bases *}
   2.266 +
   2.267 +locale semiringb = semiring +
   2.268 +  assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z"
   2.269 +  and add_mul_solve: "add (mul w y) (mul x z) =
   2.270 +    add (mul w z) (mul x y) \<longleftrightarrow> w = x \<or> y = z"
   2.271 +begin
   2.272 +
   2.273 +lemma noteq_reduce: "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
   2.274 +proof-
   2.275 +  have "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> \<not> (a = b \<or> c = d)" by simp
   2.276 +  also have "\<dots> \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
   2.277 +    using add_mul_solve by blast
   2.278 +  finally show "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
   2.279 +    by simp
   2.280 +qed
   2.281 +
   2.282 +lemma add_scale_eq_noteq: "\<lbrakk>r \<noteq> r0 ; (a = b) \<and> ~(c = d)\<rbrakk>
   2.283 +  \<Longrightarrow> add a (mul r c) \<noteq> add b (mul r d)"
   2.284 +proof(clarify)
   2.285 +  assume nz: "r\<noteq> r0" and cnd: "c\<noteq>d"
   2.286 +    and eq: "add b (mul r c) = add b (mul r d)"
   2.287 +  hence "mul r c = mul r d" using cnd add_cancel by simp
   2.288 +  hence "add (mul r0 d) (mul r c) = add (mul r0 c) (mul r d)"
   2.289 +    using mul_0 add_cancel by simp
   2.290 +  thus "False" using add_mul_solve nz cnd by simp
   2.291 +qed
   2.292 +
   2.293 +declare "axioms" [normalizer del]
   2.294 +
   2.295 +lemma "axioms" [normalizer
   2.296 +  semiring ops: semiring_ops
   2.297 +  semiring rules: semiring_rules
   2.298 +  idom rules: noteq_reduce add_scale_eq_noteq]:
   2.299 +  "semiringb add mul pwr r0 r1" .
   2.300 +
   2.301 +end
   2.302 +
   2.303 +locale ringb = semiringb + ring
   2.304 +begin
   2.305 +
   2.306 +declare "axioms" [normalizer del]
   2.307 +
   2.308 +lemma "axioms" [normalizer
   2.309 +  semiring ops: semiring_ops
   2.310 +  semiring rules: semiring_rules
   2.311 +  ring ops: ring_ops
   2.312 +  ring rules: ring_rules
   2.313 +  idom rules: noteq_reduce add_scale_eq_noteq]:
   2.314 +  "ringb add mul pwr r0 r1 sub neg" .
   2.315 +
   2.316 +end
   2.317 +
   2.318 +lemma no_zero_divirors_neq0:
   2.319 +  assumes az: "(a::'a::no_zero_divisors) \<noteq> 0"
   2.320 +    and ab: "a*b = 0" shows "b = 0"
   2.321 +proof -
   2.322 +  { assume bz: "b \<noteq> 0"
   2.323 +    from no_zero_divisors [OF az bz] ab have False by blast }
   2.324 +  thus "b = 0" by blast
   2.325 +qed
   2.326 +
   2.327 +interpretation class_ringb: ringb
   2.328 +  ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"]
   2.329 +proof(unfold_locales, simp add: ring_eq_simps power_Suc, auto)
   2.330 +  fix w x y z ::"'a::{idom,recpower,number_ring}"
   2.331 +  assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
   2.332 +  hence ynz': "y - z \<noteq> 0" by simp
   2.333 +  from p have "w * y + x* z - w*z - x*y = 0" by simp
   2.334 +  hence "w* (y - z) - x * (y - z) = 0" by (simp add: ring_eq_simps)
   2.335 +  hence "(y - z) * (w - x) = 0" by (simp add: ring_eq_simps)
   2.336 +  with  no_zero_divirors_neq0 [OF ynz']
   2.337 +  have "w - x = 0" by blast
   2.338 +  thus "w = x"  by simp
   2.339 +qed
   2.340 +
   2.341 +
   2.342 +declaration {*
   2.343 +  NormalizerData.funs @{thm class_ringb.axioms}
   2.344 +   {is_const = fn phi => numeral_is_const,
   2.345 +    dest_const = fn phi => fn ct =>
   2.346 +      Rat.rat_of_int (snd
   2.347 +        (HOLogic.dest_number (Thm.term_of ct)
   2.348 +          handle TERM _ => error "ring_dest_const")),
   2.349 +    mk_const = fn phi => fn cT => fn x =>
   2.350 +      Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
   2.351 +    conv = fn phi => numeral_conv}
   2.352 +*}
   2.353 +
   2.354 +
   2.355 +interpretation natgb: semiringb
   2.356 +  ["op +" "op *" "op ^" "0::nat" "1"]
   2.357 +proof (unfold_locales, simp add: ring_eq_simps power_Suc)
   2.358 +  fix w x y z ::"nat"
   2.359 +  { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
   2.360 +    hence "y < z \<or> y > z" by arith
   2.361 +    moreover {
   2.362 +      assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto)
   2.363 +      then obtain k where kp: "k>0" and yz:"z = y + k" by blast
   2.364 +      from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz ring_eq_simps)
   2.365 +      hence "x*k = w*k" by simp
   2.366 +      hence "w = x" using kp by (simp add: mult_cancel2) }
   2.367 +    moreover {
   2.368 +      assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto)
   2.369 +      then obtain k where kp: "k>0" and yz:"y = z + k" by blast
   2.370 +      from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz ring_eq_simps)
   2.371 +      hence "w*k = x*k" by simp
   2.372 +      hence "w = x" using kp by (simp add: mult_cancel2)}
   2.373 +    ultimately have "w=x" by blast }
   2.374 +  thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
   2.375 +qed
   2.376 +
   2.377 +declaration {*
   2.378 +  NormalizerData.funs @{thm natgb.axioms}
   2.379 +   {is_const = fn phi => numeral_is_const,
   2.380 +    dest_const = fn phi => fn ct =>
   2.381 +      Rat.rat_of_int (snd
   2.382 +        (HOLogic.dest_number (Thm.term_of ct)
   2.383 +          handle TERM _ => error "ring_dest_const")),
   2.384 +    mk_const = fn phi => fn cT => fn x =>
   2.385 +      Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
   2.386 +    conv = fn phi => numeral_conv}
   2.387 +*}
   2.388 +
   2.389 +
   2.390 +lemmas bool_simps =  simp_thms(1-34)
   2.391 +lemma dnf:
   2.392 +    "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
   2.393 +    "(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"
   2.394 +  by blast+
   2.395 +
   2.396 +lemmas weak_dnf_simps = dnf bool_simps
   2.397 +
   2.398 +lemma nnf_simps:
   2.399 +    "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
   2.400 +    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
   2.401 +  by blast+
   2.402 +
   2.403 +lemma PFalse:
   2.404 +    "P \<equiv> False \<Longrightarrow> \<not> P"
   2.405 +    "\<not> P \<Longrightarrow> (P \<equiv> False)"
   2.406 +  by auto
   2.407 +
   2.408 +use "Tools/Groebner_Basis/groebner.ML"
   2.409 +
   2.410 +ML {*
   2.411 +  fun algebra_tac ctxt i = ObjectLogic.full_atomize_tac i THEN (fn st =>
   2.412 +  rtac (Groebner.ring_conv ctxt (Thm.dest_arg (nth (cprems_of st) (i - 1)))) i st);
   2.413 +*}
   2.414 +
   2.415 +method_setup algebra = {*
   2.416 +  Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac)
   2.417 +*} ""
   2.418 +
   2.419 +end
     3.1 --- a/src/HOL/IsaMakefile	Tue Jun 05 15:17:02 2007 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Tue Jun 05 16:26:04 2007 +0200
     3.3 @@ -85,23 +85,28 @@
     3.4    ATP_Linkup.thy Accessible_Part.thy Datatype.thy	\
     3.5    Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.thy		\
     3.6    FixedPoint.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy		\
     3.7 -  Inductive.thy IntArith.thy IntDef.thy IntDiv.thy Lattices.thy List.thy\
     3.8 -  Main.thy Map.thy Nat.ML Nat.thy NatBin.thy NatSimprocs.thy Numeral.thy\
     3.9 -  OrderedGroup.thy Orderings.thy Power.thy PreList.thy Predicate.thy	\
    3.10 -  Presburger.thy Product_Type.thy ROOT.ML Recdef.thy Record.thy		\
    3.11 -  Refute.thy Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy	\
    3.12 -  Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/reduce_axiomsN.ML	\
    3.13 -  Tools/ATP/watcher.ML Tools/Presburger/cooper_dec.ML			\
    3.14 -  Tools/Presburger/cooper_proof.ML Tools/Presburger/presburger.ML	\
    3.15 -  Tools/Presburger/qelim.ML Tools/Presburger/reflected_cooper.ML	\
    3.16 +  Inductive.thy IntArith.thy IntDef.thy IntDiv.thy Lattices.thy 	\
    3.17 +  List.thy Main.thy Map.thy Nat.ML Nat.thy NatBin.thy NatSimprocs.thy 	\
    3.18 +  Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy 	\
    3.19 +  Predicate.thy Presburger.thy Product_Type.thy ROOT.ML Recdef.thy	\
    3.20 +  Record.thy Refute.thy Relation.thy Relation_Power.thy			\
    3.21 +  Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy	\
    3.22 +  Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML			\
    3.23 +  Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML		\
    3.24 +  Tools/Groebner_Basis/normalizer.ML					\
    3.25 +  Tools/Groebner_Basis/normalizer_data.ML				\
    3.26 +  Tools/Presburger/cooper_dec.ML Tools/Presburger/cooper_proof.ML	\
    3.27 +  Tools/Presburger/presburger.ML Tools/Presburger/qelim.ML		\
    3.28 +  Tools/Presburger/reflected_cooper.ML					\
    3.29    Tools/Presburger/reflected_presburger.ML Tools/TFL/dcterm.ML		\
    3.30    Tools/TFL/post.ML Tools/TFL/rules.ML Tools/TFL/tfl.ML			\
    3.31    Tools/TFL/thms.ML Tools/TFL/thry.ML Tools/TFL/usyntax.ML		\
    3.32    Tools/TFL/utils.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML	\
    3.33 -  Tools/datatype_aux.ML Tools/datatype_case.ML Tools/datatype_codegen.ML\
    3.34 -  Tools/datatype_hooks.ML Tools/datatype_package.ML			\
    3.35 -  Tools/datatype_prop.ML Tools/datatype_realizer.ML			\
    3.36 -  Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML	\
    3.37 +  Tools/datatype_aux.ML Tools/datatype_case.ML				\
    3.38 +  Tools/datatype_codegen.ML Tools/datatype_hooks.ML			\
    3.39 +  Tools/datatype_package.ML Tools/datatype_prop.ML			\
    3.40 +  Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML		\
    3.41 +  Tools/function_package/auto_term.ML					\
    3.42    Tools/function_package/context_tree.ML				\
    3.43    Tools/function_package/fundef_common.ML				\
    3.44    Tools/function_package/fundef_core.ML					\
     4.1 --- a/src/HOL/NatSimprocs.thy	Tue Jun 05 15:17:02 2007 +0200
     4.2 +++ b/src/HOL/NatSimprocs.thy	Tue Jun 05 16:26:04 2007 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  header {*Simprocs for the Naturals*}
     4.5  
     4.6  theory NatSimprocs
     4.7 -imports NatBin
     4.8 +imports Groebner_Basis
     4.9  uses "int_factor_simprocs.ML" "nat_simprocs.ML"
    4.10  begin
    4.11  
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Jun 05 16:26:04 2007 +0200
     5.3 @@ -0,0 +1,743 @@
     5.4 +(*  Title:      HOL/Tools/Groebner_Basis/groebner.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Amine Chaieb, TU Muenchen
     5.7 +*)
     5.8 +
     5.9 +signature GROEBNER =
    5.10 +sig
    5.11 +  val ring_and_ideal_conv :
    5.12 +    {idom: thm list, ring: cterm list * thm list, vars: cterm list,
    5.13 +     semiring: Thm.cterm list * thm list} ->
    5.14 +    (Thm.cterm -> Rat.rat) -> (Rat.rat -> Thm.cterm) ->
    5.15 +    Conv.conv ->  Conv.conv ->
    5.16 +    Conv.conv * (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list)
    5.17 +    val ring_conv : Proof.context -> cterm -> thm
    5.18 +end
    5.19 +
    5.20 +structure Groebner: GROEBNER =
    5.21 +struct
    5.22 +open Normalizer;
    5.23 +open Misc;
    5.24 +
    5.25 +     (* FIXME :: Already present in Tools/Presburger/qelim.ML but is much more general!! *)
    5.26 +fun cterm_frees ct =
    5.27 + let fun h acc t =
    5.28 +   case (term_of t) of
    5.29 +    _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
    5.30 +  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
    5.31 +  | Free _ => insert (op aconvc) t acc
    5.32 +  | _ => acc
    5.33 + in h [] ct end;
    5.34 +
    5.35 +fun assocd x al d = case AList.lookup (op =) al x of SOME y => y | NONE => d;
    5.36 +val rat_0 = Rat.zero;
    5.37 +val rat_1 = Rat.one;
    5.38 +val minus_rat = Rat.neg;
    5.39 +val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
    5.40 +fun int_of_rat a =
    5.41 +    case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int";
    5.42 +val lcm_rat = fn x => fn y => Rat.rat_of_int (lcm (int_of_rat x, int_of_rat y));
    5.43 +
    5.44 +val (eqF_intr, eqF_elim) =
    5.45 +  let val [th1,th2] = thms "PFalse"
    5.46 +  in (fn th => th COMP th2, fn th => th COMP th1) end;
    5.47 +
    5.48 +val (PFalse, PFalse') =
    5.49 + let val PFalse_eq = nth (thms "simp_thms") 13
    5.50 + in (PFalse_eq RS iffD1, PFalse_eq RS iffD2) end;
    5.51 +
    5.52 +
    5.53 +(* ------------------------------------------------------------------------- *)
    5.54 +(* Type for recording history, i.e. how a polynomial was obtained.           *)
    5.55 +(* ------------------------------------------------------------------------- *)
    5.56 +
    5.57 +datatype history =
    5.58 +   Start of int
    5.59 + | Mmul of (Rat.rat * (int list)) * history
    5.60 + | Add of history * history;
    5.61 +
    5.62 +
    5.63 +(* Monomial ordering. *)
    5.64 +
    5.65 +fun morder_lt m1 m2=
    5.66 +    let fun lexorder l1 l2 =
    5.67 +            case (l1,l2) of
    5.68 +                ([],[]) => false
    5.69 +              | (x1::o1,x2::o2) => x1 > x2 orelse x1 = x2 andalso lexorder o1 o2
    5.70 +              | _ => error "morder: inconsistent monomial lengths"
    5.71 +        val n1 = fold (curry op +) m1 0
    5.72 +        val n2 = fold (curry op +) m2 0 in
    5.73 +    n1 < n2 orelse n1 = n2 andalso lexorder m1 m2
    5.74 +    end;
    5.75 +
    5.76 +fun morder_le m1 m2 = morder_lt m1 m2 orelse (m1 = m2);
    5.77 +
    5.78 +fun morder_gt m1 m2 = morder_lt m2 m1;
    5.79 +
    5.80 +(* Arithmetic on canonical polynomials. *)
    5.81 +
    5.82 +fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l;
    5.83 +
    5.84 +fun grob_add l1 l2 =
    5.85 +  case (l1,l2) of
    5.86 +    ([],l2) => l2
    5.87 +  | (l1,[]) => l1
    5.88 +  | ((c1,m1)::o1,(c2,m2)::o2) =>
    5.89 +        if m1 = m2 then
    5.90 +          let val c = c1+/c2 val rest = grob_add o1 o2 in
    5.91 +          if c =/ rat_0 then rest else (c,m1)::rest end
    5.92 +        else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
    5.93 +        else (c2,m2)::(grob_add l1 o2);
    5.94 +
    5.95 +fun grob_sub l1 l2 = grob_add l1 (grob_neg l2);
    5.96 +
    5.97 +fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2,map2 (curry op +) m1 m2);
    5.98 +
    5.99 +fun grob_cmul cm pol = map (grob_mmul cm) pol;
   5.100 +
   5.101 +fun grob_mul l1 l2 =
   5.102 +  case l1 of
   5.103 +    [] => []
   5.104 +  | (h1::t1) => grob_add (grob_cmul h1 l2) (grob_mul t1 l2);
   5.105 +
   5.106 +fun grob_inv l =
   5.107 +  case l of
   5.108 +    [(c,vs)] => if (forall (fn x => x = 0) vs) then
   5.109 +                  if (c =/ rat_0) then error "grob_inv: division by zero"
   5.110 +                  else [(rat_1 // c,vs)]
   5.111 +              else error "grob_inv: non-constant divisor polynomial"
   5.112 +  | _ => error "grob_inv: non-constant divisor polynomial";
   5.113 +
   5.114 +fun grob_div l1 l2 =
   5.115 +  case l2 of
   5.116 +    [(c,l)] => if (forall (fn x => x = 0) l) then
   5.117 +                 if c =/ rat_0 then error "grob_div: division by zero"
   5.118 +                 else grob_cmul (rat_1 // c,l) l1
   5.119 +             else error "grob_div: non-constant divisor polynomial"
   5.120 +  | _ => error "grob_div: non-constant divisor polynomial";
   5.121 +
   5.122 +fun grob_pow vars l n =
   5.123 +  if n < 0 then error "grob_pow: negative power"
   5.124 +  else if n = 0 then [(rat_1,map (fn v => 0) vars)]
   5.125 +  else grob_mul l (grob_pow vars l (n - 1));
   5.126 +
   5.127 +val max = fn x => fn y => if x < y then y else x;
   5.128 +
   5.129 +fun degree vn p =
   5.130 + case p of
   5.131 +  [] => error "Zero polynomial"
   5.132 +| [(c,ns)] => nth ns vn
   5.133 +| (c,ns)::p' => max (nth ns vn) (degree vn p');
   5.134 +
   5.135 +fun head_deg vn p = let val d = degree vn p in
   5.136 + (d,fold (fn (c,r) => fn q => grob_add q [(c, map_index (fn (i,n) => if i = vn then 0 else n) r)]) (filter (fn (c,ns) => c <>/ rat_0 andalso nth ns vn = d) p) []) end;
   5.137 +
   5.138 +val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) 0) ns);
   5.139 +val grob_pdiv =
   5.140 + let fun pdiv_aux vn (n,a) p k s =
   5.141 +  if is_zerop s then (k,s) else
   5.142 +  let val (m,b) = head_deg vn s
   5.143 +  in if m < n then (k,s) else
   5.144 +     let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m - n else 0)
   5.145 +                                                (snd (hd s)))]
   5.146 +     in if a = b then pdiv_aux vn (n,a) p k (grob_sub s p')
   5.147 +        else pdiv_aux vn (n,a) p (k + 1) (grob_sub (grob_mul a s) (grob_mul b p'))
   5.148 +     end
   5.149 +  end
   5.150 + in fn vn => fn s => fn p => pdiv_aux vn (head_deg vn p) p 0 s
   5.151 + end;
   5.152 +
   5.153 +(* Monomial division operation. *)
   5.154 +
   5.155 +fun mdiv (c1,m1) (c2,m2) =
   5.156 +  (c1//c2,
   5.157 +   map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1-n2) m1 m2);
   5.158 +
   5.159 +(* Lowest common multiple of two monomials. *)
   5.160 +
   5.161 +fun mlcm (c1,m1) (c2,m2) = (rat_1,map2 max m1 m2);
   5.162 +
   5.163 +(* Reduce monomial cm by polynomial pol, returning replacement for cm.  *)
   5.164 +
   5.165 +fun reduce1 cm (pol,hpol) =
   5.166 +  case pol of
   5.167 +    [] => error "reduce1"
   5.168 +  | cm1::cms => ((let val (c,m) = mdiv cm cm1 in
   5.169 +                    (grob_cmul (minus_rat c,m) cms,
   5.170 +                     Mmul((minus_rat c,m),hpol)) end)
   5.171 +                handle  ERROR _ => error "reduce1");
   5.172 +
   5.173 +(* Try this for all polynomials in a basis.  *)
   5.174 +fun tryfind f l =
   5.175 +    case l of
   5.176 +        [] => error "tryfind"
   5.177 +      | (h::t) => ((f h) handle ERROR _ => tryfind f t);
   5.178 +
   5.179 +fun reduceb cm basis = tryfind (fn p => reduce1 cm p) basis;
   5.180 +
   5.181 +(* Reduction of a polynomial (always picking largest monomial possible).     *)
   5.182 +
   5.183 +fun reduce basis (pol,hist) =
   5.184 +  case pol of
   5.185 +    [] => (pol,hist)
   5.186 +  | cm::ptl => ((let val (q,hnew) = reduceb cm basis in
   5.187 +                   reduce basis (grob_add q ptl,Add(hnew,hist)) end)
   5.188 +               handle (ERROR _) =>
   5.189 +                   (let val (q,hist') = reduce basis (ptl,hist) in
   5.190 +                       (cm::q,hist') end));
   5.191 +
   5.192 +(* Check for orthogonality w.r.t. LCM.                                       *)
   5.193 +
   5.194 +fun orthogonal l p1 p2 =
   5.195 +  snd l = snd(grob_mmul (hd p1) (hd p2));
   5.196 +
   5.197 +(* Compute S-polynomial of two polynomials.                                  *)
   5.198 +
   5.199 +fun spoly cm ph1 ph2 =
   5.200 +  case (ph1,ph2) of
   5.201 +    (([],h),p) => ([],h)
   5.202 +  | (p,([],h)) => ([],h)
   5.203 +  | ((cm1::ptl1,his1),(cm2::ptl2,his2)) =>
   5.204 +        (grob_sub (grob_cmul (mdiv cm cm1) ptl1)
   5.205 +                  (grob_cmul (mdiv cm cm2) ptl2),
   5.206 +         Add(Mmul(mdiv cm cm1,his1),
   5.207 +             Mmul(mdiv (minus_rat(fst cm),snd cm) cm2,his2)));
   5.208 +
   5.209 +(* Make a polynomial monic.                                                  *)
   5.210 +
   5.211 +fun monic (pol,hist) =
   5.212 +  if pol = [] then (pol,hist) else
   5.213 +  let val (c',m') = hd pol in
   5.214 +  (map (fn (c,m) => (c//c',m)) pol,
   5.215 +   Mmul((rat_1 // c',map (K 0) m'),hist)) end;
   5.216 +
   5.217 +(* The most popular heuristic is to order critical pairs by LCM monomial.    *)
   5.218 +
   5.219 +fun forder ((c1,m1),_) ((c2,m2),_) = morder_lt m1 m2;
   5.220 +
   5.221 +fun poly_lt  p q =
   5.222 +  case (p,q) of
   5.223 +    (p,[]) => false
   5.224 +  | ([],q) => true
   5.225 +  | ((c1,m1)::o1,(c2,m2)::o2) =>
   5.226 +        c1 </ c2 orelse
   5.227 +        c1 =/ c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2);
   5.228 +
   5.229 +fun align  ((p,hp),(q,hq)) =
   5.230 +  if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
   5.231 +fun forall2 p l1 l2 =
   5.232 +  case (l1,l2) of
   5.233 +    ([],[]) => true
   5.234 +  | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
   5.235 +  | _ => false;
   5.236 +
   5.237 +fun poly_eq p1 p2 =
   5.238 +  forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso m1 = m2) p1 p2;
   5.239 +
   5.240 +fun memx ((p1,h1),(p2,h2)) ppairs =
   5.241 +  not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
   5.242 +
   5.243 +(* Buchberger's second criterion.                                            *)
   5.244 +
   5.245 +fun criterion2 basis (lcm,((p1,h1),(p2,h2))) opairs =
   5.246 +  exists (fn g => not(poly_eq (fst g) p1) andalso not(poly_eq (fst g) p2) andalso
   5.247 +                   can (mdiv lcm) (hd(fst g)) andalso
   5.248 +                   not(memx (align (g,(p1,h1))) (map snd opairs)) andalso
   5.249 +                   not(memx (align (g,(p2,h2))) (map snd opairs))) basis;
   5.250 +
   5.251 +(* Test for hitting constant polynomial.                                     *)
   5.252 +
   5.253 +fun constant_poly p =
   5.254 +  length p = 1 andalso forall (fn x=>x=0) (snd(hd p));
   5.255 +
   5.256 +(* ------------------------------------------------------------------------- *)
   5.257 +(* Grobner basis algorithm.                                                  *)
   5.258 +(* ------------------------------------------------------------------------- *)
   5.259 +(* FIXME: try to get rid of mergesort? *)
   5.260 +fun merge ord l1 l2 =
   5.261 + case l1 of
   5.262 +  [] => l2
   5.263 + | h1::t1 =>
   5.264 +   case l2 of
   5.265 +    [] => l1
   5.266 +   | h2::t2 => if ord h1 h2 then h1::(merge ord t1 l2)
   5.267 +               else h2::(merge ord l1 t2);
   5.268 +fun mergesort ord l =
   5.269 + let
   5.270 + fun mergepairs l1 l2 =
   5.271 +  case (l1,l2) of
   5.272 +   ([s],[]) => s
   5.273 + | (l,[]) => mergepairs [] l
   5.274 + | (l,[s1]) => mergepairs (s1::l) []
   5.275 + | (l,(s1::s2::ss)) => mergepairs ((merge ord s1 s2)::l) ss
   5.276 + in if l = []  then []  else mergepairs [] (map (fn x => [x]) l)
   5.277 + end;
   5.278 +
   5.279 +
   5.280 +fun grobner_basis basis pairs =
   5.281 +  (writeln (Int.toString(length basis)^" basis elements and "^
   5.282 +               Int.toString(length pairs)^" critical pairs");
   5.283 +  case pairs of
   5.284 +    [] => basis
   5.285 +  | (l,(p1,p2))::opairs =>
   5.286 +        let val (sph as (sp,hist)) = monic (reduce basis (spoly l p1 p2))
   5.287 +        in if sp = [] orelse criterion2 basis (l,(p1,p2)) opairs
   5.288 +           then grobner_basis basis opairs
   5.289 +           else if constant_poly sp then grobner_basis (sph::basis) []
   5.290 +           else let val rawcps = map (fn p => (mlcm (hd(fst p)) (hd sp),align(p,sph)))
   5.291 +                                     basis
   5.292 +                    val newcps = filter
   5.293 +                                     (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q)))
   5.294 +                                     rawcps
   5.295 +                in grobner_basis (sph::basis)
   5.296 +                                 (merge forder opairs (mergesort forder newcps))
   5.297 +                end
   5.298 +        end);
   5.299 +
   5.300 +(* ------------------------------------------------------------------------- *)
   5.301 +(* Interreduce initial polynomials.                                          *)
   5.302 +(* ------------------------------------------------------------------------- *)
   5.303 +
   5.304 +fun grobner_interreduce rpols ipols =
   5.305 +  case ipols of
   5.306 +    [] => map monic (rev rpols)
   5.307 +  | p::ps => let val p' = reduce (rpols @ ps) p in
   5.308 +             if fst p' = [] then grobner_interreduce rpols ps
   5.309 +             else grobner_interreduce (p'::rpols) ps end;
   5.310 +
   5.311 +(* ------------------------------------------------------------------------- *)
   5.312 +(* Overall function.                                                         *)
   5.313 +(* ------------------------------------------------------------------------- *)
   5.314 +
   5.315 +fun grobner pols =
   5.316 +    let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1))
   5.317 +        val phists = filter (fn (p,_) => p <> []) npols
   5.318 +        val bas = grobner_interreduce [] (map monic phists)
   5.319 +        val prs0 = product bas bas
   5.320 +        val prs1 = filter (fn ((x,_),(y,_)) => poly_lt x y) prs0
   5.321 +        val prs2 = map (fn (p,q) => (mlcm (hd(fst p)) (hd(fst q)),(p,q))) prs1
   5.322 +        val prs3 =
   5.323 +            filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q))) prs2 in
   5.324 +        grobner_basis bas (mergesort forder prs3) end;
   5.325 +
   5.326 +(* ------------------------------------------------------------------------- *)
   5.327 +(* Get proof of contradiction from Grobner basis.                            *)
   5.328 +(* ------------------------------------------------------------------------- *)
   5.329 +fun find p l =
   5.330 +  case l of
   5.331 +      [] => error "find"
   5.332 +    | (h::t) => if p(h) then h else find p t;
   5.333 +
   5.334 +fun grobner_refute pols =
   5.335 +  let val gb = grobner pols in
   5.336 +  snd(find (fn (p,h) => length p = 1 andalso forall (fn x=> x=0) (snd(hd p))) gb)
   5.337 +  end;
   5.338 +
   5.339 +(* ------------------------------------------------------------------------- *)
   5.340 +(* Turn proof into a certificate as sum of multipliers.                      *)
   5.341 +(*                                                                           *)
   5.342 +(* In principle this is very inefficient: in a heavily shared proof it may   *)
   5.343 +(* make the same calculation many times. Could put in a cache or something.  *)
   5.344 +(* ------------------------------------------------------------------------- *)
   5.345 +fun assoc x l = snd(find (fn p => fst p = x) l);
   5.346 +
   5.347 +fun resolve_proof vars prf =
   5.348 +  case prf of
   5.349 +    Start(~1) => []
   5.350 +  | Start m => [(m,[(rat_1,map (K 0) vars)])]
   5.351 +  | Mmul(pol,lin) =>
   5.352 +        let val lis = resolve_proof vars lin in
   5.353 +            map (fn (n,p) => (n,grob_cmul pol p)) lis end
   5.354 +  | Add(lin1,lin2) =>
   5.355 +        let val lis1 = resolve_proof vars lin1
   5.356 +            val lis2 = resolve_proof vars lin2
   5.357 +            val dom = distinct (op =) ((map fst lis1) union (map fst lis2))
   5.358 +        in
   5.359 +            map (fn n => let val a = ((assoc n lis1) handle _ => [])  (* FIXME *)
   5.360 +                             val b = ((assoc n lis2) handle _ => []) in  (* FIXME *)
   5.361 +                             (n,grob_add a b) end) dom end;
   5.362 +
   5.363 +(* ------------------------------------------------------------------------- *)
   5.364 +(* Run the procedure and produce Weak Nullstellensatz certificate.           *)
   5.365 +(* ------------------------------------------------------------------------- *)
   5.366 +fun grobner_weak vars pols =
   5.367 +    let val cert = resolve_proof vars (grobner_refute pols)
   5.368 +        val l =
   5.369 +            fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in
   5.370 +        (l,map (fn (i,p) => (i,map (fn (d,m) => (l*/d,m)) p)) cert) end;
   5.371 +
   5.372 +(* ------------------------------------------------------------------------- *)
   5.373 +(* Prove a polynomial is in ideal generated by others, using Grobner basis.  *)
   5.374 +(* ------------------------------------------------------------------------- *)
   5.375 +
   5.376 +fun grobner_ideal vars pols pol =
   5.377 +  let val (pol',h) = reduce (grobner pols) (grob_neg pol,Start(~1)) in
   5.378 +  if pol <> [] then error "grobner_ideal: not in the ideal" else
   5.379 +  resolve_proof vars h end;
   5.380 +
   5.381 +(* ------------------------------------------------------------------------- *)
   5.382 +(* Produce Strong Nullstellensatz certificate for a power of pol.            *)
   5.383 +(* ------------------------------------------------------------------------- *)
   5.384 +
   5.385 +fun grobner_strong vars pols pol =
   5.386 +    let val vars' = @{cterm "True"}::vars
   5.387 +        val grob_z = [(rat_1,1::(map (fn x => 0) vars))]
   5.388 +        val grob_1 = [(rat_1,(map (fn x => 0) vars'))]
   5.389 +        fun augment p= map (fn (c,m) => (c,0::m)) p
   5.390 +        val pols' = map augment pols
   5.391 +        val pol' = augment pol
   5.392 +        val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols'
   5.393 +        val (l,cert) = grobner_weak vars' allpols
   5.394 +        val d = fold_rev (fold_rev (max o hd o snd) o snd) cert 0
   5.395 +        fun transform_monomial (c,m) =
   5.396 +            grob_cmul (c,tl m) (grob_pow vars pol (d - hd m))
   5.397 +        fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q []
   5.398 +        val cert' = map (fn (c,q) => (c-1,transform_polynomial q))
   5.399 +                        (filter (fn (k,_) => k <> 0) cert) in
   5.400 +        (d,l,cert') end;
   5.401 +
   5.402 +fun string_of_pol vars pol =
   5.403 +    foldl (fn ((c,m),s) => ((Rat.string_of_rat c)
   5.404 +                            ^ "*(" ^
   5.405 +                            (snd (foldl
   5.406 +                                      (fn (e,(i,s)) =>
   5.407 +                                          (i+ 1,
   5.408 +                                           (nth vars i
   5.409 +                                                     |>cterm_of (the_context())
   5.410 +                                                     |> string_of_cterm)^ "^"
   5.411 +                                           ^ (Int.toString e) ^" * " ^ s)) (0,"0") m))
   5.412 +                            ^ ") + ") ^ s) "" pol;
   5.413 +
   5.414 +
   5.415 +(* ------------------------------------------------------------------------- *)
   5.416 +(* Overall parametrized universal procedure for (semi)rings.                 *)
   5.417 +(* We return an ideal_conv and the actual ring prover.                       *)
   5.418 +(* ------------------------------------------------------------------------- *)
   5.419 +fun refute_disj rfn tm =
   5.420 + case term_of tm of
   5.421 +  Const("op |",_)$l$r =>
   5.422 +   Drule.compose_single(refute_disj rfn (Thm.dest_arg tm),2,Drule.compose_single(refute_disj rfn (Thm.dest_arg1 tm),2,disjE))
   5.423 +  | _ => rfn tm ;
   5.424 +
   5.425 +val notnotD = @{thm "notnotD"};
   5.426 +fun mk_binop ct x y =
   5.427 +  Thm.capply (Thm.capply ct x) y
   5.428 +
   5.429 +val mk_comb = Thm.capply;
   5.430 +fun is_neg t =
   5.431 +    case term_of t of
   5.432 +      (Const("Not",_)$p) => true
   5.433 +    | _  => false;
   5.434 +fun is_eq t =
   5.435 + case term_of t of
   5.436 + (Const("op =",_)$_$_) => true
   5.437 +| _  => false;
   5.438 +
   5.439 +fun end_itlist f l =
   5.440 +  case l of
   5.441 +        []     => error "end_itlist"
   5.442 +      | [x]    => x
   5.443 +      | (h::t) => f h (end_itlist f t);
   5.444 +
   5.445 +val list_mk_binop = fn b => end_itlist (mk_binop b);
   5.446 +
   5.447 +val list_dest_binop = fn b =>
   5.448 + let fun h acc t =
   5.449 +  ((let val (l,r) = dest_binop b t in h (h acc r) l end)
   5.450 +   handle CTERM _ => (t::acc)) (* Why had I handle _ => ? *)
   5.451 + in h []
   5.452 + end;
   5.453 +
   5.454 +val strip_exists =
   5.455 + let fun h (acc, t) =
   5.456 +      case (term_of t) of
   5.457 +       Const("Ex",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   5.458 +     | _ => (acc,t)
   5.459 + in fn t => h ([],t)
   5.460 + end;
   5.461 +
   5.462 +fun is_forall t =
   5.463 + case term_of t of
   5.464 +  (Const("All",_)$Abs(_,_,_)) => true
   5.465 +| _ => false;
   5.466 +
   5.467 +val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
   5.468 +val bool_simps = @{thms "bool_simps"};
   5.469 +val nnf_simps = @{thms "nnf_simps"};
   5.470 +val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps bool_simps addsimps nnf_simps)
   5.471 +val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "weak_dnf_simps"}));
   5.472 +val initial_conv =
   5.473 +    Simplifier.rewrite
   5.474 +     (HOL_basic_ss addsimps nnf_simps
   5.475 +     addsimps [not_all, not_ex] addsimps map (fn th => th RS sym) (ex_simps @ all_simps));
   5.476 +
   5.477 +val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
   5.478 +
   5.479 +val cTrp = @{cterm "Trueprop"};
   5.480 +val cConj = @{cterm "op &"};
   5.481 +val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
   5.482 +val ASSUME = mk_comb cTrp #> assume;
   5.483 +val list_mk_conj = list_mk_binop cConj;
   5.484 +val conjs = list_dest_binop cConj;
   5.485 +val mk_neg = mk_comb cNot;
   5.486 +
   5.487 +
   5.488 +
   5.489 +(** main **)
   5.490 +
   5.491 +fun ring_and_ideal_conv
   5.492 +  {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom}
   5.493 +  dest_const mk_const ring_eq_conv ring_normalize_conv =
   5.494 +let
   5.495 +  val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
   5.496 +  val [ring_add_tm, ring_mul_tm, ring_pow_tm] =
   5.497 +    map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];
   5.498 +
   5.499 +  val (ring_sub_tm, ring_neg_tm) =
   5.500 +    (case r_ops of
   5.501 +      [] => (@{cterm "True"}, @{cterm "True"})
   5.502 +    | [sub_pat, neg_pat] => (Thm.dest_fun (Thm.dest_fun sub_pat), Thm.dest_fun neg_pat));
   5.503 +
   5.504 +  val [idom_thm, neq_thm] = idom;
   5.505 +
   5.506 +  val ring_dest_neg =
   5.507 +    fn t => let val (l,r) = Thm.dest_comb t in
   5.508 +        if could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t])
   5.509 +      end
   5.510 +
   5.511 + val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
   5.512 +(*
   5.513 + fun ring_dest_inv t =
   5.514 +    let val (l,r) = Thm.dest_comb t in
   5.515 +        if could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv"
   5.516 +    end
   5.517 +*)
   5.518 + val ring_dest_add = dest_binop ring_add_tm;
   5.519 + val ring_mk_add = mk_binop ring_add_tm;
   5.520 + val ring_dest_sub = dest_binop ring_sub_tm;
   5.521 + val ring_mk_sub = mk_binop ring_sub_tm;
   5.522 + val ring_dest_mul = dest_binop ring_mul_tm;
   5.523 + val ring_mk_mul = mk_binop ring_mul_tm;
   5.524 +(* val ring_dest_div = dest_binop ring_div_tm;
   5.525 + val ring_mk_div = mk_binop ring_div_tm;*)
   5.526 + val ring_dest_pow = dest_binop ring_pow_tm;
   5.527 + val ring_mk_pow = mk_binop ring_pow_tm ;
   5.528 + fun grobvars tm acc =
   5.529 +    if can dest_const tm then acc
   5.530 +    else if can ring_dest_neg tm then grobvars (Thm.dest_arg tm) acc
   5.531 +    else if can ring_dest_pow tm then grobvars (Thm.dest_arg1 tm) acc
   5.532 +    else if can ring_dest_add tm orelse can ring_dest_sub tm
   5.533 +            orelse can ring_dest_mul tm
   5.534 +    then grobvars (Thm.dest_arg1 tm) (grobvars (Thm.dest_arg tm) acc)
   5.535 +(*    else if can ring_dest_inv tm
   5.536 +       then
   5.537 +             let val gvs = grobvars (Thm.dest_arg tm) [] in
   5.538 +             if gvs = [] then acc else tm::acc
   5.539 +             end
   5.540 +    else if can ring_dest_div tm then
   5.541 +              let val lvs = grobvars (Thm.dest_arg1 tm) acc
   5.542 +                val gvs = grobvars (Thm.dest_arg tm) []
   5.543 +              in if gvs = [] then lvs else tm::acc
   5.544 +             end *)
   5.545 +    else tm::acc ;
   5.546 +
   5.547 +fun grobify_term vars tm =
   5.548 +((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
   5.549 +     [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)])
   5.550 +handle  CTERM _ =>
   5.551 + ((let val x = dest_const tm
   5.552 + in if x =/ rat_0 then [] else [(x,map (fn v => 0) vars)]
   5.553 + end)
   5.554 + handle ERROR _ =>
   5.555 +  ((grob_neg(grobify_term vars (ring_dest_neg tm)))
   5.556 +  handle CTERM _ =>
   5.557 +   (
   5.558 +(*   (grob_inv(grobify_term vars (ring_dest_inv tm)))
   5.559 +   handle CTERM _ => *)
   5.560 +    ((let val (l,r) = ring_dest_add tm
   5.561 +    in grob_add (grobify_term vars l) (grobify_term vars r)
   5.562 +    end)
   5.563 +    handle CTERM _ =>
   5.564 +     ((let val (l,r) = ring_dest_sub tm
   5.565 +     in grob_sub (grobify_term vars l) (grobify_term vars r)
   5.566 +     end)
   5.567 +     handle  CTERM _ =>
   5.568 +      ((let val (l,r) = ring_dest_mul tm
   5.569 +      in grob_mul (grobify_term vars l) (grobify_term vars r)
   5.570 +      end)
   5.571 +       handle CTERM _ =>
   5.572 +        (
   5.573 +(*  (let val (l,r) = ring_dest_div tm
   5.574 +          in grob_div (grobify_term vars l) (grobify_term vars r)
   5.575 +          end)
   5.576 +         handle CTERM _ => *)
   5.577 +          ((let val (l,r) = ring_dest_pow tm
   5.578 +          in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r)
   5.579 +          end)
   5.580 +           handle CTERM _ => error "grobify_term: unknown or invalid term")))))))));
   5.581 +val eq_tm = idom_thm |> concl |> Thm.dest_arg |> Thm.dest_arg |> Thm.dest_fun |> Thm.dest_fun ;
   5.582 +(*ring_integral |> hd |> concl |> Thm.dest_arg
   5.583 +                          |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_fun; *)
   5.584 +val dest_eq = dest_binop eq_tm;
   5.585 +
   5.586 +fun grobify_equation vars tm =
   5.587 +    let val (l,r) = dest_binop eq_tm tm
   5.588 +    in grob_sub (grobify_term vars l) (grobify_term vars r)
   5.589 +    end;
   5.590 +
   5.591 +fun grobify_equations tm =
   5.592 + let
   5.593 +  val cjs = conjs tm
   5.594 +  val  rawvars = fold_rev (fn eq => fn a =>
   5.595 +                                       grobvars (Thm.dest_arg1 eq) (grobvars (Thm.dest_arg eq) a)) cjs []
   5.596 +  val vars = sort (fn (x, y) => Term.term_ord(term_of x,term_of y))
   5.597 +                  (distinct (op aconvc) rawvars)
   5.598 + in (vars,map (grobify_equation vars) cjs)
   5.599 + end;
   5.600 +
   5.601 +val holify_polynomial =
   5.602 + let fun holify_varpow (v,n) =
   5.603 +  if n = 1 then v else ring_mk_pow v (mk_cnumber @{ctyp "nat"} n)  (* FIXME *)
   5.604 + fun holify_monomial vars (c,m) =
   5.605 +  let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
   5.606 +   in end_itlist ring_mk_mul (mk_const c :: xps)
   5.607 +  end
   5.608 + fun holify_polynomial vars p =
   5.609 +     if p = [] then mk_const (rat_0)
   5.610 +     else end_itlist ring_mk_add (map (holify_monomial vars) p)
   5.611 + in holify_polynomial
   5.612 + end ;
   5.613 +val idom_rule = simplify (HOL_basic_ss addsimps [idom_thm]);
   5.614 +fun prove_nz n = eqF_elim
   5.615 +                 (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const(rat_0))));
   5.616 +val neq_01 = prove_nz (rat_1);
   5.617 +fun neq_rule n th = [prove_nz n, th] MRS neq_thm;
   5.618 +fun mk_add th1 = combination(Drule.arg_cong_rule ring_add_tm th1);
   5.619 +
   5.620 +fun refute tm =
   5.621 + if tm aconvc false_tm then ASSUME tm else
   5.622 +  let
   5.623 +   val (nths0,eths0) = List.partition (is_neg o concl) (conjuncts(ASSUME tm))
   5.624 +   val  nths = filter (is_eq o Thm.dest_arg o concl) nths0
   5.625 +   val eths = filter (is_eq o concl) eths0
   5.626 +  in
   5.627 +   if null eths then
   5.628 +    let
   5.629 +      val th1 = end_itlist (fn th1 => fn th2 => idom_rule(conji th1 th2)) nths
   5.630 +      val th2 = Conv.fconv_rule
   5.631 +                ((arg_conv #> arg_conv)
   5.632 +                     (binop_conv ring_normalize_conv)) th1
   5.633 +      val conc = th2 |> concl |> Thm.dest_arg
   5.634 +      val (l,r) = conc |> dest_eq
   5.635 +    in implies_intr (mk_comb cTrp tm)
   5.636 +                    (equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2))
   5.637 +                           (reflexive l |> mk_object_eq))
   5.638 +    end
   5.639 +   else
   5.640 +   let
   5.641 +    val (vars,l,cert,noteqth) =(
   5.642 +     if null nths then
   5.643 +      let val (vars,pols) = grobify_equations(list_mk_conj(map concl eths))
   5.644 +          val (l,cert) = grobner_weak vars pols
   5.645 +      in (vars,l,cert,neq_01)
   5.646 +      end
   5.647 +     else
   5.648 +      let
   5.649 +       val nth = end_itlist (fn th1 => fn th2 => idom_rule(conji th1 th2)) nths
   5.650 +       val (vars,pol::pols) =
   5.651 +          grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths))
   5.652 +       val (deg,l,cert) = grobner_strong vars pols pol
   5.653 +       val th1 = Conv.fconv_rule((arg_conv o arg_conv)(binop_conv ring_normalize_conv)) nth
   5.654 +       val th2 = funpow deg (idom_rule o conji th1) neq_01
   5.655 +      in (vars,l,cert,th2)
   5.656 +      end)
   5.657 +    val _ = writeln ("Translating certificate to HOL inferences")
   5.658 +    val cert_pos = map (fn (i,p) => (i,filter (fn (c,m) => c >/ rat_0) p)) cert
   5.659 +    val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
   5.660 +                                            (filter (fn (c,m) => c </ rat_0) p))) cert
   5.661 +    val  herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
   5.662 +    val  herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
   5.663 +    fun thm_fn pols =
   5.664 +        if null pols then reflexive(mk_const rat_0) else
   5.665 +        end_itlist mk_add
   5.666 +            (map (fn (i,p) => Drule.arg_cong_rule (mk_comb ring_mul_tm p) (nth eths i |> mk_meta_eq)) pols)
   5.667 +    val th1 = thm_fn herts_pos
   5.668 +    val th2 = thm_fn herts_neg
   5.669 +    val th3 = conji(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth
   5.670 +    val th4 = Conv.fconv_rule ((arg_conv o arg_conv o binop_conv) ring_normalize_conv)
   5.671 +                               (neq_rule l th3)
   5.672 +    val (l,r) = dest_eq(Thm.dest_arg(concl th4))
   5.673 +   in implies_intr (mk_comb cTrp tm)
   5.674 +                        (equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4))
   5.675 +                   (reflexive l |> mk_object_eq))
   5.676 +   end
   5.677 +  end
   5.678 +
   5.679 +fun ring tm =
   5.680 + let
   5.681 +  fun mk_forall x p =
   5.682 +      mk_comb (Drule.cterm_rule (instantiate' [SOME (ctyp_of_term x)] []) @{cpat "All:: (?'a => bool) => _"}) (Thm.cabs x p)
   5.683 +  val avs = cterm_frees tm
   5.684 +  val P' = fold mk_forall avs tm
   5.685 +  val th1 = initial_conv(mk_neg P')
   5.686 +  val (evs,bod) = strip_exists(concl th1) in
   5.687 +   if is_forall bod then error "ring: non-universal formula"
   5.688 +   else
   5.689 +   let
   5.690 +    val th1a = weak_dnf_conv bod
   5.691 +    val boda = concl th1a
   5.692 +    val th2a = refute_disj refute boda
   5.693 +    val th2b = [mk_object_eq th1a, (th2a COMP notI) COMP PFalse'] MRS trans
   5.694 +    val th2 = fold (fn v => fn th => (forall_intr v th) COMP allI) evs (th2b RS PFalse)
   5.695 +    val th3 = equal_elim
   5.696 +                (Simplifier.rewrite (HOL_basic_ss addsimps [not_ex RS sym])
   5.697 +                          (th2 |> cprop_of)) th2
   5.698 +    in specl avs
   5.699 +             ([[[mk_object_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD)
   5.700 +   end
   5.701 + end
   5.702 +fun ideal tms tm ord =
   5.703 + let
   5.704 +  val rawvars = fold_rev grobvars (tm::tms) []
   5.705 +  val vars = sort ord (distinct (fn (x,y) => (term_of x) aconv (term_of y)) rawvars)
   5.706 +  val pols = map (grobify_term vars) tms
   5.707 +  val pol = grobify_term vars tm
   5.708 +  val cert = grobner_ideal vars pols pol
   5.709 + in map (fn n => let val p = assocd n cert [] in holify_polynomial vars p end)
   5.710 +        (0 upto (length pols-1))
   5.711 + end
   5.712 +in (ring,ideal)
   5.713 +end;
   5.714 +
   5.715 +
   5.716 +fun find_term bounds tm =
   5.717 +  (case term_of tm of
   5.718 +    Const ("op =", T) $ _ $ _ =>
   5.719 +      if domain_type T = HOLogic.boolT then find_args bounds tm
   5.720 +      else Thm.dest_arg tm
   5.721 +  | Const ("Not", _) $ _ => find_term bounds (Thm.dest_arg tm)
   5.722 +  | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
   5.723 +  | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
   5.724 +  | Const ("op &", _) $ _ $ _ => find_args bounds tm
   5.725 +  | Const ("op |", _) $ _ $ _ => find_args bounds tm
   5.726 +  | Const ("op -->", _) $ _ $ _ => find_args bounds tm
   5.727 +  | _ => raise TERM ("find_term", []))
   5.728 +and find_args bounds tm =
   5.729 +  let val (t, u) = Thm.dest_binop tm
   5.730 +  in (find_term bounds t handle TERM _ => find_term bounds u) end
   5.731 +and find_body bounds b =
   5.732 +  let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
   5.733 +  in find_term (bounds + 1) b' end;
   5.734 +
   5.735 +fun ring_conv ctxt form =
   5.736 +  (case try (find_term 0 (* FIXME !? *)) form of
   5.737 +    NONE => reflexive form
   5.738 +  | SOME tm =>
   5.739 +      (case NormalizerData.match ctxt tm of
   5.740 +        NONE => reflexive form
   5.741 +      | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) =>
   5.742 +        fst (ring_and_ideal_conv theory
   5.743 +          dest_const (mk_const (Thm.ctyp_of_term tm)) ring_eq_conv
   5.744 +          (semiring_normalize_wrapper res)) form));
   5.745 +
   5.746 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/Groebner_Basis/misc.ML	Tue Jun 05 16:26:04 2007 +0200
     6.3 @@ -0,0 +1,40 @@
     6.4 +(*  Title:      HOL/Tools/Groebner_Basis/misc.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     Amine Chaieb, TU Muenchen
     6.7 +
     6.8 +Very basic stuff for cterms.
     6.9 +*)
    6.10 +
    6.11 +structure Misc =
    6.12 +struct
    6.13 +
    6.14 +open Conv;
    6.15 +
    6.16 +val is_comb = can Thm.dest_comb;
    6.17 +val concl = cprop_of #> Thm.dest_arg;
    6.18 +
    6.19 +fun is_binop ct ct' = ct aconvc (Thm.dest_fun2 ct')
    6.20 +  handle CTERM _ => false;
    6.21 +
    6.22 +fun dest_binop ct ct' =
    6.23 +  if is_binop ct ct' then Thm.dest_binop ct'
    6.24 +  else raise CTERM ("dest_binop: bad binop", [ct,ct'])
    6.25 +
    6.26 +(* INFERENCE *)
    6.27 +fun conji th th' = 
    6.28 +let val p = concl th val q = concl th' 
    6.29 +in implies_elim (implies_elim (instantiate' [] (map SOME [p,q]) conjI) th) th' end;
    6.30 +fun conjunct1' th = th RS conjunct1;
    6.31 +fun conjunct2' th = th RS conjunct2;
    6.32 +fun conj_pair th = (conjunct1' th, conjunct2' th);
    6.33 +val conjuncts =
    6.34 + let fun CJ th acc =
    6.35 +      ((let val (th1,th2) = conj_pair th
    6.36 +      in CJ th2 (CJ th1 acc) end)
    6.37 +         handle THM _ => th::acc)
    6.38 + in fn th => rev (CJ th [])
    6.39 + end;
    6.40 +
    6.41 +fun inst_thm inst = Thm.instantiate ([], inst);
    6.42 +
    6.43 +end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Jun 05 16:26:04 2007 +0200
     7.3 @@ -0,0 +1,649 @@
     7.4 +(*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Amine Chaieb, TU Muenchen
     7.7 +*)
     7.8 +
     7.9 +signature NORMALIZER = 
    7.10 +sig
    7.11 + val mk_cnumber : ctyp -> int -> cterm
    7.12 + val mk_cnumeral : int -> cterm
    7.13 + val semiring_normalize_conv : Proof.context -> Conv.conv
    7.14 + val semiring_normalize_tac : Proof.context -> int -> tactic
    7.15 + val semiring_normalize_wrapper :  NormalizerData.entry -> Conv.conv
    7.16 + val semiring_normalizers_conv :
    7.17 +     cterm list -> cterm list * thm list -> cterm list * thm list ->
    7.18 +     (cterm -> bool) * Conv.conv * Conv.conv * Conv.conv -> (cterm -> Thm.cterm -> bool) ->
    7.19 +       {add: Conv.conv, mul: Conv.conv, neg: Conv.conv, main: Conv.conv, 
    7.20 +        pow: Conv.conv, sub: Conv.conv}
    7.21 +end
    7.22 +
    7.23 +structure Normalizer: NORMALIZER = 
    7.24 +struct
    7.25 +open Misc;
    7.26 +
    7.27 +local
    7.28 + val pls_const = @{cterm "Numeral.Pls"}
    7.29 +   and min_const = @{cterm "Numeral.Min"}
    7.30 +   and bit_const = @{cterm "Numeral.Bit"}
    7.31 +   and zero = @{cpat "0"}
    7.32 +   and one = @{cpat "1"}
    7.33 + fun mk_cbit 0 = @{cterm "Numeral.bit.B0"}
    7.34 +  | mk_cbit 1 = @{cterm "Numeral.bit.B1"}
    7.35 +  | mk_cbit _ = raise CTERM ("mk_cbit", []);
    7.36 +
    7.37 +in
    7.38 +
    7.39 +fun mk_cnumeral 0 = pls_const
    7.40 +  | mk_cnumeral ~1 = min_const
    7.41 +  | mk_cnumeral i =
    7.42 +      let val (q, r) = IntInf.divMod (i, 2)
    7.43 +      in Thm.capply (Thm.capply bit_const (mk_cnumeral q)) (mk_cbit (IntInf.toInt r)) 
    7.44 +      end;
    7.45 +
    7.46 +fun mk_cnumber cT = 
    7.47 + let 
    7.48 +  val [nb_of, z, on] = 
    7.49 +    map (Drule.cterm_rule (instantiate' [SOME cT] [])) [@{cpat "number_of"}, zero, one]
    7.50 +  fun h 0 = z
    7.51 +    | h 1 = on
    7.52 +    | h x = Thm.capply nb_of (mk_cnumeral x)
    7.53 + in h end;
    7.54 +end;
    7.55 +
    7.56 +
    7.57 +(* Very basic stuff for terms *)
    7.58 +val dest_numeral = term_of #> HOLogic.dest_number #> snd;
    7.59 +val is_numeral = can dest_numeral;
    7.60 +
    7.61 +val numeral01_conv = Simplifier.rewrite
    7.62 +                         (HOL_basic_ss addsimps [numeral_1_eq_1, numeral_0_eq_0]);
    7.63 +val zero1_numeral_conv = 
    7.64 + Simplifier.rewrite (HOL_basic_ss addsimps [numeral_1_eq_1 RS sym, numeral_0_eq_0 RS sym]);
    7.65 +val zerone_conv = fn cv => zero1_numeral_conv then_conv cv then_conv numeral01_conv;
    7.66 +val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
    7.67 +                @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, 
    7.68 +                @{thm "less_nat_number_of"}];
    7.69 +val nat_add_conv = 
    7.70 + zerone_conv 
    7.71 +  (Simplifier.rewrite 
    7.72 +    (HOL_basic_ss 
    7.73 +       addsimps arith_simps @ natarith @ rel_simps
    7.74 +             @ [if_False, if_True, add_0, add_Suc, add_number_of_left, Suc_eq_add_numeral_1]
    7.75 +             @ map (fn th => th RS sym) numerals));
    7.76 +
    7.77 +val nat_mul_conv = nat_add_conv;
    7.78 +val zeron_tm = @{cterm "0::nat"};
    7.79 +val onen_tm  = @{cterm "1::nat"};
    7.80 +val true_tm = @{cterm "True"};
    7.81 +
    7.82 +
    7.83 +(* The main function! *)
    7.84 +fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules)
    7.85 +  (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
    7.86 +let
    7.87 +
    7.88 +val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08,
    7.89 +     pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16,
    7.90 +     pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24,
    7.91 +     pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32,
    7.92 +     pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules;
    7.93 +
    7.94 +val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars;
    7.95 +val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
    7.96 +val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];
    7.97 +
    7.98 +val dest_add = dest_binop add_tm
    7.99 +val dest_mul = dest_binop mul_tm
   7.100 +fun dest_pow tm =
   7.101 + let val (l,r) = dest_binop pow_tm tm
   7.102 + in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm])
   7.103 + end;
   7.104 +val is_add = is_binop add_tm
   7.105 +val is_mul = is_binop mul_tm
   7.106 +fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm);
   7.107 +
   7.108 +val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
   7.109 +  (case (r_ops, r_rules) of
   7.110 +    ([], []) => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)
   7.111 +  | ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
   7.112 +      let
   7.113 +        val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
   7.114 +        val neg_tm = Thm.dest_fun neg_pat
   7.115 +        val dest_sub = dest_binop sub_tm
   7.116 +        val is_sub = is_binop sub_tm
   7.117 +      in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
   7.118 +          sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
   7.119 +      end);
   7.120 +in fn variable_order =>
   7.121 + let
   7.122 +
   7.123 +(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible.  *)
   7.124 +(* Also deals with "const * const", but both terms must involve powers of    *)
   7.125 +(* the same variable, or both be constants, or behaviour may be incorrect.   *)
   7.126 +
   7.127 + fun powvar_mul_conv tm =
   7.128 +  let
   7.129 +  val (l,r) = dest_mul tm
   7.130 +  in if is_semiring_constant l andalso is_semiring_constant r
   7.131 +     then semiring_mul_conv tm
   7.132 +     else
   7.133 +      ((let
   7.134 +         val (lx,ln) = dest_pow l
   7.135 +        in
   7.136 +         ((let val (rx,rn) = dest_pow r
   7.137 +               val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
   7.138 +                val (tm1,tm2) = Thm.dest_comb(concl th1) in
   7.139 +               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   7.140 +           handle CTERM _ =>
   7.141 +            (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
   7.142 +                 val (tm1,tm2) = Thm.dest_comb(concl th1) in
   7.143 +               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
   7.144 +       handle CTERM _ =>
   7.145 +           ((let val (rx,rn) = dest_pow r
   7.146 +                val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
   7.147 +                val (tm1,tm2) = Thm.dest_comb(concl th1) in
   7.148 +               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   7.149 +           handle CTERM _ => inst_thm [(cx,l)] pthm_32
   7.150 +
   7.151 +))
   7.152 + end;
   7.153 +
   7.154 +(* Remove "1 * m" from a monomial, and just leave m.                         *)
   7.155 +
   7.156 + fun monomial_deone th =
   7.157 +       (let val (l,r) = dest_mul(concl th) in
   7.158 +           if l aconvc one_tm
   7.159 +          then transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
   7.160 +       handle CTERM _ => th;
   7.161 +
   7.162 +(* Conversion for "(monomial)^n", where n is a numeral.                      *)
   7.163 +
   7.164 + val monomial_pow_conv =
   7.165 +  let
   7.166 +   fun monomial_pow tm bod ntm =
   7.167 +    if not(is_comb bod)
   7.168 +    then reflexive tm
   7.169 +    else
   7.170 +     if is_semiring_constant bod
   7.171 +     then semiring_pow_conv tm
   7.172 +     else
   7.173 +      let
   7.174 +      val (lopr,r) = Thm.dest_comb bod
   7.175 +      in if not(is_comb lopr)
   7.176 +         then reflexive tm
   7.177 +        else
   7.178 +          let
   7.179 +          val (opr,l) = Thm.dest_comb lopr
   7.180 +         in
   7.181 +           if opr aconvc pow_tm andalso is_numeral r
   7.182 +          then
   7.183 +            let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
   7.184 +                val (l,r) = Thm.dest_comb(concl th1)
   7.185 +           in transitive th1 (Drule.arg_cong_rule l (nat_mul_conv r))
   7.186 +           end
   7.187 +           else
   7.188 +            if opr aconvc mul_tm
   7.189 +            then
   7.190 +             let
   7.191 +              val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33
   7.192 +             val (xy,z) = Thm.dest_comb(concl th1)
   7.193 +              val (x,y) = Thm.dest_comb xy
   7.194 +              val thl = monomial_pow y l ntm
   7.195 +              val thr = monomial_pow z r ntm
   7.196 +             in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
   7.197 +             end
   7.198 +             else reflexive tm
   7.199 +          end
   7.200 +      end
   7.201 +  in fn tm =>
   7.202 +   let
   7.203 +    val (lopr,r) = Thm.dest_comb tm
   7.204 +    val (opr,l) = Thm.dest_comb lopr
   7.205 +   in if not (opr aconvc pow_tm) orelse not(is_numeral r)
   7.206 +      then raise CTERM ("monomial_pow_conv", [tm])
   7.207 +      else if r aconvc zeron_tm
   7.208 +      then inst_thm [(cx,l)] pthm_35
   7.209 +      else if r aconvc onen_tm
   7.210 +      then inst_thm [(cx,l)] pthm_36
   7.211 +      else monomial_deone(monomial_pow tm l r)
   7.212 +   end
   7.213 +  end;
   7.214 +
   7.215 +(* Multiplication of canonical monomials.                                    *)
   7.216 + val monomial_mul_conv =
   7.217 +  let
   7.218 +   fun powvar tm =
   7.219 +    if is_semiring_constant tm then one_tm
   7.220 +    else
   7.221 +     ((let val (lopr,r) = Thm.dest_comb tm
   7.222 +           val (opr,l) = Thm.dest_comb lopr
   7.223 +       in if opr aconvc pow_tm andalso is_numeral r then l 
   7.224 +          else raise CTERM ("monomial_mul_conv",[tm]) end)
   7.225 +     handle CTERM _ => tm)   (* FIXME !? *)
   7.226 +   fun  vorder x y =
   7.227 +    if x aconvc y then 0
   7.228 +    else
   7.229 +     if x aconvc one_tm then ~1
   7.230 +     else if y aconvc one_tm then 1
   7.231 +      else if variable_order x y then ~1 else 1
   7.232 +   fun monomial_mul tm l r =
   7.233 +    ((let val (lx,ly) = dest_mul l val vl = powvar lx
   7.234 +      in
   7.235 +      ((let
   7.236 +        val (rx,ry) = dest_mul r
   7.237 +         val vr = powvar rx
   7.238 +         val ord = vorder vl vr
   7.239 +        in
   7.240 +         if ord = 0
   7.241 +        then
   7.242 +          let
   7.243 +             val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15
   7.244 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.245 +             val (tm3,tm4) = Thm.dest_comb tm1
   7.246 +             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   7.247 +             val th3 = transitive th1 th2
   7.248 +              val  (tm5,tm6) = Thm.dest_comb(concl th3)
   7.249 +              val  (tm7,tm8) = Thm.dest_comb tm6
   7.250 +             val  th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
   7.251 +         in  transitive th3 (Drule.arg_cong_rule tm5 th4)
   7.252 +         end
   7.253 +         else
   7.254 +          let val th0 = if ord < 0 then pthm_16 else pthm_17
   7.255 +             val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
   7.256 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.257 +             val (tm3,tm4) = Thm.dest_comb tm2
   7.258 +         in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   7.259 +         end
   7.260 +        end)
   7.261 +       handle CTERM _ =>
   7.262 +        (let val vr = powvar r val ord = vorder vl vr
   7.263 +        in
   7.264 +          if ord = 0 then
   7.265 +           let
   7.266 +           val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18
   7.267 +                 val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.268 +           val (tm3,tm4) = Thm.dest_comb tm1
   7.269 +           val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   7.270 +          in transitive th1 th2
   7.271 +          end
   7.272 +          else
   7.273 +          if ord < 0 then
   7.274 +            let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
   7.275 +                val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.276 +                val (tm3,tm4) = Thm.dest_comb tm2
   7.277 +           in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   7.278 +           end
   7.279 +           else inst_thm [(ca,l),(cb,r)] pthm_09
   7.280 +        end)) end)
   7.281 +     handle CTERM _ =>
   7.282 +      (let val vl = powvar l in
   7.283 +        ((let
   7.284 +          val (rx,ry) = dest_mul r
   7.285 +          val vr = powvar rx
   7.286 +           val ord = vorder vl vr
   7.287 +         in if ord = 0 then
   7.288 +              let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
   7.289 +                 val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.290 +                 val (tm3,tm4) = Thm.dest_comb tm1
   7.291 +             in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
   7.292 +             end
   7.293 +             else if ord > 0 then
   7.294 +                 let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
   7.295 +                     val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.296 +                    val (tm3,tm4) = Thm.dest_comb tm2
   7.297 +                in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   7.298 +                end
   7.299 +             else reflexive tm
   7.300 +         end)
   7.301 +        handle CTERM _ =>
   7.302 +          (let val vr = powvar r
   7.303 +               val  ord = vorder vl vr
   7.304 +          in if ord = 0 then powvar_mul_conv tm
   7.305 +              else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
   7.306 +              else reflexive tm
   7.307 +          end)) end))
   7.308 +  in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
   7.309 +             end
   7.310 +  end;
   7.311 +(* Multiplication by monomial of a polynomial.                               *)
   7.312 +
   7.313 + val polynomial_monomial_mul_conv =
   7.314 +  let
   7.315 +   fun pmm_conv tm =
   7.316 +    let val (l,r) = dest_mul tm
   7.317 +    in
   7.318 +    ((let val (y,z) = dest_add r
   7.319 +          val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
   7.320 +          val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.321 +          val (tm3,tm4) = Thm.dest_comb tm1
   7.322 +          val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
   7.323 +      in transitive th1 th2
   7.324 +      end)
   7.325 +     handle CTERM _ => monomial_mul_conv tm)
   7.326 +   end
   7.327 + in pmm_conv
   7.328 + end;
   7.329 +
   7.330 +(* Addition of two monomials identical except for constant multiples.        *)
   7.331 +
   7.332 +fun monomial_add_conv tm =
   7.333 + let val (l,r) = dest_add tm
   7.334 + in if is_semiring_constant l andalso is_semiring_constant r
   7.335 +    then semiring_add_conv tm
   7.336 +    else
   7.337 +     let val th1 =
   7.338 +           if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l)
   7.339 +           then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then
   7.340 +                    inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02
   7.341 +                else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03
   7.342 +           else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r)
   7.343 +           then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04
   7.344 +           else inst_thm [(cm,r)] pthm_05
   7.345 +         val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.346 +         val (tm3,tm4) = Thm.dest_comb tm1
   7.347 +         val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
   7.348 +         val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
   7.349 +         val tm5 = concl th3
   7.350 +      in
   7.351 +      if (Thm.dest_arg1 tm5) aconvc zero_tm
   7.352 +      then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
   7.353 +      else monomial_deone th3
   7.354 +     end
   7.355 + end;
   7.356 +
   7.357 +(* Ordering on monomials.                                                    *)
   7.358 +
   7.359 +fun striplist dest =
   7.360 + let fun strip x acc =
   7.361 +   ((let val (l,r) = dest x in
   7.362 +        strip l (strip r acc) end)
   7.363 +    handle CTERM _ => x::acc)    (* FIXME !? *)
   7.364 + in fn x => strip x []
   7.365 + end;
   7.366 +
   7.367 +
   7.368 +fun powervars tm =
   7.369 + let val ptms = striplist dest_mul tm
   7.370 + in if is_semiring_constant (hd ptms) then tl ptms else ptms
   7.371 + end;
   7.372 +val num_0 = 0;
   7.373 +val num_1 = 1;
   7.374 +fun dest_varpow tm =
   7.375 + ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end)
   7.376 +   handle CTERM _ =>
   7.377 +   (tm,(if is_semiring_constant tm then num_0 else num_1)));
   7.378 +
   7.379 +val morder =
   7.380 + let fun lexorder l1 l2 =
   7.381 +  case (l1,l2) of
   7.382 +    ([],[]) => 0
   7.383 +  | (vps,[]) => ~1
   7.384 +  | ([],vps) => 1
   7.385 +  | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
   7.386 +     if variable_order x1 x2 then 1
   7.387 +     else if variable_order x2 x1 then ~1
   7.388 +     else if n1 < n2 then ~1
   7.389 +     else if n2 < n1 then 1
   7.390 +     else lexorder vs1 vs2
   7.391 + in fn tm1 => fn tm2 =>
   7.392 +  let val vdegs1 = map dest_varpow (powervars tm1)
   7.393 +      val vdegs2 = map dest_varpow (powervars tm2)
   7.394 +      val deg1 = fold_rev ((curry (op +)) o snd) vdegs1 num_0
   7.395 +      val deg2 = fold_rev ((curry (op +)) o snd) vdegs2 num_0
   7.396 +  in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
   7.397 +                            else lexorder vdegs1 vdegs2
   7.398 +  end
   7.399 + end;
   7.400 +
   7.401 +(* Addition of two polynomials.                                              *)
   7.402 +
   7.403 +val polynomial_add_conv =
   7.404 + let
   7.405 + fun dezero_rule th =
   7.406 +  let
   7.407 +   val tm = concl th
   7.408 +  in
   7.409 +   if not(is_add tm) then th else
   7.410 +   let val (lopr,r) = Thm.dest_comb tm
   7.411 +       val l = Thm.dest_arg lopr
   7.412 +   in
   7.413 +    if l aconvc zero_tm
   7.414 +    then transitive th (inst_thm [(ca,r)] pthm_07)   else
   7.415 +        if r aconvc zero_tm
   7.416 +        then transitive th (inst_thm [(ca,l)] pthm_08)  else th
   7.417 +   end
   7.418 +  end
   7.419 + fun padd tm =
   7.420 +  let
   7.421 +   val (l,r) = dest_add tm
   7.422 +  in
   7.423 +   if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07
   7.424 +   else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08
   7.425 +   else
   7.426 +    if is_add l
   7.427 +    then
   7.428 +     let val (a,b) = dest_add l
   7.429 +     in
   7.430 +     if is_add r then
   7.431 +      let val (c,d) = dest_add r
   7.432 +          val ord = morder a c
   7.433 +      in
   7.434 +       if ord = 0 then
   7.435 +        let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23
   7.436 +            val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.437 +            val (tm3,tm4) = Thm.dest_comb tm1
   7.438 +            val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
   7.439 +        in dezero_rule (transitive th1 (combination th2 (padd tm2)))
   7.440 +        end
   7.441 +       else (* ord <> 0*)
   7.442 +        let val th1 =
   7.443 +                if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   7.444 +                else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   7.445 +            val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.446 +        in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   7.447 +        end
   7.448 +      end
   7.449 +     else (* not (is_add r)*)
   7.450 +      let val ord = morder a r
   7.451 +      in
   7.452 +       if ord = 0 then
   7.453 +        let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26
   7.454 +            val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.455 +            val (tm3,tm4) = Thm.dest_comb tm1
   7.456 +            val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   7.457 +        in dezero_rule (transitive th1 th2)
   7.458 +        end
   7.459 +       else (* ord <> 0*)
   7.460 +        if ord > 0 then
   7.461 +          let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   7.462 +              val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.463 +          in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   7.464 +          end
   7.465 +        else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   7.466 +      end
   7.467 +    end
   7.468 +   else (* not (is_add l)*)
   7.469 +    if is_add r then
   7.470 +      let val (c,d) = dest_add r
   7.471 +          val  ord = morder l c
   7.472 +      in
   7.473 +       if ord = 0 then
   7.474 +         let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28
   7.475 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.476 +             val (tm3,tm4) = Thm.dest_comb tm1
   7.477 +             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   7.478 +         in dezero_rule (transitive th1 th2)
   7.479 +         end
   7.480 +       else
   7.481 +        if ord > 0 then reflexive tm
   7.482 +        else
   7.483 +         let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   7.484 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.485 +         in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   7.486 +         end
   7.487 +      end
   7.488 +    else
   7.489 +     let val ord = morder l r
   7.490 +     in
   7.491 +      if ord = 0 then monomial_add_conv tm
   7.492 +      else if ord > 0 then dezero_rule(reflexive tm)
   7.493 +      else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   7.494 +     end
   7.495 +  end
   7.496 + in padd
   7.497 + end;
   7.498 +
   7.499 +(* Multiplication of two polynomials.                                        *)
   7.500 +
   7.501 +val polynomial_mul_conv =
   7.502 + let
   7.503 +  fun pmul tm =
   7.504 +   let val (l,r) = dest_mul tm
   7.505 +   in
   7.506 +    if not(is_add l) then polynomial_monomial_mul_conv tm
   7.507 +    else
   7.508 +     if not(is_add r) then
   7.509 +      let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
   7.510 +      in transitive th1 (polynomial_monomial_mul_conv(concl th1))
   7.511 +      end
   7.512 +     else
   7.513 +       let val (a,b) = dest_add l
   7.514 +           val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10
   7.515 +           val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.516 +           val (tm3,tm4) = Thm.dest_comb tm1
   7.517 +           val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
   7.518 +           val th3 = transitive th1 (combination th2 (pmul tm2))
   7.519 +       in transitive th3 (polynomial_add_conv (concl th3))
   7.520 +       end
   7.521 +   end
   7.522 + in fn tm =>
   7.523 +   let val (l,r) = dest_mul tm
   7.524 +   in
   7.525 +    if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11
   7.526 +    else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12
   7.527 +    else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13
   7.528 +    else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14
   7.529 +    else pmul tm
   7.530 +   end
   7.531 + end;
   7.532 +
   7.533 +(* Power of polynomial (optimized for the monomial and trivial cases).       *)
   7.534 +
   7.535 +val Succ = @{cterm "Suc"};
   7.536 +val num_conv = fn n =>
   7.537 +        nat_add_conv (Thm.capply (Succ) (mk_cnumber @{ctyp "nat"} ((dest_numeral n) - 1)))
   7.538 +                     |> Thm.symmetric;
   7.539 +
   7.540 +
   7.541 +val polynomial_pow_conv =
   7.542 + let
   7.543 +  fun ppow tm =
   7.544 +    let val (l,n) = dest_pow tm
   7.545 +    in
   7.546 +     if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35
   7.547 +     else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36
   7.548 +     else
   7.549 +         let val th1 = num_conv n
   7.550 +             val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
   7.551 +             val (tm1,tm2) = Thm.dest_comb(concl th2)
   7.552 +             val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
   7.553 +             val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
   7.554 +         in transitive th4 (polynomial_mul_conv (concl th4))
   7.555 +         end
   7.556 +    end
   7.557 + in fn tm =>
   7.558 +       if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm
   7.559 + end;
   7.560 +
   7.561 +(* Negation.                                                                 *)
   7.562 +
   7.563 +val polynomial_neg_conv =
   7.564 + fn tm =>
   7.565 +   let val (l,r) = Thm.dest_comb tm in
   7.566 +        if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
   7.567 +        let val th1 = inst_thm [(cx',r)] neg_mul
   7.568 +            val th2 = transitive th1 (arg1_conv semiring_mul_conv (concl th1))
   7.569 +        in transitive th2 (polynomial_monomial_mul_conv (concl th2))
   7.570 +        end
   7.571 +   end;
   7.572 +
   7.573 +
   7.574 +(* Subtraction.                                                              *)
   7.575 +val polynomial_sub_conv = fn tm =>
   7.576 +  let val (l,r) = dest_sub tm
   7.577 +      val th1 = inst_thm [(cx',l),(cy',r)] sub_add
   7.578 +      val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.579 +      val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
   7.580 +  in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
   7.581 +  end;
   7.582 +
   7.583 +(* Conversion from HOL term.                                                 *)
   7.584 +
   7.585 +fun polynomial_conv tm =
   7.586 + if not(is_comb tm) orelse is_semiring_constant tm
   7.587 + then reflexive tm
   7.588 + else
   7.589 +  let val (lopr,r) = Thm.dest_comb tm
   7.590 +  in if lopr aconvc neg_tm then
   7.591 +       let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   7.592 +       in transitive th1 (polynomial_neg_conv (concl th1))
   7.593 +       end
   7.594 +     else
   7.595 +       if not(is_comb lopr) then reflexive tm
   7.596 +       else
   7.597 +         let val (opr,l) = Thm.dest_comb lopr
   7.598 +         in if opr aconvc pow_tm andalso is_numeral r
   7.599 +            then
   7.600 +              let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
   7.601 +              in transitive th1 (polynomial_pow_conv (concl th1))
   7.602 +              end
   7.603 +            else
   7.604 +              if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
   7.605 +              then
   7.606 +               let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
   7.607 +                   val f = if opr aconvc add_tm then polynomial_add_conv
   7.608 +                      else if opr aconvc mul_tm then polynomial_mul_conv
   7.609 +                      else polynomial_sub_conv
   7.610 +               in transitive th1 (f (concl th1))
   7.611 +               end
   7.612 +              else reflexive tm
   7.613 +         end
   7.614 +  end;
   7.615 + in
   7.616 +   {main = polynomial_conv,
   7.617 +    add = polynomial_add_conv,
   7.618 +    mul = polynomial_mul_conv,
   7.619 +    pow = polynomial_pow_conv,
   7.620 +    neg = polynomial_neg_conv,
   7.621 +    sub = polynomial_sub_conv}
   7.622 + end
   7.623 +end;
   7.624 +
   7.625 +val nat_arith = @{thms "nat_arith"};
   7.626 +val nat_exp_ss = HOL_basic_ss addsimps (nat_number @ nat_arith @ arith_simps @ rel_simps)
   7.627 +                              addsimps [Let_def, if_False, if_True, add_0, add_Suc];
   7.628 +
   7.629 +fun semiring_normalize_wrapper ({vars, semiring, ring, idom}, 
   7.630 +                                     {conv, dest_const, mk_const, is_const}) =
   7.631 +  let
   7.632 +    fun ord t u = Term.term_ord (term_of t, term_of u) = LESS
   7.633 +
   7.634 +    val pow_conv =
   7.635 +      arg_conv (Simplifier.rewrite nat_exp_ss)
   7.636 +      then_conv Simplifier.rewrite
   7.637 +        (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
   7.638 +      then_conv conv
   7.639 +    val dat = (is_const, conv, conv, pow_conv)
   7.640 +    val {main, ...} = semiring_normalizers_conv vars semiring ring dat ord
   7.641 +  in main end;
   7.642 +
   7.643 +fun semiring_normalize_conv ctxt tm =
   7.644 +  (case NormalizerData.match ctxt tm of
   7.645 +    NONE => reflexive tm
   7.646 +  | SOME res => semiring_normalize_wrapper res tm);
   7.647 +
   7.648 +
   7.649 +fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) =>
   7.650 +  rtac (semiring_normalize_conv ctxt
   7.651 +    (cterm_of (ProofContext.theory_of ctxt) (fst (Logic.dest_equals goal)))) i);
   7.652 +end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Tue Jun 05 16:26:04 2007 +0200
     8.3 @@ -0,0 +1,200 @@
     8.4 +(*  Title:      HOL/Tools/Groebner_Basis/normalizer_data.ML
     8.5 +    ID:         $Id$
     8.6 +    Author:     Amine Chaieb, TU Muenchen
     8.7 +
     8.8 +Ring normalization data.
     8.9 +*)
    8.10 +
    8.11 +signature NORMALIZER_DATA =
    8.12 +sig
    8.13 +  type entry
    8.14 +  val get: Proof.context -> (thm * entry) list
    8.15 +  val match: Proof.context -> cterm -> entry option
    8.16 +  val del: attribute
    8.17 +  val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list}
    8.18 +    -> attribute
    8.19 +  val funs: thm -> {is_const: morphism -> cterm -> bool,
    8.20 +    dest_const: morphism -> cterm -> Rat.rat,
    8.21 +    mk_const: morphism -> ctyp -> Rat.rat -> cterm,
    8.22 +    conv: morphism -> cterm -> thm} -> morphism -> Context.generic -> Context.generic
    8.23 +  val setup: theory -> theory
    8.24 +end;
    8.25 +
    8.26 +structure NormalizerData: NORMALIZER_DATA =
    8.27 +struct
    8.28 +
    8.29 +(* data *)
    8.30 +
    8.31 +type entry =
    8.32 + {vars: cterm list,
    8.33 +  semiring: cterm list * thm list,
    8.34 +  ring: cterm list * thm list,
    8.35 +  idom: thm list} *
    8.36 + {is_const: cterm -> bool,
    8.37 +  dest_const: cterm -> Rat.rat,
    8.38 +  mk_const: ctyp -> Rat.rat -> cterm,
    8.39 +  conv: cterm -> thm};
    8.40 +
    8.41 +val eq_key = Thm.eq_thm;
    8.42 +fun eq_data arg = eq_fst eq_key arg;
    8.43 +
    8.44 +structure Data = GenericDataFun
    8.45 +(
    8.46 +  val name = "HOL/norm";
    8.47 +  type T = (thm * entry) list;
    8.48 +  val empty = [];
    8.49 +  val extend = I;
    8.50 +  fun merge _ = AList.merge eq_key (K true);
    8.51 +  fun print _ _ = ();
    8.52 +);
    8.53 +
    8.54 +val get = Data.get o Context.Proof;
    8.55 +
    8.56 +
    8.57 +(* match data *)
    8.58 +
    8.59 +fun match ctxt tm =
    8.60 +  let
    8.61 +    fun match_inst
    8.62 +        ({vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom},
    8.63 +         fns as {is_const, dest_const, mk_const, conv}) pat =
    8.64 +       let
    8.65 +        fun h instT =
    8.66 +          let
    8.67 +            val substT = Thm.instantiate (instT, []);
    8.68 +            val substT_cterm = Drule.cterm_rule substT;
    8.69 +
    8.70 +            val vars' = map substT_cterm vars;
    8.71 +            val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
    8.72 +            val ring' = (map substT_cterm r_ops, map substT r_rules);
    8.73 +            val idom' = map substT idom;
    8.74 +
    8.75 +            val result = ({vars = vars', semiring = semiring', ring = ring', idom = idom'}, fns);
    8.76 +          in SOME result end
    8.77 +      in (case try Thm.match (pat, tm) of
    8.78 +           NONE => NONE
    8.79 +         | SOME (instT, _) => h instT)
    8.80 +      end;
    8.81 +
    8.82 +    fun match_struct (_,
    8.83 +        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), ...}, _): entry) =
    8.84 +      get_first (match_inst entry) (sr_ops @ r_ops);
    8.85 +  in get_first match_struct (get ctxt) end;
    8.86 +
    8.87 +
    8.88 +(* logical content *)
    8.89 +
    8.90 +val semiringN = "semiring";
    8.91 +val ringN = "ring";
    8.92 +val idomN = "idom";
    8.93 +
    8.94 +fun undefined _ = raise Match;
    8.95 +
    8.96 +fun del_data key = remove eq_data (key, []);
    8.97 +
    8.98 +val del = Thm.declaration_attribute (Data.map o del_data);
    8.99 +
   8.100 +fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom} =
   8.101 +  Thm.declaration_attribute (fn key => fn context => context |> Data.map
   8.102 +    let
   8.103 +      val ctxt = Context.proof_of context;
   8.104 +
   8.105 +      fun check kind name xs n =
   8.106 +        null xs orelse length xs = n orelse
   8.107 +        error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
   8.108 +      val check_ops = check "operations";
   8.109 +      val check_rules = check "rules";
   8.110 +
   8.111 +      val _ =
   8.112 +        check_ops semiringN sr_ops 5 andalso
   8.113 +        check_rules semiringN sr_rules 37 andalso
   8.114 +        check_ops ringN r_ops 2 andalso
   8.115 +        check_rules ringN r_rules 2 andalso
   8.116 +        check_rules idomN idom 2;
   8.117 +
   8.118 +      val mk_meta = LocalDefs.meta_rewrite_rule ctxt;
   8.119 +      val sr_rules' = map mk_meta sr_rules;
   8.120 +      val r_rules' = map mk_meta r_rules;
   8.121 +
   8.122 +      fun rule i = nth sr_rules' (i - 1);
   8.123 +
   8.124 +      val (cx, cy) = Thm.dest_binop (hd sr_ops);
   8.125 +      val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   8.126 +      val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   8.127 +      val ((clx, crx), (cly, cry)) =
   8.128 +        rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   8.129 +      val ((ca, cb), (cc, cd)) =
   8.130 +        rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   8.131 +      val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
   8.132 +      val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
   8.133 +
   8.134 +      val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
   8.135 +      val _ = map print_thm sr_rules';
   8.136 +      val semiring = (sr_ops, sr_rules');
   8.137 +      val ring = (r_ops, r_rules');
   8.138 +    in
   8.139 +      del_data key #>
   8.140 +      cons (key, ({vars = vars, semiring = semiring, ring = ring, idom = idom},
   8.141 +        {is_const = undefined, dest_const = undefined, mk_const = undefined,
   8.142 +          conv = undefined}))
   8.143 +    end);
   8.144 +
   8.145 +
   8.146 +(* extra-logical functions *)
   8.147 +
   8.148 +fun funs raw_key {is_const, dest_const, mk_const, conv} phi = Data.map (fn data =>
   8.149 +  let
   8.150 +    val key = Morphism.thm phi raw_key;
   8.151 +    val _ = AList.defined eq_key data key orelse
   8.152 +      raise THM ("No data entry for structure key", 0, [key]);
   8.153 +    val fns = {is_const = is_const phi, dest_const = dest_const phi,
   8.154 +      mk_const = mk_const phi, conv = conv phi};
   8.155 +  in AList.map_entry eq_key key (apsnd (K fns)) data end);
   8.156 +
   8.157 +
   8.158 +(* concrete syntax *)
   8.159 +
   8.160 +local
   8.161 +
   8.162 +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   8.163 +fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
   8.164 +fun keyword3 k1 k2 k3 =
   8.165 +  Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
   8.166 +
   8.167 +val opsN = "ops";
   8.168 +val rulesN = "rules";
   8.169 +
   8.170 +val normN = "norm";
   8.171 +val constN = "const";
   8.172 +val delN = "del";
   8.173 +
   8.174 +val any_keyword =
   8.175 +  keyword2 semiringN opsN || keyword2 semiringN rulesN ||
   8.176 +  keyword2 ringN opsN || keyword2 ringN rulesN ||
   8.177 +  keyword2 idomN rulesN;
   8.178 +
   8.179 +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   8.180 +val terms = thms >> map Drule.dest_term;
   8.181 +
   8.182 +fun optional scan = Scan.optional scan [];
   8.183 +
   8.184 +in
   8.185 +
   8.186 +fun att_syntax src = src |> Attrib.syntax
   8.187 +  (Scan.lift (Args.$$$ delN >> K del) ||
   8.188 +    ((keyword2 semiringN opsN |-- terms) --
   8.189 +     (keyword2 semiringN rulesN |-- thms)) --
   8.190 +    (optional (keyword2 ringN opsN |-- terms) --
   8.191 +     optional (keyword2 ringN rulesN |-- thms)) --
   8.192 +    optional (keyword2 idomN rulesN |-- thms)
   8.193 +    >> (fn ((sr, r), id) => add {semiring = sr, ring = r, idom = id}));
   8.194 +
   8.195 +end;
   8.196 +
   8.197 +
   8.198 +(* theory setup *)
   8.199 +
   8.200 +val setup =
   8.201 +  Attrib.add_attributes [("normalizer", att_syntax, "semiring normalizer data")];
   8.202 +
   8.203 +end;