Theory Data_Function

section ‹Data: Functions›

theory Data_Function
  imports HOLCF_Main
begin

fixrec flip :: "('a -> 'b -> 'c) -> 'b -> 'a -> 'c" where
  "flip⋅f⋅x⋅y = f⋅y⋅x"

fixrec const :: "'a → 'b → 'a" where
  "const⋅x⋅_ = x"

fixrec dollar :: "('a -> 'b) -> 'a -> 'b" where
  "dollar⋅f⋅x = f⋅x"

fixrec dollarBang :: "('a -> 'b) -> 'a -> 'b" where
  "dollarBang⋅f⋅x = seq⋅x⋅(f⋅x)"

fixrec on :: "('b -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'a -> 'c" where
  "on⋅g⋅f⋅x⋅y = g⋅(f⋅x)⋅(f⋅y)"

end