src/HOL/Groebner_Basis.thy
changeset 36712 2f4c318861b3
parent 36702 b455ebd63799
child 36714 ae84ddf03c58
     1.1 --- a/src/HOL/Groebner_Basis.thy	Thu May 06 17:09:18 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu May 06 17:55:11 2010 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  setup Normalizer.setup
     1.6  
     1.7 -locale gb_semiring =
     1.8 +locale normalizing_semiring =
     1.9    fixes add mul pwr r0 r1
    1.10    assumes add_a:"(add x (add y z) = add (add x y) z)"
    1.11      and add_c: "add x y = add y x" and add_0:"add r0 x = x"
    1.12 @@ -56,9 +56,6 @@
    1.13    thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc)
    1.14  qed
    1.15  
    1.16 -
    1.17 -subsubsection {* Declaring the abstract theory *}
    1.18 -
    1.19  lemma semiring_ops:
    1.20    shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
    1.21      and "TERM r0" and "TERM r1" .
    1.22 @@ -153,41 +150,31 @@
    1.23  qed
    1.24  
    1.25  
    1.26 -lemmas gb_semiring_axioms' =
    1.27 -  gb_semiring_axioms [normalizer
    1.28 +lemmas normalizing_semiring_axioms' =
    1.29 +  normalizing_semiring_axioms [normalizer
    1.30      semiring ops: semiring_ops
    1.31      semiring rules: semiring_rules]
    1.32  
    1.33  end
    1.34  
    1.35 -interpretation class_semiring: gb_semiring
    1.36 -    "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1"
    1.37 -  proof qed (auto simp add: algebra_simps)
    1.38 -
    1.39 -lemmas nat_arith =
    1.40 -  add_nat_number_of
    1.41 -  diff_nat_number_of
    1.42 -  mult_nat_number_of
    1.43 -  eq_nat_number_of
    1.44 -  less_nat_number_of
    1.45 +sublocale comm_semiring_1
    1.46 +  < normalizing!: normalizing_semiring plus times power zero one
    1.47 +proof
    1.48 +qed (simp_all add: algebra_simps)
    1.49  
    1.50  lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
    1.51    by simp
    1.52  
    1.53 -lemmas comp_arith =
    1.54 +lemmas semiring_norm =
    1.55    Let_def arith_simps nat_arith rel_simps neg_simps if_False
    1.56    if_True add_0 add_Suc add_number_of_left mult_number_of_left
    1.57    numeral_1_eq_1[symmetric] Suc_eq_plus1
    1.58    numeral_0_eq_0[symmetric] numerals[symmetric]
    1.59    iszero_simps not_iszero_Numeral1
    1.60  
    1.61 -lemmas semiring_norm = comp_arith
    1.62 -
    1.63  ML {*
    1.64  local
    1.65  
    1.66 -open Conv;
    1.67 -
    1.68  fun numeral_is_const ct = can HOLogic.dest_number (Thm.term_of ct);
    1.69  
    1.70  fun int_of_rat x =
    1.71 @@ -201,7 +188,7 @@
    1.72  
    1.73  in
    1.74  
    1.75 -fun normalizer_funs key =
    1.76 +fun normalizer_funs' key =
    1.77    Normalizer.funs key
    1.78     {is_const = fn phi => numeral_is_const,
    1.79      dest_const = fn phi => fn ct =>
    1.80 @@ -214,9 +201,9 @@
    1.81  end
    1.82  *}
    1.83  
    1.84 -declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms'} *}
    1.85 +declaration {* normalizer_funs' @{thm normalizing.normalizing_semiring_axioms'} *}
    1.86  
    1.87 -locale gb_ring = gb_semiring +
    1.88 +locale normalizing_ring = normalizing_semiring +
    1.89    fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.90      and neg :: "'a \<Rightarrow> 'a"
    1.91    assumes neg_mul: "neg x = mul (neg r1) x"
    1.92 @@ -227,8 +214,8 @@
    1.93  
    1.94  lemmas ring_rules = neg_mul sub_add
    1.95  
    1.96 -lemmas gb_ring_axioms' =
    1.97 -  gb_ring_axioms [normalizer
    1.98 +lemmas normalizing_ring_axioms' =
    1.99 +  normalizing_ring_axioms [normalizer
   1.100      semiring ops: semiring_ops
   1.101      semiring rules: semiring_rules
   1.102      ring ops: ring_ops
   1.103 @@ -236,15 +223,14 @@
   1.104  
   1.105  end
   1.106  
   1.107 -
   1.108 -interpretation class_ring: gb_ring "op +" "op *" "op ^"
   1.109 -    "0::'a::{comm_semiring_1,number_ring}" 1 "op -" "uminus"
   1.110 -  proof qed simp_all
   1.111 +(*FIXME add class*)
   1.112 +interpretation normalizing!: normalizing_ring plus times power
   1.113 +  "0::'a::{comm_semiring_1,number_ring}" 1 minus uminus proof
   1.114 +qed simp_all
   1.115  
   1.116 +declaration {* normalizer_funs' @{thm normalizing.normalizing_ring_axioms'} *}
   1.117  
   1.118 -declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}
   1.119 -
   1.120 -locale gb_field = gb_ring +
   1.121 +locale normalizing_field = normalizing_ring +
   1.122    fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.123      and inverse:: "'a \<Rightarrow> 'a"
   1.124    assumes divide_inverse: "divide x y = mul x (inverse y)"
   1.125 @@ -255,8 +241,8 @@
   1.126  
   1.127  lemmas field_rules = divide_inverse inverse_divide
   1.128  
   1.129 -lemmas gb_field_axioms' =
   1.130 -  gb_field_axioms [normalizer
   1.131 +lemmas normalizing_field_axioms' =
   1.132 +  normalizing_field_axioms [normalizer
   1.133      semiring ops: semiring_ops
   1.134      semiring rules: semiring_rules
   1.135      ring ops: ring_ops
   1.136 @@ -266,10 +252,7 @@
   1.137  
   1.138  end
   1.139  
   1.140 -
   1.141 -subsection {* Groebner Bases *}
   1.142 -
   1.143 -locale semiringb = gb_semiring +
   1.144 +locale normalizing_semiring_cancel = normalizing_semiring +
   1.145    assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z"
   1.146    and add_mul_solve: "add (mul w y) (mul x z) =
   1.147      add (mul w z) (mul x y) \<longleftrightarrow> w = x \<or> y = z"
   1.148 @@ -301,22 +284,23 @@
   1.149    thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
   1.150  qed
   1.151  
   1.152 -declare gb_semiring_axioms' [normalizer del]
   1.153 +declare normalizing_semiring_axioms' [normalizer del]
   1.154  
   1.155 -lemmas semiringb_axioms' = semiringb_axioms [normalizer
   1.156 -  semiring ops: semiring_ops
   1.157 -  semiring rules: semiring_rules
   1.158 -  idom rules: noteq_reduce add_scale_eq_noteq]
   1.159 +lemmas normalizing_semiring_cancel_axioms' =
   1.160 +  normalizing_semiring_cancel_axioms [normalizer
   1.161 +    semiring ops: semiring_ops
   1.162 +    semiring rules: semiring_rules
   1.163 +    idom rules: noteq_reduce add_scale_eq_noteq]
   1.164  
   1.165  end
   1.166  
   1.167 -locale ringb = semiringb + gb_ring + 
   1.168 +locale normalizing_ring_cancel = normalizing_semiring_cancel + normalizing_ring + 
   1.169    assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
   1.170  begin
   1.171  
   1.172 -declare gb_ring_axioms' [normalizer del]
   1.173 +declare normalizing_ring_axioms' [normalizer del]
   1.174  
   1.175 -lemmas ringb_axioms' = ringb_axioms [normalizer
   1.176 +lemmas normalizing_ring_cancel_axioms' = normalizing_ring_cancel_axioms [normalizer
   1.177    semiring ops: semiring_ops
   1.178    semiring rules: semiring_rules
   1.179    ring ops: ring_ops
   1.180 @@ -326,17 +310,16 @@
   1.181  
   1.182  end
   1.183  
   1.184 -
   1.185 -lemma no_zero_divirors_neq0:
   1.186 -  assumes az: "(a::'a::no_zero_divisors) \<noteq> 0"
   1.187 -    and ab: "a*b = 0" shows "b = 0"
   1.188 -proof -
   1.189 -  { assume bz: "b \<noteq> 0"
   1.190 -    from no_zero_divisors [OF az bz] ab have False by blast }
   1.191 -  thus "b = 0" by blast
   1.192 +lemma (in no_zero_divisors) prod_eq_zero_eq_zero:
   1.193 +  assumes "a * b = 0" and "a \<noteq> 0"
   1.194 +  shows "b = 0"
   1.195 +proof (rule classical)
   1.196 +  assume "b \<noteq> 0" with `a \<noteq> 0` no_zero_divisors have "a * b \<noteq> 0" by blast
   1.197 +  with `a * b = 0` show ?thesis by simp
   1.198  qed
   1.199  
   1.200 -interpretation class_ringb: ringb
   1.201 +(*FIXME introduce class*)
   1.202 +interpretation normalizing!: normalizing_ring_cancel
   1.203    "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus"
   1.204  proof(unfold_locales, simp add: algebra_simps, auto)
   1.205    fix w x y z ::"'a::{idom,number_ring}"
   1.206 @@ -345,14 +328,14 @@
   1.207    from p have "w * y + x* z - w*z - x*y = 0" by simp
   1.208    hence "w* (y - z) - x * (y - z) = 0" by (simp add: algebra_simps)
   1.209    hence "(y - z) * (w - x) = 0" by (simp add: algebra_simps)
   1.210 -  with  no_zero_divirors_neq0 [OF ynz']
   1.211 +  with  prod_eq_zero_eq_zero [OF _ ynz']
   1.212    have "w - x = 0" by blast
   1.213    thus "w = x"  by simp
   1.214  qed
   1.215  
   1.216 -declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
   1.217 +declaration {* normalizer_funs' @{thm normalizing.normalizing_ring_cancel_axioms'} *}
   1.218  
   1.219 -interpretation natgb: semiringb
   1.220 +interpretation normalizing_nat!: normalizing_semiring_cancel
   1.221    "op +" "op *" "op ^" "0::nat" "1"
   1.222  proof (unfold_locales, simp add: algebra_simps)
   1.223    fix w x y z ::"nat"
   1.224 @@ -374,14 +357,14 @@
   1.225    thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
   1.226  qed
   1.227  
   1.228 -declaration {* normalizer_funs @{thm natgb.semiringb_axioms'} *}
   1.229 +declaration {* normalizer_funs' @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *}
   1.230  
   1.231 -locale fieldgb = ringb + gb_field
   1.232 +locale normalizing_field_cancel = normalizing_ring_cancel + normalizing_field
   1.233  begin
   1.234  
   1.235 -declare gb_field_axioms' [normalizer del]
   1.236 +declare normalizing_field_axioms' [normalizer del]
   1.237  
   1.238 -lemmas fieldgb_axioms' = fieldgb_axioms [normalizer
   1.239 +lemmas normalizing_field_cancel_axioms' = normalizing_field_cancel_axioms [normalizer
   1.240    semiring ops: semiring_ops
   1.241    semiring rules: semiring_rules
   1.242    ring ops: ring_ops
   1.243 @@ -393,83 +376,10 @@
   1.244  
   1.245  end
   1.246  
   1.247 -
   1.248 -lemmas bool_simps = simp_thms(1-34)
   1.249 -lemma dnf:
   1.250 -    "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
   1.251 -    "(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"
   1.252 -  by blast+
   1.253 -
   1.254 -lemmas weak_dnf_simps = dnf bool_simps
   1.255 -
   1.256 -lemma nnf_simps:
   1.257 -    "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
   1.258 -    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
   1.259 -  by blast+
   1.260 -
   1.261 -lemma PFalse:
   1.262 -    "P \<equiv> False \<Longrightarrow> \<not> P"
   1.263 -    "\<not> P \<Longrightarrow> (P \<equiv> False)"
   1.264 -  by auto
   1.265 -
   1.266 -ML {*
   1.267 -structure Algebra_Simplification = Named_Thms(
   1.268 -  val name = "algebra"
   1.269 -  val description = "pre-simplification rules for algebraic methods"
   1.270 -)
   1.271 -*}
   1.272 -
   1.273 -setup Algebra_Simplification.setup
   1.274 -
   1.275 -use "Tools/Groebner_Basis/groebner.ML"
   1.276 -
   1.277 -method_setup algebra =
   1.278 -{*
   1.279 -let
   1.280 - fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   1.281 - val addN = "add"
   1.282 - val delN = "del"
   1.283 - val any_keyword = keyword addN || keyword delN
   1.284 - val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   1.285 -in
   1.286 -  ((Scan.optional (keyword addN |-- thms) []) -- 
   1.287 -   (Scan.optional (keyword delN |-- thms) [])) >>
   1.288 -  (fn (add_ths, del_ths) => fn ctxt =>
   1.289 -       SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
   1.290 -end
   1.291 -*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
   1.292 -declare dvd_def[algebra]
   1.293 -declare dvd_eq_mod_eq_0[symmetric, algebra]
   1.294 -declare mod_div_trivial[algebra]
   1.295 -declare mod_mod_trivial[algebra]
   1.296 -declare conjunct1[OF DIVISION_BY_ZERO, algebra]
   1.297 -declare conjunct2[OF DIVISION_BY_ZERO, algebra]
   1.298 -declare zmod_zdiv_equality[symmetric,algebra]
   1.299 -declare zdiv_zmod_equality[symmetric, algebra]
   1.300 -declare zdiv_zminus_zminus[algebra]
   1.301 -declare zmod_zminus_zminus[algebra]
   1.302 -declare zdiv_zminus2[algebra]
   1.303 -declare zmod_zminus2[algebra]
   1.304 -declare zdiv_zero[algebra]
   1.305 -declare zmod_zero[algebra]
   1.306 -declare mod_by_1[algebra]
   1.307 -declare div_by_1[algebra]
   1.308 -declare zmod_minus1_right[algebra]
   1.309 -declare zdiv_minus1_right[algebra]
   1.310 -declare mod_div_trivial[algebra]
   1.311 -declare mod_mod_trivial[algebra]
   1.312 -declare mod_mult_self2_is_0[algebra]
   1.313 -declare mod_mult_self1_is_0[algebra]
   1.314 -declare zmod_eq_0_iff[algebra]
   1.315 -declare dvd_0_left_iff[algebra]
   1.316 -declare zdvd1_eq[algebra]
   1.317 -declare zmod_eq_dvd_iff[algebra]
   1.318 -declare nat_mod_eq_iff[algebra]
   1.319 -
   1.320 -subsection{* Groebner Bases for fields *}
   1.321 -
   1.322 -interpretation class_fieldgb:
   1.323 -  fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
   1.324 +(*FIXME introduce class*)
   1.325 +interpretation normalizing!: normalizing_field_cancel "op +" "op *" "op ^"
   1.326 +  "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse"
   1.327 +apply (unfold_locales) by (simp_all add: divide_inverse)
   1.328  
   1.329  lemma divide_Numeral1: "(x::'a::{field, number_ring}) / Numeral1 = x" by simp
   1.330  lemma divide_Numeral0: "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0"
   1.331 @@ -477,9 +387,9 @@
   1.332  lemma mult_frac_frac: "((x::'a::field_inverse_zero) / y) * (z / w) = (x*z) / (y*w)"
   1.333    by simp
   1.334  lemma mult_frac_num: "((x::'a::field_inverse_zero) / y) * z  = (x*z) / y"
   1.335 -  by simp
   1.336 +  by (fact times_divide_eq_left)
   1.337  lemma mult_num_frac: "((x::'a::field_inverse_zero) / y) * z  = (x*z) / y"
   1.338 -  by simp
   1.339 +  by (fact times_divide_eq_left)
   1.340  
   1.341  lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
   1.342  
   1.343 @@ -488,13 +398,7 @@
   1.344  lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::field_inverse_zero) / y = (x + z*y) / y"
   1.345    by (simp add: add_divide_distrib)
   1.346  
   1.347 -ML {*
   1.348 -let open Conv
   1.349 -in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) (@{thm field_divide_inverse} RS sym)
   1.350 -end
   1.351 -*}
   1.352 -
   1.353 -ML{* 
   1.354 +ML {* 
   1.355  local
   1.356   val zr = @{cpat "0"}
   1.357   val zT = ctyp_of_term zr
   1.358 @@ -619,10 +523,6 @@
   1.359               @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
   1.360               name = "ord_frac_simproc", proc = proc3, identifier = []}
   1.361  
   1.362 -local
   1.363 -open Conv
   1.364 -in
   1.365 -
   1.366  val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
   1.367             @{thm "divide_Numeral1"},
   1.368             @{thm "divide_zero"}, @{thm "divide_Numeral0"},
   1.369 @@ -633,11 +533,13 @@
   1.370             @{thm "diff_def"}, @{thm "minus_divide_left"},
   1.371             @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
   1.372             @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 
   1.373 -           fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))   
   1.374 +           Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute}))))   
   1.375             (@{thm field_divide_inverse} RS sym)]
   1.376  
   1.377 -val comp_conv = (Simplifier.rewrite
   1.378 -(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
   1.379 +in
   1.380 +
   1.381 +val field_comp_conv = (Simplifier.rewrite
   1.382 +(HOL_basic_ss addsimps @{thms "semiring_norm"}
   1.383                addsimps ths addsimps @{thms simp_thms}
   1.384                addsimprocs Numeral_Simprocs.field_cancel_numeral_factors
   1.385                 addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
   1.386 @@ -645,7 +547,12 @@
   1.387                  addcongs [@{thm "if_weak_cong"}]))
   1.388  then_conv (Simplifier.rewrite (HOL_basic_ss addsimps
   1.389    [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}))
   1.390 +
   1.391  end
   1.392 +*}
   1.393 +
   1.394 +declaration {*
   1.395 +let
   1.396  
   1.397  fun numeral_is_const ct =
   1.398    case term_of ct of
   1.399 @@ -672,16 +579,93 @@
   1.400    end
   1.401  
   1.402  in
   1.403 - val field_comp_conv = comp_conv;
   1.404 - val fieldgb_declaration = 
   1.405 -  Normalizer.funs @{thm class_fieldgb.fieldgb_axioms'}
   1.406 + 
   1.407 +  Normalizer.funs @{thm normalizing.normalizing_field_cancel_axioms'}
   1.408     {is_const = K numeral_is_const,
   1.409      dest_const = K dest_const,
   1.410      mk_const = mk_const,
   1.411 -    conv = K (K comp_conv)}
   1.412 -end;
   1.413 +    conv = K (K field_comp_conv)}
   1.414 +
   1.415 +end
   1.416 +*}
   1.417 +
   1.418 +lemmas comp_arith = semiring_norm (*FIXME*)
   1.419 +
   1.420 +
   1.421 +subsection {* Groebner Bases *}
   1.422 +
   1.423 +lemmas bool_simps = simp_thms(1-34)
   1.424 +
   1.425 +lemma dnf:
   1.426 +    "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
   1.427 +    "(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"
   1.428 +  by blast+
   1.429 +
   1.430 +lemmas weak_dnf_simps = dnf bool_simps
   1.431 +
   1.432 +lemma nnf_simps:
   1.433 +    "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
   1.434 +    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
   1.435 +  by blast+
   1.436 +
   1.437 +lemma PFalse:
   1.438 +    "P \<equiv> False \<Longrightarrow> \<not> P"
   1.439 +    "\<not> P \<Longrightarrow> (P \<equiv> False)"
   1.440 +  by auto
   1.441 +
   1.442 +ML {*
   1.443 +structure Algebra_Simplification = Named_Thms(
   1.444 +  val name = "algebra"
   1.445 +  val description = "pre-simplification rules for algebraic methods"
   1.446 +)
   1.447  *}
   1.448  
   1.449 -declaration fieldgb_declaration
   1.450 +setup Algebra_Simplification.setup
   1.451 +
   1.452 +declare dvd_def[algebra]
   1.453 +declare dvd_eq_mod_eq_0[symmetric, algebra]
   1.454 +declare mod_div_trivial[algebra]
   1.455 +declare mod_mod_trivial[algebra]
   1.456 +declare conjunct1[OF DIVISION_BY_ZERO, algebra]
   1.457 +declare conjunct2[OF DIVISION_BY_ZERO, algebra]
   1.458 +declare zmod_zdiv_equality[symmetric,algebra]
   1.459 +declare zdiv_zmod_equality[symmetric, algebra]
   1.460 +declare zdiv_zminus_zminus[algebra]
   1.461 +declare zmod_zminus_zminus[algebra]
   1.462 +declare zdiv_zminus2[algebra]
   1.463 +declare zmod_zminus2[algebra]
   1.464 +declare zdiv_zero[algebra]
   1.465 +declare zmod_zero[algebra]
   1.466 +declare mod_by_1[algebra]
   1.467 +declare div_by_1[algebra]
   1.468 +declare zmod_minus1_right[algebra]
   1.469 +declare zdiv_minus1_right[algebra]
   1.470 +declare mod_div_trivial[algebra]
   1.471 +declare mod_mod_trivial[algebra]
   1.472 +declare mod_mult_self2_is_0[algebra]
   1.473 +declare mod_mult_self1_is_0[algebra]
   1.474 +declare zmod_eq_0_iff[algebra]
   1.475 +declare dvd_0_left_iff[algebra]
   1.476 +declare zdvd1_eq[algebra]
   1.477 +declare zmod_eq_dvd_iff[algebra]
   1.478 +declare nat_mod_eq_iff[algebra]
   1.479 +
   1.480 +use "Tools/Groebner_Basis/groebner.ML"
   1.481 +
   1.482 +method_setup algebra =
   1.483 +{*
   1.484 +let
   1.485 + fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   1.486 + val addN = "add"
   1.487 + val delN = "del"
   1.488 + val any_keyword = keyword addN || keyword delN
   1.489 + val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   1.490 +in
   1.491 +  ((Scan.optional (keyword addN |-- thms) []) -- 
   1.492 +   (Scan.optional (keyword delN |-- thms) [])) >>
   1.493 +  (fn (add_ths, del_ths) => fn ctxt =>
   1.494 +       SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
   1.495 +end
   1.496 +*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
   1.497  
   1.498  end