# Theory LK

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

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)"

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)"

lemma not_simps:
"⊢ ¬ False ⟷ True"
"⊢ ¬ True ⟷ False"

lemma imp_simps:
"⊢ (P ⟶ False) ⟷ ¬ P"
"⊢ (P ⟶ True) ⟷ True"
"⊢ (False ⟶ P) ⟷ True"
"⊢ (True ⟶ P) ⟷ P"
"⊢ (P ⟶ P) ⟷ True"
"⊢ (P ⟶ ¬ P) ⟷ ¬ P"

lemma iff_simps:
"⊢ (True ⟷ P) ⟷ P"
"⊢ (P ⟷ True) ⟷ P"
"⊢ (P ⟷ P) ⟷ True"
"⊢ (False ⟷ P) ⟷ ¬ P"
"⊢ (P ⟷ False) ⟷ ¬ P"

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)"

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))"

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))"

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)"

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)"

subsection ‹Named rewrite rules›

lemma conj_commute: "⊢ P ∧ Q ⟷ Q ∧ P"
and conj_left_commute: "⊢ P ∧ (Q ∧ R) ⟷ Q ∧ (P ∧ R)"

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)"

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)"

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"

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 (rule_tac P = "¬ Q" in cut)
prefer 2
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
```