Theory Pred

theory Pred
imports Main
(*  Title:      HOL/HOLCF/IOA/Pred.thy
    Author:     Olaf Müller
*)

section ‹Logical Connectives lifted to predicates›

theory Pred
imports Main
begin

default_sort type

type_synonym 'a predicate = "'a ⇒ 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"  ("¬ _" [40] 40)
  where "NOT P s ⟷ ¬ P s"

definition AND :: "'a predicate ⇒ 'a predicate ⇒ 'a predicate"  (infixr "" 35)
  where "(P  Q) s ⟷ P s ∧ Q s"

definition OR :: "'a predicate ⇒ 'a predicate ⇒ 'a predicate"  (infixr "" 30)
  where "(P  Q) s ⟷ P s ∨ Q s"

definition IMPLIES :: "'a predicate ⇒ 'a predicate ⇒ 'a predicate"  (infixr "" 25)
  where "(P  Q) s ⟷ P s ⟶ Q s"

end