# HG changeset patch
# User chaieb
# Date 1179594522 -7200
# Node ID 6c72943a71b1d61575520a73c1bfd128feb68caf
# Parent  65b4f545a76fceaebf759011db4adb586c275c3a
added a set of NNF normalization lemmas and nnf_conv

diff -r 65b4f545a76f -r 6c72943a71b1 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat May 19 19:08:06 2007 +0200
+++ b/src/HOL/HOL.thy	Sat May 19 19:08:42 2007 +0200
@@ -1408,6 +1408,12 @@
 
 lemmas eq_sym_conv = eq_commute
 
+lemma nnf_simps:
+  "(\<not>(P \<and> Q)) = (\<not> P \<or> \<not> Q)" "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)" 
+  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))" 
+  "(\<not> \<not>(P)) = P"
+by blast+
+
 
 subsection {* Basic ML bindings *}
 
@@ -1521,6 +1527,8 @@
 val theI = thm "theI"
 val theI' = thm "theI'"
 val True_implies_equals = thm "True_implies_equals";
+val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms @ @{thms "nnf_simps"})
+
 *}
 
 end