# Theory Sequence_Zip

```section ‹Zipping Sequences›

theory Sequence_Zip
imports "Sequence_LTL"
begin

subsection ‹Zipping Lists›

notation zip (infixr "||" 51)

lemmas [simp] = zip_map_fst_snd

lemma split_zip[no_atp]: "(⋀ x. PROP P x) ≡ (⋀ y z. length y = length z ⟹ PROP P (y || z))"
proof
fix y z
assume 1: "⋀ x. PROP P x"
show "PROP P (y || z)" using 1 by this
next
fix x :: "('a × 'b) list"
assume 1: "⋀ y z. length y = length z ⟹ PROP P (y || z)"
have 2: "length (map fst x) = length (map snd x)" by simp
have 3: "PROP P (map fst x || map snd x)" using 1 2 by this
show "PROP P x" using 3 by simp
qed
lemma split_zip_all[no_atp]: "(∀ x. P x) ⟷ (∀ y z. length y = length z ⟶ P (y || z))"
by (fastforce iff: split_zip)
lemma split_zip_ex[no_atp]: "(∃ x. P x) ⟷ (∃ y z. length y = length z ∧ P (y || z))"
by (fastforce iff: split_zip)

lemma zip_eq[iff]:
assumes "length u = length v" "length r = length s"
shows "u || v = r || s ⟷ u = r ∧ v = s"
using assms zip_eq_conv by metis

lemma list_rel_pred_zip: "list_all2 P xs ys ⟷ length xs = length ys ∧ list_all (case_prod P) (xs || ys)"
unfolding list_all2_conv_all_nth list_all_length by auto

lemma list_choice_zip: "list_all (λ x. ∃ y. P x y) xs ⟷
(∃ ys. length ys = length xs ∧ list_all (case_prod P) (xs || ys))"
unfolding list_choice list_rel_pred_zip by metis
lemma list_choice_pair: "list_all (λ xy. case_prod (λ x y. ∃ z. P x y z) xy) (xs || ys) ⟷
(∃ zs. length zs = min (length xs) (length ys) ∧ list_all (λ (x, y, z). P x y z) (xs || ys || zs))"
proof -
have 1: "list_all (λ (xy, z). case xy of (x, y) ⇒ P x y z) ((xs || ys) || zs) ⟷
list_all (λ (x, y, z). P x y z) (xs || ys || zs)" for zs
unfolding zip_assoc list.pred_map by (auto intro!: list.pred_cong)
have 2: "(λ (x, y). ∃ z. P x y z) = (λ xy. ∃ z. case xy of (x, y) ⇒ P x y z)" by auto
show ?thesis unfolding list_choice_zip 1 2 by force
qed

lemma list_rel_zip[iff]:
assumes "length u = length v" "length r = length s"
shows "list_all2 (rel_prod A B) (u || v) (r || s) ⟷ list_all2 A u r ∧ list_all2 B v s"
proof safe
assume [transfer_rule]: "list_all2 (rel_prod A B) (u || v) (r || s)"
have "list_all2 A (map fst (u || v)) (map fst (r || s))" by transfer_prover
then show "list_all2 A u r" using assms by simp
have "list_all2 B (map snd (u || v)) (map snd (r || s))" by transfer_prover
then show "list_all2 B v s" using assms by simp
next
assume [transfer_rule]: "list_all2 A u r" "list_all2 B v s"
show "list_all2 (rel_prod A B) (u || v) (r || s)" by transfer_prover
qed

lemma zip_last[simp]:
assumes "xs || ys ≠ []" "length xs = length ys"
shows "last (xs || ys) = (last xs, last ys)"
proof -
have 1: "xs ≠ []" "ys ≠ []" using assms(1) by auto
have "last (xs || ys) = (xs || ys) ! (length (xs || ys) - 1)" using last_conv_nth assms by blast
also have "… = (xs ! (length (xs || ys) - 1), ys ! (length (xs || ys) - 1))" using assms 1 by simp
also have "… = (xs ! (length xs - 1), ys ! (length ys - 1))" using assms(2) by simp
also have "… = (last xs, last ys)" using last_conv_nth 1 by metis
finally show ?thesis by this
qed

subsection ‹Zipping Streams›

notation szip (infixr "|||" 51)

lemmas [simp] = szip_unfold

lemma smap_szip_same: "smap f (xs ||| xs) = smap (λ x. f (x, x)) xs" by (coinduction arbitrary: xs) (auto)

lemma szip_smap[simp]: "smap fst zs ||| smap snd zs = zs" by (coinduction arbitrary: zs) (auto)
lemma szip_smap_fst[simp]: "smap fst (xs ||| ys) = xs" by (coinduction arbitrary: xs ys) (auto)
lemma szip_smap_snd[simp]: "smap snd (xs ||| ys) = ys" by (coinduction arbitrary: xs ys) (auto)

lemma szip_smap_both: "smap f xs ||| smap g ys = smap (map_prod f g) (xs ||| ys)" by (coinduction arbitrary: xs ys) (auto)
lemma szip_smap_left: "smap f xs ||| ys = smap (apfst f) (xs ||| ys)" by (coinduction arbitrary: xs ys) (auto)
lemma szip_smap_right: "xs ||| smap f ys = smap (apsnd f) (xs ||| ys)" by (coinduction arbitrary: xs ys) (auto)
lemmas szip_smap_fold = szip_smap_both szip_smap_left szip_smap_right

lemma szip_sconst_smap_fst: "sconst a ||| xs = smap (Pair a) xs"
by (coinduction arbitrary: xs) (auto)
lemma szip_sconst_smap_snd: "xs ||| sconst a = smap (prod.swap ∘ Pair a) xs"
by (coinduction arbitrary: xs) (auto)

lemma split_szip[no_atp]: "(⋀ x. PROP P x) ≡ (⋀ y z. PROP P (y ||| z))"
proof
fix y z
assume 1: "⋀ x. PROP P x"
show "PROP P (y ||| z)" using 1 by this
next
fix x
assume 1: "⋀ y z. PROP P (y ||| z)"
have 2: "PROP P (smap fst x ||| smap snd x)" using 1 by this
show "PROP P x" using 2 by simp
qed
lemma split_szip_all[no_atp]: "(∀ x. P x) ⟷ (∀ y z. P (y ||| z))" by (fastforce iff: split_szip)
lemma split_szip_ex[no_atp]: "(∃ x. P x) ⟷ (∃ y z. P (y ||| z))" by (fastforce iff: split_szip)

lemma szip_eq[iff]: "u ||| v = r ||| s ⟷ u = r ∧ v = s"
using szip_smap_fst szip_smap_snd by metis

lemma stream_rel_szip[iff]:
"stream_all2 (rel_prod A B) (u ||| v) (r ||| s) ⟷ stream_all2 A u r ∧ stream_all2 B v s"
proof safe
assume [transfer_rule]: "stream_all2 (rel_prod A B) (u ||| v) (r ||| s)"
have "stream_all2 A (smap fst (u ||| v)) (smap fst (r ||| s))" by transfer_prover
then show "stream_all2 A u r" by simp
have "stream_all2 B (smap snd (u ||| v)) (smap snd (r ||| s))" by transfer_prover
then show "stream_all2 B v s" by simp
next
assume [transfer_rule]: "stream_all2 A u r" "stream_all2 B v s"
show "stream_all2 (rel_prod A B) (u ||| v) (r ||| s)" by transfer_prover
qed

lemma szip_shift[simp]:
assumes "length u = length s"
shows "u @- v ||| s @- t = (u || s) @- (v ||| t)"
using assms by (simp add: eq_shift stake_shift sdrop_shift)

lemma szip_sset_fst[simp]: "fst ` sset (u ||| v) = sset u" by (metis stream.set_map szip_smap_fst)
lemma szip_sset_snd[simp]: "snd ` sset (u ||| v) = sset v" by (metis stream.set_map szip_smap_snd)
lemma szip_sset_elim[elim]:
assumes "(a, b) ∈ sset (u ||| v)"
obtains "a ∈ sset u" "b ∈ sset v"
using assms by (metis image_eqI fst_conv snd_conv szip_sset_fst szip_sset_snd)
lemma szip_sset[simp]: "sset (u ||| v) ⊆ sset u × sset v" by auto

lemma sset_szip_finite[iff]: "finite (sset (u ||| v)) ⟷ finite (sset u) ∧ finite (sset v)"
proof safe
assume 1: "finite (sset (u ||| v))"
have 2: "finite (fst ` sset (u ||| v))" using 1 by blast
have 3: "finite (snd ` sset (u ||| v))" using 1 by blast
show "finite (sset u)" using 2 by simp
show "finite (sset v)" using 3 by simp
next
assume 1: "finite (sset u)" "finite (sset v)"
have "sset (u ||| v) ⊆ sset u × sset v" by simp
also have "finite …" using 1 by simp
finally show "finite (sset (u ||| v))" by this
qed

lemma infs_szip_fst[iff]: "infs (P ∘ fst) (u ||| v) ⟷ infs P u"
proof -
have "infs (P ∘ fst) (u ||| v) ⟷ infs P (smap fst (u ||| v))"
by (simp add: comp_def del: szip_smap_fst)
also have "… ⟷ infs P u" by simp
finally show ?thesis by this
qed
lemma infs_szip_snd[iff]: "infs (P ∘ snd) (u ||| v) ⟷ infs P v"
proof -
have "infs (P ∘ snd) (u ||| v) ⟷ infs P (smap snd (u ||| v))"
by (simp add: comp_def del: szip_smap_snd)
also have "… ⟷ infs P v" by simp
finally show ?thesis by this
qed

end```