Theory Propositional

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