Theory Examples

header {* Functor and Monad Examples *}

theory Examples
imports MonadClass
begin

subsection {* Lists *}

subsubsection {* @{text rep} instance *}

text "Lists of representable elements are representable."

consts
  list_emb :: "U list => U"
  list_proj :: "U => U list"

primrec
  "list_emb [] = Utag 0 []"
  "list_emb (x # xs) = Utag 1 [x, list_emb xs]"

recdef list_proj "measure size"
  "list_proj (Utag 0 []) = []"
  "list_proj (Utag (Suc 0) [x,y]) = x # list_proj y"

instance list :: (rep) rep_consts ..
defs (overloaded)
  emb_list_def: "emb ≡ list_emb o map emb"
  proj_list_def: "proj ≡ map proj o list_proj"

instance list :: (rep) rep
by (intro_classes, unfold emb_list_def proj_list_def, induct_tac x, simp_all)

subsubsection {* @{text functor} instance *}

datatype List = List

instance List :: tycon ..
defs (overloaded)
  monotc_List_def: "monotc (l::List itself) ≡ functor_tc map"

text "@{typ List} is in @{term functor_locale}"

defs (overloaded)
  rep_fmap_List_def:
  "rep_fmap::(U => U) => U•List => U•List
     ≡ rep_fmap_of map"

lemmas map_id = map_ident [folded id_def]
lemmas map_map = map_compose [unfolded o_def, symmetric, standard]

lemma functor_locale_List: "functor_locale TYPE(List) map"
apply (rule functor_locale.intro)
apply (rule monotc_List_def)
apply (rule rep_fmap_List_def)
apply (simp add: map_id)
apply (rule map_map)
done

instance List :: functor
apply (rule functor_locale.functor_class)
apply (rule functor_locale_List)
done

subsubsection {* @{text monad} instance *}

constdefs
  return_list :: "'a => 'a list"
  "return_list ≡ λx. [x]"

  bind_list :: "'a list => ('a => 'b list) => 'b list"
  "bind_list ≡ λxs f. concat (map f xs)"

lemma monad_fmap_list: "map f xs = bind_list xs (λx. return_list (f x))"
by (unfold bind_list_def return_list_def, induct_tac xs, simp_all)

lemma monad_left_unit_list: "bind_list (return_list x) f = f x"
by (unfold bind_list_def return_list_def, simp)

lemma monad_bind_assoc_list:
  "bind_list (bind_list xs f) g = bind_list xs (λx. bind_list (f x) g)"
by (unfold bind_list_def return_list_def, induct_tac xs, simp_all)

defs (overloaded)
  rep_return_List_def:
   "rep_return::U => U•List
     ≡ rep_return_of return_list"

  rep_bind_List_def:
   "rep_bind::U•List => (U => U•List) => U•List
     ≡ rep_bind_of bind_list"

lemma monad_locale_List:
  "monad_locale TYPE(List) map return_list bind_list"
apply (rule monad_locale.intro)
apply (rule functor_locale_List)
apply (rule monad_locale_axioms.intro)
apply (rule rep_return_List_def)
apply (rule rep_bind_List_def)
apply (rule monad_fmap_list)
apply (rule monad_left_unit_list)
apply (rule monad_bind_assoc_list)
done

instance List :: monad
apply (rule monad_locale.monad_class)
apply (rule monad_locale_List)
done


subsection {* Option type *}

subsubsection {* @{text rep} instance *}

text "Options of representable elements are representable"

consts emb_option :: "'a::rep option => U"
primrec
  "emb_option None     = Utag 0 []"
  "emb_option (Some x) = Utag 1 [emb x]"

lemma inj_emb_option: "inj emb_option"
 apply (simp add: inj_on_def)
 apply (rule allI, induct_tac x)
  apply (rule allI, case_tac y, simp, simp)
 apply (rule allI, case_tac y, simp, simp)
done

instance option :: (rep) rep_consts ..
defs (overloaded)
  option_emb_def: "emb ≡ emb_option"
  option_proj_def: "proj ≡ inv emb_option"

instance option :: (rep) rep
 apply (intro_classes, unfold option_emb_def option_proj_def)
 apply (rule inv_f_f, rule inj_emb_option)
done

subsubsection {* @{text functor} instance *}

datatype Option = Option

instance Option :: tycon ..
defs (overloaded)
  Option_monotc_def: "monotc (l::Option itself) ≡ functor_tc option_map"

text "@{typ Option} is in @{term functor_locale}"

defs (overloaded)
  Option_rep_fmap_def:
  "rep_fmap::(U => U) => U•Option => U•Option
     ≡ rep_fmap_of option_map"

lemma functor_locale_Option: "functor_locale TYPE(Option) option_map"
apply (rule functor_locale.intro)
apply (rule Option_monotc_def)
apply (rule Option_rep_fmap_def)
apply (case_tac xs, simp, simp)
apply (simp add: option_map_comp o_def)
done

instance Option :: functor
apply (rule functor_locale.functor_class)
apply (rule functor_locale_Option)
done

subsubsection {* @{text monad} instance *}

defs (overloaded)
  Option_rep_return_def:
   "rep_return::U => U•Option
     ≡ rep_return_of Some"

  Option_rep_bind_def:
   "rep_bind::U•Option => (U => U•Option) => U•Option
     ≡ rep_bind_of (λm k. option_case None k m)"

lemma monad_locale_Option:
  "monad_locale TYPE(Option) option_map Some (λm k. option_case None k m)"
apply (rule monad_locale.intro)
apply (rule functor_locale_Option)
apply (rule monad_locale_axioms.intro)
apply (rule Option_rep_return_def)
apply (rule Option_rep_bind_def)
apply (simp split: option.split)
apply simp
apply (simp split: option.split)
done

instance Option :: monad
apply (rule monad_locale.monad_class)
apply (rule monad_locale_Option)
done


subsection {* Trivial type constructor *}

subsubsection {* @{text functor} instance *}

datatype Trivial = Trivial

instance Trivial :: tycon ..
defs (overloaded)
  Trivial_monotc_def: "monotc (l::Trivial itself) ≡ functor_tc (λf xs. ())"

text "@{typ Trivial} is in @{term functor_locale}"

defs (overloaded)
  Trivial_rep_fmap_def:
  "rep_fmap::(U => U) => U•Trivial => U•Trivial
     ≡ rep_fmap_of (λf xs. ())"

lemma functor_locale_Trivial: "functor_locale TYPE(Trivial) (λf xs. ())"
apply (rule functor_locale.intro)
apply (rule Trivial_monotc_def)
apply (rule Trivial_rep_fmap_def)
apply simp
apply simp
done

instance Trivial :: functor
apply (rule functor_locale.functor_class)
apply (rule functor_locale_Trivial)
done

subsubsection {* @{text monad} instance *}

defs (overloaded)
  Trivial_rep_return_def:
   "rep_return::U => U•Trivial
     ≡ rep_return_of (λx. ())"

  Trivial_rep_bind_def:
   "rep_bind::U•Trivial => (U => U•Trivial) => U•Trivial
     ≡ rep_bind_of (λm k. ())"

lemma monad_locale_Trivial:
  "monad_locale TYPE(Trivial) (λf xs. ()) (λx. ()) (λm k. ())"
apply (rule monad_locale.intro)
apply (rule functor_locale_Trivial)
apply (rule monad_locale_axioms.intro)
apply (rule Trivial_rep_return_def)
apply (rule Trivial_rep_bind_def)
apply simp
apply simp
apply simp
done

instance Trivial :: monad
apply (rule monad_locale.monad_class)
apply (rule monad_locale_Trivial)
done

end