author  wenzelm 
Mon, 19 Oct 2009 21:54:57 +0200  
changeset 33002  f3f02f36a3e2 
parent 31790  05c92381363c 
child 35064  1bdef0c013d3 
permissions  rwrr 
23252  1 
(* Title: HOL/Tools/Groebner_Basis/normalizer.ML 
2 
Author: Amine Chaieb, TU Muenchen 

3 
*) 

4 

5 
signature NORMALIZER = 

6 
sig 

23485  7 
val semiring_normalize_conv : Proof.context > conv 
8 
val semiring_normalize_ord_conv : Proof.context > (cterm > cterm > bool) > conv 

23252  9 
val semiring_normalize_tac : Proof.context > int > tactic 
23485  10 
val semiring_normalize_wrapper : Proof.context > NormalizerData.entry > conv 
27222  11 
val semiring_normalizers_ord_wrapper : 
12 
Proof.context > NormalizerData.entry > (cterm > cterm > bool) > 

13 
{add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} 

23485  14 
val semiring_normalize_ord_wrapper : Proof.context > NormalizerData.entry > 
15 
(cterm > cterm > bool) > conv 

23252  16 
val semiring_normalizers_conv : 
30866  17 
cterm list > cterm list * thm 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 

25253  25 
open Conv; 
23252  26 

27 
(* Very basic stuff for terms *) 

25253  28 

29 
fun is_comb ct = 

30 
(case Thm.term_of ct of 

31 
_ $ _ => true 

32 
 _ => false); 

33 

34 
val concl = Thm.cprop_of #> Thm.dest_arg; 

35 

36 
fun is_binop ct ct' = 

37 
(case Thm.term_of ct' of 

38 
c $ _ $ _ => term_of ct aconv c 

39 
 _ => false); 

40 

41 
fun dest_binop ct ct' = 

42 
if is_binop ct ct' then Thm.dest_binop ct' 

43 
else raise CTERM ("dest_binop: bad binop", [ct, ct']) 

44 

45 
fun inst_thm inst = Thm.instantiate ([], inst); 

46 

23252  47 
val dest_numeral = term_of #> HOLogic.dest_number #> snd; 
48 
val is_numeral = can dest_numeral; 

49 

50 
val numeral01_conv = Simplifier.rewrite 

25481  51 
(HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]); 
23252  52 
val zero1_numeral_conv = 
25481  53 
Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]); 
23580
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

54 
fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv; 
23252  55 
val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"}, 
56 
@{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, 

57 
@{thm "less_nat_number_of"}]; 

58 
val nat_add_conv = 

59 
zerone_conv 

60 
(Simplifier.rewrite 

61 
(HOL_basic_ss 

25481  62 
addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps} 
63 
@ [if_False, if_True, @{thm add_0}, @{thm add_Suc}, 

31790  64 
@{thm add_number_of_left}, @{thm Suc_eq_plus1}] 
25481  65 
@ map (fn th => th RS sym) @{thms numerals})); 
23252  66 

67 
val nat_mul_conv = nat_add_conv; 

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

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

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

71 

72 

73 
(* The main function! *) 

30866  74 
fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules) 
23252  75 
(is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) = 
76 
let 

77 

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

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

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

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

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

83 

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

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

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

87 

88 
val dest_add = dest_binop add_tm 

89 
val dest_mul = dest_binop mul_tm 

90 
fun dest_pow tm = 

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

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

93 
end; 

94 
val is_add = is_binop add_tm 

95 
val is_mul = is_binop mul_tm 

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

97 

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

99 
(case (r_ops, r_rules) of 

30866  100 
([sub_pat, neg_pat], [neg_mul, sub_add]) => 
23252  101 
let 
102 
val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat) 

103 
val neg_tm = Thm.dest_fun neg_pat 

104 
val dest_sub = dest_binop sub_tm 

105 
val is_sub = is_binop sub_tm 

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

107 
sub_add > concl > Thm.dest_arg > Thm.dest_arg) 

30866  108 
end 
109 
 _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)); 

110 

111 
val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = 

112 
(case (f_ops, f_rules) of 

113 
([divide_pat, inverse_pat], [div_inv, inv_div]) => 

114 
let val div_tm = funpow 2 Thm.dest_fun divide_pat 

115 
val inv_tm = Thm.dest_fun inverse_pat 

116 
in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm) 

117 
end 

118 
 _ => (TrueI, TrueI, true_tm, true_tm, K false)); 

119 

23252  120 
in fn variable_order => 
121 
let 

122 

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

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

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

126 

127 
fun powvar_mul_conv tm = 

128 
let 

129 
val (l,r) = dest_mul tm 

130 
in if is_semiring_constant l andalso is_semiring_constant r 

131 
then semiring_mul_conv tm 

132 
else 

133 
((let 

134 
val (lx,ln) = dest_pow l 

135 
in 

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

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

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

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

140 
handle CTERM _ => 

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

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

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

144 
handle CTERM _ => 

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

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

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

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

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

150 

151 
)) 

152 
end; 

153 

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

155 

156 
fun monomial_deone th = 

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

158 
if l aconvc one_tm 

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

160 
handle CTERM _ => th; 

161 

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

163 

164 
val monomial_pow_conv = 

165 
let 

166 
fun monomial_pow tm bod ntm = 

167 
if not(is_comb bod) 

168 
then reflexive tm 

169 
else 

170 
if is_semiring_constant bod 

171 
then semiring_pow_conv tm 

172 
else 

173 
let 

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

175 
in if not(is_comb lopr) 

176 
then reflexive tm 

177 
else 

178 
let 

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

180 
in 

181 
if opr aconvc pow_tm andalso is_numeral r 

182 
then 

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

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

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

186 
end 

187 
else 

188 
if opr aconvc mul_tm 

189 
then 

190 
let 

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

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

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

194 
val thl = monomial_pow y l ntm 

195 
val thr = monomial_pow z r ntm 

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

197 
end 

198 
else reflexive tm 

199 
end 

200 
end 

201 
in fn tm => 

202 
let 

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

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

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

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

207 
else if r aconvc zeron_tm 

208 
then inst_thm [(cx,l)] pthm_35 

209 
else if r aconvc onen_tm 

210 
then inst_thm [(cx,l)] pthm_36 

211 
else monomial_deone(monomial_pow tm l r) 

212 
end 

213 
end; 

214 

215 
(* Multiplication of canonical monomials. *) 

216 
val monomial_mul_conv = 

217 
let 

218 
fun powvar tm = 

219 
if is_semiring_constant tm then one_tm 

220 
else 

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

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

223 
in if opr aconvc pow_tm andalso is_numeral r then l 

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

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

226 
fun vorder x y = 

227 
if x aconvc y then 0 

228 
else 

229 
if x aconvc one_tm then ~1 

230 
else if y aconvc one_tm then 1 

231 
else if variable_order x y then ~1 else 1 

232 
fun monomial_mul tm l r = 

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

234 
in 

235 
((let 

236 
val (rx,ry) = dest_mul r 

237 
val vr = powvar rx 

238 
val ord = vorder vl vr 

239 
in 

240 
if ord = 0 

241 
then 

242 
let 

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

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

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

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

247 
val th3 = transitive th1 th2 

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

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

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

251 
in transitive th3 (Drule.arg_cong_rule tm5 th4) 

252 
end 

253 
else 

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

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

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

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

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

259 
end 

260 
end) 

261 
handle CTERM _ => 

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

263 
in 

264 
if ord = 0 then 

265 
let 

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

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

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

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

270 
in transitive th1 th2 

271 
end 

272 
else 

273 
if ord < 0 then 

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

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

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

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

278 
end 

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

280 
end)) end) 

281 
handle CTERM _ => 

282 
(let val vl = powvar l in 

283 
((let 

284 
val (rx,ry) = dest_mul r 

285 
val vr = powvar rx 

286 
val ord = vorder vl vr 

287 
in if ord = 0 then 

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

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

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

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

292 
end 

293 
else if ord > 0 then 

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

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

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

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

298 
end 

299 
else reflexive tm 

300 
end) 

301 
handle CTERM _ => 

302 
(let val vr = powvar r 

303 
val ord = vorder vl vr 

304 
in if ord = 0 then powvar_mul_conv tm 

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

306 
else reflexive tm 

307 
end)) end)) 

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

309 
end 

310 
end; 

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

312 

313 
val polynomial_monomial_mul_conv = 

314 
let 

315 
fun pmm_conv tm = 

316 
let val (l,r) = dest_mul tm 

317 
in 

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

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

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

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

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

323 
in transitive th1 th2 

324 
end) 

325 
handle CTERM _ => monomial_mul_conv tm) 

326 
end 

327 
in pmm_conv 

328 
end; 

329 

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

331 

332 
fun monomial_add_conv tm = 

333 
let val (l,r) = dest_add tm 

334 
in if is_semiring_constant l andalso is_semiring_constant r 

335 
then semiring_add_conv tm 

336 
else 

337 
let val th1 = 

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

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

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

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

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

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

344 
else inst_thm [(cm,r)] pthm_05 

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

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

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

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

349 
val tm5 = concl th3 

350 
in 

351 
if (Thm.dest_arg1 tm5) aconvc zero_tm 

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

353 
else monomial_deone th3 

354 
end 

355 
end; 

356 

357 
(* Ordering on monomials. *) 

358 

359 
fun striplist dest = 

360 
let fun strip x acc = 

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

362 
strip l (strip r acc) end) 

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

364 
in fn x => strip x [] 

365 
end; 

366 

367 

368 
fun powervars tm = 

369 
let val ptms = striplist dest_mul tm 

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

371 
end; 

372 
val num_0 = 0; 

373 
val num_1 = 1; 

374 
fun dest_varpow tm = 

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

376 
handle CTERM _ => 

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

378 

379 
val morder = 

380 
let fun lexorder l1 l2 = 

381 
case (l1,l2) of 

382 
([],[]) => 0 

383 
 (vps,[]) => ~1 

384 
 ([],vps) => 1 

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

386 
if variable_order x1 x2 then 1 

387 
else if variable_order x2 x1 then ~1 

388 
else if n1 < n2 then ~1 

389 
else if n2 < n1 then 1 

390 
else lexorder vs1 vs2 

391 
in fn tm1 => fn tm2 => 

392 
let val vdegs1 = map dest_varpow (powervars tm1) 

393 
val vdegs2 = map dest_varpow (powervars tm2) 

33002  394 
val deg1 = fold (Integer.add o snd) vdegs1 num_0 
395 
val deg2 = fold (Integer.add o snd) vdegs2 num_0 

23252  396 
in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1 
397 
else lexorder vdegs1 vdegs2 

398 
end 

399 
end; 

400 

401 
(* Addition of two polynomials. *) 

402 

403 
val polynomial_add_conv = 

404 
let 

405 
fun dezero_rule th = 

406 
let 

407 
val tm = concl th 

408 
in 

409 
if not(is_add tm) then th else 

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

411 
val l = Thm.dest_arg lopr 

412 
in 

413 
if l aconvc zero_tm 

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

415 
if r aconvc zero_tm 

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

417 
end 

418 
end 

419 
fun padd tm = 

420 
let 

421 
val (l,r) = dest_add tm 

422 
in 

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

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

425 
else 

426 
if is_add l 

427 
then 

428 
let val (a,b) = dest_add l 

429 
in 

430 
if is_add r then 

431 
let val (c,d) = dest_add r 

432 
val ord = morder a c 

433 
in 

434 
if ord = 0 then 

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

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

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

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

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

440 
end 

441 
else (* ord <> 0*) 

442 
let val th1 = 

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

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

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

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

447 
end 

448 
end 

449 
else (* not (is_add r)*) 

450 
let val ord = morder a r 

451 
in 

452 
if ord = 0 then 

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

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

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

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

457 
in dezero_rule (transitive th1 th2) 

458 
end 

459 
else (* ord <> 0*) 

460 
if ord > 0 then 

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

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

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

464 
end 

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

466 
end 

467 
end 

468 
else (* not (is_add l)*) 

469 
if is_add r then 

470 
let val (c,d) = dest_add r 

471 
val ord = morder l c 

472 
in 

473 
if ord = 0 then 

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

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

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

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

478 
in dezero_rule (transitive th1 th2) 

479 
end 

480 
else 

481 
if ord > 0 then reflexive tm 

482 
else 

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

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

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

486 
end 

487 
end 

488 
else 

489 
let val ord = morder l r 

490 
in 

491 
if ord = 0 then monomial_add_conv tm 

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

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

494 
end 

495 
end 

496 
in padd 

497 
end; 

498 

499 
(* Multiplication of two polynomials. *) 

500 

501 
val polynomial_mul_conv = 

502 
let 

503 
fun pmul tm = 

504 
let val (l,r) = dest_mul tm 

505 
in 

506 
if not(is_add l) then polynomial_monomial_mul_conv tm 

507 
else 

508 
if not(is_add r) then 

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

510 
in transitive th1 (polynomial_monomial_mul_conv(concl th1)) 

511 
end 

512 
else 

513 
let val (a,b) = dest_add l 

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

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

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

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

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

519 
in transitive th3 (polynomial_add_conv (concl th3)) 

520 
end 

521 
end 

522 
in fn tm => 

523 
let val (l,r) = dest_mul tm 

524 
in 

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

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

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

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

529 
else pmul tm 

530 
end 

531 
end; 

532 

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

534 

23580
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

535 
fun num_conv n = 
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

536 
nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n  1))) 
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

537 
> Thm.symmetric; 
23252  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 

23580
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

562 
fun polynomial_neg_conv tm = 
23252  563 
let val (l,r) = Thm.dest_comb tm in 
564 
if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else 

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

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

567 
in transitive th2 (polynomial_monomial_mul_conv (concl th2)) 

568 
end 

569 
end; 

570 

571 

572 
(* Subtraction. *) 

23580
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

573 
fun polynomial_sub_conv tm = 
23252  574 
let val (l,r) = dest_sub tm 
575 
val th1 = inst_thm [(cx',l),(cy',r)] sub_add 

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

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

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

579 
end; 

580 

581 
(* Conversion from HOL term. *) 

582 

583 
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

584 
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

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

588 
in if lopr aconvc neg_tm then 

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

590 
in transitive th1 (polynomial_neg_conv (concl th1)) 

591 
end 

30866  592 
else if lopr aconvc inverse_tm then 
593 
let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) 

594 
in transitive th1 (semiring_mul_conv (concl th1)) 

595 
end 

23252  596 
else 
597 
if not(is_comb lopr) then reflexive tm 

598 
else 

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

600 
in if opr aconvc pow_tm andalso is_numeral r 

601 
then 

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

603 
in transitive th1 (polynomial_pow_conv (concl th1)) 

604 
end 

30866  605 
else if opr aconvc divide_tm 
606 
then 

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

608 
(polynomial_conv r) 

609 
val th2 = (rewr_conv divide_inverse then_conv polynomial_mul_conv) 

610 
(Thm.rhs_of th1) 

611 
in transitive th1 th2 

612 
end 

23252  613 
else 
614 
if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm 

615 
then 

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

617 
val f = if opr aconvc add_tm then polynomial_add_conv 

618 
else if opr aconvc mul_tm then polynomial_mul_conv 

619 
else polynomial_sub_conv 

620 
in transitive th1 (f (concl th1)) 

621 
end 

622 
else reflexive tm 

623 
end 

624 
end; 

625 
in 

626 
{main = polynomial_conv, 

627 
add = polynomial_add_conv, 

628 
mul = polynomial_mul_conv, 

629 
pow = polynomial_pow_conv, 

630 
neg = polynomial_neg_conv, 

631 
sub = polynomial_sub_conv} 

632 
end 

633 
end; 

634 

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

25481  636 
val nat_exp_ss = HOL_basic_ss addsimps (@{thms nat_number} @ nat_arith @ @{thms arith_simps} @ @{thms rel_simps}) 
23880  637 
addsimps [Let_def, if_False, if_True, @{thm add_0}, @{thm add_Suc}]; 
23252  638 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
27222
diff
changeset

639 
fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS; 
27222  640 

30866  641 
fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, 
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

642 
{conv, dest_const, mk_const, is_const}) ord = 
23252  643 
let 
644 
val pow_conv = 

645 
arg_conv (Simplifier.rewrite nat_exp_ss) 

646 
then_conv Simplifier.rewrite 

647 
(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

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

649 
val dat = (is_const, conv ctxt, conv ctxt, pow_conv) 
30866  650 
in semiring_normalizers_conv vars semiring ring field dat ord end; 
27222  651 

30866  652 
fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord = 
653 
#main (semiring_normalizers_ord_wrapper ctxt ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal},{conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord); 

23252  654 

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

655 
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

656 
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

657 

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

658 
fun semiring_normalize_ord_conv ctxt ord tm = 
23252  659 
(case NormalizerData.match ctxt tm of 
660 
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

661 
 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

662 

23252  663 

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

664 
fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord; 
23252  665 

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

667 
rtac (semiring_normalize_conv ctxt 

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

669 
end; 