--- a/src/HOL/SMT/Z3.thy Tue Oct 20 14:44:19 2009 +0200
+++ b/src/HOL/SMT/Z3.thy Tue Oct 20 15:03:17 2009 +0200
@@ -19,6 +19,30 @@
lemmas [z3_rewrite] =
refl eq_commute conj_commute disj_commute simp_thms nnf_simps
- ring_distribs field_eq_simps
+ ring_distribs field_eq_simps if_True if_False
+
+lemma [z3_rewrite]: "(\<not>False \<longrightarrow> P) = P" by fast
+lemma [z3_rewrite]: "(P \<longrightarrow> Q) = (Q \<or> \<not>P)" by fast
+lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (P \<or> Q)" by fast
+lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (Q \<or> P)" by fast
+
+lemma [z3_rewrite]: "(if P then True else False) = P" by simp
+lemma [z3_rewrite]: "(if P then False else True) = (\<not>P)" by simp
+
+lemma [z3_rewrite]:
+ "0 + (x::int) = x"
+ "x + 0 = x"
+ "0 * x = 0"
+ "1 * x = x"
+ "x + y = y + x"
+ by auto
+
+lemma [z3_rewrite]:
+ "0 + (x::real) = x"
+ "x + 0 = x"
+ "0 * x = 0"
+ "1 * x = x"
+ "x + y = y + x"
+ by auto
end