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 by assuming a seven instances of separation and
ten instances of "lambda" replacements 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_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_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
lemma converse_subset : "converse(r) ⊆ {⟨snd(x),fst(x)⟩ . x∈r}"
unfolding converse_def
proof(intro subsetI, auto)
fix u v
assume "⟨u,v⟩∈r" (is "?z∈r")
moreover
have "v=snd(?z)" "u=fst(?z)" by simp_all
ultimately
show "∃z∈r. v=snd(z) ∧ u = fst(z)"
using rexI[where x="⟨u,v⟩"] by force
qed
lemma converse_eq_aux :
assumes "<0,0>∈r"
shows "converse(r) = {⟨snd(x),fst(x)⟩ . x∈r}"
using converse_subset
proof(intro equalityI subsetI,auto)
fix z
assume "z∈r"
then show "⟨fst(z),snd(z)⟩ ∈ r"
proof(cases "∃ a b . z =⟨a,b⟩")
case True
with ‹z∈r›
show ?thesis by auto
next
case False
then
have "fst(z) = 0" "snd(z)=0"
unfolding fst_def snd_def by auto
with ‹z∈r› assms
show ?thesis by auto
qed
qed
lemma converse_eq_aux' :
assumes "<0,0>∉r"
shows "converse(r) = {⟨snd(x),fst(x)⟩ . x∈r} - {<0,0>}"
using converse_subset assms
proof(intro equalityI subsetI,auto)
fix z
assume "z∈r" "snd(z)≠0"
then
obtain a b where "z = ⟨a,b⟩" unfolding snd_def by force
with ‹z∈r›
show "⟨fst(z),snd(z)⟩ ∈ r"
by auto
next
fix z
assume "z∈r" "fst(z)≠0"
then
obtain a b where "z = ⟨a,b⟩" unfolding fst_def by force
with ‹z∈r›
show "⟨fst(z),snd(z)⟩ ∈ r"
by auto
qed
lemma diff_un : "b⊆a ⟹ (a-b) ∪ b = a"
by auto
lemma converse_eq: "converse(r) = ({⟨snd(x),fst(x)⟩ . x∈r} - {<0,0>}) ∪ (r∩{<0,0>})"
proof(cases "<0,0>∈r")
case True
then
have "converse(r) = {⟨snd(x),fst(x)⟩ . x∈r}"
using converse_eq_aux by auto
moreover
from True
have "r∩{<0,0>} = {<0,0>}" "{<0,0>}⊆{⟨snd(x),fst(x)⟩ . x∈r}"
using converse_subset by auto
moreover from this True
have "{⟨snd(x),fst(x)⟩ . x∈r} = ({⟨snd(x),fst(x)⟩ . x∈r} - {<0,0>}) ∪ ({<0,0>})"
using diff_un[of "{<0,0>}",symmetric] converse_eq_aux by auto
ultimately
show ?thesis
by simp
next
case False
then
have "r∩{<0,0>} = 0" by auto
then
have "({⟨snd(x),fst(x)⟩ . x∈r} - {<0,0>}) ∪ (r∩{<0,0>}) = ({⟨snd(x),fst(x)⟩ . x∈r} - {<0,0>})"
by simp
with False
show ?thesis
using converse_eq_aux' by auto
qed
lemma range_subset : "range(r) ⊆ {snd(x). x∈r}"
unfolding range_def domain_def converse_def
proof(intro subsetI, auto)
fix u v
assume "⟨u,v⟩∈r" (is "?z∈r")
moreover
have "v=snd(?z)" "u=fst(?z)" by simp_all
ultimately
show "∃z∈r. v=snd(z)"
using rexI[where x="v"] by force
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 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 lam_replacement_domain':
assumes "∀A[M]. separation(M, λy. ∃x∈A. y = ⟨x, domain(x)⟩)"
shows "lam_replacement(M,domain)"
proof -
have "∀x∈X. domain(x) ∈ Pow⇗M⇖(⋃⋃⋃X)" if "M(X)" for X
proof
fix x
assume "x∈X"
moreover
note ‹M(X)›
moreover from calculation
have "M(x)" by (auto dest:transM)
ultimately
show "domain(x) ∈ Pow⇗M⇖(⋃⋃⋃X)"
by(rule_tac mem_Pow_rel_abs[of "domain(x)" "⋃⋃⋃X",THEN iffD2],auto simp:Pair_def,force)
qed
with assms
show ?thesis
using bounded_lam_replacement[of domain "λX. Pow⇗M⇖(⋃⋃⋃X)"] by simp
qed
lemma lam_replacement_fst':
assumes "∀A[M]. separation(M, λy. ∃x∈A. y = ⟨x, fst(x)⟩)"
shows "lam_replacement(M,fst)"
proof -
have "∀x∈X. fst(x) ∈ {0} ∪ ⋃⋃X" if "M(X)" for X
proof
fix x
assume "x∈X"
moreover
note ‹M(X)›
moreover from calculation
have "M(x)" by (auto dest:transM)
ultimately
show "fst(x) ∈ {0} ∪ ⋃⋃X" unfolding fst_def Pair_def
by (auto, rule_tac [1] the_0) force
qed
with assms
show ?thesis
using bounded_lam_replacement[of fst "λX. {0} ∪ ⋃⋃X"] by simp
qed
lemma lam_replacement_restrict:
assumes "∀A[M]. separation(M, λy. ∃x∈A. y = ⟨x, restrict(x,B)⟩)" "M(B)"
shows "lam_replacement(M, λr . restrict(r,B))"
proof -
have "∀r∈R. restrict(r,B)∈Pow⇗M⇖(⋃R)" if "M(R)" for R
proof -
{
fix r
assume "r∈R"
with ‹M(B)›
have "restrict(r,B)∈Pow(⋃R)" "M(restrict(r,B))"
using Union_upper subset_Pow_Union subset_trans[OF restrict_subset]
transM[OF _ ‹M(R)›]
by simp_all
} then show ?thesis
using Pow_rel_char that by simp
qed
with assms
show ?thesis
using bounded_lam_replacement[of "λr . restrict(r,B)" "λX. Pow⇗M⇖(⋃X)"]
by simp
qed
end
locale M_replacement = M_basic +
assumes
lam_replacement_domain: "lam_replacement(M,domain)"
and
lam_replacement_fst: "lam_replacement(M,fst)"
and
lam_replacement_snd: "lam_replacement(M,snd)"
and
lam_replacement_Union: "lam_replacement(M,Union)"
and
middle_separation: "separation(M, λx. snd(fst(x))=fst(snd(x)))"
and
middle_del_replacement: "strong_replacement(M, λx y. y=⟨fst(fst(x)),snd(snd(x))⟩)"
and
product_replacement:
"strong_replacement(M, λx y. y=⟨snd(fst(x)),⟨fst(fst(x)),snd(snd(x))⟩⟩)"
and
lam_replacement_Upair:"lam_replacement(M, λp. Upair(fst(p),snd(p)))"
and
lam_replacement_Diff:"lam_replacement(M, λp. fst(p) - snd(p))"
and
lam_replacement_Image:"lam_replacement(M, λp. fst(p) `` snd(p))"
and
separation_fst_in_snd: "separation(M, λy. fst(snd(y)) ∈ snd(snd(y)))"
and
lam_replacement_converse : "lam_replacement(M,converse)"
and
lam_replacement_comp: "lam_replacement(M, λx. fst(x) O snd(x))"
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 product_replacement ‹M(?P)› ] 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 middle_del_replacement ‹M(?P)›] 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_Collect :
assumes "M(A)" "∀x[M]. separation(M,F(x))"
"separation(M,λp . ∀x∈A. x∈snd(p) ⟷ F(fst(p),x))"
shows "lam_replacement(M,λx. {y∈A . F(x,y)})"
proof -
{
fix Z
let ?Y="λz.{x∈A . F(z,x)}"
assume "M(Z)"
moreover from this
have "M(?Y(z))" if "z∈Z" for z
using assms that transM[of _ Z] by simp
moreover from this
have "?Y(z)∈Pow⇗M⇖(A)" if "z∈Z" for z
using Pow_rel_char that assms by auto
moreover from calculation ‹M(A)›
have "M(Z×Pow⇗M⇖(A))" by simp
moreover from this
have "M({p ∈ Z×Pow⇗M⇖(A) . ∀x∈A. x∈snd(p) ⟷ F(fst(p),x)})" (is "M(?P)")
using assms by simp
ultimately
have "b ∈ ?P ⟷ (∃z[M]. z∈Z ∧ b=⟨z,?Y(z)⟩)" if "M(b)" for b
using assms(1) Pow_rel_char[OF ‹M(A)›] that
by(intro iffI,auto,intro equalityI,auto)
with ‹M(?P)›
have "∃Y[M]. ∀b[M]. b ∈ Y ⟷ (∃z[M]. z ∈ Z ∧ b = ⟨z,?Y(z)⟩)"
by (rule_tac rexI[where x="?P"],simp_all)
}
then
show ?thesis
unfolding 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)))"
"∀x[M]. ∀y[M]. M(h(x,y))"
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 lam_replacement_vimage :
shows "lam_replacement(M, λx. fst(x)-``snd(x))"
unfolding vimage_def using
lam_replacement_hcomp2[OF
lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_converse] lam_replacement_snd
_ _ lam_replacement_Image]
by auto
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 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
lemma separation_in_domain : "M(a) ⟹ separation(M, λx. a∈domain(x))"
using lam_replacement_domain lam_replacement_constant separation_in
by auto
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 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_Pair:
shows "lam_replacement(M, λx. ⟨fst(x), snd(x)⟩)"
unfolding lam_replacement_def strong_replacement_def
proof (clarsimp)
fix A
assume "M(A)"
then
show "∃Y[M]. ∀b[M]. b ∈ Y ⟷ (∃x∈A. b = ⟨x, fst(x), snd(x)⟩)"
unfolding lam_replacement_def strong_replacement_def
proof (cases "relation(A)")
case True
with ‹M(A)›
show ?thesis
using id_closed unfolding relation_def
by (rule_tac x="id(A)" in rexI) auto
next
case False
moreover
note ‹M(A)›
moreover from this
have "M({z∈A. ∃x y. z = ⟨x, y⟩})" (is "M(?rel)")
using relation_separation by auto
moreover
have "z = ⟨fst(z), snd(z)⟩" if "fst(z) ≠ 0 ∨ snd(z) ≠ 0" for z
using that
by (cases "∃a b. z=⟨a,b⟩") (auto simp add: the_0 fst_def snd_def)
ultimately
show ?thesis
using id_closed unfolding relation_def
by (rule_tac x="id(?rel) ∪ (A-?rel)×{0}×{0}" in rexI)
(force simp:fst_def snd_def)+
qed
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: "lam_replacement(M, λx. {x})"
using lam_replacement_constant lam_replacement_cons
lam_replacement_hcomp2[of "λx. x" "λ_. 0" cons]
by (force intro: lam_replacement_identity)
lemmas tag_replacement = lam_replacement_constant[unfolded lam_replacement_def]
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_sing lam_replacement_fst lam_replacement_snd
lam_replacement_Image lam_replacement_Union
unfolding apply_def
by (rule_tac lam_replacement_hcomp[of _ Union],
rule_tac lam_replacement_hcomp2[of _ _ "(``)"])
(force intro:lam_replacement_hcomp)+
definition map_snd where
"map_snd(X) = {snd(z) . z∈X}"
lemma map_sndE: "y∈map_snd(X) ⟹ ∃p∈X. y=snd(p)"
unfolding map_snd_def by auto
lemma map_sndI : "∃p∈X. y=snd(p) ⟹ y∈map_snd(X)"
unfolding map_snd_def by auto
lemma map_snd_closed: "M(x) ⟹ M(map_snd(x))"
unfolding map_snd_def
using lam_replacement_imp_strong_replacement[OF lam_replacement_snd]
RepFun_closed snd_closed[OF transM[of _ x]]
by simp
lemma lam_replacement_imp_lam_replacement_RepFun:
assumes "lam_replacement(M, f)" "∀x[M]. M(f(x))"
"separation(M, λx. ((∀y∈snd(x). fst(y) ∈ fst(x)) ∧ (∀y∈fst(x). ∃u∈snd(x). y=fst(u))))"
and
lam_replacement_RepFun_snd:"lam_replacement(M,map_snd)"
shows "lam_replacement(M, λx. {f(y) . y∈x})"
proof -
have f_closed:"M(⟨fst(z),map_snd(snd(z))⟩)" if "M(z)" for z
using pair_in_M_iff fst_closed snd_closed map_snd_closed that
by simp
have p_closed:"M(⟨x,{f(y) . y∈x}⟩)" if "M(x)" for x
using pair_in_M_iff RepFun_closed lam_replacement_imp_strong_replacement
transM[OF _ that] that assms by auto
{
fix A
assume "M(A)"
then
have "M({⟨y,f(y)⟩ . y∈x})" if "x∈A" for x
using lam_replacement_iff_lam_closed assms that transM[of _ A]
unfolding lam_def by simp
from assms ‹M(A)›
have "∀x∈⋃A. M(f(x))"
using transM[of _ "⋃A"] by auto
with assms ‹M(A)›
have "M({⟨y,f(y)⟩ . y ∈ ⋃A})" (is "M(?fUnA)")
using lam_replacement_iff_lam_closed[THEN iffD1,OF assms(2) assms(1)]
unfolding lam_def
by simp
with ‹M(A)›
have "M(Pow_rel(M,?fUnA))" by simp
with ‹M(A)›
have "M({z∈A×Pow_rel(M,?fUnA) . ((∀y∈snd(z). fst(y) ∈ fst(z)) ∧ (∀y∈fst(z). ∃u∈snd(z). y=fst(u)))})" (is "M(?T)")
using assms(3) by simp
then
have 1:"M({⟨fst(z),map_snd(snd(z))⟩ . z∈?T})" (is "M(?Y)")
using lam_replacement_product[OF lam_replacement_fst
lam_replacement_hcomp[OF lam_replacement_snd lam_replacement_RepFun_snd]]
RepFun_closed lam_replacement_imp_strong_replacement
f_closed[OF transM[OF _ ‹M(?T)›]]
by simp
have 2:"?Y = {⟨x,{f(y) . y∈x}⟩ . x∈A}" (is "_ = ?R")
proof(intro equalityI subsetI)
fix p
assume "p∈?R"
with ‹M(A)›
obtain x where "x∈A" "p=⟨x,{f(y) . y ∈ x}⟩" "M(x)"
using transM[OF _ ‹M(A)›]
by auto
moreover from calculation
have "M({⟨y,f(y)⟩ . y∈x})" (is "M(?Ux)")
using lam_replacement_iff_lam_closed assms
unfolding lam_def by auto
moreover from calculation
have "?Ux ⊆ ?fUnA"
by auto
moreover from calculation
have "?Ux ∈ Pow_rel(M,?fUnA)"
using Pow_rel_char[OF ‹M(?fUnA)›] by simp
moreover from calculation
have "∀u∈x. ∃w∈?Ux. u=fst(w)"
by force
moreover from calculation
have "⟨x,?Ux⟩ ∈ ?T" by auto
moreover from calculation
have "{f(y).y∈x} = map_snd(?Ux)"
unfolding map_snd_def
by(intro equalityI,auto)
ultimately
show "p∈?Y"
by (auto,rule_tac bexI[where x=x],simp_all,rule_tac bexI[where x="?Ux"],simp_all)
next
fix u
assume "u∈?Y"
moreover from this
obtain z where "z∈?T" "u=⟨fst(z),map_snd(snd(z))⟩"
by blast
moreover from calculation
obtain x U where
1:"x∈A" "U∈Pow_rel(M,?fUnA)" "(∀u∈U. fst(u) ∈ x) ∧ (∀w∈x. ∃v∈U. w=fst(v))" "z=⟨x,U⟩"
by force
moreover from this
have "fst(u)∈⋃A" "snd(u) = f(fst(u))" if "u∈U" for u
using that Pow_rel_char[OF ‹M(?fUnA)›]
by auto
moreover from calculation
have "map_snd(U) = {f(y) . y∈x}"
unfolding map_snd_def
by(intro equalityI subsetI,auto)
moreover from calculation
have "u=⟨x,map_snd(U)⟩"
by simp
ultimately
show "u∈?R"
by (auto)
qed
from 1 2
have "M({⟨x,{f(y) . y∈x}⟩ . x∈A})"
by simp
}
then
have "∀A[M]. M(λx∈A. {f(y) . y∈x})"
unfolding lam_def by auto
then
show ?thesis
using lam_replacement_iff_lam_closed[THEN iffD2] p_closed
by simp
qed
lemma lam_replacement_apply:"M(S) ⟹ lam_replacement(M, λx. S ` x)"
using lam_replacement_Union lam_replacement_constant lam_replacement_identity
lam_replacement_Image lam_replacement_cons
lam_replacement_hcomp2[of _ _ Image] lam_replacement_hcomp2[of "λx. x" "λ_. 0" cons]
unfolding apply_def
by (rule_tac lam_replacement_hcomp[of _ Union]) (force intro:lam_replacement_hcomp)+
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[of f]
lam_replacement_hcomp[of "λx. ⟨z, x⟩" "λx. f`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
by (force intro: lam_replacement_hcomp2 lam_replacement_constant
lam_replacement_identity)+
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 lam_replacement_vimage_sing: "lam_replacement(M, λp. fst(p) -`` {snd(p)})"
using lam_replacement_hcomp[OF lam_replacement_snd lam_replacement_sing]
lam_replacement_hcomp2[OF lam_replacement_fst _ _ _ lam_replacement_vimage]
by simp
lemma lam_replacement_vimage_sing_fun: "M(f) ⟹ lam_replacement(M, λx. f -`` {x})"
using lam_replacement_hcomp2[OF lam_replacement_constant[of f]
lam_replacement_identity _ _ lam_replacement_vimage_sing]
by simp
lemma lam_replacement_image_sing_fun: "M(f) ⟹ lam_replacement(M, λx. f `` {x})"
using lam_replacement_hcomp2[OF lam_replacement_constant[of f]
lam_replacement_hcomp[OF lam_replacement_identity lam_replacement_sing]
_ _ lam_replacement_Image]
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_hcomp[OF lam_replacement_const_id[of x]]
lam_replacement_sing pair_in_M_iff
by simp
lemma tag_singleton_closed: "M(x) ⟹ M(z) ⟹ M({{⟨z, y⟩} . y ∈ x})"
using RepFun_closed[where A=x and f="λ u. {⟨z,u⟩}"]
lam_replacement_imp_strong_replacement lam_replacement_sing_const_id
transM[of _ x]
by simp
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_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 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 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_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))"
proof (intro lam_replacement_iff_lam_closed[THEN iffD2]; clarify)
have aux_sep: "∀x[M]. separation(M,λy. ⟨fst(x), y⟩ ∈ A)"
if "M(X)" "M(A)" for X A
using separation_in lam_replacement_hcomp2[OF lam_replacement_hcomp[OF lam_replacement_constant lam_replacement_fst]
lam_replacement_identity _ _ lam_replacement_Pair]
lam_replacement_constant[of A]
that
by simp
have aux_closed: "∀x[M]. M({y ∈ X . ⟨fst(x), y⟩ ∈ A})" if "M(X)" "M(A)" for X A
using aux_sep that by simp
have aux_lemma: "lam_replacement(M,λp . {y ∈ X . ⟨fst(p), y⟩ ∈ A})"
if "M(X)" "M(A)" for X A
proof -
note lr = lam_replacement_Collect[OF ‹M(X)›]
note fst3 = lam_replacement_hcomp[OF lam_replacement_fst
lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_fst]]
then show ?thesis
using lam_replacement_Collect[OF ‹M(X)› aux_sep separation_ball[OF separation_iff']]
separation_in[OF _ lam_replacement_snd _ lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_snd]]
separation_in[OF _ lam_replacement_hcomp2[OF fst3 lam_replacement_snd _ _ lam_replacement_Pair] _
lam_replacement_constant[of A]] that
by auto
qed
from assms
show lbc:"M(x) ⟹ M(λw∈W. b(x, w))" for x
using lam_replacement_constant lam_replacement_identity
lam_replacement_hcomp2[where h=b]
by (intro lam_replacement_iff_lam_closed[THEN iffD1, rule_format])
simp_all
fix A
assume "M(A)"
moreover from this assms
have "M({b(fst(x),snd(x)). x ∈ A×W})" (is "M(?RFb)")
using lam_replacement_imp_strong_replacement transM[of _ "A×W"]
by (rule_tac RepFun_closed) auto
moreover
have "{⟨⟨x,y⟩,z⟩ ∈ (A×W)×?RFb. z = b(x,y)} = (λ⟨x,y⟩∈A×W. b(x,y)) ∩ (A×W)×?RFb"
(is "{⟨⟨x,y⟩,z⟩ ∈ (A×W)×?B. _ } = ?lam")
unfolding lam_def by auto
moreover from calculation and assms
have "M(?lam)"
using lam_replacement_iff_lam_closed unfolding split_def by simp
moreover
have "{⟨⟨x,y⟩,z⟩ ∈ (X × Y) × Z . P(x, y, z)} ⊆ (X × Y) × Z" for X Y Z P
by auto
then
have "{⟨x,y,z⟩ ∈ X×Y×Z. P(x,y,z) }= (λ⟨⟨x,y⟩,z⟩∈(X×Y)×Z. ⟨x,y,z⟩) ``
{⟨⟨x,y⟩,z⟩ ∈ (X×Y)×Z. P(x,y,z) }" (is "?C' = Lambda(?A,?f) `` ?C")
for X Y Z P
using image_lam[of ?C ?A ?f]
by (intro equalityI) (auto)
with calculation
have "{⟨x,y,z⟩ ∈ A×W×?RFb. z = b(x,y) } =
(λ⟨⟨x,y⟩,z⟩∈(A×W)×?RFb. ⟨x,y,z⟩) `` ?lam" (is "?H = ?G ")
by simp
with ‹M(A)› ‹M(W)› ‹M(?lam)› ‹M(?RFb)›
have "M(?H)"
using lam_replacement_iff_lam_closed[THEN iffD1, rule_format, OF _ lam_replacement_twist]
by simp
moreover from this and ‹M(A)›
have "(λx∈A. λw∈W. b(x, w)) =
{⟨x,Z⟩ ∈ A × Pow⇗M⇖(range(?H)). Z = {y ∈ W×?RFb . ⟨x, y⟩ ∈ ?H}}"
unfolding lam_def
by (intro equalityI; subst Pow_rel_char[of "range(?H)"])
(auto dest:transM simp: lbc[unfolded lam_def], force+)
moreover from calculation and ‹M(A)› and ‹M(W)›
have "M(A×Pow⇗M⇖(range(?H)))" "M(W×?RFb)"
by auto
moreover
note ‹M(W)›
moreover from calculation
have "M({⟨x,Z⟩ ∈ A × Pow⇗M⇖(range(?H)). Z = {y ∈ W×?RFb . ⟨x, y⟩ ∈ ?H}})"
using separation_eq[OF _ lam_replacement_snd
aux_closed[OF ‹M(W×?RFb)› ‹M(?H)›]
aux_lemma[OF ‹M(W×?RFb)› ‹M(?H)›]]
‹M(A×Pow⇗M⇖(_))› assms
unfolding split_def
by auto
ultimately
show "M(λx∈A. λw∈W. b(x, w))" by simp
qed
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 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 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 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 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 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_Pair[THEN [5] lam_replacement_hcomp2]
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 restrict_eq_separation': "M(B) ⟹ ∀A[M]. separation(M, λy. ∃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∈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
end
= M_replacement +
assumes
:"lam_replacement(M, λp. minimum(fst(p),snd(p)))"
and
:"lam_replacement(M, λp. RepFun(fst(p), λx. {⟨snd(p),x⟩}))"
begin
lemma :
assumes "lam_replacement(M,f)" "∀y[M]. M(f(y))"
shows "lam_replacement(M, λx. Sigfun(x,f))"
using lam_replacement_Union lam_replacement_identity
lam_replacement_sing[THEN lam_replacement_imp_strong_replacement]
lam_replacement_hcomp[of _ Union] assms tag_singleton_closed
lam_replacement_RepFun_cons[THEN [5] lam_replacement_hcomp2]
unfolding Sigfun_def
by (rule_tac lam_replacement_hcomp[of _ Union],simp_all)
subsection‹Particular instances›
lemma :
"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 :
"M(f) ⟹ M(r) ⟹ lam_replacement(M, λx. minimum(r, f -`` {x}))"
using lam_replacement_minimum lam_replacement_vimage_sing_fun lam_replacement_constant
by (rule_tac lam_replacement_hcomp2[of _ _ minimum])
(force intro: lam_replacement_identity)+
lemmas = lam_replacement_minimum_vimage[unfolded lam_replacement_def]
lemma : "M(y) ⟹ lam_replacement(M, λx. ⋃xa∈y. {⟨x, xa⟩})"
using lam_replacement_Union lam_replacement_identity lam_replacement_constant
lam_replacement_RepFun_cons[THEN [5] lam_replacement_hcomp2] tag_singleton_closed
by (rule_tac lam_replacement_hcomp[of _ Union],simp_all)
lemma : "M(y) ⟹ strong_replacement(M, λx z. z = (⋃xa∈y. {⟨x, xa⟩}))"
using lam_replacement_Pi[THEN lam_replacement_imp_strong_replacement, of y]
proof -
assume "M(y)"
then
have "M(x) ⟹ M(⋃xa∈y. {⟨x, xa⟩})" for x
using tag_singleton_closed
by (rule_tac Union_closed RepFun_closed)
with ‹M(y)›
show ?thesis
using lam_replacement_Pi[THEN lam_replacement_imp_strong_replacement, of y]
by blast
qed
lemma :
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 :
"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 :
"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 :
"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 :
"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 :
"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 :
"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 :
"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 :
"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 :
"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 :
"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
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_extra
begin
lemma :"∀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(M, λp. ∀x∈D. x ∈ snd(p) ⟷ (∃r∈A. restrict(r, B) = fst(p) ∧ x = domain(r)))"
if "M(B)" "M(D)" "M(A)" for A B D
using that lam_replacement_fst lam_replacement_hcomp lam_replacement_snd separation_in
separation_eq[OF _
lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_snd] _
lam_replacement_hcomp[OF lam_replacement_snd lam_replacement_domain]]
separation_eq separation_restrict_eq_dom_eq
lam_replacement_hcomp[OF lam_replacement_snd lam_replacement_restrict']
lam_replacement_hcomp[OF lam_replacement_fst
lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_fst]]
by(rule_tac separation_ball,rule_tac separation_iff',simp_all,
rule_tac separation_bex[OF _ ‹M(A)›],rule_tac separation_conj,simp_all)
lemma :
assumes
"M(B)" "M(D)" "M(A)"
shows "lam_replacement(M, drSR_Y(B,D,A))"
using lam_replacement_cong lam_replacement_Collect[OF ‹M(D)› separation_restrict_eq_dom_eq[of A B]]
assms drSR_Y_equality separation_is_insnd_restrict_eq_dom separation_restrict_eq_dom_eq
by simp
lemma :
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)› separation_restrict_eq_dom_eq[of A B]]
assms drSR_Y_equality separation_is_insnd_restrict_eq_dom separation_restrict_eq_dom_eq
by simp
lemma : "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 : "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 : "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 : "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 :
assumes "M(A)"
shows "lam_replacement(M, dC_F(A))"
proof -
have "separation(M, λp. ∀x∈A. x ∈ snd(p) ⟷ domain(x) = fst(p))" if "M(A)" for A
using separation_ball separation_iff'
lam_replacement_hcomp lam_replacement_fst lam_replacement_snd lam_replacement_domain
separation_in separation_eq that
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 :
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 : "M(f) ⟹ M(r) ⟹ lam_replacement(M, λx . minimum(r, f -`` {x}))"
using lam_replacement_hcomp2[OF lam_replacement_constant[of r] lam_replacement_vimage_sing_fun]
lam_replacement_minimum
by simp
lemma :
assumes "separation(M, λp. ∀x∈G. x ∈ snd(p) ⟷ (∀s∈fst(p). ⟨s, x⟩ ∈ Q))" "M(G)" "M(Q)"
shows "lam_replacement(M, λx . {a ∈ G . ∀s∈x. ⟨s, a⟩ ∈ Q})"
proof -
have 1:"∀x[M]. separation(M, λa . ∀s∈x. ⟨s, a⟩ ∈ Q)" if "M(Q)" for Q
using separation_in lam_replacement_hcomp2[OF _ _ _ _ lam_replacement_Pair]
lam_replacement_constant separation_ball
lam_replacement_hcomp lam_replacement_fst lam_replacement_snd that
by simp
then
show ?thesis
using assms lam_replacement_Collect
by simp_all
qed
lemma :
"(⋀x. M(x) ⟹ separation(M, λy. ∀s∈x. ⟨s, y⟩ ∈ Q)) ⟹ M(G) ⟹ M(Q) ⟹ M(x) ⟹
strong_replacement(M, λy z. y ∈ {a ∈ G . ∀s∈x. ⟨s, a⟩ ∈ Q} ∧ z = {⟨x, y⟩})"
using lam_replacement_imp_strong_replacement
using lam_replacement_sing_const_id[THEN lam_replacement_imp_strong_replacement, of x]
unfolding strong_replacement_def
by (simp, safe, drule_tac x="A ∩ {a ∈ G . ∀s∈x. ⟨s, a⟩ ∈ Q}" in rspec,
simp, erule_tac rexE, rule_tac x=Y in rexI) auto
lemmas = 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
end
end