Theory Data_Maybe

section ‹Data: Maybe›

theory Data_Maybe
  imports
    Type_Classes
    Data_Function
    Data_List
    Data_Bool
begin

domain 'a Maybe = Nothing | Just (lazy "'a")

abbreviation maybe :: "'b → ('a → 'b) → 'a Maybe → 'b" where
  "maybe ≡ Maybe_case"

fixrec isJust :: "'a Maybe → tr" where
  "isJust⋅(Just⋅a) = TT" |
  "isJust⋅Nothing = FF"

fixrec isNothing :: "'a Maybe → tr" where
  "isNothing = neg oo isJust"

fixrec fromJust :: "'a Maybe → 'a" where
  "fromJust⋅(Just⋅a) = a" |
  "fromJust⋅Nothing = ⊥"

fixrec fromMaybe :: "'a → 'a Maybe → 'a" where
  "fromMaybe⋅d⋅Nothing = d" |
  "fromMaybe⋅d⋅(Just⋅a) = a"

fixrec maybeToList :: "'a Maybe → ['a]" where
  "maybeToList⋅Nothing = []" |
  "maybeToList⋅(Just⋅a) = [a]"

fixrec listToMaybe :: "['a] → 'a Maybe" where
  "listToMaybe⋅[] = Nothing" |
  "listToMaybe⋅(a:_) = Just⋅a"

(* FIXME: The Prelude definition uses list comps, which are too advanced for our syntax *)
fixrec catMaybes :: "['a Maybe] → ['a]" where
  "catMaybes = concatMap⋅maybeToList"

fixrec mapMaybe :: "('a → 'b Maybe) → ['a] → ['b]" where
  "mapMaybe⋅f = catMaybes oo map⋅f"

instantiation Maybe :: (Eq) Eq_strict
begin

definition
  "eq = maybe⋅(maybe⋅TT⋅(Λ y. FF))⋅(Λ x. maybe⋅FF⋅(Λ y. eq⋅x⋅y))"

instance proof
  fix x :: "'a Maybe"
  show "eq⋅x⋅⊥ = ⊥"
    unfolding eq_Maybe_def by (cases x) simp_all
  show "eq⋅⊥⋅x = ⊥"
    unfolding eq_Maybe_def by simp
qed

end

lemma eq_Maybe_simps [simp]:
  "eq⋅Nothing⋅Nothing = TT"
  "eq⋅Nothing⋅(Just⋅y) = FF"
  "eq⋅(Just⋅x)⋅Nothing = FF"
  "eq⋅(Just⋅x)⋅(Just⋅y) = eq⋅x⋅y"
  unfolding eq_Maybe_def by simp_all

instance Maybe :: (Eq_sym) Eq_sym
proof
  fix x y :: "'a Maybe"
  show "eq⋅x⋅y = eq⋅y⋅x"
    by (cases x, simp, cases y, simp, simp, simp,
        cases y, simp, simp, simp add: eq_sym)
qed

instance Maybe :: (Eq_equiv) Eq_equiv
proof
  fix x y z :: "'a Maybe"
  show "eq⋅x⋅x ≠ FF"
    by (cases x, simp_all)
  assume "eq⋅x⋅y = TT" and "eq⋅y⋅z = TT" then show "eq⋅x⋅z = TT"
    by (cases x, simp, cases y, simp, cases z, simp, simp, simp, simp,
        cases y, simp, simp, cases z, simp, simp, simp, fast elim: eq_trans)
qed

instance Maybe :: (Eq_eq) Eq_eq
proof
  fix x y :: "'a Maybe"
  show "eq⋅x⋅x ≠ FF"
    by (cases x, simp_all)
  assume "eq⋅x⋅y = TT" then show "x = y"
    by (cases x, simp, cases y, simp, simp, simp,
        cases y, simp, simp, simp, fast)
qed

instantiation Maybe :: (Ord) Ord_strict
begin

definition
  "compare = maybe⋅(maybe⋅EQ⋅(Λ y. LT))⋅(Λ x. maybe⋅GT⋅(Λ y. compare⋅x⋅y))"

instance proof
  fix x :: "'a Maybe"
  show "compare⋅x⋅⊥ = ⊥"
    unfolding compare_Maybe_def by (cases x) simp_all
  show "compare⋅⊥⋅x = ⊥"
    unfolding compare_Maybe_def by simp
qed

end

lemma compare_Maybe_simps [simp]:
  "compare⋅Nothing⋅Nothing = EQ"
  "compare⋅Nothing⋅(Just⋅y) = LT"
  "compare⋅(Just⋅x)⋅Nothing = GT"
  "compare⋅(Just⋅x)⋅(Just⋅y) = compare⋅x⋅y"
  unfolding compare_Maybe_def by simp_all

instance Maybe :: (Ord_linear) Ord_linear
proof
  fix x y z :: "'a Maybe"
  show "eq⋅x⋅y = is_EQ⋅(compare⋅x⋅y)"
    by (cases x, simp, cases y, simp, simp, simp,
        cases y, simp, simp, simp add: eq_conv_compare)
  show "oppOrdering⋅(compare⋅x⋅y) = compare⋅y⋅x"
    by (cases x, simp, (cases y, simp, simp, simp)+)
  show "compare⋅x⋅x ⊑ EQ"
    by (cases x) simp_all
  show "x = y" if "compare⋅x⋅y = EQ"
    using that
    by (cases x, simp, cases y, simp, simp, simp,
        cases y, simp, simp, simp) (erule compare_EQ_dest)
  show "compare⋅x⋅z = LT" if "compare⋅x⋅y = LT" and "compare⋅y⋅z = LT"
    using that
    apply (cases x, simp)
     apply (cases y, simp, simp)
     apply (cases z, simp, simp, simp)
    apply (cases y, simp, simp)
    apply (cases z, simp, simp)
    apply (auto elim: compare_LT_trans)
    done
qed

lemma isJust_strict [simp]: "isJust⋅⊥  = ⊥" by (fixrec_simp)
lemma fromMaybe_strict [simp]: "fromMaybe⋅x⋅⊥  = ⊥" by (fixrec_simp)
lemma maybeToList_strict [simp]: "maybeToList⋅⊥  = ⊥" by (fixrec_simp)

end