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