Quelle  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')\
               ==> (P, $H ⊨ $F) ≡ (P', $H' ⊨ $F')"


subsection ‹Rewrite rules›

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 ‹Miniscoping: pushing quantifiers in›

text ‹
  We do NOT distribute of ∀ over ∧, or dually that of ∃ over ∨
  Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
  show that this step can increase proof length!
›

text ‹existential miniscoping›
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 ‹universal miniscoping›
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 ‹These are NOT supplied by default!›
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 ‹Named rewrite rules›

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 ‹
     REPEAT (resolve_tac 🍋 @{thms cut} 1 THEN
       DEPTH_SOLVE_1
         (resolve_tac 🍋 [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
           Cla.safe_tac 🍋 1)›)
  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 ‹
     REPEAT (resolve_tac 🍋 @{thms cut} 1 THEN
       DEPTH_SOLVE_1
         (resolve_tac 🍋 [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
           Cla.safe_tac 🍋 1)›)
  done

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

ML_file ‹simpdata.ML›
setup ‹map_theory_simpset (put_simpset LK_ss)›
setup ‹Simplifier.method_setup []›


text ‹To create substitution rules›

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