Semiring normalization and Groebner Bases.
--- a/CONTRIBUTORS Tue Jun 05 15:17:02 2007 +0200
+++ b/CONTRIBUTORS Tue Jun 05 16:26:04 2007 +0200
@@ -1,6 +1,9 @@
-Contributions to Isabelle
--------------------------
+Contributions to Isabelle 2007
+------------------------------
+
+* June 2007: Amine Chaieb, TUM
+ Semiring normalization and Groebner Bases
* 2006/2007: Florian Haftmann, TUM
Pure: generic code generator framework.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Groebner_Basis.thy Tue Jun 05 16:26:04 2007 +0200
@@ -0,0 +1,416 @@
+(* Title: HOL/Groebner_Basis.thy
+ ID: $Id$
+ Author: Amine Chaieb, TU Muenchen
+*)
+
+header {* Semiring normalization and Groebner Bases *}
+
+theory Groebner_Basis
+imports NatBin
+uses
+ "Tools/Groebner_Basis/misc.ML"
+ "Tools/Groebner_Basis/normalizer_data.ML"
+ ("Tools/Groebner_Basis/normalizer.ML")
+begin
+
+subsection {* Semiring normalization *}
+
+setup NormalizerData.setup
+
+
+locale semiring =
+ fixes add mul pwr r0 r1
+ assumes add_a:"(add x (add y z) = add (add x y) z)"
+ and add_c: "add x y = add y x" and add_0:"add r0 x = x"
+ and mul_a:"mul x (mul y z) = mul (mul x y) z" and mul_c:"mul x y = mul y x"
+ and mul_1:"mul r1 x = x" and mul_0:"mul r0 x = r0"
+ and mul_d:"mul x (add y z) = add (mul x y) (mul x z)"
+ and pwr_0:"pwr x 0 = r1" and pwr_Suc:"pwr x (Suc n) = mul x (pwr x n)"
+begin
+
+lemma mul_pwr:"mul (pwr x p) (pwr x q) = pwr x (p + q)"
+proof (induct p)
+ case 0
+ then show ?case by (auto simp add: pwr_0 mul_1)
+next
+ case Suc
+ from this [symmetric] show ?case
+ by (auto simp add: pwr_Suc mul_1 mul_a)
+qed
+
+lemma pwr_mul: "pwr (mul x y) q = mul (pwr x q) (pwr y q)"
+proof (induct q arbitrary: x y, auto simp add:pwr_0 pwr_Suc mul_1)
+ fix q x y
+ assume "\<And>x y. pwr (mul x y) q = mul (pwr x q) (pwr y q)"
+ have "mul (mul x y) (mul (pwr x q) (pwr y q)) = mul x (mul y (mul (pwr x q) (pwr y q)))"
+ by (simp add: mul_a)
+ also have "\<dots> = (mul (mul y (mul (pwr y q) (pwr x q))) x)" by (simp add: mul_c)
+ also have "\<dots> = (mul (mul y (pwr y q)) (mul (pwr x q) x))" by (simp add: mul_a)
+ finally show "mul (mul x y) (mul (pwr x q) (pwr y q)) =
+ mul (mul x (pwr x q)) (mul y (pwr y q))" by (simp add: mul_c)
+qed
+
+lemma pwr_pwr: "pwr (pwr x p) q = pwr x (p * q)"
+proof (induct p arbitrary: q)
+ case 0
+ show ?case using pwr_Suc mul_1 pwr_0 by (induct q) auto
+next
+ case Suc
+ thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc)
+qed
+
+
+subsubsection {* Declaring the abstract theory *}
+
+lemma semiring_ops:
+ includes meta_term_syntax
+ shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
+ and "TERM r0" and "TERM r1"
+ by rule+
+
+lemma semiring_rules:
+ "add (mul a m) (mul b m) = mul (add a b) m"
+ "add (mul a m) m = mul (add a r1) m"
+ "add m (mul a m) = mul (add a r1) m"
+ "add m m = mul (add r1 r1) m"
+ "add r0 a = a"
+ "add a r0 = a"
+ "mul a b = mul b a"
+ "mul (add a b) c = add (mul a c) (mul b c)"
+ "mul r0 a = r0"
+ "mul a r0 = r0"
+ "mul r1 a = a"
+ "mul a r1 = a"
+ "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)"
+ "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))"
+ "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)"
+ "mul (mul lx ly) rx = mul (mul lx rx) ly"
+ "mul (mul lx ly) rx = mul lx (mul ly rx)"
+ "mul lx (mul rx ry) = mul (mul lx rx) ry"
+ "mul lx (mul rx ry) = mul rx (mul lx ry)"
+ "add (add a b) (add c d) = add (add a c) (add b d)"
+ "add (add a b) c = add a (add b c)"
+ "add a (add c d) = add c (add a d)"
+ "add (add a b) c = add (add a c) b"
+ "add a c = add c a"
+ "add a (add c d) = add (add a c) d"
+ "mul (pwr x p) (pwr x q) = pwr x (p + q)"
+ "mul x (pwr x q) = pwr x (Suc q)"
+ "mul (pwr x q) x = pwr x (Suc q)"
+ "mul x x = pwr x 2"
+ "pwr (mul x y) q = mul (pwr x q) (pwr y q)"
+ "pwr (pwr x p) q = pwr x (p * q)"
+ "pwr x 0 = r1"
+ "pwr x 1 = x"
+ "mul x (add y z) = add (mul x y) (mul x z)"
+ "pwr x (Suc q) = mul x (pwr x q)"
+ "pwr x (2*n) = mul (pwr x n) (pwr x n)"
+ "pwr x (Suc (2*n)) = mul x (mul (pwr x n) (pwr x n))"
+proof -
+ show "add (mul a m) (mul b m) = mul (add a b) m" using mul_d mul_c by simp
+next show"add (mul a m) m = mul (add a r1) m" using mul_d mul_c mul_1 by simp
+next show "add m (mul a m) = mul (add a r1) m" using mul_c mul_d mul_1 add_c by simp
+next show "add m m = mul (add r1 r1) m" using mul_c mul_d mul_1 by simp
+next show "add r0 a = a" using add_0 by simp
+next show "add a r0 = a" using add_0 add_c by simp
+next show "mul a b = mul b a" using mul_c by simp
+next show "mul (add a b) c = add (mul a c) (mul b c)" using mul_c mul_d by simp
+next show "mul r0 a = r0" using mul_0 by simp
+next show "mul a r0 = r0" using mul_0 mul_c by simp
+next show "mul r1 a = a" using mul_1 by simp
+next show "mul a r1 = a" using mul_1 mul_c by simp
+next show "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)"
+ using mul_c mul_a by simp
+next show "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))"
+ using mul_a by simp
+next
+ have "mul (mul lx ly) (mul rx ry) = mul (mul rx ry) (mul lx ly)" by (rule mul_c)
+ also have "\<dots> = mul rx (mul ry (mul lx ly))" using mul_a by simp
+ finally
+ show "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)"
+ using mul_c by simp
+next show "mul (mul lx ly) rx = mul (mul lx rx) ly" using mul_c mul_a by simp
+next
+ show "mul (mul lx ly) rx = mul lx (mul ly rx)" by (simp add: mul_a)
+next show "mul lx (mul rx ry) = mul (mul lx rx) ry" by (simp add: mul_a )
+next show "mul lx (mul rx ry) = mul rx (mul lx ry)" by (simp add: mul_a,simp add: mul_c)
+next show "add (add a b) (add c d) = add (add a c) (add b d)"
+ using add_c add_a by simp
+next show "add (add a b) c = add a (add b c)" using add_a by simp
+next show "add a (add c d) = add c (add a d)"
+ apply (simp add: add_a) by (simp only: add_c)
+next show "add (add a b) c = add (add a c) b" using add_a add_c by simp
+next show "add a c = add c a" by (rule add_c)
+next show "add a (add c d) = add (add a c) d" using add_a by simp
+next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr)
+next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp
+next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp
+next show "mul x x = pwr x 2" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
+next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
+next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
+next show "pwr x 0 = r1" using pwr_0 .
+next show "pwr x 1 = x" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
+next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
+next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
+next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number mul_pwr)
+next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))"
+ by (simp add: nat_number pwr_Suc mul_pwr)
+qed
+
+
+lemma "axioms" [normalizer
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules]:
+ "semiring add mul pwr r0 r1" .
+
+end
+
+interpretation class_semiring: semiring
+ ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
+ by unfold_locales (auto simp add: ring_eq_simps power_Suc)
+
+lemmas nat_arith =
+ add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
+
+lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
+ by (simp add: numeral_1_eq_1)
+lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False
+ if_True add_0 add_Suc add_number_of_left mult_number_of_left
+ numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
+ numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1
+ iszero_number_of_1 iszero_number_of_0 nonzero_number_of_Min
+ iszero_number_of_Pls iszero_0 not_iszero_Numeral1
+
+lemmas semiring_norm = comp_arith
+
+ML {*
+ fun numeral_is_const ct =
+ can HOLogic.dest_number (Thm.term_of ct);
+
+ val numeral_conv =
+ Conv.then_conv (Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}),
+ Simplifier.rewrite (HOL_basic_ss addsimps
+ [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}));
+*}
+
+ML {*
+ fun int_of_rat x =
+ (case Rat.quotient_of_rat x of (i, 1) => i
+ | _ => error "int_of_rat: bad int")
+*}
+
+declaration {*
+ NormalizerData.funs @{thm class_semiring.axioms}
+ {is_const = fn phi => numeral_is_const,
+ dest_const = fn phi => fn ct =>
+ Rat.rat_of_int (snd
+ (HOLogic.dest_number (Thm.term_of ct)
+ handle TERM _ => error "ring_dest_const")),
+ mk_const = fn phi => fn cT => fn x =>
+ Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
+ conv = fn phi => numeral_conv}
+*}
+
+
+locale ring = semiring +
+ fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ and neg :: "'a \<Rightarrow> 'a"
+ assumes neg_mul: "neg x = mul (neg r1) x"
+ and sub_add: "sub x y = add x (neg y)"
+begin
+
+lemma ring_ops:
+ includes meta_term_syntax
+ shows "TERM (sub x y)" and "TERM (neg x)" .
+
+lemmas ring_rules = neg_mul sub_add
+
+lemma "axioms" [normalizer
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ ring ops: ring_ops
+ ring rules: ring_rules]:
+ "ring add mul pwr r0 r1 sub neg" .
+
+end
+
+
+interpretation class_ring: ring ["op +" "op *" "op ^"
+ "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
+ by unfold_locales simp_all
+
+
+declaration {*
+ NormalizerData.funs @{thm class_ring.axioms}
+ {is_const = fn phi => numeral_is_const,
+ dest_const = fn phi => fn ct =>
+ Rat.rat_of_int (snd
+ (HOLogic.dest_number (Thm.term_of ct)
+ handle TERM _ => error "ring_dest_const")),
+ mk_const = fn phi => fn cT => fn x =>
+ Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
+ conv = fn phi => numeral_conv}
+*}
+
+use "Tools/Groebner_Basis/normalizer.ML"
+
+method_setup sring_norm = {*
+ Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt))
+*} "Semiring_normalizer"
+
+
+subsection {* Gröbner Bases *}
+
+locale semiringb = semiring +
+ assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z"
+ and add_mul_solve: "add (mul w y) (mul x z) =
+ add (mul w z) (mul x y) \<longleftrightarrow> w = x \<or> y = z"
+begin
+
+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)"
+proof-
+ have "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> \<not> (a = b \<or> c = d)" by simp
+ also have "\<dots> \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
+ using add_mul_solve by blast
+ 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)"
+ by simp
+qed
+
+lemma add_scale_eq_noteq: "\<lbrakk>r \<noteq> r0 ; (a = b) \<and> ~(c = d)\<rbrakk>
+ \<Longrightarrow> add a (mul r c) \<noteq> add b (mul r d)"
+proof(clarify)
+ assume nz: "r\<noteq> r0" and cnd: "c\<noteq>d"
+ and eq: "add b (mul r c) = add b (mul r d)"
+ hence "mul r c = mul r d" using cnd add_cancel by simp
+ hence "add (mul r0 d) (mul r c) = add (mul r0 c) (mul r d)"
+ using mul_0 add_cancel by simp
+ thus "False" using add_mul_solve nz cnd by simp
+qed
+
+declare "axioms" [normalizer del]
+
+lemma "axioms" [normalizer
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ idom rules: noteq_reduce add_scale_eq_noteq]:
+ "semiringb add mul pwr r0 r1" .
+
+end
+
+locale ringb = semiringb + ring
+begin
+
+declare "axioms" [normalizer del]
+
+lemma "axioms" [normalizer
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ ring ops: ring_ops
+ ring rules: ring_rules
+ idom rules: noteq_reduce add_scale_eq_noteq]:
+ "ringb add mul pwr r0 r1 sub neg" .
+
+end
+
+lemma no_zero_divirors_neq0:
+ assumes az: "(a::'a::no_zero_divisors) \<noteq> 0"
+ and ab: "a*b = 0" shows "b = 0"
+proof -
+ { assume bz: "b \<noteq> 0"
+ from no_zero_divisors [OF az bz] ab have False by blast }
+ thus "b = 0" by blast
+qed
+
+interpretation class_ringb: ringb
+ ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"]
+proof(unfold_locales, simp add: ring_eq_simps power_Suc, auto)
+ fix w x y z ::"'a::{idom,recpower,number_ring}"
+ assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
+ hence ynz': "y - z \<noteq> 0" by simp
+ from p have "w * y + x* z - w*z - x*y = 0" by simp
+ hence "w* (y - z) - x * (y - z) = 0" by (simp add: ring_eq_simps)
+ hence "(y - z) * (w - x) = 0" by (simp add: ring_eq_simps)
+ with no_zero_divirors_neq0 [OF ynz']
+ have "w - x = 0" by blast
+ thus "w = x" by simp
+qed
+
+
+declaration {*
+ NormalizerData.funs @{thm class_ringb.axioms}
+ {is_const = fn phi => numeral_is_const,
+ dest_const = fn phi => fn ct =>
+ Rat.rat_of_int (snd
+ (HOLogic.dest_number (Thm.term_of ct)
+ handle TERM _ => error "ring_dest_const")),
+ mk_const = fn phi => fn cT => fn x =>
+ Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
+ conv = fn phi => numeral_conv}
+*}
+
+
+interpretation natgb: semiringb
+ ["op +" "op *" "op ^" "0::nat" "1"]
+proof (unfold_locales, simp add: ring_eq_simps power_Suc)
+ fix w x y z ::"nat"
+ { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
+ hence "y < z \<or> y > z" by arith
+ moreover {
+ assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto)
+ then obtain k where kp: "k>0" and yz:"z = y + k" by blast
+ from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz ring_eq_simps)
+ hence "x*k = w*k" by simp
+ hence "w = x" using kp by (simp add: mult_cancel2) }
+ moreover {
+ assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto)
+ then obtain k where kp: "k>0" and yz:"y = z + k" by blast
+ from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz ring_eq_simps)
+ hence "w*k = x*k" by simp
+ hence "w = x" using kp by (simp add: mult_cancel2)}
+ ultimately have "w=x" by blast }
+ thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
+qed
+
+declaration {*
+ NormalizerData.funs @{thm natgb.axioms}
+ {is_const = fn phi => numeral_is_const,
+ dest_const = fn phi => fn ct =>
+ Rat.rat_of_int (snd
+ (HOLogic.dest_number (Thm.term_of ct)
+ handle TERM _ => error "ring_dest_const")),
+ mk_const = fn phi => fn cT => fn x =>
+ Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),
+ conv = fn phi => numeral_conv}
+*}
+
+
+lemmas bool_simps = simp_thms(1-34)
+lemma dnf:
+ "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
+ "(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"
+ by blast+
+
+lemmas weak_dnf_simps = dnf bool_simps
+
+lemma nnf_simps:
+ "(\<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)"
+ "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
+ by blast+
+
+lemma PFalse:
+ "P \<equiv> False \<Longrightarrow> \<not> P"
+ "\<not> P \<Longrightarrow> (P \<equiv> False)"
+ by auto
+
+use "Tools/Groebner_Basis/groebner.ML"
+
+ML {*
+ fun algebra_tac ctxt i = ObjectLogic.full_atomize_tac i THEN (fn st =>
+ rtac (Groebner.ring_conv ctxt (Thm.dest_arg (nth (cprems_of st) (i - 1)))) i st);
+*}
+
+method_setup algebra = {*
+ Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac)
+*} ""
+
+end
--- a/src/HOL/IsaMakefile Tue Jun 05 15:17:02 2007 +0200
+++ b/src/HOL/IsaMakefile Tue Jun 05 16:26:04 2007 +0200
@@ -85,23 +85,28 @@
ATP_Linkup.thy Accessible_Part.thy Datatype.thy \
Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.thy \
FixedPoint.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy \
- Inductive.thy IntArith.thy IntDef.thy IntDiv.thy Lattices.thy List.thy\
- Main.thy Map.thy Nat.ML Nat.thy NatBin.thy NatSimprocs.thy Numeral.thy\
- OrderedGroup.thy Orderings.thy Power.thy PreList.thy Predicate.thy \
- Presburger.thy Product_Type.thy ROOT.ML Recdef.thy Record.thy \
- Refute.thy Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy \
- Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/reduce_axiomsN.ML \
- Tools/ATP/watcher.ML Tools/Presburger/cooper_dec.ML \
- Tools/Presburger/cooper_proof.ML Tools/Presburger/presburger.ML \
- Tools/Presburger/qelim.ML Tools/Presburger/reflected_cooper.ML \
+ Inductive.thy IntArith.thy IntDef.thy IntDiv.thy Lattices.thy \
+ List.thy Main.thy Map.thy Nat.ML Nat.thy NatBin.thy NatSimprocs.thy \
+ Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy \
+ Predicate.thy Presburger.thy Product_Type.thy ROOT.ML Recdef.thy \
+ Record.thy Refute.thy Relation.thy Relation_Power.thy \
+ Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy \
+ Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML \
+ Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML \
+ Tools/Groebner_Basis/normalizer.ML \
+ Tools/Groebner_Basis/normalizer_data.ML \
+ Tools/Presburger/cooper_dec.ML Tools/Presburger/cooper_proof.ML \
+ Tools/Presburger/presburger.ML Tools/Presburger/qelim.ML \
+ Tools/Presburger/reflected_cooper.ML \
Tools/Presburger/reflected_presburger.ML Tools/TFL/dcterm.ML \
Tools/TFL/post.ML Tools/TFL/rules.ML Tools/TFL/tfl.ML \
Tools/TFL/thms.ML Tools/TFL/thry.ML Tools/TFL/usyntax.ML \
Tools/TFL/utils.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML \
- Tools/datatype_aux.ML Tools/datatype_case.ML Tools/datatype_codegen.ML\
- Tools/datatype_hooks.ML Tools/datatype_package.ML \
- Tools/datatype_prop.ML Tools/datatype_realizer.ML \
- Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML \
+ Tools/datatype_aux.ML Tools/datatype_case.ML \
+ Tools/datatype_codegen.ML Tools/datatype_hooks.ML \
+ Tools/datatype_package.ML Tools/datatype_prop.ML \
+ Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \
+ Tools/function_package/auto_term.ML \
Tools/function_package/context_tree.ML \
Tools/function_package/fundef_common.ML \
Tools/function_package/fundef_core.ML \
--- a/src/HOL/NatSimprocs.thy Tue Jun 05 15:17:02 2007 +0200
+++ b/src/HOL/NatSimprocs.thy Tue Jun 05 16:26:04 2007 +0200
@@ -6,7 +6,7 @@
header {*Simprocs for the Naturals*}
theory NatSimprocs
-imports NatBin
+imports Groebner_Basis
uses "int_factor_simprocs.ML" "nat_simprocs.ML"
begin
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Jun 05 16:26:04 2007 +0200
@@ -0,0 +1,743 @@
+(* Title: HOL/Tools/Groebner_Basis/groebner.ML
+ ID: $Id$
+ Author: Amine Chaieb, TU Muenchen
+*)
+
+signature GROEBNER =
+sig
+ val ring_and_ideal_conv :
+ {idom: thm list, ring: cterm list * thm list, vars: cterm list,
+ semiring: Thm.cterm list * thm list} ->
+ (Thm.cterm -> Rat.rat) -> (Rat.rat -> Thm.cterm) ->
+ Conv.conv -> Conv.conv ->
+ Conv.conv * (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list)
+ val ring_conv : Proof.context -> cterm -> thm
+end
+
+structure Groebner: GROEBNER =
+struct
+open Normalizer;
+open Misc;
+
+ (* FIXME :: Already present in Tools/Presburger/qelim.ML but is much more general!! *)
+fun cterm_frees ct =
+ let fun h acc t =
+ case (term_of t) of
+ _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
+ | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
+ | Free _ => insert (op aconvc) t acc
+ | _ => acc
+ in h [] ct end;
+
+fun assocd x al d = case AList.lookup (op =) al x of SOME y => y | NONE => d;
+val rat_0 = Rat.zero;
+val rat_1 = Rat.one;
+val minus_rat = Rat.neg;
+val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
+fun int_of_rat a =
+ case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int";
+val lcm_rat = fn x => fn y => Rat.rat_of_int (lcm (int_of_rat x, int_of_rat y));
+
+val (eqF_intr, eqF_elim) =
+ let val [th1,th2] = thms "PFalse"
+ in (fn th => th COMP th2, fn th => th COMP th1) end;
+
+val (PFalse, PFalse') =
+ let val PFalse_eq = nth (thms "simp_thms") 13
+ in (PFalse_eq RS iffD1, PFalse_eq RS iffD2) end;
+
+
+(* ------------------------------------------------------------------------- *)
+(* Type for recording history, i.e. how a polynomial was obtained. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype history =
+ Start of int
+ | Mmul of (Rat.rat * (int list)) * history
+ | Add of history * history;
+
+
+(* Monomial ordering. *)
+
+fun morder_lt m1 m2=
+ let fun lexorder l1 l2 =
+ case (l1,l2) of
+ ([],[]) => false
+ | (x1::o1,x2::o2) => x1 > x2 orelse x1 = x2 andalso lexorder o1 o2
+ | _ => error "morder: inconsistent monomial lengths"
+ val n1 = fold (curry op +) m1 0
+ val n2 = fold (curry op +) m2 0 in
+ n1 < n2 orelse n1 = n2 andalso lexorder m1 m2
+ end;
+
+fun morder_le m1 m2 = morder_lt m1 m2 orelse (m1 = m2);
+
+fun morder_gt m1 m2 = morder_lt m2 m1;
+
+(* Arithmetic on canonical polynomials. *)
+
+fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l;
+
+fun grob_add l1 l2 =
+ case (l1,l2) of
+ ([],l2) => l2
+ | (l1,[]) => l1
+ | ((c1,m1)::o1,(c2,m2)::o2) =>
+ if m1 = m2 then
+ let val c = c1+/c2 val rest = grob_add o1 o2 in
+ if c =/ rat_0 then rest else (c,m1)::rest end
+ else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
+ else (c2,m2)::(grob_add l1 o2);
+
+fun grob_sub l1 l2 = grob_add l1 (grob_neg l2);
+
+fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2,map2 (curry op +) m1 m2);
+
+fun grob_cmul cm pol = map (grob_mmul cm) pol;
+
+fun grob_mul l1 l2 =
+ case l1 of
+ [] => []
+ | (h1::t1) => grob_add (grob_cmul h1 l2) (grob_mul t1 l2);
+
+fun grob_inv l =
+ case l of
+ [(c,vs)] => if (forall (fn x => x = 0) vs) then
+ if (c =/ rat_0) then error "grob_inv: division by zero"
+ else [(rat_1 // c,vs)]
+ else error "grob_inv: non-constant divisor polynomial"
+ | _ => error "grob_inv: non-constant divisor polynomial";
+
+fun grob_div l1 l2 =
+ case l2 of
+ [(c,l)] => if (forall (fn x => x = 0) l) then
+ if c =/ rat_0 then error "grob_div: division by zero"
+ else grob_cmul (rat_1 // c,l) l1
+ else error "grob_div: non-constant divisor polynomial"
+ | _ => error "grob_div: non-constant divisor polynomial";
+
+fun grob_pow vars l n =
+ if n < 0 then error "grob_pow: negative power"
+ else if n = 0 then [(rat_1,map (fn v => 0) vars)]
+ else grob_mul l (grob_pow vars l (n - 1));
+
+val max = fn x => fn y => if x < y then y else x;
+
+fun degree vn p =
+ case p of
+ [] => error "Zero polynomial"
+| [(c,ns)] => nth ns vn
+| (c,ns)::p' => max (nth ns vn) (degree vn p');
+
+fun head_deg vn p = let val d = degree vn p in
+ (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;
+
+val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) 0) ns);
+val grob_pdiv =
+ let fun pdiv_aux vn (n,a) p k s =
+ if is_zerop s then (k,s) else
+ let val (m,b) = head_deg vn s
+ in if m < n then (k,s) else
+ let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m - n else 0)
+ (snd (hd s)))]
+ in if a = b then pdiv_aux vn (n,a) p k (grob_sub s p')
+ else pdiv_aux vn (n,a) p (k + 1) (grob_sub (grob_mul a s) (grob_mul b p'))
+ end
+ end
+ in fn vn => fn s => fn p => pdiv_aux vn (head_deg vn p) p 0 s
+ end;
+
+(* Monomial division operation. *)
+
+fun mdiv (c1,m1) (c2,m2) =
+ (c1//c2,
+ map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1-n2) m1 m2);
+
+(* Lowest common multiple of two monomials. *)
+
+fun mlcm (c1,m1) (c2,m2) = (rat_1,map2 max m1 m2);
+
+(* Reduce monomial cm by polynomial pol, returning replacement for cm. *)
+
+fun reduce1 cm (pol,hpol) =
+ case pol of
+ [] => error "reduce1"
+ | cm1::cms => ((let val (c,m) = mdiv cm cm1 in
+ (grob_cmul (minus_rat c,m) cms,
+ Mmul((minus_rat c,m),hpol)) end)
+ handle ERROR _ => error "reduce1");
+
+(* Try this for all polynomials in a basis. *)
+fun tryfind f l =
+ case l of
+ [] => error "tryfind"
+ | (h::t) => ((f h) handle ERROR _ => tryfind f t);
+
+fun reduceb cm basis = tryfind (fn p => reduce1 cm p) basis;
+
+(* Reduction of a polynomial (always picking largest monomial possible). *)
+
+fun reduce basis (pol,hist) =
+ case pol of
+ [] => (pol,hist)
+ | cm::ptl => ((let val (q,hnew) = reduceb cm basis in
+ reduce basis (grob_add q ptl,Add(hnew,hist)) end)
+ handle (ERROR _) =>
+ (let val (q,hist') = reduce basis (ptl,hist) in
+ (cm::q,hist') end));
+
+(* Check for orthogonality w.r.t. LCM. *)
+
+fun orthogonal l p1 p2 =
+ snd l = snd(grob_mmul (hd p1) (hd p2));
+
+(* Compute S-polynomial of two polynomials. *)
+
+fun spoly cm ph1 ph2 =
+ case (ph1,ph2) of
+ (([],h),p) => ([],h)
+ | (p,([],h)) => ([],h)
+ | ((cm1::ptl1,his1),(cm2::ptl2,his2)) =>
+ (grob_sub (grob_cmul (mdiv cm cm1) ptl1)
+ (grob_cmul (mdiv cm cm2) ptl2),
+ Add(Mmul(mdiv cm cm1,his1),
+ Mmul(mdiv (minus_rat(fst cm),snd cm) cm2,his2)));
+
+(* Make a polynomial monic. *)
+
+fun monic (pol,hist) =
+ if pol = [] then (pol,hist) else
+ let val (c',m') = hd pol in
+ (map (fn (c,m) => (c//c',m)) pol,
+ Mmul((rat_1 // c',map (K 0) m'),hist)) end;
+
+(* The most popular heuristic is to order critical pairs by LCM monomial. *)
+
+fun forder ((c1,m1),_) ((c2,m2),_) = morder_lt m1 m2;
+
+fun poly_lt p q =
+ case (p,q) of
+ (p,[]) => false
+ | ([],q) => true
+ | ((c1,m1)::o1,(c2,m2)::o2) =>
+ c1 </ c2 orelse
+ c1 =/ c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2);
+
+fun align ((p,hp),(q,hq)) =
+ if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
+fun forall2 p l1 l2 =
+ case (l1,l2) of
+ ([],[]) => true
+ | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
+ | _ => false;
+
+fun poly_eq p1 p2 =
+ forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso m1 = m2) p1 p2;
+
+fun memx ((p1,h1),(p2,h2)) ppairs =
+ not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
+
+(* Buchberger's second criterion. *)
+
+fun criterion2 basis (lcm,((p1,h1),(p2,h2))) opairs =
+ exists (fn g => not(poly_eq (fst g) p1) andalso not(poly_eq (fst g) p2) andalso
+ can (mdiv lcm) (hd(fst g)) andalso
+ not(memx (align (g,(p1,h1))) (map snd opairs)) andalso
+ not(memx (align (g,(p2,h2))) (map snd opairs))) basis;
+
+(* Test for hitting constant polynomial. *)
+
+fun constant_poly p =
+ length p = 1 andalso forall (fn x=>x=0) (snd(hd p));
+
+(* ------------------------------------------------------------------------- *)
+(* Grobner basis algorithm. *)
+(* ------------------------------------------------------------------------- *)
+(* FIXME: try to get rid of mergesort? *)
+fun merge ord l1 l2 =
+ case l1 of
+ [] => l2
+ | h1::t1 =>
+ case l2 of
+ [] => l1
+ | h2::t2 => if ord h1 h2 then h1::(merge ord t1 l2)
+ else h2::(merge ord l1 t2);
+fun mergesort ord l =
+ let
+ fun mergepairs l1 l2 =
+ case (l1,l2) of
+ ([s],[]) => s
+ | (l,[]) => mergepairs [] l
+ | (l,[s1]) => mergepairs (s1::l) []
+ | (l,(s1::s2::ss)) => mergepairs ((merge ord s1 s2)::l) ss
+ in if l = [] then [] else mergepairs [] (map (fn x => [x]) l)
+ end;
+
+
+fun grobner_basis basis pairs =
+ (writeln (Int.toString(length basis)^" basis elements and "^
+ Int.toString(length pairs)^" critical pairs");
+ case pairs of
+ [] => basis
+ | (l,(p1,p2))::opairs =>
+ let val (sph as (sp,hist)) = monic (reduce basis (spoly l p1 p2))
+ in if sp = [] orelse criterion2 basis (l,(p1,p2)) opairs
+ then grobner_basis basis opairs
+ else if constant_poly sp then grobner_basis (sph::basis) []
+ else let val rawcps = map (fn p => (mlcm (hd(fst p)) (hd sp),align(p,sph)))
+ basis
+ val newcps = filter
+ (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q)))
+ rawcps
+ in grobner_basis (sph::basis)
+ (merge forder opairs (mergesort forder newcps))
+ end
+ end);
+
+(* ------------------------------------------------------------------------- *)
+(* Interreduce initial polynomials. *)
+(* ------------------------------------------------------------------------- *)
+
+fun grobner_interreduce rpols ipols =
+ case ipols of
+ [] => map monic (rev rpols)
+ | p::ps => let val p' = reduce (rpols @ ps) p in
+ if fst p' = [] then grobner_interreduce rpols ps
+ else grobner_interreduce (p'::rpols) ps end;
+
+(* ------------------------------------------------------------------------- *)
+(* Overall function. *)
+(* ------------------------------------------------------------------------- *)
+
+fun grobner pols =
+ let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1))
+ val phists = filter (fn (p,_) => p <> []) npols
+ val bas = grobner_interreduce [] (map monic phists)
+ val prs0 = product bas bas
+ val prs1 = filter (fn ((x,_),(y,_)) => poly_lt x y) prs0
+ val prs2 = map (fn (p,q) => (mlcm (hd(fst p)) (hd(fst q)),(p,q))) prs1
+ val prs3 =
+ filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q))) prs2 in
+ grobner_basis bas (mergesort forder prs3) end;
+
+(* ------------------------------------------------------------------------- *)
+(* Get proof of contradiction from Grobner basis. *)
+(* ------------------------------------------------------------------------- *)
+fun find p l =
+ case l of
+ [] => error "find"
+ | (h::t) => if p(h) then h else find p t;
+
+fun grobner_refute pols =
+ let val gb = grobner pols in
+ snd(find (fn (p,h) => length p = 1 andalso forall (fn x=> x=0) (snd(hd p))) gb)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Turn proof into a certificate as sum of multipliers. *)
+(* *)
+(* In principle this is very inefficient: in a heavily shared proof it may *)
+(* make the same calculation many times. Could put in a cache or something. *)
+(* ------------------------------------------------------------------------- *)
+fun assoc x l = snd(find (fn p => fst p = x) l);
+
+fun resolve_proof vars prf =
+ case prf of
+ Start(~1) => []
+ | Start m => [(m,[(rat_1,map (K 0) vars)])]
+ | Mmul(pol,lin) =>
+ let val lis = resolve_proof vars lin in
+ map (fn (n,p) => (n,grob_cmul pol p)) lis end
+ | Add(lin1,lin2) =>
+ let val lis1 = resolve_proof vars lin1
+ val lis2 = resolve_proof vars lin2
+ val dom = distinct (op =) ((map fst lis1) union (map fst lis2))
+ in
+ map (fn n => let val a = ((assoc n lis1) handle _ => []) (* FIXME *)
+ val b = ((assoc n lis2) handle _ => []) in (* FIXME *)
+ (n,grob_add a b) end) dom end;
+
+(* ------------------------------------------------------------------------- *)
+(* Run the procedure and produce Weak Nullstellensatz certificate. *)
+(* ------------------------------------------------------------------------- *)
+fun grobner_weak vars pols =
+ let val cert = resolve_proof vars (grobner_refute pols)
+ val l =
+ fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in
+ (l,map (fn (i,p) => (i,map (fn (d,m) => (l*/d,m)) p)) cert) end;
+
+(* ------------------------------------------------------------------------- *)
+(* Prove a polynomial is in ideal generated by others, using Grobner basis. *)
+(* ------------------------------------------------------------------------- *)
+
+fun grobner_ideal vars pols pol =
+ let val (pol',h) = reduce (grobner pols) (grob_neg pol,Start(~1)) in
+ if pol <> [] then error "grobner_ideal: not in the ideal" else
+ resolve_proof vars h end;
+
+(* ------------------------------------------------------------------------- *)
+(* Produce Strong Nullstellensatz certificate for a power of pol. *)
+(* ------------------------------------------------------------------------- *)
+
+fun grobner_strong vars pols pol =
+ let val vars' = @{cterm "True"}::vars
+ val grob_z = [(rat_1,1::(map (fn x => 0) vars))]
+ val grob_1 = [(rat_1,(map (fn x => 0) vars'))]
+ fun augment p= map (fn (c,m) => (c,0::m)) p
+ val pols' = map augment pols
+ val pol' = augment pol
+ val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols'
+ val (l,cert) = grobner_weak vars' allpols
+ val d = fold_rev (fold_rev (max o hd o snd) o snd) cert 0
+ fun transform_monomial (c,m) =
+ grob_cmul (c,tl m) (grob_pow vars pol (d - hd m))
+ fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q []
+ val cert' = map (fn (c,q) => (c-1,transform_polynomial q))
+ (filter (fn (k,_) => k <> 0) cert) in
+ (d,l,cert') end;
+
+fun string_of_pol vars pol =
+ foldl (fn ((c,m),s) => ((Rat.string_of_rat c)
+ ^ "*(" ^
+ (snd (foldl
+ (fn (e,(i,s)) =>
+ (i+ 1,
+ (nth vars i
+ |>cterm_of (the_context())
+ |> string_of_cterm)^ "^"
+ ^ (Int.toString e) ^" * " ^ s)) (0,"0") m))
+ ^ ") + ") ^ s) "" pol;
+
+
+(* ------------------------------------------------------------------------- *)
+(* Overall parametrized universal procedure for (semi)rings. *)
+(* We return an ideal_conv and the actual ring prover. *)
+(* ------------------------------------------------------------------------- *)
+fun refute_disj rfn tm =
+ case term_of tm of
+ Const("op |",_)$l$r =>
+ Drule.compose_single(refute_disj rfn (Thm.dest_arg tm),2,Drule.compose_single(refute_disj rfn (Thm.dest_arg1 tm),2,disjE))
+ | _ => rfn tm ;
+
+val notnotD = @{thm "notnotD"};
+fun mk_binop ct x y =
+ Thm.capply (Thm.capply ct x) y
+
+val mk_comb = Thm.capply;
+fun is_neg t =
+ case term_of t of
+ (Const("Not",_)$p) => true
+ | _ => false;
+fun is_eq t =
+ case term_of t of
+ (Const("op =",_)$_$_) => true
+| _ => false;
+
+fun end_itlist f l =
+ case l of
+ [] => error "end_itlist"
+ | [x] => x
+ | (h::t) => f h (end_itlist f t);
+
+val list_mk_binop = fn b => end_itlist (mk_binop b);
+
+val list_dest_binop = fn b =>
+ let fun h acc t =
+ ((let val (l,r) = dest_binop b t in h (h acc r) l end)
+ handle CTERM _ => (t::acc)) (* Why had I handle _ => ? *)
+ in h []
+ end;
+
+val strip_exists =
+ let fun h (acc, t) =
+ case (term_of t) of
+ Const("Ex",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+ | _ => (acc,t)
+ in fn t => h ([],t)
+ end;
+
+fun is_forall t =
+ case term_of t of
+ (Const("All",_)$Abs(_,_,_)) => true
+| _ => false;
+
+val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
+val bool_simps = @{thms "bool_simps"};
+val nnf_simps = @{thms "nnf_simps"};
+val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps bool_simps addsimps nnf_simps)
+val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "weak_dnf_simps"}));
+val initial_conv =
+ Simplifier.rewrite
+ (HOL_basic_ss addsimps nnf_simps
+ addsimps [not_all, not_ex] addsimps map (fn th => th RS sym) (ex_simps @ all_simps));
+
+val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
+
+val cTrp = @{cterm "Trueprop"};
+val cConj = @{cterm "op &"};
+val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
+val ASSUME = mk_comb cTrp #> assume;
+val list_mk_conj = list_mk_binop cConj;
+val conjs = list_dest_binop cConj;
+val mk_neg = mk_comb cNot;
+
+
+
+(** main **)
+
+fun ring_and_ideal_conv
+ {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom}
+ dest_const mk_const ring_eq_conv ring_normalize_conv =
+let
+ val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
+ val [ring_add_tm, ring_mul_tm, ring_pow_tm] =
+ map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];
+
+ val (ring_sub_tm, ring_neg_tm) =
+ (case r_ops of
+ [] => (@{cterm "True"}, @{cterm "True"})
+ | [sub_pat, neg_pat] => (Thm.dest_fun (Thm.dest_fun sub_pat), Thm.dest_fun neg_pat));
+
+ val [idom_thm, neq_thm] = idom;
+
+ val ring_dest_neg =
+ fn t => let val (l,r) = Thm.dest_comb t in
+ if could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t])
+ end
+
+ val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
+(*
+ fun ring_dest_inv t =
+ let val (l,r) = Thm.dest_comb t in
+ if could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv"
+ end
+*)
+ val ring_dest_add = dest_binop ring_add_tm;
+ val ring_mk_add = mk_binop ring_add_tm;
+ val ring_dest_sub = dest_binop ring_sub_tm;
+ val ring_mk_sub = mk_binop ring_sub_tm;
+ val ring_dest_mul = dest_binop ring_mul_tm;
+ val ring_mk_mul = mk_binop ring_mul_tm;
+(* val ring_dest_div = dest_binop ring_div_tm;
+ val ring_mk_div = mk_binop ring_div_tm;*)
+ val ring_dest_pow = dest_binop ring_pow_tm;
+ val ring_mk_pow = mk_binop ring_pow_tm ;
+ fun grobvars tm acc =
+ if can dest_const tm then acc
+ else if can ring_dest_neg tm then grobvars (Thm.dest_arg tm) acc
+ else if can ring_dest_pow tm then grobvars (Thm.dest_arg1 tm) acc
+ else if can ring_dest_add tm orelse can ring_dest_sub tm
+ orelse can ring_dest_mul tm
+ then grobvars (Thm.dest_arg1 tm) (grobvars (Thm.dest_arg tm) acc)
+(* else if can ring_dest_inv tm
+ then
+ let val gvs = grobvars (Thm.dest_arg tm) [] in
+ if gvs = [] then acc else tm::acc
+ end
+ else if can ring_dest_div tm then
+ let val lvs = grobvars (Thm.dest_arg1 tm) acc
+ val gvs = grobvars (Thm.dest_arg tm) []
+ in if gvs = [] then lvs else tm::acc
+ end *)
+ else tm::acc ;
+
+fun grobify_term vars tm =
+((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
+ [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)])
+handle CTERM _ =>
+ ((let val x = dest_const tm
+ in if x =/ rat_0 then [] else [(x,map (fn v => 0) vars)]
+ end)
+ handle ERROR _ =>
+ ((grob_neg(grobify_term vars (ring_dest_neg tm)))
+ handle CTERM _ =>
+ (
+(* (grob_inv(grobify_term vars (ring_dest_inv tm)))
+ handle CTERM _ => *)
+ ((let val (l,r) = ring_dest_add tm
+ in grob_add (grobify_term vars l) (grobify_term vars r)
+ end)
+ handle CTERM _ =>
+ ((let val (l,r) = ring_dest_sub tm
+ in grob_sub (grobify_term vars l) (grobify_term vars r)
+ end)
+ handle CTERM _ =>
+ ((let val (l,r) = ring_dest_mul tm
+ in grob_mul (grobify_term vars l) (grobify_term vars r)
+ end)
+ handle CTERM _ =>
+ (
+(* (let val (l,r) = ring_dest_div tm
+ in grob_div (grobify_term vars l) (grobify_term vars r)
+ end)
+ handle CTERM _ => *)
+ ((let val (l,r) = ring_dest_pow tm
+ in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r)
+ end)
+ handle CTERM _ => error "grobify_term: unknown or invalid term")))))))));
+val eq_tm = idom_thm |> concl |> Thm.dest_arg |> Thm.dest_arg |> Thm.dest_fun |> Thm.dest_fun ;
+(*ring_integral |> hd |> concl |> Thm.dest_arg
+ |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_fun; *)
+val dest_eq = dest_binop eq_tm;
+
+fun grobify_equation vars tm =
+ let val (l,r) = dest_binop eq_tm tm
+ in grob_sub (grobify_term vars l) (grobify_term vars r)
+ end;
+
+fun grobify_equations tm =
+ let
+ val cjs = conjs tm
+ val rawvars = fold_rev (fn eq => fn a =>
+ grobvars (Thm.dest_arg1 eq) (grobvars (Thm.dest_arg eq) a)) cjs []
+ val vars = sort (fn (x, y) => Term.term_ord(term_of x,term_of y))
+ (distinct (op aconvc) rawvars)
+ in (vars,map (grobify_equation vars) cjs)
+ end;
+
+val holify_polynomial =
+ let fun holify_varpow (v,n) =
+ if n = 1 then v else ring_mk_pow v (mk_cnumber @{ctyp "nat"} n) (* FIXME *)
+ fun holify_monomial vars (c,m) =
+ let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
+ in end_itlist ring_mk_mul (mk_const c :: xps)
+ end
+ fun holify_polynomial vars p =
+ if p = [] then mk_const (rat_0)
+ else end_itlist ring_mk_add (map (holify_monomial vars) p)
+ in holify_polynomial
+ end ;
+val idom_rule = simplify (HOL_basic_ss addsimps [idom_thm]);
+fun prove_nz n = eqF_elim
+ (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const(rat_0))));
+val neq_01 = prove_nz (rat_1);
+fun neq_rule n th = [prove_nz n, th] MRS neq_thm;
+fun mk_add th1 = combination(Drule.arg_cong_rule ring_add_tm th1);
+
+fun refute tm =
+ if tm aconvc false_tm then ASSUME tm else
+ let
+ val (nths0,eths0) = List.partition (is_neg o concl) (conjuncts(ASSUME tm))
+ val nths = filter (is_eq o Thm.dest_arg o concl) nths0
+ val eths = filter (is_eq o concl) eths0
+ in
+ if null eths then
+ let
+ val th1 = end_itlist (fn th1 => fn th2 => idom_rule(conji th1 th2)) nths
+ val th2 = Conv.fconv_rule
+ ((arg_conv #> arg_conv)
+ (binop_conv ring_normalize_conv)) th1
+ val conc = th2 |> concl |> Thm.dest_arg
+ val (l,r) = conc |> dest_eq
+ in implies_intr (mk_comb cTrp tm)
+ (equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2))
+ (reflexive l |> mk_object_eq))
+ end
+ else
+ let
+ val (vars,l,cert,noteqth) =(
+ if null nths then
+ let val (vars,pols) = grobify_equations(list_mk_conj(map concl eths))
+ val (l,cert) = grobner_weak vars pols
+ in (vars,l,cert,neq_01)
+ end
+ else
+ let
+ val nth = end_itlist (fn th1 => fn th2 => idom_rule(conji th1 th2)) nths
+ val (vars,pol::pols) =
+ grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths))
+ val (deg,l,cert) = grobner_strong vars pols pol
+ val th1 = Conv.fconv_rule((arg_conv o arg_conv)(binop_conv ring_normalize_conv)) nth
+ val th2 = funpow deg (idom_rule o conji th1) neq_01
+ in (vars,l,cert,th2)
+ end)
+ val _ = writeln ("Translating certificate to HOL inferences")
+ val cert_pos = map (fn (i,p) => (i,filter (fn (c,m) => c >/ rat_0) p)) cert
+ val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
+ (filter (fn (c,m) => c </ rat_0) p))) cert
+ val herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
+ val herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
+ fun thm_fn pols =
+ if null pols then reflexive(mk_const rat_0) else
+ end_itlist mk_add
+ (map (fn (i,p) => Drule.arg_cong_rule (mk_comb ring_mul_tm p) (nth eths i |> mk_meta_eq)) pols)
+ val th1 = thm_fn herts_pos
+ val th2 = thm_fn herts_neg
+ val th3 = conji(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth
+ val th4 = Conv.fconv_rule ((arg_conv o arg_conv o binop_conv) ring_normalize_conv)
+ (neq_rule l th3)
+ val (l,r) = dest_eq(Thm.dest_arg(concl th4))
+ in implies_intr (mk_comb cTrp tm)
+ (equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4))
+ (reflexive l |> mk_object_eq))
+ end
+ end
+
+fun ring tm =
+ let
+ fun mk_forall x p =
+ mk_comb (Drule.cterm_rule (instantiate' [SOME (ctyp_of_term x)] []) @{cpat "All:: (?'a => bool) => _"}) (Thm.cabs x p)
+ val avs = cterm_frees tm
+ val P' = fold mk_forall avs tm
+ val th1 = initial_conv(mk_neg P')
+ val (evs,bod) = strip_exists(concl th1) in
+ if is_forall bod then error "ring: non-universal formula"
+ else
+ let
+ val th1a = weak_dnf_conv bod
+ val boda = concl th1a
+ val th2a = refute_disj refute boda
+ val th2b = [mk_object_eq th1a, (th2a COMP notI) COMP PFalse'] MRS trans
+ val th2 = fold (fn v => fn th => (forall_intr v th) COMP allI) evs (th2b RS PFalse)
+ val th3 = equal_elim
+ (Simplifier.rewrite (HOL_basic_ss addsimps [not_ex RS sym])
+ (th2 |> cprop_of)) th2
+ in specl avs
+ ([[[mk_object_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD)
+ end
+ end
+fun ideal tms tm ord =
+ let
+ val rawvars = fold_rev grobvars (tm::tms) []
+ val vars = sort ord (distinct (fn (x,y) => (term_of x) aconv (term_of y)) rawvars)
+ val pols = map (grobify_term vars) tms
+ val pol = grobify_term vars tm
+ val cert = grobner_ideal vars pols pol
+ in map (fn n => let val p = assocd n cert [] in holify_polynomial vars p end)
+ (0 upto (length pols-1))
+ end
+in (ring,ideal)
+end;
+
+
+fun find_term bounds tm =
+ (case term_of tm of
+ Const ("op =", T) $ _ $ _ =>
+ if domain_type T = HOLogic.boolT then find_args bounds tm
+ else Thm.dest_arg tm
+ | Const ("Not", _) $ _ => find_term bounds (Thm.dest_arg tm)
+ | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const ("op &", _) $ _ $ _ => find_args bounds tm
+ | Const ("op |", _) $ _ $ _ => find_args bounds tm
+ | Const ("op -->", _) $ _ $ _ => find_args bounds tm
+ | _ => raise TERM ("find_term", []))
+and find_args bounds tm =
+ let val (t, u) = Thm.dest_binop tm
+ in (find_term bounds t handle TERM _ => find_term bounds u) end
+and find_body bounds b =
+ let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
+ in find_term (bounds + 1) b' end;
+
+fun ring_conv ctxt form =
+ (case try (find_term 0 (* FIXME !? *)) form of
+ NONE => reflexive form
+ | SOME tm =>
+ (case NormalizerData.match ctxt tm of
+ NONE => reflexive form
+ | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) =>
+ fst (ring_and_ideal_conv theory
+ dest_const (mk_const (Thm.ctyp_of_term tm)) ring_eq_conv
+ (semiring_normalize_wrapper res)) form));
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Groebner_Basis/misc.ML Tue Jun 05 16:26:04 2007 +0200
@@ -0,0 +1,40 @@
+(* Title: HOL/Tools/Groebner_Basis/misc.ML
+ ID: $Id$
+ Author: Amine Chaieb, TU Muenchen
+
+Very basic stuff for cterms.
+*)
+
+structure Misc =
+struct
+
+open Conv;
+
+val is_comb = can Thm.dest_comb;
+val concl = cprop_of #> Thm.dest_arg;
+
+fun is_binop ct ct' = ct aconvc (Thm.dest_fun2 ct')
+ handle CTERM _ => false;
+
+fun dest_binop ct ct' =
+ if is_binop ct ct' then Thm.dest_binop ct'
+ else raise CTERM ("dest_binop: bad binop", [ct,ct'])
+
+(* INFERENCE *)
+fun conji th th' =
+let val p = concl th val q = concl th'
+in implies_elim (implies_elim (instantiate' [] (map SOME [p,q]) conjI) th) th' end;
+fun conjunct1' th = th RS conjunct1;
+fun conjunct2' th = th RS conjunct2;
+fun conj_pair th = (conjunct1' th, conjunct2' th);
+val conjuncts =
+ let fun CJ th acc =
+ ((let val (th1,th2) = conj_pair th
+ in CJ th2 (CJ th1 acc) end)
+ handle THM _ => th::acc)
+ in fn th => rev (CJ th [])
+ end;
+
+fun inst_thm inst = Thm.instantiate ([], inst);
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Tue Jun 05 16:26:04 2007 +0200
@@ -0,0 +1,649 @@
+(* Title: HOL/Tools/Groebner_Basis/normalizer.ML
+ ID: $Id$
+ Author: Amine Chaieb, TU Muenchen
+*)
+
+signature NORMALIZER =
+sig
+ val mk_cnumber : ctyp -> int -> cterm
+ val mk_cnumeral : int -> cterm
+ val semiring_normalize_conv : Proof.context -> Conv.conv
+ val semiring_normalize_tac : Proof.context -> int -> tactic
+ val semiring_normalize_wrapper : NormalizerData.entry -> Conv.conv
+ val semiring_normalizers_conv :
+ cterm list -> cterm list * thm list -> cterm list * thm list ->
+ (cterm -> bool) * Conv.conv * Conv.conv * Conv.conv -> (cterm -> Thm.cterm -> bool) ->
+ {add: Conv.conv, mul: Conv.conv, neg: Conv.conv, main: Conv.conv,
+ pow: Conv.conv, sub: Conv.conv}
+end
+
+structure Normalizer: NORMALIZER =
+struct
+open Misc;
+
+local
+ val pls_const = @{cterm "Numeral.Pls"}
+ and min_const = @{cterm "Numeral.Min"}
+ and bit_const = @{cterm "Numeral.Bit"}
+ and zero = @{cpat "0"}
+ and one = @{cpat "1"}
+ fun mk_cbit 0 = @{cterm "Numeral.bit.B0"}
+ | mk_cbit 1 = @{cterm "Numeral.bit.B1"}
+ | mk_cbit _ = raise CTERM ("mk_cbit", []);
+
+in
+
+fun mk_cnumeral 0 = pls_const
+ | mk_cnumeral ~1 = min_const
+ | mk_cnumeral i =
+ let val (q, r) = IntInf.divMod (i, 2)
+ in Thm.capply (Thm.capply bit_const (mk_cnumeral q)) (mk_cbit (IntInf.toInt r))
+ end;
+
+fun mk_cnumber cT =
+ let
+ val [nb_of, z, on] =
+ map (Drule.cterm_rule (instantiate' [SOME cT] [])) [@{cpat "number_of"}, zero, one]
+ fun h 0 = z
+ | h 1 = on
+ | h x = Thm.capply nb_of (mk_cnumeral x)
+ in h end;
+end;
+
+
+(* Very basic stuff for terms *)
+val dest_numeral = term_of #> HOLogic.dest_number #> snd;
+val is_numeral = can dest_numeral;
+
+val numeral01_conv = Simplifier.rewrite
+ (HOL_basic_ss addsimps [numeral_1_eq_1, numeral_0_eq_0]);
+val zero1_numeral_conv =
+ Simplifier.rewrite (HOL_basic_ss addsimps [numeral_1_eq_1 RS sym, numeral_0_eq_0 RS sym]);
+val zerone_conv = fn cv => zero1_numeral_conv then_conv cv then_conv numeral01_conv;
+val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
+ @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"},
+ @{thm "less_nat_number_of"}];
+val nat_add_conv =
+ zerone_conv
+ (Simplifier.rewrite
+ (HOL_basic_ss
+ addsimps arith_simps @ natarith @ rel_simps
+ @ [if_False, if_True, add_0, add_Suc, add_number_of_left, Suc_eq_add_numeral_1]
+ @ map (fn th => th RS sym) numerals));
+
+val nat_mul_conv = nat_add_conv;
+val zeron_tm = @{cterm "0::nat"};
+val onen_tm = @{cterm "1::nat"};
+val true_tm = @{cterm "True"};
+
+
+(* The main function! *)
+fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules)
+ (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
+let
+
+val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08,
+ pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16,
+ pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24,
+ pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32,
+ pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules;
+
+val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars;
+val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
+val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];
+
+val dest_add = dest_binop add_tm
+val dest_mul = dest_binop mul_tm
+fun dest_pow tm =
+ let val (l,r) = dest_binop pow_tm tm
+ in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm])
+ end;
+val is_add = is_binop add_tm
+val is_mul = is_binop mul_tm
+fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm);
+
+val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
+ (case (r_ops, r_rules) of
+ ([], []) => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)
+ | ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
+ let
+ val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
+ val neg_tm = Thm.dest_fun neg_pat
+ val dest_sub = dest_binop sub_tm
+ val is_sub = is_binop sub_tm
+ in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
+ sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
+ end);
+in fn variable_order =>
+ let
+
+(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible. *)
+(* Also deals with "const * const", but both terms must involve powers of *)
+(* the same variable, or both be constants, or behaviour may be incorrect. *)
+
+ fun powvar_mul_conv tm =
+ let
+ val (l,r) = dest_mul tm
+ in if is_semiring_constant l andalso is_semiring_constant r
+ then semiring_mul_conv tm
+ else
+ ((let
+ val (lx,ln) = dest_pow l
+ in
+ ((let val (rx,rn) = dest_pow r
+ val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
+ val (tm1,tm2) = Thm.dest_comb(concl th1) in
+ transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
+ handle CTERM _ =>
+ (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
+ val (tm1,tm2) = Thm.dest_comb(concl th1) in
+ transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
+ handle CTERM _ =>
+ ((let val (rx,rn) = dest_pow r
+ val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
+ val (tm1,tm2) = Thm.dest_comb(concl th1) in
+ transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
+ handle CTERM _ => inst_thm [(cx,l)] pthm_32
+
+))
+ end;
+
+(* Remove "1 * m" from a monomial, and just leave m. *)
+
+ fun monomial_deone th =
+ (let val (l,r) = dest_mul(concl th) in
+ if l aconvc one_tm
+ then transitive th (inst_thm [(ca,r)] pthm_13) else th end)
+ handle CTERM _ => th;
+
+(* Conversion for "(monomial)^n", where n is a numeral. *)
+
+ val monomial_pow_conv =
+ let
+ fun monomial_pow tm bod ntm =
+ if not(is_comb bod)
+ then reflexive tm
+ else
+ if is_semiring_constant bod
+ then semiring_pow_conv tm
+ else
+ let
+ val (lopr,r) = Thm.dest_comb bod
+ in if not(is_comb lopr)
+ then reflexive tm
+ else
+ let
+ val (opr,l) = Thm.dest_comb lopr
+ in
+ if opr aconvc pow_tm andalso is_numeral r
+ then
+ let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
+ val (l,r) = Thm.dest_comb(concl th1)
+ in transitive th1 (Drule.arg_cong_rule l (nat_mul_conv r))
+ end
+ else
+ if opr aconvc mul_tm
+ then
+ let
+ val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33
+ val (xy,z) = Thm.dest_comb(concl th1)
+ val (x,y) = Thm.dest_comb xy
+ val thl = monomial_pow y l ntm
+ val thr = monomial_pow z r ntm
+ in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
+ end
+ else reflexive tm
+ end
+ end
+ in fn tm =>
+ let
+ val (lopr,r) = Thm.dest_comb tm
+ val (opr,l) = Thm.dest_comb lopr
+ in if not (opr aconvc pow_tm) orelse not(is_numeral r)
+ then raise CTERM ("monomial_pow_conv", [tm])
+ else if r aconvc zeron_tm
+ then inst_thm [(cx,l)] pthm_35
+ else if r aconvc onen_tm
+ then inst_thm [(cx,l)] pthm_36
+ else monomial_deone(monomial_pow tm l r)
+ end
+ end;
+
+(* Multiplication of canonical monomials. *)
+ val monomial_mul_conv =
+ let
+ fun powvar tm =
+ if is_semiring_constant tm then one_tm
+ else
+ ((let val (lopr,r) = Thm.dest_comb tm
+ val (opr,l) = Thm.dest_comb lopr
+ in if opr aconvc pow_tm andalso is_numeral r then l
+ else raise CTERM ("monomial_mul_conv",[tm]) end)
+ handle CTERM _ => tm) (* FIXME !? *)
+ fun vorder x y =
+ if x aconvc y then 0
+ else
+ if x aconvc one_tm then ~1
+ else if y aconvc one_tm then 1
+ else if variable_order x y then ~1 else 1
+ fun monomial_mul tm l r =
+ ((let val (lx,ly) = dest_mul l val vl = powvar lx
+ in
+ ((let
+ val (rx,ry) = dest_mul r
+ val vr = powvar rx
+ val ord = vorder vl vr
+ in
+ if ord = 0
+ then
+ let
+ val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val (tm3,tm4) = Thm.dest_comb tm1
+ val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
+ val th3 = transitive th1 th2
+ val (tm5,tm6) = Thm.dest_comb(concl th3)
+ val (tm7,tm8) = Thm.dest_comb tm6
+ val th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
+ in transitive th3 (Drule.arg_cong_rule tm5 th4)
+ end
+ else
+ let val th0 = if ord < 0 then pthm_16 else pthm_17
+ val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val (tm3,tm4) = Thm.dest_comb tm2
+ in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
+ end
+ end)
+ handle CTERM _ =>
+ (let val vr = powvar r val ord = vorder vl vr
+ in
+ if ord = 0 then
+ let
+ val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val (tm3,tm4) = Thm.dest_comb tm1
+ val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
+ in transitive th1 th2
+ end
+ else
+ if ord < 0 then
+ let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val (tm3,tm4) = Thm.dest_comb tm2
+ in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
+ end
+ else inst_thm [(ca,l),(cb,r)] pthm_09
+ end)) end)
+ handle CTERM _ =>
+ (let val vl = powvar l in
+ ((let
+ val (rx,ry) = dest_mul r
+ val vr = powvar rx
+ val ord = vorder vl vr
+ in if ord = 0 then
+ let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val (tm3,tm4) = Thm.dest_comb tm1
+ in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
+ end
+ else if ord > 0 then
+ let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val (tm3,tm4) = Thm.dest_comb tm2
+ in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
+ end
+ else reflexive tm
+ end)
+ handle CTERM _ =>
+ (let val vr = powvar r
+ val ord = vorder vl vr
+ in if ord = 0 then powvar_mul_conv tm
+ else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
+ else reflexive tm
+ end)) end))
+ in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
+ end
+ end;
+(* Multiplication by monomial of a polynomial. *)
+
+ val polynomial_monomial_mul_conv =
+ let
+ fun pmm_conv tm =
+ let val (l,r) = dest_mul tm
+ in
+ ((let val (y,z) = dest_add r
+ val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val (tm3,tm4) = Thm.dest_comb tm1
+ val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
+ in transitive th1 th2
+ end)
+ handle CTERM _ => monomial_mul_conv tm)
+ end
+ in pmm_conv
+ end;
+
+(* Addition of two monomials identical except for constant multiples. *)
+
+fun monomial_add_conv tm =
+ let val (l,r) = dest_add tm
+ in if is_semiring_constant l andalso is_semiring_constant r
+ then semiring_add_conv tm
+ else
+ let val th1 =
+ if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l)
+ then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then
+ inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02
+ else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03
+ else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r)
+ then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04
+ else inst_thm [(cm,r)] pthm_05
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val (tm3,tm4) = Thm.dest_comb tm1
+ val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
+ val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
+ val tm5 = concl th3
+ in
+ if (Thm.dest_arg1 tm5) aconvc zero_tm
+ then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
+ else monomial_deone th3
+ end
+ end;
+
+(* Ordering on monomials. *)
+
+fun striplist dest =
+ let fun strip x acc =
+ ((let val (l,r) = dest x in
+ strip l (strip r acc) end)
+ handle CTERM _ => x::acc) (* FIXME !? *)
+ in fn x => strip x []
+ end;
+
+
+fun powervars tm =
+ let val ptms = striplist dest_mul tm
+ in if is_semiring_constant (hd ptms) then tl ptms else ptms
+ end;
+val num_0 = 0;
+val num_1 = 1;
+fun dest_varpow tm =
+ ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end)
+ handle CTERM _ =>
+ (tm,(if is_semiring_constant tm then num_0 else num_1)));
+
+val morder =
+ let fun lexorder l1 l2 =
+ case (l1,l2) of
+ ([],[]) => 0
+ | (vps,[]) => ~1
+ | ([],vps) => 1
+ | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
+ if variable_order x1 x2 then 1
+ else if variable_order x2 x1 then ~1
+ else if n1 < n2 then ~1
+ else if n2 < n1 then 1
+ else lexorder vs1 vs2
+ in fn tm1 => fn tm2 =>
+ let val vdegs1 = map dest_varpow (powervars tm1)
+ val vdegs2 = map dest_varpow (powervars tm2)
+ val deg1 = fold_rev ((curry (op +)) o snd) vdegs1 num_0
+ val deg2 = fold_rev ((curry (op +)) o snd) vdegs2 num_0
+ in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
+ else lexorder vdegs1 vdegs2
+ end
+ end;
+
+(* Addition of two polynomials. *)
+
+val polynomial_add_conv =
+ let
+ fun dezero_rule th =
+ let
+ val tm = concl th
+ in
+ if not(is_add tm) then th else
+ let val (lopr,r) = Thm.dest_comb tm
+ val l = Thm.dest_arg lopr
+ in
+ if l aconvc zero_tm
+ then transitive th (inst_thm [(ca,r)] pthm_07) else
+ if r aconvc zero_tm
+ then transitive th (inst_thm [(ca,l)] pthm_08) else th
+ end
+ end
+ fun padd tm =
+ let
+ val (l,r) = dest_add tm
+ in
+ if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07
+ else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08
+ else
+ if is_add l
+ then
+ let val (a,b) = dest_add l
+ in
+ if is_add r then
+ let val (c,d) = dest_add r
+ val ord = morder a c
+ in
+ if ord = 0 then
+ let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val (tm3,tm4) = Thm.dest_comb tm1
+ val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
+ in dezero_rule (transitive th1 (combination th2 (padd tm2)))
+ end
+ else (* ord <> 0*)
+ let val th1 =
+ if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
+ else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
+ end
+ end
+ else (* not (is_add r)*)
+ let val ord = morder a r
+ in
+ if ord = 0 then
+ let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val (tm3,tm4) = Thm.dest_comb tm1
+ val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
+ in dezero_rule (transitive th1 th2)
+ end
+ else (* ord <> 0*)
+ if ord > 0 then
+ let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
+ end
+ else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
+ end
+ end
+ else (* not (is_add l)*)
+ if is_add r then
+ let val (c,d) = dest_add r
+ val ord = morder l c
+ in
+ if ord = 0 then
+ let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val (tm3,tm4) = Thm.dest_comb tm1
+ val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
+ in dezero_rule (transitive th1 th2)
+ end
+ else
+ if ord > 0 then reflexive tm
+ else
+ let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
+ end
+ end
+ else
+ let val ord = morder l r
+ in
+ if ord = 0 then monomial_add_conv tm
+ else if ord > 0 then dezero_rule(reflexive tm)
+ else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
+ end
+ end
+ in padd
+ end;
+
+(* Multiplication of two polynomials. *)
+
+val polynomial_mul_conv =
+ let
+ fun pmul tm =
+ let val (l,r) = dest_mul tm
+ in
+ if not(is_add l) then polynomial_monomial_mul_conv tm
+ else
+ if not(is_add r) then
+ let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
+ in transitive th1 (polynomial_monomial_mul_conv(concl th1))
+ end
+ else
+ let val (a,b) = dest_add l
+ val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val (tm3,tm4) = Thm.dest_comb tm1
+ val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
+ val th3 = transitive th1 (combination th2 (pmul tm2))
+ in transitive th3 (polynomial_add_conv (concl th3))
+ end
+ end
+ in fn tm =>
+ let val (l,r) = dest_mul tm
+ in
+ if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11
+ else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12
+ else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13
+ else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14
+ else pmul tm
+ end
+ end;
+
+(* Power of polynomial (optimized for the monomial and trivial cases). *)
+
+val Succ = @{cterm "Suc"};
+val num_conv = fn n =>
+ nat_add_conv (Thm.capply (Succ) (mk_cnumber @{ctyp "nat"} ((dest_numeral n) - 1)))
+ |> Thm.symmetric;
+
+
+val polynomial_pow_conv =
+ let
+ fun ppow tm =
+ let val (l,n) = dest_pow tm
+ in
+ if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35
+ else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36
+ else
+ let val th1 = num_conv n
+ val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
+ val (tm1,tm2) = Thm.dest_comb(concl th2)
+ val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
+ val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
+ in transitive th4 (polynomial_mul_conv (concl th4))
+ end
+ end
+ in fn tm =>
+ if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm
+ end;
+
+(* Negation. *)
+
+val polynomial_neg_conv =
+ fn tm =>
+ let val (l,r) = Thm.dest_comb tm in
+ if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
+ let val th1 = inst_thm [(cx',r)] neg_mul
+ val th2 = transitive th1 (arg1_conv semiring_mul_conv (concl th1))
+ in transitive th2 (polynomial_monomial_mul_conv (concl th2))
+ end
+ end;
+
+
+(* Subtraction. *)
+val polynomial_sub_conv = fn tm =>
+ let val (l,r) = dest_sub tm
+ val th1 = inst_thm [(cx',l),(cy',r)] sub_add
+ val (tm1,tm2) = Thm.dest_comb(concl th1)
+ val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
+ in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
+ end;
+
+(* Conversion from HOL term. *)
+
+fun polynomial_conv tm =
+ if not(is_comb tm) orelse is_semiring_constant tm
+ then reflexive tm
+ else
+ let val (lopr,r) = Thm.dest_comb tm
+ in if lopr aconvc neg_tm then
+ let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
+ in transitive th1 (polynomial_neg_conv (concl th1))
+ end
+ else
+ if not(is_comb lopr) then reflexive tm
+ else
+ let val (opr,l) = Thm.dest_comb lopr
+ in if opr aconvc pow_tm andalso is_numeral r
+ then
+ let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
+ in transitive th1 (polynomial_pow_conv (concl th1))
+ end
+ else
+ if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
+ then
+ let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
+ val f = if opr aconvc add_tm then polynomial_add_conv
+ else if opr aconvc mul_tm then polynomial_mul_conv
+ else polynomial_sub_conv
+ in transitive th1 (f (concl th1))
+ end
+ else reflexive tm
+ end
+ end;
+ in
+ {main = polynomial_conv,
+ add = polynomial_add_conv,
+ mul = polynomial_mul_conv,
+ pow = polynomial_pow_conv,
+ neg = polynomial_neg_conv,
+ sub = polynomial_sub_conv}
+ end
+end;
+
+val nat_arith = @{thms "nat_arith"};
+val nat_exp_ss = HOL_basic_ss addsimps (nat_number @ nat_arith @ arith_simps @ rel_simps)
+ addsimps [Let_def, if_False, if_True, add_0, add_Suc];
+
+fun semiring_normalize_wrapper ({vars, semiring, ring, idom},
+ {conv, dest_const, mk_const, is_const}) =
+ let
+ fun ord t u = Term.term_ord (term_of t, term_of u) = LESS
+
+ val pow_conv =
+ arg_conv (Simplifier.rewrite nat_exp_ss)
+ then_conv Simplifier.rewrite
+ (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
+ then_conv conv
+ val dat = (is_const, conv, conv, pow_conv)
+ val {main, ...} = semiring_normalizers_conv vars semiring ring dat ord
+ in main end;
+
+fun semiring_normalize_conv ctxt tm =
+ (case NormalizerData.match ctxt tm of
+ NONE => reflexive tm
+ | SOME res => semiring_normalize_wrapper res tm);
+
+
+fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) =>
+ rtac (semiring_normalize_conv ctxt
+ (cterm_of (ProofContext.theory_of ctxt) (fst (Logic.dest_equals goal)))) i);
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Tue Jun 05 16:26:04 2007 +0200
@@ -0,0 +1,200 @@
+(* Title: HOL/Tools/Groebner_Basis/normalizer_data.ML
+ ID: $Id$
+ Author: Amine Chaieb, TU Muenchen
+
+Ring normalization data.
+*)
+
+signature NORMALIZER_DATA =
+sig
+ type entry
+ val get: Proof.context -> (thm * entry) list
+ val match: Proof.context -> cterm -> entry option
+ val del: attribute
+ val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list}
+ -> attribute
+ val funs: thm -> {is_const: morphism -> cterm -> bool,
+ dest_const: morphism -> cterm -> Rat.rat,
+ mk_const: morphism -> ctyp -> Rat.rat -> cterm,
+ conv: morphism -> cterm -> thm} -> morphism -> Context.generic -> Context.generic
+ val setup: theory -> theory
+end;
+
+structure NormalizerData: NORMALIZER_DATA =
+struct
+
+(* data *)
+
+type entry =
+ {vars: cterm list,
+ semiring: cterm list * thm list,
+ ring: cterm list * thm list,
+ idom: thm list} *
+ {is_const: cterm -> bool,
+ dest_const: cterm -> Rat.rat,
+ mk_const: ctyp -> Rat.rat -> cterm,
+ conv: cterm -> thm};
+
+val eq_key = Thm.eq_thm;
+fun eq_data arg = eq_fst eq_key arg;
+
+structure Data = GenericDataFun
+(
+ val name = "HOL/norm";
+ type T = (thm * entry) list;
+ val empty = [];
+ val extend = I;
+ fun merge _ = AList.merge eq_key (K true);
+ fun print _ _ = ();
+);
+
+val get = Data.get o Context.Proof;
+
+
+(* match data *)
+
+fun match ctxt tm =
+ let
+ fun match_inst
+ ({vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom},
+ fns as {is_const, dest_const, mk_const, conv}) pat =
+ let
+ fun h instT =
+ let
+ val substT = Thm.instantiate (instT, []);
+ val substT_cterm = Drule.cterm_rule substT;
+
+ val vars' = map substT_cterm vars;
+ val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
+ val ring' = (map substT_cterm r_ops, map substT r_rules);
+ val idom' = map substT idom;
+
+ val result = ({vars = vars', semiring = semiring', ring = ring', idom = idom'}, fns);
+ in SOME result end
+ in (case try Thm.match (pat, tm) of
+ NONE => NONE
+ | SOME (instT, _) => h instT)
+ end;
+
+ fun match_struct (_,
+ entry as ({semiring = (sr_ops, _), ring = (r_ops, _), ...}, _): entry) =
+ get_first (match_inst entry) (sr_ops @ r_ops);
+ in get_first match_struct (get ctxt) end;
+
+
+(* logical content *)
+
+val semiringN = "semiring";
+val ringN = "ring";
+val idomN = "idom";
+
+fun undefined _ = raise Match;
+
+fun del_data key = remove eq_data (key, []);
+
+val del = Thm.declaration_attribute (Data.map o del_data);
+
+fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom} =
+ Thm.declaration_attribute (fn key => fn context => context |> Data.map
+ let
+ val ctxt = Context.proof_of context;
+
+ fun check kind name xs n =
+ null xs orelse length xs = n orelse
+ error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
+ val check_ops = check "operations";
+ val check_rules = check "rules";
+
+ val _ =
+ check_ops semiringN sr_ops 5 andalso
+ check_rules semiringN sr_rules 37 andalso
+ check_ops ringN r_ops 2 andalso
+ check_rules ringN r_rules 2 andalso
+ check_rules idomN idom 2;
+
+ val mk_meta = LocalDefs.meta_rewrite_rule ctxt;
+ val sr_rules' = map mk_meta sr_rules;
+ val r_rules' = map mk_meta r_rules;
+
+ fun rule i = nth sr_rules' (i - 1);
+
+ val (cx, cy) = Thm.dest_binop (hd sr_ops);
+ val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
+ val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
+ val ((clx, crx), (cly, cry)) =
+ rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
+ val ((ca, cb), (cc, cd)) =
+ rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
+ val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
+ val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
+
+ val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
+ val _ = map print_thm sr_rules';
+ val semiring = (sr_ops, sr_rules');
+ val ring = (r_ops, r_rules');
+ in
+ del_data key #>
+ cons (key, ({vars = vars, semiring = semiring, ring = ring, idom = idom},
+ {is_const = undefined, dest_const = undefined, mk_const = undefined,
+ conv = undefined}))
+ end);
+
+
+(* extra-logical functions *)
+
+fun funs raw_key {is_const, dest_const, mk_const, conv} phi = Data.map (fn data =>
+ let
+ val key = Morphism.thm phi raw_key;
+ val _ = AList.defined eq_key data key orelse
+ raise THM ("No data entry for structure key", 0, [key]);
+ val fns = {is_const = is_const phi, dest_const = dest_const phi,
+ mk_const = mk_const phi, conv = conv phi};
+ in AList.map_entry eq_key key (apsnd (K fns)) data end);
+
+
+(* concrete syntax *)
+
+local
+
+fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
+fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
+fun keyword3 k1 k2 k3 =
+ Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
+
+val opsN = "ops";
+val rulesN = "rules";
+
+val normN = "norm";
+val constN = "const";
+val delN = "del";
+
+val any_keyword =
+ keyword2 semiringN opsN || keyword2 semiringN rulesN ||
+ keyword2 ringN opsN || keyword2 ringN rulesN ||
+ keyword2 idomN rulesN;
+
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val terms = thms >> map Drule.dest_term;
+
+fun optional scan = Scan.optional scan [];
+
+in
+
+fun att_syntax src = src |> Attrib.syntax
+ (Scan.lift (Args.$$$ delN >> K del) ||
+ ((keyword2 semiringN opsN |-- terms) --
+ (keyword2 semiringN rulesN |-- thms)) --
+ (optional (keyword2 ringN opsN |-- terms) --
+ optional (keyword2 ringN rulesN |-- thms)) --
+ optional (keyword2 idomN rulesN |-- thms)
+ >> (fn ((sr, r), id) => add {semiring = sr, ring = r, idom = id}));
+
+end;
+
+
+(* theory setup *)
+
+val setup =
+ Attrib.add_attributes [("normalizer", att_syntax, "semiring normalizer data")];
+
+end;