|
1 (* Title: HOL/Tools/SMT2/z3_new_proof_replay.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 |
|
5 Z3 proof replay. |
|
6 *) |
|
7 |
|
8 signature Z3_NEW_PROOF_REPLAY = |
|
9 sig |
|
10 val replay: Proof.context -> SMT2_Translate.replay_data -> string list -> int list * thm |
|
11 end |
|
12 |
|
13 structure Z3_New_Proof_Replay: Z3_NEW_PROOF_REPLAY = |
|
14 struct |
|
15 |
|
16 fun params_of t = Term.strip_qnt_vars @{const_name all} t |
|
17 |
|
18 fun varify ctxt thm = |
|
19 let |
|
20 val maxidx = Thm.maxidx_of thm + 1 |
|
21 val vs = params_of (Thm.prop_of thm) |
|
22 val vars = map_index (fn (i, (n, T)) => Var ((n, i + maxidx), T)) vs |
|
23 in Drule.forall_elim_list (map (SMT2_Utils.certify ctxt) vars) thm end |
|
24 |
|
25 fun add_paramTs names t = |
|
26 fold2 (fn n => fn (_, T) => AList.update (op =) (n, T)) names (params_of t) |
|
27 |
|
28 fun new_fixes ctxt nTs = |
|
29 let |
|
30 val (ns, ctxt') = Variable.variant_fixes (replicate (length nTs) "") ctxt |
|
31 fun mk (n, T) n' = (n, SMT2_Utils.certify ctxt' (Free (n', T))) |
|
32 in (ctxt', Symtab.make (map2 mk nTs ns)) end |
|
33 |
|
34 fun forall_elim_term ct (Const (@{const_name all}, _) $ (a as Abs _)) = |
|
35 Term.betapply (a, Thm.term_of ct) |
|
36 | forall_elim_term _ qt = raise TERM ("forall_elim'", [qt]) |
|
37 |
|
38 fun apply_fixes elim env = fold (elim o the o Symtab.lookup env) |
|
39 |
|
40 val apply_fixes_prem = uncurry o apply_fixes Thm.forall_elim |
|
41 val apply_fixes_concl = apply_fixes forall_elim_term |
|
42 |
|
43 fun export_fixes env names = Drule.forall_intr_list (map (the o Symtab.lookup env) names) |
|
44 |
|
45 fun under_fixes f ctxt (prems, nthms) names concl = |
|
46 let |
|
47 val thms1 = map (varify ctxt) prems |
|
48 val (ctxt', env) = |
|
49 add_paramTs names concl [] |
|
50 |> fold (uncurry add_paramTs o apsnd Thm.prop_of) nthms |
|
51 |> new_fixes ctxt |
|
52 val thms2 = map (apply_fixes_prem env) nthms |
|
53 val t = apply_fixes_concl env names concl |
|
54 in export_fixes env names (f ctxt' (thms1 @ thms2) t) end |
|
55 |
|
56 fun replay_thm ctxt assumed nthms |
|
57 (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) = |
|
58 (tracing ("replay_thm: " ^ @{make_string} (id, rule) ^ " " ^ Syntax.string_of_term ctxt concl); |
|
59 if Z3_New_Proof_Methods.is_assumption rule then |
|
60 (case Inttab.lookup assumed id of |
|
61 SOME (_, thm) => thm |
|
62 | NONE => Thm.assume (SMT2_Utils.certify ctxt concl)) |
|
63 else |
|
64 under_fixes (Z3_New_Proof_Methods.method_for rule) ctxt |
|
65 (if is_fix_step then (map snd nthms, []) else ([], nthms)) fixes concl |
|
66 ) (*###*) |
|
67 |
|
68 fun replay_step ctxt assumed (step as Z3_New_Proof.Z3_Step {id, prems, fixes, ...}) proofs = |
|
69 let val nthms = map (the o Inttab.lookup proofs) prems |
|
70 in Inttab.update (id, (fixes, replay_thm ctxt assumed nthms step)) proofs end |
|
71 |
|
72 local |
|
73 val remove_trigger = mk_meta_eq @{thm SMT2.trigger_def} |
|
74 val remove_weight = mk_meta_eq @{thm SMT2.weight_def} |
|
75 val remove_fun_app = mk_meta_eq @{thm SMT2.fun_app_def} |
|
76 |
|
77 fun rewrite_conv _ [] = Conv.all_conv |
|
78 | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs) |
|
79 |
|
80 val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight, |
|
81 remove_fun_app, Z3_New_Proof_Literals.rewrite_true] |
|
82 |
|
83 fun rewrite _ [] = I |
|
84 | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs) |
|
85 |
|
86 fun lookup_assm assms_net ct = |
|
87 Z3_New_Proof_Tools.net_instances assms_net ct |
|
88 |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct)) |
|
89 in |
|
90 |
|
91 fun add_asserted outer_ctxt rewrite_rules assms steps ctxt = |
|
92 let |
|
93 val eqs = map (rewrite ctxt [Z3_New_Proof_Literals.rewrite_true]) rewrite_rules |
|
94 val eqs' = union Thm.eq_thm eqs prep_rules |
|
95 |
|
96 val assms_net = |
|
97 assms |
|
98 |> map (apsnd (rewrite ctxt eqs')) |
|
99 |> map (apsnd (Conv.fconv_rule Thm.eta_conversion)) |
|
100 |> Z3_New_Proof_Tools.thm_net_of snd |
|
101 |
|
102 fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion |
|
103 |
|
104 fun assume thm ctxt = |
|
105 let |
|
106 val ct = Thm.cprem_of thm 1 |
|
107 val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt |
|
108 in (thm' RS thm, ctxt') end |
|
109 |
|
110 fun add1 id fixes thm1 ((i, th), exact) ((is, thms), (ctxt, ptab)) = |
|
111 let |
|
112 val (thm, ctxt') = if exact then (Thm.implies_elim thm1 th, ctxt) else assume thm1 ctxt |
|
113 val thms' = if exact then thms else th :: thms |
|
114 in |
|
115 ((insert (op =) i is, thms'), |
|
116 (ctxt', Inttab.update (id, (fixes, thm)) ptab)) |
|
117 end |
|
118 |
|
119 fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...}) |
|
120 (cx as ((is, thms), (ctxt, ptab))) = |
|
121 if Z3_New_Proof_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then |
|
122 let |
|
123 val ct = SMT2_Utils.certify ctxt concl |
|
124 val thm1 = |
|
125 Thm.trivial ct |
|
126 |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt)) |
|
127 val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1 |
|
128 in |
|
129 (case lookup_assm assms_net (Thm.cprem_of thm2 1) of |
|
130 [] => |
|
131 let val (thm, ctxt') = assume thm1 ctxt |
|
132 in ((is, thms), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end |
|
133 | ithms => fold (add1 id fixes thm1) ithms cx) |
|
134 end |
|
135 else |
|
136 cx |
|
137 in fold add steps (([], []), (ctxt, Inttab.empty)) end |
|
138 |
|
139 end |
|
140 |
|
141 (* |- (EX x. P x) = P c |- ~ (ALL x. P x) = ~ P c *) |
|
142 local |
|
143 val sk_rules = @{lemma |
|
144 "c = (SOME x. P x) ==> (EX x. P x) = P c" |
|
145 "c = (SOME x. ~ P x) ==> (~ (ALL x. P x)) = (~ P c)" |
|
146 by (metis someI_ex)+} |
|
147 in |
|
148 |
|
149 fun discharge_sk_tac i st = |
|
150 (rtac @{thm trans} i |
|
151 THEN resolve_tac sk_rules i |
|
152 THEN (rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1) |
|
153 THEN rtac @{thm refl} i) st |
|
154 |
|
155 end |
|
156 |
|
157 fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl}, |
|
158 @{thm reflexive}, Z3_New_Proof_Literals.true_thm] |
|
159 |
|
160 val intro_def_rules = @{lemma |
|
161 "(~ P | P) & (P | ~ P)" |
|
162 "(P | ~ P) & (~ P | P)" |
|
163 by fast+} |
|
164 |
|
165 fun discharge_assms_tac rules = |
|
166 REPEAT (HEADGOAL (resolve_tac (intro_def_rules @ rules) ORELSE' SOLVED' discharge_sk_tac)) |
|
167 |
|
168 fun discharge_assms ctxt rules thm = |
|
169 (if Thm.nprems_of thm = 0 then |
|
170 thm |
|
171 else |
|
172 (case Seq.pull (discharge_assms_tac rules thm) of |
|
173 SOME (thm', _) => thm' |
|
174 | NONE => raise THM ("failed to discharge premise", 1, [thm]))) |
|
175 |> Goal.norm_result ctxt |
|
176 |
|
177 fun discharge rules outer_ctxt inner_ctxt = |
|
178 singleton (Proof_Context.export inner_ctxt outer_ctxt) |
|
179 #> discharge_assms outer_ctxt (make_discharge_rules rules) |
|
180 |
|
181 fun replay outer_ctxt |
|
182 ({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output = |
|
183 let |
|
184 val (steps, ctxt1) = Z3_New_Proof.parse typs terms output ctxt |
|
185 val ctxt2 = put_simpset (Z3_New_Proof_Tools.make_simpset ctxt1 []) ctxt1 |
|
186 val ((is, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2 |
|
187 val proofs = fold (replay_step ctxt3 assumed) steps assumed |
|
188 val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps |
|
189 in |
|
190 if Config.get ctxt3 SMT2_Config.filter_only_facts then (is, TrueI) |
|
191 else ([], Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt3) |
|
192 end |
|
193 |
|
194 end |