Theory CZH_Sets_FSequences

(* Copyright 2021 (C) Mihails Milehins *)

section‹Finite sequences›
theory CZH_Sets_FSequences
  imports CZH_Sets_Cardinality
begin



subsection‹Background›


text‹
The section presents a theory of finite sequences internalized in the 
type typ‹V›. The content of this subsection
was inspired by and draws on many ideas from the content
of the theory ‹List› in the main library of Isabelle/HOL.
›



subsection‹Definition and common properties›


text‹
A finite sequence is defined as a single-valued binary relation whose domain 
is an initial segment of the set of natural numbers.
›

locale vfsequence = vsv xs for xs +
  assumes vfsequence_vdomain_in_omega: "𝒟∘ xs ∈∘ ω"

locale vfsequence_pair = r1: vfsequence xs1 + r2: vfsequence xs2 for xs1 xs2


text‹Rules.›

lemmas [intro] = vfsequence.axioms(1)

lemma vfsequenceI[intro]:
  assumes "vsv xs" and "𝒟∘ xs ∈∘ ω"
  shows "vfsequence xs"
  using assms by (simp add: vfsequence.intro vfsequence_axioms_def)

lemma vfsequenceD[dest]:
  assumes "vfsequence xs"
  shows "𝒟∘ xs ∈∘ ω"
  using assms vfsequence.vfsequence_vdomain_in_omega by simp

lemma vfsequenceE[elim]:
  assumes "vfsequence xs" and "𝒟∘ xs ∈∘ ω ⟹ P"
  shows P
  using assms by auto

lemma vfsequence_iff: "vfsequence xs ⟷ vsv xs ∧ 𝒟∘ xs ∈∘ ω"
  using vfsequence_def by auto


text‹Elementary properties.›

lemma (in vfsequence) vfsequence_vdomain: "𝒟∘ xs = vcard xs"
  unfolding vsv_vcard_vdomain[symmetric] using vfsequence_vdomain_in_omega by simp

lemma (in vfsequence) vfsequence_vcard_in_omega[simp]: "vcard xs ∈∘ ω"
  using vfsequence_vdomain_in_omega by (simp add: vfsequence_vdomain)


text‹Set operations.›

lemma vfsequence_vempty[intro, simp]: "vfsequence 0" by (simp add: vfsequenceI)

lemma vfsequence_vsingleton[intro, simp]: "vfsequence (set {⟨0, a⟩})"  
  using vone_in_omega 
  unfolding one_V_def 
  by (intro vfsequenceI) (auto simp: set_vzero_eq_ord_of_nat_vone)

lemma (in vfsequence) vfsequence_vinsert: 
  "vfsequence (vinsert ⟨vcard xs, a⟩ xs)"
  using succ_def succ_in_omega by (auto simp: vfsequence_vdomain)


text‹Connections.›

lemma (in vfsequence) vfsequence_vfinite[simp]: "vfinite xs"
  by (simp add: vfinite_vcard_omega_iff)

lemma (in vfsequence) vfsequence_vlrestriction[intro, simp]:
  assumes "k ∈∘ ω"
  shows "vfsequence (xs ↾l∘ k)"
  using assms by (force simp: vfsequence_vdomain vdomain_vlrestriction)

lemma vfsequence_vproduct: 
  assumes "n ∈∘ ω" and "xs ∈∘ (∏∘i∈∘n. A i)"
  shows "vfsequence xs"
  using assms by auto

lemma vfsequence_vcpower: 
  assumes "n ∈∘ ω" and "xs ∈∘ A ^× n"
  shows "vfsequence xs"
  using assms vfsequence_vproduct by auto

lemma vfsequence_vcomp_vsv_vfsequence:
  assumes "vsv f" and "vfsequence xs" and "ℛ∘ xs ⊆∘ 𝒟∘ f"
  shows "vfsequence (f ∘∘ xs)"
proof(intro vfsequenceI vsv_vcomp)
  interpret xs: vfsequence xs by (rule assms(2))
  show "𝒟∘ (f ∘∘ xs) ∈∘ ω"
    unfolding vdomain_vcomp_vsubset[OF assms(3)]
    by (force simp: xs.vfsequence_vdomain_in_omega)
qed (auto intro: assms)


text‹Special properties.›

lemma (in vfsequence) vfsequence_vdomain_vlrestriction[intro, simp]: 
  assumes "k ∈∘ vcard xs"
  shows "𝒟∘ (xs ↾l∘ k) = k"
  using assms
  by 
    (
      simp add: 
        OrdmemD 
        inf_absorb2   
        order.strict_implies_order 
        vdomain_vlrestriction 
        vfsequence_vdomain
    )

lemma (in vfsequence) vfsequence_vlrestriction_vcard[simp]: 
  "xs ↾l∘ (vcard xs) = xs"
  by (rule vlrestriction_vdomain[unfolded vfsequence_vdomain])

lemma vfsequence_vfinite_vcardI:
  assumes "vsv xs" and "vfinite xs" and "𝒟∘ xs = vcard xs"
  shows "vfsequence xs"
  using assms by (intro vfsequenceI) (auto simp: vfinite_vcard_omega)

lemma (in vfsequence) vfsequence_vrangeE:
  assumes "a ∈∘ ℛ∘ xs" 
  obtains n where "n ∈∘ vcard xs" and "xs⦇n⦈ = a"
  using assms vfsequence_vdomain by auto

lemma (in vfsequence) vfsequence_vrange_vproduct:
  assumes "⋀i. i ∈∘ vcard xs ⟹ xs⦇i⦈ ∈∘ A i" 
  shows "xs ∈∘ (∏∘i∈∘vcard xs. A i)"
  using vfsequence_vdomain vsv_axioms assms 
  by 
    (
      intro vproductI; 
      (intro vsv.vsv_vrange_vsubset_vifunion_app | tactic‹all_tac›)
    ) auto

lemma (in vfsequence) vfsequence_vrange_vcpower:
  assumes "ℛ∘ xs ⊆∘ A"
  shows "xs ∈∘ A ^× (vcard xs)"
  using assms
proof(elim vsubsetE; intro vcpowerI)
  assume hyp: "x ∈∘ ℛ∘ xs ⟹ x ∈∘ A" for x
  from vfsequence_vdomain show "xs ∈∘ (∏∘i∈∘vcard xs. A)"
    by (intro vproductI) (blast intro: hyp elim: vdomain_atE)+
qed


text‹Alternative forms of existing results.›

lemmas [intro, simp] = vfsequence.vfsequence_vcard_in_omega 
  and [intro, simp] = vfsequence.vfsequence_vfinite
  and [intro, simp] = vfsequence.vfsequence_vlrestriction
  and [intro, simp] = vfsequence.vfsequence_vdomain_vlrestriction
  and [intro, simp] = vfsequence.vfsequence_vlrestriction_vcard



subsection‹Appending an element to a finite sequence: ‹vcons››


subsubsection‹Definition and common properties›

definition vcons :: "V ⇒ V ⇒ V"  (infixr ‹#∘› 65) 
  where "xs #∘ x = vinsert ⟨vcard xs, x⟩ xs"


text‹Syntax.›

abbreviation vempty_vfsequence (‹[]∘›) where 
  "vempty_vfsequence ≡ 0::V"

notation vempty_vfsequence (‹[]∘›)

nonterminal fsfields
nonterminal vlist

syntax
  "" :: "V ⇒ fsfields" (‹_›)
  "_fsfields" :: "fsfields ⇒ V ⇒ fsfields" (‹_,/ _›)
  "_vlist" :: "fsfields ⇒ V" (‹[(_)]∘›)
  "_vapp" :: "V ⇒ fsfields ⇒ V" (‹_ ⦇(_)⦈∙› [100, 100] 100)

syntax_consts
  "_vlist" == vcons and
  "_vapp" == app

translations
  "[xs, x]∘" == "[xs]∘ #∘ x"
  "[x]∘" == "[]∘ #∘ x"

translations
  "f⦇xs, x⦈∙" == "f⦇[xs, x]∘⦈"
  "f⦇x⦈∙" == "f⦇[x]∘⦈"


text‹Rules.›

lemma vconsI[intro!]: 
  assumes "a ∈∘ vinsert ⟨vcard xs, x⟩ xs"
  shows "a ∈∘ xs #∘ x"
  using assms unfolding vcons_def by clarsimp

lemma vconsD[dest!]:
  assumes "a ∈∘ xs #∘ x"
  shows "a ∈∘ vinsert ⟨vcard xs, x⟩ xs"
  using assms unfolding vcons_def by clarsimp

lemma vconsE[elim!]:
  assumes "a ∈∘ xs #∘ x"
  obtains a where "a ∈∘ vinsert ⟨vcard xs, x⟩ xs"
  using assms unfolding vcons_def by clarsimp


text‹Elementary properties.›

lemma vcons_neq_vempty[simp]: "ys #∘ y ≠ []∘" by auto


text‹Set operations.›

lemma vcons_vsingleton: "[a]∘ = set {⟨0ℕ, a⟩}" unfolding vcons_def by simp

lemma vcons_vdoubleton: "[a, b]∘ = set {⟨0ℕ, a⟩, ⟨1ℕ, b⟩}" 
  unfolding vcons_def 
  using vinsert_vsingleton 
  by (force simp: vinsert_set_insert_eq)

lemma vcons_vsubset: "xs ⊆∘ xs #∘ x" by clarsimp

lemma vcons_vsubset':
  assumes "vcons xs x ⊆∘ ys"
  shows "vcons xs x ⊆∘ vcons ys y"
  using assms unfolding vcons_def by auto


text‹Connections.›

lemma (in vfsequence) vfsequence_vcons[intro, simp]: "vfsequence (xs #∘ x)"
proof(intro vfsequenceI)
  from vfsequence_vdomain_in_omega vsv_vcard_vdomain have "vcard xs = 𝒟∘ xs" 
    by (simp add: vcard_veqpoll)
  show "vsv (xs #∘ x)" 
  proof(intro vsvI)
    fix a b c assume ab: "⟨a, b⟩ ∈∘ xs #∘ x" and ac: "⟨a, c⟩ ∈∘ xs #∘ x" 
    then consider (dom) "a ∈∘ 𝒟∘ xs" | (ndom) "a = vcard xs"
      unfolding vcons_def by auto
    then show "b = c"
    proof cases
      case dom
      with ab have "⟨a, b⟩ ∈∘ xs" 
        unfolding vcons_def by (auto simp: ‹vcard xs = 𝒟∘ xs›)
      moreover from dom ac have "⟨a, c⟩ ∈∘ xs" 
        unfolding vcons_def by (auto simp: ‹vcard xs = 𝒟∘ xs›)
      ultimately show ?thesis using vsv by simp
    next
      case ndom
      from ab have "⟨a, b⟩ = ⟨vcard xs, x⟩" 
        unfolding ndom vcons_def using ‹vcard xs = 𝒟∘ xs› mem_not_refl by blast
      moreover from ac have "⟨a, c⟩ = ⟨vcard xs, x⟩" 
        unfolding ndom vcons_def using ‹vcard xs = 𝒟∘ xs› mem_not_refl by blast
      ultimately show ?thesis by simp
    qed
  next
    show "vbrelation (xs #∘ x)" unfolding vcons_def
      using vbrelation_vinsertI by auto
  qed                     
  show "𝒟∘ (xs #∘ x) ∈∘ ω"
    unfolding vcons_def 
    using succ_in_omega  
    by (auto simp: vfsequence_vdomain_in_omega succ_def ‹vcard xs = 𝒟∘ xs›)
qed

lemma (in vfsequence) vfsequence_vcons_vdomain[simp]: 
  "𝒟∘ (xs #∘ x) = succ (vcard xs)"
  by (simp add: succ_def vcons_def vfsequence_vdomain)

lemma (in vfsequence) vfsequence_vcons_vrange[simp]: 
  "ℛ∘ (xs #∘ x) = vinsert x (ℛ∘ xs)"
  by (simp add: vcons_def)

lemma (in vfsequence) vfsequence_vrange_vconsI:
  assumes "ℛ∘ xs ⊆∘ X" and "x ∈∘ X"
  shows "ℛ∘ (xs #∘ x) ⊆∘ X"
  using assms unfolding vcons_def by auto

lemmas vfsequence_vrange_vconsI = vfsequence.vfsequence_vrange_vconsI[rotated 1]


text‹Special properties.›

lemma vcons_vrange_mono:
  assumes "xs ⊆∘ ys"
  shows "ℛ∘ (xs #∘ x) ⊆∘ ℛ∘ (ys #∘ x)"
  using assms 
  unfolding vcons_def 
  by (simp add: vrange_mono vsubset_vinsert_leftI vsubset_vinsert_rightI)

lemma (in vfsequence) vfsequence_vlrestriction_succ:
  assumes [simp]: "k ∈∘ vcard xs"
  shows "xs ↾l∘ succ k = xs ↾l∘ k #∘ (xs⦇k⦈)"
proof-
  interpret vlr: vfsequence ‹xs ↾l∘ k›
    using assms by (blast intro: vfsequence_vcard_in_omega Ord_trans)
  from vlr.vfsequence_vdomain[symmetric, simplified] show ?thesis 
    by 
      (
        simp add: 
          vcons_def succ_def vfsequence_vdomain vsv_vlrestriction_vinsert
      )
qed

lemma (in vfsequence) vfsequence_vremove_vcons_vfsequence: 
  assumes "xs = xs' #∘ x"
  shows "vfsequence xs'"
proof(cases‹⟨vcard xs', x⟩ ∈∘ xs'›)
  case True
  with assms[unfolded vcons_def] have "xs = xs'" by auto
  then show ?thesis using vfsequence_axioms by simp
next
  case False
  note x_def[simp] = assms[unfolded vcons_def]
  interpret xs': vsv xs' using vsv_axioms by (auto intro: vsv_vinsertD)
  have fin: "vfinite xs'" using vfsequence_vfinite by auto
  have vcard_xs: "vcard xs = succ (vcard xs')" by (simp add: fin False)
  have [simp]: "vcard xs' ∉∘ 𝒟∘ xs'" using False vsv_axioms by auto
  have "vcard xs' ∈∘ ω" using fin vfinite_vcard_omega by auto
  have xs'_def: "xs' = xs ↾l∘ (vcard xs')" 
    using vcard_xs fin vfsequence_vdomain 
    by (auto simp: vinsert_ident succ_def)
  from vfsequence_vlrestriction[OF ‹vcard xs' ∈∘ ω›] show ?thesis 
    unfolding xs'_def[symmetric] .
qed

lemma (in vfsequence) vfsequence_vcons_ex: 
  assumes "xs ≠ []∘" 
  obtains xs' x where "xs = xs' #∘ x" and "vfsequence xs'"
proof-
  from vcard_vempty have "0 ∈∘ vcard xs" by (simp add: assms mem_0_Ord)
  then obtain k where succk: "succ k = vcard xs"
    by (metis omega_prev vfsequence_vcard_in_omega) 
  then have "k ∈∘ vcard xs" using elts_succ by blast
  from vfsequence_vlrestriction_succ[OF this, unfolded succk] show ?thesis
    by (simp add: vfsequence_vremove_vcons_vfsequence that)
qed


subsubsection‹Induction and case analysis›

lemma vfsequence_induct[consumes 1, case_names 0 vcons]:
  assumes "vfsequence xs"
    and "P []∘"
    and "⋀xs x. ⟦vfsequence xs; P xs⟧ ⟹ P (xs #∘ x)"
  shows "P xs"
proof-
  interpret vfsequence xs by (rule assms(1))
  from assms(1) obtain n where "n ∈∘ ω" and "𝒟∘ xs = n" by auto
  then have "n ≤ 𝒟∘ xs" by auto
  define P' where "P' k = P (xs ↾l∘ k)" for k
  from ‹n ∈∘ ω› and ‹n ≤ 𝒟∘ xs› have "P' n"
  proof(induction rule: omega_induct)
    case (succ n') then show ?case
    proof-
      interpret vlr: vfsequence ‹xs ↾l∘ n'› by (simp add: succ.hyps)
      have "P' n'" using succ.prems by (force intro: succ.IH)
      then have "P (xs ↾l∘ n')" unfolding P'_def by assumption
      have "n' ∈∘ vcard xs" 
        using succ.prems by (auto simp: vsubset_iff vfsequence_vdomain)
      from vfsequence_vlrestriction_succ[OF ‹n' ∈∘ vcard xs›]
      show "P' (succ n')"
        by (simp add: P'_def ‹P (xs ↾l∘ n')› assms(3) vlr.vfsequence_axioms)
    qed
  qed (simp add: P'_def assms(2))
  then show ?thesis unfolding P'_def ‹𝒟∘ xs = n›[symmetric] by simp
qed

lemma vfsequence_cases[consumes 1, case_names 0 vcons]: 
  assumes "vfsequence xs"
    and "xs = []∘ ⟹ P"
    and "⋀xs' x. ⟦xs = xs' #∘ x; vfsequence xs'⟧ ⟹ P"
  shows P
proof-
  interpret vfsequence xs by (rule assms(1))
  show ?thesis
  proof(cases ‹xs = 0›)
    case False
    then obtain xs' x where "xs = xs' #∘ x"
      by (blast intro: vfsequence_vcons_ex)
    then show ?thesis by (auto simp: assms(3) intro: vfsequence_vcons_ex)
  qed (use assms(2) in auto)
qed


subsubsection‹Evaluation›

lemma (in vfsequence) vfsequence_vcard_vcons[simp]: 
  "vcard (xs #∘ x) = succ (vcard xs)"
proof-
  interpret xsx: vfsequence ‹xs #∘ x› by simp
  have "vcard (xs #∘ x) = 𝒟∘ (xs #∘ x)" 
    by (rule xsx.vfsequence_vdomain[symmetric])
  then show ?thesis
    by (subst vcons_def) (simp add: succ_def vcons_def vfsequence_vdomain)
qed

lemma (in vfsequence) vfsequence_at_last[intro, simp]:
  assumes "i = vcard xs"
  shows "(xs #∘ x)⦇i⦈ = x"
  by (simp add: vfsequence_vdomain vcons_def assms)

lemma (in vfsequence) vfsequence_at_not_last[intro, simp]:
  assumes "i ∈∘ vcard xs"
  shows "(xs #∘ x)⦇i⦈ = xs⦇i⦈"
proof-
  from assms have [simp]: "𝒟∘ xs = vcard xs" by (auto simp: vfsequence_vdomain)
  from assms have "i ∈∘ 𝒟∘ xs" by simp
  moreover have "i ≠ vcard xs" using assms mem_not_refl by blast
  ultimately show ?thesis
    unfolding vcons_def using vsv.vsv_vinsert vsvE vsv_axioms by auto 
qed


text‹Alternative forms of existing results.›

lemmas [intro, simp] = vfsequence.vfsequence_vcons
  and [intro, simp] = vfsequence.vfsequence_vcard_vcons
  and [intro, simp] = vfsequence.vfsequence_at_last
  and [intro, simp] = vfsequence.vfsequence_at_not_last
  and [intro, simp] = vfsequence.vfsequence_vcons_vdomain
  and [intro, simp] = vfsequence.vfsequence_vcons_vrange



subsubsection‹Congruence-like properties›

context vfsequence_pair
begin

lemma vcons_eq_vcard_eq:
  assumes "xs1 #∘ x1 = xs2 #∘ x2"
  shows "vcard xs1 = vcard xs2"
  by 
    (
      metis 
        assms 
        succ_inject_iff   
        vfsequence.vfsequence_vcons_vdomain
        r1.vfsequence_axioms 
        r2.vfsequence_axioms
    )

lemma vcons_eqD[dest]:
  assumes "xs1 #∘ x1 = xs2 #∘ x2"
  shows "xs1 = xs2" and "x1 = x2"
proof-

  have xsx1_last: "(xs1 #∘ x1)⦇vcard xs1⦈ = x1" by simp
  have xsx2_last: "(xs2 #∘ x2)⦇vcard xs2⦈ = x2" by simp

  from assms have vcard: "vcard xs1 = vcard xs2" by (rule vcons_eq_vcard_eq)
  from trans[OF xsx1_last xsx1_last[unfolded vcard assms, symmetric]]
  
  show "x1 = x2" unfolding xsx1_last xsx2_last .

  have nxs1: "⟨vcard xs1, x1⟩ ∉∘ xs1" 
    using mem_not_refl r1.vfsequence_vdomain by blast
  have nxs2: "⟨vcard xs2, x2⟩ ∉∘ xs2" 
    using mem_not_refl r2.vfsequence_vdomain by blast
  have xsx1_xsx2: "⟨vcard xs1, x1⟩ = ⟨vcard xs2, x2⟩" 
    unfolding vcons_eq_vcard_eq[OF assms(1)] ‹x1 = x2› by simp
  
  show "xs1 = xs2"
  proof(rule vinsert_identD[OF _ nxs1])
    from assms(1)[unfolded vcons_def] show 
      "vinsert ⟨vcard xs1, x1⟩ xs1 = vinsert ⟨vcard xs1, x1⟩ xs2"
      by (auto simp: xsx1_xsx2)
    show "⟨vcard xs1, x1⟩ ∉∘ xs2"
      by (rule nxs2[folded ‹x1 = x2› vcons_eq_vcard_eq[OF assms(1)]])
  qed

qed

lemma vcons_eqI:
  assumes "xs1 = xs2" and "x1 = x2"
  shows "xs1 #∘ x1 = xs2 #∘ x2"
  using assms by (rule arg_cong2)

lemma vcons_eq_iff[simp]: "(xs1 #∘ x1 = xs2 #∘ x2) ⟷ (xs1 = xs2 ∧ x1 = x2)" 
  by auto

end


text‹Alternative forms of existing results.›

context
  fixes xs1 xs2
  assumes xs1: "vfsequence xs1"
    and xs2: "vfsequence xs2"
begin

lemmas_with[OF vfsequence_pair.intro[OF xs1 xs2]]:
  vcons_eqD' = vfsequence_pair.vcons_eqD
  and vcons_eq_iff[intro, simp] = vfsequence_pair.vcons_eq_iff

end

lemmas vcons_eqD[dest] = vcons_eqD'[rotated -1]



subsection‹Transfer between the type typ‹V list› and finite sequences›


subsubsection‹Initialization›

primrec vfsequence_of_vlist :: "V list ⇒ V"
  where 
    "vfsequence_of_vlist [] = 0"
  | "vfsequence_of_vlist (x # xs) = vfsequence_of_vlist xs #∘ x"

definition vlist_of_vfsequence :: "V ⇒ V list"
  where "vlist_of_vfsequence = inv_into UNIV vfsequence_of_vlist"

lemma vfsequence_vfsequence_of_vlist: "vfsequence (vfsequence_of_vlist xs)"
  by (induction xs) auto

lemma inj_vfsequence_of_vlist: "inj vfsequence_of_vlist"
proof
  show "vfsequence_of_vlist x = vfsequence_of_vlist y ⟹ x = y" 
    for x y
  proof(induction y arbitrary: x)
    case Nil then show ?case by (cases x) auto
  next
    case (Cons a ys)
    note Cons' = Cons
    show ?case 
    proof(cases x)
      case Nil with Cons show ?thesis by auto
    next
      case (Cons b zs)
      from Cons'[unfolded Cons vfsequence_of_vlist.simps] have 
        "vfsequence_of_vlist zs #∘ b = vfsequence_of_vlist ys #∘ a"
        by simp
      then have "vfsequence_of_vlist zs = vfsequence_of_vlist ys" and "b = a"
        by (auto simp: vfsequence_vfsequence_of_vlist)
      from Cons'(1)[OF this(1)] this(2) show ?thesis unfolding Cons by auto
    qed
  qed
qed

lemma range_vfsequence_of_vlist: 
  "range vfsequence_of_vlist = {xs. vfsequence xs}"
proof(intro subset_antisym subsetI; unfold mem_Collect_eq)
  show "xs ∈ range vfsequence_of_vlist ⟹ vfsequence xs" for xs
    by (clarsimp simp: vfsequence_vfsequence_of_vlist)
  fix xs assume "vfsequence xs"
  then show "xs ∈ range vfsequence_of_vlist"
  proof(induction rule: vfsequence_induct)
    case 0 then show ?case 
      by (metis image_iff iso_tuple_UNIV_I vfsequence_of_vlist.simps(1))
  next
    case (vcons xs x) then show ?case 
      by (metis rangeE rangeI vfsequence_of_vlist.simps(2))
  qed 
qed

lemma vlist_of_vfsequence_vfsequence_of_vlist[simp]: 
  "vlist_of_vfsequence (vfsequence_of_vlist xs) = xs"
  by (simp add: inj_vfsequence_of_vlist vlist_of_vfsequence_def)

lemma (in vfsequence) vfsequence_of_vlist_vlist_of_vfsequence[simp]: 
  "vfsequence_of_vlist (vlist_of_vfsequence xs) = xs"
  using vfsequence_axioms range_vfsequence_of_vlist inj_vfsequence_of_vlist
  by (simp add: f_inv_into_f vlist_of_vfsequence_def)

lemmas vfsequence_of_vlist_vlist_of_vfsequence[intro, simp] =
  vfsequence.vfsequence_of_vlist_vlist_of_vfsequence

lemma vlist_of_vfsequence_vempty[simp]: "vlist_of_vfsequence []∘ = []"
  by 
    (
      metis 
        vfsequence_of_vlist.simps(1) 
        vlist_of_vfsequence_vfsequence_of_vlist
    )


text‹Transfer relation 1.›

definition cr_vfsequence :: "V ⇒ V list ⇒ bool"
  where "cr_vfsequence a b ⟷ (a = vfsequence_of_vlist b)"

lemma cr_vfsequence_right_total[transfer_rule]: "right_total cr_vfsequence"
  unfolding cr_vfsequence_def right_total_def by simp

lemma cr_vfsequence_bi_unqie[transfer_rule]: "bi_unique cr_vfsequence"
  unfolding cr_vfsequence_def bi_unique_def
  by (simp add: inj_eq inj_vfsequence_of_vlist)

lemma cr_vfsequence_transfer_domain_rule[transfer_domain_rule]: 
  "Domainp cr_vfsequence = (λxs. vfsequence xs)"
  unfolding cr_vfsequence_def
proof(intro HOL.ext, rule iffI)
  fix xs assume prems: "vfsequence xs"
  interpret vfsequence xs by (rule prems)
  have "∃ys. xs = vfsequence_of_vlist ys"
    using prems
  proof(induction rule: vfsequence_induct)
    show "⟦ vfsequence xs; ∃ys. xs = vfsequence_of_vlist ys ⟧ ⟹
      ∃ys. xs #∘ x = vfsequence_of_vlist ys"
      for xs x
      unfolding vfsequence_of_vlist_def by (metis list.simps(7))
  qed auto 
  then show "Domainp (λa b. a = vfsequence_of_vlist b) xs" by auto
qed (clarsimp simp: vfsequence_vfsequence_of_vlist)

lemma cr_vfsequence_vconsD:
  assumes "cr_vfsequence (xs #∘ x) (y # ys)" 
  shows "cr_vfsequence xs ys" and "x = y"
proof-
  from assms[unfolded cr_vfsequence_def] have xs_x_def: 
    "xs #∘ x = vfsequence_of_vlist (y # ys)" .
  then have xs_x: "vfsequence (xs #∘ x)" 
    by (simp add: vfsequence_vfsequence_of_vlist)
  interpret vfsequence xs
    by (blast intro: vfsequence.vfsequence_vremove_vcons_vfsequence xs_x)
  from 
    assms[unfolded cr_vfsequence_def vfsequence_of_vlist.simps(2)]
    vfsequence_axioms 
  show "cr_vfsequence xs ys" and "x = y"
    unfolding cr_vfsequence_def by (auto simp: vfsequence_vfsequence_of_vlist)
qed


text‹Transfer relation 2.›

definition cr_cr_vfsequence :: "V ⇒ V list list ⇒ bool"
  where "cr_cr_vfsequence a b ⟷ 
    (a = vfsequence_of_vlist (map vfsequence_of_vlist b))"

lemma cr_cr_vfsequence_right_total[transfer_rule]: 
  "right_total cr_cr_vfsequence"
  unfolding cr_cr_vfsequence_def right_total_def by simp

lemma cr_cr_vfsequence_bi_unqie[transfer_rule]: "bi_unique cr_cr_vfsequence"
  unfolding cr_cr_vfsequence_def bi_unique_def
  by (simp add: inj_eq inj_vfsequence_of_vlist)


text‹Transfer relation for scalars.›

definition cr_scalar :: "(V ⇒ 'a ⇒ bool) ⇒ V ⇒ 'a ⇒ bool"
  where "cr_scalar R x y = (∃a. x = [a]∘ ∧ R a y)"

lemma cr_scalar_bi_unique[transfer_rule]:
  assumes "bi_unique R"
  shows "bi_unique (cr_scalar R)"
  using assms unfolding cr_scalar_def bi_unique_def by auto

lemma cr_scalar_right_total[transfer_rule]:
  assumes "right_total R"
  shows "right_total (cr_scalar R)"
  using assms unfolding cr_scalar_def right_total_def by simp

lemma cr_scalar_transfer_domain_rule[transfer_domain_rule]: 
  "Domainp (cr_scalar R) = (λx. ∃a. x = [a]∘ ∧ Domainp R a)"
  unfolding cr_scalar_def by auto


subsubsection‹Transfer rules for previously defined entities›

context 
  includes lifting_syntax
begin

lemma vfsequence_vempty_transfer[transfer_rule]: "cr_vfsequence []∘ []"
  unfolding cr_vfsequence_def by simp

lemma vfsequence_vempty_ll_transfer[transfer_rule]: 
  "cr_cr_vfsequence [[]∘]∘ [[]]"
  unfolding cr_cr_vfsequence_def by simp

lemma vcons_transfer[transfer_rule]:
  "((=) ===> cr_vfsequence ===> cr_vfsequence) (λx xs. xs #∘ x) (λx xs. x # xs)"
  by (intro rel_funI) (simp add: cr_vfsequence_def)

lemma vcons_ll_transfer[transfer_rule]:
  "(cr_vfsequence ===> cr_cr_vfsequence ===> cr_cr_vfsequence) 
    (λx xs. xs #∘ x) (λx xs. x # xs)"
  by (intro rel_funI) (simp add: cr_vfsequence_def cr_cr_vfsequence_def)

lemma vfsequence_vrange_transfer[transfer_rule]:
  "(cr_vfsequence ===> (=)) (λxs. elts (ℛ∘ xs)) list.set"
proof(intro rel_funI)
  fix xs ys assume prems: "cr_vfsequence xs ys"
  then have "xs = vfsequence_of_vlist ys" unfolding cr_vfsequence_def by simp
  then have "vfsequence xs" by (simp add: vfsequence_vfsequence_of_vlist)
  from this prems show "elts (ℛ∘ xs) = list.set ys"
  proof(induction ys arbitrary: xs)
    case (Cons a ys)
    from Cons(2) show ?case 
    proof(cases xs rule: vfsequence_cases)
      case 0 with Cons show ?thesis by (simp add: Cons.IH cr_vfsequence_def)
    next
      case (vcons xs' x)
      interpret vfsequence xs' by (rule vcons(2))
      note vcons_transfer = cr_vfsequence_vconsD[OF Cons(3)[unfolded vcons(1)]]
      have a_ys: "list.set (a # ys) = insert a (list.set ys)" by simp
      from vcons(2) have R_xs'x: "ℛ∘ (xs' #∘ x) = vinsert x (ℛ∘ xs')" by simp
      show "elts (ℛ∘ xs) = (list.set (a # ys))"
        unfolding vcons(1) R_xs'x a_ys
        by 
          (
            auto simp: 
              vcons_transfer(2) Cons(1)[OF vfsequence_axioms vcons_transfer(1)]
          )
    qed
  qed (auto simp: cr_vfsequence_def)
qed

lemma vcard_transfer[transfer_rule]: 
  "(cr_vfsequence ===> cr_omega) vcard length"
proof(intro rel_funI)
  fix xs ys assume prems: "cr_vfsequence xs ys"
  then have "xs = vfsequence_of_vlist ys" unfolding cr_vfsequence_def by simp
  then have "vfsequence xs" by (simp add: vfsequence_vfsequence_of_vlist)
  from this prems show "cr_omega (vcard xs) (length ys)"
  proof(induction ys arbitrary: xs)
    case (Cons y ys)
    from Cons(2) show ?case 
    proof(cases xs rule: vfsequence_cases)
      case 0 with Cons show ?thesis by (simp add: Cons.IH cr_vfsequence_def)
    next
      case (vcons xs' x)
      interpret vfsequence xs' by (rule vcons(2))
      note vcons_transfer = cr_vfsequence_vconsD[OF Cons(3)[unfolded vcons(1)]]
      have vcard_xs_x: "vcard (xs' #∘ x) = succ (vcard xs')" by simp
      have vcard_y_ys: "length (y # ys) = Suc (length ys)" by simp
      from vfsequence_axioms have [transfer_rule]: 
        "cr_omega (vcard xs') (length ys)"
        by (simp add: vcons_transfer(1) Cons.IH)
      show ?thesis unfolding vcons(1) vcard_xs_x vcard_y_ys by transfer_prover
    qed
  qed (auto simp: cr_omega_def cr_vfsequence_def)
qed

lemma vcard_ll_transfer[transfer_rule]: 
  "(cr_cr_vfsequence ===> cr_omega) vcard length"
  unfolding cr_cr_vfsequence_def
  by (intro rel_funI)
    (metis cr_vfsequence_def length_map rel_funD vcard_transfer)

end


text‹Corollaries.›

lemma vdomain_vfsequence_of_vlist: "𝒟∘ (vfsequence_of_vlist xs) = length xs"
proof-
  define ys where "ys = vfsequence_of_vlist xs"
  interpret vfsequence ys
    unfolding ys_def by (rule vfsequence_vfsequence_of_vlist)
  have [transfer_rule]: "cr_vfsequence ys xs"  
    unfolding ys_def cr_vfsequence_def by simp_all
  show ?thesis
    by (fold ys_def, unfold vfsequence_vdomain, transfer) simp
qed

lemma vrange_vfsequence_of_vlist: 
  "ℛ∘ (vfsequence_of_vlist xs) = set (list.set xs)"
proof(intro vsubset_antisym vsubsetI)
  fix x assume prems: "x ∈∘ ℛ∘ (vfsequence_of_vlist xs)" 
  define ys where "ys = vfsequence_of_vlist xs"
  have [transfer_rule]: "cr_vfsequence ys xs" "x = x" 
    unfolding ys_def cr_vfsequence_def by simp_all
  show "x ∈∘ set (list.set xs)" by transfer (simp add: prems[folded ys_def])
next
  fix x assume prems: "x ∈∘ set (list.set xs)"
  define ys where "ys = vfsequence_of_vlist xs"
  have [transfer_rule]: "cr_vfsequence ys xs" "x = x" 
    unfolding ys_def cr_vfsequence_def by simp_all
  from prems[untransferred] show "x ∈∘ ℛ∘ (vfsequence_of_vlist xs)"
    unfolding ys_def by simp
qed

lemma cr_cr_vfsequence_transfer_domain_rule[transfer_domain_rule]: 
  "Domainp cr_cr_vfsequence = 
    (λxss. vfsequence xss ∧ (∀xs∈∘ℛ∘ xss. vfsequence xs))"
proof(intro HOL.ext, rule iffI; (elim conjE | intro conjI ballI))
  fix xss assume prems: "Domainp cr_cr_vfsequence xss"
  with vfsequence_vfsequence_of_vlist show xss: "vfsequence xss"
    unfolding cr_cr_vfsequence_def by clarsimp
  interpret vfsequence xss by (rule xss)
  fix xs assume prems': "xs ∈∘ ℛ∘ xss"
  from prems obtain yss where xss_def: 
    "xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)"
    unfolding cr_cr_vfsequence_def by clarsimp
  from prems' have "xs ∈∘ set (list.set (map vfsequence_of_vlist yss))"
    unfolding xss_def vrange_vfsequence_of_vlist by simp
  then obtain ys where xs_def: "xs = vfsequence_of_vlist ys" by clarsimp
  show "vfsequence xs"
    unfolding xs_def by (simp add: vfsequence_vfsequence_of_vlist)
next
  fix xss assume prems: "vfsequence xss" "∀xs∈∘ℛ∘ xss. vfsequence xs"
  have "∃yss. xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)"
    using prems
  proof(induction rule: vfsequence_induct)
    case (vcons xss x)
    let ?y = ‹vlist_of_vfsequence x›
    from vcons(2,3) obtain yss where xss_def: 
      "xss = vfsequence_of_vlist (map vfsequence_of_vlist yss)"
      by auto
    from vcons(3) have "vfsequence x" by auto
    then have x_def: "x = vfsequence_of_vlist (vlist_of_vfsequence x)" by simp
    then have 
      "xss #∘ x = vfsequence_of_vlist (map vfsequence_of_vlist (?y # yss))"
      unfolding xss_def by simp
    then show ?case by blast
  qed (auto intro: exI[of _ ‹[]›])
  then show "Domainp cr_cr_vfsequence xss" 
    unfolding cr_cr_vfsequence_def by blast
qed


subsubsection‹Appending elements›

definition vappend :: "V ⇒ V ⇒ V" (infixr ‹@∘› 65)
  where "xs @∘ ys =
    vfsequence_of_vlist (vlist_of_vfsequence ys @ vlist_of_vfsequence xs)"


text‹Transfer.›

lemma vappend_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vfsequence ===> cr_vfsequence ===> cr_vfsequence) 
    (λxs ys. vappend ys xs) append"
  by (intro rel_funI, unfold cr_vfsequence_def) (simp add: vappend_def)

lemma vappend_ll_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_cr_vfsequence ===> cr_cr_vfsequence ===> cr_cr_vfsequence) 
    (λxs ys. vappend ys xs) append"
  by (intro rel_funI, unfold cr_cr_vfsequence_def) (simp add: vappend_def)


text‹Elementary properties.›

lemma (in vfsequence) vfsequence_vappend_vempty_vfsequence[simp]: 
  "[]∘ @∘ xs = xs"
  unfolding vappend_def by auto

lemmas vfsequence_vappend_vempty_vfsequence[simp] =
  vfsequence.vfsequence_vappend_vempty_vfsequence

lemma (in vfsequence) vfsequence_vappend_vfsequence_vempty[simp]:
  "xs @∘ []∘ = xs"
  unfolding vappend_def by auto

lemmas vfsequence_vappend_vfsequence_vempty[simp] =
  vfsequence.vfsequence_vappend_vfsequence_vempty

lemma vappend_vcons[simp]: 
  assumes "vfsequence xs" and "vfsequence ys"
  shows "xs @∘ (ys #∘ y) = (xs @∘ ys) #∘ y"
  using append_Cons[where 'a=V, untransferred, OF assms(2,1)] by simp


subsubsection‹Distinct elements›

definition vdistinct :: "V ⇒ bool"
  where "vdistinct xs = distinct (vlist_of_vfsequence xs)"


text‹Transfer.›

lemma vdistinct_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vfsequence ===> (=)) vdistinct distinct"
  by (intro rel_funI, unfold cr_vfsequence_def) (simp add: vdistinct_def)

lemma vdistinct_ll_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_cr_vfsequence ===> (=)) vdistinct distinct" 
  by (intro rel_funI, unfold cr_cr_vfsequence_def)
    (
      metis 
        vdistinct_def 
        distinct_map 
        inj_onI 
        vlist_of_vfsequence_vfsequence_of_vlist
    )


text‹Elementary properties.›

lemma (in vfsequence) vfsequence_vdistinct_if_vcard_vrange_eq_vcard:
  assumes "vcard (ℛ∘ xs) = vcard xs"
  shows "vdistinct xs"
proof-
  have "finite (elts (ℛ∘ xs))" by (simp add: assms vcard_vfinite_omega)
  from vcard_finite_set[OF this] assms have "card (elts (ℛ∘ xs))ℕ = vcard xs"
    by simp
  from card_distinct[where ?'a=V, untransferred, OF vfsequence_axioms this] 
  show ?thesis.
qed

lemma vdistinct_vempty[intro, simp]: "vdistinct []∘"
proof-
  have t: "distinct ([]::V list)" by simp
  show ?thesis by (rule t[untransferred])
qed

lemma (in vfsequence) vfsequence_vcons_vdistinct:
  assumes "vdistinct (xs #∘ x)" 
  shows "vdistinct xs"
proof-
  from distinct.simps(2)[where 'a=V, THEN iffD1, THEN conjunct2, untransferred]
  show ?thesis
    using vfsequence_axioms assms by simp
qed

lemma (in vfsequence) vfsequence_vcons_nin_vrange:
  assumes "vdistinct (xs #∘ x)" 
  shows "x ∉∘ ℛ∘ xs"
proof-
  from distinct.simps(2)[where 'a=V, THEN iffD1, THEN conjunct1, untransferred]
  show ?thesis
    using vfsequence_axioms assms by simp
qed

lemma (in vfsequence) vfsequence_v11I[intro]:
  assumes "vdistinct xs"
  shows "v11 xs"
  using vfsequence_axioms assms
proof(induction xs rule: vfsequence_induct)
  case (vcons xs x)
  interpret vfsequence xs by (rule vcons(1))
  from vcons(3) have dxs: "vdistinct xs" by (rule vfsequence_vcons_vdistinct)
  interpret v11 xs using dxs by (rule vcons(2))
  from vfsequence_vcons_nin_vrange[OF vcons(3)] have "x ∉∘ ℛ∘ xs" .
  show "v11 (xs #∘ x)"
    by  
      ( 
        simp_all add: 
          vcons_def vfsequence_vdomain vfsequence_vcons_nin_vrange[OF vcons(3)]
      )
qed simp

lemma (in vfsequence) vfsequence_vcons_vdistinctI:
  assumes "vdistinct xs" and "x ∉∘ ℛ∘ xs"
  shows "vdistinct (xs #∘ x)"
proof-
  have t: "distinct xs ⟹ x ∉ list.set xs ⟹ distinct (x # xs)" 
    for x ::V and xs 
    by simp
  from vfsequence_axioms assms show ?thesis by (rule t[untransferred])
qed

lemmas vfsequence_vcons_vdistinctI[intro] =
  vfsequence.vfsequence_vcons_vdistinctI 

lemma (in vfsequence) vfsequence_nin_vrange_vcons:
  assumes "y ∉∘ ℛ∘ xs" and "y ≠ x"
  shows "y ∉∘ ℛ∘ (xs #∘ x)"
proof-
  have t: "y ∉ list.set xs ⟹ y ≠ x ⟹ y ∉ list.set (x # xs)" 
    for x y :: V and xs
    by simp
  from vfsequence_axioms assms show ?thesis by (rule t[untransferred])
qed

lemmas vfsequence_nin_vrange_vcons[intro] = 
  vfsequence.vfsequence_nin_vrange_vcons


subsubsection‹Concatenation of sequences›

definition vconcat :: "V ⇒ V"
  where "vconcat xss =
    vfsequence_of_vlist(
      concat (map vlist_of_vfsequence (vlist_of_vfsequence xss))
    )"


text‹Transfer.›

lemma vconcat_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_cr_vfsequence ===> cr_vfsequence) vconcat concat"
proof(intro rel_funI)
  fix xs ys assume "cr_cr_vfsequence xs ys"
  then have xs_def: "xs = vfsequence_of_vlist (map vfsequence_of_vlist ys)"
    unfolding cr_cr_vfsequence_def by simp
  have main_eq: "map vlist_of_vfsequence (vlist_of_vfsequence xs) = ys"
    unfolding xs_def by (simp add: map_idI)
  show "cr_vfsequence (vconcat xs) (concat ys)"
    unfolding cr_vfsequence_def vconcat_def main_eq ..
qed


text‹Elementary properties.›

lemma vconcat_vempty[simp]: "vconcat []∘ = []∘"
  unfolding vconcat_def by simp

lemma vconcat_append[simp]: 
  assumes "vfsequence xss" 
    and "∀xs∈∘ℛ∘ xss. vfsequence xs" 
    and "vfsequence yss"
    and "∀xs∈∘ℛ∘ yss. vfsequence xs" 
  shows "vconcat (xss @∘ yss) = vconcat xss @∘ vconcat yss"
  using assms concat_append[where 'a=V, untransferred] by simp

lemma vconcat_vcons[simp]: 
  assumes "vfsequence xs" and "vfsequence xss" and "∀xs∈∘ℛ∘ xss. vfsequence xs"
  shows "vconcat (xss #∘ xs) = vconcat xss @∘ xs"
  using assms concat.simps(2)[where 'a=V, untransferred] by simp

lemma (in vfsequence) vfsequence_vconcat_fsingleton[simp]: "vconcat [xs]∘ = xs"
  using vfsequence_axioms 
  by 
    (
      metis 
        vfsequence_vappend_vempty_vfsequence 
        vconcat_vcons 
        vconcat_vempty 
        vempty_nin 
        vfsequence_vempty 
        vrange_vempty
    )

lemmas vfsequence_vconcat_fsingleton[simp] = 
  vfsequence.vfsequence_vconcat_fsingleton



subsection‹Finite sequences and the Cartesian product›

lemma vfsequence_vcons_vproductI[intro!]:
  assumes "n ∈∘ ω" 
    and "xs ∈∘ (∏∘i∈∘vcard xs. A i)" 
    and "x ∈∘ A (vcard xs)" 
    and "n = vcard (xs #∘ x)"
  shows "xs #∘ x ∈∘ (∏∘i∈∘n. A i)"
proof
  interpret xs: vfsequence xs 
    using assms
    apply(intro vfsequenceI)
    subgoal by auto
    subgoal
      by 
        (
          metis 
            vcard_vfinite_omega 
            vcons_vsubset 
            vfinite_vcard_omega 
            vfinite_vsubset vproductD(2)
        )
    done
  interpret xsx: vfsequence ‹xs #∘ x› by auto
  show "vsv (xs #∘ x)" by (simp add: xsx.vsv_axioms)
  show D: "𝒟∘ (xs #∘ x) = n" unfolding assms(4) xsx.vfsequence_vdomain by auto
  from vproductD[OF assms(2)] have elem: "i ∈∘ vcard xs ⟹ xs⦇i⦈ ∈∘ A i" for i
    by auto
  show "∀i∈∘n. (xs #∘ x)⦇i⦈ ∈∘ A i" by (auto simp: elem assms(3,4))
qed

lemma vfsequence_vcons_vproductD[dest]:
  assumes "xs #∘ x ∈∘ (∏∘i∈∘n. A i)" and "n ∈∘ ω"
  shows "xs ∈∘ (∏∘i∈∘vcard xs. A i)" 
    and "x ∈∘ A (vcard xs)" 
    and "n = vcard (xs #∘ x)" 
proof-

  interpret xsx: vfsequence ‹xs #∘ x› 
    by (meson assms succ_in_omega vfsequence_vproduct)
  interpret xs: vfsequence xs
    by (blast intro: xsx.vfsequence_vremove_vcons_vfsequence)

  show n_def: "n = vcard (xs #∘ x)"
    using assms using xsx.vfsequence_vdomain by blast
  from vproductD[OF assms(1), unfolded n_def] 
  have elem_xs_x: "i ∈∘ vcard (xs #∘ x) ⟹ (xs #∘ x)⦇i⦈ ∈∘ A i" 
    for i
    by auto
  then have elem_xs[simp]: "i ∈∘ vcard xs ⟹ xs⦇i⦈ ∈∘ A i" for i
    by (metis rev_vsubsetD vcard_mono vcons_vsubset xs.vfsequence_at_not_last)
  show "xs ∈∘ (∏∘i∈∘vcard xs. A i)"
    by (auto simp: xs.vsv_axioms xs.vfsequence_vdomain)
  from elem_xs_x show "x ∈∘ A (vcard xs)" by fastforce

qed

lemma vfsequence_vcons_vproductE[elim!]:
  assumes "xs #∘ x ∈∘ (∏∘i∈∘n. A i)" and "n ∈∘ ω"
  obtains "xs ∈∘ (∏∘i∈∘vcard xs. A i)" 
    and "x ∈∘ A (vcard xs)" 
    and "n = vcard (xs #∘ x)" 
  using assms by (auto simp: vfsequence_vcons_vproductD)



subsection‹Binary Cartesian product based on finite sequences: ‹ftimes››

definition ftimes :: "V ⇒ V ⇒ V" (infixr ‹×∙› 80)
  where "ftimes a b ≡ (∏∘i∈∘2ℕ. if i = 0 then a else b)"

lemma small_fpairs[simp]: "small {[a, b]∘ | a b. [a, b]∘ ∈∘ r}"
  by (rule down[of _ r]) clarsimp


text‹Rules.›

lemma ftimesI1[intro]: 
  assumes "x = [a, b]∘" and "a ∈∘ A" and "b ∈∘ B"
  shows "x ∈∘ A ×∙ B"
  unfolding ftimes_def
proof
  show vsv: "vsv x" by (simp add: assms(1) vfsequence.axioms(1))
  then interpret vsv x .
  from assms show D: "𝒟∘ x = 2ℕ" 
    unfolding nat_omega_simps two One_nat_def by auto
  from assms(2,3) have i: "i ∈∘ 2ℕ ⟹ x⦇i⦈ ∈∘ (if i = 0ℕ then A else B)" 
    for i
    unfolding assms(1) two nat_omega_simps One_nat_def by auto
  from i show "∀i∈∘2ℕ. x⦇i⦈ ∈∘ (if i = 0 then A else B)" by auto
qed

lemma ftimesI2[intro!]: 
  assumes "a ∈∘ A" and "b ∈∘ B"
  shows "[a, b]∘ ∈∘ A ×∙ B"
  using assms ftimesI1 by auto

lemma fproductE1[elim!]:
  assumes "x ∈∘ A ×∙ B"
  obtains a b where "x = [a, b]∘" and "a ∈∘ A" and "b ∈∘ B"
proof-
  from vproduct_vdoubletonD[OF assms[unfolded two ftimes_def]] 
  have x_def: "x = set {⟨0ℕ, x⦇0ℕ⦈⟩, ⟨1ℕ, x⦇1ℕ⦈⟩}"
    and "x⦇0ℕ⦈ ∈∘ A" 
    and "x⦇1ℕ⦈ ∈∘ B" 
    by auto
  then show ?thesis using that using vcons_vdoubleton by simp
qed

lemma fproductE2[elim!]:
  assumes "[a, b]∘ ∈∘ A ×∙ B" obtains "a ∈∘ A" and "b ∈∘ B"
  using assms by blast


text‹Set operations.›

lemma vfinite_0_left[simp]: "0 ×∙ b = 0"
  by (meson eq0_iff fproductE1)

lemma vfinite_0_right[simp]: "a ×∙ 0 = 0"
  by (meson eq0_iff fproductE1)

lemma fproduct_vintersection: "(a ∩∘ b) ×∙ (c ∩∘ d) = (a ×∙ c) ∩∘ (b ×∙ d)"
  by auto

lemma fproduct_vdiff: "a ×∙ (b -∘ c) = (a ×∙ b) -∘ (a ×∙ c)" by auto

lemma vfinite_ftimesI[intro!]:
  assumes "vfinite a" and "vfinite b"
  shows "vfinite (a ×∙ b)"
  using assms(1,2) 
proof(induction arbitrary: b rule: vfinite_induct)
  case (vinsert x a')
  from vinsert(4) have "vfinite (set {x} ×∙ b)"
  proof(induction rule: vfinite_induct)
    case (vinsert y b')
    have "set {x} ×∙ vinsert y b' = vinsert [x, y]∘ (set {x} ×∙ b')" by auto
    with vinsert(3) show ?case by simp
  qed simp
  moreover have "vinsert x a' ×∙ b = (set {x} ×∙ b) ∪∘ (a' ×∙ b)" by auto
  ultimately show ?case using vinsert by (auto simp: vfinite_vunionI)
qed simp


text‹‹ftimes› and ‹vcpower››

lemma vproduct_vpair: "[a, b]∘ ∈∘ (∏∘i∈∘2ℕ. f i) ⟷ ⟨a, b⟩ ∈∘ f (0ℕ) ×∘ f (1ℕ)"
proof
  interpret vfsequence ‹[a, b]∘› by simp
  show "[a, b]∘ ∈∘ (∏∘i∈∘2ℕ. f i) ⟹ ⟨a, b⟩ ∈∘ f (0ℕ) ×∘ f (1ℕ)"
    unfolding vcons_vdoubleton two by (elim vproduct_vdoubletonE) auto
  assume hyp: "⟨a, b⟩ ∈∘ f (0ℕ) ×∘ f (1ℕ)" 
  then have af: "a ∈∘ f (0ℕ)" and bf: "b ∈∘ f (1ℕ)" by auto
  have dom: "𝒟∘ [a, b]∘ = set {0ℕ, 1ℕ}" by (auto intro!: vsubset_antisym)
  have ran: "ℛ∘ [a, b]∘ ⊆∘ (⋃∘i∈∘2ℕ. f i)"
    unfolding two using af bf vifunion_vdoubleton by auto  
  show "[a, b]∘ ∈∘ (∏∘i∈∘2ℕ. f i)"
    apply(intro vproductI)
    subgoal using dom ran vsv_axioms unfolding two by auto
    subgoal using af bf unfolding two by (auto intro!: vsubset_antisym)
    subgoal 
      unfolding two 
      using hyp VSigmaE2 small_empty vcons_vdoubleton 
      by (auto simp: vinsert_set_insert_eq)
    done
qed


text‹Connections.›

lemma vcpower_two_ftimes: "A ^× 2ℕ = A ×∙ A" 
  unfolding vcpower_def ftimes_def two by simp

lemma vcpower_two_ftimesI[intro]: 
  assumes "x ∈∘ A ×∙ A"
  shows "x ∈∘ A ^× 2ℕ"
  using assms unfolding ftimes_def two by auto

lemma vcpower_two_ftimesD[dest]:
  assumes "x ∈∘ A ^× 2ℕ"
  shows "x ∈∘ A ×∙ A"
  using assms unfolding vcpower_def ftimes_def two by simp

lemma vcpower_two_ftimesE[elim]:
  assumes "x ∈∘ A ^× 2ℕ" and "x ∈∘ A ×∙ A ⟹ P"
  shows P
  using assms unfolding vcpower_def ftimes_def two by simp

lemma vfsequence_vcpower_two_vpair: "[a, b]∘ ∈∘ A ^× 2ℕ ⟷ ⟨a, b⟩ ∈∘ A ×∘ A"
proof(rule iffI)
  show "[a, b]∘ ∈∘ A ^× 2ℕ ⟹ ⟨a, b⟩ ∈∘ A ×∘ A"
    by (elim vcpowerE, unfold vproduct_vpair) 
qed (intro vcpowerI, unfold vproduct_vpair)

lemma vsv_vfsequence_two: 
  assumes "vsv gf" and "𝒟∘ gf = 2ℕ"
  shows "[vpfst gf, vpsnd gf]∘ = gf"
proof-
  interpret gf: vsv gf by (auto intro: assms(1))
  show ?thesis
    by
      (
        rule sym,
        rule vsv_eqI, 
        blast, 
        blast, 
        simp add: assms(2) nat_omega_simps,
        unfold assms(2),
        elim_in_numeral,
        all‹simp add: nat_omega_simps›
      )
qed

lemma vsv_vfsequence_three: 
  assumes "vsv hgf" and "𝒟∘ hgf = 3ℕ"
  shows "[vpfst hgf, vpsnd hgf, vpthrd hgf]∘ = hgf"
proof-
  interpret hgf: vsv hgf by (auto intro: assms(1))
  show ?thesis
    by
      (
        rule sym,
        rule vsv_eqI, 
        blast, 
        blast, 
        simp add: assms(2) nat_omega_simps,
        unfold assms(2),
        elim_in_numeral,
        all‹simp add: nat_omega_simps›
      )
qed



subsection‹Sequence as an element of a Cartesian power of a set›

lemma vcons_in_vcpowerI[intro!]: 
  assumes "n ∈∘ ω" 
    and "xs ∈∘ A ^× vcard xs" 
    and "x ∈∘ A" 
    and "n = vcard (xs #∘ x)" 
  shows "xs #∘ x ∈∘ A ^× n"
proof-
  interpret vfsequence xs
    using assms
    by
      (
        meson 
          vcons_vsubset 
          vfinite_vcard_omega_iff 
          vfinite_vsubset 
          vfsequence_vcpower
      )
  show ?thesis 
    by 
      (
        metis 
          assms(2,3,4)
          vcpower_vrange 
          vfsequence_vcons 
          vfsequence_vcons_vrange 
          vfsequence.vfsequence_vrange_vcpower 
          vsubset_vinsert_leftI
      )
qed

lemma vcons_in_vcpowerD[dest]: 
  assumes "xs #∘ x ∈∘ A ^× n" and "n ∈∘ ω"
  shows "xs ∈∘ A ^× vcard xs" 
    and "x ∈∘ A" 
    and "n = vcard (xs #∘ x)" 
proof-
  interpret vfsequence xs 
    by 
      (
        meson 
          assms 
          vfsequence.vfsequence_vremove_vcons_vfsequence 
          vfsequence_vcpower
      )
  from assms vfsequence_vcard_vcons show "n = vcard (xs #∘ x)" by auto
  then show "xs ∈∘ A ^× vcard xs" 
    by 
      (
        metis 
          assms(1) 
          vcpower_vrange 
          vfsequence_vcons_vrange 
          vfsequence_vrange_vcpower 
          vsubset_vinsert_leftD
      )
  show "x ∈∘ A"
    by 
      (
        metis 
          assms(1) 
          vcpower_vrange 
          vfsequence.vfsequence_vcons_vrange 
          vfsequence_axioms 
          vinsertI1 
          vsubsetE
      )
qed

lemma vcons_in_vcpowerE1[elim!]: 
  assumes "xs #∘ x ∈∘ A ^× n" and "n ∈∘ ω"
  obtains "xs ∈∘ A ^× vcard xs" and "x ∈∘ A" and "n = vcard (xs #∘ x)" 
  using assms by blast

lemma vcons_in_vcpowerE2: 
  assumes "xs ∈∘ A ^× n" and "n ∈∘ ω" and "0 ∈∘ n"
  obtains x xs' where "xs = xs' #∘ x"
    and "xs' ∈∘ A ^× vcard xs'" 
    and "x ∈∘ A" 
    and "n = vcard (xs' #∘ x)" 
proof-
  interpret vfsequence xs using assms(1,2) by auto
  from assms obtain x xs' where xs_def: "xs = xs' #∘ x"
    by 
      (
        metis 
          eq0_iff vcard_0 vcpower_vdomain vfsequence_vcons_ex vfsequence_vdomain
      )
  from vcons_in_vcpowerE1[OF assms(1)[unfolded xs_def] assms(2)] have
    "xs' ∈∘ A ^× vcard xs'" and "x ∈∘ A" and "n = vcard (xs' #∘ x)" 
    by blast+
  from xs_def this show ?thesis by (clarsimp simp: that)
qed

lemma vcons_vcpower1E: (*TODO: generalize*)
  assumes "xs ∈∘ A ^× 1ℕ"  
  obtains x where "xs = [x]∘" and "x ∈∘ A"
proof-
  have 01: "0 ∈∘ 1ℕ" by simp
  from vcons_in_vcpowerE2[OF assms ord_of_nat_ω 01] obtain x xs' 
    where xs_def: "xs = xs' #∘ x"
      and xs': "xs' ∈∘ A ^× vcard xs'" 
      and x: "x ∈∘ A" 
      and one: "1ℕ = vcard (xs' #∘ x)" 
    by metis
  interpret xs: vfsequence xs using assms by (auto intro: vfsequence_vcpower)
  interpret xs': vfsequence xs' 
    using xs' xs_def xs.vfsequence_vremove_vcons_vfsequence by blast
  from one have "vcard xs' = 0" 
    by (metis ord_of_nat_succ_vempty succ_inject_iff xs'.vfsequence_vcard_vcons)
  then have "xs = [x]∘" unfolding xs_def by (simp add: vcard_vempty)
  with x that show ?thesis by simp
qed



subsection‹The set of all finite sequences on a set›


subsubsection‹Definition and elementary properties›

definition vfsequences_on :: "V ⇒ V"
  where "vfsequences_on X = set {x. vfsequence x ∧ (∀i∈∘𝒟∘ x. x⦇i⦈ ∈∘ X)}"

lemma vfsequences_on_subset_ω_set:
  "{x. vfsequence x ∧ (∀i∈elts (𝒟∘ x). x⦇i⦈ ∈∘ X)} ⊆ elts (VPow (ω ×∘ X))"
proof
  (
    intro subsetI, 
    unfold mem_Collect_eq VPow_iff, 
    elim conjE, 
    intro vsubsetI
  )
  fix xs nx
  assume prems[rule_format]: 
    "vfsequence xs"
    "∀i∈∘𝒟∘ xs. xs⦇i⦈ ∈∘ X"
    "nx ∈∘ xs"
  interpret vfsequence xs by (rule prems(1))
  from prems(3) vbrelation obtain n x where nx_def: "nx = ⟨n, x⟩" by auto
  from vsv_appI[OF prems(3)[unfolded this]] have xsn: "xs⦇n⦈ = x" . 
  from prems(3) nx_def have "n ∈∘ 𝒟∘ xs" by auto
  with prems(2) show "nx ∈∘ ω ×∘ X"
    by (auto simp: nx_def xsn[symmetric] Ord_trans vfsequence_vdomain_in_omega)
qed

lemma small_vfsequences_on[simp]: 
  "small {x. vfsequence x ∧ (∀i∈∘𝒟∘ x. x⦇i⦈ ∈∘ X)}"
  by (rule down, rule vfsequences_on_subset_ω_set)


text‹Rules.›

lemma vfsequences_onI:
  assumes "vfsequence xs" and "⋀i. i ∈∘ 𝒟∘ xs ⟹ xs⦇i⦈ ∈∘ X"
  shows "xs ∈∘ vfsequences_on X"
  using assms unfolding vfsequences_on_def by simp

lemma vfsequences_onD[dest]:
  assumes "xs ∈∘ vfsequences_on X"
  shows "vfsequence xs" and "⋀i. i ∈∘ 𝒟∘ xs ⟹ xs⦇i⦈ ∈∘ X"
  using assms unfolding vfsequences_on_def by auto

lemma vfsequences_onE[elim]:
  assumes "xs ∈∘ vfsequences_on X"
  obtains "vfsequence xs" and "⋀i. i ∈∘ 𝒟∘ xs ⟹ xs⦇i⦈ ∈∘ X"
  using assms unfolding vfsequences_on_def by auto


subsubsection‹Further properties›

lemma vfsequences_on_vsubset_mono: 
  assumes "A ⊆∘ B "
  shows "vfsequences_on A ⊆∘ vfsequences_on B"
proof(intro vsubsetI vfsequences_onI; elim vfsequences_onE)
  fix i xs assume prems: "i ∈∘ 𝒟∘ xs" "⋀i. i ∈∘ 𝒟∘ xs ⟹ xs⦇i⦈ ∈∘ A"
  from assms prems(2)[OF prems(1)] show "xs⦇i⦈ ∈∘ B" by auto
qed

text‹\newpage›

end