author | huffman |
Sat, 27 Nov 2010 16:08:10 -0800 | |
changeset 40774 | 0437dbc127b3 |
parent 36452 | src/HOLCF/IOA/meta_theory/Pred.thy@d37c6eed8117 |
child 40945 | b8703f63bfb2 |
permissions | -rw-r--r-- |
5976 | 1 |
(* Title: HOLCF/IOA/meta_theory/Pred.thy |
12218 | 2 |
Author: Olaf Müller |
17233 | 3 |
*) |
4559 | 4 |
|
17233 | 5 |
header {* Logical Connectives lifted to predicates *} |
4559 | 6 |
|
17233 | 7 |
theory Pred |
8 |
imports Main |
|
9 |
begin |
|
10 |
||
36452 | 11 |
default_sort type |
4559 | 12 |
|
13 |
types |
|
17233 | 14 |
'a predicate = "'a => bool" |
4559 | 15 |
|
16 |
consts |
|
17 |
||
18 |
satisfies ::"'a => 'a predicate => bool" ("_ |= _" [100,9] 8) |
|
17233 | 19 |
valid ::"'a predicate => bool" (* ("|-") *) |
4559 | 20 |
|
21 |
NOT ::"'a predicate => 'a predicate" (".~ _" [40] 40) |
|
22 |
AND ::"'a predicate => 'a predicate => 'a predicate" (infixr ".&" 35) |
|
23 |
OR ::"'a predicate => 'a predicate => 'a predicate" (infixr ".|" 30) |
|
24 |
IMPLIES ::"'a predicate => 'a predicate => 'a predicate" (infixr ".-->" 25) |
|
25 |
||
26 |
||
35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
27 |
notation (output) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
28 |
NOT ("~ _" [40] 40) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
29 |
AND (infixr "&" 35) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
30 |
OR (infixr "|" 30) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
31 |
IMPLIES (infixr "-->" 25) |
4559 | 32 |
|
35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
33 |
notation (xsymbols output) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
34 |
NOT ("\<not> _" [40] 40) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
35 |
AND (infixr "\<and>" 35) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
36 |
OR (infixr "\<or>" 30) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
37 |
IMPLIES (infixr "\<longrightarrow>" 25) |
4559 | 38 |
|
35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
39 |
notation (xsymbols) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
40 |
satisfies ("_ \<Turnstile> _" [100,9] 8) |
4559 | 41 |
|
35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
42 |
notation (HTML output) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
43 |
NOT ("\<not> _" [40] 40) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
44 |
AND (infixr "\<and>" 35) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35174
diff
changeset
|
45 |
OR (infixr "\<or>" 30) |
6340 | 46 |
|
4559 | 47 |
|
48 |
defs |
|
49 |
||
17233 | 50 |
satisfies_def: |
51 |
"s |= P == P s" |
|
4559 | 52 |
|
53 |
(* priority einfuegen, da clash mit |=, wenn graphisches Symbol *) |
|
17233 | 54 |
valid_def: |
4559 | 55 |
"valid P == (! s. (s |= P))" |
56 |
||
17233 | 57 |
NOT_def: |
4559 | 58 |
"NOT P s == ~ (P s)" |
59 |
||
17233 | 60 |
AND_def: |
4559 | 61 |
"(P .& Q) s == (P s) & (Q s)" |
62 |
||
17233 | 63 |
OR_def: |
4559 | 64 |
"(P .| Q) s == (P s) | (Q s)" |
65 |
||
17233 | 66 |
IMPLIES_def: |
4559 | 67 |
"(P .--> Q) s == (P s) --> (Q s)" |
68 |
||
7661 | 69 |
end |