section ‹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