(* 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 = r⇩_{1}: vfsequence xs⇩_{1}+ r⇩_{2}: vfsequence xs⇩_{2}for xs⇩_{1}xs⇩_{2}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) 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 "xs⇩_{1}#⇩_{∘}x⇩_{1}= xs⇩_{2}#⇩_{∘}x⇩_{2}" shows "vcard xs⇩_{1}= vcard xs⇩_{2}" by ( metis assms succ_inject_iff vfsequence.vfsequence_vcons_vdomain r⇩_{1}.vfsequence_axioms r⇩_{2}.vfsequence_axioms ) lemma vcons_eqD[dest]: assumes "xs⇩_{1}#⇩_{∘}x⇩_{1}= xs⇩_{2}#⇩_{∘}x⇩_{2}" shows "xs⇩_{1}= xs⇩_{2}" and "x⇩_{1}= x⇩_{2}" proof- have xsx1_last: "(xs⇩_{1}#⇩_{∘}x⇩_{1})⦇vcard xs⇩_{1}⦈ = x⇩_{1}" by simp have xsx2_last: "(xs⇩_{2}#⇩_{∘}x⇩_{2})⦇vcard xs⇩_{2}⦈ = x⇩_{2}" by simp from assms have vcard: "vcard xs⇩_{1}= vcard xs⇩_{2}" by (rule vcons_eq_vcard_eq) from trans[OF xsx1_last xsx1_last[unfolded vcard assms, symmetric]] show "x⇩_{1}= x⇩_{2}" unfolding xsx1_last xsx2_last . have nxs1: "⟨vcard xs⇩_{1}, x⇩_{1}⟩ ∉⇩_{∘}xs⇩_{1}" using mem_not_refl r⇩_{1}.vfsequence_vdomain by blast have nxs2: "⟨vcard xs⇩_{2}, x⇩_{2}⟩ ∉⇩_{∘}xs⇩_{2}" using mem_not_refl r⇩_{2}.vfsequence_vdomain by blast have xsx1_xsx2: "⟨vcard xs⇩_{1}, x⇩_{1}⟩ = ⟨vcard xs⇩_{2}, x⇩_{2}⟩" unfolding vcons_eq_vcard_eq[OF assms(1)] ‹x⇩_{1}= x⇩_{2}› by simp show "xs⇩_{1}= xs⇩_{2}" proof(rule vinsert_identD[OF _ nxs1]) from assms(1)[unfolded vcons_def] show "vinsert ⟨vcard xs⇩_{1}, x⇩_{1}⟩ xs⇩_{1}= vinsert ⟨vcard xs⇩_{1}, x⇩_{1}⟩ xs⇩_{2}" by (auto simp: xsx1_xsx2) show "⟨vcard xs⇩_{1}, x⇩_{1}⟩ ∉⇩_{∘}xs⇩_{2}" by (rule nxs2[folded ‹x⇩_{1}= x⇩_{2}› vcons_eq_vcard_eq[OF assms(1)]]) qed qed lemma vcons_eqI: assumes "xs⇩_{1}= xs⇩_{2}" and "x⇩_{1}= x⇩_{2}" shows "xs⇩_{1}#⇩_{∘}x⇩_{1}= xs⇩_{2}#⇩_{∘}x⇩_{2}" using assms by (rule arg_cong2) lemma vcons_eq_iff[simp]: "(xs⇩_{1}#⇩_{∘}x⇩_{1}= xs⇩_{2}#⇩_{∘}x⇩_{2}) ⟷ (xs⇩_{1}= xs⇩_{2}∧ x⇩_{1}= x⇩_{2})" by auto end text‹Alternative forms of existing results.› context fixes xs⇩_{1}xs⇩_{2}assumes xs⇩_{1}: "vfsequence xs⇩_{1}" and xs⇩_{2}: "vfsequence xs⇩_{2}" begin lemmas_with[OF vfsequence_pair.intro[OF xs⇩_{1}xs⇩_{2}]]: 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