13223

1 
header {* The class L satisfies the axioms of ZF*}


2 

13269

3 
theory L_axioms = Formula + Relative + Reflection:

13223

4 


5 


6 
text {* The class L satisfies the premises of locale @{text M_axioms} *}


7 


8 
lemma transL: "[ y\<in>x; L(x) ] ==> L(y)"


9 
apply (insert Transset_Lset)


10 
apply (simp add: Transset_def L_def, blast)


11 
done


12 


13 
lemma nonempty: "L(0)"


14 
apply (simp add: L_def)


15 
apply (blast intro: zero_in_Lset)


16 
done


17 


18 
lemma upair_ax: "upair_ax(L)"


19 
apply (simp add: upair_ax_def upair_def, clarify)

13299

20 
apply (rule_tac x="{x,y}" in rexI)


21 
apply (simp_all add: doubleton_in_L)

13223

22 
done


23 


24 
lemma Union_ax: "Union_ax(L)"


25 
apply (simp add: Union_ax_def big_union_def, clarify)

13299

26 
apply (rule_tac x="Union(x)" in rexI)


27 
apply (simp_all add: Union_in_L, auto)

13223

28 
apply (blast intro: transL)


29 
done


30 


31 
lemma power_ax: "power_ax(L)"


32 
apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify)

13299

33 
apply (rule_tac x="{y \<in> Pow(x). L(y)}" in rexI)


34 
apply (simp_all add: LPow_in_L, auto)

13223

35 
apply (blast intro: transL)


36 
done


37 


38 
subsubsection{*For L to satisfy Replacement *}


39 


40 
(*Can't move these to Formula unless the definition of univalent is moved


41 
there too!*)


42 


43 
lemma LReplace_in_Lset:


44 
"[X \<in> Lset(i); univalent(L,X,Q); Ord(i)]


45 
==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)"


46 
apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))"


47 
in exI)


48 
apply simp


49 
apply clarify


50 
apply (rule_tac a="x" in UN_I)


51 
apply (simp_all add: Replace_iff univalent_def)


52 
apply (blast dest: transL L_I)


53 
done


54 


55 
lemma LReplace_in_L:


56 
"[L(X); univalent(L,X,Q)]


57 
==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Y"


58 
apply (drule L_D, clarify)


59 
apply (drule LReplace_in_Lset, assumption+)


60 
apply (blast intro: L_I Lset_in_Lset_succ)


61 
done


62 


63 
lemma replacement: "replacement(L,P)"


64 
apply (simp add: replacement_def, clarify)

13268

65 
apply (frule LReplace_in_L, assumption+, clarify)

13299

66 
apply (rule_tac x=Y in rexI)


67 
apply (simp_all add: Replace_iff univalent_def, blast)

13223

68 
done


69 

13291

70 
subsection{*Instantiation of the locale @{text M_triv_axioms}*}


71 


72 
lemma Lset_mono_le: "mono_le_subset(Lset)"


73 
by (simp add: mono_le_subset_def le_imp_subset Lset_mono)


74 


75 
lemma Lset_cont: "cont_Ord(Lset)"


76 
by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord)


77 


78 
lemmas Pair_in_Lset = Formula.Pair_in_LLimit;


79 


80 
lemmas L_nat = Ord_in_L [OF Ord_nat];


81 


82 
ML


83 
{*


84 
val transL = thm "transL";


85 
val nonempty = thm "nonempty";


86 
val upair_ax = thm "upair_ax";


87 
val Union_ax = thm "Union_ax";


88 
val power_ax = thm "power_ax";


89 
val replacement = thm "replacement";


90 
val L_nat = thm "L_nat";


91 


92 
fun kill_flex_triv_prems st = Seq.hd ((REPEAT_FIRST assume_tac) st);


93 


94 
fun trivaxL th =


95 
kill_flex_triv_prems


96 
([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat]


97 
MRS (inst "M" "L" th));


98 


99 
bind_thm ("ball_abs", trivaxL (thm "M_triv_axioms.ball_abs"));


100 
bind_thm ("rall_abs", trivaxL (thm "M_triv_axioms.rall_abs"));


101 
bind_thm ("bex_abs", trivaxL (thm "M_triv_axioms.bex_abs"));


102 
bind_thm ("rex_abs", trivaxL (thm "M_triv_axioms.rex_abs"));


103 
bind_thm ("ball_iff_equiv", trivaxL (thm "M_triv_axioms.ball_iff_equiv"));


104 
bind_thm ("M_equalityI", trivaxL (thm "M_triv_axioms.M_equalityI"));


105 
bind_thm ("empty_abs", trivaxL (thm "M_triv_axioms.empty_abs"));


106 
bind_thm ("subset_abs", trivaxL (thm "M_triv_axioms.subset_abs"));


107 
bind_thm ("upair_abs", trivaxL (thm "M_triv_axioms.upair_abs"));


108 
bind_thm ("upair_in_M_iff", trivaxL (thm "M_triv_axioms.upair_in_M_iff"));


109 
bind_thm ("singleton_in_M_iff", trivaxL (thm "M_triv_axioms.singleton_in_M_iff"));


110 
bind_thm ("pair_abs", trivaxL (thm "M_triv_axioms.pair_abs"));


111 
bind_thm ("pair_in_M_iff", trivaxL (thm "M_triv_axioms.pair_in_M_iff"));


112 
bind_thm ("pair_components_in_M", trivaxL (thm "M_triv_axioms.pair_components_in_M"));


113 
bind_thm ("cartprod_abs", trivaxL (thm "M_triv_axioms.cartprod_abs"));


114 
bind_thm ("union_abs", trivaxL (thm "M_triv_axioms.union_abs"));


115 
bind_thm ("inter_abs", trivaxL (thm "M_triv_axioms.inter_abs"));


116 
bind_thm ("setdiff_abs", trivaxL (thm "M_triv_axioms.setdiff_abs"));


117 
bind_thm ("Union_abs", trivaxL (thm "M_triv_axioms.Union_abs"));


118 
bind_thm ("Union_closed", trivaxL (thm "M_triv_axioms.Union_closed"));


119 
bind_thm ("Un_closed", trivaxL (thm "M_triv_axioms.Un_closed"));


120 
bind_thm ("cons_closed", trivaxL (thm "M_triv_axioms.cons_closed"));


121 
bind_thm ("successor_abs", trivaxL (thm "M_triv_axioms.successor_abs"));


122 
bind_thm ("succ_in_M_iff", trivaxL (thm "M_triv_axioms.succ_in_M_iff"));


123 
bind_thm ("separation_closed", trivaxL (thm "M_triv_axioms.separation_closed"));


124 
bind_thm ("strong_replacementI", trivaxL (thm "M_triv_axioms.strong_replacementI"));


125 
bind_thm ("strong_replacement_closed", trivaxL (thm "M_triv_axioms.strong_replacement_closed"));


126 
bind_thm ("RepFun_closed", trivaxL (thm "M_triv_axioms.RepFun_closed"));


127 
bind_thm ("lam_closed", trivaxL (thm "M_triv_axioms.lam_closed"));


128 
bind_thm ("image_abs", trivaxL (thm "M_triv_axioms.image_abs"));


129 
bind_thm ("powerset_Pow", trivaxL (thm "M_triv_axioms.powerset_Pow"));


130 
bind_thm ("powerset_imp_subset_Pow", trivaxL (thm "M_triv_axioms.powerset_imp_subset_Pow"));


131 
bind_thm ("nat_into_M", trivaxL (thm "M_triv_axioms.nat_into_M"));


132 
bind_thm ("nat_case_closed", trivaxL (thm "M_triv_axioms.nat_case_closed"));


133 
bind_thm ("Inl_in_M_iff", trivaxL (thm "M_triv_axioms.Inl_in_M_iff"));


134 
bind_thm ("Inr_in_M_iff", trivaxL (thm "M_triv_axioms.Inr_in_M_iff"));


135 
bind_thm ("lt_closed", trivaxL (thm "M_triv_axioms.lt_closed"));


136 
bind_thm ("transitive_set_abs", trivaxL (thm "M_triv_axioms.transitive_set_abs"));


137 
bind_thm ("ordinal_abs", trivaxL (thm "M_triv_axioms.ordinal_abs"));


138 
bind_thm ("limit_ordinal_abs", trivaxL (thm "M_triv_axioms.limit_ordinal_abs"));


139 
bind_thm ("successor_ordinal_abs", trivaxL (thm "M_triv_axioms.successor_ordinal_abs"));


140 
bind_thm ("finite_ordinal_abs", trivaxL (thm "M_triv_axioms.finite_ordinal_abs"));


141 
bind_thm ("omega_abs", trivaxL (thm "M_triv_axioms.omega_abs"));


142 
bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));


143 
bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));


144 
bind_thm ("number3_abs", trivaxL (thm "M_triv_axioms.number3_abs"));


145 
*}


146 


147 
declare ball_abs [simp]


148 
declare rall_abs [simp]


149 
declare bex_abs [simp]


150 
declare rex_abs [simp]


151 
declare empty_abs [simp]


152 
declare subset_abs [simp]


153 
declare upair_abs [simp]


154 
declare upair_in_M_iff [iff]


155 
declare singleton_in_M_iff [iff]


156 
declare pair_abs [simp]


157 
declare pair_in_M_iff [iff]


158 
declare cartprod_abs [simp]


159 
declare union_abs [simp]


160 
declare inter_abs [simp]


161 
declare setdiff_abs [simp]


162 
declare Union_abs [simp]


163 
declare Union_closed [intro,simp]


164 
declare Un_closed [intro,simp]


165 
declare cons_closed [intro,simp]


166 
declare successor_abs [simp]


167 
declare succ_in_M_iff [iff]


168 
declare separation_closed [intro,simp]


169 
declare strong_replacementI [rule_format]


170 
declare strong_replacement_closed [intro,simp]


171 
declare RepFun_closed [intro,simp]


172 
declare lam_closed [intro,simp]


173 
declare image_abs [simp]


174 
declare nat_into_M [intro]


175 
declare Inl_in_M_iff [iff]


176 
declare Inr_in_M_iff [iff]


177 
declare transitive_set_abs [simp]


178 
declare ordinal_abs [simp]


179 
declare limit_ordinal_abs [simp]


180 
declare successor_ordinal_abs [simp]


181 
declare finite_ordinal_abs [simp]


182 
declare omega_abs [simp]


183 
declare number1_abs [simp]


184 
declare number1_abs [simp]


185 
declare number3_abs [simp]


186 


187 


188 
subsection{*Instantiation of the locale @{text reflection}*}


189 


190 
text{*instances of locale constants*}


191 
constdefs


192 
L_Reflects :: "[i=>o,i=>o,[i,i]=>o] => o"


193 
"L_Reflects(Cl,P,Q) == Closed_Unbounded(Cl) &


194 
(\<forall>a. Cl(a) > (\<forall>x \<in> Lset(a). P(x) <> Q(a,x)))"


195 


196 
L_F0 :: "[i=>o,i] => i"


197 
"L_F0(P,y) == \<mu>b. (\<exists>z. L(z) \<and> P(<y,z>)) > (\<exists>z\<in>Lset(b). P(<y,z>))"


198 


199 
L_FF :: "[i=>o,i] => i"


200 
"L_FF(P) == \<lambda>a. \<Union>y\<in>Lset(a). L_F0(P,y)"


201 


202 
L_ClEx :: "[i=>o,i] => o"


203 
"L_ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(L_FF(P),a) = a"


204 


205 
theorem Triv_reflection [intro]:


206 
"L_Reflects(Ord, P, \<lambda>a x. P(x))"


207 
by (simp add: L_Reflects_def)


208 


209 
theorem Not_reflection [intro]:


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


211 
by (simp add: L_Reflects_def)


212 


213 
theorem And_reflection [intro]:


214 
"[ L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') ]


215 
==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<and> P'(x),


216 
\<lambda>a x. Q(a,x) \<and> Q'(a,x))"


217 
by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)


218 


219 
theorem Or_reflection [intro]:


220 
"[ L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') ]


221 
==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<or> P'(x),


222 
\<lambda>a x. Q(a,x) \<or> Q'(a,x))"


223 
by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)


224 


225 
theorem Imp_reflection [intro]:


226 
"[ L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') ]


227 
==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a),


228 
\<lambda>x. P(x) > P'(x),


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


230 
by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)


231 


232 
theorem Iff_reflection [intro]:


233 
"[ L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') ]


234 
==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a),


235 
\<lambda>x. P(x) <> P'(x),


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


237 
by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)


238 


239 


240 
theorem Ex_reflection [intro]:


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


242 
==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. P(fst(x),snd(x)), a),


243 
\<lambda>x. \<exists>z. L(z) \<and> P(x,z),


244 
\<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z))"


245 
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)


246 
apply (rule reflection.Ex_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],


247 
assumption+)


248 
done


249 


250 
theorem All_reflection [intro]:


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


252 
==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. ~P(fst(x),snd(x)), a),


253 
\<lambda>x. \<forall>z. L(z) > P(x,z),


254 
\<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z))"


255 
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)


256 
apply (rule reflection.All_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],


257 
assumption+)


258 
done


259 


260 
theorem Rex_reflection [intro]:


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


262 
==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. P(fst(x),snd(x)), a),


263 
\<lambda>x. \<exists>z[L]. P(x,z),


264 
\<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z))"


265 
by (unfold rex_def, blast)


266 


267 
theorem Rall_reflection [intro]:


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


269 
==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. ~P(fst(x),snd(x)), a),


270 
\<lambda>x. \<forall>z[L]. P(x,z),


271 
\<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z))"


272 
by (unfold rall_def, blast)


273 


274 
lemma ReflectsD:


275 
"[L_Reflects(Cl,P,Q); Ord(i)]


276 
==> \<exists>j. i<j & (\<forall>x \<in> Lset(j). P(x) <> Q(j,x))"


277 
apply (simp add: L_Reflects_def Closed_Unbounded_def, clarify)


278 
apply (blast dest!: UnboundedD)


279 
done


280 


281 
lemma ReflectsE:


282 
"[ L_Reflects(Cl,P,Q); Ord(i);


283 
!!j. [i<j; \<forall>x \<in> Lset(j). P(x) <> Q(j,x)] ==> R ]


284 
==> R"


285 
by (blast dest!: ReflectsD)


286 


287 
lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B";


288 
by blast


289 


290 

13298

291 
subsection{*Internalized formulas for some relativized ones*}


292 


293 
subsubsection{*Unordered pairs*}


294 


295 
constdefs upair_fm :: "[i,i,i]=>i"


296 
"upair_fm(x,y,z) ==


297 
And(Member(x,z),


298 
And(Member(y,z),


299 
Forall(Implies(Member(0,succ(z)),


300 
Or(Equal(0,succ(x)), Equal(0,succ(y)))))))"


301 


302 
lemma upair_type [TC]:


303 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> upair_fm(x,y,z) \<in> formula"


304 
by (simp add: upair_fm_def)


305 


306 
lemma arity_upair_fm [simp]:


307 
"[ x \<in> nat; y \<in> nat; z \<in> nat ]


308 
==> arity(upair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"


309 
by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac)


310 


311 
lemma sats_upair_fm [simp]:


312 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)]


313 
==> sats(A, upair_fm(x,y,z), env) <>


314 
upair(**A, nth(x,env), nth(y,env), nth(z,env))"


315 
by (simp add: upair_fm_def upair_def)


316 


317 
lemma upair_iff_sats:


318 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;


319 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)]


320 
==> upair(**A, x, y, z) <> sats(A, upair_fm(i,j,k), env)"


321 
by (simp add: sats_upair_fm)


322 


323 
text{*Useful? At least it refers to "real" unordered pairs*}


324 
lemma sats_upair_fm2 [simp]:


325 
"[ x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A); Transset(A)]


326 
==> sats(A, upair_fm(x,y,z), env) <>


327 
nth(z,env) = {nth(x,env), nth(y,env)}"


328 
apply (frule lt_length_in_nat, assumption)


329 
apply (simp add: upair_fm_def Transset_def, auto)


330 
apply (blast intro: nth_type)


331 
done


332 


333 
subsubsection{*Ordered pairs*}


334 


335 
constdefs pair_fm :: "[i,i,i]=>i"


336 
"pair_fm(x,y,z) ==


337 
Exists(And(upair_fm(succ(x),succ(x),0),


338 
Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0),


339 
upair_fm(1,0,succ(succ(z)))))))"


340 


341 
lemma pair_type [TC]:


342 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> pair_fm(x,y,z) \<in> formula"


343 
by (simp add: pair_fm_def)


344 


345 
lemma arity_pair_fm [simp]:


346 
"[ x \<in> nat; y \<in> nat; z \<in> nat ]


347 
==> arity(pair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"


348 
by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac)


349 


350 
lemma sats_pair_fm [simp]:


351 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)]


352 
==> sats(A, pair_fm(x,y,z), env) <>


353 
pair(**A, nth(x,env), nth(y,env), nth(z,env))"


354 
by (simp add: pair_fm_def pair_def)


355 


356 
lemma pair_iff_sats:


357 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;


358 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)]


359 
==> pair(**A, x, y, z) <> sats(A, pair_fm(i,j,k), env)"


360 
by (simp add: sats_pair_fm)


361 


362 


363 


364 
subsection{*Proving instances of Separation using Reflection!*}


365 


366 
text{*Helps us solve for de Bruijn indices!*}


367 
lemma nth_ConsI: "[nth(n,l) = x; n \<in> nat] ==> nth(succ(n), Cons(a,l)) = x"


368 
by simp


369 


370 


371 
lemma Collect_conj_in_DPow:


372 
"[ {x\<in>A. P(x)} \<in> DPow(A); {x\<in>A. Q(x)} \<in> DPow(A) ]


373 
==> {x\<in>A. P(x) & Q(x)} \<in> DPow(A)"


374 
by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric])


375 


376 
lemma Collect_conj_in_DPow_Lset:


377 
"[z \<in> Lset(j); {x \<in> Lset(j). P(x)} \<in> DPow(Lset(j))]


378 
==> {x \<in> Lset(j). x \<in> z & P(x)} \<in> DPow(Lset(j))"


379 
apply (frule mem_Lset_imp_subset_Lset)


380 
apply (simp add: Collect_conj_in_DPow Collect_mem_eq


381 
subset_Int_iff2 elem_subset_in_DPow)


382 
done


383 


384 
lemma separation_CollectI:


385 
"(\<And>z. L(z) ==> L({x \<in> z . P(x)})) ==> separation(L, \<lambda>x. P(x))"


386 
apply (unfold separation_def, clarify)


387 
apply (rule_tac x="{x\<in>z. P(x)}" in rexI)


388 
apply simp_all


389 
done


390 


391 
text{*Reduces the original comprehension to the reflected one*}


392 
lemma reflection_imp_L_separation:


393 
"[ \<forall>x\<in>Lset(j). P(x) <> Q(x);


394 
{x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j));


395 
Ord(j); z \<in> Lset(j)] ==> L({x \<in> z . P(x)})"


396 
apply (rule_tac i = "succ(j)" in L_I)


397 
prefer 2 apply simp


398 
apply (subgoal_tac "{x \<in> z. P(x)} = {x \<in> Lset(j). x \<in> z & (Q(x))}")


399 
prefer 2


400 
apply (blast dest: mem_Lset_imp_subset_Lset)


401 
apply (simp add: Lset_succ Collect_conj_in_DPow_Lset)


402 
done


403 


404 


405 
subsubsection{*Separation for Intersection*}


406 


407 
lemma Inter_Reflects:


408 
"L_Reflects(?Cl, \<lambda>x. \<forall>y[L]. y\<in>A > x \<in> y,


409 
\<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A > x \<in> y)"


410 
by fast


411 


412 
lemma Inter_separation:


413 
"L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A > x\<in>y)"


414 
apply (rule separation_CollectI)


415 
apply (rule_tac A="{A,z}" in subset_LsetE, blast )


416 
apply (rule ReflectsE [OF Inter_Reflects], assumption)


417 
apply (drule subset_Lset_ltD, assumption)


418 
apply (erule reflection_imp_L_separation)


419 
apply (simp_all add: lt_Ord2, clarify)


420 
apply (rule DPowI2)


421 
apply (rule ball_iff_sats)


422 
apply (rule imp_iff_sats)


423 
apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats)


424 
apply (rule_tac i=0 and j=2 in mem_iff_sats)


425 
apply (simp_all add: succ_Un_distrib [symmetric])


426 
done


427 


428 
subsubsection{*Separation for Cartesian Product*}


429 


430 
text{*The @{text simplified} attribute tidies up the reflecting class.*}


431 
theorem upair_reflection [simplified,intro]:


432 
"L_Reflects(?Cl, \<lambda>x. upair(L,f(x),g(x),h(x)),


433 
\<lambda>i x. upair(**Lset(i),f(x),g(x),h(x)))"


434 
by (simp add: upair_def, fast)


435 


436 
theorem pair_reflection [simplified,intro]:


437 
"L_Reflects(?Cl, \<lambda>x. pair(L,f(x),g(x),h(x)),


438 
\<lambda>i x. pair(**Lset(i),f(x),g(x),h(x)))"


439 
by (simp only: pair_def rex_setclass_is_bex, fast)


440 


441 
lemma cartprod_Reflects [simplified]:


442 
"L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),


443 
\<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B &


444 
pair(**Lset(i),x,y,z)))"


445 
by fast


446 


447 
lemma cartprod_separation:


448 
"[ L(A); L(B) ]


449 
==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"


450 
apply (rule separation_CollectI)


451 
apply (rule_tac A="{A,B,z}" in subset_LsetE, blast )


452 
apply (rule ReflectsE [OF cartprod_Reflects], assumption)


453 
apply (drule subset_Lset_ltD, assumption)


454 
apply (erule reflection_imp_L_separation)


455 
apply (simp_all add: lt_Ord2, clarify)


456 
apply (rule DPowI2)


457 
apply (rename_tac u)


458 
apply (rule bex_iff_sats)


459 
apply (rule conj_iff_sats)


460 
apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all)


461 
apply (rule bex_iff_sats)


462 
apply (rule conj_iff_sats)


463 
apply (rule mem_iff_sats)


464 
apply (blast intro: nth_0 nth_ConsI)


465 
apply (blast intro: nth_0 nth_ConsI, simp_all)


466 
apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats)


467 
apply (simp_all add: succ_Un_distrib [symmetric])


468 
done


469 


470 
subsubsection{*Separation for Image*}


471 


472 
text{*No @{text simplified} here: it simplifies the occurrence of


473 
the predicate @{term pair}!*}


474 
lemma image_Reflects:


475 
"L_Reflects(?Cl, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),


476 
\<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(**Lset(i),x,y,p)))"


477 
by fast


478 


479 


480 
lemma image_separation:


481 
"[ L(A); L(r) ]


482 
==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"


483 
apply (rule separation_CollectI)


484 
apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )


485 
apply (rule ReflectsE [OF image_Reflects], assumption)


486 
apply (drule subset_Lset_ltD, assumption)


487 
apply (erule reflection_imp_L_separation)


488 
apply (simp_all add: lt_Ord2, clarify)


489 
apply (rule DPowI2)


490 
apply (rule bex_iff_sats)


491 
apply (rule conj_iff_sats)


492 
apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)


493 
apply (blast intro: nth_0 nth_ConsI)


494 
apply (blast intro: nth_0 nth_ConsI, simp_all)


495 
apply (rule bex_iff_sats)


496 
apply (rule conj_iff_sats)


497 
apply (rule mem_iff_sats)


498 
apply (blast intro: nth_0 nth_ConsI)


499 
apply (blast intro: nth_0 nth_ConsI, simp_all)


500 
apply (rule pair_iff_sats)


501 
apply (blast intro: nth_0 nth_ConsI)


502 
apply (blast intro: nth_0 nth_ConsI)


503 
apply (blast intro: nth_0 nth_ConsI)


504 
apply (simp_all add: succ_Un_distrib [symmetric])


505 
done


506 


507 


508 
subsubsection{*Separation for Converse*}


509 


510 
lemma converse_Reflects:


511 
"L_Reflects(?Cl,


512 
\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),


513 
\<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i).


514 
pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z)))"


515 
by fast


516 


517 
lemma converse_separation:


518 
"L(r) ==> separation(L,


519 
\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"


520 
apply (rule separation_CollectI)


521 
apply (rule_tac A="{r,z}" in subset_LsetE, blast )


522 
apply (rule ReflectsE [OF converse_Reflects], assumption)


523 
apply (drule subset_Lset_ltD, assumption)


524 
apply (erule reflection_imp_L_separation)


525 
apply (simp_all add: lt_Ord2, clarify)


526 
apply (rule DPowI2)


527 
apply (rename_tac u)


528 
apply (rule bex_iff_sats)


529 
apply (rule conj_iff_sats)


530 
apply (rule_tac i=0 and j="2" and env="[p,u,r]" in mem_iff_sats, simp_all)


531 
apply (rule bex_iff_sats)


532 
apply (rule bex_iff_sats)


533 
apply (rule conj_iff_sats)


534 
apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats, simp_all)


535 
apply (rule pair_iff_sats)


536 
apply (blast intro: nth_0 nth_ConsI)


537 
apply (blast intro: nth_0 nth_ConsI)


538 
apply (blast intro: nth_0 nth_ConsI)


539 
apply (simp_all add: succ_Un_distrib [symmetric])


540 
done


541 


542 


543 
subsubsection{*Separation for Restriction*}


544 


545 
lemma restrict_Reflects:


546 
"L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),


547 
\<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z)))"


548 
by fast


549 


550 
lemma restrict_separation:


551 
"L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"


552 
apply (rule separation_CollectI)


553 
apply (rule_tac A="{A,z}" in subset_LsetE, blast )


554 
apply (rule ReflectsE [OF restrict_Reflects], assumption)


555 
apply (drule subset_Lset_ltD, assumption)


556 
apply (erule reflection_imp_L_separation)


557 
apply (simp_all add: lt_Ord2, clarify)


558 
apply (rule DPowI2)


559 
apply (rename_tac u)


560 
apply (rule bex_iff_sats)


561 
apply (rule conj_iff_sats)


562 
apply (rule_tac i=0 and j="2" and env="[x,u,A]" in mem_iff_sats, simp_all)


563 
apply (rule bex_iff_sats)


564 
apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats)


565 
apply (simp_all add: succ_Un_distrib [symmetric])


566 
done


567 


568 


569 
subsubsection{*Separation for Composition*}


570 


571 
lemma comp_Reflects:


572 
"L_Reflects(?Cl, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].


573 
pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &


574 
xy\<in>s & yz\<in>r,


575 
\<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i).


576 
pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) &


577 
pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r)"


578 
by fast


579 


580 
lemma comp_separation:


581 
"[ L(r); L(s) ]


582 
==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].


583 
pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &


584 
xy\<in>s & yz\<in>r)"


585 
apply (rule separation_CollectI)


586 
apply (rule_tac A="{r,s,z}" in subset_LsetE, blast )


587 
apply (rule ReflectsE [OF comp_Reflects], assumption)


588 
apply (drule subset_Lset_ltD, assumption)


589 
apply (erule reflection_imp_L_separation)


590 
apply (simp_all add: lt_Ord2, clarify)


591 
apply (rule DPowI2)


592 
apply (rename_tac u)


593 
apply (rule bex_iff_sats)+


594 
apply (rename_tac x y z)


595 
apply (rule conj_iff_sats)


596 
apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)


597 
apply (blast intro: nth_0 nth_ConsI)


598 
apply (blast intro: nth_0 nth_ConsI)


599 
apply (blast intro: nth_0 nth_ConsI, simp_all)


600 
apply (rule bex_iff_sats)


601 
apply (rule conj_iff_sats)


602 
apply (rule pair_iff_sats)


603 
apply (blast intro: nth_0 nth_ConsI)


604 
apply (blast intro: nth_0 nth_ConsI)


605 
apply (blast intro: nth_0 nth_ConsI, simp_all)


606 
apply (rule bex_iff_sats)


607 
apply (rule conj_iff_sats)


608 
apply (rule pair_iff_sats)


609 
apply (blast intro: nth_0 nth_ConsI)


610 
apply (blast intro: nth_0 nth_ConsI)


611 
apply (blast intro: nth_0 nth_ConsI, simp_all)


612 
apply (rule conj_iff_sats)


613 
apply (rule mem_iff_sats)


614 
apply (blast intro: nth_0 nth_ConsI)


615 
apply (blast intro: nth_0 nth_ConsI, simp)


616 
apply (rule mem_iff_sats)


617 
apply (blast intro: nth_0 nth_ConsI)


618 
apply (blast intro: nth_0 nth_ConsI)


619 
apply (simp_all add: succ_Un_distrib [symmetric])


620 
done


621 

13304

622 
subsubsection{*Separation for Predecessors in an Order*}


623 


624 
lemma pred_Reflects:


625 
"L_Reflects(?Cl, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),


626 
\<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p))"


627 
by fast


628 


629 
lemma pred_separation:


630 
"[ L(r); L(x) ] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"


631 
apply (rule separation_CollectI)


632 
apply (rule_tac A="{r,x,z}" in subset_LsetE, blast )


633 
apply (rule ReflectsE [OF pred_Reflects], assumption)


634 
apply (drule subset_Lset_ltD, assumption)


635 
apply (erule reflection_imp_L_separation)


636 
apply (simp_all add: lt_Ord2, clarify)


637 
apply (rule DPowI2)


638 
apply (rename_tac u)


639 
apply (rule bex_iff_sats)


640 
apply (rule conj_iff_sats)


641 
apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats)


642 
apply (blast intro: nth_0 nth_ConsI)


643 
apply (blast intro: nth_0 nth_ConsI, simp)


644 
apply (rule pair_iff_sats)


645 
apply (blast intro: nth_0 nth_ConsI)


646 
apply (blast intro: nth_0 nth_ConsI)


647 
apply (blast intro: nth_0 nth_ConsI, simp_all)


648 
apply (simp_all add: succ_Un_distrib [symmetric])


649 
done


650 


651 


652 
subsubsection{*Separation for the Membership Relation*}


653 


654 
lemma Memrel_Reflects:


655 
"L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,


656 
\<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y)"


657 
by fast


658 


659 
lemma Memrel_separation:


660 
"separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"


661 
apply (rule separation_CollectI)


662 
apply (rule_tac A="{z}" in subset_LsetE, blast )


663 
apply (rule ReflectsE [OF Memrel_Reflects], assumption)


664 
apply (drule subset_Lset_ltD, assumption)


665 
apply (erule reflection_imp_L_separation)


666 
apply (simp_all add: lt_Ord2)


667 
apply (rule DPowI2)


668 
apply (rename_tac u)


669 
apply (rule bex_iff_sats)+


670 
apply (rule conj_iff_sats)


671 
apply (rule_tac env = "[y,x,u]" in pair_iff_sats)


672 
apply (blast intro: nth_0 nth_ConsI)


673 
apply (blast intro: nth_0 nth_ConsI)


674 
apply (blast intro: nth_0 nth_ConsI, simp_all)


675 
apply (rule mem_iff_sats)


676 
apply (blast intro: nth_0 nth_ConsI)


677 
apply (blast intro: nth_0 nth_ConsI)


678 
apply (simp_all add: succ_Un_distrib [symmetric])


679 
done


680 


681 

13298

682 


683 


684 

13223

685 
end
