src/HOLCF/IOA/meta_theory/Pred.thy
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
     1.1 --- a/src/HOLCF/IOA/meta_theory/Pred.thy	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,69 +0,0 @@
     1.4 -(*  Title:      HOLCF/IOA/meta_theory/Pred.thy
     1.5 -    Author:     Olaf Müller
     1.6 -*)
     1.7 -
     1.8 -header {* Logical Connectives lifted to predicates *}
     1.9 -
    1.10 -theory Pred
    1.11 -imports Main
    1.12 -begin
    1.13 -
    1.14 -default_sort type
    1.15 -
    1.16 -types
    1.17 -  'a predicate = "'a => bool"
    1.18 -
    1.19 -consts
    1.20 -
    1.21 -satisfies    ::"'a  => 'a predicate => bool"    ("_ |= _" [100,9] 8)
    1.22 -valid        ::"'a predicate => bool"           (*  ("|-") *)
    1.23 -
    1.24 -NOT          ::"'a predicate => 'a predicate"  (".~ _" [40] 40)
    1.25 -AND          ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".&" 35)
    1.26 -OR           ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".|" 30)
    1.27 -IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".-->" 25)
    1.28 -
    1.29 -
    1.30 -notation (output)
    1.31 -  NOT  ("~ _" [40] 40) and
    1.32 -  AND  (infixr "&" 35) and
    1.33 -  OR  (infixr "|" 30) and
    1.34 -  IMPLIES  (infixr "-->" 25)
    1.35 -
    1.36 -notation (xsymbols output)
    1.37 -  NOT  ("\<not> _" [40] 40) and
    1.38 -  AND  (infixr "\<and>" 35) and
    1.39 -  OR  (infixr "\<or>" 30) and
    1.40 -  IMPLIES  (infixr "\<longrightarrow>" 25)
    1.41 -
    1.42 -notation (xsymbols)
    1.43 -  satisfies  ("_ \<Turnstile> _" [100,9] 8)
    1.44 -
    1.45 -notation (HTML output)
    1.46 -  NOT  ("\<not> _" [40] 40) and
    1.47 -  AND  (infixr "\<and>" 35) and
    1.48 -  OR  (infixr "\<or>" 30)
    1.49 -
    1.50 -
    1.51 -defs
    1.52 -
    1.53 -satisfies_def:
    1.54 -   "s |= P  == P s"
    1.55 -
    1.56 -(* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)
    1.57 -valid_def:
    1.58 -   "valid P == (! s. (s |= P))"
    1.59 -
    1.60 -NOT_def:
    1.61 -  "NOT P s ==  ~ (P s)"
    1.62 -
    1.63 -AND_def:
    1.64 -  "(P .& Q) s == (P s) & (Q s)"
    1.65 -
    1.66 -OR_def:
    1.67 -  "(P .| Q) s ==  (P s) | (Q s)"
    1.68 -
    1.69 -IMPLIES_def:
    1.70 -  "(P .--> Q) s == (P s) --> (Q s)"
    1.71 -
    1.72 -end