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