equal
deleted
inserted
replaced
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 *) |
3 *) |
4 |
4 |
5 header {* The Axiom of Choice Holds in L! *} |
5 header {* The Axiom of Choice Holds in L! *} |
6 |
6 |
7 theory AC_in_L imports Formula begin |
7 theory AC_in_L imports Formula Separation begin |
8 |
8 |
9 subsection{*Extending a Wellordering over a List -- Lexicographic Power*} |
9 subsection{*Extending a Wellordering over a List -- Lexicographic Power*} |
10 |
10 |
11 text{*This could be moved into a library.*} |
11 text{*This could be moved into a library.*} |
12 |
12 |
450 using Transset_Lset x |
450 using Transset_Lset x |
451 apply (simp add: Transset_def L_def) |
451 apply (simp add: Transset_def L_def) |
452 apply (blast dest!: well_ord_L_r intro: well_ord_subset) |
452 apply (blast dest!: well_ord_L_r intro: well_ord_subset) |
453 done |
453 done |
454 |
454 |
|
455 interpretation L?: M_basic L by (rule M_basic_L) |
|
456 |
|
457 theorem "\<forall>x[L]. \<exists>r. wellordered(L,x,r)" |
|
458 proof |
|
459 fix x |
|
460 assume "L(x)" |
|
461 then obtain r where "well_ord(x,r)" |
|
462 by (blast dest: L_implies_AC) |
|
463 thus "\<exists>r. wellordered(L,x,r)" |
|
464 by (blast intro: well_ord_imp_relativized) |
|
465 qed |
|
466 |
455 text{*In order to prove @{term" \<exists>r[L]. wellordered(L, A, r)"}, it's necessary to know |
467 text{*In order to prove @{term" \<exists>r[L]. wellordered(L, A, r)"}, it's necessary to know |
456 that @{term r} is actually constructible. Of course, it follows from the assumption ``@{term V} equals @{term L''}, |
468 that @{term r} is actually constructible. Of course, it follows from the assumption ``@{term V} equals @{term L''}, |
457 but this reasoning doesn't appear to work in Isabelle.*} |
469 but this reasoning doesn't appear to work in Isabelle.*} |
458 |
470 |
459 end |
471 end |