src/HOLCF/IOA/meta_theory/Pred.thy
author mueller
Mon Jan 12 17:48:23 1998 +0100 (1998-01-12)
changeset 4559 8e604d885b54
child 5976 44290b71a85f
permissions -rw-r--r--
added files containing temproal logic and abstraction;
     1 (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
     2     ID:         $Id$
     3     Author:     Olaf M"uller
     4     Copyright   1997  TU Muenchen
     5 
     6 Logical Connectives lifted to predicates.
     7 
     8 ToDo:
     9 
    10 <--> einfuehren.
    11 
    12 *)   
    13 	       
    14 Pred = Arith +  
    15 
    16 default term
    17 
    18 types
    19 
    20 'a predicate      = "'a => bool"
    21 
    22 consts
    23 
    24 satisfies    ::"'a  => 'a predicate => bool"    ("_ |= _" [100,9] 8)
    25 valid        ::"'a predicate => bool"           (*  ("|-") *)         
    26 
    27 NOT          ::"'a predicate => 'a predicate"  (".~ _" [40] 40)
    28 AND          ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".&" 35)
    29 OR           ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".|" 30)
    30 IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".-->" 25)
    31 
    32 
    33 syntax ("" output)
    34   "NOT"     ::"'a predicate => 'a predicate" ("~ _" [40] 40)
    35   "AND"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "&" 35)
    36   "OR"      ::"'a predicate => 'a predicate => 'a predicate"    (infixr "|" 30)
    37   "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "-->" 25)
    38 
    39 syntax (symbols output)
    40   "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
    41   "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)
    42   "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)
    43   "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<midarrow>\\<rightarrow>" 25)
    44 
    45 syntax (symbols)
    46   "satisfies"  ::"'a => 'a predicate => bool"    ("_ \\<Turnstile> _" [100,9] 8)
    47 
    48 
    49 defs
    50 
    51 satisfies_def
    52    "s |= P  == P s" 
    53 
    54 (* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)
    55 valid_def
    56    "valid P == (! s. (s |= P))"
    57 
    58 
    59 NOT_def
    60   "NOT P s ==  ~ (P s)"
    61 
    62 AND_def
    63   "(P .& Q) s == (P s) & (Q s)"
    64 
    65 
    66 OR_def
    67   "(P .| Q) s ==  (P s) | (Q s)"
    68 
    69 IMPLIES_def
    70   "(P .--> Q) s == (P s) --> (Q s)"
    71 
    72 end