Theory Applicative_Option

(* Author: Joshua Schneider, ETH Zurich *)

subsection ‹Option›

theory Applicative_Option imports
  Applicative
  "HOL-Library.Adhoc_Overloading"
begin

fun ap_option :: "('a ⇒ 'b) option ⇒ 'a option ⇒ 'b option"
where
    "ap_option (Some f) (Some x) = Some (f x)"
  | "ap_option _ _ = None"

abbreviation (input) pure_option :: "'a ⇒ 'a option"
where "pure_option ≡ Some"

adhoc_overloading Applicative.pure pure_option
adhoc_overloading Applicative.ap ap_option

lemma some_ap_option: "ap_option (Some f) x = map_option f x"
by (cases x) simp_all

lemma ap_some_option: "ap_option f (Some x) = map_option (λg. g x) f"
by (cases f) simp_all

lemma ap_option_transfer[transfer_rule]:
  "rel_fun (rel_option (rel_fun A B)) (rel_fun (rel_option A) (rel_option B)) ap_option ap_option"
by(auto elim!: option.rel_cases simp add: rel_fun_def)

applicative option (C, W)
for
  pure: Some
  ap: ap_option
  rel: rel_option
  set: set_option
proof -
  include applicative_syntax
  { fix x :: "'a option"
    show "pure (λx. x) ⋄ x = x" by (cases x) simp_all
  next
    fix g :: "('b ⇒ 'c) option" and f :: "('a ⇒ 'b) option" and x
    show "pure (λg f x. g (f x)) ⋄ g ⋄ f ⋄ x = g ⋄ (f ⋄ x)"
      by (cases g f x rule: option.exhaust[case_product option.exhaust, case_product option.exhaust]) simp_all
  next
    fix f :: "('b ⇒ 'a ⇒ 'c) option" and x y
    show "pure (λf x y. f y x) ⋄ f ⋄ x ⋄ y = f ⋄ y ⋄ x"
      by (cases f x y rule: option.exhaust[case_product option.exhaust, case_product option.exhaust]) simp_all
  next
    fix f :: "('a ⇒ 'a ⇒ 'b) option" and x
    show "pure (λf x. f x x) ⋄ f ⋄ x = f ⋄ x ⋄ x"
      by (cases f x rule: option.exhaust[case_product option.exhaust]) simp_all
  next
    fix R :: "'a ⇒ 'b ⇒ bool"
    show "rel_fun R (rel_option R) pure pure" by transfer_prover
  next
    fix R and f :: "('a ⇒ 'b) option" and g :: "('a ⇒ 'c) option" and x
    assume [transfer_rule]: "rel_option (rel_fun (eq_on (set_option x)) R) f g"
    have [transfer_rule]: "rel_option (eq_on (set_option x)) x x" by (auto intro: option.rel_refl_strong)
    show "rel_option R (f ⋄ x) (g ⋄ x)" by transfer_prover
  }
qed (simp add: some_ap_option ap_some_option)

lemma map_option_ap_conv[applicative_unfold]: "map_option f x = ap_option (pure f) x"
by (cases x rule: option.exhaust) simp_all

no_adhoc_overloading Applicative.pure pure_option ― ‹We do not want to print all occurrences of @{const "Some"} as @{const "pure"}›

end