1theory ILL_predlog 2imports ILL 3begin 4 5typedecl plf 6 7consts 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 16syntax 17 "_NG" :: "plf \<Rightarrow> plf" ("- _ " [50] 55) 18 19translations 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 33lemma k49a: "\<turnstile> [* A > ( - ( - A)) *]" 34 by best_safe 35 36lemma k49b: "\<turnstile> [*( - ( - ( - A))) = ( - A)*]" 37 by best_safe 38 39lemma k49c: "\<turnstile> [* (A | - A) > ( - - A = A) *]" 40 by best_safe 41 42lemma k50a: "\<turnstile> [* - (A = - A) *]" 43 by best_power 44 45lemma k51a: "\<turnstile> [* - - (A | - A) *]" 46 by best_safe 47 48lemma k51b: "\<turnstile> [* - - (- - A > A) *]" 49 by best_power 50 51lemma k56a: "\<turnstile> [* (A | B) > - (- A & - B) *]" 52 by best_safe 53 54lemma k56b: "\<turnstile> [* (-A | B) > - (A & -B) *]" 55 by best_safe 56 57lemma k57a: "\<turnstile> [* (A & B) > - (-A | -B) *]" 58 by best_safe 59 60lemma k57b: "\<turnstile> [* (A & -B) > -(-A | B) *]" 61 by best_power 62 63lemma k58a: "\<turnstile> [* (A > B) > - (A & -B) *]" 64 by best_safe 65 66lemma k58b: "\<turnstile> [* (A > -B) = -(A & B) *]" 67 by best_safe 68 69lemma k58c: "\<turnstile> [* - (A & B) = (- - A > - B) *]" 70 by best_safe 71 72lemma k58d: "\<turnstile> [* (- - A > - B) = - - (-A | -B) *]" 73 by best_safe 74 75lemma k58e: "! [* - -B > B *] \<turnstile> [* (- -A > B) = (A > B) *]" 76 by best_safe 77 78lemma k58f: "! [* - -B > B *] \<turnstile> [* (A > B) = - (A & -B) *]" 79 by best_safe 80 81lemma k58g: "\<turnstile> [* (- -A > B) > - (A & -B) *]" 82 by best_safe 83 84lemma k59a: "\<turnstile> [* (-A | B) > (A > B) *]" 85 by best_safe 86 87lemma k59b: "\<turnstile> [* (A > B) > - - (-A | B) *]" 88 by best_power 89 90lemma k59c: "\<turnstile> [* (-A > B) > - -(A | B) *]" 91 by best_power 92 93lemma k60a: "\<turnstile> [* (A & B) > - (A > -B) *]" 94 by best_safe 95 96lemma k60b: "\<turnstile> [* (A & -B) > - (A > B) *]" 97 by best_safe 98 99lemma k60c: "\<turnstile> [* ( - - A & B) > - (A > -B) *]" 100 by best_safe 101 102lemma k60d: "\<turnstile> [* (- - A & - B) = - (A > B) *]" 103 by best_safe 104 105lemma k60e: "\<turnstile> [* - (A > B) = - (-A | B) *]" 106 by best_safe 107 108lemma k60f: "\<turnstile> [* - (-A | B) = - - (A & -B) *]" 109 by best_safe 110 111lemma k60g: "\<turnstile> [* - - (A > B) = - (A & -B) *]" 112 by best_power 113 114lemma k60h: "\<turnstile> [* - (A & -B) = (A > - -B) *]" 115 by best_safe 116 117lemma k60i: "\<turnstile> [* (A > - -B) = (- -A > - -B) *]" 118 by best_safe 119 120lemma k61a: "\<turnstile> [* (A | B) > (-A > B) *]" 121 by best_safe 122 123lemma k61b: "\<turnstile> [* - (A | B) = - (-A > B) *]" 124 by best_power 125 126lemma k62a: "\<turnstile> [* (-A | -B) > - (A & B) *]" 127 by best_safe 128 129end 130