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