|
6252
|
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 |
plf
|
|
|
11 |
|
|
|
12 |
consts
|
|
|
13 |
|
|
|
14 |
"&" :: "[plf,plf] => plf" (infixr 35)
|
|
|
15 |
"|" :: "[plf,plf] => plf" (infixr 35)
|
|
|
16 |
">" :: "[plf,plf] => plf" (infixr 35)
|
|
|
17 |
"=" :: "[plf,plf] => plf" (infixr 35)
|
|
|
18 |
"@NG" :: "plf => plf" ("- _ " [50] 55)
|
|
|
19 |
ff :: "plf"
|
|
|
20 |
|
|
|
21 |
PL :: "plf => o" ("[* / _ / *]" [] 100)
|
|
|
22 |
|
|
|
23 |
|
|
|
24 |
translations
|
|
|
25 |
|
|
|
26 |
"[* A & B *]" == "[*A*] && [*B*]"
|
|
|
27 |
"[* A | B *]" == "![*A*] ++ ![*B*]"
|
|
|
28 |
"[* - A *]" == "[*A > ff*]"
|
|
|
29 |
"[* ff *]" == "0"
|
|
|
30 |
"[* A = B *]" => "[* (A > B) & (B > A) *]"
|
|
|
31 |
|
|
|
32 |
"[* A > B *]" == "![*A*] -o [*B*]"
|
|
|
33 |
|
|
|
34 |
(* another translations for linear implication:
|
|
|
35 |
"[* A > B *]" == "!([*A*] -o [*B*])" *)
|
|
|
36 |
|
|
|
37 |
end
|