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 


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
