|
33010
|
1 |
(* Title: HOL/SMT/Z3.thy
|
|
|
2 |
Author: Sascha Boehme, TU Muenchen
|
|
|
3 |
*)
|
|
|
4 |
|
|
|
5 |
header {* Binding to the SMT solver Z3, with proof reconstruction *}
|
|
|
6 |
|
|
|
7 |
theory Z3
|
|
|
8 |
imports SMT_Base
|
|
|
9 |
uses
|
|
|
10 |
"Tools/z3_proof_terms.ML"
|
|
|
11 |
"Tools/z3_proof_rules.ML"
|
|
|
12 |
"Tools/z3_proof.ML"
|
|
|
13 |
"Tools/z3_model.ML"
|
|
|
14 |
"Tools/z3_interface.ML"
|
|
|
15 |
"Tools/z3_solver.ML"
|
|
|
16 |
begin
|
|
|
17 |
|
|
|
18 |
setup {* Z3_Proof_Rules.setup #> Z3_Solver.setup *}
|
|
|
19 |
|
|
|
20 |
lemmas [z3_rewrite] =
|
|
|
21 |
refl eq_commute conj_commute disj_commute simp_thms nnf_simps
|
|
33021
|
22 |
ring_distribs field_eq_simps if_True if_False
|
|
|
23 |
|
|
|
24 |
lemma [z3_rewrite]: "(\<not>False \<longrightarrow> P) = P" by fast
|
|
|
25 |
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
|
|
|
27 |
lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (Q \<or> P)" by fast
|
|
|
28 |
|
|
|
29 |
lemma [z3_rewrite]: "(if P then True else False) = P" by simp
|
|
|
30 |
lemma [z3_rewrite]: "(if P then False else True) = (\<not>P)" by simp
|
|
|
31 |
|
|
|
32 |
lemma [z3_rewrite]:
|
|
|
33 |
"0 + (x::int) = x"
|
|
|
34 |
"x + 0 = x"
|
|
|
35 |
"0 * x = 0"
|
|
|
36 |
"1 * x = x"
|
|
|
37 |
"x + y = y + x"
|
|
|
38 |
by auto
|
|
|
39 |
|
|
|
40 |
lemma [z3_rewrite]:
|
|
|
41 |
"0 + (x::real) = x"
|
|
|
42 |
"x + 0 = x"
|
|
|
43 |
"0 * x = 0"
|
|
|
44 |
"1 * x = x"
|
|
|
45 |
"x + y = y + x"
|
|
|
46 |
by auto
|
|
33010
|
47 |
|
|
|
48 |
end
|