Theory Lem_function

chapter ‹Generated by Lem from ‹function.lem›.›

theory "Lem_function" 

imports
  Main
  "Lem_bool"
  "Lem_basic_classes"

begin 

― ‹‹****************************************************************************››
― ‹‹ A library for common operations on functions                               ››
― ‹‹****************************************************************************››

― ‹‹open import Bool Basic_classes››

― ‹‹open import {coq} `Program.Basics`››

― ‹‹ ----------------------- ››
― ‹‹ identity function       ››
― ‹‹ ----------------------- ››

― ‹‹val id : forall 'a. 'a -> 'a››
― ‹‹let id x=  x››


― ‹‹ ----------------------- ››
― ‹‹ constant function       ››
― ‹‹ ----------------------- ››

― ‹‹val const : forall 'a 'b. 'a -> 'b -> 'a››


― ‹‹ ----------------------- ››
― ‹‹ function composition    ››
― ‹‹ ----------------------- ››

― ‹‹val comb : forall 'a 'b 'c. ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)››
― ‹‹let comb f g=  (fun x -> f (g x))››


― ‹‹ ----------------------- ››
― ‹‹ function application    ››
― ‹‹ ----------------------- ››

― ‹‹val $ [apply] : forall 'a 'b. ('a -> 'b) -> ('a -> 'b)››
― ‹‹let $ f=  (fun x -> f x)››

― ‹‹val $> [rev_apply] : forall 'a 'b. 'a -> ('a -> 'b) -> 'b››
― ‹‹let $> x f=  f x››

― ‹‹ ----------------------- ››
― ‹‹ flipping argument order ››
― ‹‹ ----------------------- ››

― ‹‹val flip : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('b -> 'a -> 'c)››
― ‹‹let flip f=  (fun x y -> f y x)››


― ‹‹ currying / uncurrying ››

― ‹‹val curry : forall 'a 'b 'c. (('a * 'b) -> 'c) -> 'a -> 'b -> 'c››
definition curry  :: "('a*'b ⇒ 'c)⇒ 'a ⇒ 'b ⇒ 'c "  where 
     " curry f = ( (λ a b .  f (a, b)))"


― ‹‹val uncurry : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('a * 'b -> 'c)››
fun uncurry  :: "('a ⇒ 'b ⇒ 'c)⇒ 'a*'b ⇒ 'c "  where 
     " uncurry f (a,b) = ( f a b )"

end