Quelle ILL_predlog.thy Sprache: Isabelle

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"    (\<open>ff\<close>)
  "_NG" :: "plf \ plf" (\- _ \ [50] 55)
translations
  "[* A & B *]" \<rightleftharpoons> "[*A*] && [*B*]"
  "[* A | B *]" \<rightleftharpoons> "![*A*] ++ ![*B*]"
  "[* - A *]" \<rightleftharpoons> "[*A > ff*]"
  "[* ff *]" \<rightleftharpoons> "0"
  "[* A = B *]" \<rightharpoonup> "[* (A > B) & (B > A) *]"

  "[* A > B *]" \<rightleftharpoons> "![*A*] -o [*B*]"
  "_PL" \<rightleftharpoons> "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

quality98%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.