author paulson Thu, 22 Mar 2012 16:41:22 +0000 changeset 47084 2e3dcec91653 parent 47083 d04b38d4035b child 47085 4a8a8b9bf414
New Message
```--- a/src/ZF/Constructible/AC_in_L.thy	Thu Mar 22 10:10:02 2012 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy	Thu Mar 22 16:41:22 2012 +0000
@@ -4,7 +4,7 @@

header {* The Axiom of Choice Holds in L! *}

-theory AC_in_L imports Formula begin
+theory AC_in_L imports Formula Separation begin

subsection{*Extending a Wellordering over a List -- Lexicographic Power*}

@@ -452,6 +452,18 @@
apply (blast dest!: well_ord_L_r intro: well_ord_subset)
done

+interpretation L?: M_basic L by (rule M_basic_L)
+
+theorem "\<forall>x[L]. \<exists>r. wellordered(L,x,r)"
+proof
+  fix x
+  assume "L(x)"
+  then obtain r where "well_ord(x,r)"
+    by (blast dest: L_implies_AC)
+  thus "\<exists>r. wellordered(L,x,r)"
+    by (blast intro: well_ord_imp_relativized)
+qed
+
text{*In order to prove @{term" \<exists>r[L]. wellordered(L, A, r)"}, it's necessary to know
that @{term r} is actually constructible. Of course, it follows from the assumption ``@{term V} equals @{term L''},
but this reasoning doesn't appear to work in Isabelle.*}```