Theory Miniscope

theory Miniscope
imports FOL
(*  Title:      FOL/ex/Miniscope.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

Classical First-Order Logic.
Conversion to nnf/miniscope format: pushing quantifiers in.
Demonstration of formula rewriting by proof.
*)

theory Miniscope
imports FOL
begin

lemmas ccontr = FalseE [THEN classical]

subsection ‹Negation Normal Form›

subsubsection ‹de Morgan laws›

lemma demorgans:
  "¬ (P ∧ Q) ⟷ ¬ P ∨ ¬ Q"
  "¬ (P ∨ Q) ⟷ ¬ P ∧ ¬ Q"
  "¬ ¬ P ⟷ P"
  "⋀P. ¬ (∀x. P(x)) ⟷ (∃x. ¬ P(x))"
  "⋀P. ¬ (∃x. P(x)) ⟷ (∀x. ¬ P(x))"
  by blast+

(*** Removal of --> and <-> (positive and negative occurrences) ***)
(*Last one is important for computing a compact CNF*)
lemma nnf_simps:
  "(P ⟶ Q) ⟷ (¬ P ∨ Q)"
  "¬ (P ⟶ Q) ⟷ (P ∧ ¬ Q)"
  "(P ⟷ Q) ⟷ (¬ P ∨ Q) ∧ (¬ Q ∨ P)"
  "¬ (P ⟷ Q) ⟷ (P ∨ Q) ∧ (¬ P ∨ ¬ Q)"
  by blast+


(* BEWARE: rewrite rules for <-> can confuse the simplifier!! *)

subsubsection ‹Pushing in the existential quantifiers›

lemma ex_simps:
  "(∃x. P) ⟷ P"
  "⋀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)) ⟷ (∃x. P(x)) ∨ (∃x. Q(x))"
  "⋀P Q. (∃x. P(x) ∨ Q) ⟷ (∃x. P(x)) ∨ Q"
  "⋀P Q. (∃x. P ∨ Q(x)) ⟷ P ∨ (∃x. Q(x))"
  by blast+


subsubsection ‹Pushing in the universal quantifiers›

lemma all_simps:
  "(∀x. P) ⟷ P"
  "⋀P Q. (∀x. P(x) ∧ Q(x)) ⟷ (∀x. P(x)) ∧ (∀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 blast+

lemmas mini_simps = demorgans nnf_simps ex_simps all_simps

ML ‹
val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps});
fun mini_tac ctxt =
  resolve_tac ctxt @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
›

end