src/HOLCF/IOA/meta_theory/Pred.thy
changeset 4559 8e604d885b54
child 5976 44290b71a85f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Mon Jan 12 17:48:23 1998 +0100
     1.3 @@ -0,0 +1,72 @@
     1.4 +(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Olaf M"uller
     1.7 +    Copyright   1997  TU Muenchen
     1.8 +
     1.9 +Logical Connectives lifted to predicates.
    1.10 +
    1.11 +ToDo:
    1.12 +
    1.13 +<--> einfuehren.
    1.14 +
    1.15 +*)   
    1.16 +	       
    1.17 +Pred = Arith +  
    1.18 +
    1.19 +default term
    1.20 +
    1.21 +types
    1.22 +
    1.23 +'a predicate      = "'a => bool"
    1.24 +
    1.25 +consts
    1.26 +
    1.27 +satisfies    ::"'a  => 'a predicate => bool"    ("_ |= _" [100,9] 8)
    1.28 +valid        ::"'a predicate => bool"           (*  ("|-") *)         
    1.29 +
    1.30 +NOT          ::"'a predicate => 'a predicate"  (".~ _" [40] 40)
    1.31 +AND          ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".&" 35)
    1.32 +OR           ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".|" 30)
    1.33 +IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".-->" 25)
    1.34 +
    1.35 +
    1.36 +syntax ("" output)
    1.37 +  "NOT"     ::"'a predicate => 'a predicate" ("~ _" [40] 40)
    1.38 +  "AND"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "&" 35)
    1.39 +  "OR"      ::"'a predicate => 'a predicate => 'a predicate"    (infixr "|" 30)
    1.40 +  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "-->" 25)
    1.41 +
    1.42 +syntax (symbols output)
    1.43 +  "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
    1.44 +  "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)
    1.45 +  "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)
    1.46 +  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<midarrow>\\<rightarrow>" 25)
    1.47 +
    1.48 +syntax (symbols)
    1.49 +  "satisfies"  ::"'a => 'a predicate => bool"    ("_ \\<Turnstile> _" [100,9] 8)
    1.50 +
    1.51 +
    1.52 +defs
    1.53 +
    1.54 +satisfies_def
    1.55 +   "s |= P  == P s" 
    1.56 +
    1.57 +(* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)
    1.58 +valid_def
    1.59 +   "valid P == (! s. (s |= P))"
    1.60 +
    1.61 +
    1.62 +NOT_def
    1.63 +  "NOT P s ==  ~ (P s)"
    1.64 +
    1.65 +AND_def
    1.66 +  "(P .& Q) s == (P s) & (Q s)"
    1.67 +
    1.68 +
    1.69 +OR_def
    1.70 +  "(P .| Q) s ==  (P s) | (Q s)"
    1.71 +
    1.72 +IMPLIES_def
    1.73 +  "(P .--> Q) s == (P s) --> (Q s)"
    1.74 +
    1.75 +end
    1.76 \ No newline at end of file