Theory Pred

(*  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_def: "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