Quelle  Cprod.thy   Sprache: Isabelle

(*  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