23252

1 
(* Title: HOL/Groebner_Basis.thy


2 
ID: $Id$


3 
Author: Amine Chaieb, TU Muenchen


4 
*)


5 


6 
header {* Semiring normalization and Groebner Bases *}


7 


8 
theory Groebner_Basis


9 
imports NatBin


10 
uses


11 
"Tools/Groebner_Basis/misc.ML"


12 
"Tools/Groebner_Basis/normalizer_data.ML"


13 
("Tools/Groebner_Basis/normalizer.ML")


14 
begin


15 


16 
subsection {* Semiring normalization *}


17 


18 
setup NormalizerData.setup


19 


20 


21 
locale semiring =


22 
fixes add mul pwr r0 r1


23 
assumes add_a:"(add x (add y z) = add (add x y) z)"


24 
and add_c: "add x y = add y x" and add_0:"add r0 x = x"


25 
and mul_a:"mul x (mul y z) = mul (mul x y) z" and mul_c:"mul x y = mul y x"


26 
and mul_1:"mul r1 x = x" and mul_0:"mul r0 x = r0"


27 
and mul_d:"mul x (add y z) = add (mul x y) (mul x z)"


28 
and pwr_0:"pwr x 0 = r1" and pwr_Suc:"pwr x (Suc n) = mul x (pwr x n)"


29 
begin


30 


31 
lemma mul_pwr:"mul (pwr x p) (pwr x q) = pwr x (p + q)"


32 
proof (induct p)


33 
case 0


34 
then show ?case by (auto simp add: pwr_0 mul_1)


35 
next


36 
case Suc


37 
from this [symmetric] show ?case


38 
by (auto simp add: pwr_Suc mul_1 mul_a)


39 
qed


40 


41 
lemma pwr_mul: "pwr (mul x y) q = mul (pwr x q) (pwr y q)"


42 
proof (induct q arbitrary: x y, auto simp add:pwr_0 pwr_Suc mul_1)


43 
fix q x y


44 
assume "\<And>x y. pwr (mul x y) q = mul (pwr x q) (pwr y q)"


45 
have "mul (mul x y) (mul (pwr x q) (pwr y q)) = mul x (mul y (mul (pwr x q) (pwr y q)))"


46 
by (simp add: mul_a)


47 
also have "\<dots> = (mul (mul y (mul (pwr y q) (pwr x q))) x)" by (simp add: mul_c)


48 
also have "\<dots> = (mul (mul y (pwr y q)) (mul (pwr x q) x))" by (simp add: mul_a)


49 
finally show "mul (mul x y) (mul (pwr x q) (pwr y q)) =


50 
mul (mul x (pwr x q)) (mul y (pwr y q))" by (simp add: mul_c)


51 
qed


52 


53 
lemma pwr_pwr: "pwr (pwr x p) q = pwr x (p * q)"


54 
proof (induct p arbitrary: q)


55 
case 0


56 
show ?case using pwr_Suc mul_1 pwr_0 by (induct q) auto


57 
next


58 
case Suc


59 
thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc)


60 
qed


61 


62 


63 
subsubsection {* Declaring the abstract theory *}


64 


65 
lemma semiring_ops:


66 
includes meta_term_syntax


67 
shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"


68 
and "TERM r0" and "TERM r1"


69 
by rule+


70 


71 
lemma semiring_rules:


72 
"add (mul a m) (mul b m) = mul (add a b) m"


73 
"add (mul a m) m = mul (add a r1) m"


74 
"add m (mul a m) = mul (add a r1) m"


75 
"add m m = mul (add r1 r1) m"


76 
"add r0 a = a"


77 
"add a r0 = a"


78 
"mul a b = mul b a"


79 
"mul (add a b) c = add (mul a c) (mul b c)"


80 
"mul r0 a = r0"


81 
"mul a r0 = r0"


82 
"mul r1 a = a"


83 
"mul a r1 = a"


84 
"mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)"


85 
"mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))"


86 
"mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)"


87 
"mul (mul lx ly) rx = mul (mul lx rx) ly"


88 
"mul (mul lx ly) rx = mul lx (mul ly rx)"


89 
"mul lx (mul rx ry) = mul (mul lx rx) ry"


90 
"mul lx (mul rx ry) = mul rx (mul lx ry)"


91 
"add (add a b) (add c d) = add (add a c) (add b d)"


92 
"add (add a b) c = add a (add b c)"


93 
"add a (add c d) = add c (add a d)"


94 
"add (add a b) c = add (add a c) b"


95 
"add a c = add c a"


96 
"add a (add c d) = add (add a c) d"


97 
"mul (pwr x p) (pwr x q) = pwr x (p + q)"


98 
"mul x (pwr x q) = pwr x (Suc q)"


99 
"mul (pwr x q) x = pwr x (Suc q)"


100 
"mul x x = pwr x 2"


101 
"pwr (mul x y) q = mul (pwr x q) (pwr y q)"


102 
"pwr (pwr x p) q = pwr x (p * q)"


103 
"pwr x 0 = r1"


104 
"pwr x 1 = x"


105 
"mul x (add y z) = add (mul x y) (mul x z)"


106 
"pwr x (Suc q) = mul x (pwr x q)"


107 
"pwr x (2*n) = mul (pwr x n) (pwr x n)"


108 
"pwr x (Suc (2*n)) = mul x (mul (pwr x n) (pwr x n))"


109 
proof 


110 
show "add (mul a m) (mul b m) = mul (add a b) m" using mul_d mul_c by simp


111 
next show"add (mul a m) m = mul (add a r1) m" using mul_d mul_c mul_1 by simp


112 
next show "add m (mul a m) = mul (add a r1) m" using mul_c mul_d mul_1 add_c by simp


113 
next show "add m m = mul (add r1 r1) m" using mul_c mul_d mul_1 by simp


114 
next show "add r0 a = a" using add_0 by simp


115 
next show "add a r0 = a" using add_0 add_c by simp


116 
next show "mul a b = mul b a" using mul_c by simp


117 
next show "mul (add a b) c = add (mul a c) (mul b c)" using mul_c mul_d by simp


118 
next show "mul r0 a = r0" using mul_0 by simp


119 
next show "mul a r0 = r0" using mul_0 mul_c by simp


120 
next show "mul r1 a = a" using mul_1 by simp


121 
next show "mul a r1 = a" using mul_1 mul_c by simp


122 
next show "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)"


123 
using mul_c mul_a by simp


124 
next show "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))"


125 
using mul_a by simp


126 
next


127 
have "mul (mul lx ly) (mul rx ry) = mul (mul rx ry) (mul lx ly)" by (rule mul_c)


128 
also have "\<dots> = mul rx (mul ry (mul lx ly))" using mul_a by simp


129 
finally


130 
show "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)"


131 
using mul_c by simp


132 
next show "mul (mul lx ly) rx = mul (mul lx rx) ly" using mul_c mul_a by simp


133 
next


134 
show "mul (mul lx ly) rx = mul lx (mul ly rx)" by (simp add: mul_a)


135 
next show "mul lx (mul rx ry) = mul (mul lx rx) ry" by (simp add: mul_a )


136 
next show "mul lx (mul rx ry) = mul rx (mul lx ry)" by (simp add: mul_a,simp add: mul_c)


137 
next show "add (add a b) (add c d) = add (add a c) (add b d)"


138 
using add_c add_a by simp


139 
next show "add (add a b) c = add a (add b c)" using add_a by simp


140 
next show "add a (add c d) = add c (add a d)"


141 
apply (simp add: add_a) by (simp only: add_c)


142 
next show "add (add a b) c = add (add a c) b" using add_a add_c by simp


143 
next show "add a c = add c a" by (rule add_c)


144 
next show "add a (add c d) = add (add a c) d" using add_a by simp


145 
next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr)


146 
next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp


147 
next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp


148 
next show "mul x x = pwr x 2" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)


149 
next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)


150 
next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)


151 
next show "pwr x 0 = r1" using pwr_0 .


152 
next show "pwr x 1 = x" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)


153 
next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp


154 
next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp


155 
next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number mul_pwr)


156 
next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))"


157 
by (simp add: nat_number pwr_Suc mul_pwr)


158 
qed


159 


160 


161 
lemma "axioms" [normalizer


162 
semiring ops: semiring_ops


163 
semiring rules: semiring_rules]:


164 
"semiring add mul pwr r0 r1" .


165 


166 
end


167 


168 
interpretation class_semiring: semiring


169 
["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]


170 
by unfold_locales (auto simp add: ring_eq_simps power_Suc)


171 


172 
lemmas nat_arith =


173 
add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of


174 


175 
lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"


176 
by (simp add: numeral_1_eq_1)


177 
lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False


178 
if_True add_0 add_Suc add_number_of_left mult_number_of_left


179 
numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1


180 
numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1


181 
iszero_number_of_1 iszero_number_of_0 nonzero_number_of_Min


182 
iszero_number_of_Pls iszero_0 not_iszero_Numeral1


183 


184 
lemmas semiring_norm = comp_arith


185 


186 
ML {*


187 
fun numeral_is_const ct =


188 
can HOLogic.dest_number (Thm.term_of ct);


189 


190 
val numeral_conv =


191 
Conv.then_conv (Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}),


192 
Simplifier.rewrite (HOL_basic_ss addsimps


193 
[@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(12)}));


194 
*}


195 


196 
ML {*


197 
fun int_of_rat x =


198 
(case Rat.quotient_of_rat x of (i, 1) => i


199 
 _ => error "int_of_rat: bad int")


200 
*}


201 


202 
declaration {*


203 
NormalizerData.funs @{thm class_semiring.axioms}


204 
{is_const = fn phi => numeral_is_const,


205 
dest_const = fn phi => fn ct =>


206 
Rat.rat_of_int (snd


207 
(HOLogic.dest_number (Thm.term_of ct)


208 
handle TERM _ => error "ring_dest_const")),


209 
mk_const = fn phi => fn cT => fn x =>


210 
Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),


211 
conv = fn phi => numeral_conv}


212 
*}


213 


214 


215 
locale ring = semiring +


216 
fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"


217 
and neg :: "'a \<Rightarrow> 'a"


218 
assumes neg_mul: "neg x = mul (neg r1) x"


219 
and sub_add: "sub x y = add x (neg y)"


220 
begin


221 


222 
lemma ring_ops:


223 
includes meta_term_syntax


224 
shows "TERM (sub x y)" and "TERM (neg x)" .


225 


226 
lemmas ring_rules = neg_mul sub_add


227 


228 
lemma "axioms" [normalizer


229 
semiring ops: semiring_ops


230 
semiring rules: semiring_rules


231 
ring ops: ring_ops


232 
ring rules: ring_rules]:


233 
"ring add mul pwr r0 r1 sub neg" .


234 


235 
end


236 


237 


238 
interpretation class_ring: ring ["op +" "op *" "op ^"


239 
"0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op " "uminus"]


240 
by unfold_locales simp_all


241 


242 


243 
declaration {*


244 
NormalizerData.funs @{thm class_ring.axioms}


245 
{is_const = fn phi => numeral_is_const,


246 
dest_const = fn phi => fn ct =>


247 
Rat.rat_of_int (snd


248 
(HOLogic.dest_number (Thm.term_of ct)


249 
handle TERM _ => error "ring_dest_const")),


250 
mk_const = fn phi => fn cT => fn x =>


251 
Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),


252 
conv = fn phi => numeral_conv}


253 
*}


254 


255 
use "Tools/Groebner_Basis/normalizer.ML"


256 


257 
method_setup sring_norm = {*


258 
Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt))


259 
*} "Semiring_normalizer"


260 


261 


262 
subsection {* Gröbner Bases *}


263 


264 
locale semiringb = semiring +


265 
assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z"


266 
and add_mul_solve: "add (mul w y) (mul x z) =


267 
add (mul w z) (mul x y) \<longleftrightarrow> w = x \<or> y = z"


268 
begin


269 


270 
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)"


271 
proof


272 
have "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> \<not> (a = b \<or> c = d)" by simp


273 
also have "\<dots> \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"


274 
using add_mul_solve by blast


275 
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)"


276 
by simp


277 
qed


278 


279 
lemma add_scale_eq_noteq: "\<lbrakk>r \<noteq> r0 ; (a = b) \<and> ~(c = d)\<rbrakk>


280 
\<Longrightarrow> add a (mul r c) \<noteq> add b (mul r d)"


281 
proof(clarify)


282 
assume nz: "r\<noteq> r0" and cnd: "c\<noteq>d"


283 
and eq: "add b (mul r c) = add b (mul r d)"


284 
hence "mul r c = mul r d" using cnd add_cancel by simp


285 
hence "add (mul r0 d) (mul r c) = add (mul r0 c) (mul r d)"


286 
using mul_0 add_cancel by simp


287 
thus "False" using add_mul_solve nz cnd by simp


288 
qed


289 


290 
declare "axioms" [normalizer del]


291 


292 
lemma "axioms" [normalizer


293 
semiring ops: semiring_ops


294 
semiring rules: semiring_rules


295 
idom rules: noteq_reduce add_scale_eq_noteq]:


296 
"semiringb add mul pwr r0 r1" .


297 


298 
end


299 


300 
locale ringb = semiringb + ring


301 
begin


302 


303 
declare "axioms" [normalizer del]


304 


305 
lemma "axioms" [normalizer


306 
semiring ops: semiring_ops


307 
semiring rules: semiring_rules


308 
ring ops: ring_ops


309 
ring rules: ring_rules


310 
idom rules: noteq_reduce add_scale_eq_noteq]:


311 
"ringb add mul pwr r0 r1 sub neg" .


312 


313 
end


314 


315 
lemma no_zero_divirors_neq0:


316 
assumes az: "(a::'a::no_zero_divisors) \<noteq> 0"


317 
and ab: "a*b = 0" shows "b = 0"


318 
proof 


319 
{ assume bz: "b \<noteq> 0"


320 
from no_zero_divisors [OF az bz] ab have False by blast }


321 
thus "b = 0" by blast


322 
qed


323 


324 
interpretation class_ringb: ringb


325 
["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op " "uminus"]


326 
proof(unfold_locales, simp add: ring_eq_simps power_Suc, auto)


327 
fix w x y z ::"'a::{idom,recpower,number_ring}"


328 
assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"


329 
hence ynz': "y  z \<noteq> 0" by simp


330 
from p have "w * y + x* z  w*z  x*y = 0" by simp


331 
hence "w* (y  z)  x * (y  z) = 0" by (simp add: ring_eq_simps)


332 
hence "(y  z) * (w  x) = 0" by (simp add: ring_eq_simps)


333 
with no_zero_divirors_neq0 [OF ynz']


334 
have "w  x = 0" by blast


335 
thus "w = x" by simp


336 
qed


337 


338 


339 
declaration {*


340 
NormalizerData.funs @{thm class_ringb.axioms}


341 
{is_const = fn phi => numeral_is_const,


342 
dest_const = fn phi => fn ct =>


343 
Rat.rat_of_int (snd


344 
(HOLogic.dest_number (Thm.term_of ct)


345 
handle TERM _ => error "ring_dest_const")),


346 
mk_const = fn phi => fn cT => fn x =>


347 
Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),


348 
conv = fn phi => numeral_conv}


349 
*}


350 


351 


352 
interpretation natgb: semiringb


353 
["op +" "op *" "op ^" "0::nat" "1"]


354 
proof (unfold_locales, simp add: ring_eq_simps power_Suc)


355 
fix w x y z ::"nat"


356 
{ assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"


357 
hence "y < z \<or> y > z" by arith


358 
moreover {


359 
assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z  y" in exI, auto)


360 
then obtain k where kp: "k>0" and yz:"z = y + k" by blast


361 
from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz ring_eq_simps)


362 
hence "x*k = w*k" by simp


363 
hence "w = x" using kp by (simp add: mult_cancel2) }


364 
moreover {


365 
assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y  z" in exI, auto)


366 
then obtain k where kp: "k>0" and yz:"y = z + k" by blast


367 
from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz ring_eq_simps)


368 
hence "w*k = x*k" by simp


369 
hence "w = x" using kp by (simp add: mult_cancel2)}


370 
ultimately have "w=x" by blast }


371 
thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto


372 
qed


373 


374 
declaration {*


375 
NormalizerData.funs @{thm natgb.axioms}


376 
{is_const = fn phi => numeral_is_const,


377 
dest_const = fn phi => fn ct =>


378 
Rat.rat_of_int (snd


379 
(HOLogic.dest_number (Thm.term_of ct)


380 
handle TERM _ => error "ring_dest_const")),


381 
mk_const = fn phi => fn cT => fn x =>


382 
Thm.cterm_of (Thm.theory_of_ctyp cT) (HOLogic.mk_number (typ_of cT) (int_of_rat x)),


383 
conv = fn phi => numeral_conv}


384 
*}


385 


386 


387 
lemmas bool_simps = simp_thms(134)


388 
lemma dnf:


389 
"(P & (Q  R)) = ((P&Q)  (P&R))" "((Q  R) & P) = ((Q&P)  (R&P))"


390 
"(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"


391 
by blast+


392 


393 
lemmas weak_dnf_simps = dnf bool_simps


394 


395 
lemma nnf_simps:


396 
"(\<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)"


397 
"(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"


398 
by blast+


399 


400 
lemma PFalse:


401 
"P \<equiv> False \<Longrightarrow> \<not> P"


402 
"\<not> P \<Longrightarrow> (P \<equiv> False)"


403 
by auto


404 


405 
use "Tools/Groebner_Basis/groebner.ML"


406 


407 
ML {*


408 
fun algebra_tac ctxt i = ObjectLogic.full_atomize_tac i THEN (fn st =>


409 
rtac (Groebner.ring_conv ctxt (Thm.dest_arg (nth (cprems_of st) (i  1)))) i st);


410 
*}


411 


412 
method_setup algebra = {*


413 
Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac)


414 
*} ""


415 


416 
end
