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 (simp add: Transset_def L_def)
 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 (simp add: L_def)
 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 (simp (no_asm_use) add: wellfounded_def)
 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)"
 apply (simp (no_asm_use) add: wellfounded_on_def)
 apply (drule_tac x="{z\<in>A. z\<in>A \<longrightarrow> ~P(z)}" in rspec)
 apply (blast intro: transM)+
@@ -153,6 +153,9 @@
 by (simp add: wellordered_def well_ord_def tot_ord_def part_ord_def
        linear_imp_relativized trans_on_imp_relativized wf_on_imp_relativized)
 
+text{*The property being well founded (and hence of being well ordered) is not absolute: 
+the set that doesn't contain a minimal element may not exist in the class M. 
+However, every set that is well founded in a transitive model M is well founded (page 124).*}
 
 subsection{* Relativized versions of order-isomorphisms and order types *}