equal
deleted
inserted
replaced
1 (* $Id$ *) |
|
2 |
|
3 theory ILL_predlog |
|
4 imports ILL |
|
5 begin |
|
6 |
|
7 typedecl plf |
|
8 |
|
9 consts |
|
10 "&" :: "[plf,plf] => plf" (infixr 35) |
|
11 "|" :: "[plf,plf] => plf" (infixr 35) |
|
12 ">" :: "[plf,plf] => plf" (infixr 35) |
|
13 "=" :: "[plf,plf] => plf" (infixr 35) |
|
14 "@NG" :: "plf => plf" ("- _ " [50] 55) |
|
15 ff :: "plf" |
|
16 |
|
17 PL :: "plf => o" ("[* / _ / *]" [] 100) |
|
18 |
|
19 |
|
20 translations |
|
21 |
|
22 "[* A & B *]" == "[*A*] && [*B*]" |
|
23 "[* A | B *]" == "![*A*] ++ ![*B*]" |
|
24 "[* - A *]" == "[*A > ff*]" |
|
25 "[* ff *]" == "0" |
|
26 "[* A = B *]" => "[* (A > B) & (B > A) *]" |
|
27 |
|
28 "[* A > B *]" == "![*A*] -o [*B*]" |
|
29 |
|
30 (* another translations for linear implication: |
|
31 "[* A > B *]" == "!([*A*] -o [*B*])" *) |
|
32 |
|
33 end |
|