author | boehmes |
Mon, 22 Nov 2010 15:45:43 +0100 | |
changeset 40663 | e080c9e68752 |
parent 40662 | 798aad2229c0 |
child 40664 | e023788a91a1 |
permissions | -rw-r--r-- |
36898 | 1 |
(* Title: HOL/Tools/SMT/z3_proof_reconstruction.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
Proof reconstruction for proofs found by Z3. |
|
5 |
*) |
|
6 |
||
7 |
signature Z3_PROOF_RECONSTRUCTION = |
|
8 |
sig |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
9 |
val add_z3_rule: thm -> Context.generic -> Context.generic |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
10 |
val reconstruct: Proof.context -> SMT_Translate.recon -> string list -> |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39557
diff
changeset
|
11 |
(int list * thm) * Proof.context |
36898 | 12 |
val setup: theory -> theory |
13 |
end |
|
14 |
||
15 |
structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION = |
|
16 |
struct |
|
17 |
||
18 |
structure P = Z3_Proof_Parser |
|
19 |
structure T = Z3_Proof_Tools |
|
20 |
structure L = Z3_Proof_Literals |
|
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
21 |
structure M = Z3_Proof_Methods |
36898 | 22 |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40274
diff
changeset
|
23 |
fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
24 |
("Z3 proof reconstruction: " ^ msg)) |
36898 | 25 |
|
26 |
||
27 |
||
28 |
(** net of schematic rules **) |
|
29 |
||
30 |
val z3_ruleN = "z3_rule" |
|
31 |
||
32 |
local |
|
33 |
val description = "declaration of Z3 proof rules" |
|
34 |
||
35 |
val eq = Thm.eq_thm |
|
36 |
||
37 |
structure Z3_Rules = Generic_Data |
|
38 |
( |
|
39 |
type T = thm Net.net |
|
40 |
val empty = Net.empty |
|
41 |
val extend = I |
|
42 |
val merge = Net.merge eq |
|
43 |
) |
|
44 |
||
45 |
val prep = `Thm.prop_of o Simplifier.rewrite_rule [L.rewrite_true] |
|
46 |
||
47 |
fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net |
|
48 |
fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net |
|
49 |
||
50 |
val add = Thm.declaration_attribute (Z3_Rules.map o ins) |
|
51 |
val del = Thm.declaration_attribute (Z3_Rules.map o del) |
|
52 |
in |
|
53 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
54 |
val add_z3_rule = Z3_Rules.map o ins |
36898 | 55 |
|
56 |
fun by_schematic_rule ctxt ct = |
|
57 |
the (T.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct) |
|
58 |
||
59 |
val z3_rules_setup = |
|
60 |
Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #> |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39020
diff
changeset
|
61 |
Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get) |
36898 | 62 |
|
63 |
end |
|
64 |
||
65 |
||
66 |
||
67 |
(** proof tools **) |
|
68 |
||
69 |
fun named ctxt name prover ct = |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40274
diff
changeset
|
70 |
let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") |
36898 | 71 |
in prover ct end |
72 |
||
73 |
fun NAMED ctxt name tac i st = |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40274
diff
changeset
|
74 |
let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") |
36898 | 75 |
in tac i st end |
76 |
||
77 |
fun pretty_goal ctxt thms t = |
|
78 |
[Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]] |
|
79 |
|> not (null thms) ? cons (Pretty.big_list "assumptions:" |
|
80 |
(map (Display.pretty_thm ctxt) thms)) |
|
81 |
||
82 |
fun try_apply ctxt thms = |
|
83 |
let |
|
84 |
fun try_apply_err ct = Pretty.string_of (Pretty.chunks [ |
|
85 |
Pretty.big_list ("Z3 found a proof," ^ |
|
86 |
" but proof reconstruction failed at the following subgoal:") |
|
87 |
(pretty_goal ctxt thms (Thm.term_of ct)), |
|
88 |
Pretty.str ("Adding a rule to the lemma group " ^ quote z3_ruleN ^ |
|
89 |
" might solve this problem.")]) |
|
90 |
||
91 |
fun apply [] ct = error (try_apply_err ct) |
|
92 |
| apply (prover :: provers) ct = |
|
93 |
(case try prover ct of |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40274
diff
changeset
|
94 |
SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm) |
36898 | 95 |
| NONE => apply provers ct) |
96 |
||
97 |
in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end |
|
98 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
99 |
local |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
100 |
val rewr_if = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
101 |
@{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
102 |
in |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
103 |
val simp_fast_tac = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
104 |
Simplifier.simp_tac (HOL_ss addsimps [rewr_if]) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
105 |
THEN_ALL_NEW Classical.fast_tac HOL_cs |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
106 |
end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
107 |
|
36898 | 108 |
|
109 |
||
110 |
(** theorems and proofs **) |
|
111 |
||
112 |
(* theorem incarnations *) |
|
113 |
||
114 |
datatype theorem = |
|
115 |
Thm of thm | (* theorem without special features *) |
|
116 |
MetaEq of thm | (* meta equality "t == s" *) |
|
117 |
Literals of thm * L.littab |
|
118 |
(* "P1 & ... & Pn" and table of all literals P1, ..., Pn *) |
|
119 |
||
120 |
fun thm_of (Thm thm) = thm |
|
121 |
| thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq} |
|
122 |
| thm_of (Literals (thm, _)) = thm |
|
123 |
||
124 |
fun meta_eq_of (MetaEq thm) = thm |
|
125 |
| meta_eq_of p = mk_meta_eq (thm_of p) |
|
126 |
||
127 |
fun literals_of (Literals (_, lits)) = lits |
|
128 |
| literals_of p = L.make_littab [thm_of p] |
|
129 |
||
130 |
||
131 |
(* proof representation *) |
|
132 |
||
133 |
datatype proof = Unproved of P.proof_step | Proved of theorem |
|
134 |
||
135 |
||
136 |
||
137 |
(** core proof rules **) |
|
138 |
||
139 |
(* assumption *) |
|
140 |
||
141 |
local |
|
142 |
val remove_trigger = @{lemma "trigger t p == p" |
|
143 |
by (rule eq_reflection, rule trigger_def)} |
|
144 |
||
145 |
val prep_rules = [@{thm Let_def}, remove_trigger, L.rewrite_true] |
|
146 |
||
147 |
fun rewrite_conv ctxt eqs = Simplifier.full_rewrite |
|
148 |
(Simplifier.context ctxt Simplifier.empty_ss addsimps eqs) |
|
149 |
||
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
150 |
fun rewrites f ctxt eqs = map (f (Conv.fconv_rule (rewrite_conv ctxt eqs))) |
36898 | 151 |
|
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
152 |
fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm) |
36898 | 153 |
fun lookup_assm ctxt assms ct = |
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
154 |
(case T.net_instance' burrow_snd_option assms ct of |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
155 |
SOME ithm => ithm |
36898 | 156 |
| _ => z3_exn ("not asserted: " ^ |
157 |
quote (Syntax.string_of_term ctxt (Thm.term_of ct)))) |
|
158 |
in |
|
159 |
fun prepare_assms ctxt unfolds assms = |
|
160 |
let |
|
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
161 |
val unfolds' = rewrites I ctxt [L.rewrite_true] unfolds |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
162 |
val assms' = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
163 |
rewrites apsnd ctxt (union Thm.eq_thm unfolds' prep_rules) assms |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
164 |
in (unfolds', T.thm_net_of snd assms') end |
36898 | 165 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
166 |
fun asserted ctxt (unfolds, assms) ct = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
167 |
let val revert_conv = rewrite_conv ctxt unfolds |
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
168 |
in Thm (T.with_conv revert_conv (snd o lookup_assm ctxt assms) ct) end |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
169 |
|
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
170 |
fun find_assm ctxt (unfolds, assms) ct = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
171 |
fst (lookup_assm ctxt assms (Thm.rhs_of (rewrite_conv ctxt unfolds ct))) |
36898 | 172 |
end |
173 |
||
174 |
||
175 |
||
176 |
(* P = Q ==> P ==> Q or P --> Q ==> P ==> Q *) |
|
177 |
local |
|
178 |
val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp} |
|
179 |
val meta_iffD1_c = T.precompose2 Thm.dest_binop meta_iffD1 |
|
180 |
||
181 |
val iffD1_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm iffD1} |
|
182 |
val mp_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm mp} |
|
183 |
in |
|
184 |
fun mp (MetaEq thm) p = Thm (Thm.implies_elim (T.compose meta_iffD1_c thm) p) |
|
185 |
| mp p_q p = |
|
186 |
let |
|
187 |
val pq = thm_of p_q |
|
188 |
val thm = T.compose iffD1_c pq handle THM _ => T.compose mp_c pq |
|
189 |
in Thm (Thm.implies_elim thm p) end |
|
190 |
end |
|
191 |
||
192 |
||
193 |
||
194 |
(* and_elim: P1 & ... & Pn ==> Pi *) |
|
195 |
(* not_or_elim: ~(P1 | ... | Pn) ==> ~Pi *) |
|
196 |
local |
|
197 |
fun is_sublit conj t = L.exists_lit conj (fn u => u aconv t) |
|
198 |
||
199 |
fun derive conj t lits idx ptab = |
|
200 |
let |
|
201 |
val lit = the (L.get_first_lit (is_sublit conj t) lits) |
|
202 |
val ls = L.explode conj false false [t] lit |
|
203 |
val lits' = fold L.insert_lit ls (L.delete_lit lit lits) |
|
204 |
||
205 |
fun upd (Proved thm) = Proved (Literals (thm_of thm, lits')) |
|
206 |
| upd p = p |
|
207 |
in (the (L.lookup_lit lits' t), Inttab.map_entry idx upd ptab) end |
|
208 |
||
209 |
fun lit_elim conj (p, idx) ct ptab = |
|
210 |
let val lits = literals_of p |
|
211 |
in |
|
212 |
(case L.lookup_lit lits (T.term_of ct) of |
|
213 |
SOME lit => (Thm lit, ptab) |
|
214 |
| NONE => apfst Thm (derive conj (T.term_of ct) lits idx ptab)) |
|
215 |
end |
|
216 |
in |
|
217 |
val and_elim = lit_elim true |
|
218 |
val not_or_elim = lit_elim false |
|
219 |
end |
|
220 |
||
221 |
||
222 |
||
223 |
(* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *) |
|
224 |
local |
|
225 |
fun step lit thm = |
|
226 |
Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit |
|
227 |
val explode_disj = L.explode false false false |
|
228 |
fun intro hyps thm th = fold step (explode_disj hyps th) thm |
|
229 |
||
230 |
fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))] |
|
231 |
val ccontr = T.precompose dest_ccontr @{thm ccontr} |
|
232 |
in |
|
233 |
fun lemma thm ct = |
|
234 |
let |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
235 |
val cu = L.negate (Thm.dest_arg ct) |
36898 | 236 |
val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm)) |
237 |
in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end |
|
238 |
end |
|
239 |
||
240 |
||
241 |
||
242 |
(* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *) |
|
243 |
local |
|
244 |
val explode_disj = L.explode false true false |
|
245 |
val join_disj = L.join false |
|
246 |
fun unit thm thms th = |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
247 |
let val t = @{const Not} $ T.prop_of thm and ts = map T.prop_of thms |
36898 | 248 |
in join_disj (L.make_littab (thms @ explode_disj ts th)) t end |
249 |
||
250 |
fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct) |
|
251 |
fun dest ct = pairself dest_arg2 (Thm.dest_binop ct) |
|
252 |
val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast} |
|
253 |
in |
|
254 |
fun unit_resolution thm thms ct = |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
255 |
L.negate (Thm.dest_arg ct) |
36898 | 256 |
|> T.under_assumption (unit thm thms) |
257 |
|> Thm o T.discharge thm o T.compose contrapos |
|
258 |
end |
|
259 |
||
260 |
||
261 |
||
262 |
(* P ==> P == True or P ==> P == False *) |
|
263 |
local |
|
264 |
val iff1 = @{lemma "P ==> P == (~ False)" by simp} |
|
265 |
val iff2 = @{lemma "~P ==> P == False" by simp} |
|
266 |
in |
|
267 |
fun iff_true thm = MetaEq (thm COMP iff1) |
|
268 |
fun iff_false thm = MetaEq (thm COMP iff2) |
|
269 |
end |
|
270 |
||
271 |
||
272 |
||
273 |
(* distributivity of | over & *) |
|
274 |
fun distributivity ctxt = Thm o try_apply ctxt [] [ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
275 |
named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] |
36898 | 276 |
(* FIXME: not very well tested *) |
277 |
||
278 |
||
279 |
||
280 |
(* Tseitin-like axioms *) |
|
281 |
||
282 |
local |
|
283 |
val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast} |
|
284 |
val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast} |
|
285 |
val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast} |
|
286 |
val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast} |
|
287 |
||
288 |
fun prove' conj1 conj2 ct2 thm = |
|
289 |
let val lits = L.true_thm :: L.explode conj1 true (conj1 <> conj2) [] thm |
|
290 |
in L.join conj2 (L.make_littab lits) (Thm.term_of ct2) end |
|
291 |
||
292 |
fun prove rule (ct1, conj1) (ct2, conj2) = |
|
293 |
T.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule |
|
294 |
||
295 |
fun prove_def_axiom ct = |
|
296 |
let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct) |
|
297 |
in |
|
298 |
(case Thm.term_of ct1 of |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
299 |
@{const Not} $ (@{const HOL.conj} $ _ $ _) => |
36898 | 300 |
prove disjI1 (Thm.dest_arg ct1, true) (ct2, true) |
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
301 |
| @{const HOL.conj} $ _ $ _ => |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
302 |
prove disjI3 (L.negate ct2, false) (ct1, true) |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
303 |
| @{const Not} $ (@{const HOL.disj} $ _ $ _) => |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
304 |
prove disjI3 (L.negate ct2, false) (ct1, false) |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
305 |
| @{const HOL.disj} $ _ $ _ => |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
306 |
prove disjI2 (L.negate ct1, false) (ct2, true) |
40274
6486c610a549
introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40164
diff
changeset
|
307 |
| Const (@{const_name SMT.distinct}, _) $ _ => |
36898 | 308 |
let |
309 |
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv) |
|
310 |
fun prv cu = |
|
311 |
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) |
|
312 |
in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end |
|
313 |
in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
314 |
| @{const Not} $ (Const (@{const_name SMT.distinct}, _) $ _) => |
36898 | 315 |
let |
316 |
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv)) |
|
317 |
fun prv cu = |
|
318 |
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) |
|
319 |
in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end |
|
320 |
in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end |
|
321 |
| _ => raise CTERM ("prove_def_axiom", [ct])) |
|
322 |
end |
|
323 |
in |
|
324 |
fun def_axiom ctxt = Thm o try_apply ctxt [] [ |
|
325 |
named ctxt "conj/disj/distinct" prove_def_axiom, |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
326 |
T.by_abstraction (true, false) ctxt [] (fn ctxt' => |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
327 |
named ctxt' "simp+fast" (T.by_tac simp_fast_tac))] |
36898 | 328 |
end |
329 |
||
330 |
||
331 |
||
332 |
(* local definitions *) |
|
333 |
local |
|
334 |
val intro_rules = [ |
|
335 |
@{lemma "n == P ==> (~n | P) & (n | ~P)" by simp}, |
|
336 |
@{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)" |
|
337 |
by simp}, |
|
338 |
@{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ] |
|
339 |
||
340 |
val apply_rules = [ |
|
341 |
@{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast}, |
|
342 |
@{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n" |
|
343 |
by (atomize(full)) fastsimp} ] |
|
344 |
||
345 |
val inst_rule = T.match_instantiate Thm.dest_arg |
|
346 |
||
347 |
fun apply_rule ct = |
|
348 |
(case get_first (try (inst_rule ct)) intro_rules of |
|
349 |
SOME thm => thm |
|
350 |
| NONE => raise CTERM ("intro_def", [ct])) |
|
351 |
in |
|
352 |
fun intro_def ct = T.make_hyp_def (apply_rule ct) #>> Thm |
|
353 |
||
354 |
fun apply_def thm = |
|
355 |
get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules |
|
356 |
|> the_default (Thm thm) |
|
357 |
end |
|
358 |
||
359 |
||
360 |
||
361 |
(* negation normal form *) |
|
362 |
||
363 |
local |
|
364 |
val quant_rules1 = ([ |
|
365 |
@{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp}, |
|
366 |
@{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [ |
|
367 |
@{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp}, |
|
368 |
@{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}]) |
|
369 |
||
370 |
val quant_rules2 = ([ |
|
371 |
@{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp}, |
|
372 |
@{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [ |
|
373 |
@{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp}, |
|
374 |
@{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}]) |
|
375 |
||
376 |
fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = ( |
|
377 |
Tactic.rtac thm ORELSE' |
|
378 |
(Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE' |
|
379 |
(Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st |
|
380 |
||
381 |
fun nnf_quant vars qs p ct = |
|
382 |
T.as_meta_eq ct |
|
383 |
|> T.by_tac (nnf_quant_tac (T.varify vars (meta_eq_of p)) qs) |
|
384 |
||
385 |
fun prove_nnf ctxt = try_apply ctxt [] [ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
386 |
named ctxt "conj/disj" L.prove_conj_disj_eq, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
387 |
T.by_abstraction (true, false) ctxt [] (fn ctxt' => |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
388 |
named ctxt' "simp+fast" (T.by_tac simp_fast_tac))] |
36898 | 389 |
in |
390 |
fun nnf ctxt vars ps ct = |
|
391 |
(case T.term_of ct of |
|
392 |
_ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) => |
|
393 |
if l aconv r |
|
394 |
then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) |
|
395 |
else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct) |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
396 |
| _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) => |
36898 | 397 |
MetaEq (nnf_quant vars quant_rules2 (hd ps) ct) |
398 |
| _ => |
|
399 |
let |
|
400 |
val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv |
|
401 |
(T.unfold_eqs ctxt (map (Thm.symmetric o meta_eq_of) ps))) |
|
402 |
in Thm (T.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end) |
|
403 |
end |
|
404 |
||
405 |
||
406 |
||
407 |
(** equality proof rules **) |
|
408 |
||
409 |
(* |- t = t *) |
|
410 |
fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) |
|
411 |
||
412 |
||
413 |
||
414 |
(* s = t ==> t = s *) |
|
415 |
local |
|
416 |
val symm_rule = @{lemma "s = t ==> t == s" by simp} |
|
417 |
in |
|
418 |
fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm) |
|
419 |
| symm p = MetaEq (thm_of p COMP symm_rule) |
|
420 |
end |
|
421 |
||
422 |
||
423 |
||
424 |
(* s = t ==> t = u ==> s = u *) |
|
425 |
local |
|
426 |
val trans1 = @{lemma "s == t ==> t = u ==> s == u" by simp} |
|
427 |
val trans2 = @{lemma "s = t ==> t == u ==> s == u" by simp} |
|
428 |
val trans3 = @{lemma "s = t ==> t = u ==> s == u" by simp} |
|
429 |
in |
|
430 |
fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2) |
|
431 |
| trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1)) |
|
432 |
| trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2)) |
|
433 |
| trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3)) |
|
434 |
end |
|
435 |
||
436 |
||
437 |
||
438 |
(* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn |
|
439 |
(reflexive antecendents are droppped) *) |
|
440 |
local |
|
441 |
exception MONO |
|
442 |
||
443 |
fun prove_refl (ct, _) = Thm.reflexive ct |
|
444 |
fun prove_comb f g cp = |
|
445 |
let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp |
|
446 |
in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end |
|
447 |
fun prove_arg f = prove_comb prove_refl f |
|
448 |
||
449 |
fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp |
|
450 |
||
451 |
fun prove_nary is_comb f = |
|
452 |
let |
|
453 |
fun prove (cp as (ct, _)) = f cp handle MONO => |
|
454 |
if is_comb (Thm.term_of ct) |
|
455 |
then prove_comb (prove_arg prove) prove cp |
|
456 |
else prove_refl cp |
|
457 |
in prove end |
|
458 |
||
459 |
fun prove_list f n cp = |
|
460 |
if n = 0 then prove_refl cp |
|
461 |
else prove_comb (prove_arg f) (prove_list f (n-1)) cp |
|
462 |
||
463 |
fun with_length f (cp as (cl, _)) = |
|
464 |
f (length (HOLogic.dest_list (Thm.term_of cl))) cp |
|
465 |
||
466 |
fun prove_distinct f = prove_arg (with_length (prove_list f)) |
|
467 |
||
468 |
fun prove_eq exn lookup cp = |
|
469 |
(case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of |
|
470 |
SOME eq => eq |
|
471 |
| NONE => if exn then raise MONO else prove_refl cp) |
|
472 |
||
473 |
val prove_eq_exn = prove_eq true |
|
474 |
and prove_eq_safe = prove_eq false |
|
475 |
||
476 |
fun mono f (cp as (cl, _)) = |
|
477 |
(case Term.head_of (Thm.term_of cl) of |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
478 |
@{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f) |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
479 |
| @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f) |
40274
6486c610a549
introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40164
diff
changeset
|
480 |
| Const (@{const_name SMT.distinct}, _) => prove_distinct (prove_eq_safe f) |
36898 | 481 |
| _ => prove (prove_eq_safe f)) cp |
482 |
in |
|
483 |
fun monotonicity eqs ct = |
|
484 |
let |
|
485 |
val lookup = AList.lookup (op aconv) (map (`Thm.prop_of o meta_eq_of) eqs) |
|
486 |
val cp = Thm.dest_binop (Thm.dest_arg ct) |
|
487 |
in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end |
|
488 |
end |
|
489 |
||
490 |
||
491 |
||
492 |
(* |- f a b = f b a (where f is equality) *) |
|
493 |
local |
|
494 |
val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)} |
|
495 |
in |
|
496 |
fun commutativity ct = MetaEq (T.match_instantiate I (T.as_meta_eq ct) rule) |
|
497 |
end |
|
498 |
||
499 |
||
500 |
||
501 |
(** quantifier proof rules **) |
|
502 |
||
503 |
(* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x) |
|
504 |
P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x) *) |
|
505 |
local |
|
506 |
val rules = [ |
|
507 |
@{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp}, |
|
508 |
@{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}] |
|
509 |
in |
|
510 |
fun quant_intro vars p ct = |
|
511 |
let |
|
512 |
val thm = meta_eq_of p |
|
513 |
val rules' = T.varify vars thm :: rules |
|
514 |
val cu = T.as_meta_eq ct |
|
515 |
in MetaEq (T.by_tac (REPEAT_ALL_NEW (Tactic.match_tac rules')) cu) end |
|
516 |
end |
|
517 |
||
518 |
||
519 |
||
520 |
(* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *) |
|
521 |
fun pull_quant ctxt = Thm o try_apply ctxt [] [ |
|
522 |
named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] |
|
523 |
(* FIXME: not very well tested *) |
|
524 |
||
525 |
||
526 |
||
527 |
(* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *) |
|
528 |
fun push_quant ctxt = Thm o try_apply ctxt [] [ |
|
529 |
named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] |
|
530 |
(* FIXME: not very well tested *) |
|
531 |
||
532 |
||
533 |
||
534 |
(* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *) |
|
535 |
local |
|
536 |
val elim_all = @{lemma "(ALL x. P) == P" by simp} |
|
537 |
val elim_ex = @{lemma "(EX x. P) == P" by simp} |
|
538 |
||
539 |
fun elim_unused_conv ctxt = |
|
540 |
Conv.params_conv ~1 (K (Conv.arg_conv (Conv.arg1_conv |
|
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset
|
541 |
(Conv.rewrs_conv [elim_all, elim_ex])))) ctxt |
36898 | 542 |
|
543 |
fun elim_unused_tac ctxt = |
|
544 |
REPEAT_ALL_NEW ( |
|
545 |
Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}] |
|
546 |
ORELSE' CONVERSION (elim_unused_conv ctxt)) |
|
547 |
in |
|
548 |
fun elim_unused_vars ctxt = Thm o T.by_tac (elim_unused_tac ctxt) |
|
549 |
end |
|
550 |
||
551 |
||
552 |
||
553 |
(* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *) |
|
554 |
fun dest_eq_res ctxt = Thm o try_apply ctxt [] [ |
|
555 |
named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] |
|
556 |
(* FIXME: not very well tested *) |
|
557 |
||
558 |
||
559 |
||
560 |
(* |- ~(ALL x1...xn. P x1...xn) | P a1...an *) |
|
561 |
local |
|
562 |
val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast} |
|
563 |
in |
|
564 |
val quant_inst = Thm o T.by_tac ( |
|
565 |
REPEAT_ALL_NEW (Tactic.match_tac [rule]) |
|
566 |
THEN' Tactic.rtac @{thm excluded_middle}) |
|
567 |
end |
|
568 |
||
569 |
||
570 |
||
571 |
(* c = SOME x. P x |- (EX x. P x) = P c |
|
572 |
c = SOME x. ~ P x |- ~(ALL x. P x) = ~ P c *) |
|
573 |
local |
|
574 |
val elim_ex = @{lemma "EX x. P == P" by simp} |
|
575 |
val elim_all = @{lemma "~ (ALL x. P) == ~P" by simp} |
|
576 |
val sk_ex = @{lemma "c == SOME x. P x ==> EX x. P x == P c" |
|
577 |
by simp (intro eq_reflection some_eq_ex[symmetric])} |
|
578 |
val sk_all = @{lemma "c == SOME x. ~ P x ==> ~(ALL x. P x) == ~ P c" |
|
579 |
by (simp only: not_all) (intro eq_reflection some_eq_ex[symmetric])} |
|
580 |
val sk_ex_rule = ((sk_ex, I), elim_ex) |
|
581 |
and sk_all_rule = ((sk_all, Thm.dest_arg), elim_all) |
|
582 |
||
583 |
fun dest f sk_rule = |
|
584 |
Thm.dest_comb (f (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of sk_rule)))) |
|
585 |
fun type_of f sk_rule = Thm.ctyp_of_term (snd (dest f sk_rule)) |
|
586 |
fun pair2 (a, b) (c, d) = [(a, c), (b, d)] |
|
587 |
fun inst_sk (sk_rule, f) p c = |
|
588 |
Thm.instantiate ([(type_of f sk_rule, Thm.ctyp_of_term c)], []) sk_rule |
|
589 |
|> (fn sk' => Thm.instantiate ([], (pair2 (dest f sk') (p, c))) sk') |
|
590 |
|> Conv.fconv_rule (Thm.beta_conversion true) |
|
591 |
||
592 |
fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I) |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
593 |
| kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) = |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
594 |
(sk_all_rule, Thm.dest_arg, L.negate) |
36898 | 595 |
| kind t = raise TERM ("skolemize", [t]) |
596 |
||
597 |
fun dest_abs_type (Abs (_, T, _)) = T |
|
598 |
| dest_abs_type t = raise TERM ("dest_abs_type", [t]) |
|
599 |
||
600 |
fun bodies_of thy lhs rhs = |
|
601 |
let |
|
602 |
val (rule, dest, make) = kind (Thm.term_of lhs) |
|
603 |
||
604 |
fun dest_body idx cbs ct = |
|
605 |
let |
|
606 |
val cb = Thm.dest_arg (dest ct) |
|
607 |
val T = dest_abs_type (Thm.term_of cb) |
|
608 |
val cv = Thm.cterm_of thy (Var (("x", idx), T)) |
|
609 |
val cu = make (Drule.beta_conv cb cv) |
|
610 |
val cbs' = (cv, cb) :: cbs |
|
611 |
in |
|
612 |
(snd (Thm.first_order_match (cu, rhs)), rev cbs') |
|
613 |
handle Pattern.MATCH => dest_body (idx+1) cbs' cu |
|
614 |
end |
|
615 |
in (rule, dest_body 1 [] lhs) end |
|
616 |
||
617 |
fun transitive f thm = Thm.transitive thm (f (Thm.rhs_of thm)) |
|
618 |
||
619 |
fun sk_step (rule, elim) (cv, mct, cb) ((is, thm), ctxt) = |
|
620 |
(case mct of |
|
621 |
SOME ct => |
|
622 |
ctxt |
|
623 |
|> T.make_hyp_def (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct) |
|
624 |
|>> pair ((cv, ct) :: is) o Thm.transitive thm |
|
625 |
| NONE => ((is, transitive (Conv.rewr_conv elim) thm), ctxt)) |
|
626 |
in |
|
627 |
fun skolemize ct ctxt = |
|
628 |
let |
|
629 |
val (lhs, rhs) = Thm.dest_binop (Thm.dest_arg ct) |
|
630 |
val (rule, (ctab, cbs)) = bodies_of (ProofContext.theory_of ctxt) lhs rhs |
|
631 |
fun lookup_var (cv, cb) = (cv, AList.lookup (op aconvc) ctab cv, cb) |
|
632 |
in |
|
633 |
(([], Thm.reflexive lhs), ctxt) |
|
634 |
|> fold (sk_step rule) (map lookup_var cbs) |
|
635 |
|>> MetaEq o snd |
|
636 |
end |
|
637 |
end |
|
638 |
||
639 |
||
640 |
||
641 |
(** theory proof rules **) |
|
642 |
||
643 |
(* theory lemmas: linear arithmetic, arrays *) |
|
644 |
||
645 |
fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
646 |
T.by_abstraction (false, true) ctxt thms (fn ctxt' => T.by_tac ( |
36898 | 647 |
NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt') |
648 |
ORELSE' NAMED ctxt' "simp+arith" (Simplifier.simp_tac simpset THEN_ALL_NEW |
|
649 |
Arith_Data.arith_tac ctxt')))] |
|
650 |
||
651 |
||
652 |
||
653 |
(* rewriting: prove equalities: |
|
654 |
* ACI of conjunction/disjunction |
|
655 |
* contradiction, excluded middle |
|
656 |
* logical rewriting rules (for negation, implication, equivalence, |
|
657 |
distinct) |
|
658 |
* normal forms for polynoms (integer/real arithmetic) |
|
659 |
* quantifier elimination over linear arithmetic |
|
660 |
* ... ? **) |
|
661 |
structure Z3_Simps = Named_Thms |
|
662 |
( |
|
663 |
val name = "z3_simp" |
|
664 |
val description = "simplification rules for Z3 proof reconstruction" |
|
665 |
) |
|
666 |
||
667 |
local |
|
668 |
fun spec_meta_eq_of thm = |
|
669 |
(case try (fn th => th RS @{thm spec}) thm of |
|
670 |
SOME thm' => spec_meta_eq_of thm' |
|
671 |
| NONE => mk_meta_eq thm) |
|
672 |
||
673 |
fun prep (Thm thm) = spec_meta_eq_of thm |
|
674 |
| prep (MetaEq thm) = thm |
|
675 |
| prep (Literals (thm, _)) = spec_meta_eq_of thm |
|
676 |
||
677 |
fun unfold_conv ctxt ths = |
|
678 |
Conv.arg_conv (Conv.binop_conv (T.unfold_eqs ctxt (map prep ths))) |
|
679 |
||
680 |
fun with_conv _ [] prv = prv |
|
681 |
| with_conv ctxt ths prv = T.with_conv (unfold_conv ctxt ths) prv |
|
682 |
||
683 |
val unfold_conv = |
|
684 |
Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv)) |
|
685 |
val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq |
|
40663 | 686 |
|
687 |
fun assume_prems ctxt thm = |
|
688 |
Assumption.add_assumes (Drule.cprems_of thm) ctxt |
|
689 |
|>> (fn thms => fold Thm.elim_implies thms thm) |
|
36898 | 690 |
in |
691 |
||
40663 | 692 |
fun rewrite simpset ths ct ctxt = |
693 |
apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [ |
|
694 |
named ctxt "conj/disj/distinct" prove_conj_disj_eq, |
|
695 |
T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac ( |
|
696 |
NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset) |
|
697 |
THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))), |
|
698 |
T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac ( |
|
699 |
NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset) |
|
700 |
THEN_ALL_NEW ( |
|
701 |
NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs) |
|
702 |
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))), |
|
703 |
T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac ( |
|
704 |
NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset) |
|
705 |
THEN_ALL_NEW ( |
|
706 |
NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs) |
|
707 |
ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))), |
|
708 |
named ctxt "injectivity" (M.prove_injectivity ctxt)]) ct)) |
|
36898 | 709 |
|
710 |
end |
|
711 |
||
712 |
||
713 |
||
714 |
(** proof reconstruction **) |
|
715 |
||
716 |
(* tracing and checking *) |
|
717 |
||
718 |
local |
|
719 |
fun count_rules ptab = |
|
720 |
let |
|
721 |
fun count (_, Unproved _) (solved, total) = (solved, total + 1) |
|
722 |
| count (_, Proved _) (solved, total) = (solved + 1, total + 1) |
|
723 |
in Inttab.fold count ptab (0, 0) end |
|
724 |
||
725 |
fun header idx r (solved, total) = |
|
726 |
"Z3: #" ^ string_of_int idx ^ ": " ^ P.string_of_rule r ^ " (goal " ^ |
|
727 |
string_of_int (solved + 1) ^ " of " ^ string_of_int total ^ ")" |
|
728 |
||
729 |
fun check ctxt idx r ps ct p = |
|
730 |
let val thm = thm_of p |> tap (Thm.join_proofs o single) |
|
731 |
in |
|
732 |
if (Thm.cprop_of thm) aconvc ct then () |
|
733 |
else z3_exn (Pretty.string_of (Pretty.big_list ("proof step failed: " ^ |
|
734 |
quote (P.string_of_rule r) ^ " (#" ^ string_of_int idx ^ ")") |
|
735 |
(pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @ |
|
736 |
[Pretty.block [Pretty.str "expected: ", |
|
737 |
Syntax.pretty_term ctxt (Thm.term_of ct)]]))) |
|
738 |
end |
|
739 |
in |
|
740 |
fun trace_rule idx prove r ps ct (cxp as (ctxt, ptab)) = |
|
741 |
let |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40274
diff
changeset
|
742 |
val _ = SMT_Config.trace_msg ctxt (header idx r o count_rules) ptab |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
743 |
val result as (p, (ctxt', _)) = prove r ps ct cxp |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40274
diff
changeset
|
744 |
val _ = if not (Config.get ctxt' SMT_Config.trace) then () |
36898 | 745 |
else check ctxt' idx r ps ct p |
746 |
in result end |
|
747 |
end |
|
748 |
||
749 |
||
750 |
(* overall reconstruction procedure *) |
|
751 |
||
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
752 |
local |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
753 |
fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^ |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
754 |
quote (P.string_of_rule r)) |
36898 | 755 |
|
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
756 |
fun step assms simpset vars r ps ct (cxp as (cx, ptab)) = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
757 |
(case (r, ps) of |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
758 |
(* core rules *) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
759 |
(P.TrueAxiom, _) => (Thm L.true_thm, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
760 |
| (P.Asserted, _) => (asserted cx assms ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
761 |
| (P.Goal, _) => (asserted cx assms ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
762 |
| (P.ModusPonens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
763 |
| (P.ModusPonensOeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
764 |
| (P.AndElim, [(p, i)]) => and_elim (p, i) ct ptab ||> pair cx |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
765 |
| (P.NotOrElim, [(p, i)]) => not_or_elim (p, i) ct ptab ||> pair cx |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
766 |
| (P.Hypothesis, _) => (Thm (Thm.assume ct), cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
767 |
| (P.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
768 |
| (P.UnitResolution, (p, _) :: ps) => |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
769 |
(unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
770 |
| (P.IffTrue, [(p, _)]) => (iff_true (thm_of p), cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
771 |
| (P.IffFalse, [(p, _)]) => (iff_false (thm_of p), cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
772 |
| (P.Distributivity, _) => (distributivity cx ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
773 |
| (P.DefAxiom, _) => (def_axiom cx ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
774 |
| (P.IntroDef, _) => intro_def ct cx ||> rpair ptab |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
775 |
| (P.ApplyDef, [(p, _)]) => (apply_def (thm_of p), cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
776 |
| (P.IffOeq, [(p, _)]) => (p, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
777 |
| (P.NnfPos, _) => (nnf cx vars (map fst ps) ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
778 |
| (P.NnfNeg, _) => (nnf cx vars (map fst ps) ct, cxp) |
36898 | 779 |
|
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
780 |
(* equality rules *) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
781 |
| (P.Reflexivity, _) => (refl ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
782 |
| (P.Symmetry, [(p, _)]) => (symm p, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
783 |
| (P.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
784 |
| (P.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
785 |
| (P.Commutativity, _) => (commutativity ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
786 |
|
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
787 |
(* quantifier rules *) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
788 |
| (P.QuantIntro, [(p, _)]) => (quant_intro vars p ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
789 |
| (P.PullQuant, _) => (pull_quant cx ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
790 |
| (P.PushQuant, _) => (push_quant cx ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
791 |
| (P.ElimUnusedVars, _) => (elim_unused_vars cx ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
792 |
| (P.DestEqRes, _) => (dest_eq_res cx ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
793 |
| (P.QuantInst, _) => (quant_inst ct, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
794 |
| (P.Skolemize, _) => skolemize ct cx ||> rpair ptab |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
795 |
|
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
796 |
(* theory rules *) |
40516 | 797 |
| (P.ThLemma _, _) => (* FIXME: use arguments *) |
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
798 |
(th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp) |
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
799 |
| (P.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab |
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
800 |
| (P.RewriteStar, ps) => rewrite simpset (map fst ps) ct cx ||> rpair ptab |
36898 | 801 |
|
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
802 |
| (P.NnfStar, _) => not_supported r |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
803 |
| (P.CnfStar, _) => not_supported r |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
804 |
| (P.TransitivityStar, _) => not_supported r |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
805 |
| (P.PullQuantStar, _) => not_supported r |
36898 | 806 |
|
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
807 |
| _ => raise Fail ("Z3: proof rule " ^ quote (P.string_of_rule r) ^ |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
808 |
" has an unexpected number of arguments.")) |
36898 | 809 |
|
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
810 |
fun prove ctxt assms vars = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
811 |
let |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
812 |
val simpset = T.make_simpset ctxt (Z3_Simps.get ctxt) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
813 |
|
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
814 |
fun conclude idx rule prop (ps, cxp) = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
815 |
trace_rule idx (step assms simpset vars) rule ps prop cxp |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
816 |
|-> (fn p => apsnd (Inttab.update (idx, Proved p)) #> pair p) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
817 |
|
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
818 |
fun lookup idx (cxp as (_, ptab)) = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
819 |
(case Inttab.lookup ptab idx of |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
820 |
SOME (Unproved (P.Proof_Step {rule, prems, prop})) => |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
821 |
fold_map lookup prems cxp |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
822 |
|>> map2 rpair prems |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
823 |
|> conclude idx rule prop |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
824 |
| SOME (Proved p) => (p, cxp) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
825 |
| NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx))) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
826 |
|
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
827 |
fun result (p, (cx, _)) = (thm_of p, cx) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
828 |
in |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
829 |
(fn idx => result o lookup idx o pair ctxt o Inttab.map (K Unproved)) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
830 |
end |
36898 | 831 |
|
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
832 |
fun filter_assms ctxt assms ptab = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
833 |
let |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
834 |
fun step r ct = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
835 |
(case r of |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
836 |
P.Asserted => insert (op =) (find_assm ctxt assms ct) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
837 |
| P.Goal => insert (op =) (find_assm ctxt assms ct) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
838 |
| _ => I) |
36898 | 839 |
|
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
840 |
fun lookup idx = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
841 |
(case Inttab.lookup ptab idx of |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
842 |
SOME (P.Proof_Step {rule, prems, prop}) => |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
843 |
fold lookup prems #> step rule prop |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
844 |
| NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx))) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
845 |
in lookup end |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
846 |
in |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
847 |
|
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
848 |
fun reconstruct ctxt {typs, terms, unfolds, assms} output = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
849 |
let |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
850 |
val (idx, (ptab, vars, cx)) = P.parse ctxt typs terms output |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
851 |
val assms' = prepare_assms cx unfolds assms |
36898 | 852 |
in |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40274
diff
changeset
|
853 |
if Config.get cx SMT_Config.filter_only_facts |
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
854 |
then ((filter_assms cx assms' ptab idx [], @{thm TrueI}), cx) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
855 |
else apfst (pair []) (prove cx assms' vars idx ptab) |
36898 | 856 |
end |
857 |
||
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
858 |
end |
36898 | 859 |
|
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset
|
860 |
val setup = z3_rules_setup #> Z3_Simps.setup |
36898 | 861 |
|
862 |
end |