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