author paulson Wed, 21 Mar 2012 15:43:02 +0000 changeset 47072 777549486d44 parent 47071 2884ee1ffbf0 child 47073 c73f7b0c7ebc
refinements to constructibility
```--- a/src/ZF/Constructible/AC_in_L.thy	Wed Mar 21 13:05:40 2012 +0000
+++ b/src/ZF/Constructible/AC_in_L.thy	Wed Mar 21 15:43:02 2012 +0000
@@ -444,16 +444,16 @@
done

-text{*Locale for proving results under the assumption @{text "V=L"}*}
-locale V_equals_L =
-  assumes VL: "L(x)"
-
-text{*The Axiom of Choice holds in @{term L}!  Or, to be precise, the
-Wellordering Theorem.*}
-theorem (in V_equals_L) AC: "\<exists>r. well_ord(x,r)"
-apply (insert Transset_Lset VL [of x])
+text{*Every constructible set is well-ordered! Therefore the Wellordering Theorem and
+      the Axiom of Choice hold in @{term L}!!*}
+theorem L_implies_AC: assumes x: "L(x)" shows "\<exists>r. well_ord(x,r)"
+  using Transset_Lset x
apply (blast dest!: well_ord_L_r intro: well_ord_subset)
done

+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.*}
+
end```
```--- a/src/ZF/Constructible/DPow_absolute.thy	Wed Mar 21 13:05:40 2012 +0000
+++ b/src/ZF/Constructible/DPow_absolute.thy	Wed Mar 21 15:43:02 2012 +0000
@@ -613,15 +613,14 @@

subsection{*The Notion of Constructible Set*}

-
definition
constructible :: "[i=>o,i] => o" where
"constructible(M,x) ==
\<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"

theorem V_equals_L_in_L:
-  "L(x) ==> constructible(L,x)"
-apply (simp add: constructible_def Lset_abs Lset_closed)
+  "L(x) \<longleftrightarrow> constructible(L,x)"
+apply (simp add: constructible_def Lset_abs Lset_closed)
apply (blast intro: Ord_in_L)
done```
```--- a/src/ZF/Constructible/Wellorderings.thy	Wed Mar 21 13:05:40 2012 +0000
+++ b/src/ZF/Constructible/Wellorderings.thy	Wed Mar 21 15:43:02 2012 +0000
@@ -109,7 +109,7 @@
lemma (in M_basic) wellfounded_induct:
"[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x));
\<forall>x. M(x) & (\<forall>y. <y,x> \<in> r \<longrightarrow> P(y)) \<longrightarrow> P(x) |]
-      ==> P(a)";
+      ==> P(a)"
apply (drule_tac x="{z \<in> domain(r). ~P(z)}" in rspec)
apply (blast dest: transM)+
@@ -119,7 +119,7 @@
"[| a\<in>A;  wellfounded_on(M,A,r);  M(A);
separation(M, \<lambda>x. x\<in>A \<longrightarrow> ~P(x));
\<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r \<longrightarrow> P(y)) \<longrightarrow> P(x) |]
-      ==> P(a)";
+      ==> P(a)"