17481
|
1 |
(* $Id$ *)
|
6252
|
2 |
|
17481
|
3 |
theory ILL_predlog
|
|
4 |
imports ILL
|
|
5 |
begin
|
6252
|
6 |
|
17481
|
7 |
typedecl plf
|
|
8 |
|
6252
|
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"
|
17481
|
16 |
|
6252
|
17 |
PL :: "plf => o" ("[* / _ / *]" [] 100)
|
|
18 |
|
|
19 |
|
|
20 |
translations
|
|
21 |
|
17481
|
22 |
"[* A & B *]" == "[*A*] && [*B*]"
|
6252
|
23 |
"[* A | B *]" == "![*A*] ++ ![*B*]"
|
|
24 |
"[* - A *]" == "[*A > ff*]"
|
|
25 |
"[* ff *]" == "0"
|
|
26 |
"[* A = B *]" => "[* (A > B) & (B > A) *]"
|
17481
|
27 |
|
6252
|
28 |
"[* A > B *]" == "![*A*] -o [*B*]"
|
17481
|
29 |
|
6252
|
30 |
(* another translations for linear implication:
|
|
31 |
"[* A > B *]" == "!([*A*] -o [*B*])" *)
|
|
32 |
|
|
33 |
end
|