Theory ZF_Trans_Interpretations
theory ZF_Trans_Interpretations
imports
Cohen_Posets_Relative
Forcing_Main
Separation_Instances
Replacement_Instances
begin
lemmas (in M_ZF_trans) separation_instances =
separation_well_ord
separation_obase_equals separation_is_obase
separation_PiP_rel separation_surjP_rel
separation_id_body separation_rvimage_body
separation_radd_body separation_rmult_body
separation_ord_iso_body
lemma (in M_ZF_trans) lam_replacement_inj_rel :
shows
"lam_replacement(##M, λp. inj⇗##M⇖(fst(p),snd(p)))"
using lam_replacement_iff_lam_closed[THEN iffD2,of "λp. inj⇗M⇖(fst(p),snd(p))"]
LambdaPair_in_M[where φ="is_inj_fm(0,1,2)" and is_f="is_inj(##M)" and env="[]",OF
is_inj_fm_type _ is_inj_iff_sats[symmetric] inj_rel_iff,simplified]
arity_is_inj_fm[of 0 1 2] ord_simp_union transitivity fst_snd_closed
inj_rel_closed zero_in_M
by simp
definition is_order_body
where "is_order_body(M,X,x,z) ≡ ∃A[M]. cartprod(M,X,X,A) ∧ subset(M,x,A) ∧ M(z) ∧ M(x) ∧
is_well_ord(M,X, x) ∧ is_ordertype(M,X, x,z)"
synthesize "is_order_body" from_definition assuming "nonempty"
arity_theorem for "is_transitive_fm"
arity_theorem for "is_linear_fm"
arity_theorem for "is_wellfounded_on_fm"
arity_theorem for "is_well_ord_fm"
arity_theorem for "pred_set_fm"
arity_theorem for "image_fm"
definition omap_wfrec_body where
"omap_wfrec_body(A,r) ≡ (⋅∃⋅image_fm(2, 0, 1) ∧
pred_set_fm
(succ(succ(succ(succ(succ(succ(succ(succ(succ(A))))))))), 3,
succ(succ(succ(succ(succ(succ(succ(succ(succ(r))))))))), 0) ⋅⋅)"
lemma type_omap_wfrec_body_fm :"A∈nat ⟹ r∈nat ⟹ omap_wfrec_body(A,r)∈formula"
unfolding omap_wfrec_body_def by simp
lemma arity_aux : "A∈nat ⟹ r∈nat ⟹ arity(omap_wfrec_body(A,r)) = (9#+A) ∪ (9#+r)"
unfolding omap_wfrec_body_def
using arity_image_fm arity_pred_set_fm pred_Un_distrib union_abs2[of 3] union_abs1
by (simp,auto simp add:Un_assoc[symmetric] union_abs1)
lemma arity_omap_wfrec : "A∈nat ⟹ r∈nat ⟹
arity(is_wfrec_fm(omap_wfrec_body(A,r),succ(succ(succ(r))), 1, 0)) =
(4#+A) ∪ (4#+r)"
using Arities.arity_is_wfrec_fm[OF _ _ _ _ _ arity_aux,of A r "3#+r" 1 0] pred_Un_distrib
union_abs1 union_abs2 type_omap_wfrec_body_fm
by auto
lemma arity_isordermap : "A∈nat ⟹ r∈nat ⟹d∈nat⟹
arity(is_ordermap_fm(A,r,d)) = succ(d) ∪ (succ(A) ∪ succ(r))"
unfolding is_ordermap_fm_def
using arity_lambda_fm[where i="(4#+A) ∪ (4#+r)",OF _ _ _ _ arity_omap_wfrec,
unfolded omap_wfrec_body_def] pred_Un_distrib union_abs1
by auto
lemma arity_is_ordertype : "A∈nat ⟹ r∈nat ⟹d∈nat⟹
arity(is_ordertype_fm(A,r,d)) = succ(d) ∪ (succ(A) ∪ succ(r))"
unfolding is_ordertype_fm_def
using arity_isordermap arity_image_fm pred_Un_distrib
by auto
arity_theorem for "is_order_body_fm"
lemma arity_is_order_body : "arity(is_order_body_fm(2,0,1)) = 3"
using arity_is_order_body_fm arity_is_ordertype ord_simp_union
by simp
lemma (in M_ZF_trans) replacement_is_order_body :
"X∈M ⟹ strong_replacement(##M, is_order_body(##M,X))"
apply(rule_tac strong_replacement_cong[
where P="λ x f. M,[x,f,X] ⊨ is_order_body_fm(2,0,1)",THEN iffD1])
apply(rule_tac is_order_body_iff_sats[where env="[_,_,X]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac replacement_ax[where env="[X]",simplified])
apply(simp_all add: arity_is_order_body )
done
lemma (in M_pre_cardinal_arith) is_order_body_abs :
"M(X) ⟹ M(x) ⟹ M(z) ⟹ is_order_body(M, X, x, z) ⟷
M(z) ∧ M(x) ∧ x∈Pow_rel(M,X×X) ∧ well_ord(X, x) ∧ z = ordertype(X, x)"
using well_ord_abs is_well_ord_iff_wellordered is_ordertype_iff' ordertype_rel_abs
well_ord_is_linear subset_abs Pow_rel_char
unfolding is_order_body_def
by simp
definition H_order_pred where
"H_order_pred(A,r) ≡ λx f . f `` Order.pred(A, x, r)"
relationalize "H_order_pred" "is_H_order_pred"
lemma (in M_basic) H_order_pred_abs :
"M(A) ⟹ M(r) ⟹ M(x) ⟹ M(f) ⟹ M(z) ⟹
is_H_order_pred(M,A,r,x,f,z) ⟷ z = H_order_pred(A,r,x,f)"
unfolding is_H_order_pred_def H_order_pred_def
by simp
synthesize "is_H_order_pred" from_definition assuming "nonempty"
definition order_pred_wfrec_body where
"order_pred_wfrec_body(M,A,r,z,x) ≡ ∃y[M].
pair(M, x, y, z) ∧
(∃f[M].
(∀z[M].
z ∈ f ⟷
(∃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, r, sx, r_sx) ∧
restriction(M, f, r_sx, f_r_sx) ∧
xaa ∈ r ∧ (∃a[M]. image(M, f_r_sx, a, y) ∧ pred_set(M, A, xa, r, a)))) ∧
(∃a[M]. image(M, f, a, y) ∧ pred_set(M, A, x, r, a)))"
synthesize "order_pred_wfrec_body" from_definition
arity_theorem for "order_pred_wfrec_body_fm"
lemma (in M_ZF_trans) wfrec_replacement_order_pred :
"A∈M ⟹ r∈M ⟹ wfrec_replacement(##M, λx g z. is_H_order_pred(##M,A,r,x,g,z) , r)"
unfolding wfrec_replacement_def is_wfrec_def M_is_recfun_def is_H_order_pred_def
apply(rule_tac strong_replacement_cong[
where P="λ x f. M,[x,f,r,A] ⊨ order_pred_wfrec_body_fm(3,2,1,0)",THEN iffD1])
apply(subst order_pred_wfrec_body_def[symmetric])
apply(rule_tac order_pred_wfrec_body_iff_sats[where env="[_,_,r,A]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac replacement_ax[where env="[r,A]",simplified])
apply(simp_all add: arity_order_pred_wfrec_body_fm ord_simp_union)
done
lemma (in M_ZF_trans) wfrec_replacement_order_pred' :
"A∈M ⟹ r∈M ⟹ wfrec_replacement(##M, λx g z. z = H_order_pred(A,r,x,g) , r)"
using wfrec_replacement_cong[OF H_order_pred_abs[of A r,rule_format] refl,THEN iffD1,
OF _ _ _ _ _ wfrec_replacement_order_pred[of A r]]
by simp
sublocale M_ZF_trans ⊆ M_pre_cardinal_arith "##M"
using separation_instances wfrec_replacement_order_pred'[unfolded H_order_pred_def]
replacement_is_order_eq_map[unfolded order_eq_map_def] banach_replacement
by unfold_locales simp_all
lemma (in M_ZF_trans) replacement_ordertype :
"X∈M ⟹ strong_replacement(##M, λx z. z ∈ M ∧ x ∈ M ∧ x ∈ Pow⇗M⇖(X × X) ∧ well_ord(X, x) ∧ z = ordertype(X, x))"
using strong_replacement_cong[THEN iffD1,OF _ replacement_is_order_body,simplified] is_order_body_abs
unfolding is_order_body_def
by simp
lemma arity_is_jump_cardinal_body : "arity(is_jump_cardinal_body'_fm(0,1)) = 2"
unfolding is_jump_cardinal_body'_fm_def
using arity_is_ordertype arity_is_well_ord_fm arity_is_Pow_fm arity_cartprod_fm
arity_Replace_fm[where i=5] ord_simp_union
by simp
lemma (in M_ZF_trans) replacement_is_jump_cardinal_body :
"strong_replacement(##M, is_jump_cardinal_body'(##M))"
apply(rule_tac strong_replacement_cong[
where P="λ x f. M,[x,f] ⊨ is_jump_cardinal_body'_fm(0,1)",THEN iffD1])
apply(rule_tac is_jump_cardinal_body'_iff_sats[where env="[_,_]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac replacement_ax[where env="[]",simplified])
apply(simp_all add: arity_is_jump_cardinal_body )
done
lemma (in M_pre_cardinal_arith) univalent_aux2 : "M(X) ⟹ univalent(M,Pow_rel(M,X×X),
λr z. M(z) ∧ M(r) ∧ is_well_ord(M, X, r) ∧ is_ordertype(M, X, r, z))"
using is_well_ord_iff_wellordered
is_ordertype_iff[of _ X]
trans_on_subset[OF well_ord_is_trans_on]
well_ord_is_wf[THEN wf_on_subset_A] mem_Pow_rel_abs
unfolding univalent_def
by (simp)
lemma (in M_pre_cardinal_arith) is_jump_cardinal_body_abs :
"M(X) ⟹ M(c) ⟹ is_jump_cardinal_body'(M, X, c) ⟷ c = jump_cardinal_body'_rel(M,X)"
using well_ord_abs is_well_ord_iff_wellordered is_ordertype_iff' ordertype_rel_abs
well_ord_is_linear subset_abs Pow_rel_iff Replace_abs[of "Pow_rel(M,X×X)",OF _ _
univalent_aux2]
unfolding is_jump_cardinal_body'_def jump_cardinal_body'_rel_def
by simp
lemma (in M_ZF_trans) replacement_jump_cardinal_body :
"strong_replacement(##M, λx z. z ∈ M ∧ x ∈ M ∧ z = jump_cardinal_body(##M, x))"
using strong_replacement_cong[THEN iffD1,OF _ replacement_is_jump_cardinal_body,simplified]
jump_cardinal_body_eq is_jump_cardinal_body_abs
by simp
sublocale M_ZF_trans ⊆ M_pre_aleph "##M"
using replacement_ordertype replacement_jump_cardinal_body HAleph_wfrec_repl
lam_replacement_min[unfolded lam_replacement_def]
lam_replacement_imp_strong_replacement lam_replacement_vimage_sing_fun
lam_replacement_Sigfun[OF lam_replacement_vimage_sing_fun]
vimage_closed singleton_closed surj_imp_inj_replacement1
by unfold_locales (simp_all add: transrec_replacement_def
wfrec_replacement_def is_wfrec_def M_is_recfun_def flip:setclass_iff)
arity_theorem intermediate for "is_HAleph_fm"
lemma arity_is_HAleph_fm : "arity(is_HAleph_fm(2, 1, 0)) = 3"
using arity_fun_apply_fm[of "11" 0 1,simplified]
arity_is_HAleph_fm' arity_ordinal_fm arity_is_If_fm
arity_empty_fm arity_is_Limit_fm
arity_is_If_fm
arity_is_Limit_fm arity_empty_fm
arity_Replace_fm[where i="12" and v=10 and n=3]
pred_Un_distrib ord_simp_union
by simp
lemma arity_is_Aleph : "arity(is_Aleph_fm(0, 1)) = 2"
unfolding is_Aleph_fm_def
using arity_transrec_fm[OF _ _ _ _ arity_is_HAleph_fm] ord_simp_union
by simp
lemma (in M_ZF_trans) replacement_is_aleph :
"strong_replacement(##M, λx y. Ord(x) ∧ is_Aleph(##M,x,y))"
apply(rule_tac strong_replacement_cong[
where P="λ x y. M,[x,y] ⊨ And(ordinal_fm(0),is_Aleph_fm(0,1))",THEN iffD1])
apply (auto simp add: ordinal_iff_sats[where env="[_,_]",symmetric])
apply(rule_tac is_Aleph_iff_sats[where env="[_,_]",THEN iffD2],simp_all add:zero_in_M)
apply(rule_tac is_Aleph_iff_sats[where env="[_,_]",THEN iffD1],simp_all add:zero_in_M)
apply(rule_tac replacement_ax[where env="[]",simplified])
apply(simp_all add:arity_is_Aleph ord_simp_union is_Aleph_fm_type)
done
lemma (in M_ZF_trans) replacement_aleph_rel :
shows "strong_replacement(##M, λx y. Ord(x) ∧ y = ℵ⇘x⇙⇗M⇖)"
using strong_replacement_cong[THEN iffD2,OF _ replacement_is_aleph,where P1="λx y . Ord(x) ∧ y=Aleph_rel(##M,x)"]
is_Aleph_iff
by auto
sublocale M_ZF_trans ⊆ M_aleph "##M"
by (unfold_locales,simp add: replacement_aleph_rel)
sublocale M_ZF_trans ⊆ M_FiniteFun "##M"
using separation_supset_body separation_cons_like_rel
replacement_range replacement_omega_funspace
by (unfold_locales,simp_all)
sublocale M_ZFC_trans ⊆ M_AC "##M"
using choice_ax by (unfold_locales, simp_all)
sublocale M_ZFC_trans ⊆ M_cardinal_AC "##M" ..
definition toplevel1_body :: "[i,i,i] ⇒ o" where
"toplevel1_body(Q,x) ≡ λa. ∀s∈x. ⟨s, a⟩ ∈ Q"
relativize functional "toplevel1_body" "toplevel1_body_rel"
relationalize "toplevel1_body_rel" "is_toplevel1_body"
synthesize "is_toplevel1_body" from_definition assuming "nonempty"
arity_theorem for "is_toplevel1_body_fm"
lemma (in M_ZF_trans) separation_is_toplevel1_body :
"(##M)(A) ⟹ (##M)(B) ⟹ separation(##M, is_toplevel1_body(##M,A,B))"
apply(rule_tac separation_cong[
where P="λ x . M,[x,A,B] ⊨ is_toplevel1_body_fm(1,2,0)",THEN iffD1])
apply(rule_tac is_toplevel1_body_iff_sats[where env="[_,A,B]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac separation_ax[where env="[A,B]",simplified])
apply(simp_all add:arity_is_toplevel1_body_fm ord_simp_union is_toplevel1_body_fm_type)
done
lemma (in M_ZF_trans) toplevel1_body_abs :
assumes "(##M)(A)" "(##M)(B)" "(##M)(x)"
shows "is_toplevel1_body(##M,A,B,x) ⟷ toplevel1_body(A,B,x)"
using assms pair_in_M_iff apply_closed transM
unfolding toplevel1_body_def is_toplevel1_body_def
by (auto)
lemma (in M_ZF_trans) separation_toplevel1_body :
"(##M)(Q) ⟹ (##M)(x) ⟹ separation(##M, λa. ∀s∈x. ⟨s, a⟩ ∈ Q)"
using separation_is_toplevel1_body toplevel1_body_abs
separation_cong[where P="is_toplevel1_body(##M,Q,x)" and M="##M",THEN iffD1]
unfolding toplevel1_body_def
by simp
definition toplevel2_body :: "[i,i] ⇒ o" where
"toplevel2_body(x) ≡ λa. |a| < x"
relativize functional "toplevel2_body" "toplevel2_body_rel"
relationalize "toplevel2_body_rel" "is_toplevel2_body"
synthesize "is_toplevel2_body" from_definition assuming "nonempty"
arity_theorem for "is_toplevel2_body_fm"
lemma (in M_ZF_trans) separation_is_toplevel2_body :
"(##M)(A) ⟹ separation(##M, is_toplevel2_body(##M,A))"
apply(rule_tac separation_cong[
where P="λ x . M,[x,A] ⊨ is_toplevel2_body_fm(1,0)",THEN iffD1])
apply(rule_tac is_toplevel2_body_iff_sats[where env="[_,A]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac separation_ax[where env="[A]",simplified])
apply(simp_all add:arity_is_toplevel2_body_fm ord_simp_union is_toplevel2_body_fm_type)
done
lemma (in M_ZF_trans) toplevel2_body_abs :
assumes "(##M)(A)" "(##M)(x)"
shows "is_toplevel2_body(##M,A,x) ⟷ toplevel2_body_rel(##M,A,x)"
using assms pair_in_M_iff apply_closed transM is_cardinal_iff
cardinal_rel_closed
unfolding toplevel2_body_rel_def is_toplevel2_body_def
by (auto simp:absolut)
lemma (in M_ZF_trans) separation_toplevel2_body :
"(##M)(x) ⟹ separation(##M, λa. |a|⇗M⇖ < x)"
using separation_is_toplevel2_body toplevel2_body_abs
separation_cong[where P="is_toplevel2_body(##M,x)" and M="##M",THEN iffD1]
unfolding toplevel2_body_rel_def
by simp
definition toplevel3_body :: "i ⇒ o" where
"toplevel3_body ≡ λx. ∃a b. x = ⟨a, b⟩ ∧ a ≠ b"
relativize functional "toplevel3_body" "toplevel3_body_rel"
relationalize "toplevel3_body_rel" "is_toplevel3_body"
synthesize "is_toplevel3_body" from_definition
arity_theorem for "is_toplevel3_body_fm"
lemma (in M_ZF_trans) separation_is_toplevel3_body :
"separation(##M, is_toplevel3_body(##M))"
apply(rule_tac separation_cong[
where P="λ x . M,[x] ⊨ is_toplevel3_body_fm(0)",THEN iffD1])
apply(rule_tac is_toplevel3_body_iff_sats[where env="[_]",symmetric])
apply(simp_all)
apply(rule_tac separation_ax[where env="[]",simplified])
apply(simp_all add:arity_is_toplevel3_body_fm ord_simp_union is_toplevel3_body_fm_type)
done
lemma (in M_ZF_trans) toplevel3_body_abs :
assumes "(##M)(x)"
shows "is_toplevel3_body(##M,x) ⟷ toplevel3_body(x)"
using assms pair_in_M_iff apply_closed
unfolding toplevel3_body_def is_toplevel3_body_def
by (auto)
lemma (in M_ZF_trans) separation_toplevel3_body :
"separation(##M, λx . ∃a b. x = ⟨a, b⟩ ∧ a ≠ b)"
using separation_is_toplevel3_body toplevel3_body_abs
separation_cong[where P="is_toplevel3_body(##M)" and M="##M",THEN iffD1]
unfolding toplevel3_body_def
by simp
definition toplevel4_body :: "[i,i] ⇒ o" where
"toplevel4_body(R) ≡ λz. ∃a b. z = ⟨a, b⟩ ∧ a ∩ b = R"
relativize functional "toplevel4_body" "toplevel4_body_rel"
relationalize "toplevel4_body_rel" "is_toplevel4_body"
synthesize "is_toplevel4_body" from_definition assuming "nonempty"
arity_theorem for "is_toplevel4_body_fm"
lemma (in M_ZF_trans) separation_is_toplevel4_body :
"(##M)(A) ⟹ separation(##M, is_toplevel4_body(##M,A))"
apply(rule_tac separation_cong[
where P="λ x . M,[x,A] ⊨ is_toplevel4_body_fm(1,0)",THEN iffD1])
apply(rule_tac is_toplevel4_body_iff_sats[where env="[_,A]",symmetric])
apply(simp_all add:nonempty[simplified])
apply(rule_tac separation_ax[where env="[A]",simplified])
apply(simp_all add:arity_is_toplevel4_body_fm ord_simp_union is_toplevel4_body_fm_type)
done
lemma (in M_ZF_trans) toplevel4_body_abs :
assumes "(##M)(R)" "(##M)(x)"
shows "is_toplevel4_body(##M,R,x) ⟷ toplevel4_body(R,x)"
using assms pair_in_M_iff is_Int_abs
unfolding toplevel4_body_def is_toplevel4_body_def
by (auto)
lemma (in M_ZF_trans) separation_toplevel4_body :
"(##M)(R) ⟹ separation
(##M, λx. ∃a b. x = ⟨a, b⟩ ∧ a ∩ b = R)"
using separation_is_toplevel4_body toplevel4_body_abs
unfolding toplevel4_body_def
by (rule_tac separation_cong[
where P="is_toplevel4_body(##M,R)",THEN iffD1])
definition toplevel5_body :: "[i,i] ⇒ o" where
"toplevel5_body(R) ≡ λx. domain(x) ∈ R"
relativize functional "toplevel5_body" "toplevel5_body_rel"
relationalize "toplevel5_body_rel" "is_toplevel5_body"
synthesize "is_toplevel5_body" from_definition assuming "nonempty"
arity_theorem for "is_toplevel5_body_fm"
lemma (in M_ZF_trans) separation_is_toplevel5_body :
"(##M)(A) ⟹ separation(##M, is_toplevel5_body(##M,A))"
apply(rule_tac separation_cong[
where P="λ x . M,[x,A] ⊨ is_toplevel5_body_fm(1,0)",THEN iffD1])
apply(rule_tac is_toplevel5_body_iff_sats[where env="[_,A]",symmetric])
apply(simp_all add:nonempty[simplified])
apply(rule_tac separation_ax[where env="[A]",simplified])
apply(simp_all add:arity_is_toplevel5_body_fm ord_simp_union is_toplevel5_body_fm_type)
done
lemma (in M_ZF_trans) toplevel5_body_abs :
assumes "(##M)(R)" "(##M)(x)"
shows "is_toplevel5_body(##M,R,x) ⟷ toplevel5_body(R,x)"
using assms pair_in_M_iff is_Int_abs
unfolding toplevel5_body_def is_toplevel5_body_def
by (auto simp:domain_closed[simplified])
lemma (in M_ZF_trans) separation_toplevel5_body :
"(##M)(R) ⟹ separation
(##M, λx. domain(x) ∈ R)"
using separation_is_toplevel5_body toplevel5_body_abs
unfolding toplevel5_body_def
by (rule_tac separation_cong[
where P="is_toplevel5_body(##M,R)",THEN iffD1])
definition toplevel7_body :: "[i,i,i] ⇒ o" where
"toplevel7_body(Q,x) ≡ λa. restrict(a, Q) = x"
relativize functional "toplevel7_body" "toplevel7_body_rel"
relationalize "toplevel7_body_rel" "is_toplevel7_body"
synthesize "is_toplevel7_body" from_definition assuming "nonempty"
arity_theorem for "is_toplevel7_body_fm"
lemma (in M_ZF_trans) separation_is_toplevel7_body :
"(##M)(A) ⟹ (##M)(B) ⟹ separation(##M, is_toplevel7_body(##M,A,B))"
apply(rule_tac separation_cong[
where P="λ x . M,[x,A,B] ⊨ is_toplevel7_body_fm(1,2,0)",THEN iffD1])
apply(rule_tac is_toplevel7_body_iff_sats[where env="[_,A,B]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac separation_ax[where env="[A,B]",simplified])
apply(simp_all add:arity_is_toplevel7_body_fm ord_simp_union is_toplevel7_body_fm_type)
done
lemma (in M_ZF_trans) toplevel7_body_abs :
assumes "(##M)(A)" "(##M)(B)" "(##M)(x)"
shows "is_toplevel7_body(##M,A,B,x) ⟷ toplevel7_body(A,B,x)"
using assms pair_in_M_iff apply_closed transM
unfolding toplevel7_body_def is_toplevel7_body_def
by (auto)
lemma (in M_ZF_trans) separation_toplevel7_body :
"(##M)(Q) ⟹ (##M)(x) ⟹ separation(##M, λa. restrict(a, Q) = x)"
using separation_is_toplevel7_body toplevel7_body_abs
separation_cong[where P="is_toplevel7_body(##M,Q,x)" and M="##M",THEN iffD1]
unfolding toplevel7_body_def
by simp
definition toplevel8_body :: "[i,i] ⇒ o" where
"toplevel8_body(R) ≡ λz. R ∈ domain(z)"
relativize functional "toplevel8_body" "toplevel8_body_rel"
relationalize "toplevel8_body_rel" "is_toplevel8_body"
synthesize "is_toplevel8_body" from_definition assuming "nonempty"
arity_theorem for "is_toplevel8_body_fm"
lemma (in M_ZF_trans) separation_is_toplevel8_body :
"(##M)(A) ⟹ separation(##M, is_toplevel8_body(##M,A))"
apply(rule_tac separation_cong[
where P="λ x . M,[x,A] ⊨ is_toplevel8_body_fm(1,0)",THEN iffD1])
apply(rule_tac is_toplevel8_body_iff_sats[where env="[_,A]",symmetric])
apply(simp_all add:nonempty[simplified])
apply(rule_tac separation_ax[where env="[A]",simplified])
apply(simp_all add:arity_is_toplevel8_body_fm ord_simp_union is_toplevel8_body_fm_type)
done
lemma (in M_ZF_trans) toplevel8_body_abs :
assumes "(##M)(R)" "(##M)(x)"
shows "is_toplevel8_body(##M,R,x) ⟷ toplevel8_body(R,x)"
using assms pair_in_M_iff is_Int_abs
unfolding toplevel8_body_def is_toplevel8_body_def
by (auto simp:domain_closed[simplified])
lemma (in M_ZF_trans) separation_toplevel8_body :
"(##M)(R) ⟹ separation
(##M, λz. R ∈ domain(z))"
using separation_is_toplevel8_body toplevel8_body_abs
unfolding toplevel8_body_def
by (rule_tac separation_cong[
where P="is_toplevel8_body(##M,R)",THEN iffD1])
definition toplevel9_body :: "[i,i,i] ⇒ o" where
"toplevel9_body(Q,x) ≡ λz. ∃n∈ω. ⟨⟨Q, n⟩, 1⟩ ∈ z ∧ ⟨⟨x, n⟩, 0⟩ ∈ z"
relativize functional "toplevel9_body" "toplevel9_body_rel"
relationalize "toplevel9_body_rel" "is_toplevel9_body"
synthesize "is_toplevel9_body" from_definition assuming "nonempty"
arity_theorem for "is_toplevel9_body_fm"
lemma (in M_ZF_trans) separation_is_toplevel9_body :
"(##M)(A) ⟹ (##M)(B) ⟹ separation(##M, is_toplevel9_body(##M,A,B))"
apply(rule_tac separation_cong[
where P="λ x . M,[x,A,B] ⊨ is_toplevel9_body_fm(1,2,0)",THEN iffD1])
apply(rule_tac is_toplevel9_body_iff_sats[where env="[_,A,B]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac separation_ax[where env="[A,B]",simplified])
apply(simp_all add:arity_is_toplevel9_body_fm ord_simp_union is_toplevel9_body_fm_type)
done
lemma (in M_ZF_trans) toplevel9_body_abs :
assumes "(##M)(A)" "(##M)(B)" "(##M)(x)"
shows "is_toplevel9_body(##M,A,B,x) ⟷ toplevel9_body(A,B,x)"
using assms pair_in_M_iff apply_closed transM
unfolding toplevel9_body_def is_toplevel9_body_def
by (auto simp:nat_into_M[simplified] M_nat[simplified])
lemma (in M_ZF_trans) separation_toplevel9_body :
"(##M)(Q) ⟹ (##M)(x) ⟹ separation(##M, λz. ∃n∈ω. ⟨⟨Q, n⟩, 1⟩ ∈ z ∧ ⟨⟨x, n⟩, 0⟩ ∈ z)"
using separation_is_toplevel9_body toplevel9_body_abs
separation_cong[where P="is_toplevel9_body(##M,Q,x)" and M="##M",THEN iffD1]
unfolding toplevel9_body_def
by simp
definition toplevel10_body :: "[i,i,i] ⇒ o" where
"toplevel10_body(A,r) ≡ λy. ∃x∈A. y = ⟨x, restrict(x, r)⟩"
relativize functional "toplevel10_body" "toplevel10_body_rel"
relationalize "toplevel10_body_rel" "is_toplevel10_body"
synthesize "is_toplevel10_body" from_definition assuming "nonempty"
arity_theorem for "is_toplevel10_body_fm"
lemma (in M_ZF_trans) separation_is_toplevel10_body :
"(##M)(A) ⟹ (##M)(r) ⟹ separation(##M, is_toplevel10_body(##M,A,r))"
apply(rule_tac separation_cong[
where P="λ x . M,[x,A,r] ⊨ is_toplevel10_body_fm(1,2,0)",THEN iffD1])
apply(rule_tac is_toplevel10_body_iff_sats[where env="[_,A,r]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac separation_ax[where env="[A,r]",simplified])
apply(simp_all add:arity_is_toplevel10_body_fm ord_simp_union is_toplevel10_body_fm_type)
done
lemma (in M_ZF_trans) toplevel10_body_abs :
assumes "(##M)(A)" "(##M)(r)" "(##M)(x)"
shows "is_toplevel10_body(##M,A,r,x) ⟷ toplevel10_body(A,r,x)"
using assms pair_in_M_iff apply_closed transM
unfolding toplevel10_body_def is_toplevel10_body_def
by auto
lemma (in M_ZF_trans) separation_toplevel10_body :
"(##M)(A) ⟹ (##M)(r) ⟹ separation(##M, λy. ∃x∈A. y = ⟨x, restrict(x, r)⟩)"
using separation_is_toplevel10_body toplevel10_body_abs
separation_cong[where P="is_toplevel10_body(##M,A,r)" and M="##M",THEN iffD1]
unfolding toplevel10_body_def
by simp
definition toplevel11_body :: "[i,i] ⇒ o" where
"toplevel11_body(A) ≡ λp. (∀x∈A. (x ∈ snd(p) ⟷ domain(x) = fst(p)))"
relativize functional "toplevel11_body" "toplevel11_body_rel"
relationalize "toplevel11_body_rel" "is_toplevel11_body"
synthesize "is_toplevel11_body" from_definition assuming "nonempty"
arity_theorem for "is_toplevel11_body_fm"
lemma (in M_ZF_trans) separation_is_toplevel11_body :
"(##M)(A) ⟹ separation(##M, is_toplevel11_body(##M,A))"
apply(rule_tac separation_cong[
where P="λ x . M,[x,A] ⊨ is_toplevel11_body_fm(1,0)",THEN iffD1])
apply(rule_tac is_toplevel11_body_iff_sats[where env="[_,A]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac separation_ax[where env="[A]",simplified])
apply(simp_all add:arity_is_toplevel11_body_fm ord_simp_union is_toplevel11_body_fm_type)
done
lemma (in M_ZF_trans) toplevel11_body_abs :
assumes "(##M)(A)" "(##M)(x)"
shows "is_toplevel11_body(##M,A,x) ⟷ toplevel11_body(A,x)"
using assms domain_closed domain_abs zero_in_M transM[of _ A] transitivity
fst_snd_closed fst_abs snd_abs
unfolding toplevel11_body_def is_toplevel11_body_def
by auto
lemma (in M_ZF_trans) separation_toplevel11_body :
"(##M)(A) ⟹ separation(##M, λp. ∀x∈A. x ∈ snd(p) ⟷ domain(x) = fst(p))"
using separation_is_toplevel11_body toplevel11_body_abs
separation_cong[where P="is_toplevel11_body(##M,A)" and M="##M",THEN iffD1]
unfolding toplevel11_body_def
by simp
definition toplevel12_body
where "toplevel12_body(G,p) ≡ ∀x∈G. x ∈ snd(p) ⟷ fst(p) ∈ x"
relativize functional "toplevel12_body" "toplevel12_body_rel"
relationalize "toplevel12_body_rel" "is_toplevel12_body"
synthesize "is_toplevel12_body" from_definition
arity_theorem for "is_toplevel12_body_fm"
lemma (in M_ZF_trans) separation_is_toplevel12_body :
"(##M)(G) ⟹ separation(##M, is_toplevel12_body(##M,G))"
apply(rule_tac separation_cong[
where P="λ x . M,[x,G] ⊨ is_toplevel12_body_fm(1,0)",THEN iffD1])
apply(rule_tac is_toplevel12_body_iff_sats[where env="[_,G]",symmetric])
apply(simp_all)
apply(rule_tac separation_ax[where env="[G]",simplified])
apply(simp_all add:arity_is_toplevel12_body_fm ord_simp_union is_toplevel12_body_fm_type)
done
lemma (in M_ZF_trans) toplevel12_body_abs :
assumes "(##M)(G)" "(##M)(x)"
shows "is_toplevel12_body(##M,G,x) ⟷ toplevel12_body(G,x)"
using assms pair_in_M_iff fst_abs snd_abs transitivity fst_snd_closed
unfolding toplevel12_body_def is_toplevel12_body_def
by force
lemma (in M_ZF_trans) separation_toplevel12_body :
"(##M)(G) ⟹ separation
(##M, λp. ∀x∈G. x ∈ snd(p) ⟷ fst(p) ∈ x)"
using toplevel12_body_abs separation_is_toplevel12_body
unfolding toplevel12_body_def
by (rule_tac separation_cong[
where P="is_toplevel12_body(##M,G)",THEN iffD1])
end