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