author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58860  fee7cfa69c50 
permissions  rwrr 
13505  1 
(* Title: ZF/Constructible/Reflection.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
*) 

4 

13223  5 
header {* The Reflection Theorem*} 
6 

16417  7 
theory Reflection imports Normal begin 
13223  8 

46823  9 
lemma all_iff_not_ex_not: "(\<forall>x. P(x)) \<longleftrightarrow> (~ (\<exists>x. ~ P(x)))"; 
13223  10 
by blast 
11 

46823  12 
lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) \<longleftrightarrow> (~ (\<exists>x\<in>A. ~ P(x)))"; 
13223  13 
by blast 
14 

46823  15 
text{*From the notes of A. S. Kechris, page 6, and from 
13223  16 
Andrzej Mostowski, \emph{Constructible Sets with Applications}, 
17 
NorthHolland, 1969, page 23.*} 

18 

19 

20 
subsection{*Basic Definitions*} 

21 

46823  22 
text{*First part: the cumulative hierarchy defining the class @{text M}. 
13223  23 
To avoid handling multiple arguments, we assume that @{text "Mset(l)"} is 
24 
closed under ordered pairing provided @{text l} is limit. Possibly this 

46823  25 
could be avoided: the induction hypothesis @{term Cl_reflects} 
13223  26 
(in locale @{text ex_reflection}) could be weakened to 
46823  27 
@{term "\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) \<longleftrightarrow> Q(a,<y,z>)"}, removing most 
28 
uses of @{term Pair_in_Mset}. But there isn't much point in doing so, since 

13223  29 
ultimately the @{text ex_reflection} proof is packaged up using the 
30 
predicate @{text Reflects}. 

31 
*} 

13428  32 
locale reflection = 
13223  33 
fixes Mset and M and Reflects 
34 
assumes Mset_mono_le : "mono_le_subset(Mset)" 

35 
and Mset_cont : "cont_Ord(Mset)" 

46823  36 
and Pair_in_Mset : "[ x \<in> Mset(a); y \<in> Mset(a); Limit(a) ] 
13223  37 
==> <x,y> \<in> Mset(a)" 
13563  38 
defines "M(x) == \<exists>a. Ord(a) & x \<in> Mset(a)" 
39 
and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) & 

46823  40 
(\<forall>a. Cl(a) \<longrightarrow> (\<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)))" 
13223  41 
fixes F0 {*ordinal for a specific value @{term y}*} 
42 
fixes FF {*sup over the whole level, @{term "y\<in>Mset(a)"}*} 

43 
fixes ClEx {*Reflecting ordinals for the formula @{term "\<exists>z. P"}*} 

46823  44 
defines "F0(P,y) == \<mu> b. (\<exists>z. M(z) & P(<y,z>)) \<longrightarrow> 
13223  45 
(\<exists>z\<in>Mset(b). P(<y,z>))" 
46 
and "FF(P) == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)" 

13563  47 
and "ClEx(P,a) == Limit(a) & normalize(FF(P),a) = a" 
13223  48 

46823  49 
lemma (in reflection) Mset_mono: "i\<le>j ==> Mset(i) \<subseteq> Mset(j)" 
50 
apply (insert Mset_mono_le) 

51 
apply (simp add: mono_le_subset_def leI) 

13223  52 
done 
53 

13434  54 
text{*Awkward: we need a version of @{text ClEx_def} as an equality 
55 
at the level of classes, which do not really exist*} 

56 
lemma (in reflection) ClEx_eq: 

13563  57 
"ClEx(P) == \<lambda>a. Limit(a) & normalize(FF(P),a) = a" 
46823  58 
by (simp add: ClEx_def [symmetric]) 
13434  59 

60 

13223  61 
subsection{*Easy Cases of the Reflection Theorem*} 
62 

63 
theorem (in reflection) Triv_reflection [intro]: 

64 
"Reflects(Ord, P, \<lambda>a x. P(x))" 

65 
by (simp add: Reflects_def) 

66 

67 
theorem (in reflection) Not_reflection [intro]: 

68 
"Reflects(Cl,P,Q) ==> Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))" 

46823  69 
by (simp add: Reflects_def) 
13223  70 

71 
theorem (in reflection) And_reflection [intro]: 

46823  72 
"[ Reflects(Cl,P,Q); Reflects(C',P',Q') ] 
73 
==> Reflects(\<lambda>a. Cl(a) & C'(a), \<lambda>x. P(x) & P'(x), 

13563  74 
\<lambda>a x. Q(a,x) & Q'(a,x))" 
13223  75 
by (simp add: Reflects_def Closed_Unbounded_Int, blast) 
76 

77 
theorem (in reflection) Or_reflection [intro]: 

46823  78 
"[ Reflects(Cl,P,Q); Reflects(C',P',Q') ] 
79 
==> Reflects(\<lambda>a. Cl(a) & C'(a), \<lambda>x. P(x)  P'(x), 

13563  80 
\<lambda>a x. Q(a,x)  Q'(a,x))" 
13223  81 
by (simp add: Reflects_def Closed_Unbounded_Int, blast) 
82 

83 
theorem (in reflection) Imp_reflection [intro]: 

46823  84 
"[ Reflects(Cl,P,Q); Reflects(C',P',Q') ] 
85 
==> Reflects(\<lambda>a. Cl(a) & C'(a), 

86 
\<lambda>x. P(x) \<longrightarrow> P'(x), 

87 
\<lambda>a x. Q(a,x) \<longrightarrow> Q'(a,x))" 

13223  88 
by (simp add: Reflects_def Closed_Unbounded_Int, blast) 
89 

90 
theorem (in reflection) Iff_reflection [intro]: 

46823  91 
"[ Reflects(Cl,P,Q); Reflects(C',P',Q') ] 
92 
==> Reflects(\<lambda>a. Cl(a) & C'(a), 

93 
\<lambda>x. P(x) \<longleftrightarrow> P'(x), 

94 
\<lambda>a x. Q(a,x) \<longleftrightarrow> Q'(a,x))" 

95 
by (simp add: Reflects_def Closed_Unbounded_Int, blast) 

13223  96 

97 
subsection{*Reflection for Existential Quantifiers*} 

98 

99 
lemma (in reflection) F0_works: 

100 
"[ y\<in>Mset(a); Ord(a); M(z); P(<y,z>) ] ==> \<exists>z\<in>Mset(F0(P,y)). P(<y,z>)" 

101 
apply (unfold F0_def M_def, clarify) 

102 
apply (rule LeastI2) 

103 
apply (blast intro: Mset_mono [THEN subsetD]) 

104 
apply (blast intro: lt_Ord2, blast) 

105 
done 

106 

107 
lemma (in reflection) Ord_F0 [intro,simp]: "Ord(F0(P,y))" 

108 
by (simp add: F0_def) 

109 

110 
lemma (in reflection) Ord_FF [intro,simp]: "Ord(FF(P,y))" 

111 
by (simp add: FF_def) 

112 

113 
lemma (in reflection) cont_Ord_FF: "cont_Ord(FF(P))" 

114 
apply (insert Mset_cont) 

115 
apply (simp add: cont_Ord_def FF_def, blast) 

116 
done 

117 

46823  118 
text{*Recall that @{term F0} depends upon @{term "y\<in>Mset(a)"}, 
13223  119 
while @{term FF} depends only upon @{term a}. *} 
120 
lemma (in reflection) FF_works: 

121 
"[ M(z); y\<in>Mset(a); P(<y,z>); Ord(a) ] ==> \<exists>z\<in>Mset(FF(P,a)). P(<y,z>)" 

122 
apply (simp add: FF_def) 

46823  123 
apply (simp_all add: cont_Ord_Union [of concl: Mset] 
13223  124 
Mset_cont Mset_mono_le not_emptyI Ord_F0) 
46823  125 
apply (blast intro: F0_works) 
13223  126 
done 
127 

128 
lemma (in reflection) FFN_works: 

46823  129 
"[ M(z); y\<in>Mset(a); P(<y,z>); Ord(a) ] 
13223  130 
==> \<exists>z\<in>Mset(normalize(FF(P),a)). P(<y,z>)" 
46823  131 
apply (drule FF_works [of concl: P], assumption+) 
13223  132 
apply (blast intro: cont_Ord_FF le_normalize [THEN Mset_mono, THEN subsetD]) 
133 
done 

134 

135 

136 
text{*Locale for the induction hypothesis*} 

137 

13428  138 
locale ex_reflection = reflection + 
13223  139 
fixes P "the original formula" 
140 
fixes Q "the reflected formula" 

141 
fixes Cl "the class of reflecting ordinals" 

46823  142 
assumes Cl_reflects: "[ Cl(a); Ord(a) ] ==> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)" 
13223  143 

144 
lemma (in ex_reflection) ClEx_downward: 

46823  145 
"[ M(z); y\<in>Mset(a); P(<y,z>); Cl(a); ClEx(P,a) ] 
13223  146 
==> \<exists>z\<in>Mset(a). Q(a,<y,z>)" 
46823  147 
apply (simp add: ClEx_def, clarify) 
148 
apply (frule Limit_is_Ord) 

149 
apply (frule FFN_works [of concl: P], assumption+) 

150 
apply (drule Cl_reflects, assumption+) 

13223  151 
apply (auto simp add: Limit_is_Ord Pair_in_Mset) 
152 
done 

153 

154 
lemma (in ex_reflection) ClEx_upward: 

46823  155 
"[ z\<in>Mset(a); y\<in>Mset(a); Q(a,<y,z>); Cl(a); ClEx(P,a) ] 
13563  156 
==> \<exists>z. M(z) & P(<y,z>)" 
13223  157 
apply (simp add: ClEx_def M_def) 
158 
apply (blast dest: Cl_reflects 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

159 
intro: Limit_is_Ord Pair_in_Mset) 
13223  160 
done 
161 

162 
text{*Class @{text ClEx} indeed consists of reflecting ordinals...*} 

163 
lemma (in ex_reflection) ZF_ClEx_iff: 

46823  164 
"[ y\<in>Mset(a); Cl(a); ClEx(P,a) ] 
165 
==> (\<exists>z. M(z) & P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))" 

166 
by (blast intro: dest: ClEx_downward ClEx_upward) 

13223  167 

168 
text{*...and it is closed and unbounded*} 

169 
lemma (in ex_reflection) ZF_Closed_Unbounded_ClEx: 

170 
"Closed_Unbounded(ClEx(P))" 

13434  171 
apply (simp add: ClEx_eq) 
13223  172 
apply (fast intro: Closed_Unbounded_Int Normal_imp_fp_Closed_Unbounded 
173 
Closed_Unbounded_Limit Normal_normalize) 

174 
done 

175 

176 
text{*The same two theorems, exported to locale @{text reflection}.*} 

177 

178 
text{*Class @{text ClEx} indeed consists of reflecting ordinals...*} 

179 
lemma (in reflection) ClEx_iff: 

180 
"[ y\<in>Mset(a); Cl(a); ClEx(P,a); 

46823  181 
!!a. [ Cl(a); Ord(a) ] ==> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x) ] 
182 
==> (\<exists>z. M(z) & P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))" 

13223  183 
apply (unfold ClEx_def FF_def F0_def M_def) 
13428  184 
apply (rule ex_reflection.ZF_ClEx_iff 
185 
[OF ex_reflection.intro, OF reflection.intro ex_reflection_axioms.intro, 

186 
of Mset Cl]) 

187 
apply (simp_all add: Mset_mono_le Mset_cont Pair_in_Mset) 

13223  188 
done 
189 

13434  190 
(*Alternative proof, less unfolding: 
191 
apply (rule Reflection.ZF_ClEx_iff [of Mset _ _ Cl, folded M_def]) 

192 
apply (fold ClEx_def FF_def F0_def) 

193 
apply (rule ex_reflection.intro, assumption) 

194 
apply (simp add: ex_reflection_axioms.intro, assumption+) 

195 
*) 

196 

13223  197 
lemma (in reflection) Closed_Unbounded_ClEx: 
46823  198 
"(!!a. [ Cl(a); Ord(a) ] ==> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)) 
13223  199 
==> Closed_Unbounded(ClEx(P))" 
46823  200 
apply (unfold ClEx_eq FF_def F0_def M_def) 
21232  201 
apply (rule ex_reflection.ZF_Closed_Unbounded_ClEx [of Mset _ _ Cl]) 
23464  202 
apply (rule ex_reflection.intro, rule reflection_axioms) 
13434  203 
apply (blast intro: ex_reflection_axioms.intro) 
13223  204 
done 
205 

13292  206 
subsection{*Packaging the Quantifier Reflection Rules*} 
207 

13223  208 
lemma (in reflection) Ex_reflection_0: 
46823  209 
"Reflects(Cl,P0,Q0) 
210 
==> Reflects(\<lambda>a. Cl(a) & ClEx(P0,a), 

211 
\<lambda>x. \<exists>z. M(z) & P0(<x,z>), 

212 
\<lambda>a x. \<exists>z\<in>Mset(a). Q0(a,<x,z>))" 

213 
apply (simp add: Reflects_def) 

13223  214 
apply (intro conjI Closed_Unbounded_Int) 
46823  215 
apply blast 
216 
apply (rule Closed_Unbounded_ClEx [of Cl P0 Q0], blast, clarify) 

217 
apply (rule_tac Cl=Cl in ClEx_iff, assumption+, blast) 

13223  218 
done 
219 

220 
lemma (in reflection) All_reflection_0: 

46823  221 
"Reflects(Cl,P0,Q0) 
222 
==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x.~P0(x), a), 

223 
\<lambda>x. \<forall>z. M(z) \<longrightarrow> P0(<x,z>), 

224 
\<lambda>a x. \<forall>z\<in>Mset(a). Q0(a,<x,z>))" 

225 
apply (simp only: all_iff_not_ex_not ball_iff_not_bex_not) 

226 
apply (rule Not_reflection, drule Not_reflection, simp) 

13223  227 
apply (erule Ex_reflection_0) 
228 
done 

229 

230 
theorem (in reflection) Ex_reflection [intro]: 

46823  231 
"Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
232 
==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. P(fst(x),snd(x)), a), 

233 
\<lambda>x. \<exists>z. M(z) & P(x,z), 

13223  234 
\<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))" 
46823  235 
by (rule Ex_reflection_0 [of _ " \<lambda>x. P(fst(x),snd(x))" 
13223  236 
"\<lambda>a x. Q(a,fst(x),snd(x))", simplified]) 
237 

238 
theorem (in reflection) All_reflection [intro]: 

239 
"Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 

46823  240 
==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
241 
\<lambda>x. \<forall>z. M(z) \<longrightarrow> P(x,z), 

242 
\<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))" 

243 
by (rule All_reflection_0 [of _ "\<lambda>x. P(fst(x),snd(x))" 

13223  244 
"\<lambda>a x. Q(a,fst(x),snd(x))", simplified]) 
245 

13292  246 
text{*And again, this time using classbounded quantifiers*} 
247 

248 
theorem (in reflection) Rex_reflection [intro]: 

46823  249 
"Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
250 
==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. P(fst(x),snd(x)), a), 

251 
\<lambda>x. \<exists>z[M]. P(x,z), 

13292  252 
\<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))" 
46823  253 
by (unfold rex_def, blast) 
13292  254 

255 
theorem (in reflection) Rall_reflection [intro]: 

256 
"Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 

46823  257 
==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
258 
\<lambda>x. \<forall>z[M]. P(x,z), 

259 
\<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))" 

260 
by (unfold rall_def, blast) 

13292  261 

262 

13223  263 
text{*No point considering bounded quantifiers, where reflection is trivial.*} 
264 

265 

266 
subsection{*Simple Examples of Reflection*} 

267 

268 
text{*Example 1: reflecting a simple formula. The reflecting class is first 

46823  269 
given as the variable @{text ?Cl} and later retrieved from the final 
13223  270 
proof state.*} 
46823  271 
schematic_lemma (in reflection) 
13223  272 
"Reflects(?Cl, 
46823  273 
\<lambda>x. \<exists>y. M(y) & x \<in> y, 
13223  274 
\<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)" 
275 
by fast 

276 

277 
text{*Problem here: there needs to be a conjunction (class intersection) 

278 
in the class of reflecting ordinals. The @{term "Ord(a)"} is redundant, 

279 
though harmless.*} 

46823  280 
lemma (in reflection) 
281 
"Reflects(\<lambda>a. Ord(a) & ClEx(\<lambda>x. fst(x) \<in> snd(x), a), 

282 
\<lambda>x. \<exists>y. M(y) & x \<in> y, 

283 
\<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)" 

13223  284 
by fast 
285 

286 

287 
text{*Example 2*} 

46823  288 
schematic_lemma (in reflection) 
13223  289 
"Reflects(?Cl, 
46823  290 
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y), 
291 
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)" 

13223  292 
by fast 
293 

294 
text{*Example 2'. We give the reflecting class explicitly. *} 

46823  295 
lemma (in reflection) 
13223  296 
"Reflects 
13563  297 
(\<lambda>a. (Ord(a) & 
46823  298 
ClEx(\<lambda>x. ~ (snd(x) \<subseteq> fst(fst(x)) \<longrightarrow> snd(x) \<in> snd(fst(x))), a)) & 
299 
ClEx(\<lambda>x. \<forall>z. M(z) \<longrightarrow> z \<subseteq> fst(x) \<longrightarrow> z \<in> snd(x), a), 

300 
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y), 

301 
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)" 

13223  302 
by fast 
303 

304 
text{*Example 2''. We expand the subset relation.*} 

46823  305 
schematic_lemma (in reflection) 
13223  306 
"Reflects(?Cl, 
46823  307 
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> (\<forall>w. M(w) \<longrightarrow> w\<in>z \<longrightarrow> w\<in>x) \<longrightarrow> z\<in>y), 
308 
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). (\<forall>w\<in>Mset(a). w\<in>z \<longrightarrow> w\<in>x) \<longrightarrow> z\<in>y)" 

13223  309 
by fast 
310 

311 
text{*Example 2'''. Singlestep version, to reveal the reflecting class.*} 

46823  312 
schematic_lemma (in reflection) 
13223  313 
"Reflects(?Cl, 
46823  314 
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y), 
315 
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)" 

316 
apply (rule Ex_reflection) 

13223  317 
txt{* 
318 
@{goals[display,indent=0,margin=60]} 

319 
*} 

46823  320 
apply (rule All_reflection) 
13223  321 
txt{* 
322 
@{goals[display,indent=0,margin=60]} 

323 
*} 

46823  324 
apply (rule Triv_reflection) 
13223  325 
txt{* 
326 
@{goals[display,indent=0,margin=60]} 

327 
*} 

328 
done 

329 

330 
text{*Example 3. Warning: the following examples make sense only 

331 
if @{term P} is quantifierfree, since it is not being relativized.*} 

46823  332 
schematic_lemma (in reflection) 
13223  333 
"Reflects(?Cl, 
46823  334 
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<in> y \<longleftrightarrow> z \<in> x & P(z)), 
335 
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y \<longleftrightarrow> z \<in> x & P(z))" 

13223  336 
by fast 
337 

338 
text{*Example 3'*} 

46823  339 
schematic_lemma (in reflection) 
13223  340 
"Reflects(?Cl, 
13563  341 
\<lambda>x. \<exists>y. M(y) & y = Collect(x,P), 
13223  342 
\<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))"; 
343 
by fast 

344 

345 
text{*Example 3''*} 

46823  346 
schematic_lemma (in reflection) 
13223  347 
"Reflects(?Cl, 
13563  348 
\<lambda>x. \<exists>y. M(y) & y = Replace(x,P), 
13223  349 
\<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))"; 
350 
by fast 

351 

352 
text{*Example 4: Axiom of Choice. Possibly wrong, since @{text \<Pi>} needs 

353 
to be relativized.*} 

46823  354 
schematic_lemma (in reflection) 
13223  355 
"Reflects(?Cl, 
46823  356 
\<lambda>A. 0\<notin>A \<longrightarrow> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)), 
357 
\<lambda>a A. 0\<notin>A \<longrightarrow> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))" 

13223  358 
by fast 
359 

360 
end 

361 