Theory Cprod

theory Cprod
imports Cfun
(*  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_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))"

  "Λ(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)