Theory Lambda_Replacement
section‹Replacements using Lambdas›
theory Lambda_Replacement
imports
"ZF-Constructible.Relative"
ZF_Miscellanea
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_in :
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_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)"
using mem_Pow_rel_abs[of "domain(x)" "⋃⋃⋃X"]
apply (auto simp:Pair_def)
apply (rule_tac x=x in bexI)
apply (rule_tac x="{{xaa}, {xaa, ya}}" in bexI)
apply (rule_tac x="{xaa}" in bexI)
by simp_all
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_vimage: "lam_replacement(M, λp. fst(p) -`` snd(p))"
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
id_separation:"separation(M, λz. ∃x[M]. z = ⟨x, x⟩)"
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_separation: "separation(M, λx. fst(fst(x))=fst(snd(x)))"
and
product_replacement:
"strong_replacement(M, λx y. y=⟨fst(fst(x)),⟨snd(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_equal : "M(a) ⟹ separation(M,λx . fst(x)=a)"
and
separation_equal_fst2 : "M(a) ⟹ separation(M,λx . fst(fst(x))=a)"
and
separation_equal_apply: "M(f) ⟹ M(a) ⟹ separation(M,λx. f`x=a)"
and
separation_restrict: "M(B) ⟹ ∀A[M]. separation(M, λy. ∃x∈A. y = ⟨x, restrict(x, B)⟩)"
begin
lemmas lam_replacement_restrict'= lam_replacement_restrict[OF separation_restrict]
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 assms
have "univalent(M,A,λx y. y=⟨x,f(x)⟩)" by simp
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
have "univalent(M,A,λx y. y=⟨x,f(x)⟩)" by simp
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(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(?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(?Y'×?Z')"
by simp
moreover from this
have "M({p ∈ ?Y'×?Z' . fst(fst(p))=fst(snd(p))})" (is "M(?P)")
using product_separation by simp
moreover from calculation
have "M({ ⟨fst(fst(p)),⟨snd(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 "⟨x,f(x)⟩ ∈ ?Y'" "⟨x,g(x)⟩ ∈ ?Z'" by auto
moreover from calculation
have "⟨⟨x,f(x)⟩,⟨x,g(x)⟩⟩∈?Y'×?Z'" by auto
moreover from calculation
have "⟨⟨x,f(x)⟩,⟨x,g(x)⟩⟩ ∈ ?P"
(is "?p∈?P")
by auto
moreover from calculation
have "b = ⟨fst(fst(?p)),⟨snd(fst(?p)),snd(snd(?p))⟩⟩" by auto
moreover from calculation
have "⟨fst(fst(?p)),⟨snd(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 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 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 lam_replacement_identity : "lam_replacement(M,λx. x)"
proof -
{
fix A
assume "M(A)"
moreover from this
have "id(A) = {z∈ A×A. ∃x[M]. z=⟨x,x⟩}"
unfolding id_def lam_def by (auto dest:transM)
moreover from calculation
have "M({z∈ A×A. ∃x[M]. z=⟨x,x⟩})"
using id_separation by simp
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_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 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 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 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 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 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
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 restrict_strong_replacement : "M(A) ⟹ strong_replacement(M, λx y. y=restrict(x,A))"
using lam_replacement_restrict separation_restrict
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')
end
locale M_replacement_extra= M_replacement +
assumes
lam_replacement_minimum:"lam_replacement(M, λp. minimum(fst(p),snd(p)))"
and
lam_replacement_RepFun_cons:"lam_replacement(M, λp. RepFun(fst(p), λx. {⟨snd(p),x⟩}))"
begin
lemma lam_replacement_Sigfun :
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]
unfolding Sigfun_def
apply (rule_tac lam_replacement_hcomp[of _ Union],simp_all)
apply (rule lam_replacement_RepFun_cons[THEN [5] lam_replacement_hcomp2])
apply(simp_all add:assms)
using assms tag_singleton_closed
by (simp_all)
subsection‹Particular instances›
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_minimum_vimage :
"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 surj_imp_inj_replacement4= lam_replacement_minimum_vimage[unfolded lam_replacement_def]
lemma lam_replacement_Pi : "M(y) ⟹ lam_replacement(M, λx. ⋃xa∈y. {⟨x, xa⟩})"
using lam_replacement_Union lam_replacement_identity lam_replacement_constant
lam_replacement_sing_const_id[THEN lam_replacement_imp_strong_replacement]
lam_replacement_hcomp2[of "λx. ⟨_,x⟩" "λ_. 0" cons,
THEN lam_replacement_imp_strong_replacement] unfolding apply_def
apply (rule_tac lam_replacement_hcomp[of _ Union])
apply (auto intro:RepFun_closed dest:transM)
by (rule lam_replacement_RepFun_cons[THEN [5] lam_replacement_hcomp2])
(auto intro:RepFun_closed dest:transM)
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]
proof -
assume "M(y)"
then
have "M(x) ⟹ M(⋃xa∈y. {⟨x, xa⟩})" for x
using lam_replacement_sing_const_id[THEN lam_replacement_imp_strong_replacement]
by (rule_tac Union_closed RepFun_closed, simp_all | safe)+
(force dest: transM)
with ‹M(y)›
show ?thesis
using lam_replacement_Pi[THEN lam_replacement_imp_strong_replacement, of y]
by blast
qed
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
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
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
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
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
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) ≡ {domain(r) .. r∈A, restrict(r,B) = x ∧ 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 SepReplace_def by auto
context M_replacement_extra
begin
lemma lam_replacement_drSR_Y :
assumes
"⋀ A B. M(A) ⟹ M(B) ⟹ ∀x[M]. separation(M, λdr. ∃r∈A . restrict(r,B) = x ∧ dr=domain(r))"
"⋀ A B D . M(A) ⟹ M(B) ⟹ M(D) ⟹
separation(M, λp. ∀x∈D. x ∈ snd(p) ⟷ (∃r∈A. restrict(r, B) = fst(p) ∧ x = domain(r)))"
"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)› assms(1)[of A B]]
assms drSR_Y_equality 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 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 lam_replacement_identity lam_replacement_apply
lam_replacement_constant[of 0] separation_univ
by simp
lemma lam_replacement_dC_F :
assumes "M(A)"
"⋀d . M(d) ⟹ separation(M, λx . domain(x) = d)"
"⋀ A . M(A) ⟹ separation(M, λp. ∀x∈A. x ∈ snd(p) ⟷ domain(x) = fst(p))"
shows "lam_replacement(M, dC_F(A))"
unfolding dC_F_def
using assms lam_replacement_Collect[of A "λ d x . domain(x) = d"]
by simp
lemma lam_replacement_min : "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 lam_replacement_Collect_ball_Pair :
assumes "separation(M, λp. ∀x∈G. x ∈ snd(p) ⟷ (∀s∈fst(p). ⟨s, x⟩ ∈ Q))"
"⋀x. M(x) ⟹ separation(M, λy. ∀s∈x. ⟨s, y⟩ ∈ Q)" "M(G)"
shows "lam_replacement(M, λx . {a ∈ G . ∀s∈x. ⟨s, a⟩ ∈ Q})"
using assms lam_replacement_Collect by simp
lemma surj_imp_inj_replacement3 :
"(⋀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 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
end
end