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