author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58871  c399ae4b836f 
permissions  rwrr 
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 
WellFounded 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 OrderIsomorphisms*} 

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 settheoretic 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 tabwidth;
wenzelm
parents:
19931
diff
changeset

119 
obase_separation obase_equals_separation 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 