Quelle  LK.thy

(*  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