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