src/HOLCF/IOA/meta_theory/Pred.thy
author mueller
Thu Nov 26 16:37:56 1998 +0100 (1998-11-26)
changeset 5976 44290b71a85f
parent 4559 8e604d885b54
child 6340 7d5cbd5819a0
permissions -rw-r--r--
tuning to assimiliate it with PhD;
     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 = Arith +  
    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 (symbols 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 "\\<midarrow>\\<rightarrow>" 25)
    40 
    41 syntax (symbols)
    42   "satisfies"  ::"'a => 'a predicate => bool"    ("_ \\<Turnstile> _" [100,9] 8)
    43 
    44 
    45 defs
    46 
    47 satisfies_def
    48    "s |= P  == P s" 
    49 
    50 (* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)
    51 valid_def
    52    "valid P == (! s. (s |= P))"
    53 
    54 
    55 NOT_def
    56   "NOT P s ==  ~ (P s)"
    57 
    58 AND_def
    59   "(P .& Q) s == (P s) & (Q s)"
    60 
    61 
    62 OR_def
    63   "(P .| Q) s ==  (P s) | (Q s)"
    64 
    65 IMPLIES_def
    66   "(P .--> Q) s == (P s) --> (Q s)"
    67 
    68 end