166 |
166 |
167 end |
167 end |
168 |
168 |
169 interpretation class_semiring: gb_semiring |
169 interpretation class_semiring: gb_semiring |
170 ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"] |
170 ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"] |
171 by unfold_locales (auto simp add: ring_eq_simps power_Suc) |
171 by unfold_locales (auto simp add: ring_simps power_Suc) |
172 |
172 |
173 lemmas nat_arith = |
173 lemmas nat_arith = |
174 add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of |
174 add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of |
175 |
175 |
176 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)" |
176 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)" |
339 thus "b = 0" by blast |
339 thus "b = 0" by blast |
340 qed |
340 qed |
341 |
341 |
342 interpretation class_ringb: ringb |
342 interpretation class_ringb: ringb |
343 ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"] |
343 ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"] |
344 proof(unfold_locales, simp add: ring_eq_simps power_Suc, auto) |
344 proof(unfold_locales, simp add: ring_simps power_Suc, auto) |
345 fix w x y z ::"'a::{idom,recpower,number_ring}" |
345 fix w x y z ::"'a::{idom,recpower,number_ring}" |
346 assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z" |
346 assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z" |
347 hence ynz': "y - z \<noteq> 0" by simp |
347 hence ynz': "y - z \<noteq> 0" by simp |
348 from p have "w * y + x* z - w*z - x*y = 0" by simp |
348 from p have "w * y + x* z - w*z - x*y = 0" by simp |
349 hence "w* (y - z) - x * (y - z) = 0" by (simp add: ring_eq_simps) |
349 hence "w* (y - z) - x * (y - z) = 0" by (simp add: ring_simps) |
350 hence "(y - z) * (w - x) = 0" by (simp add: ring_eq_simps) |
350 hence "(y - z) * (w - x) = 0" by (simp add: ring_simps) |
351 with no_zero_divirors_neq0 [OF ynz'] |
351 with no_zero_divirors_neq0 [OF ynz'] |
352 have "w - x = 0" by blast |
352 have "w - x = 0" by blast |
353 thus "w = x" by simp |
353 thus "w = x" by simp |
354 qed |
354 qed |
355 |
355 |
366 conv = fn phi => K numeral_conv} |
366 conv = fn phi => K numeral_conv} |
367 *} |
367 *} |
368 |
368 |
369 interpretation natgb: semiringb |
369 interpretation natgb: semiringb |
370 ["op +" "op *" "op ^" "0::nat" "1"] |
370 ["op +" "op *" "op ^" "0::nat" "1"] |
371 proof (unfold_locales, simp add: ring_eq_simps power_Suc) |
371 proof (unfold_locales, simp add: ring_simps power_Suc) |
372 fix w x y z ::"nat" |
372 fix w x y z ::"nat" |
373 { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z" |
373 { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z" |
374 hence "y < z \<or> y > z" by arith |
374 hence "y < z \<or> y > z" by arith |
375 moreover { |
375 moreover { |
376 assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto) |
376 assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto) |
377 then obtain k where kp: "k>0" and yz:"z = y + k" by blast |
377 then obtain k where kp: "k>0" and yz:"z = y + k" by blast |
378 from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz ring_eq_simps) |
378 from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz ring_simps) |
379 hence "x*k = w*k" by simp |
379 hence "x*k = w*k" by simp |
380 hence "w = x" using kp by (simp add: mult_cancel2) } |
380 hence "w = x" using kp by (simp add: mult_cancel2) } |
381 moreover { |
381 moreover { |
382 assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto) |
382 assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto) |
383 then obtain k where kp: "k>0" and yz:"y = z + k" by blast |
383 then obtain k where kp: "k>0" and yz:"y = z + k" by blast |
384 from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz ring_eq_simps) |
384 from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz ring_simps) |
385 hence "w*k = x*k" by simp |
385 hence "w*k = x*k" by simp |
386 hence "w = x" using kp by (simp add: mult_cancel2)} |
386 hence "w = x" using kp by (simp add: mult_cancel2)} |
387 ultimately have "w=x" by blast } |
387 ultimately have "w=x" by blast } |
388 thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto |
388 thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto |
389 qed |
389 qed |