src/Sequents/ILL_predlog.thy
author wenzelm
Mon Mar 19 21:10:33 2012 +0100 (2012-03-19)
changeset 47022 8eac39af4ec0
parent 35762 af3ff2ba4c54
child 61385 538100cc4399
permissions -rw-r--r--
moved some legacy stuff;
     1 theory ILL_predlog
     2 imports ILL
     3 begin
     4 
     5 typedecl plf
     6 
     7 consts
     8   conj :: "[plf,plf] => plf"   (infixr "&" 35)
     9   disj :: "[plf,plf] => plf"   (infixr "|" 35)
    10   impl :: "[plf,plf] => plf"   (infixr ">" 35)
    11   eq :: "[plf,plf] => plf"   (infixr "=" 35)
    12   ff :: "plf"    ("ff")
    13 
    14   PL    :: "plf => o"      ("[* / _ / *]" [] 100)
    15 
    16 syntax
    17   "_NG" :: "plf => plf"   ("- _ " [50] 55)
    18 
    19 translations
    20 
    21   "[* A & B *]" == "[*A*] && [*B*]"
    22   "[* A | B *]" == "![*A*] ++ ![*B*]"
    23   "[* - A *]" == "[*A > ff*]"
    24   "[* ff *]" == "0"
    25   "[* A = B *]" => "[* (A > B) & (B > A) *]"
    26 
    27   "[* A > B *]" == "![*A*] -o [*B*]"
    28 
    29 (* another translations for linear implication:
    30   "[* A > B *]" == "!([*A*] -o [*B*])" *)
    31 
    32 (* from [kleene 52] pp 118,119 *)
    33 
    34 lemma k49a: "|- [* A > ( - ( - A)) *]"
    35   by best_safe
    36 
    37 lemma k49b: "|- [*( - ( - ( - A))) = ( - A)*]"
    38   by best_safe
    39 
    40 lemma k49c: "|- [* (A | - A) > ( - - A = A) *]"
    41   by best_safe
    42 
    43 lemma k50a: "|- [* - (A = - A) *]"
    44   by best_power
    45 
    46 lemma k51a: "|- [* - - (A | - A) *]"
    47   by best_safe
    48 
    49 lemma k51b: "|- [* - - (- - A > A) *]"
    50   by best_power
    51 
    52 lemma k56a: "|- [* (A | B) > - (- A & - B) *]"
    53   by best_safe
    54 
    55 lemma k56b: "|- [* (-A | B) > - (A & -B) *]"
    56   by best_safe
    57 
    58 lemma k57a: "|- [* (A & B) > - (-A | -B) *]"
    59   by best_safe
    60 
    61 lemma k57b: "|- [* (A & -B) > -(-A | B) *]"
    62   by best_power
    63 
    64 lemma k58a: "|- [* (A > B) > - (A & -B) *]"
    65   by best_safe
    66 
    67 lemma k58b: "|- [* (A > -B) = -(A & B) *]"
    68   by best_safe
    69 
    70 lemma k58c: "|- [* - (A & B) = (- - A > - B) *]"
    71   by best_safe
    72 
    73 lemma k58d: "|- [* (- - A > - B) = - - (-A | -B) *]"
    74   by best_safe
    75 
    76 lemma k58e: "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]"
    77   by best_safe
    78 
    79 lemma k58f: "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]"
    80   by best_safe
    81 
    82 lemma k58g: "|- [* (- -A > B) > - (A & -B) *]"
    83   by best_safe
    84 
    85 lemma k59a: "|- [* (-A | B) > (A > B) *]"
    86   by best_safe
    87 
    88 lemma k59b: "|- [* (A > B) > - - (-A | B) *]"
    89   by best_power
    90 
    91 lemma k59c: "|- [* (-A > B) > - -(A | B) *]"
    92   by best_power
    93 
    94 lemma k60a: "|- [* (A & B) > - (A > -B) *]"
    95   by best_safe
    96 
    97 lemma k60b: "|- [* (A & -B) > - (A > B) *]"
    98   by best_safe
    99 
   100 lemma k60c: "|- [* ( - - A & B) > - (A > -B) *]"
   101   by best_safe
   102 
   103 lemma k60d: "|- [* (- - A & - B) = - (A > B) *]"
   104   by best_safe
   105 
   106 lemma k60e: "|- [* - (A > B) = - (-A | B) *]"
   107   by best_safe
   108 
   109 lemma k60f: "|- [* - (-A | B) = - - (A & -B) *]"
   110   by best_safe
   111 
   112 lemma k60g: "|- [* - - (A > B) = - (A & -B) *]"
   113   by best_power
   114 
   115 lemma k60h: "|- [* - (A & -B) = (A > - -B) *]"
   116   by best_safe
   117 
   118 lemma k60i: "|- [* (A > - -B) = (- -A > - -B) *]"
   119   by best_safe
   120 
   121 lemma k61a: "|- [* (A | B) > (-A > B) *]"
   122   by best_safe
   123 
   124 lemma k61b: "|- [* - (A | B) = - (-A > B) *]"
   125   by best_power
   126 
   127 lemma k62a: "|- [* (-A | -B) > - (A & B) *]"
   128   by best_safe
   129 
   130 end