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
have "M({⟨fst(fst(x)),snd(x)⟩ . x∈?B})" (is "M(?D)")
using rep_closed transM[of _ ?B]
lam_replacement_product[OF
lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_fst]
lam_replacement_snd]
by simp
with ‹M(A)›
have "M({⟨x,?D``{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 from calculation
have "?D``{z} = {f(z,r) . r ∈ {u∈ g(z) . P(z,u)}}" if "z∈A" for z
using that
by (intro equalityI subsetI,auto,intro imageI,force,auto)
moreover from this
have "{⟨x,?D``{x}⟩ . x∈A} = {⟨z,{f(z,r) . r ∈ {u∈ g(z) . P(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 lam_replacement_Collect' :
assumes "M(A)" "separation(M,λp . F(fst(p),snd(p)))"
shows "lam_replacement(M,λx. {y∈A . F(x,y)})"
using assms lam_replacement_constant
by(rule_tac lam_replacement_Collect, simp_all)
lemma lam_replacement_id2: "lam_replacement(M, λx. ⟨x, x⟩)"
using lam_replacement_identity lam_replacement_product[of "λx. x" "λx. x"]
by simp
lemmas id_replacement = lam_replacement_id2[unfolded lam_replacement_def]
lemma lam_replacement_apply2:"lam_replacement(M, λp. fst(p) ` snd(p))"
using lam_replacement_fst lam_replacement_sing_fun[OF lam_replacement_snd]
lam_replacement_Image lam_replacement_Union
lam_replacement_hcomp[of _ Union] lam_replacement_hcomp2[of _ _ "(``)"]
unfolding apply_def
by simp
lemma lam_replacement_apply:"M(S) ⟹ lam_replacement(M, λx. S ` x)"
using lam_replacement_constant[of S] lam_replacement_identity
lam_replacement_apply2[THEN [5] lam_replacement_hcomp2]
by simp
lemma apply_replacement:"M(S) ⟹ strong_replacement(M, λx y. y = S ` x)"
using lam_replacement_apply lam_replacement_imp_strong_replacement by simp
lemma lam_replacement_id_const: "M(b) ⟹ lam_replacement(M, λx. ⟨x, b⟩)"
using lam_replacement_identity lam_replacement_constant
lam_replacement_product[of "λx. x" "λx. b"] by simp
lemmas pospend_replacement = lam_replacement_id_const[unfolded lam_replacement_def]
lemma lam_replacement_const_id: "M(b) ⟹ lam_replacement(M, λz. ⟨b, z⟩)"
using lam_replacement_identity lam_replacement_constant
lam_replacement_product[of "λx. b" "λx. x"] by simp
lemmas prepend_replacement = lam_replacement_const_id[unfolded lam_replacement_def]
lemma lam_replacement_apply_const_id: "M(f) ⟹ M(z) ⟹
lam_replacement(M, λx. f ` ⟨z, x⟩)"
using lam_replacement_const_id[of z] lam_replacement_apply
lam_replacement_hcomp[of "λx. ⟨z, x⟩"] by simp
lemmas apply_replacement2 = lam_replacement_apply_const_id[unfolded lam_replacement_def]
lemma lam_replacement_Inl: "lam_replacement(M, Inl)"
using lam_replacement_identity lam_replacement_constant
lam_replacement_product[of "λx. 0" "λx. x"]
unfolding Inl_def by simp
lemma lam_replacement_Inr: "lam_replacement(M, Inr)"
using lam_replacement_identity lam_replacement_constant
lam_replacement_product[of "λx. 1" "λx. x"]
unfolding Inr_def by simp
lemmas Inl_replacement1 = lam_replacement_Inl[unfolded lam_replacement_def]
lemma lam_replacement_Diff': "M(X) ⟹ lam_replacement(M, λx. x - X)"
using lam_replacement_Diff[THEN [5] lam_replacement_hcomp2]
lam_replacement_constant lam_replacement_identity
by simp
lemmas Pair_diff_replacement = lam_replacement_Diff'[unfolded lam_replacement_def]
lemma diff_Pair_replacement: "M(p) ⟹ strong_replacement(M, λx y . y=⟨x,x-{p}⟩)"
using Pair_diff_replacement by simp
lemma swap_replacement:"strong_replacement(M, λx y. y = ⟨x, (λ⟨x,y⟩. ⟨y, x⟩)(x)⟩)"
using lam_replacement_swap unfolding lam_replacement_def split_def by simp
lemma lam_replacement_Un_const:"M(b) ⟹ lam_replacement(M, λx. x ∪ b)"
using lam_replacement_Un lam_replacement_hcomp2[of _ _ "(∪)"]
lam_replacement_constant[of b] lam_replacement_identity by simp
lemmas tag_union_replacement = lam_replacement_Un_const[unfolded lam_replacement_def]
lemma lam_replacement_csquare: "lam_replacement(M,λp. ⟨fst(p) ∪ snd(p), fst(p), snd(p)⟩)"
using lam_replacement_Un lam_replacement_fst lam_replacement_snd
by (fast intro: lam_replacement_product lam_replacement_hcomp2)
lemma csquare_lam_replacement:"strong_replacement(M, λx y. y = ⟨x, (λ⟨x,y⟩. ⟨x ∪ y, x, y⟩)(x)⟩)"
using lam_replacement_csquare unfolding split_def lam_replacement_def .
lemma lam_replacement_assoc:"lam_replacement(M,λx. ⟨fst(fst(x)), snd(fst(x)), snd(x)⟩)"
using lam_replacement_fst lam_replacement_snd
by (force intro: lam_replacement_product lam_replacement_hcomp)
lemma assoc_replacement:"strong_replacement(M, λx y. y = ⟨x, (λ⟨⟨x,y⟩,z⟩. ⟨x, y, z⟩)(x)⟩)"
using lam_replacement_assoc unfolding split_def lam_replacement_def .
lemma lam_replacement_prod_fun: "M(f) ⟹ M(g) ⟹ lam_replacement(M,λx. ⟨f ` fst(x), g ` snd(x)⟩)"
using lam_replacement_fst lam_replacement_snd
by (force intro: lam_replacement_product lam_replacement_hcomp lam_replacement_apply)
lemma prod_fun_replacement:"M(f) ⟹ M(g) ⟹
strong_replacement(M, λx y. y = ⟨x, (λ⟨w,y⟩. ⟨f ` w, g ` y⟩)(x)⟩)"
using lam_replacement_prod_fun unfolding split_def lam_replacement_def .
lemma separation_subset:
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 -
have "f(x) ⊆ g(x) ⟷ f(x)∪g(x) = g(x)" for x
using subset_Un_iff by simp
moreover from assms
have "separation(M,λx . f(x)∪g(x) = g(x))"
using separation_eq lam_replacement_Un lam_replacement_hcomp2
by simp
ultimately
show ?thesis
using separation_cong[THEN iffD1] by auto
qed
lemma lam_replacement_twist: "lam_replacement(M,λ⟨⟨x,y⟩,z⟩. ⟨x,y,z⟩)"
using lam_replacement_fst lam_replacement_snd
lam_replacement_Pair[THEN [5] lam_replacement_hcomp2,
of "λx. snd(fst(x))" "λx. snd(x)", THEN [2] lam_replacement_Pair[
THEN [5] lam_replacement_hcomp2, of "λx. fst(fst(x))"]]
lam_replacement_hcomp unfolding split_def by simp
lemma twist_closed[intro,simp]: "M(x) ⟹ M((λ⟨⟨x,y⟩,z⟩. ⟨x,y,z⟩)(x))"
unfolding split_def by simp
lemma lam_replacement_vimage :
shows "lam_replacement(M, λx. fst(x)-``snd(x))"
unfolding vimage_def using
lam_replacement_Image[THEN [5] lam_replacement_hcomp2]
lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_converse] lam_replacement_snd
by simp
lemma lam_replacement_vimage_sing: "lam_replacement(M, λp. fst(p) -`` {snd(p)})"
using lam_replacement_snd lam_replacement_sing_fun
lam_replacement_vimage[THEN [5] lam_replacement_hcomp2] lam_replacement_fst
by simp
lemma lam_replacement_vimage_sing_fun: "M(f) ⟹ lam_replacement(M, λx. f -`` {x})"
using lam_replacement_vimage_sing[THEN [5] lam_replacement_hcomp2] lam_replacement_constant[of f]
lam_replacement_identity
by simp
lemma lam_replacement_image_sing_fun: "M(f) ⟹ lam_replacement(M, λx. f `` {x})"
using lam_replacement_Image[THEN [5] lam_replacement_hcomp2] lam_replacement_constant[of f]
lam_replacement_sing
by simp
lemma converse_apply_projs: "∀x[M]. ⋃ (fst(x) -`` {snd(x)}) = converse(fst(x)) ` (snd(x))"
using converse_apply_eq by auto
lemma lam_replacement_converse_app: "lam_replacement(M, λp. converse(fst(p)) ` snd(p))"
using lam_replacement_cong[OF _ converse_apply_projs]
lam_replacement_hcomp[OF lam_replacement_vimage_sing lam_replacement_Union]
by simp
lemmas cardinal_lib_assms4 = lam_replacement_vimage_sing_fun[unfolded lam_replacement_def]
lemma lam_replacement_sing_const_id:
"M(x) ⟹ lam_replacement(M, λy. {⟨x, y⟩})"
using lam_replacement_const_id[of x] lam_replacement_sing_fun
by simp
lemma tag_singleton_closed: "M(x) ⟹ M(z) ⟹ M({{⟨z, y⟩} . y ∈ x})"
using RepFun_closed lam_replacement_imp_strong_replacement lam_replacement_sing_const_id
transM[of _ x]
by simp
lemma separation_ball:
assumes "separation(M, λy. f(fst(y),snd(y)))" "M(X)"
shows "separation(M, λy. ∀u∈X. f(y,u))"
unfolding separation_def
proof(clarify)
fix A
assume "M(A)"
moreover
note ‹M(X)›
moreover from calculation
have "M(A×X)"
by simp
then
have "M({p ∈ A×X . f(fst(p),snd(p))})" (is "M(?P)")
using assms(1)
by auto
moreover from calculation
have "M({a∈A . ?P``{a} = X})" (is "M(?A')")
using separation_eq lam_replacement_image_sing_fun[of "?P"] lam_replacement_constant
by simp
moreover
have "f(a,x)" if "a∈?A'" and "x∈X" for a x
proof -
from that
have "a∈A" "?P``{a}=X"
by auto
then
have "x∈?P``{a}"
using that by simp
then
show ?thesis using image_singleton_iff by simp
qed
moreover from this
have "∀a[M]. a ∈ ?A' ⟷ a ∈ A ∧ (∀x∈X. f(a, x))"
using image_singleton_iff
by auto
with ‹M(?A')›
show "∃y[M]. ∀a[M]. a ∈ y ⟷ a ∈ A ∧ (∀x∈X. f(a, x))"
by (rule_tac x="?A'" in rexI,simp_all)
qed
lemma separation_bex:
assumes "separation(M, λy. f(fst(y),snd(y)))" "M(X)"
shows "separation(M, λy. ∃u∈X. f(y,u))"
unfolding separation_def
proof(clarify)
fix A
assume "M(A)"
moreover
note ‹M(X)›
moreover from calculation
have "M(A×X)"
by simp
then
have "M({p ∈ A×X . f(fst(p),snd(p))})" (is "M(?P)")
using assms(1)
by auto
moreover from calculation
have "M({a∈A . ?P``{a} ≠ 0})" (is "M(?A')")
using separation_eq lam_replacement_image_sing_fun[of "?P"] lam_replacement_constant
separation_neg
by simp
moreover from this
have "∀a[M]. a ∈ ?A' ⟷ a ∈ A ∧ (∃x∈X. f(a, x))"
using image_singleton_iff
by auto
with ‹M(?A')›
show "∃y[M]. ∀a[M]. a ∈ y ⟷ a ∈ A ∧ (∃x∈X. f(a, x))"
by (rule_tac x="?A'" in rexI,simp_all)
qed
lemma lam_replacement_Lambda:
assumes "lam_replacement(M, λy. b(fst(y), snd(y)))"
"∀w[M]. ∀y[M]. M(b(w, y))" "M(W)"
shows "lam_replacement(M, λx. λw∈W. b(x, w))"
using assms lam_replacement_constant lam_replacement_product lam_replacement_snd
lam_replacement_RepFun transM[of _ W]
unfolding lam_def
by simp
lemma lam_replacement_apply_Pair:
assumes "M(y)"
shows "lam_replacement(M, λx. y ` ⟨fst(x), snd(x)⟩)"
using assms lam_replacement_constant lam_replacement_Pair
lam_replacement_apply2[THEN [5] lam_replacement_hcomp2]
by auto
lemma lam_replacement_apply_fst_snd:
shows "lam_replacement(M, λw. fst(w) ` fst(snd(w)) ` snd(snd(w)))"
using lam_replacement_fst lam_replacement_snd lam_replacement_hcomp
lam_replacement_apply2[THEN [5] lam_replacement_hcomp2]
by auto
lemma lam_replacement_RepFun_apply :
assumes "M(f)"
shows "lam_replacement(M, λx . {f`y . y ∈ x})"
using assms lam_replacement_identity lam_replacement_RepFun
lam_replacement_hcomp lam_replacement_snd lam_replacement_apply
by(rule_tac lam_replacement_RepFun,auto dest:transM)
lemma separation_snd_in_fst: "separation(M, λx. snd(x) ∈ fst(x))"
using separation_in lam_replacement_fst lam_replacement_snd
by auto
lemma lam_replacement_if_mem:
"lam_replacement(M, λx. if snd(x) ∈ fst(x) then 1 else 0)"
using separation_snd_in_fst
lam_replacement_constant lam_replacement_if
by auto
lemma lam_replacement_Lambda_apply_fst_snd:
assumes "M(X)"
shows "lam_replacement(M, λx. λw∈X. x ` fst(w) ` snd(w))"
using assms lam_replacement_apply_fst_snd lam_replacement_Lambda
by simp
lemma lam_replacement_Lambda_apply_Pair:
assumes "M(X)" "M(y)"
shows "lam_replacement(M, λx. λw∈X. y ` ⟨x, w⟩)"
using assms lam_replacement_apply_Pair lam_replacement_Lambda
by simp
lemma lam_replacement_Lambda_if_mem:
assumes "M(X)"
shows "lam_replacement(M, λx. λxa∈X. if xa ∈ x then 1 else 0)"
using assms lam_replacement_if_mem lam_replacement_Lambda
by simp
lemma case_closed :
assumes "∀x[M]. M(f(x))" "∀x[M]. M(g(x))"
shows "∀x[M]. M(case(f,g,x))"
unfolding case_def split_def cond_def
using assms by simp
lemma separation_fst_equal : "M(a) ⟹ separation(M,λx . fst(x)=a)"
using separation_eq lam_replacement_fst lam_replacement_constant
by auto
lemma lam_replacement_case :
assumes "lam_replacement(M,f)" "lam_replacement(M,g)"
"∀x[M]. M(f(x))" "∀x[M]. M(g(x))"
shows "lam_replacement(M, λx . case(f,g,x))"
unfolding case_def split_def cond_def
using lam_replacement_if separation_fst_equal
lam_replacement_hcomp[of "snd" g]
lam_replacement_hcomp[of "snd" f]
lam_replacement_snd assms
by simp
lemma Pi_replacement1: "M(x) ⟹ M(y) ⟹ strong_replacement(M, λya z. ya ∈ y ∧ z = {⟨x, ya⟩})"
using lam_replacement_imp_strong_replacement
strong_replacement_separation[OF lam_replacement_sing_const_id[of x],where P="λx . x ∈y"]
separation_in_constant
by simp
lemma surj_imp_inj_replacement1:
"M(f) ⟹ M(x) ⟹ strong_replacement(M, λy z. y ∈ f -`` {x} ∧ z = {⟨x, y⟩})"
using Pi_replacement1 vimage_closed singleton_closed
by simp
lemmas domain_replacement = lam_replacement_domain[unfolded lam_replacement_def]
lemma domain_replacement_simp: "strong_replacement(M, λx y. y=domain(x))"
using lam_replacement_domain lam_replacement_imp_strong_replacement by simp
lemma un_Pair_replacement: "M(p) ⟹ strong_replacement(M, λx y . y = x∪{p})"
using lam_replacement_Un_const[THEN lam_replacement_imp_strong_replacement] by simp
lemma diff_replacement: "M(X) ⟹ strong_replacement(M, λx y. y = x - X)"
using lam_replacement_Diff'[THEN lam_replacement_imp_strong_replacement] by simp
lemma lam_replacement_succ:
"lam_replacement(M,λz . succ(z))"
unfolding succ_def
using lam_replacement_hcomp2[of "λx. x" "λx. x" cons]
lam_replacement_cons lam_replacement_identity
by simp
lemma lam_replacement_hcomp_Least:
assumes "lam_replacement(M, g)" "lam_replacement(M,λx. μ i. x∈F(i,x))"
"∀x[M]. M(g(x))" "⋀x i. M(x) ⟹ i ∈ F(i, x) ⟹ M(i)"
shows "lam_replacement(M,λx. μ i. g(x)∈F(i,g(x)))"
using assms
by (rule_tac lam_replacement_hcomp[of _ "λx. μ i. x∈F(i,x)"])
(auto intro:Least_closed')
lemma domain_mem_separation: "M(A) ⟹ separation(M, λx . domain(x)∈A)"
using separation_in lam_replacement_constant lam_replacement_domain
by auto
lemma domain_eq_separation: "M(p) ⟹ separation(M, λx . domain(x) = p)"
using separation_eq lam_replacement_domain lam_replacement_constant
by auto
lemma lam_replacement_Int:
shows "lam_replacement(M, λx. fst(x) ∩ snd(x))"
proof -
have "A∩B = (A∪B) - ((A- B) ∪ (B-A))" (is "_=?f(A,B)")for A B
by auto
then
show ?thesis
using lam_replacement_cong
lam_replacement_Diff[THEN[5] lam_replacement_hcomp2]
lam_replacement_Un[THEN[5] lam_replacement_hcomp2]
lam_replacement_fst lam_replacement_snd
by simp
qed
lemma restrict_eq_separation': "M(B) ⟹ ∀A[M]. separation(M, λy. ∃x[M]. x∈A ∧ y = ⟨x, restrict(x, B)⟩)"
proof(clarify)
fix A
have "restrict(r,B) = r ∩ (B × range(r))" for r
unfolding restrict_def by(rule equalityI subsetI,auto)
moreover
assume "M(A)" "M(B)"
moreover from this
have "separation(M, λy. ∃x∈A. y = ⟨x, x ∩ (B × range(x))⟩)"
using lam_replacement_Int[THEN[5] lam_replacement_hcomp2]
lam_replacement_Pair[THEN[5] lam_replacement_hcomp2]
using lam_replacement_fst lam_replacement_snd lam_replacement_constant
lam_replacement_hcomp lam_replacement_range lam_replacement_identity
lam_replacement_CartProd separation_bex separation_eq
by simp_all
ultimately
show "separation(M, λy. ∃x[M]. x∈A ∧ y = ⟨x, restrict(x, B)⟩)"
by simp
qed
lemmas lam_replacement_restrict' = lam_replacement_restrict[OF restrict_eq_separation']
lemma restrict_strong_replacement: "M(A) ⟹ strong_replacement(M, λx y. y=restrict(x,A))"
using lam_replacement_restrict restrict_eq_separation'
lam_replacement_imp_strong_replacement
by simp
lemma restrict_eq_separation: "M(r) ⟹ M(p) ⟹ separation(M, λx . restrict(x,r) = p)"
using separation_eq lam_replacement_restrict' lam_replacement_constant
by auto
lemma separation_equal_fst2 : "M(a) ⟹ separation(M,λx . fst(fst(x))=a)"
using separation_eq lam_replacement_hcomp lam_replacement_fst lam_replacement_constant
by auto
lemma separation_equal_apply: "M(f) ⟹ M(a) ⟹ separation(M,λx. f`x=a)"
using separation_eq lam_replacement_apply[of f] lam_replacement_constant
by auto
lemma lam_apply_replacement: "M(A) ⟹ M(f) ⟹ lam_replacement(M, λx . λn∈A. f ` ⟨x, n⟩)"
using lam_replacement_Lambda lam_replacement_hcomp[OF _ lam_replacement_apply[of f]] lam_replacement_Pair
by simp
lemma lam_replacement_comp :
"lam_replacement(M, λx . fst(x) O snd(x))"
proof -
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 lam_replacement_snd lam_replacement_fst]
note lr_fff = lam_replacement_hcomp[OF lam_replacement_fst lr_ff]
have eq:"R O S =
{xz ∈ domain(S) × range(R) .
∃y∈range(S)∩domain(R) . ⟨fst(xz),y⟩∈S ∧ ⟨y,snd(xz)⟩∈R}" for R S
unfolding comp_def
by(intro equalityI subsetI,auto)
moreover
have "lam_replacement(M, λx . {xz ∈ domain(snd(x)) × range(fst(x)) .
∃y∈range(snd(x))∩domain(fst(x)) . ⟨fst(xz),y⟩∈snd(x) ∧ ⟨y,snd(xz)⟩∈fst(x)})"
using lam_replacement_CartProd lam_replacement_hcomp
lam_replacement_range lam_replacement_domain lam_replacement_fst lam_replacement_snd
lam_replacement_identity lr_fs lr_ff lr_ss lam_replacement_product
lam_replacement_Int[THEN [5] lam_replacement_hcomp2]
lam_replacement_hcomp[OF lr_ff lam_replacement_domain]
lam_replacement_hcomp[OF lr_fs lam_replacement_range]
lam_replacement_hcomp[OF lr_ff lr_ff]
lam_replacement_hcomp[OF lr_ff lr_ss]
lam_replacement_hcomp[OF lr_ff lr_sf]
lr_fff
lam_replacement_hcomp[OF lr_fff lam_replacement_snd ]
separation_ex separation_conj separation_in
by(rule_tac lam_replacement_Collect,simp_all,rule_tac separation_ex,rule_tac separation_conj,auto)
ultimately
show ?thesis
by(rule_tac lam_replacement_cong,auto,subst eq[symmetric],rule_tac comp_closed,auto)
qed
lemma lam_replacement_comp':
"M(f) ⟹ M(g) ⟹ lam_replacement(M, λx . f O x O g)"
using lam_replacement_comp[THEN [5] lam_replacement_hcomp2,
OF lam_replacement_constant lam_replacement_comp,
THEN [5] lam_replacement_hcomp2] lam_replacement_constant
lam_replacement_identity by simp
lemma RepFun_SigFun_closed: "M(x)⟹ M(z) ⟹ M({{⟨z, u⟩} . u ∈ x})"
using lam_replacement_sing_const_id lam_replacement_imp_strong_replacement RepFun_closed
transM[of _ x] singleton_in_M_iff pair_in_M_iff
by simp
lemma separation_orthogonal: "M(x) ⟹ M(Q) ⟹ separation(M, λa . ∀s∈x. ⟨s, a⟩ ∈ Q)"
using separation_in[OF _
lam_replacement_hcomp2[OF _ _ _ _ lam_replacement_Pair] _
lam_replacement_constant]
separation_ball lam_replacement_hcomp lam_replacement_fst lam_replacement_snd
by simp_all
lemma separation_Transset: "separation(M,Transset)"
unfolding Transset_def
using separation_subset lam_replacement_fst lam_replacement_snd
lam_replacement_hcomp lam_replacement_identity
by(rule_tac separation_all,auto)
lemma separation_Ord: "separation(M,Ord)"
unfolding Ord_def
using separation_Transset
separation_comp separation_Transset lam_replacement_snd lam_replacement_identity
by(rule_tac separation_conj,auto,rule_tac separation_all,auto)
lemma ord_iso_separation: "M(A) ⟹ M(r) ⟹ M(s) ⟹
separation(M, λf. ∀x∈A. ∀y∈A. ⟨x, y⟩ ∈ r ⟷ ⟨f ` x, f ` y⟩ ∈ s)"
using
lam_replacement_Pair[THEN[5] lam_replacement_hcomp2]
lam_replacement_apply2[THEN[5] lam_replacement_hcomp2]
lam_replacement_hcomp lam_replacement_fst lam_replacement_snd
lam_replacement_identity lam_replacement_constant
separation_in separation_ball[of _ A] separation_iff'
by simp
lemma separation_dist: "separation(M, λ x . ∃a. ∃b . x=⟨a,b⟩ ∧ a≠b)"
using separation_Pair separation_neg separation_eq lam_replacement_fst lam_replacement_snd
by simp
lemma separation_imp_lam_closed:
assumes "∀x∈A. F(x) ∈ B" "separation(M, λ⟨x,y⟩. F(x) = y)"
"M(A)" "M(B)"
shows "M(λx∈A. F(x))"
proof -
from ‹∀x∈A. F(x) ∈ B›
have "(λx∈A. F(x)) ⊆ A×B"
using times_subset_iff fun_is_rel[OF lam_funtype, of A F]
by auto
moreover from this
have "(λx∈A. F(x)) = {⟨x,y⟩ ∈ A × B. F(x) = y}"
unfolding lam_def by force
moreover
note ‹M(A)› ‹M(B)› ‹separation(M, λ⟨x,y⟩. F(x) = y)›
moreover from this
have "M({⟨x,y⟩ ∈ A × B. F(x) = y})"
by simp
ultimately
show ?thesis
unfolding lam_def
by auto
qed
lemma curry_closed :
assumes "M(f)" "M(A)" "M(B)"
shows "M(curry(A,B,f))"
using assms lam_replacement_apply_const_id
lam_apply_replacement lam_replacement_iff_lam_closed
unfolding curry_def
by auto
end
definition
RepFun_cons :: "i⇒i⇒i" where
"RepFun_cons(x,y) ≡ RepFun(x, λz. {⟨y,z⟩})"
context M_replacement
begin
lemma lam_replacement_RepFun_cons'':
shows "lam_replacement(M, λx . RepFun_cons(fst(x),snd(x)))"
unfolding RepFun_cons_def
using lam_replacement_fst fst_closed snd_closed lam_replacement_product
lam_replacement_snd lam_replacement_hcomp lam_replacement_sing_fun
transM[OF _ fst_closed]
lam_replacement_RepFun[of "λ x z . {<snd(x),z>}" "fst"]
by simp
lemma RepFun_cons_replacement: "lam_replacement(M, λp. RepFun(fst(p), λx. {⟨snd(p),x⟩}))"
using lam_replacement_RepFun_cons''
unfolding RepFun_cons_def
by simp
lemma lam_replacement_Sigfun:
assumes "lam_replacement(M,f)" "∀y[M]. M(f(y))"
shows "lam_replacement(M, λx. Sigfun(x,f))"
using assms lam_replacement_Union lam_replacement_sing_fun lam_replacement_Pair
tag_singleton_closed transM[of _ "f(_)"] lam_replacement_hcomp[of _ Union]
lam_replacement_RepFun
unfolding Sigfun_def
by simp
lemma phrank_repl:
assumes
"M(f)"
shows
"strong_replacement(M, λx y. y = succ(f`x))"
using assms lam_replacement_succ lam_replacement_apply
lam_replacement_imp_strong_replacement lam_replacement_hcomp
by auto
lemma lam_replacement_Powapply_rel:
assumes "∀A[M]. separation(M, λy. ∃x[M]. x ∈ A ∧ y = ⟨x, Pow_rel(M,x)⟩)"
"M(f)"
shows
"lam_replacement(M, Powapply_rel(M,f))"
using assms lam_replacement_Pow_rel lam_replacement_apply[THEN lam_replacement_hcomp]
unfolding Powapply_rel_def
by auto
lemmas Powapply_rel_replacement = lam_replacement_Powapply_rel[THEN
lam_replacement_imp_strong_replacement]
lemma surj_imp_inj_replacement2:
"M(f) ⟹ strong_replacement(M, λx z. z = Sigfun(x, λy. f -`` {y}))"
using lam_replacement_imp_strong_replacement lam_replacement_Sigfun
lam_replacement_vimage_sing_fun
by simp
lemma lam_replacement_Pi: "M(y) ⟹ lam_replacement(M, λx. ⋃xa∈y. {⟨x, xa⟩})"
using lam_replacement_constant lam_replacement_Sigfun[unfolded Sigfun_def,of "λx. y"]
by (simp)
lemma Pi_replacement2: "M(y) ⟹ strong_replacement(M, λx z. z = (⋃xa∈y. {⟨x, xa⟩}))"
using lam_replacement_Pi[THEN lam_replacement_imp_strong_replacement, of y]
by simp
lemma if_then_Inj_replacement:
shows "M(A) ⟹ strong_replacement(M, λx y. y = ⟨x, if x ∈ A then Inl(x) else Inr(x)⟩)"
using lam_replacement_if lam_replacement_Inl lam_replacement_Inr separation_in_constant
unfolding lam_replacement_def
by simp
lemma lam_if_then_replacement:
"M(b) ⟹
M(a) ⟹ M(f) ⟹ strong_replacement(M, λy ya. ya = ⟨y, if y = a then b else f ` y⟩)"
using lam_replacement_if lam_replacement_apply lam_replacement_constant
separation_equal
unfolding lam_replacement_def
by simp
lemma if_then_replacement:
"M(A) ⟹ M(f) ⟹ M(g) ⟹ strong_replacement(M, λx y. y = ⟨x, if x ∈ A then f ` x else g ` x⟩)"
using lam_replacement_if lam_replacement_apply[of f] lam_replacement_apply[of g]
separation_in_constant
unfolding lam_replacement_def
by simp
lemma ifx_replacement:
"M(f) ⟹
M(b) ⟹ strong_replacement(M, λx y. y = ⟨x, if x ∈ range(f) then converse(f) ` x else b⟩)"
using lam_replacement_if lam_replacement_apply lam_replacement_constant
separation_in_constant
unfolding lam_replacement_def
by simp
lemma if_then_range_replacement2:
"M(A) ⟹ M(C) ⟹ strong_replacement(M, λx y. y = ⟨x, if x = Inl(A) then C else x⟩)"
using lam_replacement_if lam_replacement_constant lam_replacement_identity
separation_equal
unfolding lam_replacement_def
by simp
lemma if_then_range_replacement:
"M(u) ⟹
M(f) ⟹
strong_replacement
(M,
λz y. y = ⟨z, if z = u then f ` 0 else if z ∈ range(f) then f ` succ(converse(f) ` z) else z⟩)"
using lam_replacement_if separation_equal separation_in_constant
lam_replacement_constant lam_replacement_identity
lam_replacement_succ lam_replacement_apply
lam_replacement_hcomp[of "λx. converse(f)`x" "succ"]
lam_replacement_hcomp[of "λx. succ(converse(f)`x)" "λx . f`x"]
unfolding lam_replacement_def
by simp
lemma Inl_replacement2:
"M(A) ⟹
strong_replacement(M, λx y. y = ⟨x, if fst(x) = A then Inl(snd(x)) else Inr(x)⟩)"
using lam_replacement_if separation_fst_equal
lam_replacement_hcomp[of "snd" "Inl"]
lam_replacement_Inl lam_replacement_Inr lam_replacement_snd
unfolding lam_replacement_def
by simp
lemma case_replacement1:
"strong_replacement(M, λz y. y = ⟨z, case(Inr, Inl, z)⟩)"
using lam_replacement_case lam_replacement_Inl lam_replacement_Inr
unfolding lam_replacement_def
by simp
lemma case_replacement2:
"strong_replacement(M, λz y. y = ⟨z, case(case(Inl, λy. Inr(Inl(y))), λy. Inr(Inr(y)), z)⟩)"
using lam_replacement_case lam_replacement_hcomp
case_closed[of Inl "λx. Inr(Inl(x))"]
lam_replacement_Inl lam_replacement_Inr
unfolding lam_replacement_def
by simp
lemma case_replacement4:
"M(f) ⟹ M(g) ⟹ strong_replacement(M, λz y. y = ⟨z, case(λw. Inl(f ` w), λy. Inr(g ` y), z)⟩)"
using lam_replacement_case lam_replacement_hcomp
lam_replacement_Inl lam_replacement_Inr lam_replacement_apply
unfolding lam_replacement_def
by simp
lemma case_replacement5:
"strong_replacement(M, λx y. y = ⟨x, (λ⟨x,z⟩. case(λy. Inl(⟨y, z⟩), λy. Inr(⟨y, z⟩), x))(x)⟩)"
unfolding split_def case_def cond_def
using lam_replacement_if separation_equal_fst2
lam_replacement_snd lam_replacement_Inl lam_replacement_Inr
lam_replacement_hcomp[OF
lam_replacement_product[OF
lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_snd]]]
unfolding lam_replacement_def
by simp
end
locale M_Pi_replacement = M_Pi + M_replacement
begin
lemma curry_rel_exp :
assumes "M(f)" "M(A)" "M(B)" "M(C)" "f ∈ A × B → C"
shows "curry(A,B,f) ∈ A →⇗M⇖ (B →⇗M⇖ C)"
using assms transM[of _ A] lam_closed[OF apply_replacement2]
lam_replacement_apply_const_id
lam_apply_replacement lam_replacement_iff_lam_closed
unfolding curry_def
by (intro lam_type mem_function_space_rel_abs[THEN iffD2],auto)
end
definition
dC_F :: "i ⇒ i ⇒ i" where
"dC_F(A,d) ≡ {p ∈ A. domain(p) = d }"
definition
drSR_Y :: "i ⇒ i ⇒ i ⇒ i ⇒ i" where
"drSR_Y(B,D,A,x) ≡ {y . r∈A , restrict(r,B) = x ∧ y = domain(r) ∧ domain(r) ∈ D}"
lemma drSR_Y_equality: "drSR_Y(B,D,A,x) = { dr∈D . (∃r∈A . restrict(r,B) = x ∧ dr=domain(r)) }"
unfolding drSR_Y_def by auto
context M_replacement
begin
lemma separation_restrict_eq_dom_eq:"∀x[M].separation(M, λdr. ∃r∈A . restrict(r,B) = x ∧ dr=domain(r))"
if "M(A)" and "M(B)" for A B
using that
separation_eq[OF _
lam_replacement_fst _
lam_replacement_hcomp[OF lam_replacement_snd lam_replacement_domain ]]
separation_eq[OF _
lam_replacement_hcomp[OF lam_replacement_snd lam_replacement_restrict'] _
lam_replacement_constant]
by(clarify,rule_tac separation_bex[OF _ ‹M(A)›],rule_tac separation_conj,simp_all)
lemma separation_is_insnd_restrict_eq_dom : "separation(M, λp. (∃r∈A. restrict(r, B) = fst(p) ∧ snd(p) = domain(r)))"
if "M(B)" "M(D)" "M(A)" for A B D
using that lam_replacement_fst lam_replacement_snd
separation_eq lam_replacement_hcomp lam_replacement_domain
lam_replacement_hcomp[OF _ lam_replacement_restrict']
by( rule_tac separation_bex[OF _ ‹M(A)›],rule_tac separation_conj,simp_all)
lemma lam_replacement_drSR_Y:
assumes "M(B)" "M(D)" "M(A)"
shows "lam_replacement(M, drSR_Y(B,D,A))"
using lam_replacement_cong[OF lam_replacement_Collect'[OF _ separation_is_insnd_restrict_eq_dom]]
assms drSR_Y_equality separation_restrict_eq_dom_eq
by simp
lemma drSR_Y_closed:
assumes "M(B)" "M(D)" "M(A)" "M(f)"
shows "M(drSR_Y(B,D,A,f))"
using assms drSR_Y_equality lam_replacement_Collect'[OF ‹M(D)›]
assms drSR_Y_equality separation_is_insnd_restrict_eq_dom separation_restrict_eq_dom_eq
by simp
lemma lam_if_then_apply_replacement: "M(f) ⟹ M(v) ⟹ M(u) ⟹
lam_replacement(M, λx. if f ` x = v then f ` u else f ` x)"
using lam_replacement_if separation_equal_apply lam_replacement_constant lam_replacement_apply
by simp
lemma lam_if_then_apply_replacement2: "M(f) ⟹ M(m) ⟹ M(y) ⟹
lam_replacement(M, λz . if f ` z = m then y else f ` z)"
using lam_replacement_if separation_equal_apply lam_replacement_constant lam_replacement_apply
by simp
lemma lam_if_then_replacement2: "M(A) ⟹ M(f) ⟹
lam_replacement(M, λx . if x ∈ A then f ` x else x)"
using lam_replacement_if separation_in_constant lam_replacement_identity lam_replacement_apply
by simp
lemma lam_if_then_replacement_apply: "M(G) ⟹ lam_replacement(M, λx. if M(x) then G ` x else 0)"
using lam_replacement_if separation_in_constant lam_replacement_identity lam_replacement_apply
lam_replacement_constant[of 0] separation_univ
by simp
lemma lam_replacement_dC_F:
assumes "M(A)"
shows "lam_replacement(M, dC_F(A))"
proof -
have "separation(M, λp. domain(snd(p)) = fst(p))" if "M(A)" for A
using separation_eq that
lam_replacement_hcomp lam_replacement_fst lam_replacement_snd lam_replacement_domain
by simp_all
then
show ?thesis
unfolding dC_F_def
using assms lam_replacement_Collect'[of A "λ d x . domain(x) = d"]
separation_eq[OF _ lam_replacement_domain _ lam_replacement_constant]
by simp
qed
lemma dCF_closed:
assumes "M(A)" "M(f)"
shows "M(dC_F(A,f))"
unfolding dC_F_def
using assms lam_replacement_Collect'[of A "λ d x . domain(x) = d"]
separation_eq[OF _ lam_replacement_domain _ lam_replacement_constant]
by simp
lemma lam_replacement_Collect_ball_Pair:
assumes "M(G)" "M(Q)"
shows "lam_replacement(M, λx . {a ∈ G . ∀s∈x. ⟨s, a⟩ ∈ Q})"
proof -
have "separation(M, λp. (∀s∈fst(p). ⟨s, snd(p)⟩ ∈ Q))"
using separation_in assms lam_replacement_identity
lam_replacement_constant lam_replacement_hcomp[OF lam_replacement_fst
lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_snd]]
lam_replacement_snd lam_replacement_fst
lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_fst]
by(rule_tac separation_all,simp_all,rule_tac separation_in,simp_all,rule_tac lam_replacement_product[of "snd" "λx . snd(fst(fst(x)))"],simp_all)
then
show ?thesis
using assms lam_replacement_Collect'
by simp_all
qed
lemma surj_imp_inj_replacement3:
assumes "M(G)" "M(Q)" "M(x)"
shows "strong_replacement(M, λy z. y ∈ {a ∈ G . ∀s∈x. ⟨s, a⟩ ∈ Q} ∧ z = {⟨x, y⟩})"
proof -
from assms
have "separation(M, λz. ∀s∈x. ⟨s, z⟩ ∈ Q)"
using lam_replacement_swap lam_replacement_constant separation_in separation_ball
by simp
with assms
show ?thesis
using separation_in_constant lam_replacement_sing_const_id[of x] separation_conj
by(rule_tac strong_replacement_separation,simp_all)
qed
lemmas replacements = Pair_diff_replacement id_replacement tag_replacement
pospend_replacement prepend_replacement
Inl_replacement1 diff_Pair_replacement
swap_replacement tag_union_replacement csquare_lam_replacement
assoc_replacement prod_fun_replacement
cardinal_lib_assms4 domain_replacement
apply_replacement
un_Pair_replacement restrict_strong_replacement diff_replacement
if_then_Inj_replacement lam_if_then_replacement if_then_replacement
ifx_replacement if_then_range_replacement2 if_then_range_replacement
Inl_replacement2
case_replacement1 case_replacement2 case_replacement4 case_replacement5
lemma zermelo_separation: "M(Q) ⟹ M(f) ⟹ separation(M, λX. Q ∪ f `` X ⊆ X)"
using lam_replacement_identity lam_replacement_Un[THEN [5] lam_replacement_hcomp2]
lam_replacement_constant lam_replacement_Image[THEN [5] lam_replacement_hcomp2]
separation_subset
by simp
end
subsection‹Some basic replacement lemmas›
lemma (in M_trans) strong_replacement_conj:
assumes "⋀A. M(A) ⟹ univalent(M,A,P)" "strong_replacement(M,P)"
"separation(M, λx. ∃b[M]. Q(x,b) ∧ P(x,b))"
shows "strong_replacement(M, λx z. Q(x,z) ∧ P(x,z))"
proof -
{
fix A
assume "M(A)"
with ‹separation(M, λx. ∃b[M]. Q(x,b) ∧ P(x,b))›
have "M({x∈A. ∃b[M]. Q(x,b) ∧ P(x,b)})"
by simp
with ‹M(_) ⟹ univalent(M,{x∈A. ∃b[M]. Q(x,b) ∧ P(x,b)}, P)› ‹strong_replacement(M, P)›
have "∃Y[M]. ∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ {x∈A. ∃b[M]. Q(x,b) ∧ P(x,b)} ∧ P(x, b))"
unfolding strong_replacement_def by blast
then
obtain Y where "∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ {x∈A. ∃b[M]. Q(x,b) ∧ P(x,b)} ∧ P(x, b))" "M(Y)"
by blast
with ‹M(A)› ‹M(A) ⟹ univalent(M,A,P)›
have "∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ A ∧ Q(x, b) ∧ P(x, b))"
unfolding univalent_def by auto
with ‹M(Y)›
have "∃Y[M]. ∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ A ∧ Q(x, b) ∧ P(x, b))"
by auto
}
then
show ?thesis
unfolding strong_replacement_def by simp
qed
lemma strong_replacement_iff_bounded_M:
"strong_replacement(M,P) ⟷ strong_replacement(M,λ x z . M(z) ∧ M(x) ∧ P(x,z))"
unfolding strong_replacement_def by auto
end