src/HOL/Groebner_Basis.thy
changeset 25250 b3a485b98963
parent 23573 d85a277f90fd
child 26086 3c243098b64a
     1.1 --- a/src/HOL/Groebner_Basis.thy	Wed Oct 31 12:19:33 2007 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Oct 31 12:19:35 2007 +0100
     1.3 @@ -301,6 +301,12 @@
     1.4    thus "False" using add_mul_solve nz cnd by simp
     1.5  qed
     1.6  
     1.7 +lemma add_r0_iff: " x = add x a \<longleftrightarrow> a = r0"
     1.8 +proof-
     1.9 +  have "a = r0 \<longleftrightarrow> add x a = add x r0" by (simp add: add_cancel)
    1.10 +  thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
    1.11 +qed
    1.12 +
    1.13  declare "axioms" [normalizer del]
    1.14  
    1.15  lemma "axioms" [normalizer
    1.16 @@ -311,7 +317,8 @@
    1.17  
    1.18  end
    1.19  
    1.20 -locale ringb = semiringb + gb_ring
    1.21 +locale ringb = semiringb + gb_ring + 
    1.22 +  assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
    1.23  begin
    1.24  
    1.25  declare "axioms" [normalizer del]
    1.26 @@ -321,11 +328,13 @@
    1.27    semiring rules: semiring_rules
    1.28    ring ops: ring_ops
    1.29    ring rules: ring_rules
    1.30 -  idom rules: noteq_reduce add_scale_eq_noteq]:
    1.31 +  idom rules: noteq_reduce add_scale_eq_noteq
    1.32 +  ideal rules: subr0_iff add_r0_iff]:
    1.33    "ringb add mul pwr r0 r1 sub neg" by fact
    1.34  
    1.35  end
    1.36  
    1.37 +
    1.38  lemma no_zero_divirors_neq0:
    1.39    assumes az: "(a::'a::no_zero_divisors) \<noteq> 0"
    1.40      and ab: "a*b = 0" shows "b = 0"
    1.41 @@ -349,7 +358,6 @@
    1.42    thus "w = x"  by simp
    1.43  qed
    1.44  
    1.45 -
    1.46  declaration {* normalizer_funs @{thm class_ringb.axioms} *}
    1.47  
    1.48  interpretation natgb: semiringb
    1.49 @@ -386,7 +394,8 @@
    1.50    semiring rules: semiring_rules
    1.51    ring ops: ring_ops
    1.52    ring rules: ring_rules
    1.53 -  idom rules: noteq_reduce add_scale_eq_noteq]:
    1.54 +  idom rules: noteq_reduce add_scale_eq_noteq
    1.55 +  ideal rules: subr0_iff add_r0_iff]:
    1.56    "fieldgb add mul pwr r0 r1 sub neg divide inverse" by unfold_locales
    1.57  end
    1.58  
    1.59 @@ -424,8 +433,8 @@
    1.60      ((Scan.optional (keyword addN |-- thms) []) -- 
    1.61      (Scan.optional (keyword delN |-- thms) [])) src 
    1.62   #> (fn ((add_ths, del_ths), ctxt) => 
    1.63 -       Method.SIMPLE_METHOD' (Groebner.ring_tac add_ths del_ths ctxt))
    1.64 +       Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
    1.65  end
    1.66 -*} "solve polynomial equations over (semi)rings using Groebner bases"
    1.67 +*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
    1.68  
    1.69  end