author  chaieb 
Mon, 11 Jun 2007 11:05:57 +0200  
changeset 23312  6e32a5bfc30f 
parent 23266  50f0a4f12ed3 
child 23327  1654013ec97c 
permissions  rwrr 
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") 

23312  14 
("Tools/Groebner_Basis/groebner.ML") 
23252  15 
begin 
16 

17 
subsection {* Semiring normalization *} 

18 

19 
setup NormalizerData.setup 

20 

21 

23258
9062e98fdab1
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
wenzelm
parents:
23252
diff
changeset

22 
locale gb_semiring = 
23252  23 
fixes add mul pwr r0 r1 
24 
assumes add_a:"(add x (add y z) = add (add x y) z)" 

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

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

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

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

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

30 
begin 

31 

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

33 
proof (induct p) 

34 
case 0 

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

36 
next 

37 
case Suc 

38 
from this [symmetric] show ?case 

39 
by (auto simp add: pwr_Suc mul_1 mul_a) 

40 
qed 

41 

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

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

44 
fix q x y 

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

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

47 
by (simp add: mul_a) 

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

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

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

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

52 
qed 

53 

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

55 
proof (induct p arbitrary: q) 

56 
case 0 

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

58 
next 

59 
case Suc 

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

61 
qed 

62 

63 

64 
subsubsection {* Declaring the abstract theory *} 

65 

66 
lemma semiring_ops: 

67 
includes meta_term_syntax 

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

69 
and "TERM r0" and "TERM r1" 

70 
by rule+ 

71 

72 
lemma semiring_rules: 

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

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

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

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

77 
"add r0 a = a" 

78 
"add a r0 = a" 

79 
"mul a b = mul b a" 

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

81 
"mul r0 a = r0" 

82 
"mul a r0 = r0" 

83 
"mul r1 a = a" 

84 
"mul a r1 = a" 

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

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

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

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

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

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

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

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

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

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

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

96 
"add a c = add c a" 

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

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

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

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

101 
"mul x x = pwr x 2" 

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

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

104 
"pwr x 0 = r1" 

105 
"pwr x 1 = x" 

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

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

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

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

110 
proof  

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

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

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

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

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

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

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

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

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

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

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

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

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

124 
using mul_c mul_a by simp 

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

126 
using mul_a by simp 

127 
next 

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

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

130 
finally 

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

132 
using mul_c by simp 

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

134 
next 

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

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

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

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

139 
using add_c add_a by simp 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

158 
by (simp add: nat_number pwr_Suc mul_pwr) 

159 
qed 

160 

161 

162 
lemma "axioms" [normalizer 

163 
semiring ops: semiring_ops 

164 
semiring rules: semiring_rules]: 

23258
9062e98fdab1
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
wenzelm
parents:
23252
diff
changeset

165 
"gb_semiring add mul pwr r0 r1" . 
23252  166 

167 
end 

168 

23258
9062e98fdab1
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
wenzelm
parents:
23252
diff
changeset

169 
interpretation class_semiring: gb_semiring 
23252  170 
["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"] 
171 
by unfold_locales (auto simp add: ring_eq_simps power_Suc) 

172 

173 
lemmas nat_arith = 

174 
add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of 

175 

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

177 
by (simp add: numeral_1_eq_1) 

178 
lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False 

179 
if_True add_0 add_Suc add_number_of_left mult_number_of_left 

180 
numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1 

181 
numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1 

182 
iszero_number_of_1 iszero_number_of_0 nonzero_number_of_Min 

183 
iszero_number_of_Pls iszero_0 not_iszero_Numeral1 

184 

185 
lemmas semiring_norm = comp_arith 

186 

187 
ML {* 

188 
fun numeral_is_const ct = 

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

190 

191 
val numeral_conv = 

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

193 
Simplifier.rewrite (HOL_basic_ss addsimps 

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

195 
*} 

196 

197 
ML {* 

198 
fun int_of_rat x = 

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

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

201 
*} 

202 

203 
declaration {* 

204 
NormalizerData.funs @{thm class_semiring.axioms} 

205 
{is_const = fn phi => numeral_is_const, 

206 
dest_const = fn phi => fn ct => 

207 
Rat.rat_of_int (snd 

208 
(HOLogic.dest_number (Thm.term_of ct) 

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

210 
mk_const = fn phi => fn cT => fn x => 

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

212 
conv = fn phi => numeral_conv} 

213 
*} 

214 

215 

23258
9062e98fdab1
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
wenzelm
parents:
23252
diff
changeset

216 
locale gb_ring = gb_semiring + 
23252  217 
fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
218 
and neg :: "'a \<Rightarrow> 'a" 

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

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

221 
begin 

222 

223 
lemma ring_ops: 

224 
includes meta_term_syntax 

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

226 

227 
lemmas ring_rules = neg_mul sub_add 

228 

229 
lemma "axioms" [normalizer 

230 
semiring ops: semiring_ops 

231 
semiring rules: semiring_rules 

232 
ring ops: ring_ops 

233 
ring rules: ring_rules]: 

23258
9062e98fdab1
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
wenzelm
parents:
23252
diff
changeset

234 
"gb_ring add mul pwr r0 r1 sub neg" . 
23252  235 

236 
end 

237 

238 

23258
9062e98fdab1
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
wenzelm
parents:
23252
diff
changeset

239 
interpretation class_ring: gb_ring ["op +" "op *" "op ^" 
23252  240 
"0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op " "uminus"] 
241 
by unfold_locales simp_all 

242 

243 

244 
declaration {* 

245 
NormalizerData.funs @{thm class_ring.axioms} 

246 
{is_const = fn phi => numeral_is_const, 

247 
dest_const = fn phi => fn ct => 

248 
Rat.rat_of_int (snd 

249 
(HOLogic.dest_number (Thm.term_of ct) 

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

251 
mk_const = fn phi => fn cT => fn x => 

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

253 
conv = fn phi => numeral_conv} 

254 
*} 

255 

256 
use "Tools/Groebner_Basis/normalizer.ML" 

257 

258 
method_setup sring_norm = {* 

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

260 
*} "Semiring_normalizer" 

261 

262 

23266  263 
subsection {* Groebner Bases *} 
23252  264 

23258
9062e98fdab1
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
wenzelm
parents:
23252
diff
changeset

265 
locale semiringb = gb_semiring + 
23252  266 
assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z" 
267 
and add_mul_solve: "add (mul w y) (mul x z) = 

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

269 
begin 

270 

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

272 
proof 

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

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

275 
using add_mul_solve by blast 

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

277 
by simp 

278 
qed 

279 

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

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

282 
proof(clarify) 

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

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

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

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

287 
using mul_0 add_cancel by simp 

288 
thus "False" using add_mul_solve nz cnd by simp 

289 
qed 

290 

291 
declare "axioms" [normalizer del] 

292 

293 
lemma "axioms" [normalizer 

294 
semiring ops: semiring_ops 

295 
semiring rules: semiring_rules 

296 
idom rules: noteq_reduce add_scale_eq_noteq]: 

297 
"semiringb add mul pwr r0 r1" . 

298 

299 
end 

300 

23258
9062e98fdab1
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
wenzelm
parents:
23252
diff
changeset

301 
locale ringb = semiringb + gb_ring 
23252  302 
begin 
303 

304 
declare "axioms" [normalizer del] 

305 

306 
lemma "axioms" [normalizer 

307 
semiring ops: semiring_ops 

308 
semiring rules: semiring_rules 

309 
ring ops: ring_ops 

310 
ring rules: ring_rules 

311 
idom rules: noteq_reduce add_scale_eq_noteq]: 

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

313 

314 
end 

315 

316 
lemma no_zero_divirors_neq0: 

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

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

319 
proof  

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

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

322 
thus "b = 0" by blast 

323 
qed 

324 

325 
interpretation class_ringb: ringb 

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

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

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

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

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

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

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

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

334 
with no_zero_divirors_neq0 [OF ynz'] 

335 
have "w  x = 0" by blast 

336 
thus "w = x" by simp 

337 
qed 

338 

339 

340 
declaration {* 

341 
NormalizerData.funs @{thm class_ringb.axioms} 

342 
{is_const = fn phi => numeral_is_const, 

343 
dest_const = fn phi => fn ct => 

344 
Rat.rat_of_int (snd 

345 
(HOLogic.dest_number (Thm.term_of ct) 

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

347 
mk_const = fn phi => fn cT => fn x => 

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

349 
conv = fn phi => numeral_conv} 

350 
*} 

351 

352 

353 
interpretation natgb: semiringb 

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

355 
proof (unfold_locales, simp add: ring_eq_simps power_Suc) 

356 
fix w x y z ::"nat" 

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

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

359 
moreover { 

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

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

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

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

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

365 
moreover { 

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

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

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

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

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

371 
ultimately have "w=x" by blast } 

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

373 
qed 

374 

375 
declaration {* 

376 
NormalizerData.funs @{thm natgb.axioms} 

377 
{is_const = fn phi => numeral_is_const, 

378 
dest_const = fn phi => fn ct => 

379 
Rat.rat_of_int (snd 

380 
(HOLogic.dest_number (Thm.term_of ct) 

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

382 
mk_const = fn phi => fn cT => fn x => 

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

384 
conv = fn phi => numeral_conv} 

385 
*} 

386 

387 

23258
9062e98fdab1
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
wenzelm
parents:
23252
diff
changeset

388 
lemmas bool_simps = simp_thms(134) 
23252  389 
lemma dnf: 
390 
"(P & (Q  R)) = ((P&Q)  (P&R))" "((Q  R) & P) = ((Q&P)  (R&P))" 

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

392 
by blast+ 

393 

394 
lemmas weak_dnf_simps = dnf bool_simps 

395 

396 
lemma nnf_simps: 

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

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

399 
by blast+ 

400 

401 
lemma PFalse: 

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

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

404 
by auto 

405 

406 
use "Tools/Groebner_Basis/groebner.ML" 

407 

408 
ML {* 

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

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

411 
*} 

412 

413 
method_setup algebra = {* 

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

415 
*} "" 

416 

417 
end 