(* Title: HOL/HOLCF/IOA/Pred.thy
Author: Olaf Müller
*)
section \<open>Logical Connectives lifted to predicates\<close>
theory Pred
imports Main
begin
default_sort type
type_synonym 'a predicate = "'a \<Rightarrow> bool"
definition satisfies :: "'a \ 'a predicate \ bool" ("_ \ _" [100, 9] 8)
where "(s \ P) \ P s"
definition valid :: "'a predicate \ bool" ("\ _" [9] 8)
where "(\ P) \ (\s. (s \ P))"
definition NOT :: "'a predicate \ 'a predicate" ("\<^bold>\ _" [40] 40)
where "NOT P s \ \ P s"
definition AND :: "'a predicate \ 'a predicate \ 'a predicate" (infixr "\<^bold>\" 35)
where "(P \<^bold>\ Q) s \ P s \ Q s"
definition OR :: "'a predicate \ 'a predicate \ 'a predicate" (infixr "\<^bold>\" 30)
where "(P \<^bold>\ Q) s \ P s \ Q s"
definition IMPLIES :: "'a predicate \ 'a predicate \ 'a predicate" (infixr "\<^bold>\" 25)
where "(P \<^bold>\ Q) s \ P s \ Q s"
end
¤ Dauer der Verarbeitung: 0.1 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.
|