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 "~~/src/HOL/Decision_Procs/Dense_Linear_Order" |
|
9 uses |
|
10 "Tools/z3_proof_parser.ML" |
|
11 "Tools/z3_proof_tools.ML" |
|
12 "Tools/z3_proof_literals.ML" |
|
13 "Tools/z3_proof_reconstruction.ML" |
|
14 "Tools/z3_model.ML" |
|
15 "Tools/z3_interface.ML" |
|
16 "Tools/z3_solver.ML" |
|
17 begin |
|
18 |
|
19 setup {* |
|
20 Z3_Proof_Reconstruction.setup #> |
|
21 Z3_Solver.setup #> |
|
22 Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) |
|
23 *} |
|
24 |
|
25 lemmas [z3_rule] = |
|
26 refl eq_commute conj_commute disj_commute simp_thms nnf_simps |
|
27 ring_distribs field_simps times_divide_eq_right times_divide_eq_left |
|
28 if_True if_False not_not |
|
29 |
|
30 lemma [z3_rule]: |
|
31 "(P \<longrightarrow> Q) = (Q \<or> \<not>P)" |
|
32 "(\<not>P \<longrightarrow> Q) = (P \<or> Q)" |
|
33 "(\<not>P \<longrightarrow> Q) = (Q \<or> P)" |
|
34 by auto |
|
35 |
|
36 lemma [z3_rule]: |
|
37 "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not>P)))" |
|
38 by auto |
|
39 |
|
40 lemma [z3_rule]: |
|
41 "((\<not>P) = P) = False" |
|
42 "(P = (\<not>P)) = False" |
|
43 "(P \<noteq> Q) = (Q = (\<not>P))" |
|
44 "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))" |
|
45 "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))" |
|
46 by auto |
|
47 |
|
48 lemma [z3_rule]: |
|
49 "(if P then P else \<not>P) = True" |
|
50 "(if \<not>P then \<not>P else P) = True" |
|
51 "(if P then True else False) = P" |
|
52 "(if P then False else True) = (\<not>P)" |
|
53 "(if \<not>P then x else y) = (if P then y else x)" |
|
54 by auto |
|
55 |
|
56 lemma [z3_rule]: |
|
57 "P = Q \<or> P \<or> Q" |
|
58 "P = Q \<or> \<not>P \<or> \<not>Q" |
|
59 "(\<not>P) = Q \<or> \<not>P \<or> Q" |
|
60 "(\<not>P) = Q \<or> P \<or> \<not>Q" |
|
61 "P = (\<not>Q) \<or> \<not>P \<or> Q" |
|
62 "P = (\<not>Q) \<or> P \<or> \<not>Q" |
|
63 "P \<noteq> Q \<or> P \<or> \<not>Q" |
|
64 "P \<noteq> Q \<or> \<not>P \<or> Q" |
|
65 "P \<noteq> (\<not>Q) \<or> P \<or> Q" |
|
66 "(\<not>P) \<noteq> Q \<or> P \<or> Q" |
|
67 "P \<or> Q \<or> P \<noteq> (\<not>Q)" |
|
68 "P \<or> Q \<or> (\<not>P) \<noteq> Q" |
|
69 "P \<or> \<not>Q \<or> P \<noteq> Q" |
|
70 "\<not>P \<or> Q \<or> P \<noteq> Q" |
|
71 by auto |
|
72 |
|
73 lemma [z3_rule]: |
|
74 "0 + (x::int) = x" |
|
75 "x + 0 = x" |
|
76 "0 * x = 0" |
|
77 "1 * x = x" |
|
78 "x + y = y + x" |
|
79 by auto |
|
80 |
|
81 lemma [z3_rule]: |
|
82 "0 + (x::real) = x" |
|
83 "x + 0 = x" |
|
84 "0 * x = 0" |
|
85 "1 * x = x" |
|
86 "x + y = y + x" |
|
87 by auto |
|
88 |
|
89 end |
|