Theory Lambda_Replacement
section‹Replacements using Lambdas›
theory Lambda_Replacement
imports
Discipline_Function
begin
text‹In this theory we prove several instances of separation and replacement
in @{locale M_basic}. Moreover we introduce a new locale assuming two instances
of separation and six instances of lambda replacements (ie, replacement of
the form $\lambda x y.\ y=\langle x, f(x) \rangle$) and we prove a bunch of other
instances.›
definition
lam_replacement :: "[i⇒o,i⇒i] ⇒ o" where
"lam_replacement(M,b) ≡ strong_replacement(M, λx y. y = ⟨x, b(x)⟩)"
lemma separation_univ :
shows "separation(M,M)"
unfolding separation_def by auto
context M_trivial
begin
lemma lam_replacement_iff_lam_closed:
assumes "∀x[M]. M(b(x))"
shows "lam_replacement(M, b) ⟷ (∀A[M]. M(λx∈A. b(x)))"
using assms lam_closed lam_funtype[of _ b, THEN Pi_memberD]
unfolding lam_replacement_def strong_replacement_def
by (auto intro:lamI dest:transM)
(rule lam_closed, auto simp add:strong_replacement_def dest:transM)
lemma lam_replacement_imp_lam_closed:
assumes "lam_replacement(M, b)" "M(A)" "∀x∈A. M(b(x))"
shows "M(λx∈A. b(x))"
using assms unfolding lam_replacement_def
by (rule_tac lam_closed, auto simp add:strong_replacement_def dest:transM)
lemma lam_replacement_cong:
assumes "lam_replacement(M,f)" "∀x[M]. f(x) = g(x)" "∀x[M]. M(f(x))"
shows "lam_replacement(M,g)"
proof -
note assms
moreover from this
have "∀A[M]. M(λx∈A. f(x))"
using lam_replacement_iff_lam_closed
by simp
moreover from calculation
have "(λx∈A . f(x)) = (λx∈A . g(x))" if "M(A)" for A
using lam_cong[OF refl,of A f g] transM[OF _ that]
by simp
ultimately
show ?thesis
using lam_replacement_iff_lam_closed
by simp
qed
end
context M_basic
begin
lemma separation_iff':
assumes "separation(M,λx . P(x))" "separation(M,λx . Q(x))"
shows "separation(M,λx . P(x) ⟷ Q(x))"
using assms separation_conj separation_imp iff_def
by auto
lemma separation_in_constant :
assumes "M(a)"
shows "separation(M,λx . x∈a)"
proof -
have "{x∈A . x∈a} = A ∩ a" for A by auto
with ‹M(a)›
show ?thesis using separation_iff Collect_abs
by simp
qed
lemma separation_equal :
shows "separation(M,λx . x=a)"
proof -
have "{x∈A . x=a} = (if a∈A then {a} else 0)" for A
by auto
then
have "M({x∈A . x=a})" if "M(A)" for A
using transM[OF _ ‹M(A)›] by simp
then
show ?thesis using separation_iff Collect_abs
by simp
qed
lemma (in M_basic) separation_in_rev:
assumes "(M)(a)"
shows "separation(M,λx . a∈x)"
proof -
have eq: "{x∈A. a∈x} = Memrel(A∪{a}) `` {a}" for A
unfolding ZF_Base.image_def
by(intro equalityI,auto simp:mem_not_refl)
moreover from assms
have "M(Memrel(A∪{a}) `` {a})" if "M(A)" for A
using that by simp
ultimately
show ?thesis
using separation_iff Collect_abs
by simp
qed
lemma lam_replacement_imp_strong_replacement_aux:
assumes "lam_replacement(M, b)" "∀x[M]. M(b(x))"
shows "strong_replacement(M, λx y. y = b(x))"
proof -
{
fix A
note assms
moreover
assume "M(A)"
moreover from calculation
have "M(λx∈A. b(x))" using lam_replacement_iff_lam_closed by auto
ultimately
have "M((λx∈A. b(x))``A)" "∀z[M]. z ∈ (λx∈A. b(x))``A ⟷ (∃x∈A. z = b(x))"
by (auto simp:lam_def)
}
then
show ?thesis unfolding strong_replacement_def
by clarsimp (rule_tac x="(λx∈A. b(x))``A" in rexI, auto)
qed
lemma strong_lam_replacement_imp_strong_replacement :
assumes "strong_replacement(M,λ x z . P(fst(x),snd(x)) ∧ z=⟨x,f(fst(x),snd(x))⟩)"
"⋀A . M(A) ⟹ ∀x∈A. P(X,x) ⟶ M(f(X,x))" "M(X)"
shows "strong_replacement(M,λ x z . P(X,x) ∧ z=f(X,x))"
unfolding strong_replacement_def
proof(clarsimp)
fix A
assume "M(A)"
moreover from this ‹M(X)›
have "M({X}×A)" (is "M(?A)")
by simp
moreover
have "fst(x) = X" if "x∈?A" for x
using that by auto
moreover from calculation assms
have "M({z . x∈?A , P(fst(x),snd(x)) ∧ z=⟨x,f(fst(x),snd(x))⟩})" (is "M(?F)")
using transM[of _ ?A]
by(rule_tac strong_replacement_closed,simp_all)
moreover
have "?F=({⟨x,f(fst(x),snd(x))⟩ . x∈ {x∈?A . P(fst(x),snd(x))}})" (is "_=(?G)")
by auto
moreover
note ‹M(?A)›
ultimately
have "M(?G``?A)"
by simp
moreover
have "?G``?A = {y . x∈?A , P(fst(x),snd(x)) ∧ y = f(fst(x),snd(x))}" (is "_=(?H)")
by auto
ultimately
show "∃Y[M]. ∀b[M]. b ∈ Y ⟷ (∃x∈A. P(X,x) ∧ b = f(X,x))"
by(rule_tac rexI[of _ ?H],auto,force)
qed
lemma lam_replacement_imp_RepFun_Lam:
assumes "lam_replacement(M, f)" "M(A)"
shows "M({y . x∈A , M(y) ∧ y=⟨x,f(x)⟩})"
proof -
from assms
obtain Y where 1:"M(Y)" "∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ A ∧ b = ⟨x,f(x)⟩)"
unfolding lam_replacement_def strong_replacement_def
by auto
moreover from calculation
have "Y = {y . x∈A , M(y) ∧ y = ⟨x,f(x)⟩}" (is "Y=?R")
proof(intro equalityI subsetI)
fix y
assume "y∈Y"
moreover from this 1
obtain x where "x∈A" "y=⟨x,f(x)⟩" "M(y)"
using transM[OF _ ‹M(Y)›] by auto
ultimately
show "y∈?R"
by auto
next
fix z
assume "z∈?R"
moreover from this
obtain a where "a∈A" "z=⟨a,f(a)⟩" "M(a)" "M(f(a))"
using transM[OF _ ‹M(A)›]
by auto
ultimately
show "z∈Y" using 1 by simp
qed
ultimately
show ?thesis by auto
qed
lemma lam_closed_imp_closed:
assumes "∀A[M]. M(λx∈A. f(x))"
shows "∀x[M]. M(f(x))"
proof
fix x
assume "M(x)"
moreover from this and assms
have "M(λx∈{x}. f(x))" by simp
ultimately
show "M(f(x))"
using image_lam[of "{x}" "{x}" f]
image_closed[of "{x}" "(λx∈{x}. f(x))"] by (auto dest:transM)
qed
lemma lam_replacement_if:
assumes "lam_replacement(M,f)" "lam_replacement(M,g)" "separation(M,b)"
"∀x[M]. M(f(x))" "∀x[M]. M(g(x))"
shows "lam_replacement(M, λx. if b(x) then f(x) else g(x))"
proof -
let ?G="λx. if b(x) then f(x) else g(x)"
let ?b="λA . {x∈A. b(x)}" and ?b'="λA . {x∈A. ¬b(x)}"
have eq:"(λx∈A . ?G(x)) = (λx∈?b(A) . f(x)) ∪ (λx∈?b'(A).g(x))" for A
unfolding lam_def by auto
have "?b'(A) = A - ?b(A)" for A by auto
moreover
have "M(?b(A))" if "M(A)" for A using assms that by simp
moreover from calculation
have "M(?b'(A))" if "M(A)" for A using that by simp
moreover from calculation assms
have "M(λx∈?b(A). f(x))" "M(λx∈?b'(A) . g(x))" if "M(A)" for A
using lam_replacement_iff_lam_closed that
by simp_all
moreover from this
have "M((λx∈?b(A) . f(x)) ∪ (λx∈?b'(A).g(x)))" if "M(A)" for A
using that by simp
ultimately
have "M(λx∈A. if b(x) then f(x) else g(x))" if "M(A)" for A
using that eq by simp
with assms
show ?thesis using lam_replacement_iff_lam_closed by simp
qed
lemma lam_replacement_constant: "M(b) ⟹ lam_replacement(M,λ_. b)"
unfolding lam_replacement_def strong_replacement_def
by safe (rule_tac x="_×{b}" in rexI; blast)
subsection‹Replacement instances obtained through Powerset›
txt‹The next few lemmas provide bounds for certain constructions.›
lemma not_functional_Replace_0:
assumes "¬(∀y y'. P(y) ∧ P(y') ⟶ y=y')"
shows "{y . x ∈ A, P(y)} = 0"
using assms by (blast elim!: ReplaceE)
lemma Replace_in_Pow_rel:
assumes "⋀x b. x ∈ A ⟹ P(x,b) ⟹ b ∈ U" "∀x∈A. ∀y y'. P(x,y) ∧ P(x,y') ⟶ y=y'"
"separation(M, λy. ∃x[M]. x ∈ A ∧ P(x, y))"
"M(U)" "M(A)"
shows "{y . x ∈ A, P(x, y)} ∈ Pow⇗M⇖(U)"
proof -
from assms
have "{y . x ∈ A, P(x, y)} ⊆ U"
"z ∈ {y . x ∈ A, P(x, y)} ⟹ M(z)" for z
by (auto dest:transM)
with assms
have "{y . x ∈ A, P(x, y)} = {y∈U . ∃x[M]. x∈A ∧ P(x,y)}"
by (intro equalityI) (auto, blast)
with assms
have "M({y . x ∈ A, P(x, y)})"
by simp
with assms
show ?thesis
using mem_Pow_rel_abs by auto
qed
lemma Replace_sing_0_in_Pow_rel:
assumes "⋀b. P(b) ⟹ b ∈ U"
"separation(M, λy. P(y))" "M(U)"
shows "{y . x ∈ {0}, P(y)} ∈ Pow⇗M⇖(U)"
proof (cases "∀y y'. P(y) ∧ P(y') ⟶ y=y'")
case True
with assms
show ?thesis by (rule_tac Replace_in_Pow_rel) auto
next
case False
with assms
show ?thesis
using nonempty not_functional_Replace_0[of P "{0}"] Pow_rel_char by auto
qed
lemma The_in_Pow_rel_Union:
assumes "⋀b. P(b) ⟹ b ∈ U" "separation(M, λy. P(y))" "M(U)"
shows "(THE i. P(i)) ∈ Pow⇗M⇖(⋃U)"
proof -
note assms
moreover from this
have "(THE i. P(i)) ∈ Pow(⋃U)"
unfolding the_def by auto
moreover from assms
have "M(THE i. P(i))"
using Replace_sing_0_in_Pow_rel[of P U] unfolding the_def
by (auto dest:transM)
ultimately
show ?thesis
using Pow_rel_char by auto
qed
lemma separation_least: "separation(M, λy. Ord(y) ∧ P(y) ∧ (∀j. j < y ⟶ ¬ P(j)))"
unfolding separation_def
proof
fix z
assume "M(z)"
have "M({x ∈ z . x ∈ z ∧ Ord(x) ∧ P(x) ∧ (∀j. j < x ⟶ ¬ P(j))})"
(is "M(?y)")
proof (cases "∃x∈z. Ord(x) ∧ P(x) ∧ (∀j. j < x ⟶ ¬ P(j))")
case True
with ‹M(z)›
have "∃x[M]. ?y = {x}"
by (safe, rename_tac x, rule_tac x=x in rexI)
(auto dest:transM, intro equalityI, auto elim:Ord_linear_lt)
then
show ?thesis
by auto
next
case False
then
have "{x ∈ z . x ∈ z ∧ Ord(x) ∧ P(x) ∧ (∀j. j < x ⟶ ¬ P(j))} = 0"
by auto
then
show ?thesis by auto
qed
moreover from this
have "∀x[M]. x ∈ ?y ⟷ x ∈ z ∧ Ord(x) ∧ P(x) ∧ (∀j. j < x ⟶ ¬ P(j))" by simp
ultimately
show "∃y[M]. ∀x[M]. x ∈ y ⟷ x ∈ z ∧ Ord(x) ∧ P(x) ∧ (∀j. j < x ⟶ ¬ P(j))"
by blast
qed
lemma Least_in_Pow_rel_Union:
assumes "⋀b. P(b) ⟹ b ∈ U"
"M(U)"
shows "(μ i. P(i)) ∈ Pow⇗M⇖(⋃U)"
using assms separation_least unfolding Least_def
by (rule_tac The_in_Pow_rel_Union) simp
lemma bounded_lam_replacement:
fixes U
assumes "∀X[M]. ∀x∈X. f(x) ∈ U(X)"
and separation_f:"∀A[M]. separation(M,λy. ∃x[M]. x∈A ∧ y = ⟨x, f(x)⟩)"
and U_closed [intro,simp]: "⋀X. M(X) ⟹ M(U(X))"
shows "lam_replacement(M, f)"
proof -
have "M(λx∈A. f(x))" if "M(A)" for A
proof -
have "(λx∈A. f(x)) = {y∈ Pow⇗M⇖(Pow⇗M⇖(A ∪ U(A))). ∃x[M]. x∈A ∧ y = ⟨x, f(x)⟩}"
using ‹M(A)› unfolding lam_def
proof (intro equalityI, auto)
fix x
assume "x∈A"
moreover
note ‹M(A)›
moreover from calculation assms
have "f(x) ∈ U(A)" by simp
moreover from calculation
have "{x, f(x)} ∈ Pow⇗M⇖(A ∪ U(A))" "{x,x} ∈ Pow⇗M⇖(A ∪ U(A))"
using Pow_rel_char[of "A ∪ U(A)"] by (auto dest:transM)
ultimately
show "⟨x, f(x)⟩ ∈ Pow⇗M⇖(Pow⇗M⇖(A ∪ U(A)))"
using Pow_rel_char[of "Pow⇗M⇖(A ∪ U(A))"] unfolding Pair_def
by (auto dest:transM)
qed
moreover from ‹M(A)›
have "M({y∈ Pow⇗M⇖(Pow⇗M⇖(A ∪ U(A))). ∃x[M]. x∈A ∧ y = ⟨x, f(x)⟩})"
using separation_f
by (rule_tac separation_closed) simp_all
ultimately
show ?thesis
by simp
qed
moreover from this
have "∀x[M]. M(f(x))"
using lam_closed_imp_closed by simp
ultimately
show ?thesis
using assms
by (rule_tac lam_replacement_iff_lam_closed[THEN iffD2]) simp_all
qed
lemma fst_in_double_Union:
assumes "x∈X"
shows "fst(x) ∈ {0} ∪ ⋃⋃X"
proof -
have "fst(x) ∈ {0} ∪ ⋃x" for x
unfolding fst_def
using the_0 fst_conv
by(cases "∃!a.∃b. x = ⟨a,b⟩", auto, simp add:Pair_def)
with assms
show ?thesis by auto
qed
lemma snd_in_double_Union:
assumes "x∈X"
shows "snd(x) ∈ {0} ∪ ⋃⋃X"
proof -
have "snd(x) ∈ {0} ∪ ⋃x" for x
unfolding snd_def
using the_0 snd_conv
by(cases "∃!a.∃b. x = ⟨a,b⟩", auto, simp add:Pair_def)
with assms
show ?thesis by auto
qed
lemma bounded_lam_replacement_binary:
fixes U
assumes "∀X[M]. ∀x∈X. ∀y∈X. f(x,y) ∈ U(X)"
and separation_f:"∀A[M]. separation(M,λy. ∃x[M]. x∈A ∧ y = ⟨x, f(fst(x),snd(x))⟩)"
and U_closed [intro,simp]: "⋀X. M(X) ⟹ M(U(X))"
shows "lam_replacement(M, λr . f(fst(r),snd(r)))"
proof -
have "M(λx∈A. f(fst(x),snd(x)))" if "M(A)" for A
proof -
have "(λx∈A. f(fst(x),snd(x))) =
{y∈ Pow⇗M⇖(Pow⇗M⇖(A ∪ U({0} ∪ ⋃⋃A))). ∃x[M]. x∈A ∧ y = ⟨x, f(fst(x),snd(x))⟩}"
using ‹M(A)› unfolding lam_def
proof (intro equalityI, auto)
fix x
assume "x∈A"
moreover
note ‹M(A)›
moreover from calculation assms
have "f(fst(x),snd(x)) ∈ U({0} ∪ ⋃⋃A)"
using fst_in_double_Union snd_in_double_Union by simp
moreover from calculation
have "{x, f(fst(x),snd(x))} ∈ Pow⇗M⇖(A ∪ U({0} ∪ ⋃⋃A))"
"{x,x} ∈ Pow⇗M⇖(A ∪ U({0} ∪ ⋃⋃A))"
using Pow_rel_char[of "A ∪ U({0} ∪ ⋃⋃A)"] by (auto dest:transM)
ultimately
show "⟨x, f(fst(x),snd(x))⟩ ∈ Pow⇗M⇖(Pow⇗M⇖(A ∪ U({0} ∪ ⋃⋃A)))"
using Pow_rel_char[of "Pow⇗M⇖(A ∪ U({0} ∪ ⋃⋃A))"] unfolding Pair_def
by (auto dest:transM)
qed
moreover from ‹M(A)›
have "M({y∈ Pow⇗M⇖(Pow⇗M⇖(A ∪ U({0} ∪ ⋃⋃A))). ∃x[M]. x∈A ∧ y = ⟨x, f(fst(x),snd(x))⟩})"
using separation_f
by (rule_tac separation_closed) simp_all
ultimately
show ?thesis
by simp
qed
moreover from this
have "∀x[M]. M(f(fst(x),snd(x)))"
using lam_closed_imp_closed[of "λx. f(fst(x),snd(x))"] by simp
ultimately
show ?thesis
using assms
by (rule_tac lam_replacement_iff_lam_closed[THEN iffD2]) simp_all
qed
lemma lam_replacement_fst':
assumes "∀A[M]. separation(M, λy. ∃x[M]. x∈A ∧ y = ⟨x, fst(x)⟩)"
shows "lam_replacement(M,fst)"
using fst_in_double_Union assms
bounded_lam_replacement[of fst "λX. {0} ∪ ⋃⋃X"] by simp
lemma lam_replacement_snd':
assumes "∀A[M]. separation(M, λy. ∃x[M]. x∈A ∧ y = ⟨x, snd(x)⟩)"
shows "lam_replacement(M,snd)"
using snd_in_double_Union assms
bounded_lam_replacement[of snd "λX. {0} ∪ ⋃⋃X"] by simp
lemma lam_replacement_restrict:
assumes "∀A[M]. separation(M, λy. ∃x[M]. x∈A ∧ y = ⟨x, restrict(x,B)⟩)" "M(B)"
shows "lam_replacement(M, λr . restrict(r,B))"
proof -
from assms
have "restrict(r,B)∈Pow⇗M⇖(⋃R)" if "M(R)" "r∈R" for r R
using Union_upper subset_Pow_Union subset_trans[OF restrict_subset]
Pow_rel_char that transM[of _ R]
by auto
with assms
show ?thesis
using bounded_lam_replacement[of "λr . restrict(r,B)" "λX. Pow⇗M⇖(⋃X)"]
by simp
qed
lemma lam_replacement_Union' :
assumes "∀A[M]. separation(M, λy. ∃x[M]. x ∈ A ∧ y = ⟨x, ⋃x⟩)"
shows "lam_replacement(M,Union)"
proof -
have "⋃x ∈ Pow(⋃⋃A)" if "x∈A" for x A
using that by auto
then
have "⋃x ∈ Pow⇗M⇖(⋃⋃A)" if "M(A)" "x∈A" for x A
using that transM[of x A] Pow_rel_char
by auto
with assms
show ?thesis
using bounded_lam_replacement[where U="λA . Pow⇗M⇖(⋃⋃A)"]
by auto
qed
lemma Image_in_Pow_rel_Union3:
assumes "x∈X" "y∈X" "M(X)"
shows "Image(x,y) ∈ Pow⇗M⇖(⋃⋃⋃X)"
proof -
from assms
have "⟨a, b⟩ ∈ x ⟹ b ∈ ⋃⋃x" for a b
unfolding Pair_def by (auto dest:transM)
moreover from this and assms
have "⟨a, b⟩ ∈ x ⟹ M(b)" for a b
using transM[of _ X] transM[of _ x]
by auto
ultimately
show ?thesis
using assms transM[of _ X] transM[of _ x] mem_Pow_rel_abs
by auto fast
qed
lemma lam_replacement_Image':
assumes
"∀A[M]. separation(M,λy. ∃x[M]. x∈A ∧ y = ⟨x, Image(fst(x),snd(x))⟩)"
shows
"lam_replacement(M, λr . Image(fst(r),snd(r)))"
using assms Image_in_Pow_rel_Union3
by (rule_tac bounded_lam_replacement_binary[of _ "λX. Pow⇗M⇖(⋃⋃⋃X)"]) auto
lemma minimum_in_Union:
assumes "x∈X" "y∈X"
shows "minimum(x,y) ∈ {0} ∪ ⋃X"
using assms minimum_in'
by auto
lemma lam_replacement_minimum':
assumes
"∀A[M]. separation(M,λy. ∃x[M]. x∈A ∧ y = ⟨x, minimum(fst(x),snd(x))⟩)"
shows
"lam_replacement(M, λr . minimum(fst(r),snd(r)))"
using assms minimum_in_Union
by (rule_tac bounded_lam_replacement_binary[of _ "λX. {0} ∪ ⋃X"]) auto
lemma lam_replacement_Pow_rel:
assumes "∀A[M]. separation(M, λy. ∃x[M]. x ∈ A ∧ y = ⟨x, Pow_rel(M,x)⟩)"
shows "lam_replacement(M,Pow_rel(M))"
proof -
have "Pow_rel(M,x) ∈ Pow(Pow(⋃A))" if "x∈A" "M(A)" for x A
using that transM[of x A] def_Pow_rel[of _ x] by (auto dest:transM)
then
have "Pow_rel(M,x) ∈ Pow(Pow⇗M⇖(⋃A))" if "M(A)" "x∈A" for x A
using that transM[of x A] Pow_rel_char
by auto
then
have "Pow_rel(M,x) ∈ Pow⇗M⇖(Pow⇗M⇖(⋃A))" if "M(A)" "x∈A" for x A
using that transM[of x A] Pow_rel_char[of "Pow⇗M⇖(⋃A)"]
by auto
with assms
show ?thesis
using bounded_lam_replacement[where U="λA. Pow⇗M⇖(Pow⇗M⇖(⋃A))"]
by auto
qed
end
definition
middle_del :: "i⇒i⇒i" where
"middle_del(x,y) ≡ ⟨fst(x),snd(y)⟩"
relativize functional "middle_del" "middle_del_rel"
relationalize "middle_del_rel" "is_middle_del"
synthesize "is_middle_del" from_definition
arity_theorem for "is_middle_del_fm"
context M_basic
begin
lemma middle_del_in_cartprod:
assumes "x∈X" "y∈X" "M(X)"
shows "middle_del(x,y) ∈ ({0} ∪ ⋃⋃X) × ({0} ∪ ⋃⋃X)"
using assms Pow_rel_char transM[of _ X] fst_in_double_Union snd_in_double_Union
unfolding middle_del_def by auto
lemma lam_replacement_middle_del':
assumes
"∀A[M]. separation(M,λy. ∃x[M]. x∈A ∧ y = ⟨x, middle_del(fst(x),snd(x))⟩)"
shows
"lam_replacement(M, λr . middle_del(fst(r),snd(r)))"
using assms middle_del_in_cartprod
by (rule_tac bounded_lam_replacement_binary[of _ "λX. ({0} ∪ ⋃⋃X) × ({0} ∪ ⋃⋃X)"]) auto
end
definition
prodRepl :: "i⇒i⇒i" where
"prodRepl(x,y) ≡ ⟨snd(x),⟨fst(x),snd(y)⟩⟩"
relativize functional "prodRepl" "prodRepl_rel"
relationalize "prodRepl_rel" "is_prodRepl"
synthesize "is_prodRepl" from_definition
arity_theorem for "is_prodRepl_fm"
context M_basic
begin
lemma prodRepl_in_cartprod:
assumes "x∈X" "y∈X" "M(X)"
shows "prodRepl(x,y) ∈ ({0} ∪ ⋃⋃X) × ({0} ∪ ⋃⋃X) × ({0} ∪ ⋃⋃X)"
using assms Pow_rel_char transM[of _ X] fst_in_double_Union snd_in_double_Union
unfolding prodRepl_def by auto
lemma lam_replacement_prodRepl':
assumes
"∀A[M]. separation(M,λy. ∃x[M]. x∈A ∧ y = ⟨x, prodRepl(fst(x),snd(x))⟩)"
shows
"lam_replacement(M, λr . prodRepl(fst(r),snd(r)))"
using assms prodRepl_in_cartprod
by (rule_tac bounded_lam_replacement_binary[of _
"λX. ({0} ∪ ⋃⋃X) × ({0} ∪ ⋃⋃X) × ({0} ∪ ⋃⋃X)"]) auto
end
context M_Perm
begin
lemma inj_rel_in_Pow_rel_Pow_rel:
assumes "x∈X" "y∈X" "M(X)"
shows "inj⇗M⇖(x,y) ∈ Pow⇗M⇖(Pow⇗M⇖(⋃X × ⋃X))"
using assms transM[of _ X] mem_Pow_rel_abs inj_def Pi_def
by clarsimp (use inj_rel_char in auto)
lemma lam_replacement_inj_rel':
assumes
"∀A[M]. separation(M,λy. ∃x[M]. x∈A ∧ y = ⟨x, inj⇗M⇖(fst(x),snd(x))⟩)"
shows
"lam_replacement(M, λr . inj⇗M⇖(fst(r),snd(r)))"
using assms inj_rel_in_Pow_rel_Pow_rel
by (rule_tac bounded_lam_replacement_binary[of _ "λX. Pow⇗M⇖(Pow⇗M⇖(⋃X × ⋃X))"]) auto
end
locale M_replacement = M_basic +
assumes
lam_replacement_fst: "lam_replacement(M,fst)"
and
lam_replacement_snd: "lam_replacement(M,snd)"
and
lam_replacement_Union: "lam_replacement(M,Union)"
and
lam_replacement_middle_del: "lam_replacement(M, λr. middle_del(fst(r),snd(r)))"
and
lam_replacement_prodRepl: "lam_replacement(M, λr. prodRepl(fst(r),snd(r)))"
and
lam_replacement_Image:"lam_replacement(M, λp. fst(p) `` snd(p))"
and
middle_separation: "separation(M, λx. snd(fst(x))=fst(snd(x)))"
and
separation_fst_in_snd: "separation(M, λy. fst(snd(y)) ∈ snd(snd(y)))"
begin
lemma lam_replacement_imp_strong_replacement:
assumes "lam_replacement(M, f)"
shows "strong_replacement(M, λx y. y = f(x))"
proof -
{
fix A
assume "M(A)"
moreover from calculation assms
obtain Y where 1:"M(Y)" "∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ A ∧ b = ⟨x,f(x)⟩)"
unfolding lam_replacement_def strong_replacement_def
by auto
moreover from this
have "M({snd(b) . b ∈ Y})"
using transM[OF _ ‹M(Y)›] lam_replacement_snd lam_replacement_imp_strong_replacement_aux
RepFun_closed by simp
moreover
have "{snd(b) . b ∈ Y} = {y . x∈A , M(f(x)) ∧ y=f(x)}" (is "?L=?R")
proof(intro equalityI subsetI)
fix x
assume "x∈?L"
moreover from this
obtain b where "b∈Y" "x=snd(b)" "M(b)"
using transM[OF _ ‹M(Y)›] by auto
moreover from this 1
obtain a where "a∈A" "b=⟨a,f(a)⟩" by auto
moreover from calculation
have "x=f(a)" by simp
ultimately show "x∈?R"
by auto
next
fix z
assume "z∈?R"
moreover from this
obtain a where "a∈A" "z=f(a)" "M(a)" "M(f(a))"
using transM[OF _ ‹M(A)›]
by auto
moreover from calculation this 1
have "z=snd(⟨a,f(a)⟩)" "⟨a,f(a)⟩ ∈ Y" by auto
ultimately
show "z∈?L" by force
qed
ultimately
have "∃Z[M]. ∀z[M]. z∈Z ⟷ (∃a[M]. a∈A ∧ z=f(a))"
by (rule_tac rexI[where x="{snd(b) . b ∈ Y}"],auto)
}
then
show ?thesis unfolding strong_replacement_def by simp
qed
lemma Collect_middle: "{p ∈ (λx∈A. f(x)) × (λx∈{f(x) . x∈A}. g(x)) . snd(fst(p))=fst(snd(p))}
= { ⟨⟨x,f(x)⟩,⟨f(x),g(f(x))⟩⟩ . x∈A }"
by (intro equalityI; auto simp:lam_def)
lemma RepFun_middle_del: "{ ⟨fst(fst(p)),snd(snd(p))⟩ . p ∈ { ⟨⟨x,f(x)⟩,⟨f(x),g(f(x))⟩⟩ . x∈A }}
= { ⟨x,g(f(x))⟩ . x∈A }"
by auto
lemma lam_replacement_imp_RepFun:
assumes "lam_replacement(M, f)" "M(A)"
shows "M({y . x∈A , M(y) ∧ y=f(x)})"
proof -
from assms
obtain Y where 1:"M(Y)" "∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ A ∧ b = ⟨x,f(x)⟩)"
unfolding lam_replacement_def strong_replacement_def
by auto
moreover from this
have "M({snd(b) . b ∈ Y})"
using transM[OF _ ‹M(Y)›] lam_replacement_snd lam_replacement_imp_strong_replacement_aux
RepFun_closed by simp
moreover
have "{snd(b) . b ∈ Y} = {y . x∈A , M(y) ∧ y=f(x)}" (is "?L=?R")
proof(intro equalityI subsetI)
fix x
assume "x∈?L"
moreover from this
obtain b where "b∈Y" "x=snd(b)" "M(b)"
using transM[OF _ ‹M(Y)›] by auto
moreover from this 1
obtain a where "a∈A" "b=⟨a,f(a)⟩" by auto
moreover from calculation
have "x=f(a)" by simp
ultimately show "x∈?R"
by auto
next
fix z
assume "z∈?R"
moreover from this
obtain a where "a∈A" "z=f(a)" "M(a)" "M(f(a))"
using transM[OF _ ‹M(A)›]
by auto
moreover from calculation this 1
have "z=snd(⟨a,f(a)⟩)" "⟨a,f(a)⟩ ∈ Y" by auto
ultimately
show "z∈?L" by force
qed
ultimately
show ?thesis by simp
qed
lemma lam_replacement_product:
assumes "lam_replacement(M,f)" "lam_replacement(M,g)"
shows "lam_replacement(M, λx. ⟨f(x),g(x)⟩)"
proof -
{
fix A
let ?Y="{y . x∈A , M(y) ∧ y=f(x)}"
let ?Y'="{y . x∈A ,M(y) ∧ y=⟨x,f(x)⟩}"
let ?Z="{y . x∈A , M(y) ∧ y=g(x)}"
let ?Z'="{y . x∈A ,M(y) ∧ y=⟨x,g(x)⟩}"
have "x∈C ⟹ y∈C ⟹ fst(x) = fst(y) ⟶ M(fst(y)) ∧ M(snd(x)) ∧ M(snd(y))" if "M(C)" for C y x
using transM[OF _ that] by auto
moreover
note assms
moreover
assume "M(A)"
moreover from ‹M(A)› assms(1)
have "M(converse(?Y'))" "M(?Y)"
using lam_replacement_imp_RepFun_Lam lam_replacement_imp_RepFun by auto
moreover from calculation
have "M(?Z)" "M(?Z')"
using lam_replacement_imp_RepFun_Lam lam_replacement_imp_RepFun by auto
moreover from calculation
have "M(converse(?Y')×?Z')"
by simp
moreover from this
have "M({p ∈ converse(?Y')×?Z' . snd(fst(p))=fst(snd(p))})" (is "M(?P)")
using middle_separation by simp
moreover from calculation
have "M({ ⟨snd(fst(p)),⟨fst(fst(p)),snd(snd(p))⟩⟩ . p∈?P })" (is "M(?R)")
using RepFun_closed[OF lam_replacement_prodRepl[THEN
lam_replacement_imp_strong_replacement] ‹M(?P)› ]
unfolding prodRepl_def by simp
ultimately
have "b ∈ ?R ⟷ (∃x[M]. x ∈ A ∧ b = ⟨x,⟨f(x),g(x)⟩⟩)" if "M(b)" for b
using that
apply(intro iffI) apply(auto)[1]
proof -
assume " ∃x[M]. x ∈ A ∧ b = ⟨x, f(x), g(x)⟩"
moreover from this
obtain x where "M(x)" "x∈A" "b= ⟨x, ⟨f(x), g(x)⟩⟩"
by auto
moreover from calculation that
have "M(⟨x,f(x)⟩)" "M(⟨x,g(x)⟩)" by auto
moreover from calculation
have "⟨f(x),x⟩ ∈ converse(?Y')" "⟨x,g(x)⟩ ∈ ?Z'" by auto
moreover from calculation
have "⟨⟨f(x),x⟩,⟨x,g(x)⟩⟩∈converse(?Y')×?Z'" by auto
moreover from calculation
have "⟨⟨f(x),x⟩,⟨x,g(x)⟩⟩ ∈ ?P"
(is "?p∈?P")
by auto
moreover from calculation
have "b = ⟨snd(fst(?p)),⟨fst(fst(?p)),snd(snd(?p))⟩⟩" by auto
moreover from calculation
have "⟨snd(fst(?p)),⟨fst(fst(?p)),snd(snd(?p))⟩⟩∈?R"
by(rule_tac RepFunI[of ?p ?P], simp)
ultimately show "b∈?R" by simp
qed
with ‹M(?R)›
have "∃Y[M]. ∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ A ∧ b = ⟨x,⟨f(x),g(x)⟩⟩)"
by (rule_tac rexI[where x="?R"],simp_all)
}
with assms
show ?thesis using lam_replacement_def strong_replacement_def by simp
qed
lemma lam_replacement_hcomp:
assumes "lam_replacement(M,f)" "lam_replacement(M,g)" "∀x[M]. M(f(x))"
shows "lam_replacement(M, λx. g(f(x)))"
proof -
{
fix A
let ?Y="{y . x∈A , y=f(x)}"
let ?Y'="{y . x∈A , y=⟨x,f(x)⟩}"
have "∀x∈C. M(⟨fst(fst(x)),snd(snd(x))⟩)" if "M(C)" for C
using transM[OF _ that] by auto
moreover
note assms
moreover
assume "M(A)"
moreover from assms
have eq:"?Y = {y . x∈A ,M(y) ∧ y=f(x)}" "?Y' = {y . x∈A ,M(y) ∧ y=⟨x,f(x)⟩}"
using transM[OF _ ‹M(A)›] by auto
moreover from ‹M(A)› assms(1)
have "M(?Y')" "M(?Y)"
using lam_replacement_imp_RepFun_Lam lam_replacement_imp_RepFun eq by auto
moreover from calculation
have "M({z . y∈?Y , M(z) ∧ z=⟨y,g(y)⟩})" (is "M(?Z)")
using lam_replacement_imp_RepFun_Lam by auto
moreover from calculation
have "M(?Y'×?Z)"
by simp
moreover from this
have "M({p ∈ ?Y'×?Z . snd(fst(p))=fst(snd(p))})" (is "M(?P)")
using middle_separation by simp
moreover from calculation
have "M({ ⟨fst(fst(p)),snd(snd(p))⟩ . p∈?P })" (is "M(?R)")
using RepFun_closed[OF lam_replacement_middle_del[THEN
lam_replacement_imp_strong_replacement] ‹M(?P)›]
unfolding middle_del_def by simp
ultimately
have "b ∈ ?R ⟷ (∃x[M]. x ∈ A ∧ b = ⟨x,g(f(x))⟩)" if "M(b)" for b
using that assms(3)
apply(intro iffI) apply(auto)[1]
proof -
assume "∃x[M]. x ∈ A ∧ b = ⟨x, g(f(x))⟩"
moreover from this
obtain x where "M(x)" "x∈A" "b= ⟨x, g(f(x))⟩"
by auto
moreover from calculation that assms(3)
have "M(f(x))" "M(g(f(x)))" by auto
moreover from calculation
have "⟨x,f(x)⟩ ∈ ?Y'" by auto
moreover from calculation
have "⟨f(x),g(f(x))⟩∈?Z" by auto
moreover from calculation
have "⟨⟨x,f(x)⟩,⟨f(x),g(f(x))⟩⟩ ∈ ?P"
(is "?p∈?P")
by auto
moreover from calculation
have "b = ⟨fst(fst(?p)),snd(snd(?p))⟩" by auto
moreover from calculation
have "⟨fst(fst(?p)),snd(snd(?p))⟩∈?R"
by(rule_tac RepFunI[of ?p ?P], simp)
ultimately show "b∈?R" by simp
qed
with ‹M(?R)›
have "∃Y[M]. ∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ A ∧ b = ⟨x,g(f(x))⟩)"
by (rule_tac rexI[where x="?R"],simp_all)
}
with assms
show ?thesis using lam_replacement_def strong_replacement_def by simp
qed
lemma lam_replacement_hcomp2:
assumes "lam_replacement(M,f)" "lam_replacement(M,g)"
"∀x[M]. M(f(x))" "∀x[M]. M(g(x))"
"lam_replacement(M, λp. h(fst(p),snd(p)))"
shows "lam_replacement(M, λx. h(f(x),g(x)))"
using assms lam_replacement_product[of f g]
lam_replacement_hcomp[of "λx. ⟨f(x), g(x)⟩" "λ⟨x,y⟩. h(x,y)"]
unfolding split_def by simp
lemma lam_replacement_identity: "lam_replacement(M,λx. x)"
proof -
{
fix A
assume "M(A)"
moreover from this
have "id(A) = {⟨snd(fst(z)),fst(snd(z))⟩ . z∈ {z∈ (A×A)×(A×A). snd(fst(z)) = fst(snd(z))}}"
unfolding id_def lam_def
by(intro equalityI subsetI,simp_all,auto)
moreover from calculation
have "M({z∈ (A×A)×(A×A). snd(fst(z)) = fst(snd(z))})" (is "M(?A')")
using middle_separation by simp
moreover from calculation
have "M({⟨snd(fst(z)),fst(snd(z))⟩ . z∈ ?A'})"
using transM[of _ A]
lam_replacement_product lam_replacement_hcomp lam_replacement_fst lam_replacement_snd
lam_replacement_imp_strong_replacement[THEN RepFun_closed]
by simp_all
ultimately
have "M(id(A))" by simp
}
then
show ?thesis using lam_replacement_iff_lam_closed
unfolding id_def by simp
qed
lemma strong_replacement_separation_aux :
assumes "strong_replacement(M,λ x y . y=f(x))" "separation(M,P)"
shows "strong_replacement(M, λx y . P(x) ∧ y=f(x))"
proof -
{
fix A
let ?Q="λX. ∀b[M]. b ∈ X ⟷ (∃x[M]. x ∈ A ∧ P(x) ∧ b = f(x))"
assume "M(A)"
moreover from this
have "M({x∈A . P(x)})" (is "M(?B)") using assms by simp
moreover from calculation assms
obtain Y where "M(Y)" "∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ ?B ∧ b = f(x))"
unfolding strong_replacement_def by auto
then
have "∃Y[M]. ∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ A ∧ P(x) ∧ b = f(x))"
using rexI[of ?Q _ M] by simp
}
then
show ?thesis
unfolding strong_replacement_def by simp
qed
lemma separation_in:
assumes "∀x[M]. M(f(x))" "lam_replacement(M,f)"
"∀x[M]. M(g(x))" "lam_replacement(M,g)"
shows "separation(M,λx . f(x)∈g(x))"
proof -
let ?Z="λA. {⟨x,⟨f(x),g(x)⟩⟩. x∈A}"
have "M(?Z(A))" if "M(A)" for A
using assms lam_replacement_iff_lam_closed that
lam_replacement_product[of f g]
unfolding lam_def
by auto
then
have "M({u∈?Z(A) . fst(snd(u)) ∈snd(snd(u))})" (is "M(?W(A))") if "M(A)" for A
using that separation_fst_in_snd assms
by auto
then
have "M({fst(u) . u ∈ ?W(A)})" if "M(A)" for A
using that lam_replacement_imp_strong_replacement[OF lam_replacement_fst,THEN
RepFun_closed] fst_closed[OF transM]
by auto
moreover
have "{x∈A. f(x)∈g(x)} = {fst(u) . u∈?W(A)}" for A
by auto
ultimately
show ?thesis
using separation_iff
by auto
qed
lemma lam_replacement_swap: "lam_replacement(M, λx. ⟨snd(x),fst(x)⟩)"
using lam_replacement_fst lam_replacement_snd
lam_replacement_product[of "snd" "fst"] by simp
lemma relation_separation: "separation(M, λz. ∃x y. z = ⟨x, y⟩)"
unfolding separation_def
proof (clarify)
fix A
assume "M(A)"
moreover from this
have "{z∈A. ∃x y. z = ⟨x, y⟩} = {z∈A. ∃x∈domain(A). ∃y∈range(A). pair(M, x, y, z)}"
(is "?rel = _")
by (intro equalityI, auto dest:transM)
(intro bexI, auto dest:transM simp:Pair_def)
moreover from calculation
have "M(?rel)"
using cartprod_separation[THEN separation_closed, of "domain(A)" "range(A)" A]
by simp
ultimately
show "∃y[M]. ∀x[M]. x ∈ y ⟷ x ∈ A ∧ (∃w y. x = ⟨w, y⟩)"
by (rule_tac x="{z∈A. ∃x y. z = ⟨x, y⟩}" in rexI) auto
qed
lemma separation_Pair:
assumes "separation(M, λy . P(fst(y), snd(y)))"
shows "separation(M, λy. ∃ u v . y=⟨u,v⟩ ∧ P(u,v))"
unfolding separation_def
proof(clarify)
fix A
assume "M(A)"
moreover from this
have "M({z∈A. ∃x y. z = ⟨x, y⟩})" (is "M(?P)")
using relation_separation by simp
moreover from this assms
have "M({z∈?P . P(fst(z),snd(z))})"
by(rule_tac separation_closed,simp_all)
moreover
have "{y∈A . ∃ u v . y=⟨u,v⟩ ∧ P(u,v) } = {z∈?P . P(fst(z),snd(z))}"
by(rule equalityI subsetI,auto)
moreover from calculation
have "M({y∈A . ∃ u v . y=⟨u,v⟩ ∧ P(u,v) })"
by simp
ultimately
show "∃y[M]. ∀x[M]. x ∈ y ⟷ x ∈ A ∧ (∃w y. x = ⟨w, y⟩ ∧ P(w,y))"
by (rule_tac x="{z∈A. ∃x y. z = ⟨x, y⟩ ∧ P(x,y)}" in rexI) auto
qed
lemma lam_replacement_separation :
assumes "lam_replacement(M,f)" "separation(M,P)"
shows "strong_replacement(M, λx y . P(x) ∧ y=⟨x,f(x)⟩)"
using strong_replacement_separation_aux assms
unfolding lam_replacement_def
by simp
lemmas strong_replacement_separation =
strong_replacement_separation_aux[OF lam_replacement_imp_strong_replacement]
lemma id_closed: "M(A) ⟹ M(id(A))"
using lam_replacement_identity lam_replacement_iff_lam_closed
unfolding id_def by simp
lemma lam_replacement_Pair:
shows "lam_replacement(M, λx. ⟨fst(x), snd(x)⟩)"
using lam_replacement_product lam_replacement_fst lam_replacement_snd
by simp
lemma lam_replacement_Upair: "lam_replacement(M, λp. Upair(fst(p), snd(p)))"
proof -
have "(¬(∃a b . x = <a,b>)) ⟹ fst(x) = 0 ∧ snd(x) = 0" for x
unfolding fst_def snd_def
by (simp add:the_0)
then
have "Upair(fst(x),snd(x)) = (if (∃w . ∃ z . x=<w,z>) then (⋃x) else ({0}))" for x
using fst_conv snd_conv Upair_eq_cons
by (auto simp add:Pair_def)
moreover
have "lam_replacement(M, λx . (if (∃w . ∃ z . x=<w,z>) then (⋃x) else ({0})))"
using lam_replacement_Union lam_replacement_constant relation_separation lam_replacement_if
by simp
ultimately
show ?thesis
using lam_replacement_cong
by simp
qed
lemma lam_replacement_Un: "lam_replacement(M, λp. fst(p) ∪ snd(p))"
using lam_replacement_Upair lam_replacement_Union
lam_replacement_hcomp[where g=Union and f="λp. Upair(fst(p),snd(p))"]
unfolding Un_def by simp
lemma lam_replacement_cons: "lam_replacement(M, λp. cons(fst(p),snd(p)))"
using lam_replacement_Upair
lam_replacement_hcomp2[of _ _ "(∪)"]
lam_replacement_hcomp2[of fst fst "Upair"]
lam_replacement_Un lam_replacement_fst lam_replacement_snd
unfolding cons_def
by auto
lemma lam_replacement_sing_fun:
assumes "lam_replacement(M, f)" "∀x[M]. M(f(x))"
shows "lam_replacement(M, λx. {f(x)})"
using lam_replacement_constant lam_replacement_cons
lam_replacement_hcomp2[of "f" "λ_. 0" cons] assms
by auto
lemma lam_replacement_sing: "lam_replacement(M, λx. {x})"
using lam_replacement_sing_fun lam_replacement_identity
by simp
lemma lam_replacement_CartProd:
assumes "lam_replacement(M,f)" "lam_replacement(M,g)"
"∀x[M]. M(f(x))" "∀x[M]. M(g(x))"
shows "lam_replacement(M, λx. f(x) × g(x))"
proof -
note rep_closed = lam_replacement_imp_strong_replacement[THEN RepFun_closed]
{
fix A
assume "M(A)"
moreover
note transM[OF _ ‹M(A)›]
moreover from calculation assms
have "M({⟨x,⟨f(x),g(x)⟩⟩ . x∈A})" (is "M(?A')")
using lam_replacement_product[THEN lam_replacement_imp_lam_closed[unfolded lam_def]]
by simp
moreover from calculation
have "M(⋃{f(x) . x∈A})" (is "M(?F)")
using rep_closed[OF assms(1)] assms(3)
by simp
moreover from calculation
have "M(⋃{g(x) . x∈A})" (is "M(?G)")
using rep_closed[OF assms(2)] assms(4)
by simp
moreover from calculation
have "M(?A' × (?F × ?G))" (is "M(?T)")
by simp
moreover from this
have "M({t ∈ ?T . fst(snd(t)) ∈ fst(snd(fst(t))) ∧ snd(snd(t)) ∈ snd(snd(fst(t)))})" (is "M(?Q)")
using
lam_replacement_hcomp[OF lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_snd] _ ]
lam_replacement_hcomp lam_replacement_identity lam_replacement_fst lam_replacement_snd
separation_in separation_conj
by simp
moreover from this
have "M({⟨fst(fst(t)),snd(t)⟩ . t∈?Q})" (is "M(?R)")
using rep_closed lam_replacement_product
lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_fst] lam_replacement_snd
transM[of _ ?Q]
by simp
moreover from calculation
have "M({⟨x,?R``{x}⟩ . x∈A})"
using lam_replacement_imp_lam_closed[unfolded lam_def] lam_replacement_sing
lam_replacement_Image[THEN [5] lam_replacement_hcomp2] lam_replacement_constant[of ?R]
by simp
moreover
have "?R``{x} = f(x)×g(x)" if "x∈A" for x
by(rule equalityI subsetI,force,rule subsetI,rule_tac a="x" in imageI)
(auto simp:that,(rule_tac rev_bexI[of x],simp_all add:that)+)
ultimately
have "M({⟨x,f(x) × g(x)⟩ . x∈A})" by auto
}
with assms
show ?thesis using lam_replacement_iff_lam_closed[THEN iffD2,unfolded lam_def]
by simp
qed
lemma lam_replacement_RepFun :
assumes "lam_replacement(M,λx . f(fst(x),snd(x)))" "lam_replacement(M,g)"
"∀x[M].∀y∈g(x).M(f(x,y))" "∀x[M].M(g(x))"
shows "lam_replacement(M,λx . {f(x,z) . z∈g(x)})"
proof -
note rep_closed = lam_replacement_imp_strong_replacement[THEN RepFun_closed]
from assms
have "lam_replacement(M,λx.{x}×g(x))"
using lam_replacement_CartProd lam_replacement_sing
by auto
moreover from assms
have "M({f(x,z) . z ∈ g(x)})" if "M(x)" for x
using that transM[of _ "g(_)"] rep_closed
lam_replacement_product[OF lam_replacement_fst]
lam_replacement_snd lam_replacement_identity
assms(1)[THEN [5] lam_replacement_hcomp2] lam_replacement_constant[of x]
by simp
moreover
have "M(λz∈A.{f(z,u) . u ∈ g(z)})" if "M(A)" for A
proof -
from that assms calculation
have "M(⋃{{x}×g(x) . x∈A})" (is "M(?C)")
using rep_closed transM[of _ A]
by simp
with assms ‹M(A)›
have "M({⟨fst(x),f(fst(x),snd(x))⟩ . x ∈?C})" (is "M(?B)")
using singleton_closed transM[of _ A] transM[of _ "g(_)"] rep_closed
lam_replacement_product[OF lam_replacement_fst]
lam_replacement_hcomp[OF lam_replacement_snd]
by simp
with ‹M(A)›
have "M({⟨x,?B``{x}⟩ . x∈A})"
using transM[of _ A] rep_closed
lam_replacement_product[OF lam_replacement_identity]
lam_replacement_Image[THEN [5] lam_replacement_hcomp2]
lam_replacement_constant lam_replacement_sing
by simp
moreover
have "?B``{z} = {f(z,u) . u ∈ g(z)}" if "z∈A" for z
using that
by(intro equalityI subsetI,auto simp:imageI)
moreover from this
have "{⟨x,?B``{x}⟩ . x∈A} = {⟨z,{f(z,u) . u ∈ g(z)}⟩ . z∈A}"
by auto
ultimately
show ?thesis
unfolding lam_def by auto
qed
ultimately
show ?thesis
using lam_replacement_iff_lam_closed[THEN iffD2]
by simp
qed
lemma lam_replacement_Collect :
assumes "lam_replacement(M,f)" "∀x[M].M(f(x))"
"separation(M,λx . F(fst(x),snd(x)))"
shows "lam_replacement(M,λx. {y∈f(x) . F(x,y)})"
proof -
note rep_closed = lam_replacement_imp_strong_replacement[THEN RepFun_closed]
from assms
have 1:"lam_replacement(M,λx.{x}×f(x))"
using lam_replacement_CartProd lam_replacement_sing
by auto
have "M({u∈f(x) . F(x,u)})" if "M(x)" for x
proof -
from assms that
have "M({u ∈ {x}×f(x) . F(fst(u),snd(u))})" (is "M(?F)")
by simp
with assms that
have "M({snd(u) . u ∈ ?F})"
using rep_closed transM[of _ "f(x)"] lam_replacement_snd
by simp
moreover
have "{snd(u) . u ∈ ?F} = {u∈f(x) . F(x,u)}"
by auto
ultimately show ?thesis by simp
qed
moreover
have "M(λz∈A.{y ∈ f(z) . F(z,y)})" if "M(A)" for A
proof -
from 1 that assms
have "M(⋃{{x}×f(x) . x∈A})" (is "M(?C)")
using rep_closed transM[of _ A]
by simp
moreover from this assms
have "M({p ∈ ?C . F(fst(p),snd(p))})" (is "M(?B)")
by(rule_tac separation_closed,simp_all)
with ‹M(A)›
have "M({⟨x,?B``{x}⟩ . x∈A})"
using transM[of _ A] rep_closed
lam_replacement_product[OF lam_replacement_identity]
lam_replacement_Image[THEN [5] lam_replacement_hcomp2]
lam_replacement_constant lam_replacement_sing
by simp
moreover
have "?B``{z} = {u∈f(z) . F(z,u)}" if "z∈A" for z
using that
by(intro equalityI subsetI,auto simp:imageI)
moreover from this
have "{⟨x,?B``{x}⟩ . x∈A} = {⟨z,{u∈f(z) . F(z,u)}⟩ . z∈A}"
by auto
ultimately
show ?thesis
unfolding lam_def by auto
qed
ultimately
show ?thesis
using lam_replacement_iff_lam_closed[THEN iffD2]
by simp
qed
lemma separation_eq:
assumes "∀x[M]. M(f(x))" "lam_replacement(M,f)"
"∀x[M]. M(g(x))" "lam_replacement(M,g)"
shows "separation(M,λx . f(x) = g(x))"
proof -
let ?Z="λA. {⟨x,⟨f(x),⟨g(x),x⟩⟩⟩. x∈A}"
let ?Y="λA. {⟨⟨x,f(x)⟩,⟨g(x),x⟩⟩. x∈A}"
note sndsnd = lam_replacement_hcomp[OF lam_replacement_snd lam_replacement_snd]
note fstsnd = lam_replacement_hcomp[OF lam_replacement_snd lam_replacement_fst]
note sndfst = lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_snd]
have "M(?Z(A))" if "M(A)" for A
using assms lam_replacement_iff_lam_closed that
lam_replacement_product[OF assms(2)
lam_replacement_product[OF assms(4) lam_replacement_identity]]
unfolding lam_def
by auto
moreover
have "?Y(A) = {⟨⟨fst(x), fst(snd(x))⟩, fst(snd(snd(x))), snd(snd(snd(x)))⟩ . x ∈ ?Z(A)}" for A
by auto
moreover from calculation
have "M(?Y(A))" if "M(A)" for A
using
lam_replacement_imp_strong_replacement[OF
lam_replacement_product[OF
lam_replacement_product[OF lam_replacement_fst fstsnd]
lam_replacement_product[OF
lam_replacement_hcomp[OF sndsnd lam_replacement_fst]
lam_replacement_hcomp[OF lam_replacement_snd sndsnd]
]
], THEN RepFun_closed,simplified,of "?Z(A)"]
fst_closed[OF transM] snd_closed[OF transM] that
by auto
then
have "M({u∈?Y(A) . snd(fst(u)) = fst(snd(u))})" (is "M(?W(A))") if "M(A)" for A
using that middle_separation assms
by auto
then
have "M({fst(fst(u)) . u ∈ ?W(A)})" if "M(A)" for A
using that lam_replacement_imp_strong_replacement[OF
lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_fst], THEN RepFun_closed]
fst_closed[OF transM]
by auto
moreover
have "{x∈A. f(x) = g(x)} = {fst(fst(u)) . u∈?W(A)}" for A
by auto
ultimately
show ?thesis
using separation_iff by auto
qed
lemma separation_comp :
assumes "separation(M,P)" "lam_replacement(M,f)" "∀x[M]. M(f(x))"
shows "separation(M,λx. P(f(x)))"
unfolding separation_def
proof(clarify)
fix A
assume "M(A)"
let ?B="{f(a) . a ∈ A}"
let ?C="A×{b∈?B . P(b)}"
note ‹M(A)›
moreover from calculation
have "M(?C)"
using lam_replacement_imp_strong_replacement assms RepFun_closed transM[of _ A]
by simp
moreover from calculation
have "M({p∈?C . f(fst(p)) = snd(p)})" (is "M(?Prod)")
using assms separation_eq lam_replacement_fst lam_replacement_snd
lam_replacement_hcomp
by simp
moreover from calculation
have "M({fst(p) . p∈?Prod})" (is "M(?L)")
using lam_replacement_imp_strong_replacement lam_replacement_fst RepFun_closed
transM[of _ ?Prod]
by simp
moreover
have "?L = {z∈A . P(f(z))}"
by(intro equalityI subsetI,auto)
ultimately
show " ∃y[M]. ∀z[M]. z ∈ y ⟷ z ∈ A ∧ P(f(z))"
by (rule_tac x="?L" in rexI,simp_all)
qed
lemma lam_replacement_domain: "lam_replacement(M,domain)"
proof -
have 1:"{fst(z) . z∈ {u∈x . (∃ a b. u = <a,b>)}} =domain(x)" for x
unfolding domain_def
by (intro equalityI subsetI,auto,rule_tac x="<xa,y>" in bexI,auto)
moreover
have "lam_replacement(M,λ x .{fst(z) . z∈ {u∈x . (∃ a b. u = <a,b>)}})"
using lam_replacement_hcomp lam_replacement_snd lam_replacement_fst
snd_closed[OF transM] fst_closed[OF transM] lam_replacement_identity
relation_separation relation_separation[THEN separation_comp,where f=snd]
lam_replacement_Collect
by(rule_tac lam_replacement_RepFun,simp_all)
ultimately
show ?thesis
using lam_replacement_cong
by auto
qed
lemma separation_in_domain : "M(a) ⟹ separation(M, λx. a∈domain(x))"
using lam_replacement_domain lam_replacement_constant separation_in
by auto
lemma separation_all:
assumes "separation(M, λx . P(fst(fst(x)),snd(x)))"
"lam_replacement(M,f)" "lam_replacement(M,g)"
"∀x[M]. M(f(x))" "∀x[M]. M(g(x))"
shows "separation(M, λz. ∀x∈f(z). P(g(z),x))"
unfolding separation_def
proof(clarify)
note rep_closed = lam_replacement_imp_strong_replacement[THEN RepFun_closed]
note lr_fs = lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_snd]
fix A
assume "M(A)"
with assms
have "M({f(x) . x∈A})" (is "M(?F)") "M({<g(x),f(x)> . x∈A})" (is "M(?G)")
using rep_closed transM[of _ A]
lam_replacement_product lam_replacement_imp_lam_closed
unfolding lam_def
by auto
let ?B="⋃?F"
let ?C="?G×?B"
note ‹M(A)› ‹M(?F)› ‹M(?G)›
moreover from calculation
have "M(?C)"
by simp
moreover from calculation
have "M({p∈?C . P(fst(fst(p)),snd(p)) ∧ snd(p)∈snd(fst(p))})" (is "M(?Prod)")
using assms separation_conj separation_in lam_replacement_fst lam_replacement_snd
lam_replacement_hcomp
by simp
moreover from calculation
have "M({z∈?G . snd(z)=?Prod``{z}})" (is "M(?L)")
using separation_eq
lam_replacement_constant[of ?Prod] lam_replacement_constant[of 0]
lam_replacement_hcomp[OF _ lam_replacement_sing]
lam_replacement_Image[THEN [5] lam_replacement_hcomp2]
lam_replacement_identity lam_replacement_snd
by simp
moreover from calculation assms
have "M({x∈A . <g(x),f(x)> ∈ ?L})" (is "M(?N)")
using lam_replacement_product lam_replacement_constant
by (rule_tac separation_closed,rule_tac separation_in,auto)
moreover from calculation
have "?N = {z∈A . ∀x∈f(z). P(g(z),x)}"
proof -
have "P(g(z),x)" if "z∈A" "x∈f(z)" "f(z) = ?Prod``{<g(z),f(z)>}" for z x
using that
by(rule_tac imageE[of x ?Prod "{<g(z),f(z)>}"],simp_all)
moreover
have "f(z) = ?Prod `` {<g(z),f(z)>}" if "z∈A" "∀x∈f(z). P(g(z), x)" for z
using that
by force
ultimately
show ?thesis
by auto
qed
ultimately
show " ∃y[M]. ∀z[M]. z ∈ y ⟷ z ∈ A ∧ (∀x∈f(z) . P(g(z),x))"
by (rule_tac x="?N" in rexI,simp_all)
qed
lemma separation_ex:
assumes "separation(M, λx . P(fst(fst(x)),snd(x)))"
"lam_replacement(M,f)" "lam_replacement(M,g)"
"∀x[M]. M(f(x))" "∀x[M]. M(g(x))"
shows "separation(M, λz. ∃x∈f(z). P(g(z),x))"
unfolding separation_def
proof(clarify)
note rep_closed = lam_replacement_imp_strong_replacement[THEN RepFun_closed]
note lr_fs = lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_snd]
fix A
assume "M(A)"
with assms
have "M({f(x) . x∈A})" (is "M(?F)") "M({<g(x),f(x)> . x∈A})" (is "M(?G)")
using rep_closed transM[of _ A]
lam_replacement_product lam_replacement_imp_lam_closed
unfolding lam_def
by auto
let ?B="⋃?F"
let ?C="?G×?B"
note ‹M(A)› ‹M(?F)› ‹M(?G)›
moreover from calculation
have "M(?C)"
by simp
moreover from calculation
have "M({p∈?C . P(fst(fst(p)),snd(p)) ∧ snd(p)∈snd(fst(p))})" (is "M(?Prod)")
using assms separation_conj separation_in lam_replacement_fst lam_replacement_snd
lam_replacement_hcomp
by simp
moreover from calculation
have "M({z∈?G . 0≠?Prod``{z}})" (is "M(?L)")
using separation_eq separation_neg
lam_replacement_constant[of ?Prod] lam_replacement_constant[of 0]
lam_replacement_hcomp[OF _ lam_replacement_sing]
lam_replacement_Image[THEN [5] lam_replacement_hcomp2]
lam_replacement_identity
by simp
moreover from calculation assms
have "M({x∈A . <g(x),f(x)> ∈ ?L})" (is "M(?N)")
using lam_replacement_product lam_replacement_constant
by (rule_tac separation_closed,rule_tac separation_in,auto)
moreover from calculation
have "?N = {z∈A . ∃x∈f(z). P(g(z),x)}"
by(intro equalityI subsetI,simp_all,force) (rule ccontr,force)
ultimately
show " ∃y[M]. ∀z[M]. z ∈ y ⟷ z ∈ A ∧ (∃x∈f(z) . P(g(z),x))"
by (rule_tac x="?N" in rexI,simp_all)
qed
lemma lam_replacement_converse: "lam_replacement(M,converse)"
proof-
note lr_Un = lam_replacement_Union[THEN [2] lam_replacement_hcomp]
note lr_fs = lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_snd]
note lr_ff = lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_fst]
note lr_ss = lam_replacement_hcomp[OF lam_replacement_snd lam_replacement_snd]
note lr_sf = lam_replacement_hcomp[OF lr_ff lam_replacement_snd]
note lr_fff = lam_replacement_hcomp[OF lam_replacement_fst lr_ff]
note lr_f4 = lam_replacement_hcomp[OF lr_ff lr_ff]
have eq:"converse(x) = {⟨snd(y),fst(y)⟩ . y ∈ {z ∈ x. ∃ u ∈⋃⋃x . ∃v∈⋃⋃x . z=<u,v>}}" for x
unfolding converse_def
by(intro equalityI subsetI,auto,rename_tac a b,rule_tac x="<a,b>" in bexI,simp_all)
(auto simp : Pair_def)
have "M(x) ⟹ M({z ∈ x. ∃ u ∈⋃⋃x . ∃v∈⋃⋃x . z=<u,v>})" for x
using lam_replacement_identity lr_Un[OF lr_Un] lr_Un lr_Un[OF lam_replacement_Union]
lam_replacement_snd lr_ff lam_replacement_fst lam_replacement_hcomp lr_fff
lam_replacement_product[OF lr_sf lam_replacement_snd] lr_f4
lam_replacement_hcomp[OF lr_f4 lam_replacement_snd] separation_eq
lam_replacement_constant
by(rule_tac separation_closed,rule_tac separation_ex,rule_tac separation_ex,simp_all)
moreover
have sep:"separation(M, λx. ∃u∈⋃⋃fst(x). ∃v∈⋃⋃fst(x). snd(x) = ⟨u, v⟩)"
using lam_replacement_identity lr_Un[OF lr_Un] lr_Un
lam_replacement_snd lr_ff lam_replacement_fst lam_replacement_hcomp lr_fff
lam_replacement_product[OF lr_sf lam_replacement_snd]
lam_replacement_hcomp[OF lr_f4 lam_replacement_snd] separation_eq
by(rule_tac separation_ex,rule_tac separation_ex,simp_all)
moreover from calculation
have "lam_replacement(M, λx. {z ∈ x . ∃u∈⋃⋃x. ∃v∈⋃⋃x. z = ⟨u, v⟩})"
using lam_replacement_identity
by(rule_tac lam_replacement_Collect,simp_all)
ultimately
have 1:"lam_replacement(M, λx . {⟨snd(y),fst(y)⟩ . y ∈ {z ∈ x. ∃u ∈⋃⋃x . ∃v∈⋃⋃x. z=<u,v>}})"
using lam_replacement_product lam_replacement_fst lam_replacement_hcomp
lam_replacement_identity lr_ff lr_ss
lam_replacement_snd lam_replacement_identity sep
by(rule_tac lam_replacement_RepFun,simp_all,force dest:transM)
with eq[symmetric]
show ?thesis
by(rule_tac lam_replacement_cong[OF 1],simp_all)
qed
lemma lam_replacement_Diff: "lam_replacement(M, λx . fst(x) - snd(x))"
proof -
have eq:"X - Y = {x∈X . x∉Y}" for X Y
by auto
moreover
have "lam_replacement(M, λx . {y ∈ fst(x) . y∉snd(x)})"
using lam_replacement_fst lam_replacement_hcomp
lam_replacement_snd lam_replacement_identity separation_in separation_neg
by(rule_tac lam_replacement_Collect,simp_all)
then
show ?thesis
by(rule_tac lam_replacement_cong,auto,subst eq[symmetric],simp)
qed
lemma lam_replacement_range : "lam_replacement(M,range)"
unfolding range_def
using lam_replacement_hcomp[OF lam_replacement_converse lam_replacement_domain]
by auto
lemma separation_in_range : "M(a) ⟹ separation(M, λx. a∈range(x))"
using lam_replacement_range lam_replacement_constant separation_in
by auto
lemmas tag_replacement = lam_replacement_constant[unfolded lam_replacement_def]
lemma tag_lam_replacement : "M(X) ⟹ lam_replacement(M,λx. <X,x>)"
using lam_replacement_product[OF lam_replacement_constant] lam_replacement_identity
by simp
lemma strong_lam_replacement_imp_lam_replacement_RepFun :
assumes "strong_replacement(M,λ x z . P(fst(x),snd(x)) ∧ z=⟨x,f(fst(x),snd(x))⟩)"
"lam_replacement(M,g)"
"⋀A y . M(y) ⟹ M(A) ⟹ ∀x∈A. P(y,x) ⟶ M(f(y,x))"
"∀x[M]. M(g(x))"
"separation(M, λx. P(fst(x),snd(x)))"
shows "lam_replacement(M, λx. {y . r∈ g(x) , P(x,r) ∧ y=f(x,r)}) "
proof -
note rep_closed = lam_replacement_imp_strong_replacement[THEN RepFun_closed]
moreover
have "{f(x, xa) . xa ∈ {xa ∈ g(x) . P(x, xa)}} = {y . z ∈ g(x), P(x, z) ∧ y = f(x, z)}" for x
by(intro equalityI subsetI,auto)
moreover from assms
have 0:"M({xa ∈ g(x) . P(x, xa)})" if "M(x)" for x
using that separation_closed assms(5)[THEN separation_comp,OF tag_lam_replacement]
by simp
moreover from assms
have 1:"lam_replacement(M,λx.{x}×{u∈g(x) . P(x,u)})" (is "lam_replacement(M,λx.?R(x))")
using separation_closed assms(5)[THEN separation_comp,OF tag_lam_replacement]
by(rule_tac lam_replacement_CartProd[OF lam_replacement_sing lam_replacement_Collect],simp_all)
moreover from assms
have "M({y . z∈g(x) , P(x,z) ∧ y=f(x,z)})" (is "M(?Q(x))") if "M(x)" for x
using that transM[of _ "g(_)"]
separation_closed assms(5)[THEN separation_comp,OF tag_lam_replacement]
assms(3)[of "x" "g(x)"] strong_lam_replacement_imp_strong_replacement
by simp
moreover
have "M(λz∈A.{f(z,r) . r ∈ {u∈ g(z) . P(z,u)}})" if "M(A)" for A
proof -
from that assms calculation
have "M(⋃{?R(x) . x∈A})" (is "M(?C)")
using transM[of _ A] rep_closed
by simp
moreover from assms ‹M(A)›
have "x ∈ {y} × {x ∈ g(y) . P(y, x)} ⟹ M(x) ∧ M(f(fst(x),snd(x)))" if "y∈A" for y x
using assms(3)[of "y" "g(y)"] transM[of _ A] transM[of _ "g(y)"] that
by force
moreover from this
have "∃y∈A . x ∈ {y} × {x ∈ g(y) . P(y, x)} ⟹ M(x) ∧ M(f(fst(x),snd(x)))" for x
by auto
moreover note assms ‹M(A)›
ultimately
have "M({z . x∈?C , P(fst(x),snd(x)) ∧ z = ⟨x,f(fst(x),snd(x))⟩})" (is "M(?B)")
using singleton_closed transM[of _ A] transM[of _ "g(_)"] rep_closed
lam_replacement_product[OF lam_replacement_fst]
lam_replacement_hcomp[OF lam_replacement_snd] transM[OF _ 0]
by(rule_tac strong_replacement_closed,simp_all)
then</