Theory Abstract_AF

(* Author: Joshua Schneider, ETH Zurich
   Author: Andreas Lochbihler, ETH Zurich *)

section ‹An abstract applicative functor›

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

typedef 'a af = "UNIV :: 'a set" ..

setup_lifting type_definition_af

abbreviation "af_pure ≡ Abs_af"
lift_definition af_ap :: "('a ⇒ 'b) af ⇒ 'a af ⇒ 'b af" is "λf x. f x" .

adhoc_overloading Applicative.pure Abs_af
adhoc_overloading Applicative.ap af_ap

context includes applicative_syntax
begin

lemma af_identity: "af_pure id ⋄ x = x"
by transfer simp

lemma af_homomorphism: "af_pure f ⋄ af_pure x = af_pure (f x)"
by(fact af_ap.abs_eq)

lemma af_composition: "af_pure comp ⋄ g ⋄ f ⋄ x = g ⋄ (f ⋄ x)"
by transfer simp

lemma af_interchange: "f ⋄ af_pure x = af_pure (λg. g x) ⋄ f"
by transfer simp

end

lifting_forget af.lifting

hide_const Abs_af Rep_af
hide_fact af_ap_def

applicative af
for
  pure: af_pure
  ap: af_ap
using af_homomorphism af_composition af_identity af_interchange
unfolding id_def comp_def[abs_def]
.

end