451 --{*We assume that x is not covered and extend m at the top with x*} |
451 --{*We assume that x is not covered and extend m at the top with x*} |
452 have "m \<noteq> {}" |
452 have "m \<noteq> {}" |
453 proof |
453 proof |
454 assume "m={}" |
454 assume "m={}" |
455 moreover have "Well_order {(x,x)}" |
455 moreover have "Well_order {(x,x)}" |
456 by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def) |
456 by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_unfold Domain_converse [symmetric]) |
457 ultimately show False using max |
457 ultimately show False using max |
458 by (auto simp:I_def init_seg_of_def simp del:Field_insert) |
458 by (auto simp:I_def init_seg_of_def simp del:Field_insert) |
459 qed |
459 qed |
460 hence "Field m \<noteq> {}" by(auto simp:Field_def) |
460 hence "Field m \<noteq> {}" by(auto simp:Field_def) |
461 moreover have "wf(m-Id)" using `Well_order m` |
461 moreover have "wf(m-Id)" using `Well_order m` |
468 have "Refl m" "trans m" "antisym m" "Total m" "wf(m-Id)" |
468 have "Refl m" "trans m" "antisym m" "Total m" "wf(m-Id)" |
469 using `Well_order m` by(simp_all add:order_on_defs) |
469 using `Well_order m` by(simp_all add:order_on_defs) |
470 --{*We show that the extension is a well-order*} |
470 --{*We show that the extension is a well-order*} |
471 have "Refl ?m" using `Refl m` Fm by(auto simp:refl_on_def) |
471 have "Refl ?m" using `Refl m` Fm by(auto simp:refl_on_def) |
472 moreover have "trans ?m" using `trans m` `x \<notin> Field m` |
472 moreover have "trans ?m" using `trans m` `x \<notin> Field m` |
473 unfolding trans_def Field_def Domain_def Range_def by blast |
473 unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast |
474 moreover have "antisym ?m" using `antisym m` `x \<notin> Field m` |
474 moreover have "antisym ?m" using `antisym m` `x \<notin> Field m` |
475 unfolding antisym_def Field_def Domain_def Range_def by blast |
475 unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast |
476 moreover have "Total ?m" using `Total m` Fm by(auto simp: total_on_def) |
476 moreover have "Total ?m" using `Total m` Fm by(auto simp: total_on_def) |
477 moreover have "wf(?m-Id)" |
477 moreover have "wf(?m-Id)" |
478 proof- |
478 proof- |
479 have "wf ?s" using `x \<notin> Field m` |
479 have "wf ?s" using `x \<notin> Field m` |
480 by(auto simp add:wf_eq_minimal Field_def Domain_def Range_def) metis |
480 by(auto simp add:wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis |
481 thus ?thesis using `wf(m-Id)` `x \<notin> Field m` |
481 thus ?thesis using `wf(m-Id)` `x \<notin> Field m` |
482 wf_subset[OF `wf ?s` Diff_subset] |
482 wf_subset[OF `wf ?s` Diff_subset] |
483 by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) |
483 by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) |
484 qed |
484 qed |
485 ultimately have "Well_order ?m" by(simp add:order_on_defs) |
485 ultimately have "Well_order ?m" by(simp add:order_on_defs) |
486 --{*We show that the extension is above m*} |
486 --{*We show that the extension is above m*} |
487 moreover hence "(m,?m) : I" using `Well_order m` `x \<notin> Field m` |
487 moreover hence "(m,?m) : I" using `Well_order m` `x \<notin> Field m` |
488 by(fastforce simp:I_def init_seg_of_def Field_def Domain_def Range_def) |
488 by(fastforce simp:I_def init_seg_of_def Field_def Domain_unfold Domain_converse [symmetric]) |
489 ultimately |
489 ultimately |
490 --{*This contradicts maximality of m:*} |
490 --{*This contradicts maximality of m:*} |
491 have False using max `x \<notin> Field m` unfolding Field_def by blast |
491 have False using max `x \<notin> Field m` unfolding Field_def by blast |
492 } |
492 } |
493 hence "Field m = UNIV" by auto |
493 hence "Field m = UNIV" by auto |
499 proof - |
499 proof - |
500 obtain r::"('a*'a)set" where wo: "Well_order r" and univ: "Field r = UNIV" |
500 obtain r::"('a*'a)set" where wo: "Well_order r" and univ: "Field r = UNIV" |
501 using well_ordering[where 'a = "'a"] by blast |
501 using well_ordering[where 'a = "'a"] by blast |
502 let ?r = "{(x,y). x:A & y:A & (x,y):r}" |
502 let ?r = "{(x,y). x:A & y:A & (x,y):r}" |
503 have 1: "Field ?r = A" using wo univ |
503 have 1: "Field ?r = A" using wo univ |
504 by(fastforce simp: Field_def Domain_def Range_def order_on_defs refl_on_def) |
504 by(fastforce simp: Field_def Domain_unfold Domain_converse [symmetric] order_on_defs refl_on_def) |
505 have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)" |
505 have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)" |
506 using `Well_order r` by(simp_all add:order_on_defs) |
506 using `Well_order r` by(simp_all add:order_on_defs) |
507 have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ) |
507 have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ) |
508 moreover have "trans ?r" using `trans r` |
508 moreover have "trans ?r" using `trans r` |
509 unfolding trans_def by blast |
509 unfolding trans_def by blast |