Theory Cprod

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


header {* The cpo of cartesian products *}

theory Cprod
imports Cfun
begin

default_sort cpo

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