Theory Applicative_Environment_Algebra

(* Author: Andreas Lochbihler, ETH Zurich *)

section ‹Examples of applicative lifting›

subsection ‹Algebraic operations for the environment functor›

theory Applicative_Environment_Algebra imports
  Applicative_Environment
  "HOL-Library.Function_Division"
begin

text ‹ Link between applicative instance of the environment functor with the pointwise operations
  for the algebraic type classes ›

context includes applicative_syntax
begin

lemma plus_fun_af [applicative_unfold]: "f + g = pure (+) ⋄ f ⋄ g"
unfolding plus_fun_def const_def apf_def ..

lemma zero_fun_af [applicative_unfold]: "0 = pure 0"
unfolding zero_fun_def const_def ..

lemma times_fun_af [applicative_unfold]: "f * g = pure (*) ⋄ f ⋄ g"
unfolding times_fun_def const_def apf_def ..

lemma one_fun_af [applicative_unfold]: "1 = pure 1"
unfolding one_fun_def const_def ..

lemma of_nat_fun_af [applicative_unfold]: "of_nat n = pure (of_nat n)"
unfolding of_nat_fun const_def ..

lemma inverse_fun_af [applicative_unfold]: "inverse f = pure inverse ⋄ f"
unfolding inverse_fun_def o_def const_def apf_def ..

lemma divide_fun_af [applicative_unfold]: "divide f g = pure divide ⋄ f ⋄ g"
unfolding divide_fun_def const_def apf_def ..

end

end