author | wenzelm |
Fri, 04 Apr 2014 22:21:46 +0200 | |
changeset 56412 | 2dd33da970ea |
parent 46823 | 57bf0cecb366 |
child 58871 | c399ae4b836f |
permissions | -rw-r--r-- |
13634 | 1 |
(* Title: ZF/Constructible/Rank_Separation.thy |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
*) |
|
4 |
||
5 |
header {*Separation for Facts About Order Types, Rank Functions and |
|
6 |
Well-Founded Relations*} |
|
7 |
||
16417 | 8 |
theory Rank_Separation imports Rank Rec_Separation begin |
13634 | 9 |
|
10 |
||
11 |
text{*This theory proves all instances needed for locales |
|
13687 | 12 |
@{text "M_ordertype"} and @{text "M_wfrank"}. But the material is not |
13 |
needed for proving the relative consistency of AC.*} |
|
13634 | 14 |
|
15 |
subsection{*The Locale @{text "M_ordertype"}*} |
|
16 |
||
17 |
subsubsection{*Separation for Order-Isomorphisms*} |
|
18 |
||
19 |
lemma well_ord_iso_Reflects: |
|
46823 | 20 |
"REFLECTS[\<lambda>x. x\<in>A \<longrightarrow> |
13634 | 21 |
(\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r), |
46823 | 22 |
\<lambda>i x. x\<in>A \<longrightarrow> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i). |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
23 |
fun_apply(##Lset(i),f,x,y) & pair(##Lset(i),y,x,p) & p \<in> r)]" |
13634 | 24 |
by (intro FOL_reflections function_reflections) |
25 |
||
26 |
lemma well_ord_iso_separation: |
|
27 |
"[| L(A); L(f); L(r) |] |
|
46823 | 28 |
==> separation (L, \<lambda>x. x\<in>A \<longrightarrow> (\<exists>y[L]. (\<exists>p[L]. |
13634 | 29 |
fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))" |
13687 | 30 |
apply (rule gen_separation_multi [OF well_ord_iso_Reflects, of "{A,f,r}"], |
31 |
auto) |
|
32 |
apply (rule_tac env="[A,f,r]" in DPow_LsetI) |
|
13634 | 33 |
apply (rule sep_rules | simp)+ |
34 |
done |
|
35 |
||
36 |
||
37 |
subsubsection{*Separation for @{term "obase"}*} |
|
38 |
||
39 |
lemma obase_reflects: |
|
40 |
"REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
|
41 |
ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & |
|
42 |
order_isomorphism(L,par,r,x,mx,g), |
|
43 |
\<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i). |
|
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
44 |
ordinal(##Lset(i),x) & membership(##Lset(i),x,mx) & pred_set(##Lset(i),A,a,r,par) & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
45 |
order_isomorphism(##Lset(i),par,r,x,mx,g)]" |
13634 | 46 |
by (intro FOL_reflections function_reflections fun_plus_reflections) |
47 |
||
48 |
lemma obase_separation: |
|
49 |
--{*part of the order type formalization*} |
|
50 |
"[| L(A); L(r) |] |
|
51 |
==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
|
52 |
ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & |
|
53 |
order_isomorphism(L,par,r,x,mx,g))" |
|
13687 | 54 |
apply (rule gen_separation_multi [OF obase_reflects, of "{A,r}"], auto) |
55 |
apply (rule_tac env="[A,r]" in DPow_LsetI) |
|
56 |
apply (rule ordinal_iff_sats sep_rules | simp)+ |
|
13634 | 57 |
done |
58 |
||
59 |
||
60 |
subsubsection{*Separation for a Theorem about @{term "obase"}*} |
|
61 |
||
62 |
lemma obase_equals_reflects: |
|
46823 | 63 |
"REFLECTS[\<lambda>x. x\<in>A \<longrightarrow> ~(\<exists>y[L]. \<exists>g[L]. |
13634 | 64 |
ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L]. |
65 |
membership(L,y,my) & pred_set(L,A,x,r,pxr) & |
|
66 |
order_isomorphism(L,pxr,r,y,my,g))), |
|
46823 | 67 |
\<lambda>i x. x\<in>A \<longrightarrow> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i). |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
68 |
ordinal(##Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i). |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
69 |
membership(##Lset(i),y,my) & pred_set(##Lset(i),A,x,r,pxr) & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
70 |
order_isomorphism(##Lset(i),pxr,r,y,my,g)))]" |
13634 | 71 |
by (intro FOL_reflections function_reflections fun_plus_reflections) |
72 |
||
73 |
lemma obase_equals_separation: |
|
74 |
"[| L(A); L(r) |] |
|
46823 | 75 |
==> separation (L, \<lambda>x. x\<in>A \<longrightarrow> ~(\<exists>y[L]. \<exists>g[L]. |
13634 | 76 |
ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L]. |
77 |
membership(L,y,my) & pred_set(L,A,x,r,pxr) & |
|
78 |
order_isomorphism(L,pxr,r,y,my,g))))" |
|
13687 | 79 |
apply (rule gen_separation_multi [OF obase_equals_reflects, of "{A,r}"], auto) |
80 |
apply (rule_tac env="[A,r]" in DPow_LsetI) |
|
13634 | 81 |
apply (rule sep_rules | simp)+ |
82 |
done |
|
83 |
||
84 |
||
85 |
subsubsection{*Replacement for @{term "omap"}*} |
|
86 |
||
87 |
lemma omap_reflects: |
|
88 |
"REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
|
89 |
ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & |
|
90 |
pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)), |
|
91 |
\<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B & (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). |
|
92 |
\<exists>par \<in> Lset(i). |
|
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
93 |
ordinal(##Lset(i),x) & pair(##Lset(i),a,x,z) & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
94 |
membership(##Lset(i),x,mx) & pred_set(##Lset(i),A,a,r,par) & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
95 |
order_isomorphism(##Lset(i),par,r,x,mx,g))]" |
13634 | 96 |
by (intro FOL_reflections function_reflections fun_plus_reflections) |
97 |
||
98 |
lemma omap_replacement: |
|
99 |
"[| L(A); L(r) |] |
|
100 |
==> strong_replacement(L, |
|
101 |
\<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L]. |
|
102 |
ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & |
|
103 |
pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))" |
|
104 |
apply (rule strong_replacementI) |
|
13687 | 105 |
apply (rule_tac u="{A,r,B}" in gen_separation_multi [OF omap_reflects], auto) |
106 |
apply (rule_tac env="[A,B,r]" in DPow_LsetI) |
|
13634 | 107 |
apply (rule sep_rules | simp)+ |
108 |
done |
|
109 |
||
110 |
||
111 |
||
112 |
subsection{*Instantiating the locale @{text M_ordertype}*} |
|
113 |
text{*Separation (and Strong Replacement) for basic set-theoretic constructions |
|
114 |
such as intersection, Cartesian Product and image.*} |
|
115 |
||
116 |
lemma M_ordertype_axioms_L: "M_ordertype_axioms(L)" |
|
117 |
apply (rule M_ordertype_axioms.intro) |
|
118 |
apply (assumption | rule well_ord_iso_separation |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19931
diff
changeset
|
119 |
obase_separation obase_equals_separation |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19931
diff
changeset
|
120 |
omap_replacement)+ |
13634 | 121 |
done |
122 |
||
123 |
theorem M_ordertype_L: "PROP M_ordertype(L)" |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
124 |
apply (rule M_ordertype.intro) |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
125 |
apply (rule M_basic_L) |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
126 |
apply (rule M_ordertype_axioms_L) |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
127 |
done |
13634 | 128 |
|
129 |
||
130 |
subsection{*The Locale @{text "M_wfrank"}*} |
|
131 |
||
132 |
subsubsection{*Separation for @{term "wfrank"}*} |
|
133 |
||
134 |
lemma wfrank_Reflects: |
|
46823 | 135 |
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow> |
13634 | 136 |
~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)), |
46823 | 137 |
\<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) \<longrightarrow> |
13634 | 138 |
~ (\<exists>f \<in> Lset(i). |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
139 |
M_is_recfun(##Lset(i), %x f y. is_range(##Lset(i),f,y), |
13634 | 140 |
rplus, x, f))]" |
141 |
by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection) |
|
142 |
||
143 |
lemma wfrank_separation: |
|
144 |
"L(r) ==> |
|
46823 | 145 |
separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow> |
13634 | 146 |
~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))" |
147 |
apply (rule gen_separation [OF wfrank_Reflects], simp) |
|
13687 | 148 |
apply (rule_tac env="[r]" in DPow_LsetI) |
149 |
apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+ |
|
13634 | 150 |
done |
151 |
||
152 |
||
153 |
subsubsection{*Replacement for @{term "wfrank"}*} |
|
154 |
||
155 |
lemma wfrank_replacement_Reflects: |
|
156 |
"REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A & |
|
46823 | 157 |
(\<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow> |
13634 | 158 |
(\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) & |
159 |
M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & |
|
160 |
is_range(L,f,y))), |
|
161 |
\<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A & |
|
46823 | 162 |
(\<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) \<longrightarrow> |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
163 |
(\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(##Lset(i),x,y,z) & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
164 |
M_is_recfun(##Lset(i), %x f y. is_range(##Lset(i),f,y), rplus, x, f) & |
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
165 |
is_range(##Lset(i),f,y)))]" |
13634 | 166 |
by (intro FOL_reflections function_reflections fun_plus_reflections |
167 |
is_recfun_reflection tran_closure_reflection) |
|
168 |
||
169 |
lemma wfrank_strong_replacement: |
|
170 |
"L(r) ==> |
|
171 |
strong_replacement(L, \<lambda>x z. |
|
46823 | 172 |
\<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow> |
13634 | 173 |
(\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) & |
174 |
M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & |
|
175 |
is_range(L,f,y)))" |
|
176 |
apply (rule strong_replacementI) |
|
13687 | 177 |
apply (rule_tac u="{r,B}" |
178 |
in gen_separation_multi [OF wfrank_replacement_Reflects], |
|
179 |
auto) |
|
180 |
apply (rule_tac env="[r,B]" in DPow_LsetI) |
|
181 |
apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+ |
|
13634 | 182 |
done |
183 |
||
184 |
||
185 |
subsubsection{*Separation for Proving @{text Ord_wfrank_range}*} |
|
186 |
||
187 |
lemma Ord_wfrank_Reflects: |
|
46823 | 188 |
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow> |
13634 | 189 |
~ (\<forall>f[L]. \<forall>rangef[L]. |
46823 | 190 |
is_range(L,f,rangef) \<longrightarrow> |
191 |
M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) \<longrightarrow> |
|
13634 | 192 |
ordinal(L,rangef)), |
46823 | 193 |
\<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) \<longrightarrow> |
13634 | 194 |
~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i). |
46823 | 195 |
is_range(##Lset(i),f,rangef) \<longrightarrow> |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
196 |
M_is_recfun(##Lset(i), \<lambda>x f y. is_range(##Lset(i),f,y), |
46823 | 197 |
rplus, x, f) \<longrightarrow> |
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13687
diff
changeset
|
198 |
ordinal(##Lset(i),rangef))]" |
13634 | 199 |
by (intro FOL_reflections function_reflections is_recfun_reflection |
200 |
tran_closure_reflection ordinal_reflection) |
|
201 |
||
202 |
lemma Ord_wfrank_separation: |
|
203 |
"L(r) ==> |
|
204 |
separation (L, \<lambda>x. |
|
46823 | 205 |
\<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow> |
13634 | 206 |
~ (\<forall>f[L]. \<forall>rangef[L]. |
46823 | 207 |
is_range(L,f,rangef) \<longrightarrow> |
208 |
M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) \<longrightarrow> |
|
13634 | 209 |
ordinal(L,rangef)))" |
210 |
apply (rule gen_separation [OF Ord_wfrank_Reflects], simp) |
|
13687 | 211 |
apply (rule_tac env="[r]" in DPow_LsetI) |
212 |
apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+ |
|
13634 | 213 |
done |
214 |
||
215 |
||
216 |
subsubsection{*Instantiating the locale @{text M_wfrank}*} |
|
217 |
||
218 |
lemma M_wfrank_axioms_L: "M_wfrank_axioms(L)" |
|
219 |
apply (rule M_wfrank_axioms.intro) |
|
220 |
apply (assumption | rule |
|
221 |
wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+ |
|
222 |
done |
|
223 |
||
224 |
theorem M_wfrank_L: "PROP M_wfrank(L)" |
|
225 |
apply (rule M_wfrank.intro) |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
226 |
apply (rule M_trancl_L) |
13634 | 227 |
apply (rule M_wfrank_axioms_L) |
228 |
done |
|
229 |
||
230 |
lemmas exists_wfrank = M_wfrank.exists_wfrank [OF M_wfrank_L] |
|
231 |
and M_wellfoundedrank = M_wfrank.M_wellfoundedrank [OF M_wfrank_L] |
|
232 |
and Ord_wfrank_range = M_wfrank.Ord_wfrank_range [OF M_wfrank_L] |
|
233 |
and Ord_range_wellfoundedrank = M_wfrank.Ord_range_wellfoundedrank [OF M_wfrank_L] |
|
234 |
and function_wellfoundedrank = M_wfrank.function_wellfoundedrank [OF M_wfrank_L] |
|
235 |
and domain_wellfoundedrank = M_wfrank.domain_wellfoundedrank [OF M_wfrank_L] |
|
236 |
and wellfoundedrank_type = M_wfrank.wellfoundedrank_type [OF M_wfrank_L] |
|
237 |
and Ord_wellfoundedrank = M_wfrank.Ord_wellfoundedrank [OF M_wfrank_L] |
|
238 |
and wellfoundedrank_eq = M_wfrank.wellfoundedrank_eq [OF M_wfrank_L] |
|
239 |
and wellfoundedrank_lt = M_wfrank.wellfoundedrank_lt [OF M_wfrank_L] |
|
240 |
and wellfounded_imp_subset_rvimage = M_wfrank.wellfounded_imp_subset_rvimage [OF M_wfrank_L] |
|
241 |
and wellfounded_imp_wf = M_wfrank.wellfounded_imp_wf [OF M_wfrank_L] |
|
242 |
and wellfounded_on_imp_wf_on = M_wfrank.wellfounded_on_imp_wf_on [OF M_wfrank_L] |
|
243 |
and wf_abs = M_wfrank.wf_abs [OF M_wfrank_L] |
|
244 |
and wf_on_abs = M_wfrank.wf_on_abs [OF M_wfrank_L] |
|
245 |
||
246 |
end |