Theory Interface
section‹Interface between set models and Constructibility›
text‹This theory provides an interface between Paulson's
relativization results and set models of ZFC. In particular,
it is used to prove that the locale \<^term>‹forcing_data› is
a sublocale of all relevant locales in \<^session>‹ZF-Constructible›
(\<^term>‹M_trivial›, \<^term>‹M_basic›, \<^term>‹M_eclose›, etc).
In order to interpret the locales in \<^session>‹ZF-Constructible› we
introduce new locales, each stronger than the previous one, assuming
only the instances of Replacement needed to interpret the subsequent
locales of that session. From the start we assume Separation for
every internalized formula (with one parameter, but this is not a
problem since we can use pairing).›
theory Interface
imports
Fm_Definitions
Transitive_Models.Cardinal_AC_Relative
begin
locale M_Z_basic =
fixes M
assumes
upair_ax: "upair_ax(##M)" and
Union_ax: "Union_ax(##M)" and
power_ax: "power_ax(##M)" and
extensionality:"extensionality(##M)" and
foundation_ax: "foundation_ax(##M)" and
infinity_ax: "infinity_ax(##M)" and
separation_ax: "φ ∈ formula ⟹ env ∈ list(M) ⟹
arity(φ) ≤ 1 +⇩ω length(env) ⟹
separation(##M,λx. (M, [x] @ env ⊨ φ))"
locale M_transset =
fixes M
assumes
trans_M: "Transset(M)"
locale M_Z_trans = M_Z_basic + M_transset
locale M_ZF1 = M_Z_basic +
assumes
replacement_ax1:
"replacement_assm(M,env,eclose_closed_fm)"
"replacement_assm(M,env,eclose_abs_fm)"
"replacement_assm(M,env,wfrec_rank_fm)"
"replacement_assm(M,env,transrec_VFrom_fm)"
definition instances1_fms where "instances1_fms ≡
{ eclose_closed_fm,
eclose_abs_fm,
wfrec_rank_fm,
transrec_VFrom_fm
}"
text‹This set has 4 internalized formulas.›
lemmas replacement_instances1_defs =
list_repl1_intf_fm_def list_repl2_intf_fm_def
formula_repl1_intf_fm_def formula_repl2_intf_fm_def
eclose_closed_fm_def eclose_abs_fm_def
wfrec_rank_fm_def transrec_VFrom_fm_def tl_repl_intf_fm_def
lemma instances1_fms_type[TC]: "instances1_fms ⊆ formula"
using Lambda_in_M_fm_type
unfolding replacement_instances1_defs instances1_fms_def by simp
declare (in M_ZF1) replacement_instances1_defs[simp]
locale M_ZF1_trans = M_ZF1 + M_Z_trans
context M_Z_trans
begin
lemmas transitivity = Transset_intf[OF trans_M]
subsection‹Interface with \<^term>‹M_trivial››
lemma zero_in_M: "0 ∈ M"
proof -
obtain z where "empty(##M,z)" "z∈M"
using empty_intf[OF infinity_ax]
by auto
moreover from this
have "z=0"
using transitivity empty_def
by auto
ultimately
show ?thesis
by simp
qed
lemma separation_in_ctm :
assumes
"φ ∈ formula" "env∈list(M)"
"arity(φ) ≤ 1 +⇩ω length(env)" and
satsQ: "⋀x. x∈M ⟹ (M, [x]@env ⊨ φ) ⟷ Q(x)"
shows
"separation(##M,Q)"
using assms separation_ax satsQ transitivity
separation_cong[of "##M" "λy. (M, [y]@env ⊨ φ)" "Q"]
by simp
end
locale M_ZC_basic = M_Z_basic + M_AC "##M"
locale M_ZFC1 = M_ZF1 + M_ZC_basic
locale M_ZFC1_trans = M_ZF1_trans + M_ZFC1
sublocale M_Z_trans ⊆ M_trans "##M"
using transitivity zero_in_M exI[of "λx. x∈M"]
by unfold_locales simp_all
sublocale M_Z_trans ⊆ M_trivial "##M"
using upair_ax Union_ax by unfold_locales
subsection‹Interface with \<^term>‹M_basic››
definition Intersection where
"Intersection(N,B,x) ≡ (∀y[N]. y∈B ⟶ x∈y)"
synthesize "Intersection" from_definition "Intersection" assuming "nonempty"
arity_theorem for "Intersection_fm"
definition CartProd where
"CartProd(N,B,C,z) ≡ (∃x[N]. x∈B ∧ (∃y[N]. y∈C ∧ pair(N,x,y,z)))"
synthesize "CartProd" from_definition "CartProd" assuming "nonempty"
arity_theorem for "CartProd_fm"
definition ImageSep where
"ImageSep(N,B,r,y) ≡ (∃p[N]. p∈r ∧ (∃x[N]. x∈B ∧ pair(N,x,y,p)))"
synthesize "ImageSep" from_definition assuming "nonempty"
arity_theorem for "ImageSep_fm"
definition Converse where
"Converse(N,R,z) ≡ ∃p[N]. p∈R ∧ (∃x[N].∃y[N]. pair(N,x,y,p) ∧ pair(N,y,x,z))"
synthesize "Converse" from_definition "Converse" assuming "nonempty"
arity_theorem for "Converse_fm"
definition Restrict where
"Restrict(N,A,z) ≡ ∃x[N]. x∈A ∧ (∃y[N]. pair(N,x,y,z))"
synthesize "Restrict" from_definition "Restrict" assuming "nonempty"
arity_theorem for "Restrict_fm"
definition Comp where
"Comp(N,R,S,xz) ≡ ∃x[N]. ∃y[N]. ∃z[N]. ∃xy[N]. ∃yz[N].
pair(N,x,z,xz) ∧ pair(N,x,y,xy) ∧ pair(N,y,z,yz) ∧ xy∈S ∧ yz∈R"
synthesize "Comp" from_definition "Comp" assuming "nonempty"
arity_theorem for "Comp_fm"
definition Pred where
"Pred(N,R,X,y) ≡ ∃p[N]. p∈R ∧ pair(N,y,X,p)"
synthesize "Pred" from_definition "Pred" assuming "nonempty"
arity_theorem for "Pred_fm"
definition is_Memrel where
"is_Memrel(N,z) ≡ ∃x[N]. ∃y[N]. pair(N,x,y,z) ∧ x ∈ y"
synthesize "is_Memrel" from_definition "is_Memrel" assuming "nonempty"
arity_theorem for "is_Memrel_fm"
definition RecFun where
"RecFun(N,r,f,g,a,b,x) ≡ ∃xa[N]. ∃xb[N].
pair(N,x,a,xa) ∧ xa ∈ r ∧ pair(N,x,b,xb) ∧ xb ∈ r ∧
(∃fx[N]. ∃gx[N]. fun_apply(N,f,x,fx) ∧ fun_apply(N,g,x,gx) ∧
fx ≠ gx)"
synthesize "RecFun" from_definition "RecFun" assuming "nonempty"
arity_theorem for "RecFun_fm"
arity_theorem for "rtran_closure_mem_fm"
synthesize "wellfounded_trancl" from_definition assuming "nonempty"
arity_theorem for "wellfounded_trancl_fm"
context M_Z_trans
begin
lemma inter_sep_intf :
assumes "A∈M"
shows "separation(##M,λx . ∀y∈M . y∈A ⟶ x∈y)"
using assms separation_in_ctm[of "Intersection_fm(1,0)" "[A]" "Intersection(##M,A)"]
Intersection_iff_sats[of 1 "[_,A]" A 0 _ M] arity_Intersection_fm Intersection_fm_type
ord_simp_union zero_in_M
unfolding Intersection_def
by simp
lemma diff_sep_intf :
assumes "B∈M"
shows "separation(##M,λx . x∉B)"
using assms separation_in_ctm[of "Neg(Member(0,1))" "[B]" "λx . x∉B"] ord_simp_union
by simp
lemma cartprod_sep_intf :
assumes "A∈M" and "B∈M"
shows "separation(##M,λz. ∃x∈M. x∈A ∧ (∃y∈M. y∈B ∧ pair(##M,x,y,z)))"
using assms separation_in_ctm[of "CartProd_fm(1,2,0)" "[A,B]" "CartProd(##M,A,B)"]
CartProd_iff_sats[of 1 "[_,A,B]" A 2 B 0 _ M] arity_CartProd_fm CartProd_fm_type
ord_simp_union zero_in_M
unfolding CartProd_def
by simp
lemma image_sep_intf :
assumes "A∈M" and "B∈M"
shows "separation(##M, λy. ∃p∈M. p∈B ∧ (∃x∈M. x∈A ∧ pair(##M,x,y,p)))"
using assms separation_in_ctm[of "ImageSep_fm(1,2,0)" "[A,B]" "ImageSep(##M,A,B)"]
ImageSep_iff_sats[of 1 "[_,A,B]" _ 2 _ 0 _ M] arity_ImageSep_fm ImageSep_fm_type
ord_simp_union zero_in_M
unfolding ImageSep_def
by simp
lemma converse_sep_intf :
assumes "R∈M"
shows "separation(##M,λz. ∃p∈M. p∈R ∧ (∃x∈M.∃y∈M. pair(##M,x,y,p) ∧ pair(##M,y,x,z)))"
using assms separation_in_ctm[of "Converse_fm(1,0)" "[R]" "Converse(##M,R)"]
Converse_iff_sats[of 1 "[_,R]" _ 0 _ M] arity_Converse_fm Converse_fm_type
ord_simp_union zero_in_M
unfolding Converse_def
by simp
lemma restrict_sep_intf :
assumes "A∈M"
shows "separation(##M,λz. ∃x∈M. x∈A ∧ (∃y∈M. pair(##M,x,y,z)))"
using assms separation_in_ctm[of "Restrict_fm(1,0)" "[A]" "Restrict(##M,A)"]
Restrict_iff_sats[of 1 "[_,A]" _ 0 _ M] arity_Restrict_fm Restrict_fm_type
ord_simp_union zero_in_M
unfolding Restrict_def
by simp
lemma comp_sep_intf :
assumes "R∈M" and "S∈M"
shows "separation(##M,λxz. ∃x∈M. ∃y∈M. ∃z∈M. ∃xy∈M. ∃yz∈M.
pair(##M,x,z,xz) ∧ pair(##M,x,y,xy) ∧ pair(##M,y,z,yz) ∧ xy∈S ∧ yz∈R)"
using assms separation_in_ctm[of "Comp_fm(1,2,0)" "[R,S]" "Comp(##M,R,S)"]
Comp_iff_sats[of 1 "[_,R,S]" _ 2 _ 0 _ M] arity_Comp_fm Comp_fm_type
ord_simp_union zero_in_M
unfolding Comp_def
by simp
lemma pred_sep_intf:
assumes "R∈M" and "X∈M"
shows "separation(##M, λy. ∃p∈M. p∈R ∧ pair(##M,y,X,p))"
using assms separation_in_ctm[of "Pred_fm(1,2,0)" "[R,X]" "Pred(##M,R,X)"]
Pred_iff_sats[of 1 "[_,R,X]" _ 2 _ 0 _ M] arity_Pred_fm Pred_fm_type
ord_simp_union zero_in_M
unfolding Pred_def
by simp
lemma memrel_sep_intf:
"separation(##M, λz. ∃x∈M. ∃y∈M. pair(##M,x,y,z) ∧ x ∈ y)"
using separation_in_ctm[of "is_Memrel_fm(0)" "[]" "is_Memrel(##M)"]
is_Memrel_iff_sats[of 0 "[_]" _ M] arity_is_Memrel_fm is_Memrel_fm_type
ord_simp_union zero_in_M
unfolding is_Memrel_def
by simp
lemma is_recfun_sep_intf :
assumes "r∈M" "f∈M" "g∈M" "a∈M" "b∈M"
shows "separation(##M,λx. ∃xa∈M. ∃xb∈M.
pair(##M,x,a,xa) ∧ xa ∈ r ∧ pair(##M,x,b,xb) ∧ xb ∈ r ∧
(∃fx∈M. ∃gx∈M. fun_apply(##M,f,x,fx) ∧ fun_apply(##M,g,x,gx) ∧
fx ≠ gx))"
using assms separation_in_ctm[of "RecFun_fm(1,2,3,4,5,0)" "[r,f,g,a,b]" "RecFun(##M,r,f,g,a,b)"]
RecFun_iff_sats[of 1 "[_,r,f,g,a,b]" _ 2 _ 3 _ 4 _ 5 _ 0 _ M] arity_RecFun_fm RecFun_fm_type
ord_simp_union zero_in_M
unfolding RecFun_def
by simp
lemmas M_basic_sep_instances =
inter_sep_intf diff_sep_intf cartprod_sep_intf
image_sep_intf converse_sep_intf restrict_sep_intf
pred_sep_intf memrel_sep_intf comp_sep_intf is_recfun_sep_intf
end
sublocale M_Z_trans ⊆ M_basic_no_repl "##M"
using power_ax M_basic_sep_instances
by unfold_locales simp_all
lemma Replace_eq_Collect:
assumes "⋀x y y'. x∈A ⟹ P(x,y) ⟹ P(x,y') ⟹ y=y'" "{y . x ∈ A, P(x, y)} ⊆ B"
shows "{y . x ∈ A, P(x, y)} = {y∈B . ∃x∈A. P(x,y)}"
using assms by blast
context M_Z_trans
begin
lemma Pow_inter_M_closed: assumes "A ∈ M" shows "Pow(A) ∩ M ∈ M"
proof -
have "{a ∈ Pow(A) . a ∈ M} = Pow(A) ∩ M" by auto
then
show ?thesis
using power_ax powerset_abs assms unfolding power_ax_def
by auto
qed
lemma Pow'_inter_M_closed: assumes "A ∈ M" shows "{a ∈ Pow(A) . a ∈ M} ∈ M"
using power_ax powerset_abs assms unfolding power_ax_def by auto
end
context M_basic_no_repl
begin
lemma Replace_funspace_succ_rep_intf_sub:
assumes
"M(A)" "M(n)"
shows
"{z . p ∈ A, funspace_succ_rep_intf_rel(M,p,z,n)}
⊆ Pow⇗M⇖(Pow⇗M⇖(⋃domain(A) ∪ ({n} × range(A)) ∪ (⋃({n} × range(A)))))"
unfolding funspace_succ_rep_intf_rel_def using assms mem_Pow_rel_abs
by clarsimp (auto simp: cartprod_def)
lemma funspace_succ_rep_intf_uniq:
assumes
"funspace_succ_rep_intf_rel(M,p,z,n)" "funspace_succ_rep_intf_rel(M,p,z',n)"
shows
"z = z'"
using assms unfolding funspace_succ_rep_intf_rel_def by auto
lemma Replace_funspace_succ_rep_intf_eq:
assumes
"M(A)" "M(n)"
shows
"{z . p ∈ A, funspace_succ_rep_intf_rel(M,p,z,n)} =
{z ∈ Pow⇗M⇖(Pow⇗M⇖(⋃domain(A) ∪ ({n} × range(A)) ∪ (⋃({n} × range(A))))) .
∃p∈A. funspace_succ_rep_intf_rel(M,p,z,n)}"
using assms Replace_eq_Collect[OF funspace_succ_rep_intf_uniq, of A,
OF _ _ Replace_funspace_succ_rep_intf_sub[of A n], of "λx y z. x" "λx y z. n"]
by (intro equalityI)
(auto dest:transM simp:funspace_succ_rep_intf_rel_def)
end
definition fsri where
"fsri(N,A,B) ≡ λz. ∃p∈A. ∃f[N]. ∃b[N]. p = ⟨f, b⟩ ∧ z = {cons(⟨B, b⟩, f)}"
relationalize "fsri" "is_fsri"
synthesize "is_fsri" from_definition assuming "nonempty"
arity_theorem for "is_fsri_fm"
context M_Z_trans
begin
lemma separation_fsri:
"(##M)(A) ⟹ (##M)(B) ⟹ separation(##M, is_fsri(##M,A,B))"
using separation_in_ctm[where env="[A,B]" and φ="is_fsri_fm(1,2,0)"]
zero_in_M is_fsri_iff_sats[symmetric] arity_is_fsri_fm is_fsri_fm_type
by (simp_all add: ord_simp_union)
lemma separation_funspace_succ_rep_intf_rel:
"(##M)(A) ⟹ (##M)(B) ⟹ separation(##M, λz. ∃p∈A. funspace_succ_rep_intf_rel(##M,p,z,B))"
using separation_fsri zero_in_M
by (rule_tac separation_cong[THEN iffD1, of _ "is_fsri(##M,A,B)"])
(auto simp flip:setclass_iff dest:transM
simp:is_fsri_def funspace_succ_rep_intf_rel_def, force)
lemma Replace_funspace_succ_rep_intf_in_M:
assumes
"A ∈ M" "n ∈ M"
shows
"{z . p ∈ A, funspace_succ_rep_intf_rel(##M,p,z,n)} ∈ M"
proof -
have "(##M)({z ∈ Pow⇗M⇖(Pow⇗M⇖(⋃domain(A) ∪ ({n} × range(A)) ∪ (⋃({n} × range(A))))) .
∃p∈A. funspace_succ_rep_intf_rel(##M,p,z,n)})"
using assms separation_funspace_succ_rep_intf_rel
by (intro separation_closed) (auto simp flip:setclass_iff)
with assms
show ?thesis
using Replace_funspace_succ_rep_intf_eq by auto
qed
lemma funspace_succ_rep_intf:
assumes "n∈M"
shows
"strong_replacement(##M,
λp z. ∃f∈M. ∃b∈M. ∃nb∈M. ∃cnbf∈M.
pair(##M,f,b,p) ∧ pair(##M,n,b,nb) ∧ is_cons(##M,nb,f,cnbf) ∧
upair(##M,cnbf,cnbf,z))"
using assms pair_in_M_iff[simplified] cons_closed[simplified]
unfolding strong_replacement_def univalent_def
apply (clarsimp, rename_tac A)
apply (rule_tac x="{z . p ∈ A, funspace_succ_rep_intf_rel(##M,p,z,n)}" in bexI)
apply (auto simp:funspace_succ_rep_intf_rel_def
Replace_funspace_succ_rep_intf_in_M[unfolded funspace_succ_rep_intf_rel_def, simplified])
done
end
sublocale M_Z_trans ⊆ M_basic "##M"
using power_ax M_basic_sep_instances funspace_succ_rep_intf
by unfold_locales auto
subsection‹Interface with \<^term>‹M_trancl››
context M_ZF1_trans
begin
lemma rtrancl_separation_intf:
assumes "r∈M" "A∈M"
shows "separation (##M, rtran_closure_mem(##M,A,r))"
using assms separation_in_ctm[of "rtran_closure_mem_fm(1,2,0)" "[A,r]" "rtran_closure_mem(##M,A,r)"]
arity_rtran_closure_mem_fm ord_simp_union zero_in_M
by simp
lemma wftrancl_separation_intf:
assumes "r∈M" and "Z∈M"
shows "separation (##M, wellfounded_trancl(##M,Z,r))"
using assms separation_in_ctm[of "wellfounded_trancl_fm(1,2,0)" "[Z,r]" "wellfounded_trancl(##M,Z,r)"]
arity_wellfounded_trancl_fm ord_simp_union zero_in_M
by simp
text‹To prove \<^term>‹nat ∈ M› we get an infinite set \<^term>‹I› from \<^term>‹infinity_ax›
closed under \<^term>‹0› and \<^term>‹succ›; that shows \<^term>‹nat⊆I›. Then we
can separate \<^term>‹I› with the predicate \<^term>‹λx. x∈nat›.›
lemma finite_sep_intf: "separation(##M, λx. x∈nat)"
proof -
have "(∀v∈M. separation(##M,λx. (M, [x,v] ⊨ finite_ordinal_fm(0))))"
using separation_ax arity_finite_ordinal_fm
by simp
then
have "(∀v∈M. separation(##M,finite_ordinal(##M)))"
unfolding separation_def
by simp
then
have "separation(##M,finite_ordinal(##M))"
using separation_in_ctm zero_in_M
by auto
then
show ?thesis
unfolding separation_def
by simp
qed
lemma nat_subset_I: "∃I∈M. nat ⊆ I"
proof -
have "nat ⊆ I"
if "I∈M" and "0∈I" and "⋀x. x∈I ⟹ succ(x)∈I" for I
using that
by (rule_tac subsetI,induct_tac x,simp_all)
moreover
obtain I where
"I∈M" "0∈I" "⋀x. x∈I ⟹ succ(x)∈I"
using infinity_ax transitivity
unfolding infinity_ax_def
by auto
ultimately
show ?thesis
by auto
qed
lemma nat_in_M: "nat ∈ M"
proof -
have "{x∈B . x∈A}=A" if "A⊆B" for A B
using that by auto
moreover
obtain I where
"I∈M" "nat⊆I"
using nat_subset_I by auto
moreover from this
have "{x∈I . x∈nat} ∈ M"
using finite_sep_intf separation_closed[of "λx . x∈nat"]
by simp
ultimately
show ?thesis
by simp
qed
end
sublocale M_ZF1_trans ⊆ M_trancl "##M"
using rtrancl_separation_intf wftrancl_separation_intf nat_in_M
wellfounded_trancl_def
by unfold_locales auto
subsection‹Interface with \<^term>‹M_eclose››
lemma repl_sats:
assumes
sat:"⋀x z. x∈M ⟹ z∈M ⟹ (M, Cons(x,Cons(z,env)) ⊨ φ) ⟷ P(x,z)"
shows
"strong_replacement(##M,λx z. (M, Cons(x,Cons(z,env)) ⊨ φ)) ⟷
strong_replacement(##M,P)"
by (rule strong_replacement_cong,simp add:sat)
arity_theorem for "list_functor_fm"
arity_theorem for "formula_functor_fm"
arity_theorem for "Inl_fm"
arity_theorem for "Inr_fm"
arity_theorem for "Nil_fm"
arity_theorem for "Cons_fm"
arity_theorem for "quasilist_fm"
arity_theorem for "tl_fm"
arity_theorem for "big_union_fm"
context M_ZF1_trans
begin
text‹This lemma obtains \<^term>‹iterates_replacement› for predicates
without parameters.›
lemma iterates_repl_intf :
assumes
"v∈M" and
isfm:"is_F_fm ∈ formula" and
arty:"arity(is_F_fm)=2" and
satsf: "⋀a b env'. ⟦ a∈M ; b∈M ; env'∈list(M) ⟧
⟹ is_F(a,b) ⟷ (M, [b,a]@env' ⊨ is_F_fm)"
and is_F_fm_replacement:
"⋀env. (⋅∃⋅⋅⟨1,0⟩ is 2⋅ ∧ is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0) ⋅⋅) ∈ formula ⟹ env ∈ list(M) ⟹
arity((⋅∃⋅⋅⟨1,0⟩ is 2⋅ ∧ is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0) ⋅⋅)) ≤ 2 +⇩ω length(env) ⟹
strong_replacement(##M,λx y.
M, [x,y] @ env ⊨ (⋅∃⋅⋅⟨1,0⟩ is 2⋅ ∧ is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0) ⋅⋅))"
shows
"iterates_replacement(##M,is_F,v)"
proof -
let ?f="(⋅∃⋅⋅⟨1,0⟩ is 2⋅ ∧ is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0) ⋅⋅)"
have "arity(?f) = 4" "?f∈formula"
using arity_iterates_MH_fm[where isF=is_F_fm and i=2]
arity_wfrec_replacement_fm[where i=10] isfm arty ord_simp_union
by simp_all
{
fix n
assume "n∈nat"
then
have "Memrel(succ(n))∈M"
using nat_into_M Memrel_closed
by simp
moreover
{
fix a0 a1 a2 a3 a4 y x z
assume "[a0,a1,a2,a3,a4,y,x,z]∈list(M)"
moreover
note ‹v∈M› ‹Memrel(succ(n))∈M›
moreover from calculation
have "(M, [b,a,c,d,a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v] ⊨ is_F_fm) ⟷
is_F(a,b)"
if "a∈M" "b∈M" "c∈M" "d∈M" for a b c d
using that satsf[of a b "[c,d,a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v]"]
by simp
moreover from calculation
have "(M, [a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v] ⊨ iterates_MH_fm(is_F_fm,9,2,1,0)) ⟷
iterates_MH(##M,is_F,v,a2, a1, a0)"
using sats_iterates_MH_fm[of M "is_F" "is_F_fm"]
by simp
}
moreover from calculation
have "(M, [y,x,z,Memrel(succ(n)),v] ⊨ is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0)) ⟷
is_wfrec(##M, iterates_MH(##M,is_F,v),Memrel(succ(n)), x, y)"
if "y∈M" "x∈M" "z∈M" for y x z
using that sats_is_wfrec_fm ‹v∈M› by simp
moreover from calculation
have "(M, [x,z,Memrel(succ(n)),v] ⊨ ?f) ⟷
(∃y∈M. pair(##M,x,y,z) ∧
is_wfrec(##M, iterates_MH(##M,is_F,v) , Memrel(succ(n)), x, y))"
if "x∈M" "z∈M" for x z
using that ‹v∈M›
by (simp del:pair_abs)
moreover
note ‹arity(?f) = 4› ‹?f∈formula›
moreover from calculation ‹v∈_›
have "strong_replacement(##M,λx z. (M, [x,z,Memrel(succ(n)),v] ⊨ ?f))"
using is_F_fm_replacement
by simp
ultimately
have "strong_replacement(##M,λx z.
∃y∈M. pair(##M,x,y,z) ∧ is_wfrec(##M, iterates_MH(##M,is_F,v) ,
Memrel(succ(n)), x, y))"
using repl_sats[of M ?f "[Memrel(succ(n)),v]"]
by (simp del:pair_abs)
}
then
show ?thesis
unfolding iterates_replacement_def wfrec_replacement_def
by simp
qed
lemma eclose_repl1_intf:
assumes "A∈M"
shows "iterates_replacement(##M, big_union(##M), A)"
using assms arity_big_union_fm
iterates_repl_intf[where is_F_fm="big_union_fm(1,0)"]
replacement_ax1(1)[unfolded replacement_assm_def]
ord_simp_union
by simp
lemma eclose_repl2_intf:
assumes "A∈M"
shows "strong_replacement(##M,λn y. n∈nat ∧ is_iterates(##M, big_union(##M), A, n, y))"
proof -
let ?f = "And(Member(0,3),is_iterates_fm(big_union_fm(1,0),2,0,1))"
note nat_in_M ‹A∈M›
moreover from this
have "big_union(##M,a,b) ⟷
(M, [b,a,c,d,e,f,g,h,i,j,k,n,y,A,nat] ⊨ big_union_fm(1,0))"
if "a∈M" "b∈M" "c∈M" "d∈M" "e∈M" "f∈M""g∈M""h∈M""i∈M""j∈M" "k∈M" "n∈M" "y∈M"
for a b c d e f g h i j k n y
using that by simp
moreover from calculation
have "(M, [n,y,A,nat] ⊨ is_iterates_fm(big_union_fm(1,0),2,0,1)) ⟷
is_iterates(##M, big_union(##M), A, n , y)"
if "n∈M" "y∈M" for n y
using that sats_is_iterates_fm[of M "big_union(##M)"]
by simp
moreover from calculation
have "(M, [n,y,A,nat] ⊨ ?f) ⟷
n∈nat ∧ is_iterates(##M, big_union(##M), A, n, y)"
if "n∈M" "y∈M" for n y
using that
by simp
moreover
have "arity(?f) = 4"
using arity_is_iterates_fm[where p="big_union_fm(1,0)" and i=2]
arity_big_union_fm arity_And ord_simp_union
by simp
ultimately
show ?thesis
using repl_sats[of M ?f "[A,nat]"] replacement_ax1(2)[unfolded replacement_assm_def]
by simp
qed
end
sublocale M_ZF1_trans ⊆ M_eclose "##M"
using eclose_repl1_intf eclose_repl2_intf
by unfold_locales auto
text‹Interface with \<^locale>‹M_eclose›.›
schematic_goal sats_is_Vset_fm_auto:
assumes
"i∈nat" "v∈nat" "env∈list(A)" "0∈A"
"i < length(env)" "v < length(env)"
shows
"is_Vset(##A,nth(i, env),nth(v, env)) ⟷ (A, env ⊨ ?ivs_fm(i,v))"
unfolding is_Vset_def is_Vfrom_def
by (insert assms; (rule sep_rules is_HVfrom_iff_sats is_transrec_iff_sats | simp)+)
synthesize "is_Vset" from_schematic "sats_is_Vset_fm_auto"
arity_theorem for "is_Vset_fm"
declare is_Hrank_fm_def[fm_definitions add]
context M_ZF1_trans
begin
lemma wfrec_rank :
assumes "X∈M"
shows "wfrec_replacement(##M,is_Hrank(##M),rrank(X))"
proof -
let ?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(is_Hrank_fm(2,1,0),3,1,0)))"
note assms zero_in_M
moreover from this
have
"is_Hrank(##M,a2, a1, a0) ⟷
(M, [a0,a1,a2,a3,a4,y,x,z,rrank(X)] ⊨ is_Hrank_fm(2,1,0))"
if "a4∈M" "a3∈M" "a2∈M" "a1∈M" "a0∈M" "y∈M" "x∈M" "z∈M" for a4 a3 a2 a1 a0 y x z
using that rrank_in_M is_Hrank_iff_sats
by simp
moreover from calculation
have "(M, [y,x,z,rrank(X)] ⊨ is_wfrec_fm(is_Hrank_fm(2,1,0),3,1,0)) ⟷
is_wfrec(##M, is_Hrank(##M) ,rrank(X), x, y)"
if "y∈M" "x∈M" "z∈M" for y x z
using that rrank_in_M sats_is_wfrec_fm
by simp
moreover from calculation
have "(M, [x,z,rrank(X)] ⊨ ?f) ⟷
(∃y∈M. pair(##M,x,y,z) ∧ is_wfrec(##M, is_Hrank(##M) , rrank(X), x, y))"
if "x∈M" "z∈M" for x z
using that rrank_in_M
by (simp del:pair_abs)
moreover
have "arity(?f) = 3"
using arity_wfrec_replacement_fm[where p="is_Hrank_fm(2,1,0)" and i=3,simplified]
arity_is_Hrank_fm[of 2 1 0,simplified] ord_simp_union
by simp
moreover from calculation
have "strong_replacement(##M,λx z. (M, [x,z,rrank(X)] ⊨ ?f))"
using replacement_ax1(3)[unfolded replacement_assm_def] rrank_in_M
by simp
ultimately
show ?thesis
using repl_sats[of M ?f "[rrank(X)]"]
unfolding wfrec_replacement_def
by (simp del:pair_abs)
qed
lemma trans_repl_HVFrom :
assumes "A∈M" "i∈M"
shows "transrec_replacement(##M,is_HVfrom(##M,A),i)"
proof -
let ?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(is_HVfrom_fm(8,2,1,0),4,1,0)))"
note facts = assms zero_in_M
moreover
have "∃sa∈M. ∃esa∈M. ∃mesa∈M.
upair(##M,a,a,sa) ∧ is_eclose(##M,sa,esa) ∧ membership(##M,esa,mesa)"
if "a∈M" for a
using that upair_ax eclose_closed Memrel_closed
unfolding upair_ax_def
by (simp del:upair_abs)
moreover
{
fix mesa
assume "mesa∈M"
moreover
note facts
moreover from calculation
have "is_HVfrom(##M,A,a2, a1, a0) ⟷
(M, [a0,a1,a2,a3,a4,y,x,z,A,mesa] ⊨ is_HVfrom_fm(8,2,1,0))"
if "a4∈M" "a3∈M" "a2∈M" "a1∈M" "a0∈M" "y∈M" "x∈M" "z∈M" for a4 a3 a2 a1 a0 y x z
using that sats_is_HVfrom_fm
by simp
moreover from calculation
have "(M, [y,x,z,A,mesa] ⊨ is_wfrec_fm(is_HVfrom_fm(8,2,1,0),4,1,0)) ⟷
is_wfrec(##M, is_HVfrom(##M,A),mesa, x, y)"
if "y∈M" "x∈M" "z∈M" for y x z
using that sats_is_wfrec_fm
by simp
moreover from calculation
have "(M, [x,z,A,mesa] ⊨ ?f) ⟷
(∃y∈M. pair(##M,x,y,z) ∧ is_wfrec(##M, is_HVfrom(##M,A) , mesa, x, y))"
if "x∈M" "z∈M" for x z
using that
by (simp del:pair_abs)
moreover
have "arity(?f) = 4"
using arity_wfrec_replacement_fm[where p="is_HVfrom_fm(8,2,1,0)" and i=9]
arity_is_HVfrom_fm ord_simp_union
by simp
moreover from calculation
have "strong_replacement(##M,λx z. (M, [x,z,A,mesa] ⊨ ?f))"
using replacement_ax1(4)[unfolded replacement_assm_def]
by simp
ultimately
have "wfrec_replacement(##M,is_HVfrom(##M,A),mesa)"
using repl_sats[of M ?f "[A,mesa]"]
unfolding wfrec_replacement_def
by (simp del:pair_abs)
}
ultimately
show ?thesis
unfolding transrec_replacement_def
by simp
qed
end
subsection‹Interface for proving Collects and Replace in M.›
context M_ZF1_trans
begin
lemma Collect_in_M :
assumes
"φ ∈ formula" "env∈list(M)"
"arity(φ) ≤ 1 +⇩ω length(env)" "A∈M" and
satsQ: "⋀x. x∈M ⟹ (M, [x]@env ⊨ φ) ⟷ Q(x)"
shows
"{y∈A . Q(y)}∈M"
proof -
have "separation(##M,λx. (M, [x] @ env ⊨ φ))"
using assms separation_ax by simp
then
show ?thesis
using ‹A∈M› satsQ transitivity separation_closed
separation_cong[of "##M" "λy. (M, [y]@env ⊨ φ)" "Q"]
by simp
qed
lemma separation_in_M :
assumes
"φ ∈ formula" "env∈list(M)"
"arity(φ) ≤ 1 +⇩ω length(env)" "A∈M" and
satsQ: "⋀x. x∈A ⟹ (M, [x]@env ⊨ φ) ⟷ Q(x)"
shows
"{y∈A . Q(y)} ∈ M"
proof -
let ?φ' = "And(φ,Member(0,length(env)+⇩ω1))"
note assms
moreover
have "arity(?φ') ≤ 1 +⇩ω length(env@[A])"
using assms Un_le le_trans[of "arity(φ)" "1+⇩ωlength(env)" "2+⇩ωlength(env)"]
by (force simp:FOL_arities)
moreover from calculation
have "?φ'∈formula" "nth(length(env), env @ [A]) = A"
using nth_append
by auto
moreover from calculation
have "⋀ x . x ∈ M ⟹ (M, [x]@env@[A] ⊨ ?φ') ⟷ Q(x) ∧ x∈A"
using arity_sats_iff[of _ "[A]" _ "[_]@env"]
by auto
ultimately
show ?thesis
using Collect_in_M[of ?φ' "env@[A]" _ "λx . Q(x) ∧ x∈A", OF _ _ _ ‹A∈M›]
by auto
qed
end
context M_Z_trans
begin
lemma strong_replacement_in_ctm:
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ)≤ 2 +⇩ω length(env)" and
fsats: "⋀x y. x∈M ⟹ y∈M ⟹ (M,[x,y]@env ⊨ φ) ⟷ y = f(x)" and
fclosed: "⋀x. x∈M ⟹ f(x) ∈ M" and
phi_replacement:"replacement_assm(M,env,φ)" and
"env∈list(M)"
shows "strong_replacement(##M, λx y . y = f(x))"
using assms
strong_replacement_cong[of "##M" "λx y. M,[x,y]@env⊨φ" "λx y. y = f(x)"]
unfolding replacement_assm_def
by auto
lemma strong_replacement_rel_in_ctm :
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ)≤ 2 +⇩ω length(env)" and
fsats: "⋀x y. x∈M ⟹ y∈M ⟹ (M,[x,y]@env ⊨ φ) ⟷ f(x,y)" and
phi_replacement:"replacement_assm(M,env,φ)" and
"env∈list(M)"
shows "strong_replacement(##M, f)"
using assms
strong_replacement_cong[of "##M" "λx y. M,[x,y]@env⊨φ" "f"]
unfolding replacement_assm_def
by auto
lemma Replace_in_M :
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ)≤ 2 +⇩ω length(env)" and
fsats: "⋀x y. x∈A ⟹ y∈M ⟹ (M,[x,y]@env ⊨ φ) ⟷ y = f(x)" and
fclosed: "⋀x. x∈A ⟹ f(x) ∈ M" and
"A∈M" "env∈list(M)" and
phi'_replacement:"replacement_assm(M,env@[A], ⋅φ ∧ ⋅0 ∈ length(env) +⇩ω 2⋅⋅ )"
shows "{f(x) . x∈A}∈M"
proof -
let ?φ' = "And(φ,Member(0,length(env)+⇩ω2))"
note assms
moreover from this
have "arity(?φ') ≤ 2 +⇩ω length(env@[A])"
using Un_le le_trans[of "arity(φ)" "2+⇩ω(length(env))" "3+⇩ωlength(env)"]
by (force simp:FOL_arities)
moreover from calculation
have "?φ'∈formula" "nth(length(env), env @ [A]) = A"
using nth_append by auto
moreover from calculation
have "⋀ x y. x ∈ M ⟹ y∈M ⟹ (M,[x,y]@env@[A]⊨?φ') ⟷ y=f(x) ∧x∈A"
using arity_sats_iff[of _ "[A]" _ "[_,_]@env"]
by auto
moreover from calculation
have "strong_replacement(##M, λx y. M,[x,y]@env@[A] ⊨ ?φ')"
using phi'_replacement assms(1-6) unfolding replacement_assm_def by simp
ultimately
have 4:"strong_replacement(##M, λx y. y = f(x) ∧ x∈A)"
using
strong_replacement_cong[of "##M" "λx y. M,[x,y]@env@[A]⊨?φ'" "λx y. y = f(x) ∧ x∈A"]
by simp
then
have "{y . x∈A , y = f(x)} ∈ M"
using ‹A∈M› strong_replacement_closed[OF 4,of A] fclosed by simp
moreover
have "{f(x). x∈A} = { y . x∈A , y = f(x)}"
by auto
ultimately
show ?thesis by simp
qed
lemma Replace_relativized_in_M :
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ)≤ 2 +⇩ω length(env)" and
fsats: "⋀x y. x∈A ⟹ y∈M ⟹ (M,[x,y]@env ⊨ φ) ⟷ is_f(x,y)" and
fabs: "⋀x y. x∈A ⟹ y∈M ⟹ is_f(x,y) ⟷ y = f(x)" and
fclosed: "⋀x. x∈A ⟹ f(x) ∈ M" and
"A∈M" "env∈list(M)" and
phi'_replacement:"replacement_assm(M,env@[A], ⋅φ ∧ ⋅0 ∈ length(env) +⇩ω 2⋅⋅ )"
shows "{f(x) . x∈A}∈M"
using assms Replace_in_M[of φ] by auto
lemma ren_action :
assumes
"env∈list(M)" "x∈M" "y∈M" "z∈M"
shows "∀ i . i < 2+⇩ωlength(env) ⟶
nth(i,[x,z]@env) = nth(ρ_repl(length(env))`i,[z,x,y]@env)"
proof -
let ?f="{⟨0, 1⟩, ⟨1, 0⟩}"
have 1:"(⋀j. j < length(env) ⟹ nth(j, env) = nth(id(length(env)) ` j, env))"
using assms ltD by simp
have 2:"nth(j, [x,z]) = nth(?f ` j, [z,x,y])" if "j<2" for j
proof -
consider "j=0" | "j=1" using ltD[OF ‹j<2›] by auto
then show ?thesis
proof(cases)
case 1
then show ?thesis using apply_equality f_type by simp
next
case 2
then show ?thesis using apply_equality f_type by simp
qed
qed
show ?thesis
using sum_action[OF _ _ _ _ f_type id_type _ _ _ _ _ _ _ 2 1,simplified] assms
unfolding ρ_repl_def by simp
qed
lemma Lambda_in_M :
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ)≤ 2 +⇩ω length(env)" and
fsats: "⋀x y. x∈A ⟹ y∈M ⟹ (M,[x,y]@env ⊨ φ) ⟷ is_f(x,y)" and
fabs: "⋀x y. x∈A ⟹ y∈M ⟹ is_f(x,y) ⟷ y = f(x)" and
fclosed: "⋀x. x∈A ⟹ f(x) ∈ M" and
"A∈M" "env∈list(M)" and
phi'_replacement2: "replacement_assm(M,env@[A],Lambda_in_M_fm(φ,length(env)))"
shows "(λx∈A . f(x)) ∈M"
unfolding lam_def
proof -
let ?ren="ρ_repl(length(env))"
let ?j="2+⇩ωlength(env)"
let ?k="3+⇩ωlength(env)"
let ?ψ="ren(φ)`?j`?k`?ren"
let ?φ'="Exists(And(pair_fm(1,0,2),?ψ))"
let ?p="λx y. ∃z∈M. pair(##M,x,z,y) ∧ is_f(x,z)"
have "?φ'∈formula" "?ψ∈formula"
using ‹env∈_› length_type f_fm ren_type ren_tc[of φ "2+⇩ωlength(env)" "3+⇩ωlength(env)" ?ren]
by simp_all
moreover from this
have "arity(?ψ)≤3+⇩ω(length(env))" "arity(?ψ)∈nat"
using assms arity_ren[OF f_fm _ _ ren_type,of "length(env)"] by simp_all
then
have "arity(?φ') ≤ 2+⇩ω(length(env))"
using Un_le pred_Un_distrib assms pred_le
by (simp add:arity)
moreover from this calculation
have "x∈A ⟹ y∈M ⟹ (M,[x,y]@env ⊨ ?φ') ⟷ ?p(x,y)" for x y
using ‹env∈_› length_type[OF ‹env∈_›] assms transitivity[OF _ ‹A∈M›]
sats_iff_sats_ren[OF f_fm _ _ _ _ ren_type f_ar ren_action[rule_format,of _ x y],of _ M ]
by auto
moreover
have "x∈A ⟹ y∈M ⟹ ?p(x,y) ⟷ y = <x,f(x)>" for x y
using assms transitivity[OF _ ‹A∈_›] fclosed
by simp
moreover
have "⋀ x . x∈A ⟹ <x,f(x)> ∈ M"
using transitivity[OF _ ‹A∈M›] pair_in_M_iff fclosed by simp
ultimately
show "{⟨x,f(x)⟩ . x∈A } ∈ M"
using Replace_in_M[of ?φ' env A] phi'_replacement2 ‹A∈M› ‹env∈_›
by simp
qed
lemma ren_action' :
assumes
"env∈list(M)" "x∈M" "y∈M" "z∈M" "u∈M"
shows "∀ i . i < 3+⇩ωlength(env) ⟶
nth(i,[x,z,u]@env) = nth(ρ_pair_repl(length(env))`i,[x,z,y,u]@env)"
proof -
let ?f="{⟨0, 0⟩, ⟨1, 1⟩, ⟨2,3⟩}"
have 1:"(⋀j. j < length(env) ⟹ nth(j, env) = nth(id(length(env)) ` j, env))"
using assms ltD by simp
have 2:"nth(j, [x,z,u]) = nth(?f ` j, [x,z,y,u])" if "j<3" for j
proof -
consider "j=0" | "j=1" | "j=2" using ltD[OF ‹j<3›] by auto
then show ?thesis
proof(cases)
case 1
then show ?thesis using apply_equality f_type' by simp
next
case 2
then show ?thesis using apply_equality f_type' by simp
next
case 3
then show ?thesis using apply_equality f_type' by simp
qed
qed
show ?thesis
using sum_action[OF _ _ _ _ f_type' id_type _ _ _ _ _ _ _ 2 1,simplified] assms
unfolding ρ_pair_repl_def by simp
qed
lemma LambdaPair_in_M :
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ)≤ 3 +⇩ω length(env)" and
fsats: "⋀x z r. x∈M ⟹ z∈M ⟹ r∈M ⟹ (M,[x,z,r]@env ⊨ φ) ⟷ is_f(x,z,r)" and
fabs: "⋀x z r. x∈M ⟹ z∈M ⟹ r∈M ⟹ is_f(x,z,r) ⟷ r = f(x,z)" and
fclosed: "⋀x z. x∈M ⟹ z∈M ⟹ f(x,z) ∈ M" and
"A∈M" "env∈list(M)" and
phi'_replacement3: "replacement_assm(M,env@[A],LambdaPair_in_M_fm(φ,length(env)))"
shows "(λx∈A . f(fst(x),snd(x))) ∈M"
proof -
let ?ren="ρ_pair_repl(length(env))"
let ?j="3+⇩ωlength(env)"
let ?k="4+⇩ωlength(env)"
let ?ψ="ren(φ)`?j`?k`?ren"
let ?φ'="Exists(Exists(And(fst_fm(2,0),(And(snd_fm(2,1),?ψ)))))"
let ?p="λx y. is_f(fst(x),snd(x),y)"
have "?φ'∈formula" "?ψ∈formula"
using ‹env∈_› length_type f_fm ren_type' ren_tc[of φ ?j ?k ?ren]
by simp_all
moreover from this
have "arity(?ψ)≤4+⇩ω(length(env))" "arity(?ψ)∈nat"
using assms arity_ren[OF f_fm _ _ ren_type',of "length(env)"] by simp_all
moreover from calculation
have 1:"arity(?φ') ≤ 2+⇩ω(length(env))" "?φ'∈formula"
using Un_le pred_Un_distrib assms pred_le
by (simp_all add:arity)
moreover from this calculation
have 2:"x∈A ⟹ y∈M ⟹ (M,[x,y]@env ⊨ ?φ') ⟷ ?p(x,y)" for x y
using
sats_iff_sats_ren[OF f_fm _ _ _ _ ren_type' f_ar
ren_action'[rule_format,of _ "fst(x)" x "snd(x)" y],simplified]
‹env∈_› length_type[OF ‹env∈_›] transitivity[OF _ ‹A∈M›]
fst_snd_closed pair_in_M_iff fsats[of "fst(x)" "snd(x)" y,symmetric]
fst_abs snd_abs
by auto
moreover from assms
have 3:"x∈A ⟹ y∈M ⟹ ?p(x,y) ⟷ y = f(fst(x),snd(x))" for x y
using fclosed fst_snd_closed pair_in_M_iff fabs transitivity
by auto
moreover
have 4:"⋀ x . x∈A ⟹ <x,f(fst(x),snd(x))> ∈ M" "⋀ x . x∈A ⟹ f(fst(x),snd(x)) ∈ M"
using transitivity[OF _ ‹A∈M›] pair_in_M_iff fclosed fst_snd_closed
by simp_all
ultimately
show ?thesis
using Lambda_in_M[unfolded Lambda_in_M_fm_def, of ?φ', OF _ _ _ _ _ _ _
phi'_replacement3[unfolded LambdaPair_in_M_fm_def]]
‹env∈_› ‹A∈_› by simp
qed
lemma (in M_ZF1_trans) lam_replacement2_in_ctm :
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ)≤ 3 +⇩ω length(env)" and
fsats: "⋀x z r. x∈M ⟹ z∈M ⟹ r∈M ⟹ (M,[x,z,r]@env ⊨ φ) ⟷ is_f(x,z,r)" and
fabs: "⋀x z r. x∈M ⟹ z∈M ⟹ r∈M ⟹ is_f(x,z,r) ⟷ r = f(x,z)" and
fclosed: "⋀x z. x∈M ⟹ z∈M ⟹ f(x,z) ∈ M" and
"env∈list(M)" and
phi'_replacement3: "⋀A. A∈M ⟹ replacement_assm(M,env@[A],LambdaPair_in_M_fm(φ,length(env)))"
shows "lam_replacement(##M , λx . f(fst(x),snd(x)))"
using
LambdaPair_in_M fabs
f_ar ord_simp_union transitivity assms fst_snd_closed
by (rule_tac lam_replacement_iff_lam_closed[THEN iffD2],simp_all)
simple_rename "ren_U" src "[z1,x_P, x_leq, x_o, x_t, z2_c]"
tgt "[z2_c,z1,z,x_P, x_leq, x_o, x_t]"
simple_rename "ren_V" src "[fz,x_P, x_leq, x_o,x_f, x_t, gz]"
tgt "[gz,fz,z,x_P, x_leq, x_o,x_f, x_t]"
simple_rename "ren_V3" src "[fz,x_P, x_leq, x_o,x_f, gz, hz]"
tgt "[hz,gz,fz,z,x_P, x_leq, x_o,x_f]"
lemma separation_sat_after_function_1:
assumes "[a,b,c,d]∈list(M)" and "χ∈formula" and "arity(χ) ≤ 6"
and
f_fm: "f_fm ∈ formula" and
f_ar: "arity(f_fm) ≤ 6" and
fsats: "⋀ fx x. fx∈M ⟹ x∈M ⟹ (M,[fx,x]@[a, b, c, d] ⊨ f_fm) ⟷ fx=f(x)" and
fclosed: "⋀x . x∈M ⟹ f(x) ∈ M" and
g_fm: "g_fm ∈ formula" and
g_ar: "arity(g_fm) ≤ 7" and
gsats: "⋀ gx fx x. gx∈M ⟹ fx∈M ⟹ x∈M ⟹ (M,[gx,fx,x]@[a, b, c, d] ⊨ g_fm) ⟷ gx=g(x)" and
gclosed: "⋀x . x∈M ⟹ g(x) ∈ M"
shows "separation(##M, λr. M, [f(r), a, b, c, d, g(r)] ⊨ χ)"
proof -
note types = assms(1-4)
let ?ψ="ren(χ)`6`7`ren_U_fn"
let ?ψ'="Exists(And(f_fm,Exists(And(g_fm,?ψ))))"
let ?ρ="λz.[f(z), a, b, c, d, g(z)]"
let ?env="[a, b, c, d]"
let ?η="λz.[g(z),f(z),z]@?env"
note types
moreover from this
have "arity(χ) ≤ 7" "?ψ∈formula"
using ord_simp_union ren_tc ren_U_thm(2)[folded ren_U_fn_def] le_trans[of "arity(χ)" 6]
by simp_all
moreover from calculation
have "arity(?ψ) ≤ 7" "?ψ'∈formula"
using arity_ren ren_U_thm(2)[folded ren_U_fn_def] f_fm g_fm
by simp_all
moreover from calculation f_ar g_ar f_fm g_fm
have "arity(?ψ') ≤ 5"
using ord_simp_union pred_le arity_type
by (simp add:arity)
moreover from calculation fclosed gclosed
have 0:"(M, [f(z), a, b, c, d, g(z)] ⊨ χ) ⟷ (M,?η(z)⊨ ?ψ)" if "(##M)(z)" for z
using sats_iff_sats_ren[of χ 6 7 _ _ "?η(z)"]
ren_U_thm(1)[where A=M,folded ren_U_fn_def] ren_U_thm(2)[folded ren_U_fn_def] that
by simp
moreover from calculation
have 1:"(M,?η(z)⊨ ?ψ) ⟷ M,[z]@?env⊨?ψ'" if "(##M)(z)" for z
using that fsats[OF fclosed[of z],of z] gsats[of "g(z)" "f(z)" z] fclosed gclosed f_fm g_fm
proof(rule_tac iffI,simp,rule_tac rev_bexI[where x="f(z)"],simp,(auto)[1])
assume "M, [z] @ [a, b, c, d] ⊨ (⋅∃⋅f_fm ∧ (⋅∃⋅g_fm ∧ ren(χ) ` 6 ` 7 ` ren_U_fn⋅⋅)⋅⋅)"
then
have "∃xa∈M. (M, [xa, z, a, b, c, d] ⊨ f_fm) ∧
(∃x∈M. (M, [x, xa, z, a, b, c, d] ⊨ g_fm) ∧
(M, [x, xa, z, a, b, c, d] ⊨ ren(χ) ` 6 ` 7 ` ren_U_fn))"
using that calculation by auto
then
obtain xa x where "x∈M" "xa∈M" "M, [xa, z, a, b, c, d] ⊨ f_fm"
"(M, [x, xa, z, a, b, c, d] ⊨ g_fm)"
"(M, [x, xa, z, a, b, c, d] ⊨ ren(χ) ` 6 ` 7 ` ren_U_fn)"
using that calculation by auto
moreover from this
have "xa=f(z)" "x=g(z)" using fsats[of xa] gsats[of x xa] that by simp_all
ultimately
show "M, [g(z), f(z), z] @ [a, b, c, d] ⊨ ren(χ) ` 6 ` 7 ` ren_U_fn"
by auto
qed
moreover from calculation
have "separation(##M, λz. (M,[z]@?env ⊨ ?ψ'))"
using separation_ax
by simp_all
ultimately
show ?thesis
by(rule_tac separation_cong[THEN iffD2,OF iff_trans[OF 0 1]],clarify,force)
qed
lemma separation_sat_after_function3:
assumes "[a, b, c, d]∈list(M)" and "χ∈formula" and "arity(χ) ≤ 7"
and
f_fm: "f_fm ∈ formula" and
f_ar: "arity(f_fm) ≤ 6" and
fsats: "⋀ fx x. fx∈M ⟹ x∈M ⟹ (M,[fx,x]@[a, b, c, d] ⊨ f_fm) ⟷ fx=f(x)" and
fclosed: "⋀x . x∈M ⟹ f(x) ∈ M" and
g_fm: "g_fm ∈ formula" and
g_ar: "arity(g_fm) ≤ 7" and
gsats: "⋀ gx fx x. gx∈M ⟹ fx∈M ⟹ x∈M ⟹ (M,[gx,fx,x]@[a, b, c, d] ⊨ g_fm) ⟷ gx=g(x)" and
gclosed: "⋀x . x∈M ⟹ g(x) ∈ M" and
h_fm: "h_fm ∈ formula" and
h_ar: "arity(h_fm) ≤ 8" and
hsats: "⋀ hx gx fx x. hx∈M ⟹ gx∈M ⟹ fx∈M ⟹ x∈M ⟹ (M,[hx,gx,fx,x]@[a, b, c, d] ⊨ h_fm) ⟷ hx=h(x)" and
hclosed: "⋀x . x∈M ⟹ h(x) ∈ M"
shows "separation(##M, λr. M, [f(r), a, b, c, d, g(r), h(r)] ⊨ χ)"
proof -
note types = assms(1-3)
let ?φ="χ"
let ?ψ="ren(?φ)`7`8`ren_V3_fn"
let ?ψ'="Exists(And(f_fm,Exists(And(g_fm,Exists(And(h_fm,?ψ))))))"
let ?ρ="λz.[f(z), a, b, c, d,g(z), h(z)]"
let ?env="[a, b, c, d]"
let ?η="λz.[h(z),g(z),f(z),z]@?env"
note types
moreover from this
have "?φ∈formula" by simp
moreover from calculation
have "arity(?φ) ≤ 9" "?ψ∈formula"
using ord_simp_union ren_tc ren_V3_thm(2)[folded ren_V3_fn_def] le_trans[of "arity(χ)" 7]
by simp_all
moreover from calculation
have "arity(?ψ) ≤ 8" "?ψ'∈formula"
using arity_ren ren_V3_thm(2)[folded ren_V3_fn_def] f_fm g_fm h_fm
by (simp_all)
moreover from this f_ar g_ar f_fm g_fm h_fm h_ar ‹?ψ'∈_›
have "arity(?ψ') ≤ 5"
using ord_simp_union arity_type nat_into_Ord
by (simp add:arity,(rule_tac pred_le,simp,rule_tac Un_le,simp)+,simp_all add: ‹?ψ∈_›)
moreover from calculation fclosed gclosed hclosed
have 0:"(M, ?ρ(z) ⊨ ?φ) ⟷ (M,?η(z)⊨ ?ψ)" if "(##M)(z)" for z
using sats_iff_sats_ren[of ?φ 7 8 "?ρ(z)" M "?η(z)"]
ren_V3_thm(1)[where A=M,folded ren_V3_fn_def,simplified] ren_V3_thm(2)[folded ren_V3_fn_def] that
by simp
moreover from calculation
have 1:"(M,?η(z)⊨ ?ψ) ⟷ M,[z]@?env⊨?ψ'" if "(##M)(z)" for z
using that fsats[OF fclosed[of z],of z] gsats[of "g(z)" "f(z)" z]
hsats[of "h(z)" "g(z)" "f(z)" z]
fclosed gclosed hclosed f_fm g_fm h_fm
apply(rule_tac iffI,simp,rule_tac rev_bexI[where x="f(z)"],simp)
apply(rule_tac conjI,simp,rule_tac rev_bexI[where x="g(z)"],simp)
apply(rule_tac conjI,simp,rule_tac rev_bexI[where x="h(z)"],simp,rule_tac conjI,simp,simp)
proof -
assume "M, [z] @ [a, b, c, d] ⊨ (⋅∃⋅f_fm ∧ (⋅∃⋅g_fm ∧ (⋅∃⋅h_fm ∧ ren(χ) ` 7 ` 8 ` ren_V3_fn⋅⋅)⋅⋅)⋅⋅)"
with calculation that
have "∃x∈M. (M, [x, z, a, b, c, d] ⊨ f_fm) ∧
(∃xa∈M. (M, [xa, x, z, a, b, c, d] ⊨ g_fm) ∧ (∃xb∈M. (M, [xb, xa, x, z, a, b, c, d] ⊨ h_fm) ∧ (M, [xb, xa, x, z, a, b, c, d] ⊨ ren(χ) ` 7 ` 8 ` ren_V3_fn)))"
by auto
with calculation
obtain x where "x∈M" "(M, [x, z, a, b, c, d] ⊨ f_fm)"
"(∃xa∈M. (M, [xa, x, z, a, b, c, d] ⊨ g_fm) ∧ (∃xb∈M. (M, [xb, xa, x, z, a, b, c, d] ⊨ h_fm) ∧ (M, [xb, xa, x, z, a, b, c, d] ⊨ ren(χ) ` 7 ` 8 ` ren_V3_fn)))"
by force
moreover from this
have "x=f(z)" using fsats[of x] that by simp
moreover from calculation
obtain xa where "xa∈M" "(M, [xa, x, z, a, b, c, d] ⊨ g_fm)"
"(∃xb∈M. (M, [xb, xa, x, z, a, b, c, d] ⊨ h_fm) ∧ (M, [xb, xa, x, z, a, b, c, d] ⊨ ren(χ) ` 7 ` 8 ` ren_V3_fn))"
by auto
moreover from calculation
have "xa=g(z)" using gsats[of xa x] that by simp
moreover from calculation
obtain xb where "xb∈M" "(M, [xb, xa, x, z, a, b, c, d] ⊨ h_fm)"
"(M, [xb, xa, x, z, a, b, c, d] ⊨ ren(χ) ` 7 ` 8 ` ren_V3_fn)"
by auto
moreover from calculation
have "xb=h(z)" using hsats[of xb xa x] that by simp
ultimately
show "M, [h(z), g(z), f(z), z] @ [a, b, c, d] ⊨ ren(χ) ` 7 ` 8 ` ren_V3_fn"
by auto
qed
moreover from calculation ‹?ψ'∈_›
have "separation(##M, λz. (M,[z]@?env ⊨ ?ψ'))"
using separation_ax
by simp
ultimately
show ?thesis
by(rule_tac separation_cong[THEN iffD2,OF iff_trans[OF 0 1]],clarify,force)
qed
lemma separation_sat_after_function:
assumes "[a, b, c, d, τ]∈list(M)" and "χ∈formula" and "arity(χ) ≤ 7"
and
f_fm: "f_fm ∈ formula" and
f_ar: "arity(f_fm) ≤ 7" and
fsats: "⋀ fx x. fx∈M ⟹ x∈M ⟹ (M,[fx,x]@[a, b, c, d, τ] ⊨ f_fm) ⟷ fx=f(x)" and
fclosed: "⋀x . x∈M ⟹ f(x) ∈ M" and
g_fm: "g_fm ∈ formula" and
g_ar: "arity(g_fm) ≤ 8" and
gsats: "⋀ gx fx x. gx∈M ⟹ fx∈M ⟹ x∈M ⟹ (M,[gx,fx,x]@[a, b, c, d, τ] ⊨ g_fm) ⟷ gx=g(x)" and
gclosed: "⋀x . x∈M ⟹ g(x) ∈ M"
shows "separation(##M, λr. M, [f(r), a, b, c, d, τ, g(r)] ⊨ χ)"
proof -
note types = assms(1-3)
let ?φ="χ"
let ?ψ="ren(?φ)`7`8`ren_V_fn"
let ?ψ'="Exists(And(f_fm,Exists(And(g_fm,?ψ))))"
let ?ρ="λz.[f(z), a, b, c, d, τ, g(z)]"
let ?env="[a, b, c, d, τ]"
let ?η="λz.[g(z),f(z),z]@?env"
note types
moreover from this
have "?φ∈formula" by simp
moreover from calculation
have "arity(?φ) ≤ 8" "?ψ∈formula"
using ord_simp_union ren_tc ren_V_thm(2)[folded ren_V_fn_def] le_trans[of "arity(χ)" 7]
by simp_all
moreover from calculation
have "arity(?ψ) ≤ 8" "?ψ'∈formula"
using arity_ren ren_V_thm(2)[folded ren_V_fn_def] f_fm g_fm
by (simp_all)
moreover from calculation f_ar g_ar f_fm g_fm
have "arity(?ψ') ≤ 6"
using ord_simp_union pred_le arity_type
by (simp add:arity)
moreover from calculation fclosed gclosed
have 0:"(M, ?ρ(z) ⊨ ?φ) ⟷ (M,?η(z)⊨ ?ψ)" if "(##M)(z)" for z
using sats_iff_sats_ren[of ?φ 7 8 "?ρ(z)" _ "?η(z)"]
ren_V_thm(1)[where A=M,folded ren_V_fn_def] ren_V_thm(2)[folded ren_V_fn_def] that
by simp
moreover from calculation
have 1:"(M,?η(z)⊨ ?ψ) ⟷ M,[z]@?env⊨?ψ'" if "(##M)(z)" for z
using that fsats[OF fclosed[of z],of z] gsats[of "g(z)" "f(z)" z]
fclosed gclosed f_fm g_fm
apply(rule_tac iffI,simp,rule_tac rev_bexI[where x="f(z)"],simp)
apply(auto)[1]
proof -
assume "M, [z] @ [a, b, c, d, τ] ⊨ (⋅∃⋅f_fm ∧ (⋅∃⋅g_fm ∧ ren(χ) ` 7 ` 8 ` ren_V_fn⋅⋅)⋅⋅)"
then have "∃xa∈M. (M, [xa, z, a, b, c, d, τ] ⊨ f_fm) ∧
(∃x∈M. (M, [x, xa, z, a, b, c, d, τ] ⊨ g_fm) ∧ (M, [x, xa, z, a, b, c, d, τ] ⊨ ren(χ) ` 7 ` 8 ` ren_V_fn))"
using that calculation by auto
then
obtain xa where "xa∈M" "M, [xa, z, a, b, c, d, τ] ⊨ f_fm"
"(∃x∈M. (M, [x, xa, z, a, b, c, d, τ] ⊨ g_fm) ∧ (M, [x, xa, z, a, b, c, d, τ] ⊨ ren(χ) ` 7 ` 8 ` ren_V_fn))"
by auto
moreover from this
have "xa=f(z)" using fsats[of xa] that by simp
moreover from calculation
obtain x where "x∈M" "M, [x, xa, z, a, b, c, d, τ] ⊨ g_fm" "M, [x, xa, z, a, b, c, d, τ] ⊨ ren(χ) ` 7 ` 8 ` ren_V_fn"
by auto
moreover from calculation
have "x=g(z)" using gsats[of x xa] that by simp
ultimately
show "M, [g(z), f(z), z] @ [a, b, c, d, τ] ⊨ ren(χ) ` 7 ` 8 ` ren_V_fn"
by auto
qed
moreover from calculation
have "separation(##M, λz. (M,[z]@?env ⊨ ?ψ'))"
using separation_ax
by simp_all
ultimately
show ?thesis
by(rule_tac separation_cong[THEN iffD2,OF iff_trans[OF 0 1]],clarify,force)
qed
end
definition separation_assm_fm :: "[i,i,i] ⇒ i"
where
"separation_assm_fm(A,x,f_fm) ≡ (⋅∃ (⋅∃ ⋅⋅0 ∈ A +⇩ω 2⋅ ∧ ⋅⋅⟨0,1⟩ is x+⇩ω 2 ⋅ ∧ f_fm ⋅⋅⋅)⋅)"
lemma separation_assm_fm_type[TC]:
"A ∈ ω ⟹ y ∈ ω ⟹ f_fm ∈ formula ⟹ separation_assm_fm(A, y,f_fm) ∈ formula"
unfolding separation_assm_fm_def
by simp
lemma arity_separation_assm_fm : "A ∈ ω ⟹ x ∈ ω ⟹ f_fm ∈ formula ⟹
arity(separation_assm_fm(A, x, f_fm)) = succ(A) ∪ succ(x) ∪ pred(pred(arity(f_fm)))"
using pred_Un_distrib
unfolding separation_assm_fm_def
by (auto simp add:arity)
definition separation_assm_bin_fm where
"separation_assm_bin_fm(A,y,f_fm) ≡
(⋅∃(⋅∃(⋅∃(⋅∃(⋅(⋅⋅3 ∈ A +⇩ω 4⋅ ∧ ⋅⟨3,2⟩ is y +⇩ω 4⋅⋅ ) ∧ ⋅f_fm ∧ ⋅ ⋅fst(3) is 0 ⋅ ∧ ⋅snd(3) is 1⋅⋅⋅⋅ ) ⋅)⋅)⋅)⋅) "
lemma separation_assm_bin_fm_type[TC]:
"A ∈ ω ⟹ y ∈ ω ⟹ f_fm ∈ formula ⟹ separation_assm_bin_fm(A, y,f_fm) ∈ formula"
unfolding separation_assm_bin_fm_def
by simp
lemma arity_separation_assm_bin_fm : "A ∈ ω ⟹ x ∈ ω ⟹ f_fm ∈ formula ⟹
arity(separation_assm_bin_fm(A, x, f_fm)) = succ(A) ∪ succ(x) ∪ (pred^4(arity(f_fm)))"
using pred_Un_distrib
unfolding separation_assm_bin_fm_def
by (auto simp add:arity)
context M_Z_trans
begin
lemma separation_assm_sats :
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ) = 2" and
fsats: "⋀env x y. env∈list(M) ⟹ x∈M ⟹ y∈M ⟹ (M,[x,y]@env ⊨ φ) ⟷ is_f(x,y)" and
fabs: "⋀x y. x∈M ⟹ y∈M ⟹ is_f(x,y) ⟷ y = f(x)" and
fclosed: "⋀x. x∈M ⟹ f(x) ∈ M" and
"A∈M"
shows "separation(##M, λy. ∃x ∈ M . x∈A ∧ y = ⟨x, f(x)⟩)"
proof -
let ?φ'="separation_assm_fm(1,0,φ)"
let ?p="λy. ∃x∈M . x∈A ∧ y = ⟨x, f(x)⟩"
from f_fm
have "?φ'∈formula"
by simp
moreover from this f_ar f_fm
have "arity(?φ') = 2"
using arity_separation_assm_fm[of 1 0 φ] ord_simp_union
by simp
moreover from ‹A∈M› calculation
have "separation(##M,λy . M,[y,A] ⊨ ?φ')"
using separation_ax by auto
moreover
have "y∈M ⟹ (M,[y,A] ⊨ ?φ') ⟷ ?p(y)" for y
using assms transitivity[OF _ ‹A∈M›]
unfolding separation_assm_fm_def
by auto
ultimately
show ?thesis
by(rule_tac separation_cong[THEN iffD1],auto)
qed
lemma separation_assm_bin_sats :
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ) = 3" and
fsats: "⋀env x z y. env∈list(M) ⟹ x∈M ⟹ z∈M ⟹ y∈M ⟹ (M,[x,z,y]@env ⊨ φ) ⟷ is_f(x,z,y)" and
fabs: "⋀x z y. x∈M ⟹ z∈M ⟹ y∈M ⟹ is_f(x,z,y) ⟷ y = f(x,z)" and
fclosed: "⋀x z . x∈M ⟹ z∈M ⟹ f(x,z) ∈ M" and
"A∈M"
shows "separation(##M, λy. ∃x ∈ M . x∈A ∧ y = ⟨x, f(fst(x),snd(x))⟩)"
proof -
let ?φ'="separation_assm_bin_fm(1,0,φ)"
let ?p="λy. ∃x∈M . x∈A ∧ y = ⟨x, f(fst(x),snd(x))⟩"
from f_fm
have "?φ'∈formula"
by simp
moreover from this f_ar f_fm
have "arity(?φ') = 2"
using arity_separation_assm_bin_fm[of 1 0 φ] ord_simp_union
by simp
moreover from ‹A∈M› calculation
have "separation(##M,λy . M,[y,A] ⊨ ?φ')"
using separation_ax by auto
moreover
have "y∈M ⟹ (M,[y,A] ⊨ ?φ') ⟷ ?p(y)" for y
using assms transitivity[OF _ ‹A∈M›] pair_in_M_iff fst_abs snd_abs fst_closed snd_closed
unfolding separation_assm_bin_fm_def
by auto
ultimately
show ?thesis
by(rule_tac separation_cong[THEN iffD1],auto)
qed
lemma separation_Union: "A∈M ⟹
separation(##M, λy. ∃x ∈ M . x∈A ∧ y = ⟨x, Union(x)⟩)"
using separation_assm_sats[of "big_union_fm(0,1)"] arity_big_union_fm ord_simp_union
Union_closed[simplified]
by simp
lemma lam_replacement_Union: "lam_replacement(##M, Union)"
using lam_replacement_Union' separation_Union transM by simp
lemma separation_fst: "A∈M ⟹
separation(##M, λy. ∃x ∈ M . x∈A ∧ y = ⟨x, fst(x)⟩)"
using separation_assm_sats[of "fst_fm(0,1)"] arity_fst_fm ord_simp_union
fst_closed fst_abs
by simp
lemma lam_replacement_fst: "lam_replacement(##M, fst)"
using lam_replacement_fst' separation_fst transM by simp
lemma separation_snd: "A∈M ⟹
separation(##M, λy. ∃x ∈ M . x∈A ∧ y = ⟨x, snd(x)⟩)"
using separation_assm_sats[of "snd_fm(0,1)"] arity_snd_fm ord_simp_union
snd_closed[simplified] snd_abs
by simp
lemma lam_replacement_snd: "lam_replacement(##M, snd)"
using lam_replacement_snd' separation_snd transM by simp
text‹Binary lambda-replacements›
lemma separation_Image: "A∈M ⟹
separation(##M, λy. ∃x∈M. x ∈ A ∧ y = ⟨x, fst(x) `` snd(x)⟩)"
using arity_image_fm ord_simp_union
nonempty image_closed image_abs
by (rule_tac separation_assm_bin_sats[of "image_fm(0,1,2)"],auto)
lemma lam_replacement_Image: "lam_replacement(##M, λx . fst(x) `` snd(x))"
using lam_replacement_Image' separation_Image
by simp
lemma separation_middle_del: "A∈M ⟹
separation(##M, λy. ∃x∈M. x ∈ A ∧ y = ⟨x, middle_del(fst(x), snd(x))⟩)"
using arity_is_middle_del_fm ord_simp_union nonempty
fst_abs snd_abs fst_closed snd_closed pair_in_M_iff
by (rule_tac separation_assm_bin_sats[of "is_middle_del_fm(0,1,2)"],
auto simp:is_middle_del_def middle_del_def)
lemma lam_replacement_middle_del: "lam_replacement(##M, λr . middle_del(fst(r),snd(r)))"
using lam_replacement_middle_del' separation_middle_del
by simp
lemma separation_prodRepl: "A∈M ⟹
separation(##M, λy. ∃x∈M. x ∈ A ∧ y = ⟨x, prodRepl(fst(x), snd(x))⟩)"
using arity_is_prodRepl_fm ord_simp_union nonempty
fst_abs snd_abs fst_closed snd_closed pair_in_M_iff
by (rule_tac separation_assm_bin_sats[of "is_prodRepl_fm(0,1,2)"],
auto simp:is_prodRepl_def prodRepl_def)
lemma lam_replacement_prodRepl: "lam_replacement(##M, λr . prodRepl(fst(r),snd(r)))"
using lam_replacement_prodRepl' separation_prodRepl
by simp
end
context M_trivial
begin
lemma first_closed:
"M(B) ⟹ M(r) ⟹ first(u,r,B) ⟹ M(u)"
using transM[OF first_is_elem] by simp
is_iff_rel for "first"
unfolding is_first_def first_rel_def by auto
is_iff_rel for "minimum"
unfolding is_minimum_def minimum_rel_def
using is_first_iff The_abs nonempty
by force
end
context M_Z_trans
begin
lemma (in M_basic) is_minimum_equivalence :
"M(R) ⟹ M(X) ⟹ M(u) ⟹ is_minimum(M,R,X,u) ⟷ is_minimum'(M,R,X,u)"
unfolding is_minimum_def is_minimum'_def is_The_def is_first_def by simp
lemma separation_minimum: "A∈M ⟹
separation(##M, λy. ∃x∈M. x ∈ A ∧ y = ⟨x, minimum(fst(x), snd(x))⟩)"
using arity_minimum_fm ord_simp_union is_minimum_iff minimum_abs
is_minimum_equivalence nonempty minimum_closed minimum_abs
by (rule_tac separation_assm_bin_sats[of "minimum_fm(0,1,2)"], auto)
lemma lam_replacement_minimum: "lam_replacement(##M, λx . minimum(fst(x),snd(x)))"
using lam_replacement_minimum' separation_minimum
by simp
end
end