Theory FiniteFun_Relative
section‹Relativization of Finite Functions›
theory FiniteFun_Relative
imports
Lambda_Replacement
begin
lemma FiniteFunI :
assumes "f∈Fin(A×B)" "function(f)"
shows "f ∈ A -||> B"
using assms
proof(induct)
case 0
then show ?case using emptyI by simp
next
case (cons p f)
moreover
from assms this
have "fst(p)∈A" "snd(p)∈B" "function(f)"
using snd_type[OF ‹p∈_›] function_subset
by auto
moreover
from ‹function(cons(p,f))› ‹p∉f› ‹p∈_›
have "fst(p)∉domain(f)"
unfolding function_def
by force
ultimately
show ?case
using consI[of "fst(p)" _ "snd(p)"]
by auto
qed
subsection‹The set of finite binary sequences›
text‹We implement the poset for adding one Cohen real, the set
$2^{<\omega}$ of finite binary sequences.›
definition
seqspace :: "[i,i] ⇒ i" (‹_⇗<_⇖› [100,1]100) where
"B⇗<α⇖ ≡ ⋃n∈α. (n→B)"
lemma seqspaceI[intro]: "n∈α ⟹ f:n→B ⟹ f∈B⇗<α⇖"
unfolding seqspace_def by blast
lemma seqspaceD[dest]: "f∈B⇗<α⇖ ⟹ ∃n∈α. f:n→B"
unfolding seqspace_def by blast
locale M_pre_seqspace = M_trancl + M_replacement + M_Pi
begin
lemma function_space_subset_Pow_rel:
assumes "n∈ω" "M(B)"
shows "n→B ⊆ Pow⇗M⇖(⋃(ω→⇗M⇖B))"
proof -
{
fix f p
assume "f ⊆ n × B" "p ∈ f"
with assms
obtain x y where "p =⟨x,y⟩" "x∈n" "y∈B" by auto
with assms
have "p ∈ (λ_∈ω. y)"
using Ord_trans[of _ _ ω] lam_constant_eq_cartprod by simp
moreover
note assms and ‹y∈B›
moreover from this
have "M(λ_∈ω. y)" using lam_constant_eq_cartprod by (auto dest:transM)
moreover from calculation
have "(λ_∈ω. y) : ω →⇗M⇖ B"
using mem_function_space_rel_abs[of ω B, THEN iffD2]
by simp
ultimately
have "∃B∈ω →⇗M⇖ B. p ∈ B"
by (rule_tac x="λ_∈ω. y" in bexI)
}
with assms
show ?thesis
by (auto dest:transM intro!:mem_Pow_rel_abs[THEN iffD2])
(unfold Pi_def, auto)
qed
lemma seqspace_subset_Pow_rel:
assumes "M(B)"
shows "B⇗<ω⇖ ⊆ Pow⇗M⇖(⋃(ω→⇗M⇖B))"
using assms function_space_subset_Pow_rel unfolding seqspace_def
by auto
lemma seqspace_imp_M:
assumes "x ∈ B⇗<ω⇖" "M(B)"
shows "M(x)"
using assms seqspace_subset_Pow_rel
by (auto dest:transM)
lemma seqspace_eq_Collect:
assumes "M(B)"
shows "B⇗<ω⇖ = {z ∈ Pow⇗M⇖(⋃(ω→⇗M⇖B)). ∃x[M]. ∃n[M]. n ∈ ω ∧ z ∈ x ∧ x = n →⇗M⇖ B}"
using assms seqspace_subset_Pow_rel nat_into_M seqspace_imp_M
transM[OF _ finite_funspace_closed, of _ _ B] function_space_rel_char
by (intro equalityI) (auto dest:transM dest!:seqspaceD)
end
locale M_seqspace = M_pre_seqspace +
assumes
seqspace_separation: "M(B) ⟹ separation(M,λz. ∃x[M]. ∃n[M]. n ∈ ω ∧ z ∈ x ∧ x = n →⇗M⇖ B)"
begin
lemma seqspace_closed:
"M(B) ⟹ M(B⇗<ω⇖)"
using seqspace_eq_Collect using seqspace_separation
by simp
end
subsection‹Representation of finite functions›
text‹A function $f\in A\to_{\mathit{fin}}B$ can be represented by a function
$g\in |f| \to A\times B$. It is clear that $f$ can be represented by
any $g' = g \cdot \pi$, where $\pi$ is a permutation $\pi\in dom(g)\to dom(g)$.
We use this representation of $A\to_{\mathit{fin}}B$ to prove that our model is
closed under $\_\to_{\mathit{fin}}\_$.›
text‹A function $g\in n\to A\times B$ that is functional in the first components.›
definition cons_like :: "i ⇒ o" where
"cons_like(f) ≡ ∀ i∈domain(f) . ∀j∈i . fst(f`i) ≠ fst(f`j)"
definition FiniteFun_iso :: "[i,i,i,i,i] ⇒ o" where
"FiniteFun_iso(A,B,n,g,f) ≡ (∀ i∈n . g`i ∈ f) ∧ (∀ ab∈f. (∃ i∈n. g`i=ab))"
text‹From a function $g\in n \to A\times B$ we obtain a finite function in \<^term>‹A-||>B›.›
definition to_FiniteFun :: "i ⇒ i" where
"to_FiniteFun(f) ≡ {f`i. i∈domain(f)}"
definition FiniteFun_Repr :: "[i,i] ⇒ i" where
"FiniteFun_Repr(A,B) ≡ {f ∈ (A×B)⇗<ω⇖ . cons_like(f) }"
locale M_FiniteFun = M_seqspace +
assumes
separation_is_function : "separation(M, is_function(M))"
begin
lemma cons_like_separation : "separation(M,λf. cons_like(f))"
unfolding cons_like_def
using lam_replacement_identity lam_replacement_domain lam_replacement_snd
lam_replacement_hcomp[OF _ lam_replacement_snd ]
lam_replacement_hcomp[OF _ lam_replacement_fst]
separation_eq lam_replacement_apply2[THEN [5] lam_replacement_hcomp2] separation_neg
by(rule_tac separation_all,auto,rule_tac separation_all,auto)
lemma supset_separation: "separation(M, λ x. ∃a. ∃b. x = ⟨a,b⟩ ∧ b ⊆ a)"
using separation_Pair separation_subset lam_replacement_fst lam_replacement_snd
by simp
lemma to_finiteFun_replacement: "strong_replacement(M, λx y. y = range(x))"
using lam_replacement_range lam_replacement_imp_strong_replacement
by simp
lemma fun_range_eq: "f∈A→B ⟹ {f`i . i∈domain(f) } = range(f)"
using ZF_Library.range_eq_image[of f] domain_of_fun image_fun func.apply_rangeI
by simp
lemma FiniteFun_fst_type:
assumes "h∈A-||>B" "p∈h"
shows "fst(p)∈domain(h)"
using assms
by(induct h, auto)
lemma FinFun_closed:
"M(A) ⟹ M(B) ⟹ M(⋃{n→A×B . n∈ω})"
using cartprod_closed seqspace_closed
unfolding seqspace_def by simp
lemma cons_like_lt :
assumes "n∈ω" "f∈succ(n)→A×B" "cons_like(f)"
shows "restrict(f,n)∈n→A×B" "cons_like(restrict(f,n))"
using assms
proof (auto simp add: le_imp_subset restrict_type2)
from ‹f∈_›
have D:"domain(restrict(f,n)) = n" "domain(f) = succ(n)"
using domain_of_fun domain_restrict by auto
{
fix i j
assume "i∈domain(restrict(f,n))" (is "i∈?D") "j∈i"
with ‹n∈_› D
have "j∈?D" "i∈n" "j∈n" using Ord_trans[of j] by simp_all
with D ‹cons_like(f)› ‹j∈n› ‹i∈n› ‹j∈i›
have "fst(restrict(f,n)`i) ≠ fst(restrict(f,n)`j)"
using restrict_if unfolding cons_like_def by auto
}
then show "cons_like(restrict(f,n))"
unfolding cons_like_def by auto
qed
text‹A finite function \<^term>‹f ∈ A -||> B› can be represented by a
function $g \in n \to A \times B$, with $n=|f|$.›
lemma FiniteFun_iso_intro1:
assumes "f ∈ (A -||> B)"
shows "∃n∈ω . ∃g∈n→A×B. FiniteFun_iso(A,B,n,g,f) ∧ cons_like(g)"
using assms
proof(induct f,force simp add:emptyI FiniteFun_iso_def cons_like_def)
case (consI a b h)
then obtain n g where
HI: "n∈ω" "g∈n→A×B" "FiniteFun_iso(A,B,n,g,h)" "cons_like(g)" by auto
let ?G="λ i ∈ succ(n) . if i=n then <a,b> else g`i"
from HI ‹a∈_› ‹b∈_›
have G: "?G ∈ succ(n)→A×B"
by (auto intro:lam_type)
have "FiniteFun_iso(A,B,succ(n),?G,cons(<a,b>,h))"
unfolding FiniteFun_iso_def
proof(intro conjI)
{
fix i
assume "i∈succ(n)"
then consider "i=n" | "i∈n∧i≠n" by auto
then have "?G ` i ∈ cons(<a,b>,h)"
using HI
by(cases,simp;auto simp add:HI FiniteFun_iso_def)
}
then show "∀i∈succ(n). ?G ` i ∈ cons(⟨a, b⟩, h)" ..
next
{ fix ab'
assume "ab' ∈ cons(<a,b>,h)"
then
consider "ab' = <a,b>" | "ab' ∈ h" using cons_iff by auto
then
have "∃i ∈ succ(n) . ?G`i = ab'" unfolding FiniteFun_iso_def
proof(cases,simp)
case 2
with HI obtain i
where "i∈n" "g`i=ab'" unfolding FiniteFun_iso_def by auto
with HI show ?thesis using ltI[OF ‹i∈_›] by auto
qed
}
then
show "∀ab∈cons(⟨a, b⟩, h). ∃i∈succ(n). ?G`i = ab" ..
qed
with HI G
have 1: "?G∈succ(n)→A×B" "FiniteFun_iso(A,B,succ(n),?G,cons(<a,b>,h))" "succ(n)∈ω" by simp_all
have "cons_like(?G)"
proof -
from ‹?G∈_› ‹g∈_›
have "domain(g) = n" using domain_of_fun by simp
{
fix i j
assume "i∈domain(?G)" "j∈i"
with ‹n∈_›
have "j∈n" using Ord_trans[of j _ n] by auto
from ‹i∈_› consider (a) "i=n ∧ i∉n" | (b) "i∈n" by auto
then
have " fst(?G`i) ≠ fst(?G`j)"
proof(cases)
case a
with ‹j∈n› HI
have "?G`i=<a,b>" "?G`j=g`j" "g`j∈h"
unfolding FiniteFun_iso_def by auto
with ‹a∉_› ‹h∈_›
show ?thesis using FiniteFun_fst_type by auto
next
case b
with ‹i∈n› ‹j∈i› ‹j∈n› HI ‹domain(g) = n›
show ?thesis unfolding cons_like_def
using mem_not_refl by auto
qed
}
then show ?thesis unfolding cons_like_def by auto
qed
with 1 show ?case by auto
qed
text‹All the representations of \<^term>‹f∈A-||>B› are equal.›
lemma FiniteFun_isoD :
assumes "n∈ω" "g∈n→A×B" "f∈A-||>B" "FiniteFun_iso(A,B,n,g,f)"
shows "to_FiniteFun(g) = f"
proof
show "to_FiniteFun(g) ⊆ f"
proof
fix ab
assume "ab∈to_FiniteFun(g)"
moreover
note assms
moreover from calculation
obtain i where "i∈n" "g`i=ab" "ab∈A×B"
unfolding to_FiniteFun_def using domain_of_fun by auto
ultimately
show "ab∈f" unfolding FiniteFun_iso_def by auto
qed
next
show "f ⊆ to_FiniteFun(g)"
proof
fix ab
assume "ab∈f"
with assms
obtain i where "i∈n" "g`i=ab" "ab∈A×B"
unfolding FiniteFun_iso_def by auto
with assms
show "ab ∈ to_FiniteFun(g)"
unfolding to_FiniteFun_def
using domain_of_fun by auto
qed
qed
lemma to_FiniteFun_succ_eq :
assumes "n∈ω" "f∈succ(n) → A"
shows "to_FiniteFun(f) = cons(f`n,to_FiniteFun(restrict(f,n)))"
using assms domain_restrict domain_of_fun
unfolding to_FiniteFun_def by auto
text‹If $g \in n\to A\times B$ is \<^term>‹cons_like›, then it is a representation of
\<^term>‹to_FiniteFun(g)›.›
lemma FiniteFun_iso_intro_to:
assumes "n∈ω" "g∈n→A×B" "cons_like(g)"
shows "to_FiniteFun(g) ∈ (A -||> B) ∧ FiniteFun_iso(A,B,n,g,to_FiniteFun(g))"
using assms
proof(induct n arbitrary:g rule:nat_induct)
case 0
fix g
assume "g∈0→A×B"
then
have "g=0" by simp
then have "to_FiniteFun(g)=0" unfolding to_FiniteFun_def by simp
then show "to_FiniteFun(g) ∈ (A -||> B) ∧ FiniteFun_iso(A,B,0,g,to_FiniteFun(g))"
using emptyI unfolding FiniteFun_iso_def by simp
next
case (succ x)
fix g
let ?g'="restrict(g,x)"
assume "g∈succ(x)→A×B" "cons_like(g)"
with succ.hyps ‹g∈_›
have "cons_like(?g')" "?g' ∈ x→A×B" "g`x∈A×B" "domain(g) = succ(x)"
using cons_like_lt succI1 apply_funtype domain_of_fun by simp_all
with succ.hyps ‹?g'∈_› ‹x∈ω›
have HI:
"to_FiniteFun(?g') ∈ A -||> B" (is "(?h) ∈ _")
"FiniteFun_iso(A,B,x,?g',to_FiniteFun(?g'))"
by simp_all
then
have "fst(g`x) ∉ domain(?h)"
proof -
{
assume "fst(g`x) ∈ domain(?h)"
with HI ‹x∈_›
obtain i b
where "i∈x" "<fst(?g'`i),b>∈?h" "i<x" "fst(g`x) = fst(?g'`i)"
unfolding FiniteFun_iso_def using ltI by auto
with ‹cons_like(g)› ‹domain(g) = _›
have False
unfolding cons_like_def by auto
}
then show ?thesis ..
qed
with HI assms ‹g`x∈_›
have "cons(g`x,?h) ∈ A-||>B" (is "?h' ∈_") using consI by auto
have "FiniteFun_iso(A,B,succ(x),g,?h')"
unfolding FiniteFun_iso_def
proof
{ fix i
assume "i∈succ(x)"
with ‹x∈_› consider (a) "i=x"| (b) "i∈x∧i≠x" by auto
then have "g`i∈ ?h'"
proof(cases,simp)
case b
with ‹FiniteFun_iso(_,_,_,?g',?h)›
show ?thesis unfolding FiniteFun_iso_def by simp
qed
}
then show "∀i∈succ(x). g ` i ∈ cons(g ` x, ?h)" ..
next
{
fix ab
assume "ab∈?h'"
then consider "ab=g`x" | "ab ∈ ?h" using cons_iff by auto
then
have "∃i ∈ succ(x) . g`i = ab" unfolding FiniteFun_iso_def
proof(cases,simp)
case 2
with HI obtain i
where 2:"i∈x" "?g'`i=ab" unfolding FiniteFun_iso_def by auto
with ‹x∈_›
have "i≠x" "i∈succ(x)" using ltI[OF ‹i∈_›] by auto
with 2 HI show ?thesis by auto
qed
} then show "∀ab∈cons(g ` x, ?h). ∃i∈succ(x). g ` i = ab" ..
qed
with ‹?h'∈_›
show "to_FiniteFun(g) ∈ A -||>B ∧ FiniteFun_iso(A,B,succ(x),g,to_FiniteFun(g))"
using to_FiniteFun_succ_eq[OF ‹x∈_› ‹g∈_›,symmetric] by auto
qed
lemma FiniteFun_iso_intro2:
assumes "n∈ω" "f∈n→A×B" "cons_like(f)"
shows "∃ g ∈ (A -||> B) . FiniteFun_iso(A,B,n,f,g)"
using assms FiniteFun_iso_intro_to by blast
lemma FiniteFun_eq_range_Repr :
shows "{range(h) . h ∈ FiniteFun_Repr(A,B) } = {to_FiniteFun(h) . h ∈ FiniteFun_Repr(A,B) }"
unfolding FiniteFun_Repr_def to_FiniteFun_def seqspace_def
using fun_range_eq
by(intro equalityI subsetI,auto)
lemma FiniteFun_eq_to_FiniteFun_Repr :
shows "A-||>B = {to_FiniteFun(h) . h ∈ FiniteFun_Repr(A,B) } "
(is "?Y=?X")
proof
{
fix f
assume "f∈A-||>B"
then obtain n g where
1: "n∈ω" "g∈n→A×B" "FiniteFun_iso(A,B,n,g,f)" "cons_like(g)"
using FiniteFun_iso_intro1 by blast
with ‹f∈_›
have "cons_like(g)" "f=to_FiniteFun(g)" "domain(g) = n" "g∈FiniteFun_Repr(A,B)"
using FiniteFun_isoD domain_of_fun
unfolding FiniteFun_Repr_def
by auto
with 1 have "f∈?X"
by auto
} then show "?Y⊆?X" ..
next
{
fix f
assume "f∈?X"
then obtain g where
A:"g∈FiniteFun_Repr(A,B)" "f=to_FiniteFun(g)" "cons_like(g)"
using RepFun_iff unfolding FiniteFun_Repr_def by auto
then obtain n where "n∈ω" "g∈n→A×B" "domain(g) = n"
unfolding FiniteFun_Repr_def using domain_of_fun by force
with A
have "f∈?Y"
using FiniteFun_iso_intro_to by simp
} then show "?X⊆?Y" ..
qed
lemma FiniteFun_Repr_closed :
assumes "M(A)" "M(B)"
shows "M(FiniteFun_Repr(A,B))"
unfolding FiniteFun_Repr_def
using assms cartprod_closed
seqspace_closed separation_closed cons_like_separation
by simp
lemma to_FiniteFun_closed:
assumes "M(A)" "f∈A"
shows "M(range(f))"
using assms transM[of _ A] by simp
lemma To_FiniteFun_Repr_closed :
assumes "M(A)" "M(B)"
shows "M({range(h) . h ∈ FiniteFun_Repr(A,B) })"
using assms FiniteFun_Repr_closed
RepFun_closed to_finiteFun_replacement
to_FiniteFun_closed[OF FiniteFun_Repr_closed]
by simp
lemma FiniteFun_closed[intro,simp] :
assumes "M(A)" "M(B)"
shows "M(A -||> B)"
using assms To_FiniteFun_Repr_closed FiniteFun_eq_to_FiniteFun_Repr
FiniteFun_eq_range_Repr
by simp
end
end