src/Sequents/ILL/ILL_predlog.thy
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 14854 61bdf2ae4dc5
permissions -rw-r--r--
converted to Isar theory format;
     1 (* $Id$ *)
     2 
     3 theory ILL_predlog
     4 imports ILL
     5 begin
     6 
     7 typedecl plf
     8 
     9 consts
    10   "&"   :: "[plf,plf] => plf"   (infixr 35)
    11   "|"   :: "[plf,plf] => plf"   (infixr 35)
    12   ">"   :: "[plf,plf] => plf"   (infixr 35)
    13   "="   :: "[plf,plf] => plf"   (infixr 35)
    14   "@NG" :: "plf => plf"   ("- _ " [50] 55)
    15   ff    :: "plf"
    16 
    17   PL    :: "plf => o"      ("[* / _ / *]" [] 100)
    18 
    19 
    20 translations
    21 
    22   "[* A & B *]" == "[*A*] && [*B*]"
    23   "[* A | B *]" == "![*A*] ++ ![*B*]"
    24   "[* - A *]"   == "[*A > ff*]"
    25   "[* ff *]"    == "0"
    26   "[* A = B *]" => "[* (A > B) & (B > A) *]"
    27 
    28   "[* A > B *]" == "![*A*] -o [*B*]"
    29 
    30 (* another translations for linear implication:
    31   "[* A > B *]" == "!([*A*] -o [*B*])" *)
    32 
    33 end