src/HOLCF/IOA/meta_theory/Pred.thy

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

(*  Title:      HOLCF/IOA/meta_theory/Pred.thy
    ID:         $Id$
    Author:     Olaf Müller
*)

header {* Logical Connectives lifted to predicates *}

theory Pred
imports Main
begin

defaultsort 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)


syntax ("" output)
  "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)

syntax (xsymbols output)
  "NOT"    ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
  "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\<and>" 35)
  "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\<or>" 30)
  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\<longrightarrow>" 25)

syntax (xsymbols)
  "satisfies"  ::"'a => 'a predicate => bool"    ("_ \<Turnstile> _" [100,9] 8)

syntax (HTML output)
  "NOT"    ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
  "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\<and>" 35)
  "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (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