|
(* Title: HOL/HOLCF/Cprod.thy
Author: Franz Regensburger
*)
section \<open>The cpo of cartesian products\<close>
theory Cprod
imports Cfun
begin
default_sort cpo
subsection \<open>Continuous case function for unit type\<close>
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 \<open>Continuous version of split function\<close>
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 \<open>Convert all lemmas to the continuous versions\<close>
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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
