Theory ILL_predlog

theory ILL_predlog
imports ILL
begin

typedecl plf
consts "PL" :: "plf ⇒ o"

syntax
  "_PL" :: "plf ⇒ o"      (‹[* / _ / *]› [] 100)
  "_conj" :: "[plf,plf] ⇒ plf"   (infixr ‹&› 35)
  "_disj" :: "[plf,plf] ⇒ plf"   (infixr ‹|› 35)
  "_impl" :: "[plf,plf] ⇒ plf"   (infixr ‹>› 35)
  "_eq" :: "[plf,plf] ⇒ plf"   (infixr ‹=› 35)
  "_ff" :: "plf"    (‹ff›)
  "_NG" :: "plf ⇒ plf"   (‹- _ › [50] 55)
translations
  "[* A & B *]" ⇌ "[*A*] && [*B*]"
  "[* A | B *]" ⇌ "![*A*] ++ ![*B*]"
  "[* - A *]" ⇌ "[*A > ff*]"
  "[* ff *]" ⇌ "0"
  "[* A = B *]" ⇀ "[* (A > B) & (B > A) *]"

  "[* A > B *]" ⇌ "![*A*] -o [*B*]"
  "_PL" ⇌ "CONST PL"

(* another translations for linear implication:
  "[* A > B *]" == "!([*A*] -o [*B*])" *)

(* from [kleene 52] pp 118,119 *)

lemma k49a: "⊢ [* A > ( - ( - A)) *]"
  by best_safe

lemma k49b: "⊢ [*( - ( - ( - A))) = ( - A)*]"
  by best_safe

lemma k49c: "⊢ [* (A | - A) > ( - - A = A) *]"
  by best_safe

lemma k50a: "⊢ [* - (A = - A) *]"
  by best_power

lemma k51a: "⊢ [* - - (A | - A) *]"
  by best_safe

lemma k51b: "⊢ [* - - (- - A > A) *]"
  by best_power

lemma k56a: "⊢ [* (A | B) > - (- A & - B) *]"
  by best_safe

lemma k56b: "⊢ [* (-A | B) > - (A & -B) *]"
  by best_safe

lemma k57a: "⊢ [* (A & B) > - (-A | -B) *]"
  by best_safe

lemma k57b: "⊢ [* (A & -B) > -(-A | B) *]"
  by best_power

lemma k58a: "⊢ [* (A > B) > - (A & -B) *]"
  by best_safe

lemma k58b: "⊢ [* (A > -B) = -(A & B) *]"
  by best_safe

lemma k58c: "⊢ [* - (A & B) = (- - A > - B) *]"
  by best_safe

lemma k58d: "⊢ [* (- - A > - B) = - - (-A | -B) *]"
  by best_safe

lemma k58e: "! [* - -B > B *] ⊢ [* (- -A > B) = (A > B) *]"
  by best_safe

lemma k58f: "! [* - -B > B *] ⊢ [* (A > B) = - (A & -B) *]"
  by best_safe

lemma k58g: "⊢ [* (- -A > B) > - (A & -B) *]"
  by best_safe

lemma k59a: "⊢ [* (-A | B) > (A > B) *]"
  by best_safe

lemma k59b: "⊢ [* (A > B) > - - (-A | B) *]"
  by best_power

lemma k59c: "⊢ [* (-A > B) > - -(A | B) *]"
  by best_power

lemma k60a: "⊢ [* (A & B) > - (A > -B) *]"
  by best_safe

lemma k60b: "⊢ [* (A & -B) > - (A > B) *]"
  by best_safe

lemma k60c: "⊢ [* ( - - A & B) > - (A > -B) *]"
  by best_safe

lemma k60d: "⊢ [* (- - A & - B) = - (A > B) *]"
  by best_safe

lemma k60e: "⊢ [* - (A > B) = - (-A | B) *]"
  by best_safe

lemma k60f: "⊢ [* - (-A | B) = - - (A & -B) *]"
  by best_safe

lemma k60g: "⊢ [* - - (A > B) = - (A & -B) *]"
  by best_power

lemma k60h: "⊢ [* - (A & -B) = (A > - -B) *]"
  by best_safe

lemma k60i: "⊢ [* (A > - -B) = (- -A > - -B) *]"
  by best_safe

lemma k61a: "⊢ [* (A | B) > (-A > B) *]"
  by best_safe

lemma k61b: "⊢ [* - (A | B) = - (-A > B) *]"
  by best_power

lemma k62a: "⊢ [* (-A | -B) > - (A & B) *]"
  by best_safe

end