Theory FiniteFun_Relative

section‹Relativization of Finite Functions›
theory FiniteFun_Relative
  imports
    Lambda_Replacement
begin

lemma FiniteFunI :
  assumes  "fFin(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)) pf 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α. (nB)"

lemma seqspaceI[intro]: "nα  f:nB  fB⇗<α⇖"
  unfolding seqspace_def by blast

lemma seqspaceD[dest]: "fB⇗<α nα. f:nB"
  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 "nB  Pow⇗M⇖((ω→⇗MB))"
proof -
  {
    fix f p
    assume "f  n × B" "p  f"
    with assms
    obtain x y where "p =x,y" "xn" "yB" by auto
    with assms
    have "p  (λ_ω. y)"
      using Ord_trans[of _ _ ω] lam_constant_eq_cartprod by simp
    moreover
    note assms and yB
    moreover from this
    have "M(λ_ω. y)" using lam_constant_eq_cartprod by (auto dest:transM)
    moreover from calculation
    have "(λ_ω. y) : ω →⇗MB"
      using mem_function_space_rel_abs[of ω B, THEN iffD2]
      by simp
    ultimately
    have "Bω →⇗MB. 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⇖((ω→⇗MB))"
  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⇖((ω→⇗MB)). x[M]. n[M]. n  ω  z  x  x = n →⇗MB}"
  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 ― ‹localeM_pre_seqspace

locale M_seqspace =  M_pre_seqspace +
  assumes
    seqspace_separation: "M(B)  separation(M,λz. x[M]. n[M]. n  ω  z  x  x = n →⇗MB)"
begin

lemma seqspace_closed:
  "M(B)  M(B⇗<ω)"
  using seqspace_eq_Collect using seqspace_separation
  by simp

end ― ‹localeM_seqspace

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)   idomain(f) . ji . fst(f`i)  fst(f`j)"

definition FiniteFun_iso :: "[i,i,i,i,i]  o" where
  "FiniteFun_iso(A,B,n,g,f)   ( in . g`i  f)  ( abf. ( in. g`i=ab))"

text‹From a function $g\in n \to A\times B$ we obtain a finite function in termA-||>B.›

definition to_FiniteFun :: "i  i" where
  "to_FiniteFun(f)  {f`i. idomain(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: "fAB  {f`i . idomain(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 "hA-||>B" "ph"
  shows  "fst(p)domain(h)"
  using assms
  by(induct h, auto)

lemma FinFun_closed:
  "M(A)  M(B)  M({nA×B . nω})"
  using cartprod_closed seqspace_closed
  unfolding seqspace_def by simp

lemma cons_like_lt :
  assumes "nω" "fsucc(n)A×B" "cons_like(f)"
  shows "restrict(f,n)nA×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 "idomain(restrict(f,n))" (is "i?D") "ji"
    with n_ D
    have "j?D" "in" "jn" using Ord_trans[of j] by simp_all
    with D cons_like(f)  jn in ji
    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 termf  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ω . gnA×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ω" "gnA×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 "isucc(n)"
      then consider "i=n" | "inin" by auto
      then have "?G ` i  cons(<a,b>,h)"
        using HI
        by(cases,simp;auto simp add:HI FiniteFun_iso_def)
    }
    then show "isucc(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 "in" "g`i=ab'" unfolding FiniteFun_iso_def by auto
        with HI show ?thesis using  ltI[OF i_] by auto
      qed
    }
    then
    show "abcons(a, b, h). isucc(n). ?G`i = ab"  ..
  qed
  with HI G
  have 1: "?Gsucc(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 "idomain(?G)" "ji"
      with n_
      have "jn" using Ord_trans[of j _ n] by auto
      from i_ consider (a) "i=n  in" | (b) "in" by auto
      then
      have " fst(?G`i)  fst(?G`j)"
      proof(cases)
        case a
        with jn HI
        have "?G`i=<a,b>" "?G`j=g`j" "g`jh"
          unfolding FiniteFun_iso_def by auto
        with a_ h_
        show ?thesis using  FiniteFun_fst_type by auto
      next
        case b
        with in ji jn 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 termfA-||>B are equal.›
lemma FiniteFun_isoD :
  assumes "nω" "gnA×B" "fA-||>B" "FiniteFun_iso(A,B,n,g,f)"
  shows "to_FiniteFun(g) = f"
proof
  show "to_FiniteFun(g)  f"
  proof
    fix ab
    assume "abto_FiniteFun(g)"
    moreover
    note assms
    moreover from calculation
    obtain i where "in" "g`i=ab" "abA×B"
      unfolding to_FiniteFun_def using domain_of_fun by auto
    ultimately
    show "abf" unfolding FiniteFun_iso_def by auto
  qed
next
  show "f  to_FiniteFun(g)"
  proof
    fix ab
    assume "abf"
    with assms
    obtain i where "in" "g`i=ab" "abA×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ω" "fsucc(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 termcons_like, then it is a representation of
termto_FiniteFun(g).›
lemma FiniteFun_iso_intro_to:
  assumes "nω" "gnA×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 "g0A×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 "gsucc(x)A×B" "cons_like(g)"
  with succ.hyps g_
  have "cons_like(?g')" "?g'  xA×B" "g`xA×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 "ix" "<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 "isucc(x)"
      with x_ consider (a) "i=x"| (b) "ixix" 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 "isucc(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:"ix" "?g'`i=ab"  unfolding FiniteFun_iso_def by auto
        with x_
        have "ix" "isucc(x)" using  ltI[OF i_] by auto
        with 2 HI show ?thesis by auto
      qed
    } then show "abcons(g ` x, ?h). isucc(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ω" "fnA×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 "fA-||>B"
    then obtain n g where
      1: "nω" "gnA×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" "gFiniteFun_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:"gFiniteFun_Repr(A,B)" "f=to_FiniteFun(g)" "cons_like(g)"
      using RepFun_iff unfolding FiniteFun_Repr_def by auto
    then obtain n where "nω" "gnA×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)" "fA"
  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 ― ‹localeM_FiniteFun

end