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(Justa) = TT" |
  "isJustNothing = FF"

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

fixrec fromJust :: "'a Maybe  'a" where
  "fromJust(Justa) = a" |
  "fromJustNothing = "

fixrec fromMaybe :: "'a  'a Maybe  'a" where
  "fromMaybedNothing = d" |
  "fromMaybed(Justa) = a"

fixrec maybeToList :: "'a Maybe  ['a]" where
  "maybeToListNothing = []" |
  "maybeToList(Justa) = [a]"

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

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

fixrec mapMaybe :: "('a  'b Maybe)  ['a]  ['b]" where
  "mapMaybef = catMaybes oo mapf"

instantiation Maybe :: (Eq) Eq_strict
begin

definition
  "eq = maybe(maybeTT(Λ y. FF))(Λ x. maybeFF(Λ y. eqxy))"

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

end

lemma eq_Maybe_simps [simp]:
  "eqNothingNothing = TT"
  "eqNothing(Justy) = FF"
  "eq(Justx)Nothing = FF"
  "eq(Justx)(Justy) = eqxy"
  unfolding eq_Maybe_def by simp_all

instance Maybe :: (Eq_sym) Eq_sym
proof
  fix x y :: "'a Maybe"
  show "eqxy = eqyx"
    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 "eqxx  FF"
    by (cases x, simp_all)
  assume "eqxy = TT" and "eqyz = TT" then show "eqxz = 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 "eqxx  FF"
    by (cases x, simp_all)
  assume "eqxy = 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(maybeEQ(Λ y. LT))(Λ x. maybeGT(Λ y. comparexy))"

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

end

lemma compare_Maybe_simps [simp]:
  "compareNothingNothing = EQ"
  "compareNothing(Justy) = LT"
  "compare(Justx)Nothing = GT"
  "compare(Justx)(Justy) = comparexy"
  unfolding compare_Maybe_def by simp_all

instance Maybe :: (Ord_linear) Ord_linear
proof
  fix x y z :: "'a Maybe"
  show "eqxy = is_EQ(comparexy)"
    by (cases x, simp, cases y, simp, simp, simp,
        cases y, simp, simp, simp add: eq_conv_compare)
  show "oppOrdering(comparexy) = compareyx"
    by (cases x, simp, (cases y, simp, simp, simp)+)
  show "comparexx  EQ"
    by (cases x) simp_all
  show "x = y" if "comparexy = EQ"
    using that
    by (cases x, simp, cases y, simp, simp, simp,
        cases y, simp, simp, simp) (erule compare_EQ_dest)
  show "comparexz = LT" if "comparexy = LT" and "compareyz = 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]: "fromMaybex  = " by (fixrec_simp)
lemma maybeToList_strict [simp]: "maybeToList  = " by (fixrec_simp)

end