Theory FiniteFun_Relative
section‹Relativization of Finite Functions›
theory FiniteFun_Relative
imports
Synthetic_Definition
"Delta_System_Lemma.ZF_Library"
Discipline_Function
Lambda_Replacement
Cohen_Posets
begin
subsection‹The set of finite binary sequences›
notation nat (‹ω›)
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_seqspace= M_trancl + M_replacement +
assumes
seqspace_replacement: "M(B) ⟹ strong_replacement(M,λn z. n∈nat ∧ is_funspace(M,n,B,z))"
begin
lemma seqspace_closed :
"M(B) ⟹ M(B⇗<ω⇖)"
unfolding seqspace_def using seqspace_replacement[of B] RepFun_closed2
by simp
end
schematic_goal seqspace_fm_auto :
assumes
"i ∈ nat" "j ∈ nat" "h∈nat" "env ∈ list(A)"
shows
"(∃om∈A. omega(##A,om) ∧ nth(i,env) ∈ om ∧ is_funspace(##A, nth(i,env), nth(h,env), nth(j,env))) ⟷ (A, env ⊨ (?sqsprp(i,j,h)))"
unfolding is_funspace_def
by (insert assms ; (rule iff_sats | simp)+)
synthesize "seqspace_rel" from_schematic "seqspace_fm_auto"
arity_theorem for "seqspace_rel_fm"
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)"
relativize "cons_like" "cons_like_rel"
lemma (in M_seqspace) cons_like_abs :
"M(f) ⟹ cons_like(f) ⟷ cons_like_rel(M,f)"
unfolding cons_like_def cons_like_rel_def
using fst_abs
by simp
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
cons_like_separation : "separation(M,λf. cons_like_rel(M,f))"
and
to_finiteFun_replacement: "strong_replacement(M, λx y. y = range(x))"
and
supset_separation: "separation(M, λ x. ∃a. ∃b. x = ⟨a,b⟩ ∧ b ⊆ a)"
begin
lemma fun_range_eq : "f∈A→B ⟹ {f`i . i∈domain(f) } = range(f)"
using range_eq_image[of f] domain_of_fun image_fun func.apply_rangeI
by auto
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_abs 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
lemma Fnle_nat_closed [intro,simp]:
assumes "M(I)" "M(J)"
shows "M(Fnle(ω,I,J))"
unfolding Fnle_def Fnlerel_def Rrel_def
using supset_separation FiniteFun_closed Fn_nat_eq_FiniteFun assms by simp
end
end