author  boehmes 
Wed, 12 May 2010 23:53:48 +0200  
changeset 36884  88cf4896b980 
parent 36350  bc7982c54e37 
child 36895  a96f9793d9c5 
permissions  rwrr 
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 

36884
88cf4896b980
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
boehmes
parents:
36350
diff
changeset

8 
imports SMT_Base "~~/src/HOL/Decision_Procs/Dense_Linear_Order" 
33010  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 

36884
88cf4896b980
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
boehmes
parents:
36350
diff
changeset

18 
setup {* 
88cf4896b980
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
boehmes
parents:
36350
diff
changeset

19 
Z3_Proof_Rules.setup #> 
88cf4896b980
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
boehmes
parents:
36350
diff
changeset

20 
Z3_Solver.setup #> 
88cf4896b980
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
boehmes
parents:
36350
diff
changeset

21 
Arith_Data.add_tactic "FerranteRackoff" (K FerranteRackoff.dlo_tac) 
88cf4896b980
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
boehmes
parents:
36350
diff
changeset

22 
*} 
33010  23 

24 
lemmas [z3_rewrite] = 

25 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps 

36350  26 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left if_True if_False 
33021  27 

33610  28 
lemma [z3_rewrite]: "(P \<noteq> Q) = (Q = (\<not>P))" by fast 
29 

33021  30 
lemma [z3_rewrite]: "(\<not>False \<longrightarrow> P) = P" by fast 
31 
lemma [z3_rewrite]: "(P \<longrightarrow> Q) = (Q \<or> \<not>P)" by fast 

32 
lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (P \<or> Q)" by fast 

33 
lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (Q \<or> P)" by fast 

34 

35 
lemma [z3_rewrite]: "(if P then True else False) = P" by simp 

36 
lemma [z3_rewrite]: "(if P then False else True) = (\<not>P)" by simp 

37 

38 
lemma [z3_rewrite]: 

39 
"0 + (x::int) = x" 

40 
"x + 0 = x" 

41 
"0 * x = 0" 

42 
"1 * x = x" 

43 
"x + y = y + x" 

44 
by auto 

45 

46 
lemma [z3_rewrite]: 

47 
"0 + (x::real) = x" 

48 
"x + 0 = x" 

49 
"0 * x = 0" 

50 
"1 * x = x" 

51 
"x + y = y + x" 

52 
by auto 

33010  53 

54 
end 