Theory Miniscope

(*  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 demorgans1:
  ¬ (P  Q)  ¬ P  ¬ Q
  ¬ (P  Q)  ¬ P  ¬ Q
  ¬ ¬ P  P
  by blast+

lemma demorgans2:
  P. ¬ (x. P(x))  (x. ¬ P(x))
  P. ¬ (x. P(x))  (x. ¬ P(x))
  by blast+

lemmas demorgans = demorgans1 demorgans2

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