src/HOLCF/IOA/meta_theory/Pred.thy
author wenzelm
Sat Dec 01 18:52:32 2001 +0100 (2001-12-01)
changeset 12338 de0f4a63baa5
parent 12218 6597093b77e7
child 14565 c6dc17aab88a
permissions -rw-r--r--
renamed class "term" to "type" (actually "HOL.type");
     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 
    46 
    47 defs
    48 
    49 satisfies_def
    50    "s |= P  == P s" 
    51 
    52 (* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)
    53 valid_def
    54    "valid P == (! s. (s |= P))"
    55 
    56 
    57 NOT_def
    58   "NOT P s ==  ~ (P s)"
    59 
    60 AND_def
    61   "(P .& Q) s == (P s) & (Q s)"
    62 
    63 
    64 OR_def
    65   "(P .| Q) s ==  (P s) | (Q s)"
    66 
    67 IMPLIES_def
    68   "(P .--> Q) s == (P s) --> (Q s)"
    69 
    70 end