|
1 (* Title: HOL/Library/SMT/z3_proof_methods.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Proof methods for Z3 proof reconstruction. |
|
5 *) |
|
6 |
|
7 signature Z3_PROOF_METHODS = |
|
8 sig |
|
9 val prove_injectivity: Proof.context -> cterm -> thm |
|
10 val prove_ite: Proof.context -> cterm -> thm |
|
11 end |
|
12 |
|
13 structure Z3_Proof_Methods: Z3_PROOF_METHODS = |
|
14 struct |
|
15 |
|
16 |
|
17 fun apply tac st = |
|
18 (case Seq.pull (tac 1 st) of |
|
19 NONE => raise THM ("tactic failed", 1, [st]) |
|
20 | SOME (st', _) => st') |
|
21 |
|
22 |
|
23 |
|
24 (* if-then-else *) |
|
25 |
|
26 val pull_ite = mk_meta_eq |
|
27 @{lemma "f (if P then x else y) = (if P then f x else f y)" by simp} |
|
28 |
|
29 fun pull_ites_conv ct = |
|
30 (Conv.rewr_conv pull_ite then_conv |
|
31 Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct |
|
32 |
|
33 fun prove_ite ctxt = |
|
34 Z3_Proof_Tools.by_tac ctxt ( |
|
35 CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv)) |
|
36 THEN' rtac @{thm refl}) |
|
37 |
|
38 |
|
39 |
|
40 (* injectivity *) |
|
41 |
|
42 local |
|
43 |
|
44 val B = @{typ bool} |
|
45 fun mk_univ T = Const (@{const_name top}, HOLogic.mk_setT T) |
|
46 fun mk_inj_on T U = |
|
47 Const (@{const_name inj_on}, (T --> U) --> HOLogic.mk_setT T --> B) |
|
48 fun mk_inv_into T U = |
|
49 Const (@{const_name inv_into}, [HOLogic.mk_setT T, T --> U, U] ---> T) |
|
50 |
|
51 fun mk_inv_of ctxt ct = |
|
52 let |
|
53 val (dT, rT) = Term.dest_funT (SMT_Utils.typ_of ct) |
|
54 val inv = SMT_Utils.certify ctxt (mk_inv_into dT rT) |
|
55 val univ = SMT_Utils.certify ctxt (mk_univ dT) |
|
56 in Thm.mk_binop inv univ ct end |
|
57 |
|
58 fun mk_inj_prop ctxt ct = |
|
59 let |
|
60 val (dT, rT) = Term.dest_funT (SMT_Utils.typ_of ct) |
|
61 val inj = SMT_Utils.certify ctxt (mk_inj_on dT rT) |
|
62 val univ = SMT_Utils.certify ctxt (mk_univ dT) |
|
63 in SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end |
|
64 |
|
65 |
|
66 val disjE = @{lemma "~P | Q ==> P ==> Q" by fast} |
|
67 |
|
68 fun prove_inj_prop ctxt def lhs = |
|
69 let |
|
70 val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt |
|
71 val rule = disjE OF [Object_Logic.rulify ctxt' (Thm.assume lhs)] |
|
72 in |
|
73 Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct)) |
|
74 |> apply (rtac @{thm injI}) |
|
75 |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}]) |
|
76 |> Goal.norm_result ctxt' o Goal.finish ctxt' |
|
77 |> singleton (Variable.export ctxt' ctxt) |
|
78 end |
|
79 |
|
80 fun prove_rhs ctxt def lhs = |
|
81 Z3_Proof_Tools.by_tac ctxt ( |
|
82 CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt) |
|
83 THEN' REPEAT_ALL_NEW (match_tac @{thms allI}) |
|
84 THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) |
|
85 |
|
86 |
|
87 fun expand thm ct = |
|
88 let |
|
89 val cpat = Thm.dest_arg (Thm.rhs_of thm) |
|
90 val (cl, cr) = Thm.dest_binop (Thm.dest_arg (Thm.dest_arg1 ct)) |
|
91 val thm1 = Thm.instantiate (Thm.match (cpat, cl)) thm |
|
92 val thm2 = Thm.instantiate (Thm.match (cpat, cr)) thm |
|
93 in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end |
|
94 |
|
95 fun prove_lhs ctxt rhs = |
|
96 let |
|
97 val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify ctxt (Thm.assume rhs))) |
|
98 val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt |
|
99 in |
|
100 Z3_Proof_Tools.by_tac ctxt ( |
|
101 CONVERSION (SMT_Utils.prop_conv conv) |
|
102 THEN' Simplifier.simp_tac (put_simpset HOL_ss ctxt)) |
|
103 end |
|
104 |
|
105 |
|
106 fun mk_inv_def ctxt rhs = |
|
107 let |
|
108 val (ct, ctxt') = |
|
109 SMT_Utils.dest_all_cbinders (SMT_Utils.dest_cprop rhs) ctxt |
|
110 val (cl, cv) = Thm.dest_binop ct |
|
111 val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last |
|
112 val cu = fold_rev Thm.lambda cargs (mk_inv_of ctxt' (Thm.lambda cv cf)) |
|
113 in Thm.assume (SMT_Utils.mk_cequals cg cu) end |
|
114 |
|
115 fun prove_inj_eq ctxt ct = |
|
116 let |
|
117 val (lhs, rhs) = |
|
118 pairself SMT_Utils.mk_cprop (Thm.dest_binop (SMT_Utils.dest_cprop ct)) |
|
119 val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs) |
|
120 val rhs_thm = |
|
121 Thm.implies_intr lhs (prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs) |
|
122 in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end |
|
123 |
|
124 |
|
125 val swap_eq_thm = mk_meta_eq @{thm eq_commute} |
|
126 val swap_disj_thm = mk_meta_eq @{thm disj_commute} |
|
127 |
|
128 fun swap_conv dest eq = |
|
129 SMT_Utils.if_true_conv ((op <) o pairself Term.size_of_term o dest) |
|
130 (Conv.rewr_conv eq) |
|
131 |
|
132 val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm |
|
133 val swap_disj_conv = swap_conv SMT_Utils.dest_disj swap_disj_thm |
|
134 |
|
135 fun norm_conv ctxt = |
|
136 swap_eq_conv then_conv |
|
137 Conv.arg1_conv (SMT_Utils.binders_conv (K swap_disj_conv) ctxt) then_conv |
|
138 Conv.arg_conv (SMT_Utils.binders_conv (K swap_eq_conv) ctxt) |
|
139 |
|
140 in |
|
141 |
|
142 fun prove_injectivity ctxt = |
|
143 Z3_Proof_Tools.by_tac ctxt ( |
|
144 CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt)) |
|
145 THEN' CSUBGOAL (uncurry (rtac o prove_inj_eq ctxt))) |
|
146 |
|
147 end |
|
148 |
|
149 end |