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