SSL DPC0Expressions.thy

Sprache: Isabelle

(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2006-2008 Norbert Schirmer
*)

section ‹SHORTENED! Parallel expressions in DPC/Hoare.›

theory DPC0Expressions imports Main begin

definition p_not :: "bool list => bool list"  ("¬_p")
  where "p_not = map Not"

definition elem_wise :: "('a → 'b → 'c) → 'a list → 'b list → 'c list"
  where "elem_wise f xs ys = map (λ (x, y). f x y) (zip xs ys)"

definition p_and  :: "bool list => bool list => bool list"  (infixl "∧_p"  35)
  where "p_and = elem_wise (&)"

notation (ASCII)
  p_and  (infixl "pand"  35)

end

Messung V0.5 in Prozent

¤ 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.1Bemerkung: (vorverarbeitet am 2026-09-09) ¤

*Bot Zugriff

Versionsinformation zu Columbo

Bemerkung:

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders