src/FOL/ex/Miniscope.thy

tuned;

(*  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 \<open>Negation Normal Form\<close>

subsubsection \<open>de Morgan laws\<close>

lemma demorgans:
  "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
  "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q"
  "\<not> \<not> P \<longleftrightarrow> P"
  "\<And>P. \<not> (\<forall>x. P(x)) \<longleftrightarrow> (\<exists>x. \<not> P(x))"
  "\<And>P. \<not> (\<exists>x. P(x)) \<longleftrightarrow> (\<forall>x. \<not> P(x))"
  by blast+

(*** Removal of --> and <-> (positive and negative occurrences) ***)
(*Last one is important for computing a compact CNF*)
lemma nnf_simps:
  "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
  "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)"
  "(P \<longleftrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q) \<and> (\<not> Q \<or> P)"
  "\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<or> Q) \<and> (\<not> P \<or> \<not> Q)"
  by blast+


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

subsubsection \<open>Pushing in the existential quantifiers\<close>

lemma ex_simps:
  "(\<exists>x. P) \<longleftrightarrow> P"
  "\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
  "\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
  "\<And>P Q. (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
  "\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
  "\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
  by blast+


subsubsection \<open>Pushing in the universal quantifiers\<close>

lemma all_simps:
  "(\<forall>x. P) \<longleftrightarrow> P"
  "\<And>P Q. (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
  "\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
  "\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
  "\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
  "\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))"
  by blast+

lemmas mini_simps = demorgans nnf_simps ex_simps all_simps

ML \<open>
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);
\<close>

end