343 thus "b = 0" by blast |
343 thus "b = 0" by blast |
344 qed |
344 qed |
345 |
345 |
346 interpretation class_ringb!: ringb |
346 interpretation class_ringb!: ringb |
347 "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus" |
347 "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus" |
348 proof(unfold_locales, simp add: ring_simps power_Suc, auto) |
348 proof(unfold_locales, simp add: algebra_simps power_Suc, auto) |
349 fix w x y z ::"'a::{idom,recpower,number_ring}" |
349 fix w x y z ::"'a::{idom,recpower,number_ring}" |
350 assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z" |
350 assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z" |
351 hence ynz': "y - z \<noteq> 0" by simp |
351 hence ynz': "y - z \<noteq> 0" by simp |
352 from p have "w * y + x* z - w*z - x*y = 0" by simp |
352 from p have "w * y + x* z - w*z - x*y = 0" by simp |
353 hence "w* (y - z) - x * (y - z) = 0" by (simp add: ring_simps) |
353 hence "w* (y - z) - x * (y - z) = 0" by (simp add: algebra_simps) |
354 hence "(y - z) * (w - x) = 0" by (simp add: ring_simps) |
354 hence "(y - z) * (w - x) = 0" by (simp add: algebra_simps) |
355 with no_zero_divirors_neq0 [OF ynz'] |
355 with no_zero_divirors_neq0 [OF ynz'] |
356 have "w - x = 0" by blast |
356 have "w - x = 0" by blast |
357 thus "w = x" by simp |
357 thus "w = x" by simp |
358 qed |
358 qed |
359 |
359 |
360 declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *} |
360 declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *} |
361 |
361 |
362 interpretation natgb!: semiringb |
362 interpretation natgb!: semiringb |
363 "op +" "op *" "op ^" "0::nat" "1" |
363 "op +" "op *" "op ^" "0::nat" "1" |
364 proof (unfold_locales, simp add: ring_simps power_Suc) |
364 proof (unfold_locales, simp add: algebra_simps power_Suc) |
365 fix w x y z ::"nat" |
365 fix w x y z ::"nat" |
366 { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z" |
366 { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z" |
367 hence "y < z \<or> y > z" by arith |
367 hence "y < z \<or> y > z" by arith |
368 moreover { |
368 moreover { |
369 assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto) |
369 assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto) |
370 then obtain k where kp: "k>0" and yz:"z = y + k" by blast |
370 then obtain k where kp: "k>0" and yz:"z = y + k" by blast |
371 from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz ring_simps) |
371 from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps) |
372 hence "x*k = w*k" by simp |
372 hence "x*k = w*k" by simp |
373 hence "w = x" using kp by (simp add: mult_cancel2) } |
373 hence "w = x" using kp by (simp add: mult_cancel2) } |
374 moreover { |
374 moreover { |
375 assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto) |
375 assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto) |
376 then obtain k where kp: "k>0" and yz:"y = z + k" by blast |
376 then obtain k where kp: "k>0" and yz:"y = z + k" by blast |
377 from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz ring_simps) |
377 from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps) |
378 hence "w*k = x*k" by simp |
378 hence "w*k = x*k" by simp |
379 hence "w = x" using kp by (simp add: mult_cancel2)} |
379 hence "w = x" using kp by (simp add: mult_cancel2)} |
380 ultimately have "w=x" by blast } |
380 ultimately have "w=x" by blast } |
381 thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto |
381 thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto |
382 qed |
382 qed |