Theory Cprod

(*  Title:      HOL/HOLCF/Cprod.thy
    Author:     Franz Regensburger
*)

section ‹The cpo of cartesian products›

theory Cprod
  imports Cfun
begin

subsection ‹Continuous case function for unit type›

definition unit_when :: "'a → unit → 'a"
  where "unit_when = (Λ a _. a)"

translations
  "Λ(). t" ⇌ "CONST unit_when⋅t"

lemma unit_when [simp]: "unit_when⋅a⋅u = a"
  by (simp add: unit_when_def)


subsection ‹Continuous version of split function›

definition csplit :: "('a → 'b → 'c) → ('a × 'b) → 'c"
  where "csplit = (Λ f p. f⋅(fst p)⋅(snd p))"

translations
  "Λ(CONST Pair x y). t" ⇌ "CONST csplit⋅(Λ x y. t)"

abbreviation cfst :: "'a × 'b → 'a"
  where "cfst ≡ Abs_cfun fst"

abbreviation csnd :: "'a × 'b → 'b"
  where "csnd ≡ Abs_cfun snd"


subsection ‹Convert all lemmas to the continuous versions›

lemma csplit1 [simp]: "csplit⋅f⋅⊥ = f⋅⊥⋅⊥"
  by (simp add: csplit_def)

lemma csplit_Pair [simp]: "csplit⋅f⋅(x, y) = f⋅x⋅y"
  by (simp add: csplit_def)

end