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