Quelle Cprod.thy Sprache: Isabelle

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

section \<open>The cpo of cartesian products\<close>

theory Cprod
  imports Cfun
begin

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

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.