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