Theory Hs_Compat

theory Hs_Compat
imports Main
begin

section‹Definitions inspired by the Haskell World.›

definition uncurry :: "('b  'c  'a)  'b × 'c  'a"
where
  "uncurry f a  (case a of (x,y)  f x y)"

lemma uncurry_simp[simp]: "uncurry f (a,b) = f a b" 
  by(simp add: uncurry_def)

lemma uncurry_curry_id: "uncurry  curry = id" "curry  uncurry = id" 
  by(simp_all add: fun_eq_iff)

lemma uncurry_split: "P (uncurry f p)  (x1 x2. p = (x1, x2)  P (f x1 x2))"
  by(cases p) simp

lemma uncurry_split_asm: "P (uncurry f a)  ¬(x y. a = (x,y)  ¬P (f x y))" 
  by(simp split: uncurry_split)

lemmas uncurry_splits = uncurry_split uncurry_split_asm

lemma uncurry_case_stmt: "(case x of (a, b)  f a b) = uncurry f x"
  by(cases x, simp)

end