(*  Title:      HOLCF/IOA/meta_theory/Pred.thy

     Author:     Olaf Müller

 *)

 header {* Logical Connectives lifted to predicates *}

 theory Pred

 imports Main

 begin

 default_sort type

 types

   'a predicate = "'a => bool"

 consts

 satisfies    ::"'a  => 'a predicate => bool"    ("_ |= _" [100,9] 8)

 valid        ::"'a predicate => bool"           (*  ("|-") *)

 NOT          ::"'a predicate => 'a predicate"  (".~ _" [40] 40)

 AND          ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".&" 35)

 OR           ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".|" 30)

 IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".-->" 25)

 notation (output)

   NOT  ("~ _" [40] 40) and

   AND  (infixr "&" 35) and

   OR  (infixr "|" 30) and

   IMPLIES  (infixr "-->" 25)

 notation (xsymbols output)

   NOT  ("\<not> _" [40] 40) and

   AND  (infixr "\<and>" 35) and

   OR  (infixr "\<or>" 30) and

   IMPLIES  (infixr "\<longrightarrow>" 25)

 notation (xsymbols)

   satisfies  ("_ \<Turnstile> _" [100,9] 8)

 notation (HTML output)

   NOT  ("\<not> _" [40] 40) and

   AND  (infixr "\<and>" 35) and

   OR  (infixr "\<or>" 30)

 defs

 satisfies_def:

    "s |= P  == P s"

 (* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)

 valid_def:

    "valid P == (! s. (s |= P))"

 NOT_def:

   "NOT P s ==  ~ (P s)"

 AND_def:

   "(P .& Q) s == (P s) & (Q s)"

 OR_def:

   "(P .| Q) s ==  (P s) | (Q s)"

 IMPLIES_def:

   "(P .--> Q) s == (P s) --> (Q s)"

 end