# HG changeset patch # User wenzelm # Date 1181053564 -7200 # Node ID 67268bb40b219debaba96d63156df4a16f760718 # Parent 471b576aad25ae019e296a8baee482f741f7205e Semiring normalization and Groebner Bases. diff -r 471b576aad25 -r 67268bb40b21 CONTRIBUTORS --- 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. diff -r 471b576aad25 -r 67268bb40b21 src/HOL/Groebner_Basis.thy --- /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 "\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 "\ = (mul (mul y (mul (pwr y q) (pwr x q))) x)" by (simp add: mul_c) + also have "\ = (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 "\ = 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: "\ 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 \ 'a \ 'a" + and neg :: "'a \ '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 \ y = z" + and add_mul_solve: "add (mul w y) (mul x z) = + add (mul w z) (mul x y) \ w = x \ y = z" +begin + +lemma noteq_reduce: "a \ b \ c \ d \ add (mul a c) (mul b d) \ add (mul a d) (mul b c)" +proof- + have "a \ b \ c \ d \ \ (a = b \ c = d)" by simp + also have "\ \ add (mul a c) (mul b d) \ add (mul a d) (mul b c)" + using add_mul_solve by blast + finally show "a \ b \ c \ d \ add (mul a c) (mul b d) \ add (mul a d) (mul b c)" + by simp +qed + +lemma add_scale_eq_noteq: "\r \ r0 ; (a = b) \ ~(c = d)\ + \ add a (mul r c) \ add b (mul r d)" +proof(clarify) + assume nz: "r\ r0" and cnd: "c\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) \ 0" + and ab: "a*b = 0" shows "b = 0" +proof - + { assume bz: "b \ 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 \ z" + hence ynz': "y - z \ 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 \ z" + hence "y < z \ y > z" by arith + moreover { + assume lt:"y k. z = y + k \ 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 "\k. y = z + k \ 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 \ 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 \ Q) = (Q \ P)" "(P \ Q) = (Q \ P)" + by blast+ + +lemmas weak_dnf_simps = dnf bool_simps + +lemma nnf_simps: + "(\(P \ Q)) = (\P \ \Q)" "(\(P \ Q)) = (\P \ \Q)" "(P \ Q) = (\P \ Q)" + "(P = Q) = ((P \ Q) \ (\P \ \ Q))" "(\ \(P)) = P" + by blast+ + +lemma PFalse: + "P \ False \ \ P" + "\ P \ (P \ 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 diff -r 471b576aad25 -r 67268bb40b21 src/HOL/IsaMakefile --- 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 \ diff -r 471b576aad25 -r 67268bb40b21 src/HOL/NatSimprocs.thy --- 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 diff -r 471b576aad25 -r 67268bb40b21 src/HOL/Tools/Groebner_Basis/groebner.ML --- /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 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 (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; diff -r 471b576aad25 -r 67268bb40b21 src/HOL/Tools/Groebner_Basis/misc.ML --- /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; diff -r 471b576aad25 -r 67268bb40b21 src/HOL/Tools/Groebner_Basis/normalizer.ML --- /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; diff -r 471b576aad25 -r 67268bb40b21 src/HOL/Tools/Groebner_Basis/normalizer_data.ML --- /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;