author  wenzelm 
Tue, 03 Jul 2007 22:27:25 +0200  
changeset 23559  0de527730294 
parent 23485  881b04972953 
child 23580  998a6fda9bb6 
permissions  rwrr 
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 

23259  8 
val mk_cnumber : ctyp > integer > cterm 
9 
val mk_cnumeral : integer > cterm 

23485  10 
val semiring_normalize_conv : Proof.context > conv 
11 
val semiring_normalize_ord_conv : Proof.context > (cterm > cterm > bool) > conv 

23252  12 
val semiring_normalize_tac : Proof.context > int > tactic 
23485  13 
val semiring_normalize_wrapper : Proof.context > NormalizerData.entry > conv 
14 
val semiring_normalize_ord_wrapper : Proof.context > NormalizerData.entry > 

15 
(cterm > cterm > bool) > conv 

23252  16 
val semiring_normalizers_conv : 
17 
cterm list > cterm list * thm list > cterm list * thm list > 

23485  18 
(cterm > bool) * conv * conv * conv > (cterm > cterm > bool) > 
19 
{add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} 

23252  20 
end 
21 

22 
structure Normalizer: NORMALIZER = 

23 
struct 

23559  24 

25 
open Conv Misc; 

23252  26 

27 
local 

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

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

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

31 
and zero = @{cpat "0"} 

32 
and one = @{cpat "1"} 

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

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

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

36 

37 
in 

38 

39 
fun mk_cnumeral 0 = pls_const 

40 
 mk_cnumeral ~1 = min_const 

41 
 mk_cnumeral i = 

23259  42 
let val (q, r) = Integer.divmod i 2 
43 
in Thm.capply (Thm.capply bit_const (mk_cnumeral q)) (mk_cbit (Integer.machine_int r)) end; 

23252  44 

45 
fun mk_cnumber cT = 

46 
let 

47 
val [nb_of, z, on] = 

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

49 
fun h 0 = z 

50 
 h 1 = on 

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

52 
in h end; 

53 
end; 

54 

55 

56 
(* Very basic stuff for terms *) 

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

58 
val is_numeral = can dest_numeral; 

59 

60 
val numeral01_conv = Simplifier.rewrite 

61 
(HOL_basic_ss addsimps [numeral_1_eq_1, numeral_0_eq_0]); 

62 
val zero1_numeral_conv = 

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

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

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

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

67 
@{thm "less_nat_number_of"}]; 

68 
val nat_add_conv = 

69 
zerone_conv 

70 
(Simplifier.rewrite 

71 
(HOL_basic_ss 

72 
addsimps arith_simps @ natarith @ rel_simps 

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

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

75 

76 
val nat_mul_conv = nat_add_conv; 

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

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

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

80 

81 

82 
(* The main function! *) 

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

84 
(is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) = 

85 
let 

86 

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

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

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

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

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

92 

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

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

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

96 

97 
val dest_add = dest_binop add_tm 

98 
val dest_mul = dest_binop mul_tm 

99 
fun dest_pow tm = 

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

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

102 
end; 

103 
val is_add = is_binop add_tm 

104 
val is_mul = is_binop mul_tm 

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

106 

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

108 
(case (r_ops, r_rules) of 

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

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

111 
let 

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

113 
val neg_tm = Thm.dest_fun neg_pat 

114 
val dest_sub = dest_binop sub_tm 

115 
val is_sub = is_binop sub_tm 

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

117 
sub_add > concl > Thm.dest_arg > Thm.dest_arg) 

118 
end); 

119 
in fn variable_order => 

120 
let 

121 

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

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

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

125 

126 
fun powvar_mul_conv tm = 

127 
let 

128 
val (l,r) = dest_mul tm 

129 
in if is_semiring_constant l andalso is_semiring_constant r 

130 
then semiring_mul_conv tm 

131 
else 

132 
((let 

133 
val (lx,ln) = dest_pow l 

134 
in 

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

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

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

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

139 
handle CTERM _ => 

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

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

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

143 
handle CTERM _ => 

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

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

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

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

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

149 

150 
)) 

151 
end; 

152 

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

154 

155 
fun monomial_deone th = 

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

157 
if l aconvc one_tm 

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

159 
handle CTERM _ => th; 

160 

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

162 

163 
val monomial_pow_conv = 

164 
let 

165 
fun monomial_pow tm bod ntm = 

166 
if not(is_comb bod) 

167 
then reflexive tm 

168 
else 

169 
if is_semiring_constant bod 

170 
then semiring_pow_conv tm 

171 
else 

172 
let 

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

174 
in if not(is_comb lopr) 

175 
then reflexive tm 

176 
else 

177 
let 

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

179 
in 

180 
if opr aconvc pow_tm andalso is_numeral r 

181 
then 

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

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

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

185 
end 

186 
else 

187 
if opr aconvc mul_tm 

188 
then 

189 
let 

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

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

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

193 
val thl = monomial_pow y l ntm 

194 
val thr = monomial_pow z r ntm 

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

196 
end 

197 
else reflexive tm 

198 
end 

199 
end 

200 
in fn tm => 

201 
let 

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

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

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

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

206 
else if r aconvc zeron_tm 

207 
then inst_thm [(cx,l)] pthm_35 

208 
else if r aconvc onen_tm 

209 
then inst_thm [(cx,l)] pthm_36 

210 
else monomial_deone(monomial_pow tm l r) 

211 
end 

212 
end; 

213 

214 
(* Multiplication of canonical monomials. *) 

215 
val monomial_mul_conv = 

216 
let 

217 
fun powvar tm = 

218 
if is_semiring_constant tm then one_tm 

219 
else 

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

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

222 
in if opr aconvc pow_tm andalso is_numeral r then l 

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

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

225 
fun vorder x y = 

226 
if x aconvc y then 0 

227 
else 

228 
if x aconvc one_tm then ~1 

229 
else if y aconvc one_tm then 1 

230 
else if variable_order x y then ~1 else 1 

231 
fun monomial_mul tm l r = 

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

233 
in 

234 
((let 

235 
val (rx,ry) = dest_mul r 

236 
val vr = powvar rx 

237 
val ord = vorder vl vr 

238 
in 

239 
if ord = 0 

240 
then 

241 
let 

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

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

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

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

246 
val th3 = transitive th1 th2 

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

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

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

250 
in transitive th3 (Drule.arg_cong_rule tm5 th4) 

251 
end 

252 
else 

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

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

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

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

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

258 
end 

259 
end) 

260 
handle CTERM _ => 

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

262 
in 

263 
if ord = 0 then 

264 
let 

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

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

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

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

269 
in transitive th1 th2 

270 
end 

271 
else 

272 
if ord < 0 then 

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

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

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

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

277 
end 

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

279 
end)) end) 

280 
handle CTERM _ => 

281 
(let val vl = powvar l in 

282 
((let 

283 
val (rx,ry) = dest_mul r 

284 
val vr = powvar rx 

285 
val ord = vorder vl vr 

286 
in if ord = 0 then 

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

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

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

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

291 
end 

292 
else if ord > 0 then 

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

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

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

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

297 
end 

298 
else reflexive tm 

299 
end) 

300 
handle CTERM _ => 

301 
(let val vr = powvar r 

302 
val ord = vorder vl vr 

303 
in if ord = 0 then powvar_mul_conv tm 

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

305 
else reflexive tm 

306 
end)) end)) 

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

308 
end 

309 
end; 

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

311 

312 
val polynomial_monomial_mul_conv = 

313 
let 

314 
fun pmm_conv tm = 

315 
let val (l,r) = dest_mul tm 

316 
in 

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

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

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

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

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

322 
in transitive th1 th2 

323 
end) 

324 
handle CTERM _ => monomial_mul_conv tm) 

325 
end 

326 
in pmm_conv 

327 
end; 

328 

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

330 

331 
fun monomial_add_conv tm = 

332 
let val (l,r) = dest_add tm 

333 
in if is_semiring_constant l andalso is_semiring_constant r 

334 
then semiring_add_conv tm 

335 
else 

336 
let val th1 = 

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

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

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

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

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

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

343 
else inst_thm [(cm,r)] pthm_05 

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

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

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

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

348 
val tm5 = concl th3 

349 
in 

350 
if (Thm.dest_arg1 tm5) aconvc zero_tm 

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

352 
else monomial_deone th3 

353 
end 

354 
end; 

355 

356 
(* Ordering on monomials. *) 

357 

358 
fun striplist dest = 

359 
let fun strip x acc = 

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

361 
strip l (strip r acc) end) 

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

363 
in fn x => strip x [] 

364 
end; 

365 

366 

367 
fun powervars tm = 

368 
let val ptms = striplist dest_mul tm 

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

370 
end; 

371 
val num_0 = 0; 

372 
val num_1 = 1; 

373 
fun dest_varpow tm = 

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

375 
handle CTERM _ => 

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

377 

378 
val morder = 

379 
let fun lexorder l1 l2 = 

380 
case (l1,l2) of 

381 
([],[]) => 0 

382 
 (vps,[]) => ~1 

383 
 ([],vps) => 1 

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

385 
if variable_order x1 x2 then 1 

386 
else if variable_order x2 x1 then ~1 

387 
else if n1 < n2 then ~1 

388 
else if n2 < n1 then 1 

389 
else lexorder vs1 vs2 

390 
in fn tm1 => fn tm2 => 

391 
let val vdegs1 = map dest_varpow (powervars tm1) 

392 
val vdegs2 = map dest_varpow (powervars tm2) 

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

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

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

396 
else lexorder vdegs1 vdegs2 

397 
end 

398 
end; 

399 

400 
(* Addition of two polynomials. *) 

401 

402 
val polynomial_add_conv = 

403 
let 

404 
fun dezero_rule th = 

405 
let 

406 
val tm = concl th 

407 
in 

408 
if not(is_add tm) then th else 

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

410 
val l = Thm.dest_arg lopr 

411 
in 

412 
if l aconvc zero_tm 

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

414 
if r aconvc zero_tm 

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

416 
end 

417 
end 

418 
fun padd tm = 

419 
let 

420 
val (l,r) = dest_add tm 

421 
in 

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

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

424 
else 

425 
if is_add l 

426 
then 

427 
let val (a,b) = dest_add l 

428 
in 

429 
if is_add r then 

430 
let val (c,d) = dest_add r 

431 
val ord = morder a c 

432 
in 

433 
if ord = 0 then 

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

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

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

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

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

439 
end 

440 
else (* ord <> 0*) 

441 
let val th1 = 

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

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

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

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

446 
end 

447 
end 

448 
else (* not (is_add r)*) 

449 
let val ord = morder a r 

450 
in 

451 
if ord = 0 then 

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

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

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

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

456 
in dezero_rule (transitive th1 th2) 

457 
end 

458 
else (* ord <> 0*) 

459 
if ord > 0 then 

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

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

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

463 
end 

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

465 
end 

466 
end 

467 
else (* not (is_add l)*) 

468 
if is_add r then 

469 
let val (c,d) = dest_add r 

470 
val ord = morder l c 

471 
in 

472 
if ord = 0 then 

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

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

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

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

477 
in dezero_rule (transitive th1 th2) 

478 
end 

479 
else 

480 
if ord > 0 then reflexive tm 

481 
else 

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

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

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

485 
end 

486 
end 

487 
else 

488 
let val ord = morder l r 

489 
in 

490 
if ord = 0 then monomial_add_conv tm 

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

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

493 
end 

494 
end 

495 
in padd 

496 
end; 

497 

498 
(* Multiplication of two polynomials. *) 

499 

500 
val polynomial_mul_conv = 

501 
let 

502 
fun pmul tm = 

503 
let val (l,r) = dest_mul tm 

504 
in 

505 
if not(is_add l) then polynomial_monomial_mul_conv tm 

506 
else 

507 
if not(is_add r) then 

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

509 
in transitive th1 (polynomial_monomial_mul_conv(concl th1)) 

510 
end 

511 
else 

512 
let val (a,b) = dest_add l 

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

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

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

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

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

518 
in transitive th3 (polynomial_add_conv (concl th3)) 

519 
end 

520 
end 

521 
in fn tm => 

522 
let val (l,r) = dest_mul tm 

523 
in 

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

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

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

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

528 
else pmul tm 

529 
end 

530 
end; 

531 

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

533 

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

535 
val num_conv = fn n => 

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

537 
> Thm.symmetric; 

538 

539 

540 
val polynomial_pow_conv = 

541 
let 

542 
fun ppow tm = 

543 
let val (l,n) = dest_pow tm 

544 
in 

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

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

547 
else 

548 
let val th1 = num_conv n 

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

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

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

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

553 
in transitive th4 (polynomial_mul_conv (concl th4)) 

554 
end 

555 
end 

556 
in fn tm => 

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

558 
end; 

559 

560 
(* Negation. *) 

561 

562 
val polynomial_neg_conv = 

563 
fn tm => 

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

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

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

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

568 
in transitive th2 (polynomial_monomial_mul_conv (concl th2)) 

569 
end 

570 
end; 

571 

572 

573 
(* Subtraction. *) 

574 
val polynomial_sub_conv = fn tm => 

575 
let val (l,r) = dest_sub tm 

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

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

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

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

580 
end; 

581 

582 
(* Conversion from HOL term. *) 

583 

584 
fun polynomial_conv tm = 

23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

585 
if is_semiring_constant tm then semiring_add_conv tm 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

586 
else if not(is_comb tm) then reflexive tm 
23252  587 
else 
588 
let val (lopr,r) = Thm.dest_comb tm 

589 
in if lopr aconvc neg_tm then 

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

591 
in transitive th1 (polynomial_neg_conv (concl th1)) 

592 
end 

593 
else 

594 
if not(is_comb lopr) then reflexive tm 

595 
else 

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

597 
in if opr aconvc pow_tm andalso is_numeral r 

598 
then 

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

600 
in transitive th1 (polynomial_pow_conv (concl th1)) 

601 
end 

602 
else 

603 
if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm 

604 
then 

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

606 
val f = if opr aconvc add_tm then polynomial_add_conv 

607 
else if opr aconvc mul_tm then polynomial_mul_conv 

608 
else polynomial_sub_conv 

609 
in transitive th1 (f (concl th1)) 

610 
end 

611 
else reflexive tm 

612 
end 

613 
end; 

614 
in 

615 
{main = polynomial_conv, 

616 
add = polynomial_add_conv, 

617 
mul = polynomial_mul_conv, 

618 
pow = polynomial_pow_conv, 

619 
neg = polynomial_neg_conv, 

620 
sub = polynomial_sub_conv} 

621 
end 

622 
end; 

623 

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

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

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

627 

23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

628 
fun simple_cterm_ord t u = Term.term_ord (term_of t, term_of u) = LESS; 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

629 
fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom}, 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

630 
{conv, dest_const, mk_const, is_const}) ord = 
23252  631 
let 
632 
val pow_conv = 

633 
arg_conv (Simplifier.rewrite nat_exp_ss) 

634 
then_conv Simplifier.rewrite 

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

23330
01c09922ce59
Conversion for computation on constants now depends on the context
chaieb
parents:
23259
diff
changeset

636 
then_conv conv ctxt 
01c09922ce59
Conversion for computation on constants now depends on the context
chaieb
parents:
23259
diff
changeset

637 
val dat = (is_const, conv ctxt, conv ctxt, pow_conv) 
23252  638 
val {main, ...} = semiring_normalizers_conv vars semiring ring dat ord 
639 
in main end; 

640 

23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

641 
fun semiring_normalize_wrapper ctxt data = 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

642 
semiring_normalize_ord_wrapper ctxt data simple_cterm_ord; 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

643 

0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

644 
fun semiring_normalize_ord_conv ctxt ord tm = 
23252  645 
(case NormalizerData.match ctxt tm of 
646 
NONE => reflexive tm 

23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

647 
 SOME res => semiring_normalize_ord_wrapper ctxt res ord tm); 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

648 

23252  649 

23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

650 
fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord; 
23252  651 

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

653 
rtac (semiring_normalize_conv ctxt 

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

655 
end; 