equal
deleted
inserted
replaced
18 setup {* Z3_Proof_Rules.setup #> Z3_Solver.setup *} |
18 setup {* Z3_Proof_Rules.setup #> Z3_Solver.setup *} |
19 |
19 |
20 lemmas [z3_rewrite] = |
20 lemmas [z3_rewrite] = |
21 refl eq_commute conj_commute disj_commute simp_thms nnf_simps |
21 refl eq_commute conj_commute disj_commute simp_thms nnf_simps |
22 ring_distribs field_eq_simps if_True if_False |
22 ring_distribs field_eq_simps if_True if_False |
|
23 |
|
24 lemma [z3_rewrite]: "(P \<noteq> Q) = (Q = (\<not>P))" by fast |
23 |
25 |
24 lemma [z3_rewrite]: "(\<not>False \<longrightarrow> P) = P" by fast |
26 lemma [z3_rewrite]: "(\<not>False \<longrightarrow> P) = P" by fast |
25 lemma [z3_rewrite]: "(P \<longrightarrow> Q) = (Q \<or> \<not>P)" by fast |
27 lemma [z3_rewrite]: "(P \<longrightarrow> Q) = (Q \<or> \<not>P)" by fast |
26 lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (P \<or> Q)" by fast |
28 lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (P \<or> Q)" by fast |
27 lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (Q \<or> P)" by fast |
29 lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (Q \<or> P)" by fast |