Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ILL.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      Sequents/ILL.thy
    Author:     Sara Kalvala and Valeria de Paiva
    Copyright   1995  University of Cambridge
*)

theory ILL
imports Sequents
begin

consts
  Trueprop       :: "two_seqi"

  tens :: "[o, o] \ o" (infixr "><" 35)
  limp :: "[o, o] \ o" (infixr "-o" 45)
  FShriek :: "o \ o" ("! _" [100] 1000)
  lconj :: "[o, o] \ o" (infixr "&&" 35)
  ldisj :: "[o, o] \ o" (infixr "++" 35)
  zero :: "o"                  ("0")
  top :: "o"                   ("1")
  eye :: "o"                   ("I")

  (* context manipulation *)

Context      :: "two_seqi"

  (* promotion rule *)

  PromAux :: "three_seqi"

syntax
  "_Trueprop" :: "single_seqe" ("((_)/ \ (_))" [6,6] 5)
  "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
  "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")

parse_translation \<open>
  [(\<^syntax_const>\<open>_Trueprop\<close>, K (single_tr \<^const_syntax>\<open>Trueprop\<close>)),
   (\<^syntax_const>\<open>_Context\<close>, K (two_seq_tr \<^const_syntax>\<open>Context\<close>)),
   (\<^syntax_const>\<open>_PromAux\<close>, K (three_seq_tr \<^const_syntax>\<open>PromAux\<close>))]
\<close>

print_translation \<open>
  [(\<^const_syntax>\<open>Trueprop\<close>, K (single_tr' \<^syntax_const>\<open>_Trueprop\<close>)),
   (\<^const_syntax>\<open>Context\<close>, K (two_seq_tr' \<^syntax_const>\<open>_Context\<close>)),
   (\<^const_syntax>\<open>PromAux\<close>, K (three_seq_tr' \<^syntax_const>\<open>_PromAux\<close>))]
\<close>

definition liff :: "[o, o] \ o" (infixr "o-o" 45)
  where "P o-o Q == (P -o Q) >< (Q -o P)"

definition aneg :: "o\o" ("~_")
  where "~A == A -o 0"

axiomatization where

identity:        "P \ P" and

zerol:           "$G, 0, $H \ A" and

  (* RULES THAT DO NOT DIVIDE CONTEXT *)

derelict:   "$F, A, $G \ C \ $F, !A, $G \ C" and
  (* unfortunately, this one removes !A  *)

contract:  "$F, !A, !A, $G \ C \ $F, !A, $G \ C" and

weaken:     "$F, $G \ C \ $G, !A, $F \ C" and
  (* weak form of weakening, in practice just to clean context *)
  (* weaken and contract not needed (CHECK)  *)

promote2:        "promaux{ || $H || B} \ $H \ !B" and
promote1:        "promaux{!A, $G || $H || B}
                  \<Longrightarrow> promaux {$G || $H, !A || B}" and
promote0:        "$G \ A \ promaux {$G || || A}" and

tensl:     "$H, A, B, $G \ C \ $H, A >< B, $G \ C" and

impr:      "A, $F \ B \ $F \ A -o B" and

conjr:           "\$F \ A ;
                 $F \<turnstile> B\<rbrakk>
                \<Longrightarrow> $F \<turnstile> (A && B)" and

conjll:          "$G, A, $H \ C \ $G, A && B, $H \ C" and

conjlr:          "$G, B, $H \ C \ $G, A && B, $H \ C" and

disjrl:          "$G \ A \ $G \ A ++ B" and
disjrr:          "$G \ B \ $G \ A ++ B" and
disjl:           "\$G, A, $H \ C ;
                   $G, B, $H \<turnstile> C\<rbrakk>
                 \<Longrightarrow> $G, A ++ B, $H \<turnstile> C" and

      (* RULES THAT DIVIDE CONTEXT *)

tensr:           "\$F, $J :=: $G;
                   $F \<turnstile> A ;
                   $J \<turnstile> B\<rbrakk>
                     \<Longrightarrow> $G \<turnstile> A >< B" and

impl:            "\$G, $F :=: $J, $H ;
                   B, $F \<turnstile> C ;
                   $G \<turnstile> A\<rbrakk>
                     \<Longrightarrow> $J, A -o B, $H \<turnstile> C" and

cut: "\ $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
        $H1, $H2, $H3, $H4 \<turnstile> A ;
        $J1, $J2, A, $J3, $J4 \<turnstile> B\<rbrakk> \<Longrightarrow> $F \<turnstile> B" and

  (* CONTEXT RULES *)

context1:     "$G :=: $G" and
context2:     "$F, $G :=: $H, !A, $G \ $F, A, $G :=: $H, !A, $G" and
context3:     "$F, $G :=: $H, $J \ $F, A, $G :=: $H, A, $J" and
context4a:    "$F :=: $H, $G \ $F :=: $H, !A, $G" and
context4b:    "$F, $H :=: $G \ $F, !A, $H :=: $G" and
context5:     "$F, $G :=: $H \ $G, $F :=: $H"

text "declarations for lazy classical reasoning:"
lemmas [safe] =
  context3
  context2
  promote0
  disjl
  conjr
  tensl
lemmas [unsafe] =
  context4b
  context4a
  context1
  promote2
  promote1
  weaken
  derelict
  impl
  tensr
  impr
  disjrr
  disjrl
  conjlr
  conjll
  zerol
  identity

lemma aux_impl: "$F, $G \ A \ $F, !(A -o B), $G \ B"
  apply (rule derelict)
  apply (rule impl)
  apply (rule_tac [2] identity)
  apply (rule context1)
  apply assumption
  done

lemma conj_lemma: " $F, !A, !B, $G \ C \ $F, !(A && B), $G \ C"
  apply (rule contract)
  apply (rule_tac A = " (!A) >< (!B) " in cut)
  apply (rule_tac [2] tensr)
  prefer 3
  apply (subgoal_tac "! (A && B) \ !A")
  apply assumption
  apply best
  prefer 3
  apply (subgoal_tac "! (A && B) \ !B")
  apply assumption
  apply best
  apply (rule_tac [2] context1)
  apply (rule_tac [2] tensl)
  prefer 2 apply assumption
  apply (rule context3)
  apply (rule context3)
  apply (rule context1)
  done

lemma impr_contract: "!A, !A, $G \ B \ $G \ (!A) -o B"
  apply (rule impr)
  apply (rule contract)
  apply assumption
  done

lemma impr_contr_der: "A, !A, $G \ B \ $G \ (!A) -o B"
  apply (rule impr)
  apply (rule contract)
  apply (rule derelict)
  apply assumption
  done

lemma contrad1: "$F, (!B) -o 0, $G, !B, $H \ A"
  apply (rule impl)
  apply (rule_tac [3] identity)
  apply (rule context3)
  apply (rule context1)
  apply (rule zerol)
  done

lemma contrad2: "$F, !B, $G, (!B) -o 0, $H \ A"
  apply (rule impl)
  apply (rule_tac [3] identity)
  apply (rule context3)
  apply (rule context1)
  apply (rule zerol)
  done

lemma ll_mp: "A -o B, A \ B"
  apply (rule impl)
  apply (rule_tac [2] identity)
  apply (rule_tac [2] identity)
  apply (rule context1)
  done

lemma mp_rule1: "$F, B, $G, $H \ C \ $F, A, $G, A -o B, $H \ C"
  apply (rule_tac A = "B" in cut)
  apply (rule_tac [2] ll_mp)
  prefer 2 apply (assumption)
  apply (rule context3)
  apply (rule context3)
  apply (rule context1)
  done

lemma mp_rule2: "$F, B, $G, $H \ C \ $F, A -o B, $G, A, $H \ C"
  apply (rule_tac A = "B" in cut)
  apply (rule_tac [2] ll_mp)
  prefer 2 apply (assumption)
  apply (rule context3)
  apply (rule context3)
  apply (rule context1)
  done

lemma or_to_and: "!((!(A ++ B)) -o 0) \ !( ((!A) -o 0) && ((!B) -o 0))"
  by best

lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G \ C \
          $F, !((!(A ++ B)) -o 0), $G \<turnstile> C"
  apply (rule cut)
  apply (rule_tac [2] or_to_and)
  prefer 2 apply (assumption)
  apply (rule context3)
  apply (rule context1)
  done

lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) \ (!(A && B)) -o C"
  apply (rule impr)
  apply (rule conj_lemma)
  apply (rule disjl)
  apply (rule mp_rule1, best)+
  done

lemma not_imp: "!A, !((!B) -o 0) \ (!((!A) -o B)) -o 0"
  by best

lemma a_not_a: "!A -o (!A -o 0) \ !A -o 0"
  apply (rule impr)
  apply (rule contract)
  apply (rule impl)
  apply (rule_tac [3] identity)
  apply (rule context1)
  apply best
  done

lemma a_not_a_rule: "$J1, !A -o 0, $J2 \ B \ $J1, !A -o (!A -o 0), $J2 \ B"
  apply (rule_tac A = "!A -o 0" in cut)
  apply (rule_tac [2] a_not_a)
  prefer 2 apply assumption
  apply best
  done

ML \<open>
  val safe_pack =
    \<^context>
    |> fold_rev Cla.add_safe @{thms conj_lemma ll_mp contrad1
        contrad2 mp_rule1 mp_rule2 o_a_rule a_not_a_rule}
    |> Cla.add_unsafe @{thm aux_impl}
    |> Cla.get_pack;

  val power_pack =
    Cla.put_pack safe_pack \<^context>
    |> Cla.add_unsafe @{thm impr_contr_der}
    |> Cla.get_pack;
\<close>

method_setup best_safe =
  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack safe_pack ctxt)))\<close>

method_setup best_power =
  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack power_pack ctxt)))\<close>

(* Some examples from Troelstra and van Dalen *)

lemma "!((!A) -o ((!B) -o 0)) \ (!(A && B)) -o 0"
  by best_safe

lemma "!((!(A && B)) -o 0) \ !((!A) -o ((!B) -o 0))"
  by best_safe

lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) \
        (!A) -o ( (!  ((!B) -o 0)) -o 0)"
  by best_safe

lemma "!( (!A) -o ( (! ((!B) -o 0)) -o 0) ) \
          (!((! ((!A) -o B) ) -o 0)) -o 0"
  by best_power

end

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.