# HG changeset patch # User paulson # Date 1332344582 0 # Node ID 777549486d4421e8155864b4c0dbd3cbcfb35adc # Parent 2884ee1ffbf0791f9d4d2384a7e69267f515ab76 refinements to constructibility diff -r 2884ee1ffbf0 -r 777549486d44 src/ZF/Constructible/AC_in_L.thy --- 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: "\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 "\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" \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 diff -r 2884ee1ffbf0 -r 777549486d44 src/ZF/Constructible/DPow_absolute.thy --- 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) == \i[M]. \Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \ Li" theorem V_equals_L_in_L: - "L(x) ==> constructible(L,x)" -apply (simp add: constructible_def Lset_abs Lset_closed) + "L(x) \ constructible(L,x)" +apply (simp add: constructible_def Lset_abs Lset_closed) apply (simp add: L_def) apply (blast intro: Ord_in_L) done diff -r 2884ee1ffbf0 -r 777549486d44 src/ZF/Constructible/Wellorderings.thy --- 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, \x. ~P(x)); \x. M(x) & (\y. \ r \ P(y)) \ P(x) |] - ==> P(a)"; + ==> P(a)" apply (simp (no_asm_use) add: wellfounded_def) apply (drule_tac x="{z \ domain(r). ~P(z)}" in rspec) apply (blast dest: transM)+ @@ -119,7 +119,7 @@ "[| a\A; wellfounded_on(M,A,r); M(A); separation(M, \x. x\A \ ~P(x)); \x\A. M(x) & (\y\A. \ r \ P(y)) \ P(x) |] - ==> P(a)"; + ==> P(a)" apply (simp (no_asm_use) add: wellfounded_on_def) apply (drule_tac x="{z\A. z\A \ ~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 *}