Theory Cprod

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

section ‹The cpo of cartesian products›

theory Cprod
  imports Cfun

default_sort cpo

subsection ‹Continuous case function for unit type›

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

  "Λ(). t"  "CONST unit_whent"

lemma unit_when [simp]: "unit_whenau = 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))"

  "Λ(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]: "csplitf = f"
  by (simp add: csplit_def)

lemma csplit_Pair [simp]: "csplitf(x, y) = fxy"
  by (simp add: csplit_def)