src/HOL/Groebner_Basis.thy
changeset 54251 adea9f6986b2
parent 48891 c0eafbd55de3
child 55178 318cd8ac1817
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Nov 04 20:10:09 2013 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Nov 04 20:10:10 2013 +0100
     1.3 @@ -10,20 +10,23 @@
     1.4  
     1.5  subsection {* Groebner Bases *}
     1.6  
     1.7 -lemmas bool_simps = simp_thms(1-34)
     1.8 +lemmas bool_simps = simp_thms(1-34) -- {* FIXME move to @{theory HOL} *}
     1.9 +
    1.10 +lemma nnf_simps: -- {* FIXME shadows fact binding in @{theory HOL} *}
    1.11 +  "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
    1.12 +  "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
    1.13 +  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
    1.14 +  by blast+
    1.15  
    1.16  lemma dnf:
    1.17 -    "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
    1.18 -    "(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"
    1.19 +  "(P & (Q | R)) = ((P&Q) | (P&R))"
    1.20 +  "((Q | R) & P) = ((Q&P) | (R&P))"
    1.21 +  "(P \<and> Q) = (Q \<and> P)"
    1.22 +  "(P \<or> Q) = (Q \<or> P)"
    1.23    by blast+
    1.24  
    1.25  lemmas weak_dnf_simps = dnf bool_simps
    1.26  
    1.27 -lemma nnf_simps:
    1.28 -    "(\<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)"
    1.29 -    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
    1.30 -  by blast+
    1.31 -
    1.32  lemma PFalse:
    1.33      "P \<equiv> False \<Longrightarrow> \<not> P"
    1.34      "\<not> P \<Longrightarrow> (P \<equiv> False)"