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