(*
File: /Nfs/toton/usr20/sk/isa_files/ll/NEW/pred_log.thy
Theory Name: pred_log
Logic Image: HOL
*)
ILL_predlog = ILL +
types
plf
arities
plf :: logic
consts
"&" :: "[plf,plf] => plf" (infixr 35)
"|" :: "[plf,plf] => plf" (infixr 35)
">" :: "[plf,plf] => plf" (infixr 35)
"=" :: "[plf,plf] => plf" (infixr 35)
"@NG" :: "plf => plf" ("- _ " [50] 55)
ff :: "plf"
PL :: "plf => o" ("[* / _ / *]" [] 100)
translations
"[* A & B *]" == "[*A*] && [*B*]"
"[* A | B *]" == "![*A*] ++ ![*B*]"
"[* - A *]" == "[*A > ff*]"
"[* ff *]" == "0"
"[* A = B *]" => "[* (A > B) & (B > A) *]"
"[* A > B *]" == "![*A*] -o [*B*]"
(* another translations for linear implication:
"[* A > B *]" == "!([*A*] -o [*B*])" *)
end