src/HOLCF/IOA/meta_theory/Pred.thy
author kleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565 c6dc17aab88a
parent 12338 de0f4a63baa5
child 14981 e73f8140af78
permissions -rw-r--r--
use more symbols in HTML output
     1 (*  Title:      HOLCF/IOA/meta_theory/Pred.thy
     2     ID:         $Id$
     3     Author:     Olaf Müller
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Logical Connectives lifted to predicates.
     7 *)   
     8 	       
     9 Pred = Main +
    10 
    11 default type
    12 
    13 types
    14 
    15 'a predicate      = "'a => bool"
    16 
    17 consts
    18 
    19 satisfies    ::"'a  => 'a predicate => bool"    ("_ |= _" [100,9] 8)
    20 valid        ::"'a predicate => bool"           (*  ("|-") *)         
    21 
    22 NOT          ::"'a predicate => 'a predicate"  (".~ _" [40] 40)
    23 AND          ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".&" 35)
    24 OR           ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".|" 30)
    25 IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".-->" 25)
    26 
    27 
    28 syntax ("" output)
    29   "NOT"     ::"'a predicate => 'a predicate" ("~ _" [40] 40)
    30   "AND"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "&" 35)
    31   "OR"      ::"'a predicate => 'a predicate => 'a predicate"    (infixr "|" 30)
    32   "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "-->" 25)
    33 
    34 syntax (xsymbols output)
    35   "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
    36   "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)
    37   "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)
    38   "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<longrightarrow>" 25)
    39 
    40 syntax (xsymbols)
    41   "satisfies"  ::"'a => 'a predicate => bool"    ("_ \\<Turnstile> _" [100,9] 8)
    42 
    43 syntax (HTML output)
    44   "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
    45   "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)
    46   "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)
    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