Suchen Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Haftungshinweis

Bemerkung: zur Agenda Produktseite wechseln Projekt Beratung

Eigene Datei ansehen e.g. http://myserver.net/mysource.java Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/HOLCF/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 16.11.2025 mit Größe 1 kB

Quellcode-Bibliothek 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%

¤ 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.0.13Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.