refinements to constructibility
authorpaulson
Wed Mar 21 15:43:02 2012 +0000 (2012-03-21)
changeset 47072777549486d44
parent 47071 2884ee1ffbf0
child 47073 c73f7b0c7ebc
refinements to constructibility
src/ZF/Constructible/AC_in_L.thy
src/ZF/Constructible/DPow_absolute.thy
src/ZF/Constructible/Wellorderings.thy
     1.1 --- a/src/ZF/Constructible/AC_in_L.thy	Wed Mar 21 13:05:40 2012 +0000
     1.2 +++ b/src/ZF/Constructible/AC_in_L.thy	Wed Mar 21 15:43:02 2012 +0000
     1.3 @@ -444,16 +444,16 @@
     1.4  done
     1.5  
     1.6  
     1.7 -text{*Locale for proving results under the assumption @{text "V=L"}*}
     1.8 -locale V_equals_L =
     1.9 -  assumes VL: "L(x)"
    1.10 -
    1.11 -text{*The Axiom of Choice holds in @{term L}!  Or, to be precise, the
    1.12 -Wellordering Theorem.*}
    1.13 -theorem (in V_equals_L) AC: "\<exists>r. well_ord(x,r)"
    1.14 -apply (insert Transset_Lset VL [of x])
    1.15 +text{*Every constructible set is well-ordered! Therefore the Wellordering Theorem and
    1.16 +      the Axiom of Choice hold in @{term L}!!*}
    1.17 +theorem L_implies_AC: assumes x: "L(x)" shows "\<exists>r. well_ord(x,r)"
    1.18 +  using Transset_Lset x
    1.19  apply (simp add: Transset_def L_def)
    1.20  apply (blast dest!: well_ord_L_r intro: well_ord_subset)
    1.21  done
    1.22  
    1.23 +text{*In order to prove @{term" \<exists>r[L]. wellordered(L, A, r)"}, it's necessary to know 
    1.24 +that @{term r} is actually constructible. Of course, it follows from the assumption ``@{term V} equals @{term L''}, 
    1.25 +but this reasoning doesn't appear to work in Isabelle.*}
    1.26 +
    1.27  end
     2.1 --- a/src/ZF/Constructible/DPow_absolute.thy	Wed Mar 21 13:05:40 2012 +0000
     2.2 +++ b/src/ZF/Constructible/DPow_absolute.thy	Wed Mar 21 15:43:02 2012 +0000
     2.3 @@ -613,15 +613,14 @@
     2.4  
     2.5  subsection{*The Notion of Constructible Set*}
     2.6  
     2.7 -
     2.8  definition
     2.9    constructible :: "[i=>o,i] => o" where
    2.10      "constructible(M,x) ==
    2.11         \<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"
    2.12  
    2.13  theorem V_equals_L_in_L:
    2.14 -  "L(x) ==> constructible(L,x)"
    2.15 -apply (simp add: constructible_def Lset_abs Lset_closed) 
    2.16 +  "L(x) \<longleftrightarrow> constructible(L,x)"
    2.17 +apply (simp add: constructible_def Lset_abs Lset_closed)
    2.18  apply (simp add: L_def)
    2.19  apply (blast intro: Ord_in_L) 
    2.20  done
     3.1 --- a/src/ZF/Constructible/Wellorderings.thy	Wed Mar 21 13:05:40 2012 +0000
     3.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Wed Mar 21 15:43:02 2012 +0000
     3.3 @@ -109,7 +109,7 @@
     3.4  lemma (in M_basic) wellfounded_induct: 
     3.5       "[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x));  
     3.6           \<forall>x. M(x) & (\<forall>y. <y,x> \<in> r \<longrightarrow> P(y)) \<longrightarrow> P(x) |]
     3.7 -      ==> P(a)";
     3.8 +      ==> P(a)"
     3.9  apply (simp (no_asm_use) add: wellfounded_def)
    3.10  apply (drule_tac x="{z \<in> domain(r). ~P(z)}" in rspec)
    3.11  apply (blast dest: transM)+
    3.12 @@ -119,7 +119,7 @@
    3.13       "[| a\<in>A;  wellfounded_on(M,A,r);  M(A);  
    3.14         separation(M, \<lambda>x. x\<in>A \<longrightarrow> ~P(x));  
    3.15         \<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r \<longrightarrow> P(y)) \<longrightarrow> P(x) |]
    3.16 -      ==> P(a)";
    3.17 +      ==> P(a)"
    3.18  apply (simp (no_asm_use) add: wellfounded_on_def)
    3.19  apply (drule_tac x="{z\<in>A. z\<in>A \<longrightarrow> ~P(z)}" in rspec)
    3.20  apply (blast intro: transM)+
    3.21 @@ -153,6 +153,9 @@
    3.22  by (simp add: wellordered_def well_ord_def tot_ord_def part_ord_def
    3.23         linear_imp_relativized trans_on_imp_relativized wf_on_imp_relativized)
    3.24  
    3.25 +text{*The property being well founded (and hence of being well ordered) is not absolute: 
    3.26 +the set that doesn't contain a minimal element may not exist in the class M. 
    3.27 +However, every set that is well founded in a transitive model M is well founded (page 124).*}
    3.28  
    3.29  subsection{* Relativized versions of order-isomorphisms and order types *}
    3.30