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