Theory Replacement_Instances
section‹More Instances of Replacement›
theory Replacement_Instances
imports
Separation_Instances
Transitive_Models.Pointed_DC_Relative
begin
lemma composition_fm_type[TC]: "a0 ∈ ω ⟹ a1 ∈ ω ⟹ a2 ∈ ω ⟹
composition_fm(a0,a1,a2) ∈ formula"
unfolding composition_fm_def by simp
arity_theorem for "composition_fm"
definition is_omega_funspace :: "[i⇒o,i,i,i]⇒o" where
"is_omega_funspace(N,B,n,z) ≡ ∃o[N]. omega(N,o) ∧ n∈o ∧ is_funspace(N, n, B, z)"
synthesize "omega_funspace" from_definition "is_omega_funspace" assuming "nonempty"
arity_theorem for "omega_funspace_fm"
definition HAleph_wfrec_repl_body where
"HAleph_wfrec_repl_body(N,mesa,x,z) ≡ ∃y[N].
pair(N, x, y, z) ∧
(∃g[N].
(∀u[N].
u ∈ g ⟷
(∃a[N].
∃y[N].
∃ax[N].
∃sx[N].
∃r_sx[N].
∃f_r_sx[N].
pair(N, a, y, u) ∧
pair(N, a, x, ax) ∧
upair(N, a, a, sx) ∧
pre_image(N, mesa, sx, r_sx) ∧
restriction(N, g, r_sx, f_r_sx) ∧ ax ∈ mesa ∧ is_HAleph(N, a, f_r_sx, y))) ∧
is_HAleph(N, x, g, y))"
arity_theorem for "ordinal_fm"
arity_theorem for "is_Limit_fm"
arity_theorem for "empty_fm"
arity_theorem for "fun_apply_fm"
synthesize "HAleph_wfrec_repl_body" from_definition assuming "nonempty"
arity_theorem for "HAleph_wfrec_repl_body_fm"
definition dcwit_repl_body where
"dcwit_repl_body(N,mesa,A,a,s,R) ≡ λx z. ∃y[N]. pair(N, x, y, z) ∧
is_wfrec
(N, λn f. is_nat_case
(N, a,
λm bmfm.
∃fm[N].
∃cp[N].
is_apply(N, f, m, fm) ∧
is_Collect(N, A, λx. ∃fmx[N]. (N(x) ∧ fmx ∈ R) ∧ pair(N, fm, x, fmx), cp) ∧
is_apply(N, s, cp, bmfm),
n),
mesa, x, y)"
manual_schematic for "dcwit_repl_body" assuming "nonempty"
unfolding dcwit_repl_body_def
by (rule iff_sats is_nat_case_iff_sats is_eclose_iff_sats sep_rules | simp)+
synthesize "dcwit_repl_body" from_schematic
definition dcwit_aux_fm where
"dcwit_aux_fm(A,s,R) ≡ (⋅∃⋅⋅4`2 is 0⋅ ∧
(⋅∃⋅Collect_fm
(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(A)))))))))),
(⋅∃⋅⋅0 ∈
succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(R)))))))))))) ⋅ ∧
pair_fm(3, 1, 0) ⋅⋅),
0) ∧
⋅ succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(s))))))))))`0 is 2⋅⋅⋅)⋅⋅)"
arity_theorem for "dcwit_aux_fm"
lemma dcwit_aux_fm_type[TC]: "A ∈ ω ⟹ s ∈ ω ⟹ R ∈ ω ⟹ dcwit_aux_fm(A,s,R) ∈ formula"
by (simp_all add: dcwit_aux_fm_def)
definition is_nat_case_dcwit_aux_fm where
"is_nat_case_dcwit_aux_fm(A,a,s,R) ≡ is_nat_case_fm
(succ(succ(succ(succ(succ(succ(a)))))),dcwit_aux_fm(A,s,R),
2, 0)"
lemma is_nat_case_dcwit_aux_fm_type[TC]: "A ∈ ω ⟹ a ∈ ω ⟹ s ∈ ω ⟹ R ∈ ω ⟹ is_nat_case_dcwit_aux_fm(A,a,s,R) ∈ formula"
by (simp_all add: is_nat_case_dcwit_aux_fm_def)
manual_arity for "is_nat_case_dcwit_aux_fm"
unfolding is_nat_case_dcwit_aux_fm_def
by (rule arity_dcwit_aux_fm[THEN [6] arity_is_nat_case_fm]) simp_all
manual_arity for "dcwit_repl_body_fm"
using arity_is_nat_case_dcwit_aux_fm[THEN [6] arity_is_wfrec_fm]
unfolding dcwit_repl_body_fm_def is_nat_case_dcwit_aux_fm_def dcwit_aux_fm_def
by (auto simp add: arity(1-33))
lemma arity_dcwit_repl_body: "arity(dcwit_repl_body_fm(6,5,4,3,2,0,1)) = 7"
by (simp_all add: FOL_arities arity_dcwit_repl_body_fm ord_simp_union)
definition fst2_snd2
where "fst2_snd2(x) ≡ ⟨fst(fst(x)), snd(snd(x))⟩"
relativize functional "fst2_snd2" "fst2_snd2_rel"
relationalize "fst2_snd2_rel" "is_fst2_snd2"
lemma (in M_trivial) fst2_snd2_abs:
assumes "M(x)" "M(res)"
shows "is_fst2_snd2(M, x, res) ⟷ res = fst2_snd2(x)"
unfolding is_fst2_snd2_def fst2_snd2_def
using fst_rel_abs snd_rel_abs fst_abs snd_abs assms
by simp
synthesize "is_fst2_snd2" from_definition assuming "nonempty"
arity_theorem for "is_fst2_snd2_fm"
definition sndfst_fst2_snd2
where "sndfst_fst2_snd2(x) ≡ ⟨snd(fst(x)), fst(fst(x)), snd(snd(x))⟩"
relativize functional "sndfst_fst2_snd2" "sndfst_fst2_snd2_rel"
relationalize "sndfst_fst2_snd2_rel" "is_sndfst_fst2_snd2"
synthesize "is_sndfst_fst2_snd2" from_definition assuming "nonempty"
arity_theorem for "is_sndfst_fst2_snd2_fm"
definition order_eq_map where
"order_eq_map(M,A,r,a,z) ≡ ∃x[M]. ∃g[M]. ∃mx[M]. ∃par[M].
ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g)"
synthesize "order_eq_map" from_definition assuming "nonempty"
arity_theorem for "is_ord_iso_fm"
arity_theorem for "order_eq_map_fm"
synthesize "is_banach_functor" from_definition assuming "nonempty"
arity_theorem for "is_banach_functor_fm"
definition banach_body_iterates where
"banach_body_iterates(M,X,Y,f,g,W,n,x,z) ≡
∃y[M].
pair(M, x, y, z) ∧
(∃fa[M].
(∀z[M].
z ∈ fa ⟷
(∃xa[M].
∃y[M].
∃xaa[M].
∃sx[M].
∃r_sx[M].
∃f_r_sx[M]. ∃sn[M]. ∃msn[M]. successor(M,n,sn) ∧
membership(M,sn,msn) ∧
pair(M, xa, y, z) ∧
pair(M, xa, x, xaa) ∧
upair(M, xa, xa, sx) ∧
pre_image(M, msn, sx, r_sx) ∧
restriction(M, fa, r_sx, f_r_sx) ∧
xaa ∈ msn ∧
(empty(M, xa) ⟶ y = W) ∧
(∀m[M].
successor(M, m, xa) ⟶
(∃gm[M].
is_apply(M, f_r_sx, m, gm) ∧ is_banach_functor(M, X, Y, f, g, gm, y))) ∧
(is_quasinat(M, xa) ∨ empty(M, y)))) ∧
(empty(M, x) ⟶ y = W) ∧
(∀m[M].
successor(M, m, x) ⟶
(∃gm[M]. is_apply(M, fa, m, gm) ∧ is_banach_functor(M, X, Y, f, g, gm, y))) ∧
(is_quasinat(M, x) ∨ empty(M, y)))"
synthesize "is_quasinat" from_definition assuming "nonempty"
arity_theorem for "is_quasinat_fm"
synthesize "banach_body_iterates" from_definition assuming "nonempty"
arity_theorem for "banach_body_iterates_fm"
definition banach_is_iterates_body where
"banach_is_iterates_body(M,X,Y,f,g,W,n,y) ≡ ∃om[M]. omega(M,om) ∧ n ∈ om ∧
(∃sn[M].
∃msn[M].
successor(M, n, sn) ∧
membership(M, sn, msn) ∧
(∃fa[M].
(∀z[M].
z ∈ fa ⟷
(∃x[M].
∃y[M].
∃xa[M].
∃sx[M].
∃r_sx[M].
∃f_r_sx[M].
pair(M, x, y, z) ∧
pair(M, x, n, xa) ∧
upair(M, x, x, sx) ∧
pre_image(M, msn, sx, r_sx) ∧
restriction(M, fa, r_sx, f_r_sx) ∧
xa ∈ msn ∧
(empty(M, x) ⟶ y = W) ∧
(∀m[M].
successor(M, m, x) ⟶
(∃gm[M].
fun_apply(M, f_r_sx, m, gm) ∧ is_banach_functor(M, X, Y, f, g, gm, y))) ∧
(is_quasinat(M, x) ∨ empty(M, y)))) ∧
(empty(M, n) ⟶ y = W) ∧
(∀m[M].
successor(M, m, n) ⟶
(∃gm[M]. fun_apply(M, fa, m, gm) ∧ is_banach_functor(M, X, Y, f, g, gm, y))) ∧
(is_quasinat(M, n) ∨ empty(M, y))))"
synthesize "banach_is_iterates_body" from_definition assuming "nonempty"
arity_theorem for "banach_is_iterates_body_fm"
definition trans_apply_image where
"trans_apply_image(f) ≡ λa g. f ` (g `` a)"
relativize functional "trans_apply_image" "trans_apply_image_rel"
relationalize "trans_apply_image" "is_trans_apply_image"
schematic_goal arity_is_recfun_fm[arity]:
"p ∈ formula ⟹ a ∈ ω ⟹ z ∈ ω ⟹ r ∈ ω ⟹ arity(is_recfun_fm(p, a, z ,r)) = ?ar"
unfolding is_recfun_fm_def
by (simp add:arity)
schematic_goal arity_is_wfrec_fm[arity]:
"p ∈ formula ⟹ a ∈ ω ⟹ z ∈ ω ⟹ r ∈ ω ⟹ arity(is_wfrec_fm(p, a, z ,r)) = ?ar"
unfolding is_wfrec_fm_def
by (simp add:arity)
schematic_goal arity_is_transrec_fm[arity]:
"p ∈ formula ⟹ a ∈ ω ⟹ z ∈ ω ⟹ arity(is_transrec_fm(p, a, z)) = ?ar"
unfolding is_transrec_fm_def
by (simp add:arity)
synthesize "is_trans_apply_image" from_definition assuming "nonempty"
arity_theorem for "is_trans_apply_image_fm"
definition transrec_apply_image_body where
"transrec_apply_image_body(M,f,mesa,x,z) ≡ ∃y[M]. pair(M, x, y, z) ∧
(∃fa[M].
(∀z[M].
z ∈ fa ⟷
(∃xa[M].
∃y[M].
∃xaa[M].
∃sx[M].
∃r_sx[M].
∃f_r_sx[M].
pair(M, xa, y, z) ∧
pair(M, xa, x, xaa) ∧
upair(M, xa, xa, sx) ∧
pre_image(M, mesa, sx, r_sx) ∧
restriction(M, fa, r_sx, f_r_sx) ∧
xaa ∈ mesa ∧ is_trans_apply_image(M, f, xa, f_r_sx, y))) ∧
is_trans_apply_image(M, f, x, fa, y))"
synthesize "transrec_apply_image_body" from_definition assuming "nonempty"
arity_theorem for "transrec_apply_image_body_fm"
definition is_trans_apply_image_body where
"is_trans_apply_image_body(M,f,β,a,w) ≡ ∃z[M]. pair(M,a,z,w) ∧ a∈β ∧ (∃sa[M].
∃esa[M].
∃mesa[M].
upair(M, a, a, sa) ∧
is_eclose(M, sa, esa) ∧
membership(M, esa, mesa) ∧
(∃fa[M].
(∀z[M].
z ∈ fa ⟷
(∃x[M].
∃y[M].
∃xa[M].
∃sx[M].
∃r_sx[M].
∃f_r_sx[M].
pair(M, x, y, z) ∧
pair(M, x, a, xa) ∧
upair(M, x, x, sx) ∧
pre_image(M, mesa, sx, r_sx) ∧
restriction(M, fa, r_sx, f_r_sx) ∧
xa ∈ mesa ∧ is_trans_apply_image(M, f, x, f_r_sx, y))) ∧
is_trans_apply_image(M, f, a, fa, z)))"
synthesize "is_trans_apply_image_body" from_definition assuming "nonempty"
arity_theorem for "is_trans_apply_image_body_fm"
definition replacement_is_omega_funspace_fm where "replacement_is_omega_funspace_fm ≡ omega_funspace_fm(2,0,1)"
definition wfrec_Aleph_fm where "wfrec_Aleph_fm ≡ HAleph_wfrec_repl_body_fm(2,0,1)"
definition replacement_is_fst2_snd2_fm where "replacement_is_fst2_snd2_fm ≡ is_fst2_snd2_fm(0,1)"
definition replacement_is_sndfst_fst2_snd2_fm where "replacement_is_sndfst_fst2_snd2_fm ≡ is_sndfst_fst2_snd2_fm(0,1)"
definition omap_replacement_fm where "omap_replacement_fm ≡ order_eq_map_fm(2,3,0,1)"
definition rec_constr_abs_fm where "rec_constr_abs_fm ≡ transrec_apply_image_body_fm(3,2,0,1)"
definition banach_replacement_iterates_fm where "banach_replacement_iterates_fm ≡ banach_is_iterates_body_fm(6,5,4,3,2,0,1)"
definition rec_constr_fm where "rec_constr_fm ≡ is_trans_apply_image_body_fm(3,2,0,1)"
definition dc_abs_fm where "dc_abs_fm ≡ dcwit_repl_body_fm(6,5,4,3,2,0,1)"
definition lam_replacement_check_fm where "lam_replacement_check_fm ≡ Lambda_in_M_fm(check_fm(2,0,1),1)"
text‹The following instances are needed only on the ground model. The
first one corresponds to the recursive definition of forces for atomic
formulas; the next two corresponds to \<^term>‹PHcheck›; the following
is used to get a generic filter using some form of choice.›
locale M_ZF_ground = M_ZF1 +
assumes
ZF_ground_replacements:
"replacement_assm(M,env,wfrec_Hfrc_at_fm)"
"replacement_assm(M,env,wfrec_Hcheck_fm)"
"replacement_assm(M,env,lam_replacement_check_fm)"
locale M_ZF_ground_trans = M_ZF1_trans + M_ZF_ground
definition instances_ground_fms where "instances_ground_fms ≡
{ wfrec_Hfrc_at_fm,
wfrec_Hcheck_fm,
lam_replacement_check_fm }"
lemmas replacement_instances_ground_defs =
wfrec_Hfrc_at_fm_def wfrec_Hcheck_fm_def lam_replacement_check_fm_def
declare (in M_ZF_ground) replacement_instances_ground_defs [simp]
lemma instances_ground_fms_type[TC]: "instances_ground_fms ⊆ formula"
using Lambda_in_M_fm_type
unfolding instances_ground_fms_def replacement_instances_ground_defs
by simp
locale M_ZF_ground_notCH = M_ZF_ground +
assumes
ZF_ground_notCH_replacements:
"replacement_assm(M,env,rec_constr_abs_fm)"
"replacement_assm(M,env,rec_constr_fm)"
definition instances_ground_notCH_fms where "instances_ground_notCH_fms ≡
{ rec_constr_abs_fm,
rec_constr_fm }"
lemma instances_ground_notCH_fms_type[TC]: "instances_ground_notCH_fms ⊆ formula"
unfolding instances_ground_notCH_fms_def rec_constr_abs_fm_def
rec_constr_fm_def
by simp
declare (in M_ZF_ground_notCH) rec_constr_abs_fm_def[simp]
rec_constr_fm_def[simp]
locale M_ZF_ground_notCH_trans = M_ZF_ground_trans + M_ZF_ground_notCH
locale M_ZF_ground_CH = M_ZF_ground_notCH +
assumes
dcwit_replacement: "replacement_assm(M,env,dc_abs_fm)"
declare (in M_ZF_ground_CH) dc_abs_fm_def [simp]
locale M_ZF_ground_CH_trans = M_ZF_ground_notCH_trans + M_ZF_ground_CH
locale M_ctm1 = M_ZF1_trans + M_ZF_ground_trans +
fixes enum
assumes M_countable: "enum∈bij(nat,M)"
locale M_ctm1_AC = M_ctm1 + M_ZFC1_trans
context M_ZF_ground_CH_trans
begin
lemma replacement_dcwit_repl_body:
"(##M)(mesa) ⟹ (##M)(A) ⟹ (##M)(a) ⟹ (##M)(s) ⟹ (##M)(R) ⟹
strong_replacement(##M, dcwit_repl_body(##M,mesa,A,a,s,R))"
using strong_replacement_rel_in_ctm[where φ="dcwit_repl_body_fm(6,5,4,3,2,0,1)"
and env="[R,s,a,A,mesa]" and f="dcwit_repl_body(##M,mesa,A,a,s,R)"]
zero_in_M arity_dcwit_repl_body dcwit_replacement
unfolding dc_abs_fm_def
by simp
lemma dcwit_repl:
"(##M)(sa) ⟹
(##M)(esa) ⟹
(##M)(mesa) ⟹ (##M)(A) ⟹ (##M)(a) ⟹ (##M)(s) ⟹ (##M)(R) ⟹
strong_replacement
((##M), λx z. ∃y[(##M)]. pair((##M), x, y, z) ∧
is_wfrec
((##M), λn f. is_nat_case
((##M), a,
λm bmfm.
∃fm[(##M)].
∃cp[(##M)].
is_apply((##M), f, m, fm) ∧
is_Collect((##M), A, λx. ∃fmx[(##M)]. ((##M)(x) ∧ fmx ∈ R) ∧ pair((##M), fm, x, fmx), cp) ∧
is_apply((##M), s, cp, bmfm),
n),
mesa, x, y))"
using replacement_dcwit_repl_body unfolding dcwit_repl_body_def by simp
end
context M_ZF1_trans
begin
lemmas M_replacement_ZF_instances = lam_replacement_fst lam_replacement_snd
lam_replacement_Union lam_replacement_Image
lam_replacement_middle_del lam_replacement_prodRepl
lemmas M_separation_ZF_instances = separation_fstsnd_in_sndsnd separation_sndfst_eq_fstsnd
lemma separation_is_dcwit_body:
assumes "(##M)(A)" "(##M)(a)" "(##M)(g)" "(##M)(R)"
shows "separation(##M,is_dcwit_body(##M, A, a, g, R))"
using assms separation_in_ctm[where env="[A,a,g,R]" and φ="is_dcwit_body_fm(1,2,3,4,0)",
OF _ _ _ is_dcwit_body_iff_sats[symmetric],
of "λ_.A" "λ_.a" "λ_.g" "λ_.R" "λx. x"]
nonempty arity_is_dcwit_body_fm is_dcwit_body_fm_type
by (simp add:ord_simp_union)
end
sublocale M_ZF1_trans ⊆ M_replacement "##M"
using M_replacement_ZF_instances M_separation_ZF_instances
by unfold_locales simp
context M_ZF1_trans
begin
lemma separation_Pow_rel: "A∈M ⟹
separation(##M, λy. ∃x ∈ M . x∈A ∧ y = ⟨x, Pow⇗##M⇖(x)⟩)"
using separation_assm_sats[of "is_Pow_fm(0,1)"] arity_is_Pow_fm ord_simp_union
Pow_rel_closed nonempty Pow_rel_iff
by simp
lemma strong_replacement_Powapply_rel:
"f∈M ⟹ strong_replacement(##M, λx y. y = Powapply⇗##M⇖(f,x))"
using Powapply_rel_replacement separation_Pow_rel transM
by simp
end
sublocale M_ZF1_trans ⊆ M_Vfrom "##M"
using power_ax strong_replacement_Powapply_rel phrank_repl trans_repl_HVFrom wfrec_rank
by unfold_locales auto
sublocale M_ZF1_trans ⊆ M_Perm "##M"
using separation_PiP_rel separation_injP_rel separation_surjP_rel
lam_replacement_imp_strong_replacement[OF
lam_replacement_Sigfun[OF lam_replacement_constant]]
Pi_replacement1 unfolding Sigfun_def
by unfold_locales simp_all
sublocale M_ZF1_trans ⊆ M_pre_seqspace "##M"
by unfold_locales
context M_ZF1_trans
begin
lemma separation_inj_rel: "A∈M ⟹
separation(##M, λy. ∃x∈M. x ∈ A ∧ y = ⟨x, inj_rel(##M,fst(x), snd(x))⟩)"
using arity_is_inj_fm ord_simp_union
nonempty inj_rel_closed[simplified] inj_rel_iff[simplified]
by (rule_tac separation_assm_bin_sats[of "is_inj_fm(0,1,2)"])
(simp_all add:setclass_def)
lemma lam_replacement_inj_rel: "lam_replacement(##M, λx . inj_rel(##M,fst(x),snd(x)))"
using lam_replacement_inj_rel' separation_inj_rel
by simp
end
lemma (in M_basic) rel2_trans_apply:
"M(f) ⟹ relation2(M,is_trans_apply_image(M,f),trans_apply_image(f))"
unfolding is_trans_apply_image_def trans_apply_image_def relation2_def
by auto
lemma (in M_basic) apply_image_closed:
shows "M(f) ⟹ ∀x[M]. ∀g[M]. M(trans_apply_image(f, x, g))"
unfolding trans_apply_image_def by simp
context M_ZF_ground_notCH_trans
begin
lemma replacement_transrec_apply_image_body :
"(##M)(f) ⟹ (##M)(mesa) ⟹ strong_replacement(##M,transrec_apply_image_body(##M,f,mesa))"
using strong_replacement_rel_in_ctm[where φ="transrec_apply_image_body_fm(3,2,0,1)" and env="[mesa,f]"]
zero_in_M arity_transrec_apply_image_body_fm ord_simp_union
ZF_ground_notCH_replacements(1)
by simp
lemma transrec_replacement_apply_image:
assumes "(##M)(f)" "(##M)(α)"
shows "transrec_replacement(##M, is_trans_apply_image(##M, f), α)"
using replacement_transrec_apply_image_body[unfolded transrec_apply_image_body_def] assms
Memrel_closed singleton_closed eclose_closed
unfolding transrec_replacement_def wfrec_replacement_def is_wfrec_def M_is_recfun_def
by simp
lemma rec_trans_apply_image_abs:
assumes "(##M)(f)" "(##M)(x)" "(##M)(y)" "Ord(x)"
shows "is_transrec(##M,is_trans_apply_image(##M, f),x,y) ⟷ y = transrec(x,trans_apply_image(f))"
using transrec_abs[OF transrec_replacement_apply_image rel2_trans_apply] assms apply_image_closed
by simp
lemma replacement_is_trans_apply_image:
"(##M)(f) ⟹ (##M)(β) ⟹ strong_replacement(##M, λ x z .
∃y[##M]. pair(##M,x,y,z) ∧ x∈β ∧ (is_transrec(##M,is_trans_apply_image(##M, f),x,y)))"
unfolding is_transrec_def is_wfrec_def M_is_recfun_def
apply(rule_tac strong_replacement_cong[
where P="λ x z. M,[x,z,β,f] ⊨ is_trans_apply_image_body_fm(3,2,0,1)",THEN iffD1])
apply(rule_tac is_trans_apply_image_body_iff_sats[symmetric,unfolded is_trans_apply_image_body_def,where env="[_,_,β,f]"])
apply(simp_all add:zero_in_M)
apply(rule_tac ZF_ground_notCH_replacements(2)[unfolded replacement_assm_def, rule_format, where env="[β,f]",simplified])
apply(simp_all add: arity_is_trans_apply_image_body_fm is_trans_apply_image_body_fm_type ord_simp_union)
done
lemma trans_apply_abs:
"(##M)(f) ⟹ (##M)(β) ⟹ Ord(β) ⟹ (##M)(x) ⟹ (##M)(z) ⟹
(x∈β ∧ z = ⟨x, transrec(x, λa g. f ` (g `` a)) ⟩) ⟷
(∃y[##M]. pair(##M,x,y,z) ∧ x∈β ∧ (is_transrec(##M,is_trans_apply_image(##M, f),x,y)))"
using rec_trans_apply_image_abs Ord_in_Ord
transrec_closed[OF transrec_replacement_apply_image rel2_trans_apply,of f,simplified]
apply_image_closed
unfolding trans_apply_image_def
by auto
lemma replacement_trans_apply_image:
"(##M)(f) ⟹ (##M)(β) ⟹ Ord(β) ⟹
strong_replacement(##M, λx y. x∈β ∧ y = ⟨x, transrec(x, λa g. f ` (g `` a))⟩)"
using strong_replacement_cong[THEN iffD1,OF _ replacement_is_trans_apply_image,simplified]
trans_apply_abs Ord_in_Ord
by simp
end
definition ifrFb_body where
"ifrFb_body(M,b,f,x,i) ≡ x ∈
(if b = 0 then if i ∈ range(f) then
if M(converse(f) ` i) then converse(f) ` i else 0 else 0 else if M(i) then i else 0)"
relativize functional "ifrFb_body" "ifrFb_body_rel"
relationalize "ifrFb_body_rel" "is_ifrFb_body"
synthesize "is_ifrFb_body" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body_fm"
definition ifrangeF_body :: "[i⇒o,i,i,i,i] ⇒ o" where
"ifrangeF_body(M,A,b,f) ≡ λy. ∃x∈A. y = ⟨x,μ i. ifrFb_body(M,b,f,x,i)⟩"
relativize functional "ifrangeF_body" "ifrangeF_body_rel"
relationalize "ifrangeF_body_rel" "is_ifrangeF_body"
synthesize "is_ifrangeF_body" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body_fm"
lemma (in M_Z_trans) separation_is_ifrangeF_body:
"(##M)(A) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation(##M, is_ifrangeF_body(##M,A,r,s))"
using separation_in_ctm[where φ="is_ifrangeF_body_fm(1,2,3,0)" and env="[A,r,s]"]
zero_in_M arity_is_ifrangeF_body_fm ord_simp_union is_ifrangeF_body_fm_type
by simp
lemma (in M_basic) is_ifrFb_body_closed: "M(r) ⟹ M(s) ⟹ is_ifrFb_body(M, r, s, x, i) ⟹ M(i)"
unfolding ifrangeF_body_def is_ifrangeF_body_def is_ifrFb_body_def If_abs
by (cases "i∈range(s)"; cases "r=0"; auto dest:transM)
lemma (in M_ZF1_trans) ifrangeF_body_abs:
assumes "(##M)(A)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
shows "is_ifrangeF_body(##M,A,r,s,x) ⟷ ifrangeF_body(##M,A,r,s,x)"
proof -
{
fix a
assume "a∈M"
with assms
have "(μ i. i∈ M ∧ is_ifrFb_body(##M, r, s, z, i))= (μ i. is_ifrFb_body(##M, r, s, z, i))" for z
using is_ifrFb_body_closed[of r s z]
by (rule_tac Least_cong[of "λi. i∈M ∧ is_ifrFb_body(##M,r,s,z,i)"]) auto
moreover
have "(μ i. is_ifrFb_body(##M, r, s, z, i))= (μ i. ifrFb_body(##M, r, s, z, i))" for z
proof (rule_tac Least_cong[of "λi. is_ifrFb_body(##M,r,s,z,i)" "λi. ifrFb_body(##M,r,s,z,i)"])
fix y
from assms ‹a∈M›
show "is_ifrFb_body(##M, r, s, z, y) ⟷ ifrFb_body(##M, r, s, z, y)"
using If_abs apply_0
unfolding ifrFb_body_def is_ifrFb_body_def
by (cases "y∈M"; cases "y∈range(s)"; cases "converse(s)`y ∈ M";
auto dest:transM split del: split_if del:iffI)
(auto simp flip:setclass_iff; (force simp only:setclass_iff))+
qed
moreover from ‹a∈M›
have "least(##M, λi. i ∈ M ∧ is_ifrFb_body(##M, r, s, z, i), a)
⟷ a = (μ i. i∈ M ∧ is_ifrFb_body(##M, r, s, z,i))" for z
using If_abs least_abs'[of "λi. (##M)(i) ∧ is_ifrFb_body(##M,r,s,z,i)" a]
by simp
ultimately
have "least(##M, λi. i ∈ M ∧ is_ifrFb_body(##M, r, s, z, i), a)
⟷ a = (μ i. ifrFb_body(##M, r, s, z,i))" for z
by simp
}
with assms
show ?thesis
using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
unfolding ifrangeF_body_def is_ifrangeF_body_def
by (auto dest:transM)
qed
lemma (in M_ZF1_trans) separation_ifrangeF_body:
"(##M)(A) ⟹ (##M)(b) ⟹ (##M)(f) ⟹ separation
(##M, λy. ∃x∈A. y = ⟨x, μ i. x ∈ if_range_F_else_F(λx. if (##M)(x) then x else 0, b, f, i)⟩)"
using separation_is_ifrangeF_body ifrangeF_body_abs
separation_cong[where P="is_ifrangeF_body(##M,A,b,f)" and M="##M",THEN iffD1]
unfolding ifrangeF_body_def if_range_F_def if_range_F_else_F_def ifrFb_body_def
by simp
definition ifrFb_body2 where
"ifrFb_body2(M,G,b,f,x,i) ≡ x ∈
(if b = 0 then if i ∈ range(f) then
if M(converse(f) ` i) then G`(converse(f) ` i) else 0 else 0 else if M(i) then G`i else 0)"
relativize functional "ifrFb_body2" "ifrFb_body2_rel"
relationalize "ifrFb_body2_rel" "is_ifrFb_body2"
synthesize "is_ifrFb_body2" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body2_fm"
definition ifrangeF_body2 :: "[i⇒o,i,i,i,i,i] ⇒ o" where
"ifrangeF_body2(M,A,G,b,f) ≡ λy. ∃x∈A. y = ⟨x,μ i. ifrFb_body2(M,G,b,f,x,i)⟩"
relativize functional "ifrangeF_body2" "ifrangeF_body2_rel"
relationalize "ifrangeF_body2_rel" "is_ifrangeF_body2"
synthesize "is_ifrangeF_body2" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body2_fm"
lemma (in M_Z_trans) separation_is_ifrangeF_body2:
"(##M)(A) ⟹ (##M)(G) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation(##M, is_ifrangeF_body2(##M,A,G,r,s))"
using separation_in_ctm[where φ="is_ifrangeF_body2_fm(1,2,3,4,0)" and env="[A,G,r,s]"]
zero_in_M arity_is_ifrangeF_body2_fm ord_simp_union is_ifrangeF_body2_fm_type
by simp
lemma (in M_basic) is_ifrFb_body2_closed: "M(G) ⟹ M(r) ⟹ M(s) ⟹ is_ifrFb_body2(M, G, r, s, x, i) ⟹ M(i)"
unfolding ifrangeF_body2_def is_ifrangeF_body2_def is_ifrFb_body2_def If_abs
by (cases "i∈range(s)"; cases "r=0"; auto dest:transM)
lemma (in M_ZF1_trans) ifrangeF_body2_abs:
assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
shows "is_ifrangeF_body2(##M,A,G,r,s,x) ⟷ ifrangeF_body2(##M,A,G,r,s,x)"
proof -
{
fix a
assume "a∈M"
with assms
have "(μ i. i∈ M ∧ is_ifrFb_body2(##M, G, r, s, z, i))= (μ i. is_ifrFb_body2(##M, G, r, s, z, i))" for z
using is_ifrFb_body2_closed[of G r s z]
by (rule_tac Least_cong[of "λi. i∈M ∧ is_ifrFb_body2(##M,G,r,s,z,i)"]) auto
moreover
have "(μ i. is_ifrFb_body2(##M, G, r, s, z, i))= (μ i. ifrFb_body2(##M, G, r, s, z, i))" for z
proof (rule_tac Least_cong[of "λi. is_ifrFb_body2(##M,G,r,s,z,i)" "λi. ifrFb_body2(##M,G,r,s,z,i)"])
fix y
from assms ‹a∈M›
show "is_ifrFb_body2(##M, G, r, s, z, y) ⟷ ifrFb_body2(##M, G, r, s, z, y)"
using If_abs apply_0
unfolding ifrFb_body2_def is_ifrFb_body2_def
by (cases "y∈M"; cases "y∈range(s)"; cases "converse(s)`y ∈ M";
auto dest:transM split del: split_if del:iffI)
(auto simp flip:setclass_iff; (force simp only:setclass_iff))+
qed
moreover from ‹a∈M›
have "least(##M, λi. i ∈ M ∧ is_ifrFb_body2(##M, G, r, s, z, i), a)
⟷ a = (μ i. i∈ M ∧ is_ifrFb_body2(##M, G, r, s, z,i))" for z
using If_abs least_abs'[of "λi. (##M)(i) ∧ is_ifrFb_body2(##M,G,r,s,z,i)" a]
by simp
ultimately
have "least(##M, λi. i ∈ M ∧ is_ifrFb_body2(##M, G, r, s, z, i), a)
⟷ a = (μ i. ifrFb_body2(##M, G, r, s, z,i))" for z
by simp
}
with assms
show ?thesis
using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
unfolding ifrangeF_body2_def is_ifrangeF_body2_def
by (auto dest:transM)
qed
lemma (in M_ZF1_trans) separation_ifrangeF_body2:
"(##M)(A) ⟹ (##M)(G) ⟹ (##M)(b) ⟹ (##M)(f) ⟹
separation
(##M,
λy. ∃x∈A.
y =
⟨x, μ i. x ∈
if_range_F_else_F(λa. if (##M)(a) then G ` a else 0, b, f, i)⟩)"
using separation_is_ifrangeF_body2 ifrangeF_body2_abs
separation_cong[where P="is_ifrangeF_body2(##M,A,G,b,f)" and M="##M",THEN iffD1]
unfolding ifrangeF_body2_def if_range_F_def if_range_F_else_F_def ifrFb_body2_def
by simp
definition ifrFb_body3 where
"ifrFb_body3(M,G,b,f,x,i) ≡ x ∈
(if b = 0 then if i ∈ range(f) then
if M(converse(f) ` i) then G-``{converse(f) ` i} else 0 else 0 else if M(i) then G-``{i} else 0)"
relativize functional "ifrFb_body3" "ifrFb_body3_rel"
relationalize "ifrFb_body3_rel" "is_ifrFb_body3"
synthesize "is_ifrFb_body3" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body3_fm"
definition ifrangeF_body3 :: "[i⇒o,i,i,i,i,i] ⇒ o" where
"ifrangeF_body3(M,A,G,b,f) ≡ λy. ∃x∈A. y = ⟨x,μ i. ifrFb_body3(M,G,b,f,x,i)⟩"
relativize functional "ifrangeF_body3" "ifrangeF_body3_rel"
relationalize "ifrangeF_body3_rel" "is_ifrangeF_body3"
synthesize "is_ifrangeF_body3" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body3_fm"
lemma (in M_Z_trans) separation_is_ifrangeF_body3:
"(##M)(A) ⟹ (##M)(G) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation(##M, is_ifrangeF_body3(##M,A,G,r,s))"
using separation_in_ctm[where φ="is_ifrangeF_body3_fm(1,2,3,4,0)" and env="[A,G,r,s]"]
zero_in_M arity_is_ifrangeF_body3_fm ord_simp_union is_ifrangeF_body3_fm_type
by simp
lemma (in M_basic) is_ifrFb_body3_closed: "M(G) ⟹ M(r) ⟹ M(s) ⟹ is_ifrFb_body3(M, G, r, s, x, i) ⟹ M(i)"
unfolding ifrangeF_body3_def is_ifrangeF_body3_def is_ifrFb_body3_def If_abs
by (cases "i∈range(s)"; cases "r=0"; auto dest:transM)
lemma (in M_ZF1_trans) ifrangeF_body3_abs:
assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
shows "is_ifrangeF_body3(##M,A,G,r,s,x) ⟷ ifrangeF_body3(##M,A,G,r,s,x)"
proof -
{
fix a
assume "a∈M"
with assms
have "(μ i. i∈ M ∧ is_ifrFb_body3(##M, G, r, s, z, i))= (μ i. is_ifrFb_body3(##M, G, r, s, z, i))" for z
using is_ifrFb_body3_closed[of G r s z]
by (rule_tac Least_cong[of "λi. i∈M ∧ is_ifrFb_body3(##M,G,r,s,z,i)"]) auto
moreover
have "(μ i. is_ifrFb_body3(##M, G, r, s, z, i))= (μ i. ifrFb_body3(##M, G, r, s, z, i))" for z
proof (rule_tac Least_cong[of "λi. is_ifrFb_body3(##M,G,r,s,z,i)" "λi. ifrFb_body3(##M,G,r,s,z,i)"])
fix y
from assms ‹a∈M›
show "is_ifrFb_body3(##M, G, r, s, z, y) ⟷ ifrFb_body3(##M, G, r, s, z, y)"
using If_abs apply_0
unfolding ifrFb_body3_def is_ifrFb_body3_def
by (cases "y∈M"; cases "y∈range(s)"; cases "converse(s)`y ∈ M";
auto dest:transM split del: split_if del:iffI)
(auto simp flip:setclass_iff; (force simp only:setclass_iff))+
qed
moreover from ‹a∈M›
have "least(##M, λi. i ∈ M ∧ is_ifrFb_body3(##M, G, r, s, z, i), a)
⟷ a = (μ i. i∈ M ∧ is_ifrFb_body3(##M, G, r, s, z,i))" for z
using If_abs least_abs'[of "λi. (##M)(i) ∧ is_ifrFb_body3(##M,G,r,s,z,i)" a]
by simp
ultimately
have "least(##M, λi. i ∈ M ∧ is_ifrFb_body3(##M, G, r, s, z, i), a)
⟷ a = (μ i. ifrFb_body3(##M, G, r, s, z,i))" for z
by simp
}
with assms
show ?thesis
using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
unfolding ifrangeF_body3_def is_ifrangeF_body3_def
by (auto dest:transM)
qed
lemma (in M_ZF1_trans) separation_ifrangeF_body3:
"(##M)(A) ⟹ (##M)(G) ⟹ (##M)(b) ⟹ (##M)(f) ⟹
separation
(##M,
λy. ∃x∈A.
y =
⟨x, μ i. x ∈
if_range_F_else_F(λa. if (##M)(a) then G-``{a} else 0, b, f, i)⟩)"
using separation_is_ifrangeF_body3 ifrangeF_body3_abs
separation_cong[where P="is_ifrangeF_body3(##M,A,G,b,f)" and M="##M",THEN iffD1]
unfolding ifrangeF_body3_def if_range_F_def if_range_F_else_F_def ifrFb_body3_def
by simp
definition ifrFb_body4 where
"ifrFb_body4(G,b,f,x,i) ≡ x ∈
(if b = 0 then if i ∈ range(f) then G`(converse(f) ` i) else 0 else G`i)"
relativize functional "ifrFb_body4" "ifrFb_body4_rel"
relationalize "ifrFb_body4_rel" "is_ifrFb_body4"
synthesize "is_ifrFb_body4" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body4_fm"
definition ifrangeF_body4 :: "[i⇒o,i,i,i,i,i] ⇒ o" where
"ifrangeF_body4(M,A,G,b,f) ≡ λy. ∃x∈A. y = ⟨x,μ i. ifrFb_body4(G,b,f,x,i)⟩"
relativize functional "ifrangeF_body4" "ifrangeF_body4_rel"
relationalize "ifrangeF_body4_rel" "is_ifrangeF_body4"
synthesize "is_ifrangeF_body4" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body4_fm"
lemma (in M_Z_trans) separation_is_ifrangeF_body4:
"(##M)(A) ⟹ (##M)(G) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation(##M, is_ifrangeF_body4(##M,A,G,r,s))"
using separation_in_ctm[where φ="is_ifrangeF_body4_fm(1,2,3,4,0)" and env="[A,G,r,s]"]
zero_in_M arity_is_ifrangeF_body4_fm ord_simp_union is_ifrangeF_body4_fm_type
by simp
lemma (in M_basic) is_ifrFb_body4_closed: "M(G) ⟹ M(r) ⟹ M(s) ⟹ is_ifrFb_body4(M, G, r, s, x, i) ⟹ M(i)"
using If_abs
unfolding ifrangeF_body4_def is_ifrangeF_body4_def is_ifrFb_body4_def fun_apply_def
by (cases "i∈range(s)"; cases "r=0"; auto dest:transM)
lemma (in M_ZF1_trans) ifrangeF_body4_abs:
assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
shows "is_ifrangeF_body4(##M,A,G,r,s,x) ⟷ ifrangeF_body4(##M,A,G,r,s,x)"
proof -
{
fix a
assume "a∈M"
with assms
have "(μ i. i∈ M ∧ is_ifrFb_body4(##M, G, r, s, z, i))= (μ i. is_ifrFb_body4(##M, G, r, s, z, i))" for z
using is_ifrFb_body4_closed[of G r s z]
by (rule_tac Least_cong[of "λi. i∈M ∧ is_ifrFb_body4(##M,G,r,s,z,i)"]) auto
moreover
have "(μ i. is_ifrFb_body4(##M, G, r, s, z, i))= (μ i. ifrFb_body4(G, r, s, z, i))" if "z∈M" for z
proof (rule_tac Least_cong[of "λi. is_ifrFb_body4(##M,G,r,s,z,i)" "λi. ifrFb_body4(G,r,s,z,i)"])
fix y
from assms ‹a∈M› ‹z∈M›
show "is_ifrFb_body4(##M, G, r, s, z, y) ⟷ ifrFb_body4(G, r, s, z, y)"
using If_abs apply_0
unfolding ifrFb_body4_def is_ifrFb_body4_def
apply (cases "y∈M"; cases "y∈range(s)"; cases "r=0"; cases "y∈domain(G)";
auto dest:transM split del: split_if del:iffI)
by (auto simp flip:setclass_iff; (force simp only: fun_apply_def setclass_iff))
(auto simp flip:setclass_iff simp: fun_apply_def )
qed
moreover from ‹a∈M›
have "least(##M, λi. i ∈ M ∧ is_ifrFb_body4(##M, G, r, s, z, i), a)
⟷ a = (μ i. i∈ M ∧ is_ifrFb_body4(##M, G, r, s, z,i))" for z
using If_abs least_abs'[of "λi. (##M)(i) ∧ is_ifrFb_body4(##M,G,r,s,z,i)" a]
by simp
ultimately
have "z∈M ⟹ least(##M, λi. i ∈ M ∧ is_ifrFb_body4(##M, G, r, s, z, i), a)
⟷ a = (μ i. ifrFb_body4(G, r, s, z,i))" for z
by simp
}
with assms
show ?thesis
using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
unfolding ifrangeF_body4_def is_ifrangeF_body4_def
by (auto dest:transM)
qed
lemma (in M_ZF1_trans) separation_ifrangeF_body4:
"(##M)(A) ⟹ (##M)(G) ⟹ (##M)(b) ⟹ (##M)(f) ⟹
separation(##M, λy. ∃x∈A. y = ⟨x, μ i. x ∈ if_range_F_else_F((`)(G), b, f, i)⟩)"
using separation_is_ifrangeF_body4 ifrangeF_body4_abs
separation_cong[where P="is_ifrangeF_body4(##M,A,G,b,f)" and M="##M",THEN iffD1]
unfolding ifrangeF_body4_def if_range_F_def if_range_F_else_F_def ifrFb_body4_def
by simp
definition ifrFb_body5 where
"ifrFb_body5(G,b,f,x,i) ≡ x ∈
(if b = 0 then if i ∈ range(f) then {xa ∈ G . converse(f) ` i ∈ xa} else 0 else {xa ∈ G . i ∈ xa})"
relativize functional "ifrFb_body5" "ifrFb_body5_rel"
relationalize "ifrFb_body5_rel" "is_ifrFb_body5"
synthesize "is_ifrFb_body5" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body5_fm"
definition ifrangeF_body5 :: "[i⇒o,i,i,i,i,i] ⇒ o" where
"ifrangeF_body5(M,A,G,b,f) ≡ λy. ∃x∈A. y = ⟨x,μ i. ifrFb_body5(G,b,f,x,i)⟩"
relativize functional "ifrangeF_body5" "ifrangeF_body5_rel"
relationalize "ifrangeF_body5_rel" "is_ifrangeF_body5"
synthesize "is_ifrangeF_body5" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body5_fm"
lemma (in M_Z_trans) separation_is_ifrangeF_body5:
"(##M)(A) ⟹ (##M)(G) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation(##M, is_ifrangeF_body5(##M,A,G,r,s))"
using separation_in_ctm[where φ="is_ifrangeF_body5_fm(1,2,3,4,0)" and env="[A,G,r,s]"]
zero_in_M arity_is_ifrangeF_body5_fm ord_simp_union is_ifrangeF_body5_fm_type
by simp
lemma (in M_basic) is_ifrFb_body5_closed: "M(G) ⟹ M(r) ⟹ M(s) ⟹ is_ifrFb_body5(M, G, r, s, x, i) ⟹ M(i)"
using If_abs
unfolding ifrangeF_body5_def is_ifrangeF_body5_def is_ifrFb_body5_def fun_apply_def
by (cases "i∈range(s)"; cases "r=0"; auto dest:transM)
lemma (in M_ZF1_trans) ifrangeF_body5_abs:
assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
shows "is_ifrangeF_body5(##M,A,G,r,s,x) ⟷ ifrangeF_body5(##M,A,G,r,s,x)"
proof -
{
fix a
assume "a∈M"
with assms
have "(μ i. i∈ M ∧ is_ifrFb_body5(##M, G, r, s, z, i))= (μ i. is_ifrFb_body5(##M, G, r, s, z, i))" for z
using is_ifrFb_body5_closed[of G r s z]
by (rule_tac Least_cong[of "λi. i∈M ∧ is_ifrFb_body5(##M,G,r,s,z,i)"]) auto
moreover
have "(μ i. is_ifrFb_body5(##M, G, r, s, z, i))= (μ i. ifrFb_body5(G, r, s, z, i))" if "z∈M" for z
proof (rule_tac Least_cong[of "λi. is_ifrFb_body5(##M,G,r,s,z,i)" "λi. ifrFb_body5(G,r,s,z,i)"])
fix y
from assms ‹a∈M› ‹z∈M›
show "is_ifrFb_body5(##M, G, r, s, z, y) ⟷ ifrFb_body5(G, r, s, z, y)"
using If_abs apply_0 separation_in_constant separation_in_rev
unfolding ifrFb_body5_def is_ifrFb_body5_def
apply (cases "y∈M"; cases "y∈range(s)"; cases "r=0"; cases "y∈domain(G)";
auto dest:transM split del: split_if del:iffI)
apply (auto simp flip:setclass_iff; (force simp only: fun_apply_def setclass_iff))
apply (auto simp flip:setclass_iff simp: fun_apply_def)
apply (auto dest:transM)
done
qed
moreover from ‹a∈M›
have "least(##M, λi. i ∈ M ∧ is_ifrFb_body5(##M, G, r, s, z, i), a)
⟷ a = (μ i. i∈ M ∧ is_ifrFb_body5(##M, G, r, s, z,i))" for z
using If_abs least_abs'[of "λi. (##M)(i) ∧ is_ifrFb_body5(##M,G,r,s,z,i)" a]
by simp
ultimately
have "z∈M ⟹ least(##M, λi. i ∈ M ∧ is_ifrFb_body5(##M, G, r, s, z, i), a)
⟷ a = (μ i. ifrFb_body5(G, r, s, z,i))" for z
by simp
}
with assms
show ?thesis
using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
unfolding ifrangeF_body5_def is_ifrangeF_body5_def
by (auto dest:transM)
qed
lemma (in M_ZF1_trans) separation_ifrangeF_body5:
"(##M)(A) ⟹ (##M)(G) ⟹ (##M)(b) ⟹ (##M)(f) ⟹
separation(##M, λy. ∃x∈A. y = ⟨x, μ i. x ∈ if_range_F_else_F(λx. {xa ∈ G . x ∈ xa}, b, f, i)⟩)"
using separation_is_ifrangeF_body5 ifrangeF_body5_abs
separation_cong[where P="is_ifrangeF_body5(##M,A,G,b,f)" and M="##M",THEN iffD1]
unfolding ifrangeF_body5_def if_range_F_def if_range_F_else_F_def ifrFb_body5_def
by simp
definition ifrFb_body6 where
"ifrFb_body6(G,b,f,x,i) ≡ x ∈
(if b = 0 then if i ∈ range(f) then {p∈G . domain(p) = converse(f) ` i} else 0 else {p∈G . domain(p) = i})"
relativize functional "ifrFb_body6" "ifrFb_body6_rel"
relationalize "ifrFb_body6_rel" "is_ifrFb_body6"
synthesize "is_ifrFb_body6" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body6_fm"
definition ifrangeF_body6 :: "[i⇒o,i,i,i,i,i] ⇒ o" where
"ifrangeF_body6(M,A,G,b,f) ≡ λy. ∃x∈A. y = ⟨x,μ i. ifrFb_body6(G,b,f,x,i)⟩"
relativize functional "ifrangeF_body6" "ifrangeF_body6_rel"
relationalize "ifrangeF_body6_rel" "is_ifrangeF_body6"
synthesize "is_ifrangeF_body6" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body6_fm"
lemma (in M_Z_trans) separation_is_ifrangeF_body6:
"(##M)(A) ⟹ (##M)(G) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation(##M, is_ifrangeF_body6(##M,A,G,r,s))"
using separation_in_ctm[where φ="is_ifrangeF_body6_fm(1,2,3,4,0)" and env="[A,G,r,s]"]
zero_in_M arity_is_ifrangeF_body6_fm ord_simp_union is_ifrangeF_body6_fm_type
by simp
lemma (in M_basic) ifrFb_body6_closed: "M(G) ⟹ M(r) ⟹ M(s) ⟹ ifrFb_body6(G, r, s, x, i) ⟷ M(i) ∧ ifrFb_body6(G, r, s, x, i)"
using If_abs
unfolding ifrangeF_body6_def is_ifrangeF_body6_def ifrFb_body6_def fun_apply_def
by (cases "i∈range(s)"; cases "r=0"; auto dest:transM)
lemma (in M_basic) is_ifrFb_body6_closed: "M(G) ⟹ M(r) ⟹ M(s) ⟹ is_ifrFb_body6(M, G, r, s, x, i) ⟹ M(i)"
using If_abs
unfolding ifrangeF_body6_def is_ifrangeF_body6_def is_ifrFb_body6_def fun_apply_def
by (cases "i∈range(s)"; cases "r=0"; auto dest:transM)
lemma (in M_ZF1_trans) ifrangeF_body6_abs:
assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
shows "is_ifrangeF_body6(##M,A,G,r,s,x) ⟷ ifrangeF_body6(##M,A,G,r,s,x)"
proof -
{
fix a
assume "a∈M"
with assms
have "(μ i. i∈ M ∧ is_ifrFb_body6(##M, G, r, s, z, i))= (μ i. is_ifrFb_body6(##M, G, r, s, z, i))" for z
using is_ifrFb_body6_closed[of G r s z]
by (rule_tac Least_cong[of "λi. i∈M ∧ is_ifrFb_body6(##M,G,r,s,z,i)"]) auto
moreover
have "(μ i. i∈M ∧ is_ifrFb_body6(##M, G, r, s, z, i))= (μ i. i∈M ∧ ifrFb_body6(G, r, s, z, i))" if "z∈M" for z
proof (rule_tac Least_cong[of "λi. i∈M ∧ is_ifrFb_body6(##M,G,r,s,z,i)" "λi. i∈M ∧ ifrFb_body6(G,r,s,z,i)"])
fix y
from assms ‹a∈M› ‹z∈M›
show "y∈M ∧ is_ifrFb_body6(##M, G, r, s, z, y) ⟷ y∈M ∧ ifrFb_body6(G, r, s, z, y)"
using If_abs apply_0 separation_in_constant transitivity[of _ G]
separation_closed converse_closed apply_closed range_closed zero_in_M
separation_cong[OF eq_commute,THEN iffD1,OF domain_eq_separation]
unfolding ifrFb_body6_def is_ifrFb_body6_def
by auto
qed
moreover from ‹a∈M›
have "least(##M, λi. i ∈ M ∧ is_ifrFb_body6(##M, G, r, s, z, i), a)
⟷ a = (μ i. i∈ M ∧ is_ifrFb_body6(##M, G, r, s, z,i))" for z
using If_abs least_abs'[of "λi. (##M)(i) ∧ is_ifrFb_body6(##M,G,r,s,z,i)" a]
by simp
ultimately
have "z∈M ⟹ least(##M, λi. i ∈ M ∧ is_ifrFb_body6(##M, G, r, s, z, i), a)
⟷ a = (μ i. ifrFb_body6(G, r, s, z,i))" for z
using Least_cong[OF ifrFb_body6_closed[of G r s]] assms
by simp
}
with assms
show ?thesis
using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
unfolding ifrangeF_body6_def is_ifrangeF_body6_def
by (auto dest:transM)
qed
lemma (in M_ZF1_trans) separation_ifrangeF_body6:
"(##M)(A) ⟹ (##M)(G) ⟹ (##M)(b) ⟹ (##M)(f) ⟹
separation(##M,
λy. ∃x∈A. y = ⟨x, μ i. x ∈ if_range_F_else_F(λa. {p ∈ G . domain(p) = a}, b, f, i)⟩)"
using separation_is_ifrangeF_body6 ifrangeF_body6_abs
separation_cong[where P="is_ifrangeF_body6(##M,A,G,b,f)" and M="##M",THEN iffD1]
unfolding ifrangeF_body6_def if_range_F_def if_range_F_else_F_def ifrFb_body6_def
by simp
definition ifrFb_body7 where
"ifrFb_body7(B,D,A,b,f,x,i) ≡ x ∈
(if b = 0 then if i ∈ range(f) then
{d ∈ D . ∃r∈A. restrict(r, B) = converse(f) ` i ∧ d = domain(r)} else 0
else {d ∈ D . ∃r∈A. restrict(r, B) = i ∧ d = domain(r)})"
relativize functional "ifrFb_body7" "ifrFb_body7_rel"
relationalize "ifrFb_body7_rel" "is_ifrFb_body7"
synthesize "is_ifrFb_body7" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body7_fm"
definition ifrangeF_body7 :: "[i⇒o,i,i,i,i,i,i,i] ⇒ o" where
"ifrangeF_body7(M,A,B,D,G,b,f) ≡ λy. ∃x∈A. y = ⟨x,μ i. ifrFb_body7(B,D,G,b,f,x,i)⟩"
relativize functional "ifrangeF_body7" "ifrangeF_body7_rel"
relationalize "ifrangeF_body7_rel" "is_ifrangeF_body7"
synthesize "is_ifrangeF_body7" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body7_fm"
lemma (in M_Z_trans) separation_is_ifrangeF_body7:
"(##M)(A) ⟹ (##M)(B) ⟹ (##M)(D) ⟹ (##M)(G) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation(##M, is_ifrangeF_body7(##M,A,B,D,G,r,s))"
using separation_in_ctm[where φ="is_ifrangeF_body7_fm(1,2,3,4,5,6,0)" and env="[A,B,D,G,r,s]"]
zero_in_M arity_is_ifrangeF_body7_fm ord_simp_union is_ifrangeF_body7_fm_type
by simp
lemma (in M_basic) ifrFb_body7_closed: "M(B) ⟹ M(D) ⟹ M(G) ⟹ M(r) ⟹ M(s) ⟹
ifrFb_body7(B,D,G, r, s, x, i) ⟷ M(i) ∧ ifrFb_body7(B,D,G, r, s, x, i)"
using If_abs
unfolding ifrangeF_body7_def is_ifrangeF_body7_def ifrFb_body7_def fun_apply_def
by (cases "i∈range(s)"; cases "r=0"; auto dest:transM)
lemma (in M_basic) is_ifrFb_body7_closed: "M(B) ⟹ M(D) ⟹ M(G) ⟹ M(r) ⟹ M(s) ⟹
is_ifrFb_body7(M, B,D,G, r, s, x, i) ⟹ M(i)"
using If_abs
unfolding ifrangeF_body7_def is_ifrangeF_body7_def is_ifrFb_body7_def fun_apply_def
by (cases "i∈range(s)"; cases "r=0"; auto dest:transM)
lemma (in M_ZF1_trans) ifrangeF_body7_abs:
assumes "(##M)(A)" "(##M)(B)" "(##M)(D)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
shows "is_ifrangeF_body7(##M,A,B,D,G,r,s,x) ⟷ ifrangeF_body7(##M,A,B,D,G,r,s,x)"
proof -
from assms
have sep_dr: "y∈M ⟹ separation(##M, λd . ∃r∈M . r∈G ∧ y = restrict(r, B) ∧ d = domain(r))" for y
by(rule_tac separation_cong[where P'="λd . ∃r∈ M . r∈G ∧ y = restrict(r, B) ∧ d = domain(r)",THEN iffD1,OF _
separation_restrict_eq_dom_eq[rule_format,of G B y]],auto simp:transitivity[of _ G])
from assms
have sep_dr'': "y∈M ⟹ separation(##M, λd . ∃r∈M. r ∈ G ∧ d = domain(r) ∧ converse(s) ` y = restrict(r, B))" for y
by(rule_tac separation_cong[THEN iffD1,OF _ separation_restrict_eq_dom_eq[rule_format,of G B "converse(s) ` y "]],
auto simp:transitivity[of _ G] apply_closed[simplified] converse_closed[simplified])
{
fix a
assume "a∈M"
with assms
have "(μ i. i∈ M ∧ is_ifrFb_body7(##M, B,D,G, r, s, z, i))= (μ i. is_ifrFb_body7(##M,B,D, G, r, s, z, i))" for z
using is_ifrFb_body7_closed[of B D G r s z]
by (rule_tac Least_cong[of "λi. i∈M ∧ is_ifrFb_body7(##M,B,D,G,r,s,z,i)"]) auto
moreover from this
have "(μ i. i∈M ∧ is_ifrFb_body7(##M, B,D,G, r, s, z, i))= (μ i. i∈M ∧ ifrFb_body7(B,D,G, r, s, z, i))" if "z∈M" for z
proof (rule_tac Least_cong[of "λi. i∈M ∧ is_ifrFb_body7(##M,B,D,G,r,s,z,i)" "λi. i∈M ∧ ifrFb_body7(B,D,G,r,s,z,i)"])
from assms ‹a∈M› ‹z∈M›
have "is_ifrFb_body7(##M, B,D,G, r, s, z, y) ⟷ ifrFb_body7(B,D,G, r, s, z, y)" if "y∈M" for y
using If_abs apply_0
separation_closed converse_closed apply_closed range_closed zero_in_M
transitivity[of _ D] transitivity[of _ G] that sep_dr sep_dr''
unfolding ifrFb_body7_def is_ifrFb_body7_def
by auto
then
show " y ∈ M ∧ is_ifrFb_body7(##M, B, D, G, r, s, z, y) ⟷ y ∈ M ∧ ifrFb_body7(B, D, G, r, s, z, y)" for y
using conj_cong
by simp
qed
moreover from ‹a∈M›
have "least(##M, λi. i ∈ M ∧ is_ifrFb_body7(##M, B,D,G, r, s, z, i), a)
⟷ a = (μ i. i∈ M ∧ is_ifrFb_body7(##M,B,D,G, r, s, z,i))" for z
using If_abs least_abs'[of "λi. (##M)(i) ∧ is_ifrFb_body7(##M,B,D,G,r,s,z,i)" a]
by simp
ultimately
have "z∈M ⟹ least(##M, λi. i ∈ M ∧ is_ifrFb_body7(##M,B,D,G, r, s, z, i), a)
⟷ a = (μ i. ifrFb_body7(B,D,G, r, s, z,i))" for z
using Least_cong[OF ifrFb_body7_closed[of B D G r s]] assms
by simp
}
with assms
show ?thesis
using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
unfolding ifrangeF_body7_def is_ifrangeF_body7_def
by (auto dest:transM)
qed
lemma (in M_ZF1_trans) separation_ifrangeF_body7:
"(##M)(A) ⟹ (##M)(B) ⟹ (##M)(D) ⟹ (##M)(G) ⟹ (##M)(b) ⟹ (##M)(f) ⟹
separation(##M,
λy. ∃x∈A. y = ⟨x, μ i. x ∈ if_range_F_else_F(drSR_Y(B, D, G), b, f, i)⟩)"
using separation_is_ifrangeF_body7 ifrangeF_body7_abs drSR_Y_equality
separation_cong[where P="is_ifrangeF_body7(##M,A,B,D,G,b,f)" and M="##M",THEN iffD1]
unfolding ifrangeF_body7_def if_range_F_def if_range_F_else_F_def ifrFb_body7_def
by simp
definition omfunspace :: "[i,i] ⇒ o" where
"omfunspace(B) ≡ λz. ∃x. ∃n∈ω. z∈x ∧ x = n→B"
relativize functional "omfunspace" "omfunspace_rel"
relationalize "omfunspace_rel" "is_omfunspace"
synthesize "is_omfunspace" from_definition assuming "nonempty"
arity_theorem for "is_omfunspace_fm"
context M_pre_seqspace
begin
is_iff_rel for "omfunspace"
using is_function_space_iff
unfolding omfunspace_rel_def is_omfunspace_def
by (simp add:absolut)
end
context M_ZF1_trans
begin
lemma separation_omfunspace:
assumes "(##M)(B)"
shows "separation(##M, λz. ∃x[##M]. ∃n[##M]. n ∈ ω ∧ z ∈ x ∧ x = n →⇗M⇖ B)"
using assms separation_in_ctm[where env="[B]" and φ="is_omfunspace_fm(1,0)"
and Q="is_omfunspace(##M,B)"]
nonempty is_omfunspace_iff[of B, THEN separation_cong, of "##M"]
arity_is_omfunspace_fm is_omfunspace_fm_type
unfolding omfunspace_rel_def
by (auto simp add:ord_simp_union)
end
sublocale M_ZF1_trans ⊆ M_seqspace "##M"
using separation_omfunspace by unfold_locales
definition cdltgamma :: "[i,i] ⇒ o" where
"cdltgamma(γ) ≡ λZ . |Z| < γ"
relativize functional "cdltgamma" "cdltgamma_rel"
relationalize "cdltgamma_rel" "is_cdltgamma"
synthesize "is_cdltgamma" from_definition assuming "nonempty"
arity_theorem for "is_cdltgamma_fm"
definition cdeqgamma :: "[i] ⇒ o" where
"cdeqgamma ≡ λZ . |fst(Z)| = snd(Z)"
relativize functional "cdeqgamma" "cdeqgamma_rel"
relationalize "cdeqgamma_rel" "is_cdeqgamma"
synthesize "is_cdeqgamma" from_definition assuming "nonempty"
arity_theorem for "is_cdeqgamma_fm"
context M_Perm
begin
is_iff_rel for "cdltgamma"
using is_cardinal_iff
unfolding cdltgamma_rel_def is_cdltgamma_def
by (simp add:absolut)
is_iff_rel for "cdeqgamma"
using is_cardinal_iff fst_rel_abs snd_rel_abs
unfolding cdeqgamma_rel_def is_cdeqgamma_def
by (auto simp add:absolut)
lemma is_cdeqgamma_iff_split: "M(Z) ⟹ cdeqgamma_rel(M, Z) ⟷ (λ⟨x,y⟩. |x|⇗M⇖ = y)(Z)"
using fst_rel_abs snd_rel_abs
unfolding cdeqgamma_rel_def split_def
by simp
end
context M_ZF1_trans
begin
lemma separation_cdltgamma:
assumes "(##M)(γ)"
shows "separation(##M, λZ . cardinal_rel(##M,Z) < γ)"
using assms separation_in_ctm[where env="[γ]" and φ="is_cdltgamma_fm(1,0)"
and Q="cdltgamma_rel(##M,γ)"]
nonempty is_cdltgamma_iff[of γ] arity_is_cdltgamma_fm is_cdltgamma_fm_type
unfolding cdltgamma_rel_def
by (auto simp add:ord_simp_union)
lemma separation_cdeqgamma:
shows "separation(##M, λZ. (λ⟨x,y⟩ . cardinal_rel(##M,x) = y)(Z))"
using separation_in_ctm[where env="[]" and φ="is_cdeqgamma_fm(0)"
and Q="cdeqgamma_rel(##M)"] is_cdeqgamma_iff_split
nonempty is_cdeqgamma_iff arity_is_cdeqgamma_fm is_cdeqgamma_fm_type
separation_cong[OF is_cdeqgamma_iff_split, of "##M"]
unfolding cdeqgamma_rel_def
by (simp add:ord_simp_union)
end
end