src/HOLCF/IOA/meta_theory/Pred.thy
author wenzelm
Fri Nov 09 00:09:47 2001 +0100 (2001-11-09)
changeset 12114 a8e860c86252
parent 7661 8c3190b173aa
child 12218 6597093b77e7
permissions -rw-r--r--
eliminated old "symbols" syntax, use "xsymbols" instead;
     1 (*  Title:      HOLCF/IOA/meta_theory/Pred.thy
     2     ID:         $Id$
     3     Author:     Olaf M"uller
     4     Copyright   1997  TU Muenchen
     5 
     6 Logical Connectives lifted to predicates.
     7 
     8 *)   
     9 	       
    10 Pred = Main +
    11 
    12 default term
    13 
    14 types
    15 
    16 'a predicate      = "'a => bool"
    17 
    18 consts
    19 
    20 satisfies    ::"'a  => 'a predicate => bool"    ("_ |= _" [100,9] 8)
    21 valid        ::"'a predicate => bool"           (*  ("|-") *)         
    22 
    23 NOT          ::"'a predicate => 'a predicate"  (".~ _" [40] 40)
    24 AND          ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".&" 35)
    25 OR           ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".|" 30)
    26 IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".-->" 25)
    27 
    28 
    29 syntax ("" output)
    30   "NOT"     ::"'a predicate => 'a predicate" ("~ _" [40] 40)
    31   "AND"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "&" 35)
    32   "OR"      ::"'a predicate => 'a predicate => 'a predicate"    (infixr "|" 30)
    33   "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "-->" 25)
    34 
    35 syntax (xsymbols output)
    36   "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
    37   "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)
    38   "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)
    39   "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<longrightarrow>" 25)
    40 
    41 syntax (xsymbols)
    42   "satisfies"  ::"'a => 'a predicate => bool"    ("_ \\<Turnstile> _" [100,9] 8)
    43 
    44 syntax (HTML output)
    45   "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
    46 
    47 
    48 defs
    49 
    50 satisfies_def
    51    "s |= P  == P s" 
    52 
    53 (* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)
    54 valid_def
    55    "valid P == (! s. (s |= P))"
    56 
    57 
    58 NOT_def
    59   "NOT P s ==  ~ (P s)"
    60 
    61 AND_def
    62   "(P .& Q) s == (P s) & (Q s)"
    63 
    64 
    65 OR_def
    66   "(P .| Q) s ==  (P s) | (Q s)"
    67 
    68 IMPLIES_def
    69   "(P .--> Q) s == (P s) --> (Q s)"
    70 
    71 end