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

section ‹Classical sequent calculus: examples with propositional connectives›

theory Propositional
imports "../LK"
begin

text "absorptive laws of ∧ and ∨"

lemma "⊨ P ∧ P ⟷ P"
  by fast_prop

lemma "⊨ P ∨ P ⟷ P"
  by fast_prop


text "commutative laws of ∧ and ∨"

lemma "⊨ P ∧ Q ⟷ Q ∧ P"
  by fast_prop

lemma "⊨ P ∨ Q ⟷ Q ∨ P"
  by fast_prop


text "associative laws of ∧ and ∨"

lemma "⊨ (P ∧ Q) ∧ R ⟷ P ∧ (Q ∧ R)"
  by fast_prop

lemma "⊨ (P ∨ Q) ∨ R ⟷ P ∨ (Q ∨ R)"
  by fast_prop


text "distributive laws of ∧ and ∨"

lemma "⊨ (P ∧ Q) ∨ R ⟷ (P ∨ R) ∧ (Q ∨ R)"
  by fast_prop

lemma "⊨ (P ∨ Q) ∧ R ⟷ (P ∧ R) ∨ (Q ∧ R)"
  by fast_prop


text "Laws involving implication"

lemma "⊨ (P ∨ Q ⟶ R) ⟷ (P ⟶ R) ∧ (Q ⟶ R)"
  by fast_prop

lemma "⊨ (P ∧ Q ⟶ R) ⟷ (P ⟶ (Q ⟶ R))"
  by fast_prop

lemma "⊨ (P ⟶ Q ∧ R) ⟷ (P ⟶ Q) ∧ (P ⟶ R)"
  by fast_prop


text "Classical theorems"

lemma "⊨ P ∨ Q ⟶ P ∨ ¬ P ∧ Q"
  by fast_prop

lemma "⊨ (P ⟶ Q) ∧ (¬ P ⟶ R) ⟶ (P ∧ Q ∨ R)"
  by fast_prop

lemma "⊨ P ∧ Q ∨ ¬ P ∧ R ⟷ (P ⟶ Q) ∧ (¬ P ⟶ R)"
  by fast_prop

lemma "⊨ (P ⟶ Q) ∨ (P ⟶ R) ⟷ (P ⟶ Q ∨ R)"
  by fast_prop


(*If and only if*)

lemma "⊨ (P ⟷ Q) ⟷ (Q ⟷ P)"
  by fast_prop

lemma "⊨ ¬ (P ⟷ ¬ P)"
  by fast_prop


(*Sample problems from 
  F. J. Pelletier, 
  Seventy-Five Problems for Testing Automatic Theorem Provers,
  J. Automated Reasoning 2 (1986), 191-216.
  Errata, JAR 4 (1988), 236-236.
*)

(*1*)
lemma "⊨ (P ⟶ Q) ⟷ (¬ Q ⟶ ¬ P)"
  by fast_prop

(*2*)
lemma "⊨ ¬ ¬ P ⟷ P"
  by fast_prop

(*3*)
lemma "⊨ ¬ (P ⟶ Q) ⟶ (Q ⟶ P)"
  by fast_prop

(*4*)
lemma "⊨ (¬ P ⟶ Q) ⟷ (¬ Q ⟶ P)"
  by fast_prop

(*5*)
lemma "⊨ ((P ∨ Q) ⟶ (P ∨ R)) ⟶ (P ∨ (Q ⟶ R))"
  by fast_prop

(*6*)
lemma "⊨ P ∨ ¬ P"
  by fast_prop

(*7*)
lemma "⊨ P ∨ ¬ ¬ ¬ P"
  by fast_prop

(*8.  Peirce's law*)
lemma "⊨ ((P ⟶ Q) ⟶ P) ⟶ P"
  by fast_prop

(*9*)
lemma "⊨ ((P ∨ Q) ∧ (¬ P ∨ Q) ∧ (P ∨ ¬ Q)) ⟶ ¬ (¬ P ∨ ¬ Q)"
  by fast_prop

(*10*)
lemma "Q ⟶ R, R ⟶ P ∧ Q, P ⟶ (Q ∨ R) ⊨ P ⟷ Q"
  by fast_prop

(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
lemma "⊨ P ⟷ P"
  by fast_prop

(*12.  "Dijkstra's law"*)
lemma "⊨ ((P ⟷ Q) ⟷ R) ⟷ (P ⟷ (Q ⟷ R))"
  by fast_prop

(*13.  Distributive law*)
lemma "⊨ P ∨ (Q ∧ R) ⟷ (P ∨ Q) ∧ (P ∨ R)"
  by fast_prop

(*14*)
lemma "⊨ (P ⟷ Q) ⟷ ((Q ∨ ¬ P) ∧ (¬ Q ∨ P))"
  by fast_prop

(*15*)
lemma "⊨ (P ⟶ Q) ⟷ (¬ P ∨ Q)"
  by fast_prop

(*16*)
lemma "⊨ (P ⟶ Q) ∨ (Q ⟶ P)"
  by fast_prop

(*17*)
lemma "⊨ ((P ∧ (Q ⟶ R)) ⟶ S) ⟷ ((¬ P ∨ Q ∨ S) ∧ (¬ P ∨ ¬ R ∨ S))"
  by fast_prop

end