src/ZF/Constructible/Wellorderings.thy
changeset 47072 777549486d44
parent 46823 57bf0cecb366
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Wed Mar 21 13:05:40 2012 +0000
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Wed Mar 21 15:43:02 2012 +0000
     1.3 @@ -109,7 +109,7 @@
     1.4  lemma (in M_basic) wellfounded_induct: 
     1.5       "[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x));  
     1.6           \<forall>x. M(x) & (\<forall>y. <y,x> \<in> r \<longrightarrow> P(y)) \<longrightarrow> P(x) |]
     1.7 -      ==> P(a)";
     1.8 +      ==> P(a)"
     1.9  apply (simp (no_asm_use) add: wellfounded_def)
    1.10  apply (drule_tac x="{z \<in> domain(r). ~P(z)}" in rspec)
    1.11  apply (blast dest: transM)+
    1.12 @@ -119,7 +119,7 @@
    1.13       "[| a\<in>A;  wellfounded_on(M,A,r);  M(A);  
    1.14         separation(M, \<lambda>x. x\<in>A \<longrightarrow> ~P(x));  
    1.15         \<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r \<longrightarrow> P(y)) \<longrightarrow> P(x) |]
    1.16 -      ==> P(a)";
    1.17 +      ==> P(a)"
    1.18  apply (simp (no_asm_use) add: wellfounded_on_def)
    1.19  apply (drule_tac x="{z\<in>A. z\<in>A \<longrightarrow> ~P(z)}" in rspec)
    1.20  apply (blast intro: transM)+
    1.21 @@ -153,6 +153,9 @@
    1.22  by (simp add: wellordered_def well_ord_def tot_ord_def part_ord_def
    1.23         linear_imp_relativized trans_on_imp_relativized wf_on_imp_relativized)
    1.24  
    1.25 +text{*The property being well founded (and hence of being well ordered) is not absolute: 
    1.26 +the set that doesn't contain a minimal element may not exist in the class M. 
    1.27 +However, every set that is well founded in a transitive model M is well founded (page 124).*}
    1.28  
    1.29  subsection{* Relativized versions of order-isomorphisms and order types *}
    1.30