Quelle  Miniscope.thy

(*  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 (🍋 |> Simplifier.add_simps @{thms mini_simps});
 fun mini_tac ctxt =
  resolve_tac ctxt @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
 ›

end