SSL LK.thy Sprache: Isabelle

(*  Title:      Sequents/LK.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
link between \<turnstile> and \<Longrightarrow>, needed for instance to prove imp_cong.

Axiom left_cong allows the simplifier to use left-side formulas.  Ideally it
should be derived from lower-level axioms.

CANNOT be added to LK0.thy because modal logic is built upon it, and
various modal rules would become inconsistent.
*)

theory LK
imports LK0
begin

axiomatization where
  monotonic:  "($H \ P \ $H \ Q) \ $H, P \ Q" and

  left_cong:  "\P == P'; \ P' \ ($H \ $F) \ ($H' \ $F')\
               \<Longrightarrow> (P, $H \<turnstile> $F) \<equiv> (P', $H' \<turnstile> $F')"

subsection \<open>Rewrite rules\<close>

lemma conj_simps:
  "\ P \ True \ P"
  "\ True \ P \ P"
  "\ P \ False \ False"
  "\ False \ P \ False"
  "\ P \ P \ P"
  "\ P \ P \ Q \ P \ Q"
  "\ P \ \ P \ False"
  "\ \ P \ P \ False"
  "\ (P \ Q) \ R \ P \ (Q \ R)"
  by (fast add!: subst)+

lemma disj_simps:
  "\ P \ True \ True"
  "\ True \ P \ True"
  "\ P \ False \ P"
  "\ False \ P \ P"
  "\ P \ P \ P"
  "\ P \ P \ Q \ P \ Q"
  "\ (P \ Q) \ R \ P \ (Q \ R)"
  by (fast add!: subst)+

lemma not_simps:
  "\ \ False \ True"
  "\ \ True \ False"
  by (fast add!: subst)+

lemma imp_simps:
  "\ (P \ False) \ \ P"
  "\ (P \ True) \ True"
  "\ (False \ P) \ True"
  "\ (True \ P) \ P"
  "\ (P \ P) \ True"
  "\ (P \ \ P) \ \ P"
  by (fast add!: subst)+

lemma iff_simps:
  "\ (True \ P) \ P"
  "\ (P \ True) \ P"
  "\ (P \ P) \ True"
  "\ (False \ P) \ \ P"
  "\ (P \ False) \ \ P"
  by (fast add!: subst)+

lemma quant_simps:
  "\P. \ (\x. P) \ P"
  "\P. \ (\x. x = t \ P(x)) \ P(t)"
  "\P. \ (\x. t = x \ P(x)) \ P(t)"
  "\P. \ (\x. P) \ P"
  "\P. \ (\x. x = t \ P(x)) \ P(t)"
  "\P. \ (\x. t = x \ P(x)) \ P(t)"
  by (fast add!: subst)+

subsection \<open>Miniscoping: pushing quantifiers in\<close>

text \<open>
  We do NOT distribute of \<forall> over \<and>, or dually that of \<exists> over \<or>
  Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
  show that this step can increase proof length!
\<close>

text \<open>existential miniscoping\<close>
lemma ex_simps:
  "\P Q. \ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
  "\P Q. \ (\x. P \ Q(x)) \ P \ (\x. Q(x))"
  "\P Q. \ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
  "\P Q. \ (\x. P \ Q(x)) \ P \ (\x. Q(x))"
  "\P Q. \ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
  "\P Q. \ (\x. P \ Q(x)) \ P \ (\x. Q(x))"
  by (fast add!: subst)+

text \<open>universal miniscoping\<close>
lemma all_simps:
  "\P Q. \ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
  "\P Q. \ (\x. P \ Q(x)) \ P \ (\x. Q(x))"
  "\P Q. \ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
  "\P Q. \ (\x. P \ Q(x)) \ P \ (\x. Q(x))"
  "\P Q. \ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
  "\P Q. \ (\x. P \ Q(x)) \ P \ (\x. Q(x))"
  by (fast add!: subst)+

text \<open>These are NOT supplied by default!\<close>
lemma distrib_simps:
  "\ P \ (Q \ R) \ P \ Q \ P \ R"
  "\ (Q \ R) \ P \ Q \ P \ R \ P"
  "\ (P \ Q \ R) \ (P \ R) \ (Q \ R)"
  by (fast add!: subst)+

lemma P_iff_F: "\ \ P \ \ (P \ False)"
  apply (erule thinR [THEN cut])
  apply fast
  done

lemmas iff_reflection_F = P_iff_F [THEN iff_reflection]

lemma P_iff_T: "\ P \ \ (P \ True)"
  apply (erule thinR [THEN cut])
  apply fast
  done

lemmas iff_reflection_T = P_iff_T [THEN iff_reflection]

lemma LK_extra_simps:
  "\ P \ \ P"
  "\ \ P \ P"
  "\ \ \ P \ P"
  "\ (\ P \ P) \ P"
  "\ (\ P \ \ Q) \ (P \ Q)"
  by (fast add!: subst)+

subsection \<open>Named rewrite rules\<close>

lemma conj_commute: "\ P \ Q \ Q \ P"
  and conj_left_commute: "\ P \ (Q \ R) \ Q \ (P \ R)"
  by (fast add!: subst)+

lemmas conj_comms = conj_commute conj_left_commute

lemma disj_commute: "\ P \ Q \ Q \ P"
  and disj_left_commute: "\ P \ (Q \ R) \ Q \ (P \ R)"
  by (fast add!: subst)+

lemmas disj_comms = disj_commute disj_left_commute

lemma conj_disj_distribL: "\ P \ (Q \ R) \ (P \ Q \ P \ R)"
  and conj_disj_distribR: "\ (P \ Q) \ R \ (P \ R \ Q \ R)"

  and disj_conj_distribL: "\ P \ (Q \ R) \ (P \ Q) \ (P \ R)"
  and disj_conj_distribR: "\ (P \ Q) \ R \ (P \ R) \ (Q \ R)"

  and imp_conj_distrib: "\ (P \ (Q \ R)) \ (P \ Q) \ (P \ R)"
  and imp_conj: "\ ((P \ Q) \ R) \ (P \ (Q \ R))"
  and imp_disj: "\ (P \ Q \ R) \ (P \ R) \ (Q \ R)"

  and imp_disj1: "\ (P \ Q) \ R \ (P \ Q \ R)"
  and imp_disj2: "\ Q \ (P \ R) \ (P \ Q \ R)"

  and de_Morgan_disj: "\ (\ (P \ Q)) \ (\ P \ \ Q)"
  and de_Morgan_conj: "\ (\ (P \ Q)) \ (\ P \ \ Q)"

  and not_iff: "\ \ (P \ Q) \ (P \ \ Q)"
  by (fast add!: subst)+

lemma imp_cong:
  assumes p1: "\ P \ P'"
    and p2: "\ P' \ \ Q \ Q'"
  shows "\ (P \ Q) \ (P' \ Q')"
  apply (lem p1)
  apply safe
   apply (tactic \<open>
     REPEAT (resolve_tac \<^context> @{thms cut} 1 THEN
       DEPTH_SOLVE_1
         (resolve_tac \<^context> [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
           Cla.safe_tac \<^context> 1)\<close>)
  done

lemma conj_cong:
  assumes p1: "\ P \ P'"
    and p2: "\ P' \ \ Q \ Q'"
  shows "\ (P \ Q) \ (P' \ Q')"
  apply (lem p1)
  apply safe
   apply (tactic \<open>
     REPEAT (resolve_tac \<^context> @{thms cut} 1 THEN
       DEPTH_SOLVE_1
         (resolve_tac \<^context> [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
           Cla.safe_tac \<^context> 1)\<close>)
  done

lemma eq_sym_conv: "\ x = y \ y = x"
  by (fast add!: subst)

ML_file \<open>simpdata.ML\<close>
setup \<open>map_theory_simpset (put_simpset LK_ss)\<close>
setup \<open>Simplifier.method_setup []\<close>

text \<open>To create substitution rules\<close>

lemma eq_imp_subst: "\ a = b \ $H, A(a), $G \ $E, A(b), $F"
  by simp

lemma split_if: "\ P(if Q then x else y) \ ((Q \ P(x)) \ (\ Q \ P(y)))"
  apply (rule_tac P = Q in cut)
   prefer 2
   apply (simp add: if_P)
  apply (rule_tac P = "\ Q" in cut)
   prefer 2
   apply (simp add: if_not_P)
  apply fast
  done

lemma if_cancel: "\ (if P then x else x) = x"
  apply (lem split_if)
  apply fast
  done

lemma if_eq_cancel: "\ (if x = y then y else x) = x"
  apply (lem split_if)
  apply safe
  apply (rule symL)
  apply (rule basic)
  done

end

quality100%

¤ Dauer der Verarbeitung: 0.11 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.