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