1 (* |
1 (* $Id$ *) |
2 File: /Nfs/toton/usr20/sk/isa_files/ll/NEW/pred_log.thy |
|
3 Theory Name: pred_log |
|
4 Logic Image: HOL |
|
5 *) |
|
6 |
2 |
7 ILL_predlog = ILL + |
3 theory ILL_predlog |
|
4 imports ILL |
|
5 begin |
8 |
6 |
9 types |
7 typedecl plf |
10 plf |
8 |
11 |
|
12 consts |
9 consts |
13 |
|
14 "&" :: "[plf,plf] => plf" (infixr 35) |
10 "&" :: "[plf,plf] => plf" (infixr 35) |
15 "|" :: "[plf,plf] => plf" (infixr 35) |
11 "|" :: "[plf,plf] => plf" (infixr 35) |
16 ">" :: "[plf,plf] => plf" (infixr 35) |
12 ">" :: "[plf,plf] => plf" (infixr 35) |
17 "=" :: "[plf,plf] => plf" (infixr 35) |
13 "=" :: "[plf,plf] => plf" (infixr 35) |
18 "@NG" :: "plf => plf" ("- _ " [50] 55) |
14 "@NG" :: "plf => plf" ("- _ " [50] 55) |
19 ff :: "plf" |
15 ff :: "plf" |
20 |
16 |
21 PL :: "plf => o" ("[* / _ / *]" [] 100) |
17 PL :: "plf => o" ("[* / _ / *]" [] 100) |
22 |
18 |
23 |
19 |
24 translations |
20 translations |
25 |
21 |
26 "[* A & B *]" == "[*A*] && [*B*]" |
22 "[* A & B *]" == "[*A*] && [*B*]" |
27 "[* A | B *]" == "![*A*] ++ ![*B*]" |
23 "[* A | B *]" == "![*A*] ++ ![*B*]" |
28 "[* - A *]" == "[*A > ff*]" |
24 "[* - A *]" == "[*A > ff*]" |
29 "[* ff *]" == "0" |
25 "[* ff *]" == "0" |
30 "[* A = B *]" => "[* (A > B) & (B > A) *]" |
26 "[* A = B *]" => "[* (A > B) & (B > A) *]" |
31 |
27 |
32 "[* A > B *]" == "![*A*] -o [*B*]" |
28 "[* A > B *]" == "![*A*] -o [*B*]" |
33 |
29 |
34 (* another translations for linear implication: |
30 (* another translations for linear implication: |
35 "[* A > B *]" == "!([*A*] -o [*B*])" *) |
31 "[* A > B *]" == "!([*A*] -o [*B*])" *) |
36 |
32 |
37 end |
33 end |