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;
mueller@4559
     1
(*  Title:      HOLCF/IOA/meta_theory/TLS.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
ToDo:
mueller@4559
     9
mueller@4559
    10
<--> einfuehren.
mueller@4559
    11
mueller@4559
    12
*)   
mueller@4559
    13
	       
mueller@4559
    14
Pred = Arith +  
mueller@4559
    15
mueller@4559
    16
default term
mueller@4559
    17
mueller@4559
    18
types
mueller@4559
    19
mueller@4559
    20
'a predicate      = "'a => bool"
mueller@4559
    21
mueller@4559
    22
consts
mueller@4559
    23
mueller@4559
    24
satisfies    ::"'a  => 'a predicate => bool"    ("_ |= _" [100,9] 8)
mueller@4559
    25
valid        ::"'a predicate => bool"           (*  ("|-") *)         
mueller@4559
    26
mueller@4559
    27
NOT          ::"'a predicate => 'a predicate"  (".~ _" [40] 40)
mueller@4559
    28
AND          ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".&" 35)
mueller@4559
    29
OR           ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".|" 30)
mueller@4559
    30
IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".-->" 25)
mueller@4559
    31
mueller@4559
    32
mueller@4559
    33
syntax ("" output)
mueller@4559
    34
  "NOT"     ::"'a predicate => 'a predicate" ("~ _" [40] 40)
mueller@4559
    35
  "AND"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "&" 35)
mueller@4559
    36
  "OR"      ::"'a predicate => 'a predicate => 'a predicate"    (infixr "|" 30)
mueller@4559
    37
  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "-->" 25)
mueller@4559
    38
mueller@4559
    39
syntax (symbols output)
mueller@4559
    40
  "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
mueller@4559
    41
  "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)
mueller@4559
    42
  "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)
mueller@4559
    43
  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<midarrow>\\<rightarrow>" 25)
mueller@4559
    44
mueller@4559
    45
syntax (symbols)
mueller@4559
    46
  "satisfies"  ::"'a => 'a predicate => bool"    ("_ \\<Turnstile> _" [100,9] 8)
mueller@4559
    47
mueller@4559
    48
mueller@4559
    49
defs
mueller@4559
    50
mueller@4559
    51
satisfies_def
mueller@4559
    52
   "s |= P  == P s" 
mueller@4559
    53
mueller@4559
    54
(* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)
mueller@4559
    55
valid_def
mueller@4559
    56
   "valid P == (! s. (s |= P))"
mueller@4559
    57
mueller@4559
    58
mueller@4559
    59
NOT_def
mueller@4559
    60
  "NOT P s ==  ~ (P s)"
mueller@4559
    61
mueller@4559
    62
AND_def
mueller@4559
    63
  "(P .& Q) s == (P s) & (Q s)"
mueller@4559
    64
mueller@4559
    65
mueller@4559
    66
OR_def
mueller@4559
    67
  "(P .| Q) s ==  (P s) | (Q s)"
mueller@4559
    68
mueller@4559
    69
IMPLIES_def
mueller@4559
    70
  "(P .--> Q) s == (P s) --> (Q s)"
mueller@4559
    71
mueller@4559
    72
end