# HG changeset patch # User haftmann # Date 1273331750 -7200 # Node ID 5ce217fc769af0cfab0d3adff40204b6b46dc926 # Parent dce592144219ddd9ad594b375d71ac9f54a1bdf1# Parent 5cf4e9128f222bb67a04f482ab87a64a1f0ab164 merged diff -r dce592144219 -r 5ce217fc769a src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri May 07 23:44:10 2010 +0200 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sat May 08 17:15:50 2010 +0200 @@ -700,14 +700,14 @@ val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t]) (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv - (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th + (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th in rth end | ("x+t",[t]) => let val T = ctyp_of_term x val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"} val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv - (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th + (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th in rth end | ("c*x",[c]) => let @@ -744,14 +744,14 @@ val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t]) (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv - (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th + (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th in rth end | ("x+t",[t]) => let val T = ctyp_of_term x val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"} val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv - (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th + (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th in rth end | ("c*x",[c]) => let @@ -786,14 +786,14 @@ val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv - (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th + (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th in rth end | ("x+t",[t]) => let val T = ctyp_of_term x val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"} val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv - (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th + (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th in rth end | ("c*x",[c]) => let @@ -822,7 +822,7 @@ val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0 val nth = Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv - (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th + (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) in rth end | Const(@{const_name Orderings.less_eq},_)$a$b => @@ -831,7 +831,7 @@ val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0 val nth = Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv - (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th + (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) in rth end @@ -841,7 +841,7 @@ val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0 val nth = Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv - (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th + (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) in rth end | @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct diff -r dce592144219 -r 5ce217fc769a src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Fri May 07 23:44:10 2010 +0200 +++ b/src/HOL/Groebner_Basis.thy Sat May 08 17:15:50 2010 +0200 @@ -2,341 +2,14 @@ Author: Amine Chaieb, TU Muenchen *) -header {* Semiring normalization and Groebner Bases *} +header {* Groebner bases *} theory Groebner_Basis -imports Numeral_Simprocs Nat_Transfer +imports Semiring_Normalization uses - "Tools/Groebner_Basis/normalizer.ML" - ("Tools/Groebner_Basis/groebner.ML") -begin - -subsection {* Semiring normalization *} - -setup Normalizer.setup - -locale normalizing_semiring = - fixes add mul pwr r0 r1 - assumes add_a:"(add x (add y z) = add (add x y) z)" - and add_c: "add x y = add y x" and add_0:"add r0 x = x" - and mul_a:"mul x (mul y z) = mul (mul x y) z" and mul_c:"mul x y = mul y x" - and mul_1:"mul r1 x = x" and mul_0:"mul r0 x = r0" - and mul_d:"mul x (add y z) = add (mul x y) (mul x z)" - and pwr_0:"pwr x 0 = r1" and pwr_Suc:"pwr x (Suc n) = mul x (pwr x n)" -begin - -lemma mul_pwr:"mul (pwr x p) (pwr x q) = pwr x (p + q)" -proof (induct p) - case 0 - then show ?case by (auto simp add: pwr_0 mul_1) -next - case Suc - from this [symmetric] show ?case - by (auto simp add: pwr_Suc mul_1 mul_a) -qed - -lemma pwr_mul: "pwr (mul x y) q = mul (pwr x q) (pwr y q)" -proof (induct q arbitrary: x y, auto simp add:pwr_0 pwr_Suc mul_1) - fix q x y - assume "\x y. pwr (mul x y) q = mul (pwr x q) (pwr y q)" - have "mul (mul x y) (mul (pwr x q) (pwr y q)) = mul x (mul y (mul (pwr x q) (pwr y q)))" - by (simp add: mul_a) - also have "\ = (mul (mul y (mul (pwr y q) (pwr x q))) x)" by (simp add: mul_c) - also have "\ = (mul (mul y (pwr y q)) (mul (pwr x q) x))" by (simp add: mul_a) - finally show "mul (mul x y) (mul (pwr x q) (pwr y q)) = - mul (mul x (pwr x q)) (mul y (pwr y q))" by (simp add: mul_c) -qed - -lemma pwr_pwr: "pwr (pwr x p) q = pwr x (p * q)" -proof (induct p arbitrary: q) - case 0 - show ?case using pwr_Suc mul_1 pwr_0 by (induct q) auto -next - case Suc - thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc) -qed - -lemma semiring_ops: - shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)" - and "TERM r0" and "TERM r1" . - -lemma semiring_rules: - "add (mul a m) (mul b m) = mul (add a b) m" - "add (mul a m) m = mul (add a r1) m" - "add m (mul a m) = mul (add a r1) m" - "add m m = mul (add r1 r1) m" - "add r0 a = a" - "add a r0 = a" - "mul a b = mul b a" - "mul (add a b) c = add (mul a c) (mul b c)" - "mul r0 a = r0" - "mul a r0 = r0" - "mul r1 a = a" - "mul a r1 = a" - "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)" - "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))" - "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)" - "mul (mul lx ly) rx = mul (mul lx rx) ly" - "mul (mul lx ly) rx = mul lx (mul ly rx)" - "mul lx (mul rx ry) = mul (mul lx rx) ry" - "mul lx (mul rx ry) = mul rx (mul lx ry)" - "add (add a b) (add c d) = add (add a c) (add b d)" - "add (add a b) c = add a (add b c)" - "add a (add c d) = add c (add a d)" - "add (add a b) c = add (add a c) b" - "add a c = add c a" - "add a (add c d) = add (add a c) d" - "mul (pwr x p) (pwr x q) = pwr x (p + q)" - "mul x (pwr x q) = pwr x (Suc q)" - "mul (pwr x q) x = pwr x (Suc q)" - "mul x x = pwr x 2" - "pwr (mul x y) q = mul (pwr x q) (pwr y q)" - "pwr (pwr x p) q = pwr x (p * q)" - "pwr x 0 = r1" - "pwr x 1 = x" - "mul x (add y z) = add (mul x y) (mul x z)" - "pwr x (Suc q) = mul x (pwr x q)" - "pwr x (2*n) = mul (pwr x n) (pwr x n)" - "pwr x (Suc (2*n)) = mul x (mul (pwr x n) (pwr x n))" -proof - - show "add (mul a m) (mul b m) = mul (add a b) m" using mul_d mul_c by simp -next show"add (mul a m) m = mul (add a r1) m" using mul_d mul_c mul_1 by simp -next show "add m (mul a m) = mul (add a r1) m" using mul_c mul_d mul_1 add_c by simp -next show "add m m = mul (add r1 r1) m" using mul_c mul_d mul_1 by simp -next show "add r0 a = a" using add_0 by simp -next show "add a r0 = a" using add_0 add_c by simp -next show "mul a b = mul b a" using mul_c by simp -next show "mul (add a b) c = add (mul a c) (mul b c)" using mul_c mul_d by simp -next show "mul r0 a = r0" using mul_0 by simp -next show "mul a r0 = r0" using mul_0 mul_c by simp -next show "mul r1 a = a" using mul_1 by simp -next show "mul a r1 = a" using mul_1 mul_c by simp -next show "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)" - using mul_c mul_a by simp -next show "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))" - using mul_a by simp -next - have "mul (mul lx ly) (mul rx ry) = mul (mul rx ry) (mul lx ly)" by (rule mul_c) - also have "\ = mul rx (mul ry (mul lx ly))" using mul_a by simp - finally - show "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)" - using mul_c by simp -next show "mul (mul lx ly) rx = mul (mul lx rx) ly" using mul_c mul_a by simp -next - show "mul (mul lx ly) rx = mul lx (mul ly rx)" by (simp add: mul_a) -next show "mul lx (mul rx ry) = mul (mul lx rx) ry" by (simp add: mul_a ) -next show "mul lx (mul rx ry) = mul rx (mul lx ry)" by (simp add: mul_a,simp add: mul_c) -next show "add (add a b) (add c d) = add (add a c) (add b d)" - using add_c add_a by simp -next show "add (add a b) c = add a (add b c)" using add_a by simp -next show "add a (add c d) = add c (add a d)" - apply (simp add: add_a) by (simp only: add_c) -next show "add (add a b) c = add (add a c) b" using add_a add_c by simp -next show "add a c = add c a" by (rule add_c) -next show "add a (add c d) = add (add a c) d" using add_a by simp -next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr) -next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp -next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp -next show "mul x x = pwr x 2" by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c) -next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul) -next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr) -next show "pwr x 0 = r1" using pwr_0 . -next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c) -next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp -next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp -next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number' mul_pwr) -next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))" - by (simp add: nat_number' pwr_Suc mul_pwr) -qed - - -lemmas normalizing_semiring_axioms' = - normalizing_semiring_axioms [normalizer - semiring ops: semiring_ops - semiring rules: semiring_rules] - -end - -sublocale comm_semiring_1 - < normalizing!: normalizing_semiring plus times power zero one -proof -qed (simp_all add: algebra_simps) - -declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *} - -locale normalizing_ring = normalizing_semiring + - fixes sub :: "'a \ 'a \ 'a" - and neg :: "'a \ 'a" - assumes neg_mul: "neg x = mul (neg r1) x" - and sub_add: "sub x y = add x (neg y)" + ("Tools/groebner.ML") begin -lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" . - -lemmas ring_rules = neg_mul sub_add - -lemmas normalizing_ring_axioms' = - normalizing_ring_axioms [normalizer - semiring ops: semiring_ops - semiring rules: semiring_rules - ring ops: ring_ops - ring rules: ring_rules] - -end - -sublocale comm_ring_1 - < normalizing!: normalizing_ring plus times power zero one minus uminus -proof -qed (simp_all add: diff_minus) - -declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *} - -locale normalizing_field = normalizing_ring + - fixes divide :: "'a \ 'a \ 'a" - and inverse:: "'a \ 'a" - assumes divide_inverse: "divide x y = mul x (inverse y)" - and inverse_divide: "inverse x = divide r1 x" -begin - -lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" . - -lemmas field_rules = divide_inverse inverse_divide - -lemmas normalizing_field_axioms' = - normalizing_field_axioms [normalizer - semiring ops: semiring_ops - semiring rules: semiring_rules - ring ops: ring_ops - ring rules: ring_rules - field ops: field_ops - field rules: field_rules] - -end - -locale normalizing_semiring_cancel = normalizing_semiring + - assumes add_cancel: "add (x::'a) y = add x z \ y = z" - and add_mul_solve: "add (mul w y) (mul x z) = - add (mul w z) (mul x y) \ w = x \ y = z" -begin - -lemma noteq_reduce: "a \ b \ c \ d \ add (mul a c) (mul b d) \ add (mul a d) (mul b c)" -proof- - have "a \ b \ c \ d \ \ (a = b \ c = d)" by simp - also have "\ \ add (mul a c) (mul b d) \ add (mul a d) (mul b c)" - using add_mul_solve by blast - finally show "a \ b \ c \ d \ add (mul a c) (mul b d) \ add (mul a d) (mul b c)" - by simp -qed - -lemma add_scale_eq_noteq: "\r \ r0 ; (a = b) \ ~(c = d)\ - \ add a (mul r c) \ add b (mul r d)" -proof(clarify) - assume nz: "r\ r0" and cnd: "c\d" - and eq: "add b (mul r c) = add b (mul r d)" - hence "mul r c = mul r d" using cnd add_cancel by simp - hence "add (mul r0 d) (mul r c) = add (mul r0 c) (mul r d)" - using mul_0 add_cancel by simp - thus "False" using add_mul_solve nz cnd by simp -qed - -lemma add_r0_iff: " x = add x a \ a = r0" -proof- - have "a = r0 \ add x a = add x r0" by (simp add: add_cancel) - thus "x = add x a \ a = r0" by (auto simp add: add_c add_0) -qed - -declare normalizing_semiring_axioms' [normalizer del] - -lemmas normalizing_semiring_cancel_axioms' = - normalizing_semiring_cancel_axioms [normalizer - semiring ops: semiring_ops - semiring rules: semiring_rules - idom rules: noteq_reduce add_scale_eq_noteq] - -end - -locale normalizing_ring_cancel = normalizing_semiring_cancel + normalizing_ring + - assumes subr0_iff: "sub x y = r0 \ x = y" -begin - -declare normalizing_ring_axioms' [normalizer del] - -lemmas normalizing_ring_cancel_axioms' = normalizing_ring_cancel_axioms [normalizer - semiring ops: semiring_ops - semiring rules: semiring_rules - ring ops: ring_ops - ring rules: ring_rules - idom rules: noteq_reduce add_scale_eq_noteq - ideal rules: subr0_iff add_r0_iff] - -end - -sublocale idom - < normalizing!: normalizing_ring_cancel plus times power zero one minus uminus -proof - fix w x y z - show "w * y + x * z = w * z + x * y \ w = x \ y = z" - proof - assume "w * y + x * z = w * z + x * y" - then have "w * y + x * z - w * z - x * y = 0" by (simp add: algebra_simps) - then have "w * (y - z) - x * (y - z) = 0" by (simp add: algebra_simps) - then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps) - then have "y - z = 0 \ w - x = 0" by (rule divisors_zero) - then show "w = x \ y = z" by auto - qed (auto simp add: add_ac) -qed (simp_all add: algebra_simps) - -declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *} - -interpretation normalizing_nat!: normalizing_semiring_cancel - "op +" "op *" "op ^" "0::nat" "1" -proof (unfold_locales, simp add: algebra_simps) - fix w x y z ::"nat" - { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \ z" - hence "y < z \ y > z" by arith - moreover { - assume lt:"y k. z = y + k \ k > 0" by (rule_tac x="z - y" in exI, auto) - then obtain k where kp: "k>0" and yz:"z = y + k" by blast - from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps) - hence "x*k = w*k" by simp - hence "w = x" using kp by simp } - moreover { - assume lt: "y >z" hence "\k. y = z + k \ k>0" by (rule_tac x="y - z" in exI, auto) - then obtain k where kp: "k>0" and yz:"y = z + k" by blast - from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps) - hence "w*k = x*k" by simp - hence "w = x" using kp by simp } - ultimately have "w=x" by blast } - thus "(w * y + x * z = w * z + x * y) = (w = x \ y = z)" by auto -qed - -declaration {* Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *} - -locale normalizing_field_cancel = normalizing_ring_cancel + normalizing_field -begin - -declare normalizing_field_axioms' [normalizer del] - -lemmas normalizing_field_cancel_axioms' = normalizing_field_cancel_axioms [normalizer - semiring ops: semiring_ops - semiring rules: semiring_rules - ring ops: ring_ops - ring rules: ring_rules - field ops: field_ops - field rules: field_rules - idom rules: noteq_reduce add_scale_eq_noteq - ideal rules: subr0_iff add_r0_iff] - -end - -sublocale field - < normalizing!: normalizing_field_cancel plus times power zero one minus uminus divide inverse -proof -qed (simp_all add: divide_inverse) - -declaration {* Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *} - - subsection {* Groebner Bases *} lemmas bool_simps = simp_thms(1-34) @@ -367,6 +40,11 @@ setup Algebra_Simplification.setup +use "Tools/groebner.ML" + +method_setup algebra = Groebner.algebra_method + "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" + declare dvd_def[algebra] declare dvd_eq_mod_eq_0[symmetric, algebra] declare mod_div_trivial[algebra] @@ -395,9 +73,4 @@ declare zmod_eq_dvd_iff[algebra] declare nat_mod_eq_iff[algebra] -use "Tools/Groebner_Basis/groebner.ML" - -method_setup algebra = Groebner.algebra_method - "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" - end diff -r dce592144219 -r 5ce217fc769a src/HOL/Int.thy --- a/src/HOL/Int.thy Fri May 07 23:44:10 2010 +0200 +++ b/src/HOL/Int.thy Sat May 08 17:15:50 2010 +0200 @@ -2173,6 +2173,25 @@ apply (auto simp add: dvd_imp_le) done +lemma zdvd_period: + fixes a d :: int + assumes "a dvd d" + shows "a dvd (x + t) \ a dvd ((x + c * d) + t)" +proof - + from assms obtain k where "d = a * k" by (rule dvdE) + show ?thesis proof + assume "a dvd (x + t)" + then obtain l where "x + t = a * l" by (rule dvdE) + then have "x = a * l - t" by simp + with `d = a * k` show "a dvd x + c * d + t" by simp + next + assume "a dvd x + c * d + t" + then obtain l where "x + c * d + t = a * l" by (rule dvdE) + then have "x = a * l - c * d - t" by simp + with `d = a * k` show "a dvd (x + t)" by simp + qed +qed + subsection {* Configuration of the code generator *} diff -r dce592144219 -r 5ce217fc769a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri May 07 23:44:10 2010 +0200 +++ b/src/HOL/IsaMakefile Sat May 08 17:15:50 2010 +0200 @@ -271,6 +271,7 @@ Random.thy \ Random_Sequence.thy \ Recdef.thy \ + Semiring_Normalization.thy \ SetInterval.thy \ Sledgehammer.thy \ String.thy \ @@ -283,10 +284,9 @@ $(SRC)/Tools/Metis/metis.ML \ Tools/ATP_Manager/atp_manager.ML \ Tools/ATP_Manager/atp_systems.ML \ - Tools/Groebner_Basis/groebner.ML \ - Tools/Groebner_Basis/normalizer.ML \ Tools/choice_specification.ML \ Tools/int_arith.ML \ + Tools/groebner.ML \ Tools/list_code.ML \ Tools/meson.ML \ Tools/nat_numeral_simprocs.ML \ @@ -313,6 +313,7 @@ Tools/Quotient/quotient_term.ML \ Tools/Quotient/quotient_typ.ML \ Tools/recdef.ML \ + Tools/semiring_normalizer.ML \ Tools/Sledgehammer/meson_tactic.ML \ Tools/Sledgehammer/metis_tactics.ML \ Tools/Sledgehammer/sledgehammer_fact_filter.ML \ diff -r dce592144219 -r 5ce217fc769a src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri May 07 23:44:10 2010 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat May 08 17:15:50 2010 +0200 @@ -1194,8 +1194,8 @@ (* FIXME: Replace tryfind by get_first !! *) fun real_nonlinear_prover proof_method ctxt = let - val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt - (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) + val {add,mul,neg,pow,sub,main} = Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt + (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv, real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main) @@ -1222,7 +1222,7 @@ in (let val th = tryfind trivial_axiom (keq @ klep @ kltp) in - (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv Normalizer.field_comp_conv) th, RealArith.Trivial) + (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv Numeral_Simprocs.field_comp_conv) th, RealArith.Trivial) end) handle Failure _ => (let val proof = @@ -1309,8 +1309,8 @@ fun real_nonlinear_subst_prover prover ctxt = let - val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt - (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) + val {add,mul,neg,pow,sub,main} = Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt + (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv, diff -r dce592144219 -r 5ce217fc769a src/HOL/Library/normarith.ML --- a/src/HOL/Library/normarith.ML Fri May 07 23:44:10 2010 +0200 +++ b/src/HOL/Library/normarith.ML Sat May 08 17:15:50 2010 +0200 @@ -166,9 +166,9 @@ let (* FIXME : Should be computed statically!! *) val real_poly_conv = - Normalizer.semiring_normalize_wrapper ctxt - (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) - in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Normalizer.field_comp_conv then_conv real_poly_conv))) + Semiring_Normalizer.semiring_normalize_wrapper ctxt + (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) + in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Numeral_Simprocs.field_comp_conv then_conv real_poly_conv))) end; fun absc cv ct = case term_of ct of @@ -190,8 +190,8 @@ val apply_pth5 = rewr_conv @{thm pth_5}; val apply_pth6 = rewr_conv @{thm pth_6}; val apply_pth7 = rewrs_conv @{thms pth_7}; - val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv Normalizer.field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left}))); - val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv Normalizer.field_comp_conv); + val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv Numeral_Simprocs.field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left}))); + val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv Numeral_Simprocs.field_comp_conv); val apply_ptha = rewr_conv @{thm pth_a}; val apply_pthb = rewrs_conv @{thms pth_b}; val apply_pthc = rewrs_conv @{thms pth_c}; @@ -204,7 +204,7 @@ | _ => error "headvector: non-canonical term" fun vector_cmul_conv ct = - ((apply_pth5 then_conv arg1_conv Normalizer.field_comp_conv) else_conv + ((apply_pth5 then_conv arg1_conv Numeral_Simprocs.field_comp_conv) else_conv (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct fun vector_add_conv ct = apply_pth7 ct @@ -277,8 +277,8 @@ let (* FIXME: Should be computed statically!!*) val real_poly_conv = - Normalizer.semiring_normalize_wrapper ctxt - (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) + Semiring_Normalizer.semiring_normalize_wrapper ctxt + (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" @@ -383,8 +383,8 @@ fun splitequation ctxt th acc = let val real_poly_neg_conv = #neg - (Normalizer.semiring_normalizers_ord_wrapper ctxt - (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord) + (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt + (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord) val (th1,th2) = conj_pair(rawrule th) in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc end @@ -396,7 +396,7 @@ fun init_conv ctxt = Simplifier.rewrite (Simplifier.context ctxt (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) - then_conv Normalizer.field_comp_conv + then_conv Numeral_Simprocs.field_comp_conv then_conv nnf_conv fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); diff -r dce592144219 -r 5ce217fc769a src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Fri May 07 23:44:10 2010 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Sat May 08 17:15:50 2010 +0200 @@ -747,11 +747,11 @@ let fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS val {add,mul,neg,pow,sub,main} = - Normalizer.semiring_normalizers_ord_wrapper ctxt - (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) + Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt + (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord in gen_real_arith ctxt - (cterm_of_rat, Normalizer.field_comp_conv, Normalizer.field_comp_conv, Normalizer.field_comp_conv, + (cterm_of_rat, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv, main,neg,add,mul, prover) end; diff -r dce592144219 -r 5ce217fc769a src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Fri May 07 23:44:10 2010 +0200 +++ b/src/HOL/Presburger.thy Sat May 08 17:15:50 2010 +0200 @@ -457,14 +457,4 @@ lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \ \ 2 dvd m " by presburger lemma [presburger, algebra]: "m mod 2 = (1::int) \ \ 2 dvd m " by presburger - -lemma zdvd_period: - fixes a d :: int - assumes advdd: "a dvd d" - shows "a dvd (x + t) \ a dvd ((x + c * d) + t)" - using advdd - apply - - apply (rule iffI) - by algebra+ - end diff -r dce592144219 -r 5ce217fc769a src/HOL/Semiring_Normalization.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Semiring_Normalization.thy Sat May 08 17:15:50 2010 +0200 @@ -0,0 +1,336 @@ +(* Title: HOL/Semiring_Normalization.thy + Author: Amine Chaieb, TU Muenchen +*) + +header {* Semiring normalization *} + +theory Semiring_Normalization +imports Numeral_Simprocs Nat_Transfer +uses + "Tools/semiring_normalizer.ML" +begin + +setup Semiring_Normalizer.setup + +locale normalizing_semiring = + fixes add mul pwr r0 r1 + assumes add_a:"(add x (add y z) = add (add x y) z)" + and add_c: "add x y = add y x" and add_0:"add r0 x = x" + and mul_a:"mul x (mul y z) = mul (mul x y) z" and mul_c:"mul x y = mul y x" + and mul_1:"mul r1 x = x" and mul_0:"mul r0 x = r0" + and mul_d:"mul x (add y z) = add (mul x y) (mul x z)" + and pwr_0:"pwr x 0 = r1" and pwr_Suc:"pwr x (Suc n) = mul x (pwr x n)" +begin + +lemma mul_pwr:"mul (pwr x p) (pwr x q) = pwr x (p + q)" +proof (induct p) + case 0 + then show ?case by (auto simp add: pwr_0 mul_1) +next + case Suc + from this [symmetric] show ?case + by (auto simp add: pwr_Suc mul_1 mul_a) +qed + +lemma pwr_mul: "pwr (mul x y) q = mul (pwr x q) (pwr y q)" +proof (induct q arbitrary: x y, auto simp add:pwr_0 pwr_Suc mul_1) + fix q x y + assume "\x y. pwr (mul x y) q = mul (pwr x q) (pwr y q)" + have "mul (mul x y) (mul (pwr x q) (pwr y q)) = mul x (mul y (mul (pwr x q) (pwr y q)))" + by (simp add: mul_a) + also have "\ = (mul (mul y (mul (pwr y q) (pwr x q))) x)" by (simp add: mul_c) + also have "\ = (mul (mul y (pwr y q)) (mul (pwr x q) x))" by (simp add: mul_a) + finally show "mul (mul x y) (mul (pwr x q) (pwr y q)) = + mul (mul x (pwr x q)) (mul y (pwr y q))" by (simp add: mul_c) +qed + +lemma pwr_pwr: "pwr (pwr x p) q = pwr x (p * q)" +proof (induct p arbitrary: q) + case 0 + show ?case using pwr_Suc mul_1 pwr_0 by (induct q) auto +next + case Suc + thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc) +qed + +lemma semiring_ops: + shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)" + and "TERM r0" and "TERM r1" . + +lemma semiring_rules: + "add (mul a m) (mul b m) = mul (add a b) m" + "add (mul a m) m = mul (add a r1) m" + "add m (mul a m) = mul (add a r1) m" + "add m m = mul (add r1 r1) m" + "add r0 a = a" + "add a r0 = a" + "mul a b = mul b a" + "mul (add a b) c = add (mul a c) (mul b c)" + "mul r0 a = r0" + "mul a r0 = r0" + "mul r1 a = a" + "mul a r1 = a" + "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)" + "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))" + "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)" + "mul (mul lx ly) rx = mul (mul lx rx) ly" + "mul (mul lx ly) rx = mul lx (mul ly rx)" + "mul lx (mul rx ry) = mul (mul lx rx) ry" + "mul lx (mul rx ry) = mul rx (mul lx ry)" + "add (add a b) (add c d) = add (add a c) (add b d)" + "add (add a b) c = add a (add b c)" + "add a (add c d) = add c (add a d)" + "add (add a b) c = add (add a c) b" + "add a c = add c a" + "add a (add c d) = add (add a c) d" + "mul (pwr x p) (pwr x q) = pwr x (p + q)" + "mul x (pwr x q) = pwr x (Suc q)" + "mul (pwr x q) x = pwr x (Suc q)" + "mul x x = pwr x 2" + "pwr (mul x y) q = mul (pwr x q) (pwr y q)" + "pwr (pwr x p) q = pwr x (p * q)" + "pwr x 0 = r1" + "pwr x 1 = x" + "mul x (add y z) = add (mul x y) (mul x z)" + "pwr x (Suc q) = mul x (pwr x q)" + "pwr x (2*n) = mul (pwr x n) (pwr x n)" + "pwr x (Suc (2*n)) = mul x (mul (pwr x n) (pwr x n))" +proof - + show "add (mul a m) (mul b m) = mul (add a b) m" using mul_d mul_c by simp +next show"add (mul a m) m = mul (add a r1) m" using mul_d mul_c mul_1 by simp +next show "add m (mul a m) = mul (add a r1) m" using mul_c mul_d mul_1 add_c by simp +next show "add m m = mul (add r1 r1) m" using mul_c mul_d mul_1 by simp +next show "add r0 a = a" using add_0 by simp +next show "add a r0 = a" using add_0 add_c by simp +next show "mul a b = mul b a" using mul_c by simp +next show "mul (add a b) c = add (mul a c) (mul b c)" using mul_c mul_d by simp +next show "mul r0 a = r0" using mul_0 by simp +next show "mul a r0 = r0" using mul_0 mul_c by simp +next show "mul r1 a = a" using mul_1 by simp +next show "mul a r1 = a" using mul_1 mul_c by simp +next show "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)" + using mul_c mul_a by simp +next show "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))" + using mul_a by simp +next + have "mul (mul lx ly) (mul rx ry) = mul (mul rx ry) (mul lx ly)" by (rule mul_c) + also have "\ = mul rx (mul ry (mul lx ly))" using mul_a by simp + finally + show "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)" + using mul_c by simp +next show "mul (mul lx ly) rx = mul (mul lx rx) ly" using mul_c mul_a by simp +next + show "mul (mul lx ly) rx = mul lx (mul ly rx)" by (simp add: mul_a) +next show "mul lx (mul rx ry) = mul (mul lx rx) ry" by (simp add: mul_a ) +next show "mul lx (mul rx ry) = mul rx (mul lx ry)" by (simp add: mul_a,simp add: mul_c) +next show "add (add a b) (add c d) = add (add a c) (add b d)" + using add_c add_a by simp +next show "add (add a b) c = add a (add b c)" using add_a by simp +next show "add a (add c d) = add c (add a d)" + apply (simp add: add_a) by (simp only: add_c) +next show "add (add a b) c = add (add a c) b" using add_a add_c by simp +next show "add a c = add c a" by (rule add_c) +next show "add a (add c d) = add (add a c) d" using add_a by simp +next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr) +next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp +next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp +next show "mul x x = pwr x 2" by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c) +next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul) +next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr) +next show "pwr x 0 = r1" using pwr_0 . +next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c) +next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp +next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp +next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number' mul_pwr) +next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))" + by (simp add: nat_number' pwr_Suc mul_pwr) +qed + + +lemmas normalizing_semiring_axioms' = + normalizing_semiring_axioms [normalizer + semiring ops: semiring_ops + semiring rules: semiring_rules] + +end + +sublocale comm_semiring_1 + < normalizing!: normalizing_semiring plus times power zero one +proof +qed (simp_all add: algebra_simps) + +declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *} + +locale normalizing_ring = normalizing_semiring + + fixes sub :: "'a \ 'a \ 'a" + and neg :: "'a \ 'a" + assumes neg_mul: "neg x = mul (neg r1) x" + and sub_add: "sub x y = add x (neg y)" +begin + +lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" . + +lemmas ring_rules = neg_mul sub_add + +lemmas normalizing_ring_axioms' = + normalizing_ring_axioms [normalizer + semiring ops: semiring_ops + semiring rules: semiring_rules + ring ops: ring_ops + ring rules: ring_rules] + +end + +sublocale comm_ring_1 + < normalizing!: normalizing_ring plus times power zero one minus uminus +proof +qed (simp_all add: diff_minus) + +declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *} + +locale normalizing_field = normalizing_ring + + fixes divide :: "'a \ 'a \ 'a" + and inverse:: "'a \ 'a" + assumes divide_inverse: "divide x y = mul x (inverse y)" + and inverse_divide: "inverse x = divide r1 x" +begin + +lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" . + +lemmas field_rules = divide_inverse inverse_divide + +lemmas normalizing_field_axioms' = + normalizing_field_axioms [normalizer + semiring ops: semiring_ops + semiring rules: semiring_rules + ring ops: ring_ops + ring rules: ring_rules + field ops: field_ops + field rules: field_rules] + +end + +locale normalizing_semiring_cancel = normalizing_semiring + + assumes add_cancel: "add (x::'a) y = add x z \ y = z" + and add_mul_solve: "add (mul w y) (mul x z) = + add (mul w z) (mul x y) \ w = x \ y = z" +begin + +lemma noteq_reduce: "a \ b \ c \ d \ add (mul a c) (mul b d) \ add (mul a d) (mul b c)" +proof- + have "a \ b \ c \ d \ \ (a = b \ c = d)" by simp + also have "\ \ add (mul a c) (mul b d) \ add (mul a d) (mul b c)" + using add_mul_solve by blast + finally show "a \ b \ c \ d \ add (mul a c) (mul b d) \ add (mul a d) (mul b c)" + by simp +qed + +lemma add_scale_eq_noteq: "\r \ r0 ; (a = b) \ ~(c = d)\ + \ add a (mul r c) \ add b (mul r d)" +proof(clarify) + assume nz: "r\ r0" and cnd: "c\d" + and eq: "add b (mul r c) = add b (mul r d)" + hence "mul r c = mul r d" using cnd add_cancel by simp + hence "add (mul r0 d) (mul r c) = add (mul r0 c) (mul r d)" + using mul_0 add_cancel by simp + thus "False" using add_mul_solve nz cnd by simp +qed + +lemma add_r0_iff: " x = add x a \ a = r0" +proof- + have "a = r0 \ add x a = add x r0" by (simp add: add_cancel) + thus "x = add x a \ a = r0" by (auto simp add: add_c add_0) +qed + +declare normalizing_semiring_axioms' [normalizer del] + +lemmas normalizing_semiring_cancel_axioms' = + normalizing_semiring_cancel_axioms [normalizer + semiring ops: semiring_ops + semiring rules: semiring_rules + idom rules: noteq_reduce add_scale_eq_noteq] + +end + +locale normalizing_ring_cancel = normalizing_semiring_cancel + normalizing_ring + + assumes subr0_iff: "sub x y = r0 \ x = y" +begin + +declare normalizing_ring_axioms' [normalizer del] + +lemmas normalizing_ring_cancel_axioms' = normalizing_ring_cancel_axioms [normalizer + semiring ops: semiring_ops + semiring rules: semiring_rules + ring ops: ring_ops + ring rules: ring_rules + idom rules: noteq_reduce add_scale_eq_noteq + ideal rules: subr0_iff add_r0_iff] + +end + +sublocale idom + < normalizing!: normalizing_ring_cancel plus times power zero one minus uminus +proof + fix w x y z + show "w * y + x * z = w * z + x * y \ w = x \ y = z" + proof + assume "w * y + x * z = w * z + x * y" + then have "w * y + x * z - w * z - x * y = 0" by (simp add: algebra_simps) + then have "w * (y - z) - x * (y - z) = 0" by (simp add: algebra_simps) + then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps) + then have "y - z = 0 \ w - x = 0" by (rule divisors_zero) + then show "w = x \ y = z" by auto + qed (auto simp add: add_ac) +qed (simp_all add: algebra_simps) + +declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *} + +interpretation normalizing_nat!: normalizing_semiring_cancel + "op +" "op *" "op ^" "0::nat" "1" +proof (unfold_locales, simp add: algebra_simps) + fix w x y z ::"nat" + { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \ z" + hence "y < z \ y > z" by arith + moreover { + assume lt:"y k. z = y + k \ k > 0" by (rule_tac x="z - y" in exI, auto) + then obtain k where kp: "k>0" and yz:"z = y + k" by blast + from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps) + hence "x*k = w*k" by simp + hence "w = x" using kp by simp } + moreover { + assume lt: "y >z" hence "\k. y = z + k \ k>0" by (rule_tac x="y - z" in exI, auto) + then obtain k where kp: "k>0" and yz:"y = z + k" by blast + from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps) + hence "w*k = x*k" by simp + hence "w = x" using kp by simp } + ultimately have "w=x" by blast } + thus "(w * y + x * z = w * z + x * y) = (w = x \ y = z)" by auto +qed + +declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *} + +locale normalizing_field_cancel = normalizing_ring_cancel + normalizing_field +begin + +declare normalizing_field_axioms' [normalizer del] + +lemmas normalizing_field_cancel_axioms' = normalizing_field_cancel_axioms [normalizer + semiring ops: semiring_ops + semiring rules: semiring_rules + ring ops: ring_ops + ring rules: ring_rules + field ops: field_ops + field rules: field_rules + idom rules: noteq_reduce add_scale_eq_noteq + ideal rules: subr0_iff add_r0_iff] + +end + +sublocale field + < normalizing!: normalizing_field_cancel plus times power zero one minus uminus divide inverse +proof +qed (simp_all add: divide_inverse) + +declaration {* Semiring_Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *} + +end diff -r dce592144219 -r 5ce217fc769a src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Fri May 07 23:44:10 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1045 +0,0 @@ -(* Title: HOL/Tools/Groebner_Basis/groebner.ML - Author: Amine Chaieb, TU Muenchen -*) - -signature GROEBNER = -sig - val ring_and_ideal_conv : - {idom: thm list, ring: cterm list * thm list, field: cterm list * thm list, - vars: cterm list, semiring: cterm list * thm list, ideal : thm list} -> - (cterm -> Rat.rat) -> (Rat.rat -> cterm) -> - conv -> conv -> - {ring_conv : conv, - simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list), - multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list, - poly_eq_ss: simpset, unwind_conv : conv} - val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic - val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic - val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic - val algebra_method: (Proof.context -> Method.method) context_parser -end - -structure Groebner : GROEBNER = -struct - -open Conv Drule Thm; - -fun is_comb ct = - (case Thm.term_of ct of - _ $ _ => true - | _ => false); - -val concl = Thm.cprop_of #> Thm.dest_arg; - -fun is_binop ct ct' = - (case Thm.term_of ct' of - c $ _ $ _ => term_of ct aconv c - | _ => false); - -fun dest_binary ct ct' = - if is_binop ct ct' then Thm.dest_binop ct' - else raise CTERM ("dest_binary: bad binop", [ct, ct']) - -fun inst_thm inst = Thm.instantiate ([], inst); - -val rat_0 = Rat.zero; -val rat_1 = Rat.one; -val minus_rat = Rat.neg; -val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int; -fun int_of_rat a = - case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int"; -val lcm_rat = fn x => fn y => Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y)); - -val (eqF_intr, eqF_elim) = - let val [th1,th2] = @{thms PFalse} - in (fn th => th COMP th2, fn th => th COMP th1) end; - -val (PFalse, PFalse') = - let val PFalse_eq = nth @{thms simp_thms} 13 - in (PFalse_eq RS iffD1, PFalse_eq RS iffD2) end; - - -(* Type for recording history, i.e. how a polynomial was obtained. *) - -datatype history = - Start of int - | Mmul of (Rat.rat * int list) * history - | Add of history * history; - - -(* Monomial ordering. *) - -fun morder_lt m1 m2= - let fun lexorder l1 l2 = - case (l1,l2) of - ([],[]) => false - | (x1::o1,x2::o2) => x1 > x2 orelse x1 = x2 andalso lexorder o1 o2 - | _ => error "morder: inconsistent monomial lengths" - val n1 = Integer.sum m1 - val n2 = Integer.sum m2 in - n1 < n2 orelse n1 = n2 andalso lexorder m1 m2 - end; - -fun morder_le m1 m2 = morder_lt m1 m2 orelse (m1 = m2); - -fun morder_gt m1 m2 = morder_lt m2 m1; - -(* Arithmetic on canonical polynomials. *) - -fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l; - -fun grob_add l1 l2 = - case (l1,l2) of - ([],l2) => l2 - | (l1,[]) => l1 - | ((c1,m1)::o1,(c2,m2)::o2) => - if m1 = m2 then - let val c = c1+/c2 val rest = grob_add o1 o2 in - if c =/ rat_0 then rest else (c,m1)::rest end - else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2) - else (c2,m2)::(grob_add l1 o2); - -fun grob_sub l1 l2 = grob_add l1 (grob_neg l2); - -fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2, ListPair.map (op +) (m1, m2)); - -fun grob_cmul cm pol = map (grob_mmul cm) pol; - -fun grob_mul l1 l2 = - case l1 of - [] => [] - | (h1::t1) => grob_add (grob_cmul h1 l2) (grob_mul t1 l2); - -fun grob_inv l = - case l of - [(c,vs)] => if (forall (fn x => x = 0) vs) then - if (c =/ rat_0) then error "grob_inv: division by zero" - else [(rat_1 // c,vs)] - else error "grob_inv: non-constant divisor polynomial" - | _ => error "grob_inv: non-constant divisor polynomial"; - -fun grob_div l1 l2 = - case l2 of - [(c,l)] => if (forall (fn x => x = 0) l) then - if c =/ rat_0 then error "grob_div: division by zero" - else grob_cmul (rat_1 // c,l) l1 - else error "grob_div: non-constant divisor polynomial" - | _ => error "grob_div: non-constant divisor polynomial"; - -fun grob_pow vars l n = - if n < 0 then error "grob_pow: negative power" - else if n = 0 then [(rat_1,map (fn v => 0) vars)] - else grob_mul l (grob_pow vars l (n - 1)); - -fun degree vn p = - case p of - [] => error "Zero polynomial" -| [(c,ns)] => nth ns vn -| (c,ns)::p' => Int.max (nth ns vn, degree vn p'); - -fun head_deg vn p = let val d = degree vn p in - (d,fold (fn (c,r) => fn q => grob_add q [(c, map_index (fn (i,n) => if i = vn then 0 else n) r)]) (filter (fn (c,ns) => c <>/ rat_0 andalso nth ns vn = d) p) []) end; - -val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) 0) ns); -val grob_pdiv = - let fun pdiv_aux vn (n,a) p k s = - if is_zerop s then (k,s) else - let val (m,b) = head_deg vn s - in if m < n then (k,s) else - let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m - n else 0) - (snd (hd s)))] - in if a = b then pdiv_aux vn (n,a) p k (grob_sub s p') - else pdiv_aux vn (n,a) p (k + 1) (grob_sub (grob_mul a s) (grob_mul b p')) - end - end - in fn vn => fn s => fn p => pdiv_aux vn (head_deg vn p) p 0 s - end; - -(* Monomial division operation. *) - -fun mdiv (c1,m1) (c2,m2) = - (c1//c2, - map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 - n2) m1 m2); - -(* Lowest common multiple of two monomials. *) - -fun mlcm (c1,m1) (c2,m2) = (rat_1, ListPair.map Int.max (m1, m2)); - -(* Reduce monomial cm by polynomial pol, returning replacement for cm. *) - -fun reduce1 cm (pol,hpol) = - case pol of - [] => error "reduce1" - | cm1::cms => ((let val (c,m) = mdiv cm cm1 in - (grob_cmul (minus_rat c,m) cms, - Mmul((minus_rat c,m),hpol)) end) - handle ERROR _ => error "reduce1"); - -(* Try this for all polynomials in a basis. *) -fun tryfind f l = - case l of - [] => error "tryfind" - | (h::t) => ((f h) handle ERROR _ => tryfind f t); - -fun reduceb cm basis = tryfind (fn p => reduce1 cm p) basis; - -(* Reduction of a polynomial (always picking largest monomial possible). *) - -fun reduce basis (pol,hist) = - case pol of - [] => (pol,hist) - | cm::ptl => ((let val (q,hnew) = reduceb cm basis in - reduce basis (grob_add q ptl,Add(hnew,hist)) end) - handle (ERROR _) => - (let val (q,hist') = reduce basis (ptl,hist) in - (cm::q,hist') end)); - -(* Check for orthogonality w.r.t. LCM. *) - -fun orthogonal l p1 p2 = - snd l = snd(grob_mmul (hd p1) (hd p2)); - -(* Compute S-polynomial of two polynomials. *) - -fun spoly cm ph1 ph2 = - case (ph1,ph2) of - (([],h),p) => ([],h) - | (p,([],h)) => ([],h) - | ((cm1::ptl1,his1),(cm2::ptl2,his2)) => - (grob_sub (grob_cmul (mdiv cm cm1) ptl1) - (grob_cmul (mdiv cm cm2) ptl2), - Add(Mmul(mdiv cm cm1,his1), - Mmul(mdiv (minus_rat(fst cm),snd cm) cm2,his2))); - -(* Make a polynomial monic. *) - -fun monic (pol,hist) = - if null pol then (pol,hist) else - let val (c',m') = hd pol in - (map (fn (c,m) => (c//c',m)) pol, - Mmul((rat_1 // c',map (K 0) m'),hist)) end; - -(* The most popular heuristic is to order critical pairs by LCM monomial. *) - -fun forder ((c1,m1),_) ((c2,m2),_) = morder_lt m1 m2; - -fun poly_lt p q = - case (p,q) of - (p,[]) => false - | ([],q) => true - | ((c1,m1)::o1,(c2,m2)::o2) => - c1 true - | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2 - | _ => false; - -fun poly_eq p1 p2 = - forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2; - -fun memx ((p1,h1),(p2,h2)) ppairs = - not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs); - -(* Buchberger's second criterion. *) - -fun criterion2 basis (lcm,((p1,h1),(p2,h2))) opairs = - exists (fn g => not(poly_eq (fst g) p1) andalso not(poly_eq (fst g) p2) andalso - can (mdiv lcm) (hd(fst g)) andalso - not(memx (align (g,(p1,h1))) (map snd opairs)) andalso - not(memx (align (g,(p2,h2))) (map snd opairs))) basis; - -(* Test for hitting constant polynomial. *) - -fun constant_poly p = - length p = 1 andalso forall (fn x => x = 0) (snd(hd p)); - -(* Grobner basis algorithm. *) - -(* FIXME: try to get rid of mergesort? *) -fun merge ord l1 l2 = - case l1 of - [] => l2 - | h1::t1 => - case l2 of - [] => l1 - | h2::t2 => if ord h1 h2 then h1::(merge ord t1 l2) - else h2::(merge ord l1 t2); -fun mergesort ord l = - let - fun mergepairs l1 l2 = - case (l1,l2) of - ([s],[]) => s - | (l,[]) => mergepairs [] l - | (l,[s1]) => mergepairs (s1::l) [] - | (l,(s1::s2::ss)) => mergepairs ((merge ord s1 s2)::l) ss - in if null l then [] else mergepairs [] (map (fn x => [x]) l) - end; - - -fun grobner_basis basis pairs = - case pairs of - [] => basis - | (l,(p1,p2))::opairs => - let val (sph as (sp,hist)) = monic (reduce basis (spoly l p1 p2)) - in - if null sp orelse criterion2 basis (l,(p1,p2)) opairs - then grobner_basis basis opairs - else if constant_poly sp then grobner_basis (sph::basis) [] - else - let - val rawcps = map (fn p => (mlcm (hd(fst p)) (hd sp),align(p,sph))) - basis - val newcps = filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q))) - rawcps - in grobner_basis (sph::basis) - (merge forder opairs (mergesort forder newcps)) - end - end; - -(* Interreduce initial polynomials. *) - -fun grobner_interreduce rpols ipols = - case ipols of - [] => map monic (rev rpols) - | p::ps => let val p' = reduce (rpols @ ps) p in - if null (fst p') then grobner_interreduce rpols ps - else grobner_interreduce (p'::rpols) ps end; - -(* Overall function. *) - -fun grobner pols = - let val npols = map_index (fn (n, p) => (p, Start n)) pols - val phists = filter (fn (p,_) => not (null p)) npols - val bas = grobner_interreduce [] (map monic phists) - val prs0 = map_product pair bas bas - val prs1 = filter (fn ((x,_),(y,_)) => poly_lt x y) prs0 - val prs2 = map (fn (p,q) => (mlcm (hd(fst p)) (hd(fst q)),(p,q))) prs1 - val prs3 = - filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q))) prs2 in - grobner_basis bas (mergesort forder prs3) end; - -(* Get proof of contradiction from Grobner basis. *) - -fun find p l = - case l of - [] => error "find" - | (h::t) => if p(h) then h else find p t; - -fun grobner_refute pols = - let val gb = grobner pols in - snd(find (fn (p,h) => length p = 1 andalso forall (fn x=> x=0) (snd(hd p))) gb) - end; - -(* Turn proof into a certificate as sum of multipliers. *) -(* In principle this is very inefficient: in a heavily shared proof it may *) -(* make the same calculation many times. Could put in a cache or something. *) - -fun resolve_proof vars prf = - case prf of - Start(~1) => [] - | Start m => [(m,[(rat_1,map (K 0) vars)])] - | Mmul(pol,lin) => - let val lis = resolve_proof vars lin in - map (fn (n,p) => (n,grob_cmul pol p)) lis end - | Add(lin1,lin2) => - let val lis1 = resolve_proof vars lin1 - val lis2 = resolve_proof vars lin2 - val dom = distinct (op =) (union (op =) (map fst lis1) (map fst lis2)) - in - map (fn n => let val a = these (AList.lookup (op =) lis1 n) - val b = these (AList.lookup (op =) lis2 n) - in (n,grob_add a b) end) dom end; - -(* Run the procedure and produce Weak Nullstellensatz certificate. *) - -fun grobner_weak vars pols = - let val cert = resolve_proof vars (grobner_refute pols) - val l = - fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in - (l,map (fn (i,p) => (i,map (fn (d,m) => (l*/d,m)) p)) cert) end; - -(* Prove a polynomial is in ideal generated by others, using Grobner basis. *) - -fun grobner_ideal vars pols pol = - let val (pol',h) = reduce (grobner pols) (grob_neg pol,Start(~1)) in - if not (null pol') then error "grobner_ideal: not in the ideal" else - resolve_proof vars h end; - -(* Produce Strong Nullstellensatz certificate for a power of pol. *) - -fun grobner_strong vars pols pol = - let val vars' = @{cterm "True"}::vars - val grob_z = [(rat_1,1::(map (fn x => 0) vars))] - val grob_1 = [(rat_1,(map (fn x => 0) vars'))] - fun augment p= map (fn (c,m) => (c,0::m)) p - val pols' = map augment pols - val pol' = augment pol - val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols' - val (l,cert) = grobner_weak vars' allpols - val d = fold (fold (Integer.max o hd o snd) o snd) cert 0 - fun transform_monomial (c,m) = - grob_cmul (c,tl m) (grob_pow vars pol (d - hd m)) - fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q [] - val cert' = map (fn (c,q) => (c-1,transform_polynomial q)) - (filter (fn (k,_) => k <> 0) cert) in - (d,l,cert') end; - - -(* Overall parametrized universal procedure for (semi)rings. *) -(* We return an ideal_conv and the actual ring prover. *) - -fun refute_disj rfn tm = - case term_of tm of - Const("op |",_)$l$r => - compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE)) - | _ => rfn tm ; - -val notnotD = @{thm notnotD}; -fun mk_binop ct x y = capply (capply ct x) y - -val mk_comb = capply; -fun is_neg t = - case term_of t of - (Const("Not",_)$p) => true - | _ => false; -fun is_eq t = - case term_of t of - (Const("op =",_)$_$_) => true -| _ => false; - -fun end_itlist f l = - case l of - [] => error "end_itlist" - | [x] => x - | (h::t) => f h (end_itlist f t); - -val list_mk_binop = fn b => end_itlist (mk_binop b); - -val list_dest_binop = fn b => - let fun h acc t = - ((let val (l,r) = dest_binary b t in h (h acc r) l end) - handle CTERM _ => (t::acc)) (* Why had I handle _ => ? *) - in h [] - end; - -val strip_exists = - let fun h (acc, t) = - case (term_of t) of - Const("Ex",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc)) - | _ => (acc,t) - in fn t => h ([],t) - end; - -fun is_forall t = - case term_of t of - (Const("All",_)$Abs(_,_,_)) => true -| _ => false; - -val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq; -val bool_simps = @{thms bool_simps}; -val nnf_simps = @{thms nnf_simps}; -val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps bool_simps addsimps nnf_simps) -val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms weak_dnf_simps}); -val initial_conv = - Simplifier.rewrite - (HOL_basic_ss addsimps nnf_simps - addsimps [not_all, not_ex] - addsimps map (fn th => th RS sym) (@{thms ex_simps} @ @{thms all_simps})); - -val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec)); - -val cTrp = @{cterm "Trueprop"}; -val cConj = @{cterm "op &"}; -val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"}); -val assume_Trueprop = mk_comb cTrp #> assume; -val list_mk_conj = list_mk_binop cConj; -val conjs = list_dest_binop cConj; -val mk_neg = mk_comb cNot; - -fun striplist dest = - let - fun h acc x = case try dest x of - SOME (a,b) => h (h acc b) a - | NONE => x::acc - in h [] end; -fun list_mk_binop b = foldr1 (fn (s,t) => Thm.capply (Thm.capply b s) t); - -val eq_commute = mk_meta_eq @{thm eq_commute}; - -fun sym_conv eq = - let val (l,r) = Thm.dest_binop eq - in instantiate' [SOME (ctyp_of_term l)] [SOME l, SOME r] eq_commute - end; - - (* FIXME : copied from cqe.ML -- complex QE*) -fun conjuncts ct = - case term_of ct of - @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct)) -| _ => [ct]; - -fun fold1 f = foldr1 (uncurry f); - -val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ; - -fun mk_conj_tab th = - let fun h acc th = - case prop_of th of - @{term "Trueprop"}$(@{term "op &"}$p$q) => - h (h acc (th RS conjunct2)) (th RS conjunct1) - | @{term "Trueprop"}$p => (p,th)::acc -in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end; - -fun is_conj (@{term "op &"}$_$_) = true - | is_conj _ = false; - -fun prove_conj tab cjs = - case cjs of - [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c - | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs]; - -fun conj_ac_rule eq = - let - val (l,r) = Thm.dest_equals eq - val ctabl = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} l)) - val ctabr = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} r)) - fun tabl c = the (Termtab.lookup ctabl (term_of c)) - fun tabr c = the (Termtab.lookup ctabr (term_of c)) - val thl = prove_conj tabl (conjuncts r) |> implies_intr_hyps - val thr = prove_conj tabr (conjuncts l) |> implies_intr_hyps - val eqI = instantiate' [] [SOME l, SOME r] @{thm iffI} - in implies_elim (implies_elim eqI thl) thr |> mk_meta_eq end; - - (* END FIXME.*) - - (* Conversion for the equivalence of existential statements where - EX quantifiers are rearranged differently *) - fun ext T = cterm_rule (instantiate' [SOME T] []) @{cpat Ex} - fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t) - -fun choose v th th' = case concl_of th of - @{term Trueprop} $ (Const("Ex",_)$_) => - let - val p = (funpow 2 Thm.dest_arg o cprop_of) th - val T = (hd o Thm.dest_ctyp o ctyp_of_term) p - val th0 = fconv_rule (Thm.beta_conversion true) - (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE) - val pv = (Thm.rhs_of o Thm.beta_conversion true) - (Thm.capply @{cterm Trueprop} (Thm.capply p v)) - val th1 = forall_intr v (implies_intr pv th') - in implies_elim (implies_elim th0 th) th1 end -| _ => error "" - -fun simple_choose v th = - choose v (assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th - - - fun mkexi v th = - let - val p = Thm.cabs v (Thm.dest_arg (Thm.cprop_of th)) - in implies_elim - (fconv_rule (Thm.beta_conversion true) (instantiate' [SOME (ctyp_of_term v)] [SOME p, SOME v] @{thm exI})) - th - end - fun ex_eq_conv t = - let - val (p0,q0) = Thm.dest_binop t - val (vs',P) = strip_exists p0 - val (vs,_) = strip_exists q0 - val th = assume (Thm.capply @{cterm Trueprop} P) - val th1 = implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th)) - val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th)) - val p = (Thm.dest_arg o Thm.dest_arg1 o cprop_of) th1 - val q = (Thm.dest_arg o Thm.dest_arg o cprop_of) th1 - in implies_elim (implies_elim (instantiate' [] [SOME p, SOME q] iffI) th1) th2 - |> mk_meta_eq - end; - - - fun getname v = case term_of v of - Free(s,_) => s - | Var ((s,_),_) => s - | _ => "x" - fun mk_eq s t = Thm.capply (Thm.capply @{cterm "op == :: bool => _"} s) t - fun mkeq s t = Thm.capply @{cterm Trueprop} (Thm.capply (Thm.capply @{cterm "op = :: bool => _"} s) t) - fun mk_exists v th = arg_cong_rule (ext (ctyp_of_term v)) - (Thm.abstract_rule (getname v) v th) - val simp_ex_conv = - Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms(39)}) - -fun frees t = Thm.add_cterm_frees t []; -fun free_in v t = member op aconvc (frees t) v; - -val vsubst = let - fun vsubst (t,v) tm = - (Thm.rhs_of o Thm.beta_conversion false) (Thm.capply (Thm.cabs v tm) t) -in fold vsubst end; - - -(** main **) - -fun ring_and_ideal_conv - {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), - field = (f_ops, f_rules), idom, ideal} - dest_const mk_const ring_eq_conv ring_normalize_conv = -let - val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops; - val [ring_add_tm, ring_mul_tm, ring_pow_tm] = - map dest_fun2 [add_pat, mul_pat, pow_pat]; - - val (ring_sub_tm, ring_neg_tm) = - (case r_ops of - [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat) - |_ => (@{cterm "True"}, @{cterm "True"})); - - val (field_div_tm, field_inv_tm) = - (case f_ops of - [div_pat, inv_pat] => (dest_fun2 div_pat, dest_fun inv_pat) - | _ => (@{cterm "True"}, @{cterm "True"})); - - val [idom_thm, neq_thm] = idom; - val [idl_sub, idl_add0] = - if length ideal = 2 then ideal else [eq_commute, eq_commute] - fun ring_dest_neg t = - let val (l,r) = dest_comb t - in if Term.could_unify(term_of l,term_of ring_neg_tm) then r - else raise CTERM ("ring_dest_neg", [t]) - end - - val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm); - fun field_dest_inv t = - let val (l,r) = dest_comb t in - if Term.could_unify(term_of l, term_of field_inv_tm) then r - else raise CTERM ("field_dest_inv", [t]) - end - val ring_dest_add = dest_binary ring_add_tm; - val ring_mk_add = mk_binop ring_add_tm; - val ring_dest_sub = dest_binary ring_sub_tm; - val ring_mk_sub = mk_binop ring_sub_tm; - val ring_dest_mul = dest_binary ring_mul_tm; - val ring_mk_mul = mk_binop ring_mul_tm; - val field_dest_div = dest_binary field_div_tm; - val field_mk_div = mk_binop field_div_tm; - val ring_dest_pow = dest_binary ring_pow_tm; - val ring_mk_pow = mk_binop ring_pow_tm ; - fun grobvars tm acc = - if can dest_const tm then acc - else if can ring_dest_neg tm then grobvars (dest_arg tm) acc - else if can ring_dest_pow tm then grobvars (dest_arg1 tm) acc - else if can ring_dest_add tm orelse can ring_dest_sub tm - orelse can ring_dest_mul tm - then grobvars (dest_arg1 tm) (grobvars (dest_arg tm) acc) - else if can field_dest_inv tm - then - let val gvs = grobvars (dest_arg tm) [] - in if null gvs then acc else tm::acc - end - else if can field_dest_div tm then - let val lvs = grobvars (dest_arg1 tm) acc - val gvs = grobvars (dest_arg tm) [] - in if null gvs then lvs else tm::acc - end - else tm::acc ; - -fun grobify_term vars tm = -((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else - [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)]) -handle CTERM _ => - ((let val x = dest_const tm - in if x =/ rat_0 then [] else [(x,map (fn v => 0) vars)] - end) - handle ERROR _ => - ((grob_neg(grobify_term vars (ring_dest_neg tm))) - handle CTERM _ => - ( - (grob_inv(grobify_term vars (field_dest_inv tm))) - handle CTERM _ => - ((let val (l,r) = ring_dest_add tm - in grob_add (grobify_term vars l) (grobify_term vars r) - end) - handle CTERM _ => - ((let val (l,r) = ring_dest_sub tm - in grob_sub (grobify_term vars l) (grobify_term vars r) - end) - handle CTERM _ => - ((let val (l,r) = ring_dest_mul tm - in grob_mul (grobify_term vars l) (grobify_term vars r) - end) - handle CTERM _ => - ( (let val (l,r) = field_dest_div tm - in grob_div (grobify_term vars l) (grobify_term vars r) - end) - handle CTERM _ => - ((let val (l,r) = ring_dest_pow tm - in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r) - end) - handle CTERM _ => error "grobify_term: unknown or invalid term"))))))))); -val eq_tm = idom_thm |> concl |> dest_arg |> dest_arg |> dest_fun2; -val dest_eq = dest_binary eq_tm; - -fun grobify_equation vars tm = - let val (l,r) = dest_binary eq_tm tm - in grob_sub (grobify_term vars l) (grobify_term vars r) - end; - -fun grobify_equations tm = - let - val cjs = conjs tm - val rawvars = fold_rev (fn eq => fn a => - grobvars (dest_arg1 eq) (grobvars (dest_arg eq) a)) cjs [] - val vars = sort (fn (x, y) => Term_Ord.term_ord(term_of x,term_of y)) - (distinct (op aconvc) rawvars) - in (vars,map (grobify_equation vars) cjs) - end; - -val holify_polynomial = - let fun holify_varpow (v,n) = - if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp "nat"} n) (* FIXME *) - fun holify_monomial vars (c,m) = - let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m)) - in end_itlist ring_mk_mul (mk_const c :: xps) - end - fun holify_polynomial vars p = - if null p then mk_const (rat_0) - else end_itlist ring_mk_add (map (holify_monomial vars) p) - in holify_polynomial - end ; -val idom_rule = simplify (HOL_basic_ss addsimps [idom_thm]); -fun prove_nz n = eqF_elim - (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const(rat_0)))); -val neq_01 = prove_nz (rat_1); -fun neq_rule n th = [prove_nz n, th] MRS neq_thm; -fun mk_add th1 = combination(arg_cong_rule ring_add_tm th1); - -fun refute tm = - if tm aconvc false_tm then assume_Trueprop tm else - ((let - val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims (assume_Trueprop tm)) - val nths = filter (is_eq o dest_arg o concl) nths0 - val eths = filter (is_eq o concl) eths0 - in - if null eths then - let - val th1 = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths - val th2 = Conv.fconv_rule - ((arg_conv #> arg_conv) - (binop_conv ring_normalize_conv)) th1 - val conc = th2 |> concl |> dest_arg - val (l,r) = conc |> dest_eq - in implies_intr (mk_comb cTrp tm) - (equal_elim (arg_cong_rule cTrp (eqF_intr th2)) - (reflexive l |> mk_object_eq)) - end - else - let - val (vars,l,cert,noteqth) =( - if null nths then - let val (vars,pols) = grobify_equations(list_mk_conj(map concl eths)) - val (l,cert) = grobner_weak vars pols - in (vars,l,cert,neq_01) - end - else - let - val nth = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths - val (vars,pol::pols) = - grobify_equations(list_mk_conj(dest_arg(concl nth)::map concl eths)) - val (deg,l,cert) = grobner_strong vars pols pol - val th1 = Conv.fconv_rule((arg_conv o arg_conv)(binop_conv ring_normalize_conv)) nth - val th2 = funpow deg (idom_rule o HOLogic.conj_intr th1) neq_01 - in (vars,l,cert,th2) - end) - val cert_pos = map (fn (i,p) => (i,filter (fn (c,m) => c >/ rat_0) p)) cert - val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m)) - (filter (fn (c,m) => c (i,holify_polynomial vars p)) cert_pos - val herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg - fun thm_fn pols = - if null pols then reflexive(mk_const rat_0) else - end_itlist mk_add - (map (fn (i,p) => arg_cong_rule (mk_comb ring_mul_tm p) - (nth eths i |> mk_meta_eq)) pols) - val th1 = thm_fn herts_pos - val th2 = thm_fn herts_neg - val th3 = HOLogic.conj_intr(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth - val th4 = Conv.fconv_rule ((arg_conv o arg_conv o binop_conv) ring_normalize_conv) - (neq_rule l th3) - val (l,r) = dest_eq(dest_arg(concl th4)) - in implies_intr (mk_comb cTrp tm) - (equal_elim (arg_cong_rule cTrp (eqF_intr th4)) - (reflexive l |> mk_object_eq)) - end - end) handle ERROR _ => raise CTERM ("Gorbner-refute: unable to refute",[tm])) - -fun ring tm = - let - fun mk_forall x p = - mk_comb (cterm_rule (instantiate' [SOME (ctyp_of_term x)] []) @{cpat "All:: (?'a => bool) => _"}) (cabs x p) - val avs = add_cterm_frees tm [] - val P' = fold mk_forall avs tm - val th1 = initial_conv(mk_neg P') - val (evs,bod) = strip_exists(concl th1) in - if is_forall bod then raise CTERM("ring: non-universal formula",[tm]) - else - let - val th1a = weak_dnf_conv bod - val boda = concl th1a - val th2a = refute_disj refute boda - val th2b = [mk_object_eq th1a, (th2a COMP notI) COMP PFalse'] MRS trans - val th2 = fold (fn v => fn th => (forall_intr v th) COMP allI) evs (th2b RS PFalse) - val th3 = equal_elim - (Simplifier.rewrite (HOL_basic_ss addsimps [not_ex RS sym]) - (th2 |> cprop_of)) th2 - in specl avs - ([[[mk_object_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD) - end - end -fun ideal tms tm ord = - let - val rawvars = fold_rev grobvars (tm::tms) [] - val vars = sort ord (distinct (fn (x,y) => (term_of x) aconv (term_of y)) rawvars) - val pols = map (grobify_term vars) tms - val pol = grobify_term vars tm - val cert = grobner_ideal vars pols pol - in map_range (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars) - (length pols) - end - -fun poly_eq_conv t = - let val (a,b) = Thm.dest_binop t - in fconv_rule (arg_conv (arg1_conv ring_normalize_conv)) - (instantiate' [] [SOME a, SOME b] idl_sub) - end - val poly_eq_simproc = - let - fun proc phi ss t = - let val th = poly_eq_conv t - in if Thm.is_reflexive th then NONE else SOME th - end - in make_simproc {lhss = [Thm.lhs_of idl_sub], - name = "poly_eq_simproc", proc = proc, identifier = []} - end; - val poly_eq_ss = HOL_basic_ss addsimps @{thms simp_thms} - addsimprocs [poly_eq_simproc] - - local - fun is_defined v t = - let - val mons = striplist(dest_binary ring_add_tm) t - in member (op aconvc) mons v andalso - forall (fn m => v aconvc m - orelse not(member (op aconvc) (Thm.add_cterm_frees m []) v)) mons - end - - fun isolate_variable vars tm = - let - val th = poly_eq_conv tm - val th' = (sym_conv then_conv poly_eq_conv) tm - val (v,th1) = - case find_first(fn v=> is_defined v (Thm.dest_arg1 (Thm.rhs_of th))) vars of - SOME v => (v,th') - | NONE => (the (find_first - (fn v => is_defined v (Thm.dest_arg1 (Thm.rhs_of th'))) vars) ,th) - val th2 = transitive th1 - (instantiate' [] [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v] - idl_add0) - in fconv_rule(funpow 2 arg_conv ring_normalize_conv) th2 - end - in - fun unwind_polys_conv tm = - let - val (vars,bod) = strip_exists tm - val cjs = striplist (dest_binary @{cterm "op &"}) bod - val th1 = (the (get_first (try (isolate_variable vars)) cjs) - handle Option => raise CTERM ("unwind_polys_conv",[tm])) - val eq = Thm.lhs_of th1 - val bod' = list_mk_binop @{cterm "op &"} (eq::(remove op aconvc eq cjs)) - val th2 = conj_ac_rule (mk_eq bod bod') - val th3 = transitive th2 - (Drule.binop_cong_rule @{cterm "op &"} th1 - (reflexive (Thm.dest_arg (Thm.rhs_of th2)))) - val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3)) - val vars' = (remove op aconvc v vars) @ [v] - val th4 = fconv_rule (arg_conv simp_ex_conv) (mk_exists v th3) - val th5 = ex_eq_conv (mk_eq tm (fold mk_ex (remove op aconvc v vars) (Thm.lhs_of th4))) - in transitive th5 (fold mk_exists (remove op aconvc v vars) th4) - end; -end - -local - fun scrub_var v m = - let - val ps = striplist ring_dest_mul m - val ps' = remove op aconvc v ps - in if null ps' then one_tm else fold1 ring_mk_mul ps' - end - fun find_multipliers v mons = - let - val mons1 = filter (fn m => free_in v m) mons - val mons2 = map (scrub_var v) mons1 - in if null mons2 then zero_tm else fold1 ring_mk_add mons2 - end - - fun isolate_monomials vars tm = - let - val (cmons,vmons) = - List.partition (fn m => null (inter (op aconvc) vars (frees m))) - (striplist ring_dest_add tm) - val cofactors = map (fn v => find_multipliers v vmons) vars - val cnc = if null cmons then zero_tm - else Thm.capply ring_neg_tm - (list_mk_binop ring_add_tm cmons) - in (cofactors,cnc) - end; - -fun isolate_variables evs ps eq = - let - val vars = filter (fn v => free_in v eq) evs - val (qs,p) = isolate_monomials vars eq - val rs = ideal (qs @ ps) p - (fn (s,t) => Term_Ord.term_ord (term_of s, term_of t)) - in (eq, take (length qs) rs ~~ vars) - end; - fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p)); -in - fun solve_idealism evs ps eqs = - if null evs then [] else - let - val (eq,cfs) = get_first (try (isolate_variables evs ps)) eqs |> the - val evs' = subtract op aconvc evs (map snd cfs) - val eqs' = map (subst_in_poly cfs) (remove op aconvc eq eqs) - in cfs @ solve_idealism evs' ps eqs' - end; -end; - - -in {ring_conv = ring, simple_ideal = ideal, multi_ideal = solve_idealism, - poly_eq_ss = poly_eq_ss, unwind_conv = unwind_polys_conv} -end; - - -fun find_term bounds tm = - (case term_of tm of - Const ("op =", T) $ _ $ _ => - if domain_type T = HOLogic.boolT then find_args bounds tm - else dest_arg tm - | Const ("Not", _) $ _ => find_term bounds (dest_arg tm) - | Const ("All", _) $ _ => find_body bounds (dest_arg tm) - | Const ("Ex", _) $ _ => find_body bounds (dest_arg tm) - | Const ("op &", _) $ _ $ _ => find_args bounds tm - | Const ("op |", _) $ _ $ _ => find_args bounds tm - | Const ("op -->", _) $ _ $ _ => find_args bounds tm - | @{term "op ==>"} $_$_ => find_args bounds tm - | Const("op ==",_)$_$_ => find_args bounds tm - | @{term Trueprop}$_ => find_term bounds (dest_arg tm) - | _ => raise TERM ("find_term", [])) -and find_args bounds tm = - let val (t, u) = Thm.dest_binop tm - in (find_term bounds t handle TERM _ => find_term bounds u) end -and find_body bounds b = - let val (_, b') = dest_abs (SOME (Name.bound bounds)) b - in find_term (bounds + 1) b' end; - - -fun get_ring_ideal_convs ctxt form = - case try (find_term 0) form of - NONE => NONE -| SOME tm => - (case Normalizer.match ctxt tm of - NONE => NONE - | SOME (res as (theory, {is_const, dest_const, - mk_const, conv = ring_eq_conv})) => - SOME (ring_and_ideal_conv theory - dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt) - (Normalizer.semiring_normalize_wrapper ctxt res))) - -fun ring_solve ctxt form = - (case try (find_term 0 (* FIXME !? *)) form of - NONE => reflexive form - | SOME tm => - (case Normalizer.match ctxt tm of - NONE => reflexive form - | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) => - #ring_conv (ring_and_ideal_conv theory - dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt) - (Normalizer.semiring_normalize_wrapper ctxt res)) form)); - -fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (Simplifier.context ctxt - (HOL_basic_ss addsimps (Algebra_Simplification.get ctxt) delsimps del_thms addsimps add_thms)); - -fun ring_tac add_ths del_ths ctxt = - Object_Logic.full_atomize_tac - THEN' presimplify ctxt add_ths del_ths - THEN' CSUBGOAL (fn (p, i) => - rtac (let val form = Object_Logic.dest_judgment p - in case get_ring_ideal_convs ctxt form of - NONE => reflexive form - | SOME thy => #ring_conv thy form - end) i - handle TERM _ => no_tac - | CTERM _ => no_tac - | THM _ => no_tac); - -local - fun lhs t = case term_of t of - Const("op =",_)$_$_ => Thm.dest_arg1 t - | _=> raise CTERM ("ideal_tac - lhs",[t]) - fun exitac NONE = no_tac - | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1 -in -fun ideal_tac add_ths del_ths ctxt = - presimplify ctxt add_ths del_ths - THEN' - CSUBGOAL (fn (p, i) => - case get_ring_ideal_convs ctxt p of - NONE => no_tac - | SOME thy => - let - fun poly_exists_tac {asms = asms, concl = concl, prems = prems, - params = params, context = ctxt, schematics = scs} = - let - val (evs,bod) = strip_exists (Thm.dest_arg concl) - val ps = map_filter (try (lhs o Thm.dest_arg)) asms - val cfs = (map swap o #multi_ideal thy evs ps) - (map Thm.dest_arg1 (conjuncts bod)) - val ws = map (exitac o AList.lookup op aconvc cfs) evs - in EVERY (rev ws) THEN Method.insert_tac prems 1 - THEN ring_tac add_ths del_ths ctxt 1 - end - in - clarify_tac @{claset} i - THEN Object_Logic.full_atomize_tac i - THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i - THEN clarify_tac @{claset} i - THEN (REPEAT (CONVERSION (#unwind_conv thy) i)) - THEN SUBPROOF poly_exists_tac ctxt i - end - handle TERM _ => no_tac - | CTERM _ => no_tac - | THM _ => no_tac); -end; - -fun algebra_tac add_ths del_ths ctxt i = - ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i - -local - -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () -val addN = "add" -val delN = "del" -val any_keyword = keyword addN || keyword delN -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; - -in - -val algebra_method = ((Scan.optional (keyword addN |-- thms) []) -- - (Scan.optional (keyword delN |-- thms) [])) >> - (fn (add_ths, del_ths) => fn ctxt => - SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt)) - -end; - -end; diff -r dce592144219 -r 5ce217fc769a src/HOL/Tools/Groebner_Basis/normalizer.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Fri May 07 23:44:10 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1062 +0,0 @@ -(* Title: HOL/Tools/Groebner_Basis/normalizer.ML - Author: Amine Chaieb, TU Muenchen - -Normalization of expressions in semirings. -*) - -signature NORMALIZER = -sig - type entry - val get: Proof.context -> (thm * entry) list - val match: Proof.context -> cterm -> entry option - val del: attribute - val add: {semiring: cterm list * thm list, ring: cterm list * thm list, - field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute - val funs: thm -> {is_const: morphism -> cterm -> bool, - dest_const: morphism -> cterm -> Rat.rat, - mk_const: morphism -> ctyp -> Rat.rat -> cterm, - conv: morphism -> Proof.context -> cterm -> thm} -> declaration - val semiring_funs: thm -> declaration - val field_funs: thm -> declaration - - val semiring_normalize_conv: Proof.context -> conv - val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv - val semiring_normalize_wrapper: Proof.context -> entry -> conv - val semiring_normalize_ord_wrapper: Proof.context -> entry - -> (cterm -> cterm -> bool) -> conv - val semiring_normalizers_conv: cterm list -> cterm list * thm list - -> cterm list * thm list -> cterm list * thm list -> - (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) -> - {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} - val semiring_normalizers_ord_wrapper: Proof.context -> entry -> - (cterm -> cterm -> bool) -> - {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} - val field_comp_conv: conv - - val setup: theory -> theory -end - -structure Normalizer: NORMALIZER = -struct - -(** some conversion **) - -local - val zr = @{cpat "0"} - val zT = ctyp_of_term zr - val geq = @{cpat "op ="} - val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd - val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} - val add_frac_num = mk_meta_eq @{thm "add_frac_num"} - val add_num_frac = mk_meta_eq @{thm "add_num_frac"} - - fun prove_nz ss T t = - let - val z = instantiate_cterm ([(zT,T)],[]) zr - val eq = instantiate_cterm ([(eqT,T)],[]) geq - val th = Simplifier.rewrite (ss addsimps @{thms simp_thms}) - (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} - (Thm.capply (Thm.capply eq t) z))) - in equal_elim (symmetric th) TrueI - end - - fun proc phi ss ct = - let - val ((x,y),(w,z)) = - (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct - val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] - val T = ctyp_of_term x - val [y_nz, z_nz] = map (prove_nz ss T) [y, z] - val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq - in SOME (implies_elim (implies_elim th y_nz) z_nz) - end - handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE - - fun proc2 phi ss ct = - let - val (l,r) = Thm.dest_binop ct - val T = ctyp_of_term l - in (case (term_of l, term_of r) of - (Const(@{const_name Rings.divide},_)$_$_, _) => - let val (x,y) = Thm.dest_binop l val z = r - val _ = map (HOLogic.dest_number o term_of) [x,y,z] - val ynz = prove_nz ss T y - in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) - end - | (_, Const (@{const_name Rings.divide},_)$_$_) => - let val (x,y) = Thm.dest_binop r val z = l - val _ = map (HOLogic.dest_number o term_of) [x,y,z] - val ynz = prove_nz ss T y - in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) - end - | _ => NONE) - end - handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE - - fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b - | is_number t = can HOLogic.dest_number t - - val is_number = is_number o term_of - - fun proc3 phi ss ct = - (case term_of ct of - Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => - let - val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"} - in SOME (mk_meta_eq th) end - | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => - let - val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"} - in SOME (mk_meta_eq th) end - | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => - let - val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"} - in SOME (mk_meta_eq th) end - | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => - let - val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"} - in SOME (mk_meta_eq th) end - | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => - let - val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"} - in SOME (mk_meta_eq th) end - | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) => - let - val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} - in SOME (mk_meta_eq th) end - | _ => NONE) - handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE - -val add_frac_frac_simproc = - make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], - name = "add_frac_frac_simproc", - proc = proc, identifier = []} - -val add_frac_num_simproc = - make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], - name = "add_frac_num_simproc", - proc = proc2, identifier = []} - -val ord_frac_simproc = - make_simproc - {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, - @{cpat "(?a::(?'a::{field, ord}))/?b <= ?c"}, - @{cpat "?c < (?a::(?'a::{field, ord}))/?b"}, - @{cpat "?c <= (?a::(?'a::{field, ord}))/?b"}, - @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"}, - @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}], - name = "ord_frac_simproc", proc = proc3, identifier = []} - -val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, - @{thm "divide_Numeral1"}, - @{thm "divide_zero"}, @{thm "divide_Numeral0"}, - @{thm "divide_divide_eq_left"}, - @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"}, - @{thm "times_divide_times_eq"}, - @{thm "divide_divide_eq_right"}, - @{thm "diff_def"}, @{thm "minus_divide_left"}, - @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym, - @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, - Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute})))) - (@{thm field_divide_inverse} RS sym)] - -in - -val field_comp_conv = (Simplifier.rewrite -(HOL_basic_ss addsimps @{thms "semiring_norm"} - addsimps ths addsimps @{thms simp_thms} - addsimprocs Numeral_Simprocs.field_cancel_numeral_factors - addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, - ord_frac_simproc] - addcongs [@{thm "if_weak_cong"}])) -then_conv (Simplifier.rewrite (HOL_basic_ss addsimps - [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)})) - -end - - -(** data **) - -type entry = - {vars: cterm list, - semiring: cterm list * thm list, - ring: cterm list * thm list, - field: cterm list * thm list, - idom: thm list, - ideal: thm list} * - {is_const: cterm -> bool, - dest_const: cterm -> Rat.rat, - mk_const: ctyp -> Rat.rat -> cterm, - conv: Proof.context -> cterm -> thm}; - -structure Data = Generic_Data -( - type T = (thm * entry) list; - val empty = []; - val extend = I; - val merge = AList.merge Thm.eq_thm (K true); -); - -val get = Data.get o Context.Proof; - -fun match ctxt tm = - let - fun match_inst - ({vars, semiring = (sr_ops, sr_rules), - ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal}, - fns as {is_const, dest_const, mk_const, conv}) pat = - let - fun h instT = - let - val substT = Thm.instantiate (instT, []); - val substT_cterm = Drule.cterm_rule substT; - - val vars' = map substT_cterm vars; - val semiring' = (map substT_cterm sr_ops, map substT sr_rules); - val ring' = (map substT_cterm r_ops, map substT r_rules); - val field' = (map substT_cterm f_ops, map substT f_rules); - val idom' = map substT idom; - val ideal' = map substT ideal; - - val result = ({vars = vars', semiring = semiring', - ring = ring', field = field', idom = idom', ideal = ideal'}, fns); - in SOME result end - in (case try Thm.match (pat, tm) of - NONE => NONE - | SOME (instT, _) => h instT) - end; - - fun match_struct (_, - entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) = - get_first (match_inst entry) (sr_ops @ r_ops @ f_ops); - in get_first match_struct (get ctxt) end; - - -(* logical content *) - -val semiringN = "semiring"; -val ringN = "ring"; -val idomN = "idom"; -val idealN = "ideal"; -val fieldN = "field"; - -val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm); - -fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), - field = (f_ops, f_rules), idom, ideal} = - Thm.declaration_attribute (fn key => fn context => context |> Data.map - let - val ctxt = Context.proof_of context; - - fun check kind name xs n = - null xs orelse length xs = n orelse - error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); - val check_ops = check "operations"; - val check_rules = check "rules"; - - val _ = - check_ops semiringN sr_ops 5 andalso - check_rules semiringN sr_rules 37 andalso - check_ops ringN r_ops 2 andalso - check_rules ringN r_rules 2 andalso - check_ops fieldN f_ops 2 andalso - check_rules fieldN f_rules 2 andalso - check_rules idomN idom 2; - - val mk_meta = Local_Defs.meta_rewrite_rule ctxt; - val sr_rules' = map mk_meta sr_rules; - val r_rules' = map mk_meta r_rules; - val f_rules' = map mk_meta f_rules; - - fun rule i = nth sr_rules' (i - 1); - - val (cx, cy) = Thm.dest_binop (hd sr_ops); - val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; - val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; - val ((clx, crx), (cly, cry)) = - rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; - val ((ca, cb), (cc, cd)) = - rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; - val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg; - val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg; - - val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; - val semiring = (sr_ops, sr_rules'); - val ring = (r_ops, r_rules'); - val field = (f_ops, f_rules'); - val ideal' = map (symmetric o mk_meta) ideal - in - AList.delete Thm.eq_thm key #> - cons (key, ({vars = vars, semiring = semiring, - ring = ring, field = field, idom = idom, ideal = ideal'}, - {is_const = undefined, dest_const = undefined, mk_const = undefined, - conv = undefined})) - end); - - -(* extra-logical functions *) - -fun funs raw_key {is_const, dest_const, mk_const, conv} phi = - Data.map (fn data => - let - val key = Morphism.thm phi raw_key; - val _ = AList.defined Thm.eq_thm data key orelse - raise THM ("No data entry for structure key", 0, [key]); - val fns = {is_const = is_const phi, dest_const = dest_const phi, - mk_const = mk_const phi, conv = conv phi}; - in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end); - -fun semiring_funs key = funs key - {is_const = fn phi => can HOLogic.dest_number o Thm.term_of, - dest_const = fn phi => fn ct => - Rat.rat_of_int (snd - (HOLogic.dest_number (Thm.term_of ct) - handle TERM _ => error "ring_dest_const")), - mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT - (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"), - conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}) - then_conv Simplifier.rewrite (HOL_basic_ss addsimps - (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))}; - -fun field_funs key = - let - fun numeral_is_const ct = - case term_of ct of - Const (@{const_name Rings.divide},_) $ a $ b => - can HOLogic.dest_number a andalso can HOLogic.dest_number b - | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t - | t => can HOLogic.dest_number t - fun dest_const ct = ((case term_of ct of - Const (@{const_name Rings.divide},_) $ a $ b=> - Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) - | Const (@{const_name Rings.inverse},_)$t => - Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t))) - | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) - handle TERM _ => error "ring_dest_const") - fun mk_const phi cT x = - let val (a, b) = Rat.quotient_of_rat x - in if b = 1 then Numeral.mk_cnumber cT a - else Thm.capply - (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) - (Numeral.mk_cnumber cT a)) - (Numeral.mk_cnumber cT b) - end - in funs key - {is_const = K numeral_is_const, - dest_const = K dest_const, - mk_const = mk_const, - conv = K (K field_comp_conv)} - end; - - - -(** auxiliary **) - -fun is_comb ct = - (case Thm.term_of ct of - _ $ _ => true - | _ => false); - -val concl = Thm.cprop_of #> Thm.dest_arg; - -fun is_binop ct ct' = - (case Thm.term_of ct' of - c $ _ $ _ => term_of ct aconv c - | _ => false); - -fun dest_binop ct ct' = - if is_binop ct ct' then Thm.dest_binop ct' - else raise CTERM ("dest_binop: bad binop", [ct, ct']) - -fun inst_thm inst = Thm.instantiate ([], inst); - -val dest_numeral = term_of #> HOLogic.dest_number #> snd; -val is_numeral = can dest_numeral; - -val numeral01_conv = Simplifier.rewrite - (HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]); -val zero1_numeral_conv = - Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]); -fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv; -val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"}, - @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, - @{thm "less_nat_number_of"}]; - -val nat_add_conv = - zerone_conv - (Simplifier.rewrite - (HOL_basic_ss - addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps} - @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}, - @{thm add_number_of_left}, @{thm Suc_eq_plus1}] - @ map (fn th => th RS sym) @{thms numerals})); - -val zeron_tm = @{cterm "0::nat"}; -val onen_tm = @{cterm "1::nat"}; -val true_tm = @{cterm "True"}; - - -(** normalizing conversions **) - -(* core conversion *) - -fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules) - (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) = -let - -val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08, - pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16, - pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24, - pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32, - pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules; - -val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars; -val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops; -val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat]; - -val dest_add = dest_binop add_tm -val dest_mul = dest_binop mul_tm -fun dest_pow tm = - let val (l,r) = dest_binop pow_tm tm - in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm]) - end; -val is_add = is_binop add_tm -val is_mul = is_binop mul_tm -fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm); - -val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') = - (case (r_ops, r_rules) of - ([sub_pat, neg_pat], [neg_mul, sub_add]) => - let - val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat) - val neg_tm = Thm.dest_fun neg_pat - val dest_sub = dest_binop sub_tm - val is_sub = is_binop sub_tm - in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg, - sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg) - end - | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)); - -val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = - (case (f_ops, f_rules) of - ([divide_pat, inverse_pat], [div_inv, inv_div]) => - let val div_tm = funpow 2 Thm.dest_fun divide_pat - val inv_tm = Thm.dest_fun inverse_pat - in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm) - end - | _ => (TrueI, TrueI, true_tm, true_tm, K false)); - -in fn variable_order => - let - -(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible. *) -(* Also deals with "const * const", but both terms must involve powers of *) -(* the same variable, or both be constants, or behaviour may be incorrect. *) - - fun powvar_mul_conv tm = - let - val (l,r) = dest_mul tm - in if is_semiring_constant l andalso is_semiring_constant r - then semiring_mul_conv tm - else - ((let - val (lx,ln) = dest_pow l - in - ((let val (rx,rn) = dest_pow r - val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29 - val (tm1,tm2) = Thm.dest_comb(concl th1) in - transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end) - handle CTERM _ => - (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31 - val (tm1,tm2) = Thm.dest_comb(concl th1) in - transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end) - handle CTERM _ => - ((let val (rx,rn) = dest_pow r - val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30 - val (tm1,tm2) = Thm.dest_comb(concl th1) in - transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end) - handle CTERM _ => inst_thm [(cx,l)] pthm_32 - -)) - end; - -(* Remove "1 * m" from a monomial, and just leave m. *) - - fun monomial_deone th = - (let val (l,r) = dest_mul(concl th) in - if l aconvc one_tm - then transitive th (inst_thm [(ca,r)] pthm_13) else th end) - handle CTERM _ => th; - -(* Conversion for "(monomial)^n", where n is a numeral. *) - - val monomial_pow_conv = - let - fun monomial_pow tm bod ntm = - if not(is_comb bod) - then reflexive tm - else - if is_semiring_constant bod - then semiring_pow_conv tm - else - let - val (lopr,r) = Thm.dest_comb bod - in if not(is_comb lopr) - then reflexive tm - else - let - val (opr,l) = Thm.dest_comb lopr - in - if opr aconvc pow_tm andalso is_numeral r - then - let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34 - val (l,r) = Thm.dest_comb(concl th1) - in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r)) - end - else - if opr aconvc mul_tm - then - let - val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33 - val (xy,z) = Thm.dest_comb(concl th1) - val (x,y) = Thm.dest_comb xy - val thl = monomial_pow y l ntm - val thr = monomial_pow z r ntm - in transitive th1 (combination (Drule.arg_cong_rule x thl) thr) - end - else reflexive tm - end - end - in fn tm => - let - val (lopr,r) = Thm.dest_comb tm - val (opr,l) = Thm.dest_comb lopr - in if not (opr aconvc pow_tm) orelse not(is_numeral r) - then raise CTERM ("monomial_pow_conv", [tm]) - else if r aconvc zeron_tm - then inst_thm [(cx,l)] pthm_35 - else if r aconvc onen_tm - then inst_thm [(cx,l)] pthm_36 - else monomial_deone(monomial_pow tm l r) - end - end; - -(* Multiplication of canonical monomials. *) - val monomial_mul_conv = - let - fun powvar tm = - if is_semiring_constant tm then one_tm - else - ((let val (lopr,r) = Thm.dest_comb tm - val (opr,l) = Thm.dest_comb lopr - in if opr aconvc pow_tm andalso is_numeral r then l - else raise CTERM ("monomial_mul_conv",[tm]) end) - handle CTERM _ => tm) (* FIXME !? *) - fun vorder x y = - if x aconvc y then 0 - else - if x aconvc one_tm then ~1 - else if y aconvc one_tm then 1 - else if variable_order x y then ~1 else 1 - fun monomial_mul tm l r = - ((let val (lx,ly) = dest_mul l val vl = powvar lx - in - ((let - val (rx,ry) = dest_mul r - val vr = powvar rx - val ord = vorder vl vr - in - if ord = 0 - then - let - val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15 - val (tm1,tm2) = Thm.dest_comb(concl th1) - val (tm3,tm4) = Thm.dest_comb tm1 - val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2 - val th3 = transitive th1 th2 - val (tm5,tm6) = Thm.dest_comb(concl th3) - val (tm7,tm8) = Thm.dest_comb tm6 - val th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8 - in transitive th3 (Drule.arg_cong_rule tm5 th4) - end - else - let val th0 = if ord < 0 then pthm_16 else pthm_17 - val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0 - val (tm1,tm2) = Thm.dest_comb(concl th1) - val (tm3,tm4) = Thm.dest_comb tm2 - in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) - end - end) - handle CTERM _ => - (let val vr = powvar r val ord = vorder vl vr - in - if ord = 0 then - let - val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18 - val (tm1,tm2) = Thm.dest_comb(concl th1) - val (tm3,tm4) = Thm.dest_comb tm1 - val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2 - in transitive th1 th2 - end - else - if ord < 0 then - let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19 - val (tm1,tm2) = Thm.dest_comb(concl th1) - val (tm3,tm4) = Thm.dest_comb tm2 - in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) - end - else inst_thm [(ca,l),(cb,r)] pthm_09 - end)) end) - handle CTERM _ => - (let val vl = powvar l in - ((let - val (rx,ry) = dest_mul r - val vr = powvar rx - val ord = vorder vl vr - in if ord = 0 then - let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21 - val (tm1,tm2) = Thm.dest_comb(concl th1) - val (tm3,tm4) = Thm.dest_comb tm1 - in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2) - end - else if ord > 0 then - let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22 - val (tm1,tm2) = Thm.dest_comb(concl th1) - val (tm3,tm4) = Thm.dest_comb tm2 - in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) - end - else reflexive tm - end) - handle CTERM _ => - (let val vr = powvar r - val ord = vorder vl vr - in if ord = 0 then powvar_mul_conv tm - else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09 - else reflexive tm - end)) end)) - in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r) - end - end; -(* Multiplication by monomial of a polynomial. *) - - val polynomial_monomial_mul_conv = - let - fun pmm_conv tm = - let val (l,r) = dest_mul tm - in - ((let val (y,z) = dest_add r - val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37 - val (tm1,tm2) = Thm.dest_comb(concl th1) - val (tm3,tm4) = Thm.dest_comb tm1 - val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2) - in transitive th1 th2 - end) - handle CTERM _ => monomial_mul_conv tm) - end - in pmm_conv - end; - -(* Addition of two monomials identical except for constant multiples. *) - -fun monomial_add_conv tm = - let val (l,r) = dest_add tm - in if is_semiring_constant l andalso is_semiring_constant r - then semiring_add_conv tm - else - let val th1 = - if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l) - then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then - inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02 - else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03 - else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) - then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04 - else inst_thm [(cm,r)] pthm_05 - val (tm1,tm2) = Thm.dest_comb(concl th1) - val (tm3,tm4) = Thm.dest_comb tm1 - val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4) - val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2) - val tm5 = concl th3 - in - if (Thm.dest_arg1 tm5) aconvc zero_tm - then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11) - else monomial_deone th3 - end - end; - -(* Ordering on monomials. *) - -fun striplist dest = - let fun strip x acc = - ((let val (l,r) = dest x in - strip l (strip r acc) end) - handle CTERM _ => x::acc) (* FIXME !? *) - in fn x => strip x [] - end; - - -fun powervars tm = - let val ptms = striplist dest_mul tm - in if is_semiring_constant (hd ptms) then tl ptms else ptms - end; -val num_0 = 0; -val num_1 = 1; -fun dest_varpow tm = - ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end) - handle CTERM _ => - (tm,(if is_semiring_constant tm then num_0 else num_1))); - -val morder = - let fun lexorder l1 l2 = - case (l1,l2) of - ([],[]) => 0 - | (vps,[]) => ~1 - | ([],vps) => 1 - | (((x1,n1)::vs1),((x2,n2)::vs2)) => - if variable_order x1 x2 then 1 - else if variable_order x2 x1 then ~1 - else if n1 < n2 then ~1 - else if n2 < n1 then 1 - else lexorder vs1 vs2 - in fn tm1 => fn tm2 => - let val vdegs1 = map dest_varpow (powervars tm1) - val vdegs2 = map dest_varpow (powervars tm2) - val deg1 = fold (Integer.add o snd) vdegs1 num_0 - val deg2 = fold (Integer.add o snd) vdegs2 num_0 - in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1 - else lexorder vdegs1 vdegs2 - end - end; - -(* Addition of two polynomials. *) - -val polynomial_add_conv = - let - fun dezero_rule th = - let - val tm = concl th - in - if not(is_add tm) then th else - let val (lopr,r) = Thm.dest_comb tm - val l = Thm.dest_arg lopr - in - if l aconvc zero_tm - then transitive th (inst_thm [(ca,r)] pthm_07) else - if r aconvc zero_tm - then transitive th (inst_thm [(ca,l)] pthm_08) else th - end - end - fun padd tm = - let - val (l,r) = dest_add tm - in - if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07 - else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08 - else - if is_add l - then - let val (a,b) = dest_add l - in - if is_add r then - let val (c,d) = dest_add r - val ord = morder a c - in - if ord = 0 then - let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23 - val (tm1,tm2) = Thm.dest_comb(concl th1) - val (tm3,tm4) = Thm.dest_comb tm1 - val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4) - in dezero_rule (transitive th1 (combination th2 (padd tm2))) - end - else (* ord <> 0*) - let val th1 = - if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24 - else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25 - val (tm1,tm2) = Thm.dest_comb(concl th1) - in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) - end - end - else (* not (is_add r)*) - let val ord = morder a r - in - if ord = 0 then - let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26 - val (tm1,tm2) = Thm.dest_comb(concl th1) - val (tm3,tm4) = Thm.dest_comb tm1 - val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2 - in dezero_rule (transitive th1 th2) - end - else (* ord <> 0*) - if ord > 0 then - let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24 - val (tm1,tm2) = Thm.dest_comb(concl th1) - in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) - end - else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27) - end - end - else (* not (is_add l)*) - if is_add r then - let val (c,d) = dest_add r - val ord = morder l c - in - if ord = 0 then - let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28 - val (tm1,tm2) = Thm.dest_comb(concl th1) - val (tm3,tm4) = Thm.dest_comb tm1 - val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2 - in dezero_rule (transitive th1 th2) - end - else - if ord > 0 then reflexive tm - else - let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25 - val (tm1,tm2) = Thm.dest_comb(concl th1) - in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) - end - end - else - let val ord = morder l r - in - if ord = 0 then monomial_add_conv tm - else if ord > 0 then dezero_rule(reflexive tm) - else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27) - end - end - in padd - end; - -(* Multiplication of two polynomials. *) - -val polynomial_mul_conv = - let - fun pmul tm = - let val (l,r) = dest_mul tm - in - if not(is_add l) then polynomial_monomial_mul_conv tm - else - if not(is_add r) then - let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09 - in transitive th1 (polynomial_monomial_mul_conv(concl th1)) - end - else - let val (a,b) = dest_add l - val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10 - val (tm1,tm2) = Thm.dest_comb(concl th1) - val (tm3,tm4) = Thm.dest_comb tm1 - val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4) - val th3 = transitive th1 (combination th2 (pmul tm2)) - in transitive th3 (polynomial_add_conv (concl th3)) - end - end - in fn tm => - let val (l,r) = dest_mul tm - in - if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11 - else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12 - else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13 - else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14 - else pmul tm - end - end; - -(* Power of polynomial (optimized for the monomial and trivial cases). *) - -fun num_conv n = - nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1))) - |> Thm.symmetric; - - -val polynomial_pow_conv = - let - fun ppow tm = - let val (l,n) = dest_pow tm - in - if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35 - else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36 - else - let val th1 = num_conv n - val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38 - val (tm1,tm2) = Thm.dest_comb(concl th2) - val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2)) - val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3 - in transitive th4 (polynomial_mul_conv (concl th4)) - end - end - in fn tm => - if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm - end; - -(* Negation. *) - -fun polynomial_neg_conv tm = - let val (l,r) = Thm.dest_comb tm in - if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else - let val th1 = inst_thm [(cx',r)] neg_mul - val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1)) - in transitive th2 (polynomial_monomial_mul_conv (concl th2)) - end - end; - - -(* Subtraction. *) -fun polynomial_sub_conv tm = - let val (l,r) = dest_sub tm - val th1 = inst_thm [(cx',l),(cy',r)] sub_add - val (tm1,tm2) = Thm.dest_comb(concl th1) - val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2) - in transitive th1 (transitive th2 (polynomial_add_conv (concl th2))) - end; - -(* Conversion from HOL term. *) - -fun polynomial_conv tm = - if is_semiring_constant tm then semiring_add_conv tm - else if not(is_comb tm) then reflexive tm - else - let val (lopr,r) = Thm.dest_comb tm - in if lopr aconvc neg_tm then - let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) - in transitive th1 (polynomial_neg_conv (concl th1)) - end - else if lopr aconvc inverse_tm then - let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) - in transitive th1 (semiring_mul_conv (concl th1)) - end - else - if not(is_comb lopr) then reflexive tm - else - let val (opr,l) = Thm.dest_comb lopr - in if opr aconvc pow_tm andalso is_numeral r - then - let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r - in transitive th1 (polynomial_pow_conv (concl th1)) - end - else if opr aconvc divide_tm - then - let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) - (polynomial_conv r) - val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv) - (Thm.rhs_of th1) - in transitive th1 th2 - end - else - if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm - then - let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r) - val f = if opr aconvc add_tm then polynomial_add_conv - else if opr aconvc mul_tm then polynomial_mul_conv - else polynomial_sub_conv - in transitive th1 (f (concl th1)) - end - else reflexive tm - end - end; - in - {main = polynomial_conv, - add = polynomial_add_conv, - mul = polynomial_mul_conv, - pow = polynomial_pow_conv, - neg = polynomial_neg_conv, - sub = polynomial_sub_conv} - end -end; - -val nat_exp_ss = - HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps}) - addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]; - -fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS; - - -(* various normalizing conversions *) - -fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, - {conv, dest_const, mk_const, is_const}) ord = - let - val pow_conv = - Conv.arg_conv (Simplifier.rewrite nat_exp_ss) - then_conv Simplifier.rewrite - (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34]) - then_conv conv ctxt - val dat = (is_const, conv ctxt, conv ctxt, pow_conv) - in semiring_normalizers_conv vars semiring ring field dat ord end; - -fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord = - #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); - -fun semiring_normalize_wrapper ctxt data = - semiring_normalize_ord_wrapper ctxt data simple_cterm_ord; - -fun semiring_normalize_ord_conv ctxt ord tm = - (case match ctxt tm of - NONE => reflexive tm - | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm); - -fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord; - - -(** Isar setup **) - -local - -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); -fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K (); -fun keyword3 k1 k2 k3 = - Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K (); - -val opsN = "ops"; -val rulesN = "rules"; - -val normN = "norm"; -val constN = "const"; -val delN = "del"; - -val any_keyword = - keyword2 semiringN opsN || keyword2 semiringN rulesN || - keyword2 ringN opsN || keyword2 ringN rulesN || - keyword2 fieldN opsN || keyword2 fieldN rulesN || - keyword2 idomN rulesN || keyword2 idealN rulesN; - -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; -val terms = thms >> map Drule.dest_term; - -fun optional scan = Scan.optional scan []; - -in - -val setup = - Attrib.setup @{binding normalizer} - (Scan.lift (Args.$$$ delN >> K del) || - ((keyword2 semiringN opsN |-- terms) -- - (keyword2 semiringN rulesN |-- thms)) -- - (optional (keyword2 ringN opsN |-- terms) -- - optional (keyword2 ringN rulesN |-- thms)) -- - (optional (keyword2 fieldN opsN |-- terms) -- - optional (keyword2 fieldN rulesN |-- thms)) -- - optional (keyword2 idomN rulesN |-- thms) -- - optional (keyword2 idealN rulesN |-- thms) - >> (fn ((((sr, r), f), id), idl) => - add {semiring = sr, ring = r, field = f, idom = id, ideal = idl})) - "semiring normalizer data"; - -end; - -end; diff -r dce592144219 -r 5ce217fc769a src/HOL/Tools/groebner.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/groebner.ML Sat May 08 17:15:50 2010 +0200 @@ -0,0 +1,1045 @@ +(* Title: HOL/Tools/Groebner_Basis/groebner.ML + Author: Amine Chaieb, TU Muenchen +*) + +signature GROEBNER = +sig + val ring_and_ideal_conv : + {idom: thm list, ring: cterm list * thm list, field: cterm list * thm list, + vars: cterm list, semiring: cterm list * thm list, ideal : thm list} -> + (cterm -> Rat.rat) -> (Rat.rat -> cterm) -> + conv -> conv -> + {ring_conv : conv, + simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list), + multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list, + poly_eq_ss: simpset, unwind_conv : conv} + val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic + val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic + val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic + val algebra_method: (Proof.context -> Method.method) context_parser +end + +structure Groebner : GROEBNER = +struct + +open Conv Drule Thm; + +fun is_comb ct = + (case Thm.term_of ct of + _ $ _ => true + | _ => false); + +val concl = Thm.cprop_of #> Thm.dest_arg; + +fun is_binop ct ct' = + (case Thm.term_of ct' of + c $ _ $ _ => term_of ct aconv c + | _ => false); + +fun dest_binary ct ct' = + if is_binop ct ct' then Thm.dest_binop ct' + else raise CTERM ("dest_binary: bad binop", [ct, ct']) + +fun inst_thm inst = Thm.instantiate ([], inst); + +val rat_0 = Rat.zero; +val rat_1 = Rat.one; +val minus_rat = Rat.neg; +val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int; +fun int_of_rat a = + case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int"; +val lcm_rat = fn x => fn y => Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y)); + +val (eqF_intr, eqF_elim) = + let val [th1,th2] = @{thms PFalse} + in (fn th => th COMP th2, fn th => th COMP th1) end; + +val (PFalse, PFalse') = + let val PFalse_eq = nth @{thms simp_thms} 13 + in (PFalse_eq RS iffD1, PFalse_eq RS iffD2) end; + + +(* Type for recording history, i.e. how a polynomial was obtained. *) + +datatype history = + Start of int + | Mmul of (Rat.rat * int list) * history + | Add of history * history; + + +(* Monomial ordering. *) + +fun morder_lt m1 m2= + let fun lexorder l1 l2 = + case (l1,l2) of + ([],[]) => false + | (x1::o1,x2::o2) => x1 > x2 orelse x1 = x2 andalso lexorder o1 o2 + | _ => error "morder: inconsistent monomial lengths" + val n1 = Integer.sum m1 + val n2 = Integer.sum m2 in + n1 < n2 orelse n1 = n2 andalso lexorder m1 m2 + end; + +fun morder_le m1 m2 = morder_lt m1 m2 orelse (m1 = m2); + +fun morder_gt m1 m2 = morder_lt m2 m1; + +(* Arithmetic on canonical polynomials. *) + +fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l; + +fun grob_add l1 l2 = + case (l1,l2) of + ([],l2) => l2 + | (l1,[]) => l1 + | ((c1,m1)::o1,(c2,m2)::o2) => + if m1 = m2 then + let val c = c1+/c2 val rest = grob_add o1 o2 in + if c =/ rat_0 then rest else (c,m1)::rest end + else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2) + else (c2,m2)::(grob_add l1 o2); + +fun grob_sub l1 l2 = grob_add l1 (grob_neg l2); + +fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2, ListPair.map (op +) (m1, m2)); + +fun grob_cmul cm pol = map (grob_mmul cm) pol; + +fun grob_mul l1 l2 = + case l1 of + [] => [] + | (h1::t1) => grob_add (grob_cmul h1 l2) (grob_mul t1 l2); + +fun grob_inv l = + case l of + [(c,vs)] => if (forall (fn x => x = 0) vs) then + if (c =/ rat_0) then error "grob_inv: division by zero" + else [(rat_1 // c,vs)] + else error "grob_inv: non-constant divisor polynomial" + | _ => error "grob_inv: non-constant divisor polynomial"; + +fun grob_div l1 l2 = + case l2 of + [(c,l)] => if (forall (fn x => x = 0) l) then + if c =/ rat_0 then error "grob_div: division by zero" + else grob_cmul (rat_1 // c,l) l1 + else error "grob_div: non-constant divisor polynomial" + | _ => error "grob_div: non-constant divisor polynomial"; + +fun grob_pow vars l n = + if n < 0 then error "grob_pow: negative power" + else if n = 0 then [(rat_1,map (fn v => 0) vars)] + else grob_mul l (grob_pow vars l (n - 1)); + +fun degree vn p = + case p of + [] => error "Zero polynomial" +| [(c,ns)] => nth ns vn +| (c,ns)::p' => Int.max (nth ns vn, degree vn p'); + +fun head_deg vn p = let val d = degree vn p in + (d,fold (fn (c,r) => fn q => grob_add q [(c, map_index (fn (i,n) => if i = vn then 0 else n) r)]) (filter (fn (c,ns) => c <>/ rat_0 andalso nth ns vn = d) p) []) end; + +val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) 0) ns); +val grob_pdiv = + let fun pdiv_aux vn (n,a) p k s = + if is_zerop s then (k,s) else + let val (m,b) = head_deg vn s + in if m < n then (k,s) else + let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m - n else 0) + (snd (hd s)))] + in if a = b then pdiv_aux vn (n,a) p k (grob_sub s p') + else pdiv_aux vn (n,a) p (k + 1) (grob_sub (grob_mul a s) (grob_mul b p')) + end + end + in fn vn => fn s => fn p => pdiv_aux vn (head_deg vn p) p 0 s + end; + +(* Monomial division operation. *) + +fun mdiv (c1,m1) (c2,m2) = + (c1//c2, + map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 - n2) m1 m2); + +(* Lowest common multiple of two monomials. *) + +fun mlcm (c1,m1) (c2,m2) = (rat_1, ListPair.map Int.max (m1, m2)); + +(* Reduce monomial cm by polynomial pol, returning replacement for cm. *) + +fun reduce1 cm (pol,hpol) = + case pol of + [] => error "reduce1" + | cm1::cms => ((let val (c,m) = mdiv cm cm1 in + (grob_cmul (minus_rat c,m) cms, + Mmul((minus_rat c,m),hpol)) end) + handle ERROR _ => error "reduce1"); + +(* Try this for all polynomials in a basis. *) +fun tryfind f l = + case l of + [] => error "tryfind" + | (h::t) => ((f h) handle ERROR _ => tryfind f t); + +fun reduceb cm basis = tryfind (fn p => reduce1 cm p) basis; + +(* Reduction of a polynomial (always picking largest monomial possible). *) + +fun reduce basis (pol,hist) = + case pol of + [] => (pol,hist) + | cm::ptl => ((let val (q,hnew) = reduceb cm basis in + reduce basis (grob_add q ptl,Add(hnew,hist)) end) + handle (ERROR _) => + (let val (q,hist') = reduce basis (ptl,hist) in + (cm::q,hist') end)); + +(* Check for orthogonality w.r.t. LCM. *) + +fun orthogonal l p1 p2 = + snd l = snd(grob_mmul (hd p1) (hd p2)); + +(* Compute S-polynomial of two polynomials. *) + +fun spoly cm ph1 ph2 = + case (ph1,ph2) of + (([],h),p) => ([],h) + | (p,([],h)) => ([],h) + | ((cm1::ptl1,his1),(cm2::ptl2,his2)) => + (grob_sub (grob_cmul (mdiv cm cm1) ptl1) + (grob_cmul (mdiv cm cm2) ptl2), + Add(Mmul(mdiv cm cm1,his1), + Mmul(mdiv (minus_rat(fst cm),snd cm) cm2,his2))); + +(* Make a polynomial monic. *) + +fun monic (pol,hist) = + if null pol then (pol,hist) else + let val (c',m') = hd pol in + (map (fn (c,m) => (c//c',m)) pol, + Mmul((rat_1 // c',map (K 0) m'),hist)) end; + +(* The most popular heuristic is to order critical pairs by LCM monomial. *) + +fun forder ((c1,m1),_) ((c2,m2),_) = morder_lt m1 m2; + +fun poly_lt p q = + case (p,q) of + (p,[]) => false + | ([],q) => true + | ((c1,m1)::o1,(c2,m2)::o2) => + c1 true + | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2 + | _ => false; + +fun poly_eq p1 p2 = + forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2; + +fun memx ((p1,h1),(p2,h2)) ppairs = + not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs); + +(* Buchberger's second criterion. *) + +fun criterion2 basis (lcm,((p1,h1),(p2,h2))) opairs = + exists (fn g => not(poly_eq (fst g) p1) andalso not(poly_eq (fst g) p2) andalso + can (mdiv lcm) (hd(fst g)) andalso + not(memx (align (g,(p1,h1))) (map snd opairs)) andalso + not(memx (align (g,(p2,h2))) (map snd opairs))) basis; + +(* Test for hitting constant polynomial. *) + +fun constant_poly p = + length p = 1 andalso forall (fn x => x = 0) (snd(hd p)); + +(* Grobner basis algorithm. *) + +(* FIXME: try to get rid of mergesort? *) +fun merge ord l1 l2 = + case l1 of + [] => l2 + | h1::t1 => + case l2 of + [] => l1 + | h2::t2 => if ord h1 h2 then h1::(merge ord t1 l2) + else h2::(merge ord l1 t2); +fun mergesort ord l = + let + fun mergepairs l1 l2 = + case (l1,l2) of + ([s],[]) => s + | (l,[]) => mergepairs [] l + | (l,[s1]) => mergepairs (s1::l) [] + | (l,(s1::s2::ss)) => mergepairs ((merge ord s1 s2)::l) ss + in if null l then [] else mergepairs [] (map (fn x => [x]) l) + end; + + +fun grobner_basis basis pairs = + case pairs of + [] => basis + | (l,(p1,p2))::opairs => + let val (sph as (sp,hist)) = monic (reduce basis (spoly l p1 p2)) + in + if null sp orelse criterion2 basis (l,(p1,p2)) opairs + then grobner_basis basis opairs + else if constant_poly sp then grobner_basis (sph::basis) [] + else + let + val rawcps = map (fn p => (mlcm (hd(fst p)) (hd sp),align(p,sph))) + basis + val newcps = filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q))) + rawcps + in grobner_basis (sph::basis) + (merge forder opairs (mergesort forder newcps)) + end + end; + +(* Interreduce initial polynomials. *) + +fun grobner_interreduce rpols ipols = + case ipols of + [] => map monic (rev rpols) + | p::ps => let val p' = reduce (rpols @ ps) p in + if null (fst p') then grobner_interreduce rpols ps + else grobner_interreduce (p'::rpols) ps end; + +(* Overall function. *) + +fun grobner pols = + let val npols = map_index (fn (n, p) => (p, Start n)) pols + val phists = filter (fn (p,_) => not (null p)) npols + val bas = grobner_interreduce [] (map monic phists) + val prs0 = map_product pair bas bas + val prs1 = filter (fn ((x,_),(y,_)) => poly_lt x y) prs0 + val prs2 = map (fn (p,q) => (mlcm (hd(fst p)) (hd(fst q)),(p,q))) prs1 + val prs3 = + filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q))) prs2 in + grobner_basis bas (mergesort forder prs3) end; + +(* Get proof of contradiction from Grobner basis. *) + +fun find p l = + case l of + [] => error "find" + | (h::t) => if p(h) then h else find p t; + +fun grobner_refute pols = + let val gb = grobner pols in + snd(find (fn (p,h) => length p = 1 andalso forall (fn x=> x=0) (snd(hd p))) gb) + end; + +(* Turn proof into a certificate as sum of multipliers. *) +(* In principle this is very inefficient: in a heavily shared proof it may *) +(* make the same calculation many times. Could put in a cache or something. *) + +fun resolve_proof vars prf = + case prf of + Start(~1) => [] + | Start m => [(m,[(rat_1,map (K 0) vars)])] + | Mmul(pol,lin) => + let val lis = resolve_proof vars lin in + map (fn (n,p) => (n,grob_cmul pol p)) lis end + | Add(lin1,lin2) => + let val lis1 = resolve_proof vars lin1 + val lis2 = resolve_proof vars lin2 + val dom = distinct (op =) (union (op =) (map fst lis1) (map fst lis2)) + in + map (fn n => let val a = these (AList.lookup (op =) lis1 n) + val b = these (AList.lookup (op =) lis2 n) + in (n,grob_add a b) end) dom end; + +(* Run the procedure and produce Weak Nullstellensatz certificate. *) + +fun grobner_weak vars pols = + let val cert = resolve_proof vars (grobner_refute pols) + val l = + fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in + (l,map (fn (i,p) => (i,map (fn (d,m) => (l*/d,m)) p)) cert) end; + +(* Prove a polynomial is in ideal generated by others, using Grobner basis. *) + +fun grobner_ideal vars pols pol = + let val (pol',h) = reduce (grobner pols) (grob_neg pol,Start(~1)) in + if not (null pol') then error "grobner_ideal: not in the ideal" else + resolve_proof vars h end; + +(* Produce Strong Nullstellensatz certificate for a power of pol. *) + +fun grobner_strong vars pols pol = + let val vars' = @{cterm "True"}::vars + val grob_z = [(rat_1,1::(map (fn x => 0) vars))] + val grob_1 = [(rat_1,(map (fn x => 0) vars'))] + fun augment p= map (fn (c,m) => (c,0::m)) p + val pols' = map augment pols + val pol' = augment pol + val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols' + val (l,cert) = grobner_weak vars' allpols + val d = fold (fold (Integer.max o hd o snd) o snd) cert 0 + fun transform_monomial (c,m) = + grob_cmul (c,tl m) (grob_pow vars pol (d - hd m)) + fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q [] + val cert' = map (fn (c,q) => (c-1,transform_polynomial q)) + (filter (fn (k,_) => k <> 0) cert) in + (d,l,cert') end; + + +(* Overall parametrized universal procedure for (semi)rings. *) +(* We return an ideal_conv and the actual ring prover. *) + +fun refute_disj rfn tm = + case term_of tm of + Const("op |",_)$l$r => + compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE)) + | _ => rfn tm ; + +val notnotD = @{thm notnotD}; +fun mk_binop ct x y = capply (capply ct x) y + +val mk_comb = capply; +fun is_neg t = + case term_of t of + (Const("Not",_)$p) => true + | _ => false; +fun is_eq t = + case term_of t of + (Const("op =",_)$_$_) => true +| _ => false; + +fun end_itlist f l = + case l of + [] => error "end_itlist" + | [x] => x + | (h::t) => f h (end_itlist f t); + +val list_mk_binop = fn b => end_itlist (mk_binop b); + +val list_dest_binop = fn b => + let fun h acc t = + ((let val (l,r) = dest_binary b t in h (h acc r) l end) + handle CTERM _ => (t::acc)) (* Why had I handle _ => ? *) + in h [] + end; + +val strip_exists = + let fun h (acc, t) = + case (term_of t) of + Const("Ex",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc)) + | _ => (acc,t) + in fn t => h ([],t) + end; + +fun is_forall t = + case term_of t of + (Const("All",_)$Abs(_,_,_)) => true +| _ => false; + +val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq; +val bool_simps = @{thms bool_simps}; +val nnf_simps = @{thms nnf_simps}; +val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps bool_simps addsimps nnf_simps) +val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms weak_dnf_simps}); +val initial_conv = + Simplifier.rewrite + (HOL_basic_ss addsimps nnf_simps + addsimps [not_all, not_ex] + addsimps map (fn th => th RS sym) (@{thms ex_simps} @ @{thms all_simps})); + +val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec)); + +val cTrp = @{cterm "Trueprop"}; +val cConj = @{cterm "op &"}; +val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"}); +val assume_Trueprop = mk_comb cTrp #> assume; +val list_mk_conj = list_mk_binop cConj; +val conjs = list_dest_binop cConj; +val mk_neg = mk_comb cNot; + +fun striplist dest = + let + fun h acc x = case try dest x of + SOME (a,b) => h (h acc b) a + | NONE => x::acc + in h [] end; +fun list_mk_binop b = foldr1 (fn (s,t) => Thm.capply (Thm.capply b s) t); + +val eq_commute = mk_meta_eq @{thm eq_commute}; + +fun sym_conv eq = + let val (l,r) = Thm.dest_binop eq + in instantiate' [SOME (ctyp_of_term l)] [SOME l, SOME r] eq_commute + end; + + (* FIXME : copied from cqe.ML -- complex QE*) +fun conjuncts ct = + case term_of ct of + @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct)) +| _ => [ct]; + +fun fold1 f = foldr1 (uncurry f); + +val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ; + +fun mk_conj_tab th = + let fun h acc th = + case prop_of th of + @{term "Trueprop"}$(@{term "op &"}$p$q) => + h (h acc (th RS conjunct2)) (th RS conjunct1) + | @{term "Trueprop"}$p => (p,th)::acc +in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end; + +fun is_conj (@{term "op &"}$_$_) = true + | is_conj _ = false; + +fun prove_conj tab cjs = + case cjs of + [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c + | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs]; + +fun conj_ac_rule eq = + let + val (l,r) = Thm.dest_equals eq + val ctabl = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} l)) + val ctabr = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} r)) + fun tabl c = the (Termtab.lookup ctabl (term_of c)) + fun tabr c = the (Termtab.lookup ctabr (term_of c)) + val thl = prove_conj tabl (conjuncts r) |> implies_intr_hyps + val thr = prove_conj tabr (conjuncts l) |> implies_intr_hyps + val eqI = instantiate' [] [SOME l, SOME r] @{thm iffI} + in implies_elim (implies_elim eqI thl) thr |> mk_meta_eq end; + + (* END FIXME.*) + + (* Conversion for the equivalence of existential statements where + EX quantifiers are rearranged differently *) + fun ext T = cterm_rule (instantiate' [SOME T] []) @{cpat Ex} + fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t) + +fun choose v th th' = case concl_of th of + @{term Trueprop} $ (Const("Ex",_)$_) => + let + val p = (funpow 2 Thm.dest_arg o cprop_of) th + val T = (hd o Thm.dest_ctyp o ctyp_of_term) p + val th0 = fconv_rule (Thm.beta_conversion true) + (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE) + val pv = (Thm.rhs_of o Thm.beta_conversion true) + (Thm.capply @{cterm Trueprop} (Thm.capply p v)) + val th1 = forall_intr v (implies_intr pv th') + in implies_elim (implies_elim th0 th) th1 end +| _ => error "" + +fun simple_choose v th = + choose v (assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th + + + fun mkexi v th = + let + val p = Thm.cabs v (Thm.dest_arg (Thm.cprop_of th)) + in implies_elim + (fconv_rule (Thm.beta_conversion true) (instantiate' [SOME (ctyp_of_term v)] [SOME p, SOME v] @{thm exI})) + th + end + fun ex_eq_conv t = + let + val (p0,q0) = Thm.dest_binop t + val (vs',P) = strip_exists p0 + val (vs,_) = strip_exists q0 + val th = assume (Thm.capply @{cterm Trueprop} P) + val th1 = implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th)) + val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th)) + val p = (Thm.dest_arg o Thm.dest_arg1 o cprop_of) th1 + val q = (Thm.dest_arg o Thm.dest_arg o cprop_of) th1 + in implies_elim (implies_elim (instantiate' [] [SOME p, SOME q] iffI) th1) th2 + |> mk_meta_eq + end; + + + fun getname v = case term_of v of + Free(s,_) => s + | Var ((s,_),_) => s + | _ => "x" + fun mk_eq s t = Thm.capply (Thm.capply @{cterm "op == :: bool => _"} s) t + fun mkeq s t = Thm.capply @{cterm Trueprop} (Thm.capply (Thm.capply @{cterm "op = :: bool => _"} s) t) + fun mk_exists v th = arg_cong_rule (ext (ctyp_of_term v)) + (Thm.abstract_rule (getname v) v th) + val simp_ex_conv = + Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms(39)}) + +fun frees t = Thm.add_cterm_frees t []; +fun free_in v t = member op aconvc (frees t) v; + +val vsubst = let + fun vsubst (t,v) tm = + (Thm.rhs_of o Thm.beta_conversion false) (Thm.capply (Thm.cabs v tm) t) +in fold vsubst end; + + +(** main **) + +fun ring_and_ideal_conv + {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), + field = (f_ops, f_rules), idom, ideal} + dest_const mk_const ring_eq_conv ring_normalize_conv = +let + val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops; + val [ring_add_tm, ring_mul_tm, ring_pow_tm] = + map dest_fun2 [add_pat, mul_pat, pow_pat]; + + val (ring_sub_tm, ring_neg_tm) = + (case r_ops of + [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat) + |_ => (@{cterm "True"}, @{cterm "True"})); + + val (field_div_tm, field_inv_tm) = + (case f_ops of + [div_pat, inv_pat] => (dest_fun2 div_pat, dest_fun inv_pat) + | _ => (@{cterm "True"}, @{cterm "True"})); + + val [idom_thm, neq_thm] = idom; + val [idl_sub, idl_add0] = + if length ideal = 2 then ideal else [eq_commute, eq_commute] + fun ring_dest_neg t = + let val (l,r) = dest_comb t + in if Term.could_unify(term_of l,term_of ring_neg_tm) then r + else raise CTERM ("ring_dest_neg", [t]) + end + + val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm); + fun field_dest_inv t = + let val (l,r) = dest_comb t in + if Term.could_unify(term_of l, term_of field_inv_tm) then r + else raise CTERM ("field_dest_inv", [t]) + end + val ring_dest_add = dest_binary ring_add_tm; + val ring_mk_add = mk_binop ring_add_tm; + val ring_dest_sub = dest_binary ring_sub_tm; + val ring_mk_sub = mk_binop ring_sub_tm; + val ring_dest_mul = dest_binary ring_mul_tm; + val ring_mk_mul = mk_binop ring_mul_tm; + val field_dest_div = dest_binary field_div_tm; + val field_mk_div = mk_binop field_div_tm; + val ring_dest_pow = dest_binary ring_pow_tm; + val ring_mk_pow = mk_binop ring_pow_tm ; + fun grobvars tm acc = + if can dest_const tm then acc + else if can ring_dest_neg tm then grobvars (dest_arg tm) acc + else if can ring_dest_pow tm then grobvars (dest_arg1 tm) acc + else if can ring_dest_add tm orelse can ring_dest_sub tm + orelse can ring_dest_mul tm + then grobvars (dest_arg1 tm) (grobvars (dest_arg tm) acc) + else if can field_dest_inv tm + then + let val gvs = grobvars (dest_arg tm) [] + in if null gvs then acc else tm::acc + end + else if can field_dest_div tm then + let val lvs = grobvars (dest_arg1 tm) acc + val gvs = grobvars (dest_arg tm) [] + in if null gvs then lvs else tm::acc + end + else tm::acc ; + +fun grobify_term vars tm = +((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else + [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)]) +handle CTERM _ => + ((let val x = dest_const tm + in if x =/ rat_0 then [] else [(x,map (fn v => 0) vars)] + end) + handle ERROR _ => + ((grob_neg(grobify_term vars (ring_dest_neg tm))) + handle CTERM _ => + ( + (grob_inv(grobify_term vars (field_dest_inv tm))) + handle CTERM _ => + ((let val (l,r) = ring_dest_add tm + in grob_add (grobify_term vars l) (grobify_term vars r) + end) + handle CTERM _ => + ((let val (l,r) = ring_dest_sub tm + in grob_sub (grobify_term vars l) (grobify_term vars r) + end) + handle CTERM _ => + ((let val (l,r) = ring_dest_mul tm + in grob_mul (grobify_term vars l) (grobify_term vars r) + end) + handle CTERM _ => + ( (let val (l,r) = field_dest_div tm + in grob_div (grobify_term vars l) (grobify_term vars r) + end) + handle CTERM _ => + ((let val (l,r) = ring_dest_pow tm + in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r) + end) + handle CTERM _ => error "grobify_term: unknown or invalid term"))))))))); +val eq_tm = idom_thm |> concl |> dest_arg |> dest_arg |> dest_fun2; +val dest_eq = dest_binary eq_tm; + +fun grobify_equation vars tm = + let val (l,r) = dest_binary eq_tm tm + in grob_sub (grobify_term vars l) (grobify_term vars r) + end; + +fun grobify_equations tm = + let + val cjs = conjs tm + val rawvars = fold_rev (fn eq => fn a => + grobvars (dest_arg1 eq) (grobvars (dest_arg eq) a)) cjs [] + val vars = sort (fn (x, y) => Term_Ord.term_ord(term_of x,term_of y)) + (distinct (op aconvc) rawvars) + in (vars,map (grobify_equation vars) cjs) + end; + +val holify_polynomial = + let fun holify_varpow (v,n) = + if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp "nat"} n) (* FIXME *) + fun holify_monomial vars (c,m) = + let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m)) + in end_itlist ring_mk_mul (mk_const c :: xps) + end + fun holify_polynomial vars p = + if null p then mk_const (rat_0) + else end_itlist ring_mk_add (map (holify_monomial vars) p) + in holify_polynomial + end ; +val idom_rule = simplify (HOL_basic_ss addsimps [idom_thm]); +fun prove_nz n = eqF_elim + (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const(rat_0)))); +val neq_01 = prove_nz (rat_1); +fun neq_rule n th = [prove_nz n, th] MRS neq_thm; +fun mk_add th1 = combination(arg_cong_rule ring_add_tm th1); + +fun refute tm = + if tm aconvc false_tm then assume_Trueprop tm else + ((let + val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims (assume_Trueprop tm)) + val nths = filter (is_eq o dest_arg o concl) nths0 + val eths = filter (is_eq o concl) eths0 + in + if null eths then + let + val th1 = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths + val th2 = Conv.fconv_rule + ((arg_conv #> arg_conv) + (binop_conv ring_normalize_conv)) th1 + val conc = th2 |> concl |> dest_arg + val (l,r) = conc |> dest_eq + in implies_intr (mk_comb cTrp tm) + (equal_elim (arg_cong_rule cTrp (eqF_intr th2)) + (reflexive l |> mk_object_eq)) + end + else + let + val (vars,l,cert,noteqth) =( + if null nths then + let val (vars,pols) = grobify_equations(list_mk_conj(map concl eths)) + val (l,cert) = grobner_weak vars pols + in (vars,l,cert,neq_01) + end + else + let + val nth = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths + val (vars,pol::pols) = + grobify_equations(list_mk_conj(dest_arg(concl nth)::map concl eths)) + val (deg,l,cert) = grobner_strong vars pols pol + val th1 = Conv.fconv_rule((arg_conv o arg_conv)(binop_conv ring_normalize_conv)) nth + val th2 = funpow deg (idom_rule o HOLogic.conj_intr th1) neq_01 + in (vars,l,cert,th2) + end) + val cert_pos = map (fn (i,p) => (i,filter (fn (c,m) => c >/ rat_0) p)) cert + val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m)) + (filter (fn (c,m) => c (i,holify_polynomial vars p)) cert_pos + val herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg + fun thm_fn pols = + if null pols then reflexive(mk_const rat_0) else + end_itlist mk_add + (map (fn (i,p) => arg_cong_rule (mk_comb ring_mul_tm p) + (nth eths i |> mk_meta_eq)) pols) + val th1 = thm_fn herts_pos + val th2 = thm_fn herts_neg + val th3 = HOLogic.conj_intr(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth + val th4 = Conv.fconv_rule ((arg_conv o arg_conv o binop_conv) ring_normalize_conv) + (neq_rule l th3) + val (l,r) = dest_eq(dest_arg(concl th4)) + in implies_intr (mk_comb cTrp tm) + (equal_elim (arg_cong_rule cTrp (eqF_intr th4)) + (reflexive l |> mk_object_eq)) + end + end) handle ERROR _ => raise CTERM ("Gorbner-refute: unable to refute",[tm])) + +fun ring tm = + let + fun mk_forall x p = + mk_comb (cterm_rule (instantiate' [SOME (ctyp_of_term x)] []) @{cpat "All:: (?'a => bool) => _"}) (cabs x p) + val avs = add_cterm_frees tm [] + val P' = fold mk_forall avs tm + val th1 = initial_conv(mk_neg P') + val (evs,bod) = strip_exists(concl th1) in + if is_forall bod then raise CTERM("ring: non-universal formula",[tm]) + else + let + val th1a = weak_dnf_conv bod + val boda = concl th1a + val th2a = refute_disj refute boda + val th2b = [mk_object_eq th1a, (th2a COMP notI) COMP PFalse'] MRS trans + val th2 = fold (fn v => fn th => (forall_intr v th) COMP allI) evs (th2b RS PFalse) + val th3 = equal_elim + (Simplifier.rewrite (HOL_basic_ss addsimps [not_ex RS sym]) + (th2 |> cprop_of)) th2 + in specl avs + ([[[mk_object_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD) + end + end +fun ideal tms tm ord = + let + val rawvars = fold_rev grobvars (tm::tms) [] + val vars = sort ord (distinct (fn (x,y) => (term_of x) aconv (term_of y)) rawvars) + val pols = map (grobify_term vars) tms + val pol = grobify_term vars tm + val cert = grobner_ideal vars pols pol + in map_range (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars) + (length pols) + end + +fun poly_eq_conv t = + let val (a,b) = Thm.dest_binop t + in fconv_rule (arg_conv (arg1_conv ring_normalize_conv)) + (instantiate' [] [SOME a, SOME b] idl_sub) + end + val poly_eq_simproc = + let + fun proc phi ss t = + let val th = poly_eq_conv t + in if Thm.is_reflexive th then NONE else SOME th + end + in make_simproc {lhss = [Thm.lhs_of idl_sub], + name = "poly_eq_simproc", proc = proc, identifier = []} + end; + val poly_eq_ss = HOL_basic_ss addsimps @{thms simp_thms} + addsimprocs [poly_eq_simproc] + + local + fun is_defined v t = + let + val mons = striplist(dest_binary ring_add_tm) t + in member (op aconvc) mons v andalso + forall (fn m => v aconvc m + orelse not(member (op aconvc) (Thm.add_cterm_frees m []) v)) mons + end + + fun isolate_variable vars tm = + let + val th = poly_eq_conv tm + val th' = (sym_conv then_conv poly_eq_conv) tm + val (v,th1) = + case find_first(fn v=> is_defined v (Thm.dest_arg1 (Thm.rhs_of th))) vars of + SOME v => (v,th') + | NONE => (the (find_first + (fn v => is_defined v (Thm.dest_arg1 (Thm.rhs_of th'))) vars) ,th) + val th2 = transitive th1 + (instantiate' [] [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v] + idl_add0) + in fconv_rule(funpow 2 arg_conv ring_normalize_conv) th2 + end + in + fun unwind_polys_conv tm = + let + val (vars,bod) = strip_exists tm + val cjs = striplist (dest_binary @{cterm "op &"}) bod + val th1 = (the (get_first (try (isolate_variable vars)) cjs) + handle Option => raise CTERM ("unwind_polys_conv",[tm])) + val eq = Thm.lhs_of th1 + val bod' = list_mk_binop @{cterm "op &"} (eq::(remove op aconvc eq cjs)) + val th2 = conj_ac_rule (mk_eq bod bod') + val th3 = transitive th2 + (Drule.binop_cong_rule @{cterm "op &"} th1 + (reflexive (Thm.dest_arg (Thm.rhs_of th2)))) + val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3)) + val vars' = (remove op aconvc v vars) @ [v] + val th4 = fconv_rule (arg_conv simp_ex_conv) (mk_exists v th3) + val th5 = ex_eq_conv (mk_eq tm (fold mk_ex (remove op aconvc v vars) (Thm.lhs_of th4))) + in transitive th5 (fold mk_exists (remove op aconvc v vars) th4) + end; +end + +local + fun scrub_var v m = + let + val ps = striplist ring_dest_mul m + val ps' = remove op aconvc v ps + in if null ps' then one_tm else fold1 ring_mk_mul ps' + end + fun find_multipliers v mons = + let + val mons1 = filter (fn m => free_in v m) mons + val mons2 = map (scrub_var v) mons1 + in if null mons2 then zero_tm else fold1 ring_mk_add mons2 + end + + fun isolate_monomials vars tm = + let + val (cmons,vmons) = + List.partition (fn m => null (inter (op aconvc) vars (frees m))) + (striplist ring_dest_add tm) + val cofactors = map (fn v => find_multipliers v vmons) vars + val cnc = if null cmons then zero_tm + else Thm.capply ring_neg_tm + (list_mk_binop ring_add_tm cmons) + in (cofactors,cnc) + end; + +fun isolate_variables evs ps eq = + let + val vars = filter (fn v => free_in v eq) evs + val (qs,p) = isolate_monomials vars eq + val rs = ideal (qs @ ps) p + (fn (s,t) => Term_Ord.term_ord (term_of s, term_of t)) + in (eq, take (length qs) rs ~~ vars) + end; + fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p)); +in + fun solve_idealism evs ps eqs = + if null evs then [] else + let + val (eq,cfs) = get_first (try (isolate_variables evs ps)) eqs |> the + val evs' = subtract op aconvc evs (map snd cfs) + val eqs' = map (subst_in_poly cfs) (remove op aconvc eq eqs) + in cfs @ solve_idealism evs' ps eqs' + end; +end; + + +in {ring_conv = ring, simple_ideal = ideal, multi_ideal = solve_idealism, + poly_eq_ss = poly_eq_ss, unwind_conv = unwind_polys_conv} +end; + + +fun find_term bounds tm = + (case term_of tm of + Const ("op =", T) $ _ $ _ => + if domain_type T = HOLogic.boolT then find_args bounds tm + else dest_arg tm + | Const ("Not", _) $ _ => find_term bounds (dest_arg tm) + | Const ("All", _) $ _ => find_body bounds (dest_arg tm) + | Const ("Ex", _) $ _ => find_body bounds (dest_arg tm) + | Const ("op &", _) $ _ $ _ => find_args bounds tm + | Const ("op |", _) $ _ $ _ => find_args bounds tm + | Const ("op -->", _) $ _ $ _ => find_args bounds tm + | @{term "op ==>"} $_$_ => find_args bounds tm + | Const("op ==",_)$_$_ => find_args bounds tm + | @{term Trueprop}$_ => find_term bounds (dest_arg tm) + | _ => raise TERM ("find_term", [])) +and find_args bounds tm = + let val (t, u) = Thm.dest_binop tm + in (find_term bounds t handle TERM _ => find_term bounds u) end +and find_body bounds b = + let val (_, b') = dest_abs (SOME (Name.bound bounds)) b + in find_term (bounds + 1) b' end; + + +fun get_ring_ideal_convs ctxt form = + case try (find_term 0) form of + NONE => NONE +| SOME tm => + (case Semiring_Normalizer.match ctxt tm of + NONE => NONE + | SOME (res as (theory, {is_const, dest_const, + mk_const, conv = ring_eq_conv})) => + SOME (ring_and_ideal_conv theory + dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt) + (Semiring_Normalizer.semiring_normalize_wrapper ctxt res))) + +fun ring_solve ctxt form = + (case try (find_term 0 (* FIXME !? *)) form of + NONE => reflexive form + | SOME tm => + (case Semiring_Normalizer.match ctxt tm of + NONE => reflexive form + | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) => + #ring_conv (ring_and_ideal_conv theory + dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt) + (Semiring_Normalizer.semiring_normalize_wrapper ctxt res)) form)); + +fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (Simplifier.context ctxt + (HOL_basic_ss addsimps (Algebra_Simplification.get ctxt) delsimps del_thms addsimps add_thms)); + +fun ring_tac add_ths del_ths ctxt = + Object_Logic.full_atomize_tac + THEN' presimplify ctxt add_ths del_ths + THEN' CSUBGOAL (fn (p, i) => + rtac (let val form = Object_Logic.dest_judgment p + in case get_ring_ideal_convs ctxt form of + NONE => reflexive form + | SOME thy => #ring_conv thy form + end) i + handle TERM _ => no_tac + | CTERM _ => no_tac + | THM _ => no_tac); + +local + fun lhs t = case term_of t of + Const("op =",_)$_$_ => Thm.dest_arg1 t + | _=> raise CTERM ("ideal_tac - lhs",[t]) + fun exitac NONE = no_tac + | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1 +in +fun ideal_tac add_ths del_ths ctxt = + presimplify ctxt add_ths del_ths + THEN' + CSUBGOAL (fn (p, i) => + case get_ring_ideal_convs ctxt p of + NONE => no_tac + | SOME thy => + let + fun poly_exists_tac {asms = asms, concl = concl, prems = prems, + params = params, context = ctxt, schematics = scs} = + let + val (evs,bod) = strip_exists (Thm.dest_arg concl) + val ps = map_filter (try (lhs o Thm.dest_arg)) asms + val cfs = (map swap o #multi_ideal thy evs ps) + (map Thm.dest_arg1 (conjuncts bod)) + val ws = map (exitac o AList.lookup op aconvc cfs) evs + in EVERY (rev ws) THEN Method.insert_tac prems 1 + THEN ring_tac add_ths del_ths ctxt 1 + end + in + clarify_tac @{claset} i + THEN Object_Logic.full_atomize_tac i + THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i + THEN clarify_tac @{claset} i + THEN (REPEAT (CONVERSION (#unwind_conv thy) i)) + THEN SUBPROOF poly_exists_tac ctxt i + end + handle TERM _ => no_tac + | CTERM _ => no_tac + | THM _ => no_tac); +end; + +fun algebra_tac add_ths del_ths ctxt i = + ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i + +local + +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () +val addN = "add" +val delN = "del" +val any_keyword = keyword addN || keyword delN +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; + +in + +val algebra_method = ((Scan.optional (keyword addN |-- thms) []) -- + (Scan.optional (keyword delN |-- thms) [])) >> + (fn (add_ths, del_ths) => fn ctxt => + SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt)) + +end; + +end; diff -r dce592144219 -r 5ce217fc769a src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Fri May 07 23:44:10 2010 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Sat May 08 17:15:50 2010 +0200 @@ -1,7 +1,7 @@ (* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 2000 University of Cambridge -Simprocs for the integer numerals. +Simprocs for the (integer) numerals. *) (*To quote from Provers/Arith/cancel_numeral_factor.ML: @@ -24,6 +24,7 @@ val field_combine_numerals: simproc val field_cancel_numeral_factors: simproc list val num_ss: simpset + val field_comp_conv: conv end; structure Numeral_Simprocs : NUMERAL_SIMPROCS = @@ -602,6 +603,157 @@ "(l::'a::field_inverse_zero) / (m * n)"], K DivideCancelFactor.proc)]; +local + val zr = @{cpat "0"} + val zT = ctyp_of_term zr + val geq = @{cpat "op ="} + val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd + val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} + val add_frac_num = mk_meta_eq @{thm "add_frac_num"} + val add_num_frac = mk_meta_eq @{thm "add_num_frac"} + + fun prove_nz ss T t = + let + val z = instantiate_cterm ([(zT,T)],[]) zr + val eq = instantiate_cterm ([(eqT,T)],[]) geq + val th = Simplifier.rewrite (ss addsimps @{thms simp_thms}) + (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} + (Thm.capply (Thm.capply eq t) z))) + in equal_elim (symmetric th) TrueI + end + + fun proc phi ss ct = + let + val ((x,y),(w,z)) = + (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct + val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] + val T = ctyp_of_term x + val [y_nz, z_nz] = map (prove_nz ss T) [y, z] + val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq + in SOME (implies_elim (implies_elim th y_nz) z_nz) + end + handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE + + fun proc2 phi ss ct = + let + val (l,r) = Thm.dest_binop ct + val T = ctyp_of_term l + in (case (term_of l, term_of r) of + (Const(@{const_name Rings.divide},_)$_$_, _) => + let val (x,y) = Thm.dest_binop l val z = r + val _ = map (HOLogic.dest_number o term_of) [x,y,z] + val ynz = prove_nz ss T y + in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) + end + | (_, Const (@{const_name Rings.divide},_)$_$_) => + let val (x,y) = Thm.dest_binop r val z = l + val _ = map (HOLogic.dest_number o term_of) [x,y,z] + val ynz = prove_nz ss T y + in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) + end + | _ => NONE) + end + handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE + + fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b + | is_number t = can HOLogic.dest_number t + + val is_number = is_number o term_of + + fun proc3 phi ss ct = + (case term_of ct of + Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + let + val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"} + in SOME (mk_meta_eq th) end + | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + let + val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"} + in SOME (mk_meta_eq th) end + | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + let + val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"} + in SOME (mk_meta_eq th) end + | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + let + val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"} + in SOME (mk_meta_eq th) end + | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + let + val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"} + in SOME (mk_meta_eq th) end + | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + let + val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} + in SOME (mk_meta_eq th) end + | _ => NONE) + handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE + +val add_frac_frac_simproc = + make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], + name = "add_frac_frac_simproc", + proc = proc, identifier = []} + +val add_frac_num_simproc = + make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], + name = "add_frac_num_simproc", + proc = proc2, identifier = []} + +val ord_frac_simproc = + make_simproc + {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, + @{cpat "(?a::(?'a::{field, ord}))/?b <= ?c"}, + @{cpat "?c < (?a::(?'a::{field, ord}))/?b"}, + @{cpat "?c <= (?a::(?'a::{field, ord}))/?b"}, + @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"}, + @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}], + name = "ord_frac_simproc", proc = proc3, identifier = []} + +val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, + @{thm "divide_Numeral1"}, + @{thm "divide_zero"}, @{thm "divide_Numeral0"}, + @{thm "divide_divide_eq_left"}, + @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"}, + @{thm "times_divide_times_eq"}, + @{thm "divide_divide_eq_right"}, + @{thm "diff_def"}, @{thm "minus_divide_left"}, + @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym, + @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, + Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute})))) + (@{thm field_divide_inverse} RS sym)] + +in + +val field_comp_conv = (Simplifier.rewrite +(HOL_basic_ss addsimps @{thms "semiring_norm"} + addsimps ths addsimps @{thms simp_thms} + addsimprocs field_cancel_numeral_factors + addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, + ord_frac_simproc] + addcongs [@{thm "if_weak_cong"}])) +then_conv (Simplifier.rewrite (HOL_basic_ss addsimps + [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)})) + +end + end; Addsimprocs Numeral_Simprocs.cancel_numerals; diff -r dce592144219 -r 5ce217fc769a src/HOL/Tools/semiring_normalizer.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/semiring_normalizer.ML Sat May 08 17:15:50 2010 +0200 @@ -0,0 +1,907 @@ +(* Title: HOL/Tools/Groebner_Basis/normalizer.ML + Author: Amine Chaieb, TU Muenchen + +Normalization of expressions in semirings. +*) + +signature SEMIRING_NORMALIZER = +sig + type entry + val get: Proof.context -> (thm * entry) list + val match: Proof.context -> cterm -> entry option + val del: attribute + val add: {semiring: cterm list * thm list, ring: cterm list * thm list, + field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute + val funs: thm -> {is_const: morphism -> cterm -> bool, + dest_const: morphism -> cterm -> Rat.rat, + mk_const: morphism -> ctyp -> Rat.rat -> cterm, + conv: morphism -> Proof.context -> cterm -> thm} -> declaration + val semiring_funs: thm -> declaration + val field_funs: thm -> declaration + + val semiring_normalize_conv: Proof.context -> conv + val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv + val semiring_normalize_wrapper: Proof.context -> entry -> conv + val semiring_normalize_ord_wrapper: Proof.context -> entry + -> (cterm -> cterm -> bool) -> conv + val semiring_normalizers_conv: cterm list -> cterm list * thm list + -> cterm list * thm list -> cterm list * thm list -> + (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) -> + {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} + val semiring_normalizers_ord_wrapper: Proof.context -> entry -> + (cterm -> cterm -> bool) -> + {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} + + val setup: theory -> theory +end + +structure Semiring_Normalizer: SEMIRING_NORMALIZER = +struct + +(** data **) + +type entry = + {vars: cterm list, + semiring: cterm list * thm list, + ring: cterm list * thm list, + field: cterm list * thm list, + idom: thm list, + ideal: thm list} * + {is_const: cterm -> bool, + dest_const: cterm -> Rat.rat, + mk_const: ctyp -> Rat.rat -> cterm, + conv: Proof.context -> cterm -> thm}; + +structure Data = Generic_Data +( + type T = (thm * entry) list; + val empty = []; + val extend = I; + val merge = AList.merge Thm.eq_thm (K true); +); + +val get = Data.get o Context.Proof; + +fun match ctxt tm = + let + fun match_inst + ({vars, semiring = (sr_ops, sr_rules), + ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal}, + fns as {is_const, dest_const, mk_const, conv}) pat = + let + fun h instT = + let + val substT = Thm.instantiate (instT, []); + val substT_cterm = Drule.cterm_rule substT; + + val vars' = map substT_cterm vars; + val semiring' = (map substT_cterm sr_ops, map substT sr_rules); + val ring' = (map substT_cterm r_ops, map substT r_rules); + val field' = (map substT_cterm f_ops, map substT f_rules); + val idom' = map substT idom; + val ideal' = map substT ideal; + + val result = ({vars = vars', semiring = semiring', + ring = ring', field = field', idom = idom', ideal = ideal'}, fns); + in SOME result end + in (case try Thm.match (pat, tm) of + NONE => NONE + | SOME (instT, _) => h instT) + end; + + fun match_struct (_, + entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) = + get_first (match_inst entry) (sr_ops @ r_ops @ f_ops); + in get_first match_struct (get ctxt) end; + + +(* logical content *) + +val semiringN = "semiring"; +val ringN = "ring"; +val idomN = "idom"; +val idealN = "ideal"; +val fieldN = "field"; + +val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm); + +fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), + field = (f_ops, f_rules), idom, ideal} = + Thm.declaration_attribute (fn key => fn context => context |> Data.map + let + val ctxt = Context.proof_of context; + + fun check kind name xs n = + null xs orelse length xs = n orelse + error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); + val check_ops = check "operations"; + val check_rules = check "rules"; + + val _ = + check_ops semiringN sr_ops 5 andalso + check_rules semiringN sr_rules 37 andalso + check_ops ringN r_ops 2 andalso + check_rules ringN r_rules 2 andalso + check_ops fieldN f_ops 2 andalso + check_rules fieldN f_rules 2 andalso + check_rules idomN idom 2; + + val mk_meta = Local_Defs.meta_rewrite_rule ctxt; + val sr_rules' = map mk_meta sr_rules; + val r_rules' = map mk_meta r_rules; + val f_rules' = map mk_meta f_rules; + + fun rule i = nth sr_rules' (i - 1); + + val (cx, cy) = Thm.dest_binop (hd sr_ops); + val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; + val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; + val ((clx, crx), (cly, cry)) = + rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; + val ((ca, cb), (cc, cd)) = + rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; + val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg; + val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg; + + val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; + val semiring = (sr_ops, sr_rules'); + val ring = (r_ops, r_rules'); + val field = (f_ops, f_rules'); + val ideal' = map (symmetric o mk_meta) ideal + in + AList.delete Thm.eq_thm key #> + cons (key, ({vars = vars, semiring = semiring, + ring = ring, field = field, idom = idom, ideal = ideal'}, + {is_const = undefined, dest_const = undefined, mk_const = undefined, + conv = undefined})) + end); + + +(* extra-logical functions *) + +fun funs raw_key {is_const, dest_const, mk_const, conv} phi = + Data.map (fn data => + let + val key = Morphism.thm phi raw_key; + val _ = AList.defined Thm.eq_thm data key orelse + raise THM ("No data entry for structure key", 0, [key]); + val fns = {is_const = is_const phi, dest_const = dest_const phi, + mk_const = mk_const phi, conv = conv phi}; + in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end); + +fun semiring_funs key = funs key + {is_const = fn phi => can HOLogic.dest_number o Thm.term_of, + dest_const = fn phi => fn ct => + Rat.rat_of_int (snd + (HOLogic.dest_number (Thm.term_of ct) + handle TERM _ => error "ring_dest_const")), + mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT + (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"), + conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}) + then_conv Simplifier.rewrite (HOL_basic_ss addsimps + (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))}; + +fun field_funs key = + let + fun numeral_is_const ct = + case term_of ct of + Const (@{const_name Rings.divide},_) $ a $ b => + can HOLogic.dest_number a andalso can HOLogic.dest_number b + | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t + | t => can HOLogic.dest_number t + fun dest_const ct = ((case term_of ct of + Const (@{const_name Rings.divide},_) $ a $ b=> + Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) + | Const (@{const_name Rings.inverse},_)$t => + Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t))) + | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) + handle TERM _ => error "ring_dest_const") + fun mk_const phi cT x = + let val (a, b) = Rat.quotient_of_rat x + in if b = 1 then Numeral.mk_cnumber cT a + else Thm.capply + (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) + (Numeral.mk_cnumber cT a)) + (Numeral.mk_cnumber cT b) + end + in funs key + {is_const = K numeral_is_const, + dest_const = K dest_const, + mk_const = mk_const, + conv = K (K Numeral_Simprocs.field_comp_conv)} + end; + + + +(** auxiliary **) + +fun is_comb ct = + (case Thm.term_of ct of + _ $ _ => true + | _ => false); + +val concl = Thm.cprop_of #> Thm.dest_arg; + +fun is_binop ct ct' = + (case Thm.term_of ct' of + c $ _ $ _ => term_of ct aconv c + | _ => false); + +fun dest_binop ct ct' = + if is_binop ct ct' then Thm.dest_binop ct' + else raise CTERM ("dest_binop: bad binop", [ct, ct']) + +fun inst_thm inst = Thm.instantiate ([], inst); + +val dest_numeral = term_of #> HOLogic.dest_number #> snd; +val is_numeral = can dest_numeral; + +val numeral01_conv = Simplifier.rewrite + (HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]); +val zero1_numeral_conv = + Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]); +fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv; +val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"}, + @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, + @{thm "less_nat_number_of"}]; + +val nat_add_conv = + zerone_conv + (Simplifier.rewrite + (HOL_basic_ss + addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps} + @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}, + @{thm add_number_of_left}, @{thm Suc_eq_plus1}] + @ map (fn th => th RS sym) @{thms numerals})); + +val zeron_tm = @{cterm "0::nat"}; +val onen_tm = @{cterm "1::nat"}; +val true_tm = @{cterm "True"}; + + +(** normalizing conversions **) + +(* core conversion *) + +fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules) + (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) = +let + +val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08, + pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16, + pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24, + pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32, + pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules; + +val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars; +val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops; +val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat]; + +val dest_add = dest_binop add_tm +val dest_mul = dest_binop mul_tm +fun dest_pow tm = + let val (l,r) = dest_binop pow_tm tm + in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm]) + end; +val is_add = is_binop add_tm +val is_mul = is_binop mul_tm +fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm); + +val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') = + (case (r_ops, r_rules) of + ([sub_pat, neg_pat], [neg_mul, sub_add]) => + let + val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat) + val neg_tm = Thm.dest_fun neg_pat + val dest_sub = dest_binop sub_tm + val is_sub = is_binop sub_tm + in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg, + sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg) + end + | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)); + +val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = + (case (f_ops, f_rules) of + ([divide_pat, inverse_pat], [div_inv, inv_div]) => + let val div_tm = funpow 2 Thm.dest_fun divide_pat + val inv_tm = Thm.dest_fun inverse_pat + in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm) + end + | _ => (TrueI, TrueI, true_tm, true_tm, K false)); + +in fn variable_order => + let + +(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible. *) +(* Also deals with "const * const", but both terms must involve powers of *) +(* the same variable, or both be constants, or behaviour may be incorrect. *) + + fun powvar_mul_conv tm = + let + val (l,r) = dest_mul tm + in if is_semiring_constant l andalso is_semiring_constant r + then semiring_mul_conv tm + else + ((let + val (lx,ln) = dest_pow l + in + ((let val (rx,rn) = dest_pow r + val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29 + val (tm1,tm2) = Thm.dest_comb(concl th1) in + transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end) + handle CTERM _ => + (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31 + val (tm1,tm2) = Thm.dest_comb(concl th1) in + transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end) + handle CTERM _ => + ((let val (rx,rn) = dest_pow r + val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30 + val (tm1,tm2) = Thm.dest_comb(concl th1) in + transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end) + handle CTERM _ => inst_thm [(cx,l)] pthm_32 + +)) + end; + +(* Remove "1 * m" from a monomial, and just leave m. *) + + fun monomial_deone th = + (let val (l,r) = dest_mul(concl th) in + if l aconvc one_tm + then transitive th (inst_thm [(ca,r)] pthm_13) else th end) + handle CTERM _ => th; + +(* Conversion for "(monomial)^n", where n is a numeral. *) + + val monomial_pow_conv = + let + fun monomial_pow tm bod ntm = + if not(is_comb bod) + then reflexive tm + else + if is_semiring_constant bod + then semiring_pow_conv tm + else + let + val (lopr,r) = Thm.dest_comb bod + in if not(is_comb lopr) + then reflexive tm + else + let + val (opr,l) = Thm.dest_comb lopr + in + if opr aconvc pow_tm andalso is_numeral r + then + let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34 + val (l,r) = Thm.dest_comb(concl th1) + in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r)) + end + else + if opr aconvc mul_tm + then + let + val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33 + val (xy,z) = Thm.dest_comb(concl th1) + val (x,y) = Thm.dest_comb xy + val thl = monomial_pow y l ntm + val thr = monomial_pow z r ntm + in transitive th1 (combination (Drule.arg_cong_rule x thl) thr) + end + else reflexive tm + end + end + in fn tm => + let + val (lopr,r) = Thm.dest_comb tm + val (opr,l) = Thm.dest_comb lopr + in if not (opr aconvc pow_tm) orelse not(is_numeral r) + then raise CTERM ("monomial_pow_conv", [tm]) + else if r aconvc zeron_tm + then inst_thm [(cx,l)] pthm_35 + else if r aconvc onen_tm + then inst_thm [(cx,l)] pthm_36 + else monomial_deone(monomial_pow tm l r) + end + end; + +(* Multiplication of canonical monomials. *) + val monomial_mul_conv = + let + fun powvar tm = + if is_semiring_constant tm then one_tm + else + ((let val (lopr,r) = Thm.dest_comb tm + val (opr,l) = Thm.dest_comb lopr + in if opr aconvc pow_tm andalso is_numeral r then l + else raise CTERM ("monomial_mul_conv",[tm]) end) + handle CTERM _ => tm) (* FIXME !? *) + fun vorder x y = + if x aconvc y then 0 + else + if x aconvc one_tm then ~1 + else if y aconvc one_tm then 1 + else if variable_order x y then ~1 else 1 + fun monomial_mul tm l r = + ((let val (lx,ly) = dest_mul l val vl = powvar lx + in + ((let + val (rx,ry) = dest_mul r + val vr = powvar rx + val ord = vorder vl vr + in + if ord = 0 + then + let + val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15 + val (tm1,tm2) = Thm.dest_comb(concl th1) + val (tm3,tm4) = Thm.dest_comb tm1 + val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2 + val th3 = transitive th1 th2 + val (tm5,tm6) = Thm.dest_comb(concl th3) + val (tm7,tm8) = Thm.dest_comb tm6 + val th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8 + in transitive th3 (Drule.arg_cong_rule tm5 th4) + end + else + let val th0 = if ord < 0 then pthm_16 else pthm_17 + val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0 + val (tm1,tm2) = Thm.dest_comb(concl th1) + val (tm3,tm4) = Thm.dest_comb tm2 + in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) + end + end) + handle CTERM _ => + (let val vr = powvar r val ord = vorder vl vr + in + if ord = 0 then + let + val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18 + val (tm1,tm2) = Thm.dest_comb(concl th1) + val (tm3,tm4) = Thm.dest_comb tm1 + val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2 + in transitive th1 th2 + end + else + if ord < 0 then + let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19 + val (tm1,tm2) = Thm.dest_comb(concl th1) + val (tm3,tm4) = Thm.dest_comb tm2 + in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) + end + else inst_thm [(ca,l),(cb,r)] pthm_09 + end)) end) + handle CTERM _ => + (let val vl = powvar l in + ((let + val (rx,ry) = dest_mul r + val vr = powvar rx + val ord = vorder vl vr + in if ord = 0 then + let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21 + val (tm1,tm2) = Thm.dest_comb(concl th1) + val (tm3,tm4) = Thm.dest_comb tm1 + in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2) + end + else if ord > 0 then + let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22 + val (tm1,tm2) = Thm.dest_comb(concl th1) + val (tm3,tm4) = Thm.dest_comb tm2 + in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) + end + else reflexive tm + end) + handle CTERM _ => + (let val vr = powvar r + val ord = vorder vl vr + in if ord = 0 then powvar_mul_conv tm + else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09 + else reflexive tm + end)) end)) + in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r) + end + end; +(* Multiplication by monomial of a polynomial. *) + + val polynomial_monomial_mul_conv = + let + fun pmm_conv tm = + let val (l,r) = dest_mul tm + in + ((let val (y,z) = dest_add r + val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37 + val (tm1,tm2) = Thm.dest_comb(concl th1) + val (tm3,tm4) = Thm.dest_comb tm1 + val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2) + in transitive th1 th2 + end) + handle CTERM _ => monomial_mul_conv tm) + end + in pmm_conv + end; + +(* Addition of two monomials identical except for constant multiples. *) + +fun monomial_add_conv tm = + let val (l,r) = dest_add tm + in if is_semiring_constant l andalso is_semiring_constant r + then semiring_add_conv tm + else + let val th1 = + if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l) + then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then + inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02 + else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03 + else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) + then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04 + else inst_thm [(cm,r)] pthm_05 + val (tm1,tm2) = Thm.dest_comb(concl th1) + val (tm3,tm4) = Thm.dest_comb tm1 + val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4) + val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2) + val tm5 = concl th3 + in + if (Thm.dest_arg1 tm5) aconvc zero_tm + then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11) + else monomial_deone th3 + end + end; + +(* Ordering on monomials. *) + +fun striplist dest = + let fun strip x acc = + ((let val (l,r) = dest x in + strip l (strip r acc) end) + handle CTERM _ => x::acc) (* FIXME !? *) + in fn x => strip x [] + end; + + +fun powervars tm = + let val ptms = striplist dest_mul tm + in if is_semiring_constant (hd ptms) then tl ptms else ptms + end; +val num_0 = 0; +val num_1 = 1; +fun dest_varpow tm = + ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end) + handle CTERM _ => + (tm,(if is_semiring_constant tm then num_0 else num_1))); + +val morder = + let fun lexorder l1 l2 = + case (l1,l2) of + ([],[]) => 0 + | (vps,[]) => ~1 + | ([],vps) => 1 + | (((x1,n1)::vs1),((x2,n2)::vs2)) => + if variable_order x1 x2 then 1 + else if variable_order x2 x1 then ~1 + else if n1 < n2 then ~1 + else if n2 < n1 then 1 + else lexorder vs1 vs2 + in fn tm1 => fn tm2 => + let val vdegs1 = map dest_varpow (powervars tm1) + val vdegs2 = map dest_varpow (powervars tm2) + val deg1 = fold (Integer.add o snd) vdegs1 num_0 + val deg2 = fold (Integer.add o snd) vdegs2 num_0 + in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1 + else lexorder vdegs1 vdegs2 + end + end; + +(* Addition of two polynomials. *) + +val polynomial_add_conv = + let + fun dezero_rule th = + let + val tm = concl th + in + if not(is_add tm) then th else + let val (lopr,r) = Thm.dest_comb tm + val l = Thm.dest_arg lopr + in + if l aconvc zero_tm + then transitive th (inst_thm [(ca,r)] pthm_07) else + if r aconvc zero_tm + then transitive th (inst_thm [(ca,l)] pthm_08) else th + end + end + fun padd tm = + let + val (l,r) = dest_add tm + in + if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07 + else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08 + else + if is_add l + then + let val (a,b) = dest_add l + in + if is_add r then + let val (c,d) = dest_add r + val ord = morder a c + in + if ord = 0 then + let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23 + val (tm1,tm2) = Thm.dest_comb(concl th1) + val (tm3,tm4) = Thm.dest_comb tm1 + val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4) + in dezero_rule (transitive th1 (combination th2 (padd tm2))) + end + else (* ord <> 0*) + let val th1 = + if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24 + else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25 + val (tm1,tm2) = Thm.dest_comb(concl th1) + in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) + end + end + else (* not (is_add r)*) + let val ord = morder a r + in + if ord = 0 then + let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26 + val (tm1,tm2) = Thm.dest_comb(concl th1) + val (tm3,tm4) = Thm.dest_comb tm1 + val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2 + in dezero_rule (transitive th1 th2) + end + else (* ord <> 0*) + if ord > 0 then + let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24 + val (tm1,tm2) = Thm.dest_comb(concl th1) + in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) + end + else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27) + end + end + else (* not (is_add l)*) + if is_add r then + let val (c,d) = dest_add r + val ord = morder l c + in + if ord = 0 then + let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28 + val (tm1,tm2) = Thm.dest_comb(concl th1) + val (tm3,tm4) = Thm.dest_comb tm1 + val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2 + in dezero_rule (transitive th1 th2) + end + else + if ord > 0 then reflexive tm + else + let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25 + val (tm1,tm2) = Thm.dest_comb(concl th1) + in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) + end + end + else + let val ord = morder l r + in + if ord = 0 then monomial_add_conv tm + else if ord > 0 then dezero_rule(reflexive tm) + else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27) + end + end + in padd + end; + +(* Multiplication of two polynomials. *) + +val polynomial_mul_conv = + let + fun pmul tm = + let val (l,r) = dest_mul tm + in + if not(is_add l) then polynomial_monomial_mul_conv tm + else + if not(is_add r) then + let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09 + in transitive th1 (polynomial_monomial_mul_conv(concl th1)) + end + else + let val (a,b) = dest_add l + val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10 + val (tm1,tm2) = Thm.dest_comb(concl th1) + val (tm3,tm4) = Thm.dest_comb tm1 + val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4) + val th3 = transitive th1 (combination th2 (pmul tm2)) + in transitive th3 (polynomial_add_conv (concl th3)) + end + end + in fn tm => + let val (l,r) = dest_mul tm + in + if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11 + else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12 + else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13 + else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14 + else pmul tm + end + end; + +(* Power of polynomial (optimized for the monomial and trivial cases). *) + +fun num_conv n = + nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1))) + |> Thm.symmetric; + + +val polynomial_pow_conv = + let + fun ppow tm = + let val (l,n) = dest_pow tm + in + if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35 + else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36 + else + let val th1 = num_conv n + val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38 + val (tm1,tm2) = Thm.dest_comb(concl th2) + val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2)) + val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3 + in transitive th4 (polynomial_mul_conv (concl th4)) + end + end + in fn tm => + if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm + end; + +(* Negation. *) + +fun polynomial_neg_conv tm = + let val (l,r) = Thm.dest_comb tm in + if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else + let val th1 = inst_thm [(cx',r)] neg_mul + val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1)) + in transitive th2 (polynomial_monomial_mul_conv (concl th2)) + end + end; + + +(* Subtraction. *) +fun polynomial_sub_conv tm = + let val (l,r) = dest_sub tm + val th1 = inst_thm [(cx',l),(cy',r)] sub_add + val (tm1,tm2) = Thm.dest_comb(concl th1) + val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2) + in transitive th1 (transitive th2 (polynomial_add_conv (concl th2))) + end; + +(* Conversion from HOL term. *) + +fun polynomial_conv tm = + if is_semiring_constant tm then semiring_add_conv tm + else if not(is_comb tm) then reflexive tm + else + let val (lopr,r) = Thm.dest_comb tm + in if lopr aconvc neg_tm then + let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) + in transitive th1 (polynomial_neg_conv (concl th1)) + end + else if lopr aconvc inverse_tm then + let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) + in transitive th1 (semiring_mul_conv (concl th1)) + end + else + if not(is_comb lopr) then reflexive tm + else + let val (opr,l) = Thm.dest_comb lopr + in if opr aconvc pow_tm andalso is_numeral r + then + let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r + in transitive th1 (polynomial_pow_conv (concl th1)) + end + else if opr aconvc divide_tm + then + let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) + (polynomial_conv r) + val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv) + (Thm.rhs_of th1) + in transitive th1 th2 + end + else + if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm + then + let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r) + val f = if opr aconvc add_tm then polynomial_add_conv + else if opr aconvc mul_tm then polynomial_mul_conv + else polynomial_sub_conv + in transitive th1 (f (concl th1)) + end + else reflexive tm + end + end; + in + {main = polynomial_conv, + add = polynomial_add_conv, + mul = polynomial_mul_conv, + pow = polynomial_pow_conv, + neg = polynomial_neg_conv, + sub = polynomial_sub_conv} + end +end; + +val nat_exp_ss = + HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps}) + addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]; + +fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS; + + +(* various normalizing conversions *) + +fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, + {conv, dest_const, mk_const, is_const}) ord = + let + val pow_conv = + Conv.arg_conv (Simplifier.rewrite nat_exp_ss) + then_conv Simplifier.rewrite + (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34]) + then_conv conv ctxt + val dat = (is_const, conv ctxt, conv ctxt, pow_conv) + in semiring_normalizers_conv vars semiring ring field dat ord end; + +fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord = + #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); + +fun semiring_normalize_wrapper ctxt data = + semiring_normalize_ord_wrapper ctxt data simple_cterm_ord; + +fun semiring_normalize_ord_conv ctxt ord tm = + (case match ctxt tm of + NONE => reflexive tm + | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm); + +fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord; + + +(** Isar setup **) + +local + +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); +fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K (); +fun keyword3 k1 k2 k3 = + Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K (); + +val opsN = "ops"; +val rulesN = "rules"; + +val normN = "norm"; +val constN = "const"; +val delN = "del"; + +val any_keyword = + keyword2 semiringN opsN || keyword2 semiringN rulesN || + keyword2 ringN opsN || keyword2 ringN rulesN || + keyword2 fieldN opsN || keyword2 fieldN rulesN || + keyword2 idomN rulesN || keyword2 idealN rulesN; + +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; +val terms = thms >> map Drule.dest_term; + +fun optional scan = Scan.optional scan []; + +in + +val setup = + Attrib.setup @{binding normalizer} + (Scan.lift (Args.$$$ delN >> K del) || + ((keyword2 semiringN opsN |-- terms) -- + (keyword2 semiringN rulesN |-- thms)) -- + (optional (keyword2 ringN opsN |-- terms) -- + optional (keyword2 ringN rulesN |-- thms)) -- + (optional (keyword2 fieldN opsN |-- terms) -- + optional (keyword2 fieldN rulesN |-- thms)) -- + optional (keyword2 idomN rulesN |-- thms) -- + optional (keyword2 idealN rulesN |-- thms) + >> (fn ((((sr, r), f), id), idl) => + add {semiring = sr, ring = r, field = f, idom = id, ideal = idl})) + "semiring normalizer data"; + +end; + +end; diff -r dce592144219 -r 5ce217fc769a src/HOL/ex/Groebner_Examples.thy --- a/src/HOL/ex/Groebner_Examples.thy Fri May 07 23:44:10 2010 +0200 +++ b/src/HOL/ex/Groebner_Examples.thy Sat May 08 17:15:50 2010 +0200 @@ -14,21 +14,21 @@ fixes x :: int shows "x ^ 3 = x ^ 3" apply (tactic {* ALLGOALS (CONVERSION - (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *}) + (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *}) by (rule refl) lemma fixes x :: int shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\ + (80 * x + 32))))" apply (tactic {* ALLGOALS (CONVERSION - (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *}) + (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *}) by (rule refl) schematic_lemma fixes x :: int shows "(x - (-2))^5 * (y - 78) ^ 8 = ?X" apply (tactic {* ALLGOALS (CONVERSION - (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *}) + (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *}) by (rule refl) lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"