# HG changeset patch
# User boehmes
# Date 1256043797 -7200
# Node ID c065b9300d441f5795948d5ee01884fabdaa2383
# Parent  0908ed080ccfb9dae87028f1d99150694c79b50e
additional schematic rules for Z3's rewrite rule

diff -r 0908ed080ccf -r c065b9300d44 src/HOL/SMT/Z3.thy
--- 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