Theory Option_Extra

theory Option_Extra
  imports Main
begin

fun ap_option (infixl "⋄" 60) where
  "(Some f) ⋄ (Some x) = Some (f x)" |
  "_ ⋄ _ = None"

lemma ap_option_eq_Some_conv: "f ⋄ x = Some y ⟷ (∃f' x'. f = Some f' ∧ x = Some x' ∧ y = f' x')"
  by (cases f; simp; cases x; auto)

definition ap_map_prod where
  "ap_map_prod f g p ≡ Some Pair ⋄ f (fst p) ⋄ g (snd p)"

lemma ap_map_prod_eq_Some_conv:
  "ap_map_prod f g p = Some p' ⟷ (∃x y. p = (x, y) ∧ (∃x' y'. p' = (x', y') ∧ f x = Some x' ∧ g y = Some y'))"
proof (cases p)
  case (Pair x y)
  then show ?thesis
    unfolding ap_map_prod_def
    by (auto simp add: ap_map_prod_def ap_option_eq_Some_conv)
qed

fun ap_map_list :: "('a ⇒ 'b option) ⇒ 'a list ⇒ 'b list option" where
  "ap_map_list _ [] = Some []" |
  "ap_map_list f (x # xs) = Some (#) ⋄ f x ⋄ ap_map_list f xs"

lemma length_ap_map_list: "ap_map_list f xs = Some ys ⟹ length ys = length xs"
  by (induction xs arbitrary: ys) (auto simp add: ap_option_eq_Some_conv)

lemma ap_map_list_imp_rel_option_map_of:
  assumes "ap_map_list f xs = Some ys" and
    "⋀x y. (x, y) ∈ set (zip xs ys) ⟹ f x = Some y ⟹ fst x = fst y"
  shows "rel_option (λx y. f (k, x) = Some (k, y)) (map_of xs k) (map_of ys k)"
  using assms
proof (induction xs arbitrary: ys)
  case Nil
  thus ?case by simp
next
  case (Cons x xs)
  from Cons.prems show ?case
    apply (auto simp add: ap_option_eq_Some_conv option_rel_Some1 elim!: Cons.IH)
      apply (metis prod.collapse)
     apply (metis prod.collapse)
    by blast
qed

lemma ap_map_list_ap_map_prod_imp_rel_option_map_of:
  assumes "ap_map_list (ap_map_prod Some f) xs = Some ys"
  shows "rel_option (λx y. f x = Some y) (map_of xs k) (map_of ys k)"
  using assms
proof (induction xs arbitrary: ys)
  case Nil
  thus ?case by simp
next
  case (Cons x xs)
  from Cons.prems show ?case
    by (auto simp: ap_option_eq_Some_conv ap_map_prod_eq_Some_conv elim: Cons.IH[simplified])
qed

lemma ex_ap_map_list_eq_SomeI:
  assumes "list_all (λx. ∃y. f x = Some y) xs"
  shows "∃ys. ap_map_list f xs = Some ys"
  using assms
  by (induction xs) auto

lemma ap_map_list_iff_list_all2:
  "ap_map_list f xs = Some ys ⟷ list_all2 (λx y. f x = Some y) xs ys"
proof (rule iffI)
  show "ap_map_list f xs = Some ys ⟹ list_all2 (λx y. f x = Some y) xs ys"
    by (induction xs arbitrary: ys) (auto simp: ap_option_eq_Some_conv)
next
  show "list_all2 (λx y. f x = Some y) xs ys ⟹ ap_map_list f xs = Some ys"
    by (induction xs ys rule: list.rel_induct) auto
qed

lemma ap_map_list_map_conv:
  assumes
    "ap_map_list f xs = Some ys" and
    "⋀x y. x ∈ set xs ⟹ f x = Some y ⟹ y = g x"
  shows "ys = map g xs"
  using assms
  by (induction xs arbitrary: ys) (auto simp: ap_option_eq_Some_conv)

end