author paulson Wed Mar 21 15:43:02 2012 +0000 (2012-03-21) changeset 47072 777549486d44 parent 47071 2884ee1ffbf0 child 47073 c73f7b0c7ebc
refinements to constructibility
```     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.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
```