# 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
```