equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Binding to the SMT solver Z3, with proof reconstruction *} |
5 header {* Binding to the SMT solver Z3, with proof reconstruction *} |
6 |
6 |
7 theory Z3 |
7 theory Z3 |
8 imports SMT_Base |
8 imports SMT_Base "~~/src/HOL/Decision_Procs/Dense_Linear_Order" |
9 uses |
9 uses |
10 "Tools/z3_proof_terms.ML" |
10 "Tools/z3_proof_terms.ML" |
11 "Tools/z3_proof_rules.ML" |
11 "Tools/z3_proof_rules.ML" |
12 "Tools/z3_proof.ML" |
12 "Tools/z3_proof.ML" |
13 "Tools/z3_model.ML" |
13 "Tools/z3_model.ML" |
14 "Tools/z3_interface.ML" |
14 "Tools/z3_interface.ML" |
15 "Tools/z3_solver.ML" |
15 "Tools/z3_solver.ML" |
16 begin |
16 begin |
17 |
17 |
18 setup {* Z3_Proof_Rules.setup #> Z3_Solver.setup *} |
18 setup {* |
|
19 Z3_Proof_Rules.setup #> |
|
20 Z3_Solver.setup #> |
|
21 Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) |
|
22 *} |
19 |
23 |
20 lemmas [z3_rewrite] = |
24 lemmas [z3_rewrite] = |
21 refl eq_commute conj_commute disj_commute simp_thms nnf_simps |
25 refl eq_commute conj_commute disj_commute simp_thms nnf_simps |
22 ring_distribs field_simps times_divide_eq_right times_divide_eq_left if_True if_False |
26 ring_distribs field_simps times_divide_eq_right times_divide_eq_left if_True if_False |
23 |
27 |