Theory List_Extra

theory List_Extra
  imports Main "HOL-Library.Quotient_List"
begin

text ‹
  This theory contains some extra lemmas that were useful in proving some lemmas in
  🗏‹Modular_Splitting_Calculus.thy› and 🗏‹Lightweight_Avatar.thy›.
›

lemma map2_first_is_first [simp]: ‹length x = length y ⟹ map2 (λ x y. x) x y = x›
  by (metis fst_def map_eq_conv map_fst_zip)

lemma map2_second_is_second [simp]: ‹length A = length B ⟹ map2 (λ x y. y) A B = B›
  by (metis map_eq_conv map_snd_zip snd_def)

lemma list_all_exists_is_exists_list_all2:
  assumes ‹list_all (λ x. ∃ y. P x y) xs›
  shows ‹∃ ys. list_all2 P xs ys›
  using assms
  by (induct xs, auto)

lemma ball_set_f_to_ball_set_map: ‹(∀ x ∈ set A. P (f x)) ⟷ (∀ x ∈ set (map f A). P x)›
  by simp

lemma list_all_ex_to_ex_list_all2:
  ‹list_all (λ x. ∃ y. P x y) A ⟷ (∃ ys. length A = length ys ∧ list_all2 (λ x y. P x y) A ys)›
  by (metis list_all2_conv_all_nth list_all_exists_is_exists_list_all2 list_all_length)

lemma list_all2_to_map:
  assumes lengths_eq: ‹length A = length B›
  shows ‹list_all2 (λ x y. P (f x y)) A B ⟷ list_all P (map2 f A B)›
proof -
  have ‹list_all2 (λ x y. P (f x y)) A B ⟷ list_all (λ (x, y). P (f x y)) (zip A B)›
    by (simp add: lengths_eq list_all2_iff list_all_iff)
  also have ‹... ⟷ list_all (λ x. P x) (map2 f A B)›
    by (simp add: case_prod_beta list_all_iff)
  finally show ?thesis .
qed

(*<*)
(*! All these could belong in the ‹List› theory, although these definitions lack a few lemmas
 *  which aren't useful in our case.
 *  Note that it would be better to remove calls to the ‹smt› method as these take a bit long. *)
primrec zip3 :: ‹'a list ⇒ 'b list ⇒ 'c list ⇒ ('a × 'b × 'c) list› where
  ‹zip3 xs ys [] = []›
  | ‹zip3 xs ys (z # zs) =
  (case xs of [] ⇒ [] | x # xs ⇒
  (case ys of [] ⇒ [] | y # ys ⇒ (x, y, z) # zip3 xs ys zs))›

abbreviation map3 :: ‹('a ⇒ 'b ⇒ 'c ⇒ 'd) ⇒ 'a list ⇒ 'b list ⇒ 'c list ⇒ 'd list› where
  ‹map3 f xs ys zs ≡ map (λ(x, y, z). f x y z) (zip3 xs ys zs)› 

fun list_all3 :: ‹('a ⇒ 'b ⇒ 'c ⇒ bool) ⇒ 'a list ⇒ 'b list ⇒ 'c list ⇒ bool› where
  ‹list_all3 p [] [] [] = HOL.True›
| ‹list_all3 p (x # xs) (y # ys) (z # zs) = (p x y z ∧ list_all3 p xs ys zs)›
| ‹list_all3 _ _ _ _ = False› 

lemma list_all3_length_eq1: ‹list_all3 P xs ys zs ⟹ length xs = length ys›
  by (induction P xs ys zs rule: list_all3.induct, auto)

lemma list_all3_length_eq2: ‹list_all3 P xs ys zs ⟹ length ys = length zs›
  by (induction P xs ys zs rule: list_all3.induct, auto) 

lemma list_all3_length_eq3: ‹list_all3 P xs ys zs ⟹ length xs = length zs›
  using list_all3_length_eq1 list_all3_length_eq2
  by fastforce 

lemma list_all2_ex_to_ex_list_all3:
  ‹list_all2 (λ x y. ∃ z. P x y z) xs ys ⟷ (∃ zs. list_all3 P xs ys zs)›
proof (intro iffI)
  assume ‹list_all2 (λ x y. ∃ z. P x y z) xs ys›
  then show ‹∃ zs. list_all3 P xs ys zs›
    by (induct xs ys; metis list_all3.simps(1) list_all3.simps(2))
next
  assume ‹∃ zs. list_all3 P xs ys zs›
  then obtain zs where
    all3_xs_ys_zs: ‹list_all3 P xs ys zs› 
    by blast
  then show ‹list_all2 (λ x y. ∃ z. P x y z) xs ys›
    using all3_xs_ys_zs
    by (induction P xs ys zs rule: list_all3.induct, auto)
qed 

lemma list_all3_conj_distrib: ‹list_all3 (λ x y z. P x y z ∧ Q x y z) xs ys zs ⟷
  list_all3 P xs ys zs ∧ list_all3 Q xs ys zs›
  by (induction ‹λ x y z. P x y z ∧ Q x y z› xs ys zs rule: list_all3.induct, auto)

lemma list_all3_conv_list_all_3: ‹list_all3 (λ x y z. P z) xs ys zs ⟹ list_all P zs›
proof -
  assume ‹list_all3 (λ x y z. P z) xs ys zs› (is ‹list_all3 ?P xs ys zs›)
  then show ‹list_all P zs› 
    by (induction ?P xs ys zs rule: list_all3.induct, auto)
qed

lemma list_all3_reorder:
  ‹list_all3 (λ x y z. P x y z) xs ys zs ⟷ list_all3 (λ x z y. P x y z) xs zs ys›
  by (induction ‹λ x y z. P x y z› xs ys zs rule: list_all3.induct, auto)

lemma list_all3_reorder2:
  ‹list_all3 (λ x y z. P x y z) xs ys zs ⟷ list_all3 (λ y z x. P x y z) ys zs xs›
  by (induction ‹λ x y z. P x y z› xs ys zs rule: list_all3.induct, auto)

lemma list_all2_conj_distrib:
  ‹list_all2 (λ x y. P x y ∧ Q x y) A B ⟷ list_all2 P A B ∧ list_all2 Q A B›
  by (smt (verit, ccfv_SIG) list_all2_conv_all_nth)

(* This lemma depends on "HOL-Library.Quotient_List" in its proof. *)
lemma list_all_bex_ex_list_all2_conv:
  ‹list.list_all (λ x. ∃ y ∈ ys. P x y) xs ⟷ (∃ ys'. set ys' ⊆ ys ∧ list_all2 P xs ys')›
proof (intro iffI)
  assume ‹list.list_all (λ x. ∃ y ∈ ys. P x y) xs›
  then have ‹list.list_all (λ x. ∃ y. y ∈ ys ∧ P x y) xs›
    by meson 
  then have ‹∃ ys'. list_all2 (λ x y. y ∈ ys ∧ P x y) xs ys'›
    by (induct xs, auto)
  then have ‹∃ ys'. list_all2 (λ x y. y ∈ ys) xs ys' ∧ list_all2 (λ x y. P x y) xs ys'›
    using list_all2_conj_distrib
    by blast
  then have ‹∃ ys'. list.list_all (λ y. y ∈ ys) ys' ∧ list_all2 P xs ys'›
    by (metis list_all2_conv_all_nth list_all_length)
  then show ‹∃ ys'. set ys' ⊆ ys ∧ list_all2 P xs ys'›
    by (metis list.pred_set subsetI)
next
  assume ‹∃ ys'. set ys' ⊆ ys ∧ list_all2 P xs ys'›
  then show ‹list.list_all (λ x. ∃ y ∈ ys. P x y) xs›
    (* /!\ A bit slow /!\ *)
    by (smt (verit, del_insts) list.pred_set list_all2_find_element subsetD) 
qed 
(*>*)

end