equal
deleted
inserted
replaced
398 finally show ?thesis . |
398 finally show ?thesis . |
399 qed |
399 qed |
400 |
400 |
401 end |
401 end |
402 |
402 |
|
403 lemma Card_order_cmax: |
|
404 assumes r: "Card_order r" and s: "Card_order s" |
|
405 shows "Card_order (cmax r s)" |
|
406 unfolding cmax_def by (auto simp: Card_order_csum) |
|
407 |
|
408 lemma ordLeq_cmax: |
|
409 assumes r: "Card_order r" and s: "Card_order s" |
|
410 shows "r \<le>o cmax r s \<and> s \<le>o cmax r s" |
|
411 proof- |
|
412 {assume "r \<le>o s" |
|
413 hence ?thesis by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s) |
|
414 } |
|
415 moreover |
|
416 {assume "s \<le>o r" |
|
417 hence ?thesis using cmax_com by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s) |
|
418 } |
|
419 ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto |
|
420 qed |
|
421 |
|
422 lemmas ordLeq_cmax1 = ordLeq_cmax[THEN conjunct1] and |
|
423 ordLeq_cmax2 = ordLeq_cmax[THEN conjunct2] |
|
424 |
|
425 lemma finite_cmax: |
|
426 assumes r: "Card_order r" and s: "Card_order s" |
|
427 shows "finite (Field (cmax r s)) \<longleftrightarrow> finite (Field r) \<and> finite (Field s)" |
|
428 proof- |
|
429 {assume "r \<le>o s" |
|
430 hence ?thesis by (metis cmax2 ordIso_finite_Field ordLeq_finite_Field r s) |
|
431 } |
|
432 moreover |
|
433 {assume "s \<le>o r" |
|
434 hence ?thesis by (metis cmax1 ordIso_finite_Field ordLeq_finite_Field r s) |
|
435 } |
|
436 ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto |
|
437 qed |
|
438 |
403 end |
439 end |