Theory LK

(*  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 ⊢ and ⟹, 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 \<^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)›)
  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 \<^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)›)
  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