Theory Applicative_Environment

(* Author: Joshua Schneider, ETH Zurich *)

section ‹Common applicative functors›

subsection ‹Environment functor›

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

definition "const x = (λ_. x)"
definition "apf x y = (λz. x z (y z))"

adhoc_overloading Applicative.pure const
adhoc_overloading Applicative.ap apf

text ‹The declaration below demonstrates that applicative functors which lift the reductions
  for combinators K and W also lift C. However, the interchange law must be supplied in this case.›

applicative env (K, W)
for
  pure: const
  ap: apf
  rel: "rel_fun (=)"
  set: range
by(simp_all add: const_def apf_def rel_fun_def)

lemma
  includes applicative_syntax
  shows "const (λf x y. f y x) ⋄ f ⋄ x ⋄ y = f ⋄ y ⋄ x"
by applicative_lifting simp

end