author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 12218 | 6597093b77e7 |
child 14565 | c6dc17aab88a |
permissions | -rw-r--r-- |
5976 | 1 |
(* Title: HOLCF/IOA/meta_theory/Pred.thy |
4559 | 2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
4559 | 5 |
|
6 |
Logical Connectives lifted to predicates. |
|
7 |
*) |
|
8 |
||
7661 | 9 |
Pred = Main + |
4559 | 10 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12218
diff
changeset
|
11 |
default type |
4559 | 12 |
|
13 |
types |
|
14 |
||
15 |
'a predicate = "'a => bool" |
|
16 |
||
17 |
consts |
|
18 |
||
19 |
satisfies ::"'a => 'a predicate => bool" ("_ |= _" [100,9] 8) |
|
20 |
valid ::"'a predicate => bool" (* ("|-") *) |
|
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) |
4559 | 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) |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
7661
diff
changeset
|
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) |
4559 | 41 |
"satisfies" ::"'a => 'a predicate => bool" ("_ \\<Turnstile> _" [100,9] 8) |
42 |
||
6340 | 43 |
syntax (HTML output) |
44 |
"NOT" ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40) |
|
45 |
||
4559 | 46 |
|
47 |
defs |
|
48 |
||
49 |
satisfies_def |
|
50 |
"s |= P == P s" |
|
51 |
||
52 |
(* priority einfuegen, da clash mit |=, wenn graphisches Symbol *) |
|
53 |
valid_def |
|
54 |
"valid P == (! s. (s |= P))" |
|
55 |
||
56 |
||
57 |
NOT_def |
|
58 |
"NOT P s == ~ (P s)" |
|
59 |
||
60 |
AND_def |
|
61 |
"(P .& Q) s == (P s) & (Q s)" |
|
62 |
||
63 |
||
64 |
OR_def |
|
65 |
"(P .| Q) s == (P s) | (Q s)" |
|
66 |
||
67 |
IMPLIES_def |
|
68 |
"(P .--> Q) s == (P s) --> (Q s)" |
|
69 |
||
7661 | 70 |
end |