src/HOL/Groebner_Basis.thy
changeset 25250 b3a485b98963
parent 23573 d85a277f90fd
child 26086 3c243098b64a
equal deleted inserted replaced
25249:76b9892020d5 25250:b3a485b98963
   299   hence "add (mul r0 d) (mul r c) = add (mul r0 c) (mul r d)"
   299   hence "add (mul r0 d) (mul r c) = add (mul r0 c) (mul r d)"
   300     using mul_0 add_cancel by simp
   300     using mul_0 add_cancel by simp
   301   thus "False" using add_mul_solve nz cnd by simp
   301   thus "False" using add_mul_solve nz cnd by simp
   302 qed
   302 qed
   303 
   303 
       
   304 lemma add_r0_iff: " x = add x a \<longleftrightarrow> a = r0"
       
   305 proof-
       
   306   have "a = r0 \<longleftrightarrow> add x a = add x r0" by (simp add: add_cancel)
       
   307   thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
       
   308 qed
       
   309 
   304 declare "axioms" [normalizer del]
   310 declare "axioms" [normalizer del]
   305 
   311 
   306 lemma "axioms" [normalizer
   312 lemma "axioms" [normalizer
   307   semiring ops: semiring_ops
   313   semiring ops: semiring_ops
   308   semiring rules: semiring_rules
   314   semiring rules: semiring_rules
   309   idom rules: noteq_reduce add_scale_eq_noteq]:
   315   idom rules: noteq_reduce add_scale_eq_noteq]:
   310   "semiringb add mul pwr r0 r1" by fact
   316   "semiringb add mul pwr r0 r1" by fact
   311 
   317 
   312 end
   318 end
   313 
   319 
   314 locale ringb = semiringb + gb_ring
   320 locale ringb = semiringb + gb_ring + 
       
   321   assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
   315 begin
   322 begin
   316 
   323 
   317 declare "axioms" [normalizer del]
   324 declare "axioms" [normalizer del]
   318 
   325 
   319 lemma "axioms" [normalizer
   326 lemma "axioms" [normalizer
   320   semiring ops: semiring_ops
   327   semiring ops: semiring_ops
   321   semiring rules: semiring_rules
   328   semiring rules: semiring_rules
   322   ring ops: ring_ops
   329   ring ops: ring_ops
   323   ring rules: ring_rules
   330   ring rules: ring_rules
   324   idom rules: noteq_reduce add_scale_eq_noteq]:
   331   idom rules: noteq_reduce add_scale_eq_noteq
       
   332   ideal rules: subr0_iff add_r0_iff]:
   325   "ringb add mul pwr r0 r1 sub neg" by fact
   333   "ringb add mul pwr r0 r1 sub neg" by fact
   326 
   334 
   327 end
   335 end
       
   336 
   328 
   337 
   329 lemma no_zero_divirors_neq0:
   338 lemma no_zero_divirors_neq0:
   330   assumes az: "(a::'a::no_zero_divisors) \<noteq> 0"
   339   assumes az: "(a::'a::no_zero_divisors) \<noteq> 0"
   331     and ab: "a*b = 0" shows "b = 0"
   340     and ab: "a*b = 0" shows "b = 0"
   332 proof -
   341 proof -
   346   hence "(y - z) * (w - x) = 0" by (simp add: ring_simps)
   355   hence "(y - z) * (w - x) = 0" by (simp add: ring_simps)
   347   with  no_zero_divirors_neq0 [OF ynz']
   356   with  no_zero_divirors_neq0 [OF ynz']
   348   have "w - x = 0" by blast
   357   have "w - x = 0" by blast
   349   thus "w = x"  by simp
   358   thus "w = x"  by simp
   350 qed
   359 qed
   351 
       
   352 
   360 
   353 declaration {* normalizer_funs @{thm class_ringb.axioms} *}
   361 declaration {* normalizer_funs @{thm class_ringb.axioms} *}
   354 
   362 
   355 interpretation natgb: semiringb
   363 interpretation natgb: semiringb
   356   ["op +" "op *" "op ^" "0::nat" "1"]
   364   ["op +" "op *" "op ^" "0::nat" "1"]
   384 lemma "axioms" [normalizer
   392 lemma "axioms" [normalizer
   385   semiring ops: semiring_ops
   393   semiring ops: semiring_ops
   386   semiring rules: semiring_rules
   394   semiring rules: semiring_rules
   387   ring ops: ring_ops
   395   ring ops: ring_ops
   388   ring rules: ring_rules
   396   ring rules: ring_rules
   389   idom rules: noteq_reduce add_scale_eq_noteq]:
   397   idom rules: noteq_reduce add_scale_eq_noteq
       
   398   ideal rules: subr0_iff add_r0_iff]:
   390   "fieldgb add mul pwr r0 r1 sub neg divide inverse" by unfold_locales
   399   "fieldgb add mul pwr r0 r1 sub neg divide inverse" by unfold_locales
   391 end
   400 end
   392 
   401 
   393 
   402 
   394 lemmas bool_simps = simp_thms(1-34)
   403 lemmas bool_simps = simp_thms(1-34)
   422 in
   431 in
   423 fn src => Method.syntax 
   432 fn src => Method.syntax 
   424     ((Scan.optional (keyword addN |-- thms) []) -- 
   433     ((Scan.optional (keyword addN |-- thms) []) -- 
   425     (Scan.optional (keyword delN |-- thms) [])) src 
   434     (Scan.optional (keyword delN |-- thms) [])) src 
   426  #> (fn ((add_ths, del_ths), ctxt) => 
   435  #> (fn ((add_ths, del_ths), ctxt) => 
   427        Method.SIMPLE_METHOD' (Groebner.ring_tac add_ths del_ths ctxt))
   436        Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
   428 end
   437 end
   429 *} "solve polynomial equations over (semi)rings using Groebner bases"
   438 *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
   430 
   439 
   431 end
   440 end