section ‹Functor Class›

theory Functor
imports TypeApp Coerce
keywords "tycondef" :: thy_defn and "⋅"
begin

subsection ‹Class definition›

text ‹Here we define the ‹functor› class, which models the
  class \texttt{Functor}. For technical reasons, we split the
  of ‹functor› into two separate classes: First, we
  ‹prefunctor›, which only requires ‹fmap› to
  the identity function, and not function composition.›

text ‹The Haskell class \texttt{Functor f} fixes a polymorphic
  \texttt{fmap :: (a -> b) -> f a -> f b}. Since functions in
  type classes can only mention one type variable, we have the
 ‹prefunctor› class fix a function ‹fmapU› that fixes both
  the polymorphic types to be the universal domain. We will use the
  operator to recover a polymorphic ‹fmap›.›

text ‹The single axiom of the ‹prefunctor› class is stated in
  of the HOLCF constant ‹isodefl›, which relates a function
 ‹f :: 'a → 'a› with a deflation ‹t :: udom defl›:
 {thm isodefl_def [of f t, no_vars]}.›

class prefunctor = "tycon" +
  fixes fmapU :: "(udom → udom) → udom⋅'a → udom⋅'a::tycon"
  assumes isodefl_fmapU:
    "isodefl (fmapU⋅(cast⋅t)) (TC('a::tycon)⋅t)"

text ‹The ‹functor› class extends ‹prefunctor› with an
  stating that ‹fmapU› preserves composition.›

class "functor" = prefunctor +
  assumes fmapU_fmapU [coerce_simp]:
    "∧f g (xs::udom⋅'a::tycon).
      fmapU⋅f⋅(fmapU⋅g⋅xs) = fmapU⋅(Λ x. f⋅(g⋅x))⋅xs"

text ‹We define the polymorphic ‹fmap› by coercion from ‹fmapU›, then we proceed to derive the polymorphic versions of the
  laws.›

definition fmap :: "('a → 'b) → 'a⋅'f → 'b⋅'f::functor"
  where "fmap = coerce⋅(fmapU :: _ → udom⋅'f → udom⋅'f)"

subsection ‹Polymorphic functor laws›

lemma fmapU_eq_fmap: "fmapU = fmap"
by (simp add: fmap_def eta_cfun)

lemma fmap_eq_fmapU: "fmap = fmapU"
  by (simp only: fmapU_eq_fmap)

lemma cast_TC:
  "cast⋅(TC('f)⋅t) = emb oo fmapU⋅(cast⋅t) oo PRJ(udom⋅'f::prefunctor)"
by (rule isodefl_fmapU [unfolded isodefl_def])

lemma isodefl_cast: "isodefl (cast⋅t) t"
by (simp add: isodefl_def)

lemma cast_cast_below1: "A ⊑ B ==> cast⋅A⋅(cast⋅B⋅x) = cast⋅A⋅x"
by (intro deflation_below_comp1 deflation_cast monofun_cfun_arg)

lemma cast_cast_below2: "A ⊑ B ==> cast⋅B⋅(cast⋅A⋅x) = cast⋅A⋅x"
by (intro deflation_below_comp2 deflation_cast monofun_cfun_arg)

lemma isodefl_fmap:
  assumes "isodefl d t"
  shows "isodefl (fmap⋅d :: 'a⋅'f → _) (TC('f::functor)⋅t)"
proof -
  have deflation_d: "deflation d"
    using assms by (rule isodefl_imp_deflation)
  have cast_t: "cast⋅t = emb oo d oo prj"
    using assms unfolding isodefl_def .
  have t_below: "t ⊑ DEFL('a)"
    apply (rule cast_below_imp_below)
    apply (simp only: cast_t cast_DEFL)
    apply (simp add: cfun_below_iff deflation.below [OF deflation_d])
    done
  have fmap_eq: "fmap⋅d = PRJ('a⋅'f) oo cast⋅(TC('f)⋅t) oo emb"
    by (simp add: fmap_def coerce_cfun cast_TC cast_t prj_emb cfcomp1)
  show ?thesis
    apply (simp add: fmap_eq isodefl_def cfun_eq_iff emb_prj)
    apply (simp add: DEFL_app)
    apply (simp add: cast_cast_below1 monofun_cfun t_below)
    apply (simp add: cast_cast_below2 monofun_cfun t_below)
    done
qed

lemma fmap_ID [simp]: "fmap⋅ID = ID"
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_app)
apply (rule isodefl_fmap)
apply (rule isodefl_ID_DEFL)
done

lemma fmap_ident [simp]: "fmap⋅(Λ x. x) = ID"
by (simp add: ID_def [symmetric])

lemma coerce_coerce_eq_fmapU_cast [coerce_simp]:
  fixes xs :: "udom⋅'f::functor"
  shows "COERCE('a⋅'f, udom⋅'f)⋅(COERCE(udom⋅'f, 'a⋅'f)⋅xs) =
    fmapU⋅(cast⋅DEFL('a))⋅xs"
by (simp add: coerce_def emb_prj DEFL_app cast_TC)

lemma fmap_fmap:
  fixes xs :: "'a⋅'f::functor" and g :: "'a → 'b" and f :: "'b → 'c"
  shows "fmap⋅f⋅(fmap⋅g⋅xs) = fmap⋅(Λ x. f⋅(g⋅x))⋅xs"
unfolding fmap_def
by (simp add: coerce_simp)

lemma fmap_cfcomp: "fmap⋅(f oo g) = fmap⋅f oo fmap⋅g"
by (simp add: cfcomp1 fmap_fmap eta_cfun)

subsection ‹Derived properties of ‹fmap››

text ‹Other theorems about ‹fmap› can be derived using only
  abstract functor laws.›

lemma deflation_fmap:
  "deflation d ==> deflation (fmap⋅d)"
 apply (rule deflation.intro)
  apply (simp add: fmap_fmap deflation.idem eta_cfun)
 apply (subgoal_tac "fmap⋅d⋅x ⊑ fmap⋅ID⋅x", simp)
 apply (rule monofun_cfun_fun, rule monofun_cfun_arg)
 apply (erule deflation.below_ID)
done

lemma ep_pair_fmap:
  "ep_pair e p ==> ep_pair (fmap⋅e) (fmap⋅p)"
 apply (rule ep_pair.intro)
  apply (simp add: fmap_fmap ep_pair.e_inverse)
 apply (simp add: fmap_fmap)
 apply (rule_tac y="fmap⋅ID⋅y" in below_trans)
  apply (rule monofun_cfun_fun)
  apply (rule monofun_cfun_arg)
  apply (rule cfun_belowI, simp)
  apply (erule ep_pair.e_p_below)
 apply simp
done

lemma fmap_strict:
  fixes f :: "'a → 'b"
  assumes "f⋅⊥ = ⊥" shows "fmap⋅f⋅⊥ = (⊥::'b⋅'f::functor)"
proof (rule bottomI)
  have "fmap⋅f⋅(⊥::'a⋅'f) ⊑ fmap⋅f⋅(fmap⋅⊥⋅(⊥::'b⋅'f))"
    by (simp add: monofun_cfun)
  also have "... = fmap⋅(Λ x. f⋅(⊥⋅x))⋅(⊥::'b⋅'f)"
    by (simp add: fmap_fmap)
  also have "... ⊑ fmap⋅ID⋅⊥"
    by (simp add: monofun_cfun assms del: fmap_ID)
  also have "... = ⊥"
    by simp
  finally show "fmap⋅f⋅⊥ ⊑ (⊥::'b⋅'f::functor)" .
qed

subsection ‹Proving that ‹fmap⋅coerce = coerce››

lemma fmapU_cast_eq:
  "fmapU⋅(cast⋅A) =
    PRJ(udom⋅'f) oo cast⋅(TC('f::functor)⋅A) oo emb"
by (subst cast_TC, rule cfun_eqI, simp)

lemma fmapU_cast_DEFL:
  "fmapU⋅(cast⋅DEFL('a)) =
    PRJ(udom⋅'f) oo cast⋅DEFL('a⋅'f::functor) oo emb"
by (simp add: fmapU_cast_eq DEFL_app)

lemma coerce_functor: "COERCE('a⋅'f, 'b⋅'f::functor) = fmap⋅coerce"
apply (rule cfun_eqI, rename_tac xs)
apply (simp add: fmap_def coerce_cfun)
apply (simp add: coerce_def)
apply (simp add: cfcomp1)
apply (simp only: emb_prj)
apply (subst fmapU_fmapU [symmetric])
apply (simp add: fmapU_cast_DEFL)
apply (simp add: emb_prj)
apply (simp add: cast_cast_below1 cast_cast_below2)
done

subsection ‹Lemmas for reasoning about coercion›

lemma fmapU_cast_coerce [coerce_simp]:
  fixes m :: "'a⋅'f::functor"
  shows "fmapU⋅(cast⋅DEFL('a))⋅(COERCE('a⋅'f, udom⋅'f)⋅m) =
    COERCE('a⋅'f, udom⋅'f)⋅m"
by (simp add: coerce_functor cast_DEFL fmapU_eq_fmap fmap_fmap eta_cfun)

lemma coerce_fmap [coerce_simp]:
  fixes xs :: "'a⋅'f::functor" and f :: "'a → 'b"
  shows "COERCE('b⋅'f, 'c⋅'f)⋅(fmap⋅f⋅xs) = fmap⋅(Λ x. COERCE('b,'c)⋅(f⋅x))⋅xs"
by (simp add: coerce_functor fmap_fmap)

lemma fmap_coerce [coerce_simp]:
  fixes xs :: "'a⋅'f::functor" and f :: "'b → 'c"
  shows "fmap⋅f⋅(COERCE('a⋅'f, 'b⋅'f)⋅xs) = fmap⋅(Λ x. f⋅(COERCE('a,'b)⋅x))⋅xs"
by (simp add: coerce_functor fmap_fmap)

subsection ‹Configuration of Domain package›

text ‹We make various theorem declarations to enable Domain
 package definitions that involve ‹tycon› application.›

setup ‹Domain_Take_Proofs.add_rec_type (@{type_name app}, [true, false])›

declare DEFL_app [domain_defl_simps]
declare fmap_ID [domain_map_ID]
declare deflation_fmap [domain_deflation]
declare isodefl_fmap [domain_isodefl]

subsection ‹Configuration of the Tycon package›

text ‹We now set up a new type definition command, which is used for
 defining new ‹tycon› instances. The ‹tycondef› command
 is implemented using much of the same code as the Domain package,
 and supports a similar input syntax. It automatically generates a
 ‹prefunctor› instance for each new type. (The user must
 provide a proof of the composition law to obtain a ‹functor›
 class instance.)›

ML_file ‹tycondef.ML›

end