Theory Applicative_Environment_Algebra
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