23252

1 
(* Title: HOL/Tools/Groebner_Basis/normalizer.ML


2 
ID: $Id$


3 
Author: Amine Chaieb, TU Muenchen


4 
*)


5 


6 
signature NORMALIZER =


7 
sig


8 
val mk_cnumber : ctyp > int > cterm


9 
val mk_cnumeral : int > cterm


10 
val semiring_normalize_conv : Proof.context > Conv.conv


11 
val semiring_normalize_tac : Proof.context > int > tactic


12 
val semiring_normalize_wrapper : NormalizerData.entry > Conv.conv


13 
val semiring_normalizers_conv :


14 
cterm list > cterm list * thm list > cterm list * thm list >


15 
(cterm > bool) * Conv.conv * Conv.conv * Conv.conv > (cterm > Thm.cterm > bool) >


16 
{add: Conv.conv, mul: Conv.conv, neg: Conv.conv, main: Conv.conv,


17 
pow: Conv.conv, sub: Conv.conv}


18 
end


19 


20 
structure Normalizer: NORMALIZER =


21 
struct


22 
open Misc;


23 


24 
local


25 
val pls_const = @{cterm "Numeral.Pls"}


26 
and min_const = @{cterm "Numeral.Min"}


27 
and bit_const = @{cterm "Numeral.Bit"}


28 
and zero = @{cpat "0"}


29 
and one = @{cpat "1"}


30 
fun mk_cbit 0 = @{cterm "Numeral.bit.B0"}


31 
 mk_cbit 1 = @{cterm "Numeral.bit.B1"}


32 
 mk_cbit _ = raise CTERM ("mk_cbit", []);


33 


34 
in


35 


36 
fun mk_cnumeral 0 = pls_const


37 
 mk_cnumeral ~1 = min_const


38 
 mk_cnumeral i =


39 
let val (q, r) = IntInf.divMod (i, 2)


40 
in Thm.capply (Thm.capply bit_const (mk_cnumeral q)) (mk_cbit (IntInf.toInt r))


41 
end;


42 


43 
fun mk_cnumber cT =


44 
let


45 
val [nb_of, z, on] =


46 
map (Drule.cterm_rule (instantiate' [SOME cT] [])) [@{cpat "number_of"}, zero, one]


47 
fun h 0 = z


48 
 h 1 = on


49 
 h x = Thm.capply nb_of (mk_cnumeral x)


50 
in h end;


51 
end;


52 


53 


54 
(* Very basic stuff for terms *)


55 
val dest_numeral = term_of #> HOLogic.dest_number #> snd;


56 
val is_numeral = can dest_numeral;


57 


58 
val numeral01_conv = Simplifier.rewrite


59 
(HOL_basic_ss addsimps [numeral_1_eq_1, numeral_0_eq_0]);


60 
val zero1_numeral_conv =


61 
Simplifier.rewrite (HOL_basic_ss addsimps [numeral_1_eq_1 RS sym, numeral_0_eq_0 RS sym]);


62 
val zerone_conv = fn cv => zero1_numeral_conv then_conv cv then_conv numeral01_conv;


63 
val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},


64 
@{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"},


65 
@{thm "less_nat_number_of"}];


66 
val nat_add_conv =


67 
zerone_conv


68 
(Simplifier.rewrite


69 
(HOL_basic_ss


70 
addsimps arith_simps @ natarith @ rel_simps


71 
@ [if_False, if_True, add_0, add_Suc, add_number_of_left, Suc_eq_add_numeral_1]


72 
@ map (fn th => th RS sym) numerals));


73 


74 
val nat_mul_conv = nat_add_conv;


75 
val zeron_tm = @{cterm "0::nat"};


76 
val onen_tm = @{cterm "1::nat"};


77 
val true_tm = @{cterm "True"};


78 


79 


80 
(* The main function! *)


81 
fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules)


82 
(is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =


83 
let


84 


85 
val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08,


86 
pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16,


87 
pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24,


88 
pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32,


89 
pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules;


90 


91 
val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars;


92 
val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;


93 
val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];


94 


95 
val dest_add = dest_binop add_tm


96 
val dest_mul = dest_binop mul_tm


97 
fun dest_pow tm =


98 
let val (l,r) = dest_binop pow_tm tm


99 
in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm])


100 
end;


101 
val is_add = is_binop add_tm


102 
val is_mul = is_binop mul_tm


103 
fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm);


104 


105 
val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =


106 
(case (r_ops, r_rules) of


107 
([], []) => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)


108 
 ([sub_pat, neg_pat], [neg_mul, sub_add]) =>


109 
let


110 
val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)


111 
val neg_tm = Thm.dest_fun neg_pat


112 
val dest_sub = dest_binop sub_tm


113 
val is_sub = is_binop sub_tm


114 
in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul > concl > Thm.dest_arg,


115 
sub_add > concl > Thm.dest_arg > Thm.dest_arg)


116 
end);


117 
in fn variable_order =>


118 
let


119 


120 
(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible. *)


121 
(* Also deals with "const * const", but both terms must involve powers of *)


122 
(* the same variable, or both be constants, or behaviour may be incorrect. *)


123 


124 
fun powvar_mul_conv tm =


125 
let


126 
val (l,r) = dest_mul tm


127 
in if is_semiring_constant l andalso is_semiring_constant r


128 
then semiring_mul_conv tm


129 
else


130 
((let


131 
val (lx,ln) = dest_pow l


132 
in


133 
((let val (rx,rn) = dest_pow r


134 
val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29


135 
val (tm1,tm2) = Thm.dest_comb(concl th1) in


136 
transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)


137 
handle CTERM _ =>


138 
(let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31


139 
val (tm1,tm2) = Thm.dest_comb(concl th1) in


140 
transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)


141 
handle CTERM _ =>


142 
((let val (rx,rn) = dest_pow r


143 
val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30


144 
val (tm1,tm2) = Thm.dest_comb(concl th1) in


145 
transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)


146 
handle CTERM _ => inst_thm [(cx,l)] pthm_32


147 


148 
))


149 
end;


150 


151 
(* Remove "1 * m" from a monomial, and just leave m. *)


152 


153 
fun monomial_deone th =


154 
(let val (l,r) = dest_mul(concl th) in


155 
if l aconvc one_tm


156 
then transitive th (inst_thm [(ca,r)] pthm_13) else th end)


157 
handle CTERM _ => th;


158 


159 
(* Conversion for "(monomial)^n", where n is a numeral. *)


160 


161 
val monomial_pow_conv =


162 
let


163 
fun monomial_pow tm bod ntm =


164 
if not(is_comb bod)


165 
then reflexive tm


166 
else


167 
if is_semiring_constant bod


168 
then semiring_pow_conv tm


169 
else


170 
let


171 
val (lopr,r) = Thm.dest_comb bod


172 
in if not(is_comb lopr)


173 
then reflexive tm


174 
else


175 
let


176 
val (opr,l) = Thm.dest_comb lopr


177 
in


178 
if opr aconvc pow_tm andalso is_numeral r


179 
then


180 
let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34


181 
val (l,r) = Thm.dest_comb(concl th1)


182 
in transitive th1 (Drule.arg_cong_rule l (nat_mul_conv r))


183 
end


184 
else


185 
if opr aconvc mul_tm


186 
then


187 
let


188 
val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33


189 
val (xy,z) = Thm.dest_comb(concl th1)


190 
val (x,y) = Thm.dest_comb xy


191 
val thl = monomial_pow y l ntm


192 
val thr = monomial_pow z r ntm


193 
in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)


194 
end


195 
else reflexive tm


196 
end


197 
end


198 
in fn tm =>


199 
let


200 
val (lopr,r) = Thm.dest_comb tm


201 
val (opr,l) = Thm.dest_comb lopr


202 
in if not (opr aconvc pow_tm) orelse not(is_numeral r)


203 
then raise CTERM ("monomial_pow_conv", [tm])


204 
else if r aconvc zeron_tm


205 
then inst_thm [(cx,l)] pthm_35


206 
else if r aconvc onen_tm


207 
then inst_thm [(cx,l)] pthm_36


208 
else monomial_deone(monomial_pow tm l r)


209 
end


210 
end;


211 


212 
(* Multiplication of canonical monomials. *)


213 
val monomial_mul_conv =


214 
let


215 
fun powvar tm =


216 
if is_semiring_constant tm then one_tm


217 
else


218 
((let val (lopr,r) = Thm.dest_comb tm


219 
val (opr,l) = Thm.dest_comb lopr


220 
in if opr aconvc pow_tm andalso is_numeral r then l


221 
else raise CTERM ("monomial_mul_conv",[tm]) end)


222 
handle CTERM _ => tm) (* FIXME !? *)


223 
fun vorder x y =


224 
if x aconvc y then 0


225 
else


226 
if x aconvc one_tm then ~1


227 
else if y aconvc one_tm then 1


228 
else if variable_order x y then ~1 else 1


229 
fun monomial_mul tm l r =


230 
((let val (lx,ly) = dest_mul l val vl = powvar lx


231 
in


232 
((let


233 
val (rx,ry) = dest_mul r


234 
val vr = powvar rx


235 
val ord = vorder vl vr


236 
in


237 
if ord = 0


238 
then


239 
let


240 
val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15


241 
val (tm1,tm2) = Thm.dest_comb(concl th1)


242 
val (tm3,tm4) = Thm.dest_comb tm1


243 
val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2


244 
val th3 = transitive th1 th2


245 
val (tm5,tm6) = Thm.dest_comb(concl th3)


246 
val (tm7,tm8) = Thm.dest_comb tm6


247 
val th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8


248 
in transitive th3 (Drule.arg_cong_rule tm5 th4)


249 
end


250 
else


251 
let val th0 = if ord < 0 then pthm_16 else pthm_17


252 
val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0


253 
val (tm1,tm2) = Thm.dest_comb(concl th1)


254 
val (tm3,tm4) = Thm.dest_comb tm2


255 
in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))


256 
end


257 
end)


258 
handle CTERM _ =>


259 
(let val vr = powvar r val ord = vorder vl vr


260 
in


261 
if ord = 0 then


262 
let


263 
val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18


264 
val (tm1,tm2) = Thm.dest_comb(concl th1)


265 
val (tm3,tm4) = Thm.dest_comb tm1


266 
val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2


267 
in transitive th1 th2


268 
end


269 
else


270 
if ord < 0 then


271 
let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19


272 
val (tm1,tm2) = Thm.dest_comb(concl th1)


273 
val (tm3,tm4) = Thm.dest_comb tm2


274 
in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))


275 
end


276 
else inst_thm [(ca,l),(cb,r)] pthm_09


277 
end)) end)


278 
handle CTERM _ =>


279 
(let val vl = powvar l in


280 
((let


281 
val (rx,ry) = dest_mul r


282 
val vr = powvar rx


283 
val ord = vorder vl vr


284 
in if ord = 0 then


285 
let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21


286 
val (tm1,tm2) = Thm.dest_comb(concl th1)


287 
val (tm3,tm4) = Thm.dest_comb tm1


288 
in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)


289 
end


290 
else if ord > 0 then


291 
let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22


292 
val (tm1,tm2) = Thm.dest_comb(concl th1)


293 
val (tm3,tm4) = Thm.dest_comb tm2


294 
in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))


295 
end


296 
else reflexive tm


297 
end)


298 
handle CTERM _ =>


299 
(let val vr = powvar r


300 
val ord = vorder vl vr


301 
in if ord = 0 then powvar_mul_conv tm


302 
else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09


303 
else reflexive tm


304 
end)) end))


305 
in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)


306 
end


307 
end;


308 
(* Multiplication by monomial of a polynomial. *)


309 


310 
val polynomial_monomial_mul_conv =


311 
let


312 
fun pmm_conv tm =


313 
let val (l,r) = dest_mul tm


314 
in


315 
((let val (y,z) = dest_add r


316 
val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37


317 
val (tm1,tm2) = Thm.dest_comb(concl th1)


318 
val (tm3,tm4) = Thm.dest_comb tm1


319 
val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)


320 
in transitive th1 th2


321 
end)


322 
handle CTERM _ => monomial_mul_conv tm)


323 
end


324 
in pmm_conv


325 
end;


326 


327 
(* Addition of two monomials identical except for constant multiples. *)


328 


329 
fun monomial_add_conv tm =


330 
let val (l,r) = dest_add tm


331 
in if is_semiring_constant l andalso is_semiring_constant r


332 
then semiring_add_conv tm


333 
else


334 
let val th1 =


335 
if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l)


336 
then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then


337 
inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02


338 
else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03


339 
else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r)


340 
then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04


341 
else inst_thm [(cm,r)] pthm_05


342 
val (tm1,tm2) = Thm.dest_comb(concl th1)


343 
val (tm3,tm4) = Thm.dest_comb tm1


344 
val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)


345 
val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)


346 
val tm5 = concl th3


347 
in


348 
if (Thm.dest_arg1 tm5) aconvc zero_tm


349 
then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)


350 
else monomial_deone th3


351 
end


352 
end;


353 


354 
(* Ordering on monomials. *)


355 


356 
fun striplist dest =


357 
let fun strip x acc =


358 
((let val (l,r) = dest x in


359 
strip l (strip r acc) end)


360 
handle CTERM _ => x::acc) (* FIXME !? *)


361 
in fn x => strip x []


362 
end;


363 


364 


365 
fun powervars tm =


366 
let val ptms = striplist dest_mul tm


367 
in if is_semiring_constant (hd ptms) then tl ptms else ptms


368 
end;


369 
val num_0 = 0;


370 
val num_1 = 1;


371 
fun dest_varpow tm =


372 
((let val (x,n) = dest_pow tm in (x,dest_numeral n) end)


373 
handle CTERM _ =>


374 
(tm,(if is_semiring_constant tm then num_0 else num_1)));


375 


376 
val morder =


377 
let fun lexorder l1 l2 =


378 
case (l1,l2) of


379 
([],[]) => 0


380 
 (vps,[]) => ~1


381 
 ([],vps) => 1


382 
 (((x1,n1)::vs1),((x2,n2)::vs2)) =>


383 
if variable_order x1 x2 then 1


384 
else if variable_order x2 x1 then ~1


385 
else if n1 < n2 then ~1


386 
else if n2 < n1 then 1


387 
else lexorder vs1 vs2


388 
in fn tm1 => fn tm2 =>


389 
let val vdegs1 = map dest_varpow (powervars tm1)


390 
val vdegs2 = map dest_varpow (powervars tm2)


391 
val deg1 = fold_rev ((curry (op +)) o snd) vdegs1 num_0


392 
val deg2 = fold_rev ((curry (op +)) o snd) vdegs2 num_0


393 
in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1


394 
else lexorder vdegs1 vdegs2


395 
end


396 
end;


397 


398 
(* Addition of two polynomials. *)


399 


400 
val polynomial_add_conv =


401 
let


402 
fun dezero_rule th =


403 
let


404 
val tm = concl th


405 
in


406 
if not(is_add tm) then th else


407 
let val (lopr,r) = Thm.dest_comb tm


408 
val l = Thm.dest_arg lopr


409 
in


410 
if l aconvc zero_tm


411 
then transitive th (inst_thm [(ca,r)] pthm_07) else


412 
if r aconvc zero_tm


413 
then transitive th (inst_thm [(ca,l)] pthm_08) else th


414 
end


415 
end


416 
fun padd tm =


417 
let


418 
val (l,r) = dest_add tm


419 
in


420 
if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07


421 
else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08


422 
else


423 
if is_add l


424 
then


425 
let val (a,b) = dest_add l


426 
in


427 
if is_add r then


428 
let val (c,d) = dest_add r


429 
val ord = morder a c


430 
in


431 
if ord = 0 then


432 
let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23


433 
val (tm1,tm2) = Thm.dest_comb(concl th1)


434 
val (tm3,tm4) = Thm.dest_comb tm1


435 
val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)


436 
in dezero_rule (transitive th1 (combination th2 (padd tm2)))


437 
end


438 
else (* ord <> 0*)


439 
let val th1 =


440 
if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24


441 
else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25


442 
val (tm1,tm2) = Thm.dest_comb(concl th1)


443 
in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))


444 
end


445 
end


446 
else (* not (is_add r)*)


447 
let val ord = morder a r


448 
in


449 
if ord = 0 then


450 
let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26


451 
val (tm1,tm2) = Thm.dest_comb(concl th1)


452 
val (tm3,tm4) = Thm.dest_comb tm1


453 
val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2


454 
in dezero_rule (transitive th1 th2)


455 
end


456 
else (* ord <> 0*)


457 
if ord > 0 then


458 
let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24


459 
val (tm1,tm2) = Thm.dest_comb(concl th1)


460 
in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))


461 
end


462 
else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)


463 
end


464 
end


465 
else (* not (is_add l)*)


466 
if is_add r then


467 
let val (c,d) = dest_add r


468 
val ord = morder l c


469 
in


470 
if ord = 0 then


471 
let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28


472 
val (tm1,tm2) = Thm.dest_comb(concl th1)


473 
val (tm3,tm4) = Thm.dest_comb tm1


474 
val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2


475 
in dezero_rule (transitive th1 th2)


476 
end


477 
else


478 
if ord > 0 then reflexive tm


479 
else


480 
let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25


481 
val (tm1,tm2) = Thm.dest_comb(concl th1)


482 
in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))


483 
end


484 
end


485 
else


486 
let val ord = morder l r


487 
in


488 
if ord = 0 then monomial_add_conv tm


489 
else if ord > 0 then dezero_rule(reflexive tm)


490 
else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)


491 
end


492 
end


493 
in padd


494 
end;


495 


496 
(* Multiplication of two polynomials. *)


497 


498 
val polynomial_mul_conv =


499 
let


500 
fun pmul tm =


501 
let val (l,r) = dest_mul tm


502 
in


503 
if not(is_add l) then polynomial_monomial_mul_conv tm


504 
else


505 
if not(is_add r) then


506 
let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09


507 
in transitive th1 (polynomial_monomial_mul_conv(concl th1))


508 
end


509 
else


510 
let val (a,b) = dest_add l


511 
val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10


512 
val (tm1,tm2) = Thm.dest_comb(concl th1)


513 
val (tm3,tm4) = Thm.dest_comb tm1


514 
val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)


515 
val th3 = transitive th1 (combination th2 (pmul tm2))


516 
in transitive th3 (polynomial_add_conv (concl th3))


517 
end


518 
end


519 
in fn tm =>


520 
let val (l,r) = dest_mul tm


521 
in


522 
if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11


523 
else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12


524 
else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13


525 
else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14


526 
else pmul tm


527 
end


528 
end;


529 


530 
(* Power of polynomial (optimized for the monomial and trivial cases). *)


531 


532 
val Succ = @{cterm "Suc"};


533 
val num_conv = fn n =>


534 
nat_add_conv (Thm.capply (Succ) (mk_cnumber @{ctyp "nat"} ((dest_numeral n)  1)))


535 
> Thm.symmetric;


536 


537 


538 
val polynomial_pow_conv =


539 
let


540 
fun ppow tm =


541 
let val (l,n) = dest_pow tm


542 
in


543 
if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35


544 
else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36


545 
else


546 
let val th1 = num_conv n


547 
val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38


548 
val (tm1,tm2) = Thm.dest_comb(concl th2)


549 
val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))


550 
val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3


551 
in transitive th4 (polynomial_mul_conv (concl th4))


552 
end


553 
end


554 
in fn tm =>


555 
if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm


556 
end;


557 


558 
(* Negation. *)


559 


560 
val polynomial_neg_conv =


561 
fn tm =>


562 
let val (l,r) = Thm.dest_comb tm in


563 
if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else


564 
let val th1 = inst_thm [(cx',r)] neg_mul


565 
val th2 = transitive th1 (arg1_conv semiring_mul_conv (concl th1))


566 
in transitive th2 (polynomial_monomial_mul_conv (concl th2))


567 
end


568 
end;


569 


570 


571 
(* Subtraction. *)


572 
val polynomial_sub_conv = fn tm =>


573 
let val (l,r) = dest_sub tm


574 
val th1 = inst_thm [(cx',l),(cy',r)] sub_add


575 
val (tm1,tm2) = Thm.dest_comb(concl th1)


576 
val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)


577 
in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))


578 
end;


579 


580 
(* Conversion from HOL term. *)


581 


582 
fun polynomial_conv tm =


583 
if not(is_comb tm) orelse is_semiring_constant tm


584 
then reflexive tm


585 
else


586 
let val (lopr,r) = Thm.dest_comb tm


587 
in if lopr aconvc neg_tm then


588 
let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)


589 
in transitive th1 (polynomial_neg_conv (concl th1))


590 
end


591 
else


592 
if not(is_comb lopr) then reflexive tm


593 
else


594 
let val (opr,l) = Thm.dest_comb lopr


595 
in if opr aconvc pow_tm andalso is_numeral r


596 
then


597 
let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r


598 
in transitive th1 (polynomial_pow_conv (concl th1))


599 
end


600 
else


601 
if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm


602 
then


603 
let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)


604 
val f = if opr aconvc add_tm then polynomial_add_conv


605 
else if opr aconvc mul_tm then polynomial_mul_conv


606 
else polynomial_sub_conv


607 
in transitive th1 (f (concl th1))


608 
end


609 
else reflexive tm


610 
end


611 
end;


612 
in


613 
{main = polynomial_conv,


614 
add = polynomial_add_conv,


615 
mul = polynomial_mul_conv,


616 
pow = polynomial_pow_conv,


617 
neg = polynomial_neg_conv,


618 
sub = polynomial_sub_conv}


619 
end


620 
end;


621 


622 
val nat_arith = @{thms "nat_arith"};


623 
val nat_exp_ss = HOL_basic_ss addsimps (nat_number @ nat_arith @ arith_simps @ rel_simps)


624 
addsimps [Let_def, if_False, if_True, add_0, add_Suc];


625 


626 
fun semiring_normalize_wrapper ({vars, semiring, ring, idom},


627 
{conv, dest_const, mk_const, is_const}) =


628 
let


629 
fun ord t u = Term.term_ord (term_of t, term_of u) = LESS


630 


631 
val pow_conv =


632 
arg_conv (Simplifier.rewrite nat_exp_ss)


633 
then_conv Simplifier.rewrite


634 
(HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])


635 
then_conv conv


636 
val dat = (is_const, conv, conv, pow_conv)


637 
val {main, ...} = semiring_normalizers_conv vars semiring ring dat ord


638 
in main end;


639 


640 
fun semiring_normalize_conv ctxt tm =


641 
(case NormalizerData.match ctxt tm of


642 
NONE => reflexive tm


643 
 SOME res => semiring_normalize_wrapper res tm);


644 


645 


646 
fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) =>


647 
rtac (semiring_normalize_conv ctxt


648 
(cterm_of (ProofContext.theory_of ctxt) (fst (Logic.dest_equals goal)))) i);


649 
end;
