author | wenzelm |
Thu, 30 May 2013 12:35:40 +0200 | |
changeset 52230 | 1105b3b5aa77 |
parent 51717 | 9e7d1c139569 |
child 52732 | b4da1f2ec73f |
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 -> |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset
|
11 |
int list * thm |
36898 | 12 |
val setup: theory -> theory |
13 |
end |
|
14 |
||
15 |
structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION = |
|
16 |
struct |
|
17 |
||
18 |
||
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
|
19 |
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
|
20 |
("Z3 proof reconstruction: " ^ msg)) |
36898 | 21 |
|
22 |
||
23 |
||
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
24 |
(* net of schematic rules *) |
36898 | 25 |
|
26 |
val z3_ruleN = "z3_rule" |
|
27 |
||
28 |
local |
|
29 |
val description = "declaration of Z3 proof rules" |
|
30 |
||
31 |
val eq = Thm.eq_thm |
|
32 |
||
33 |
structure Z3_Rules = Generic_Data |
|
34 |
( |
|
35 |
type T = thm Net.net |
|
36 |
val empty = Net.empty |
|
37 |
val extend = I |
|
38 |
val merge = Net.merge eq |
|
39 |
) |
|
40 |
||
52230 | 41 |
val prep = `Thm.prop_of o rewrite_rule [Z3_Proof_Literals.rewrite_true] |
36898 | 42 |
|
43 |
fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net |
|
44 |
fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net |
|
45 |
||
46 |
val add = Thm.declaration_attribute (Z3_Rules.map o ins) |
|
47 |
val del = Thm.declaration_attribute (Z3_Rules.map o del) |
|
48 |
in |
|
49 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
50 |
val add_z3_rule = Z3_Rules.map o ins |
36898 | 51 |
|
52 |
fun by_schematic_rule ctxt ct = |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
53 |
the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct) |
36898 | 54 |
|
55 |
val z3_rules_setup = |
|
56 |
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
|
57 |
Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get) |
36898 | 58 |
|
59 |
end |
|
60 |
||
61 |
||
62 |
||
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
63 |
(* proof tools *) |
36898 | 64 |
|
65 |
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
|
66 |
let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") |
36898 | 67 |
in prover ct end |
68 |
||
69 |
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
|
70 |
let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") |
36898 | 71 |
in tac i st end |
72 |
||
73 |
fun pretty_goal ctxt thms t = |
|
74 |
[Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]] |
|
75 |
|> not (null thms) ? cons (Pretty.big_list "assumptions:" |
|
76 |
(map (Display.pretty_thm ctxt) thms)) |
|
77 |
||
78 |
fun try_apply ctxt thms = |
|
79 |
let |
|
80 |
fun try_apply_err ct = Pretty.string_of (Pretty.chunks [ |
|
81 |
Pretty.big_list ("Z3 found a proof," ^ |
|
82 |
" but proof reconstruction failed at the following subgoal:") |
|
83 |
(pretty_goal ctxt thms (Thm.term_of ct)), |
|
84 |
Pretty.str ("Adding a rule to the lemma group " ^ quote z3_ruleN ^ |
|
85 |
" might solve this problem.")]) |
|
86 |
||
87 |
fun apply [] ct = error (try_apply_err ct) |
|
88 |
| apply (prover :: provers) ct = |
|
89 |
(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
|
90 |
SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm) |
36898 | 91 |
| NONE => apply provers ct) |
92 |
||
43893
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset
|
93 |
fun schematic_label full = "schematic rules" |> full ? suffix " (full)" |
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset
|
94 |
fun schematic ctxt full ct = |
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset
|
95 |
ct |
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset
|
96 |
|> full ? fold_rev (curry Drule.mk_implies o Thm.cprop_of) thms |
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset
|
97 |
|> named ctxt (schematic_label full) (by_schematic_rule ctxt) |
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset
|
98 |
|> fold Thm.elim_implies thms |
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset
|
99 |
|
f3e75541cb78
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents:
42992
diff
changeset
|
100 |
in apply o cons (schematic ctxt false) o cons (schematic ctxt true) end |
36898 | 101 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
102 |
local |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
103 |
val rewr_if = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
104 |
@{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
|
105 |
in |
42793 | 106 |
|
107 |
fun HOL_fast_tac ctxt = |
|
108 |
Classical.fast_tac (put_claset HOL_cs ctxt) |
|
109 |
||
110 |
fun simp_fast_tac ctxt = |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset
|
111 |
Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [rewr_if]) |
42793 | 112 |
THEN_ALL_NEW HOL_fast_tac ctxt |
113 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
114 |
end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
115 |
|
36898 | 116 |
|
117 |
||
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
118 |
(* theorems and proofs *) |
36898 | 119 |
|
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
120 |
(** theorem incarnations **) |
36898 | 121 |
|
122 |
datatype theorem = |
|
123 |
Thm of thm | (* theorem without special features *) |
|
124 |
MetaEq of thm | (* meta equality "t == s" *) |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
125 |
Literals of thm * Z3_Proof_Literals.littab |
36898 | 126 |
(* "P1 & ... & Pn" and table of all literals P1, ..., Pn *) |
127 |
||
128 |
fun thm_of (Thm thm) = thm |
|
129 |
| thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq} |
|
130 |
| thm_of (Literals (thm, _)) = thm |
|
131 |
||
132 |
fun meta_eq_of (MetaEq thm) = thm |
|
133 |
| meta_eq_of p = mk_meta_eq (thm_of p) |
|
134 |
||
135 |
fun literals_of (Literals (_, lits)) = lits |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
136 |
| literals_of p = Z3_Proof_Literals.make_littab [thm_of p] |
36898 | 137 |
|
138 |
||
139 |
||
140 |
(** core proof rules **) |
|
141 |
||
142 |
(* assumption *) |
|
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
143 |
|
36898 | 144 |
local |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
145 |
val remove_trigger = mk_meta_eq @{thm SMT.trigger_def} |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
146 |
val remove_weight = mk_meta_eq @{thm SMT.weight_def} |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
147 |
val remove_fun_app = mk_meta_eq @{thm SMT.fun_app_def} |
36898 | 148 |
|
44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset
|
149 |
fun rewrite_conv _ [] = Conv.all_conv |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset
|
150 |
| rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs) |
36898 | 151 |
|
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
152 |
val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight, |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
153 |
remove_fun_app, Z3_Proof_Literals.rewrite_true] |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
154 |
|
44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset
|
155 |
fun rewrite _ [] = I |
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset
|
156 |
| rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs) |
36898 | 157 |
|
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
158 |
fun lookup_assm assms_net ct = |
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
159 |
Z3_Proof_Tools.net_instances assms_net ct |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
160 |
|> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct)) |
36898 | 161 |
in |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
162 |
|
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
163 |
fun add_asserted outer_ctxt rewrite_rules assms asserted ctxt = |
36898 | 164 |
let |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
165 |
val eqs = map (rewrite ctxt [Z3_Proof_Literals.rewrite_true]) rewrite_rules |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
166 |
val eqs' = union Thm.eq_thm eqs prep_rules |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
167 |
|
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
168 |
val assms_net = |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset
|
169 |
assms |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
170 |
|> map (apsnd (rewrite ctxt eqs')) |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset
|
171 |
|> map (apsnd (Conv.fconv_rule Thm.eta_conversion)) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
172 |
|> Z3_Proof_Tools.thm_net_of snd |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
173 |
|
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
174 |
fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
175 |
|
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
176 |
fun assume thm ctxt = |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
177 |
let |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
178 |
val ct = Thm.cprem_of thm 1 |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
179 |
val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
180 |
in (Thm.implies_elim thm thm', ctxt') end |
36898 | 181 |
|
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
182 |
fun add1 idx thm1 ((i, th), exact) ((is, thms), (ctxt, ptab)) = |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
183 |
let |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
184 |
val (thm, ctxt') = |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
185 |
if exact then (Thm.implies_elim thm1 th, ctxt) |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
186 |
else assume thm1 ctxt |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
187 |
val thms' = if exact then thms else th :: thms |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
188 |
in |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
189 |
((insert (op =) i is, thms'), |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
190 |
(ctxt', Inttab.update (idx, Thm thm) ptab)) |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
191 |
end |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
192 |
|
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
193 |
fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) = |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
194 |
let |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
195 |
val thm1 = |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
196 |
Thm.trivial ct |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
197 |
|> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt)) |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
198 |
val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1 |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
199 |
in |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
200 |
(case lookup_assm assms_net (Thm.cprem_of thm2 1) of |
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
201 |
[] => |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
202 |
let val (thm, ctxt') = assume thm1 ctxt |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
203 |
in ((is, thms), (ctxt', Inttab.update (idx, Thm thm) ptab)) end |
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
204 |
| ithms => fold (add1 idx thm1) ithms cx) |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
205 |
end |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
206 |
in fold add asserted (([], []), (ctxt, Inttab.empty)) end |
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
|
207 |
|
36898 | 208 |
end |
209 |
||
210 |
||
211 |
(* P = Q ==> P ==> Q or P --> Q ==> P ==> Q *) |
|
212 |
local |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
213 |
val precomp = Z3_Proof_Tools.precompose2 |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
214 |
val comp = Z3_Proof_Tools.compose |
36898 | 215 |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
216 |
val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp} |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
217 |
val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1 |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
218 |
|
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
219 |
val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1} |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
220 |
val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp} |
36898 | 221 |
in |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
222 |
fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p) |
36898 | 223 |
| mp p_q p = |
224 |
let |
|
225 |
val pq = thm_of p_q |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
226 |
val thm = comp iffD1_c pq handle THM _ => comp mp_c pq |
36898 | 227 |
in Thm (Thm.implies_elim thm p) end |
228 |
end |
|
229 |
||
230 |
||
231 |
(* and_elim: P1 & ... & Pn ==> Pi *) |
|
232 |
(* not_or_elim: ~(P1 | ... | Pn) ==> ~Pi *) |
|
233 |
local |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
234 |
fun is_sublit conj t = Z3_Proof_Literals.exists_lit conj (fn u => u aconv t) |
36898 | 235 |
|
236 |
fun derive conj t lits idx ptab = |
|
237 |
let |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
238 |
val lit = the (Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
239 |
val ls = Z3_Proof_Literals.explode conj false false [t] lit |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
240 |
val lits' = fold Z3_Proof_Literals.insert_lit ls |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
241 |
(Z3_Proof_Literals.delete_lit lit lits) |
36898 | 242 |
|
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
243 |
fun upd thm = Literals (thm_of thm, lits') |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
244 |
val ptab' = Inttab.map_entry idx upd ptab |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
245 |
in (the (Z3_Proof_Literals.lookup_lit lits' t), ptab') end |
36898 | 246 |
|
247 |
fun lit_elim conj (p, idx) ct ptab = |
|
248 |
let val lits = literals_of p |
|
249 |
in |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
250 |
(case Z3_Proof_Literals.lookup_lit lits (SMT_Utils.term_of ct) of |
36898 | 251 |
SOME lit => (Thm lit, ptab) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
252 |
| NONE => apfst Thm (derive conj (SMT_Utils.term_of ct) lits idx ptab)) |
36898 | 253 |
end |
254 |
in |
|
255 |
val and_elim = lit_elim true |
|
256 |
val not_or_elim = lit_elim false |
|
257 |
end |
|
258 |
||
259 |
||
260 |
(* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *) |
|
261 |
local |
|
262 |
fun step lit thm = |
|
263 |
Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
264 |
val explode_disj = Z3_Proof_Literals.explode false false false |
36898 | 265 |
fun intro hyps thm th = fold step (explode_disj hyps th) thm |
266 |
||
267 |
fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))] |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
268 |
val ccontr = Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr} |
36898 | 269 |
in |
270 |
fun lemma thm ct = |
|
271 |
let |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
272 |
val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct) |
44058 | 273 |
val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
274 |
val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
275 |
in Thm (Z3_Proof_Tools.compose ccontr th) end |
36898 | 276 |
end |
277 |
||
278 |
||
279 |
(* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *) |
|
280 |
local |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
281 |
val explode_disj = Z3_Proof_Literals.explode false true false |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
282 |
val join_disj = Z3_Proof_Literals.join false |
36898 | 283 |
fun unit thm thms th = |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
284 |
let |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
285 |
val t = @{const Not} $ SMT_Utils.prop_of thm |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
286 |
val ts = map SMT_Utils.prop_of thms |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
287 |
in |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
288 |
join_disj (Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
289 |
end |
36898 | 290 |
|
291 |
fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct) |
|
292 |
fun dest ct = pairself dest_arg2 (Thm.dest_binop ct) |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
293 |
val contrapos = |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
294 |
Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast} |
36898 | 295 |
in |
296 |
fun unit_resolution thm thms ct = |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
297 |
Z3_Proof_Literals.negate (Thm.dest_arg ct) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
298 |
|> Z3_Proof_Tools.under_assumption (unit thm thms) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
299 |
|> Thm o Z3_Proof_Tools.discharge thm o Z3_Proof_Tools.compose contrapos |
36898 | 300 |
end |
301 |
||
302 |
||
303 |
(* P ==> P == True or P ==> P == False *) |
|
304 |
local |
|
305 |
val iff1 = @{lemma "P ==> P == (~ False)" by simp} |
|
306 |
val iff2 = @{lemma "~P ==> P == False" by simp} |
|
307 |
in |
|
308 |
fun iff_true thm = MetaEq (thm COMP iff1) |
|
309 |
fun iff_false thm = MetaEq (thm COMP iff2) |
|
310 |
end |
|
311 |
||
312 |
||
313 |
(* distributivity of | over & *) |
|
314 |
fun distributivity ctxt = Thm o try_apply ctxt [] [ |
|
42793 | 315 |
named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))] |
36898 | 316 |
(* FIXME: not very well tested *) |
317 |
||
318 |
||
319 |
(* Tseitin-like axioms *) |
|
320 |
local |
|
321 |
val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast} |
|
322 |
val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast} |
|
323 |
val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast} |
|
324 |
val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast} |
|
325 |
||
326 |
fun prove' conj1 conj2 ct2 thm = |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
327 |
let |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
328 |
val littab = |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
329 |
Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
330 |
|> cons Z3_Proof_Literals.true_thm |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
331 |
|> Z3_Proof_Literals.make_littab |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
332 |
in Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end |
36898 | 333 |
|
334 |
fun prove rule (ct1, conj1) (ct2, conj2) = |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
335 |
Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule |
36898 | 336 |
|
337 |
fun prove_def_axiom ct = |
|
338 |
let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct) |
|
339 |
in |
|
340 |
(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
|
341 |
@{const Not} $ (@{const HOL.conj} $ _ $ _) => |
36898 | 342 |
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
|
343 |
| @{const HOL.conj} $ _ $ _ => |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
344 |
prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, 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
|
345 |
| @{const Not} $ (@{const HOL.disj} $ _ $ _) => |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
346 |
prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, false) |
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
|
347 |
| @{const HOL.disj} $ _ $ _ => |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
348 |
prove disjI2 (Z3_Proof_Literals.negate ct1, false) (ct2, true) |
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40680
diff
changeset
|
349 |
| Const (@{const_name distinct}, _) $ _ => |
36898 | 350 |
let |
351 |
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv) |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
352 |
val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv |
36898 | 353 |
fun prv cu = |
354 |
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) |
|
355 |
in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
356 |
in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end |
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40680
diff
changeset
|
357 |
| @{const Not} $ (Const (@{const_name distinct}, _) $ _) => |
36898 | 358 |
let |
359 |
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv)) |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
360 |
val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv |
36898 | 361 |
fun prv cu = |
362 |
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) |
|
363 |
in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
364 |
in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end |
36898 | 365 |
| _ => raise CTERM ("prove_def_axiom", [ct])) |
366 |
end |
|
367 |
in |
|
368 |
fun def_axiom ctxt = Thm o try_apply ctxt [] [ |
|
369 |
named ctxt "conj/disj/distinct" prove_def_axiom, |
|
42992
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
370 |
Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' => |
42793 | 371 |
named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))] |
36898 | 372 |
end |
373 |
||
374 |
||
375 |
(* local definitions *) |
|
376 |
local |
|
377 |
val intro_rules = [ |
|
378 |
@{lemma "n == P ==> (~n | P) & (n | ~P)" by simp}, |
|
379 |
@{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)" |
|
380 |
by simp}, |
|
381 |
@{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ] |
|
382 |
||
383 |
val apply_rules = [ |
|
384 |
@{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast}, |
|
385 |
@{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n" |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44488
diff
changeset
|
386 |
by (atomize(full)) fastforce} ] |
36898 | 387 |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
388 |
val inst_rule = Z3_Proof_Tools.match_instantiate Thm.dest_arg |
36898 | 389 |
|
390 |
fun apply_rule ct = |
|
391 |
(case get_first (try (inst_rule ct)) intro_rules of |
|
392 |
SOME thm => thm |
|
393 |
| NONE => raise CTERM ("intro_def", [ct])) |
|
394 |
in |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
395 |
fun intro_def ct = Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm |
36898 | 396 |
|
397 |
fun apply_def thm = |
|
398 |
get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules |
|
399 |
|> the_default (Thm thm) |
|
400 |
end |
|
401 |
||
402 |
||
403 |
(* negation normal form *) |
|
404 |
local |
|
405 |
val quant_rules1 = ([ |
|
406 |
@{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp}, |
|
407 |
@{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [ |
|
408 |
@{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp}, |
|
409 |
@{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}]) |
|
410 |
||
411 |
val quant_rules2 = ([ |
|
412 |
@{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp}, |
|
413 |
@{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [ |
|
414 |
@{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp}, |
|
415 |
@{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}]) |
|
416 |
||
417 |
fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = ( |
|
418 |
Tactic.rtac thm ORELSE' |
|
419 |
(Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE' |
|
420 |
(Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st |
|
421 |
||
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
422 |
fun nnf_quant_tac_varified vars eq = |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
423 |
nnf_quant_tac (Z3_Proof_Tools.varify vars eq) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
424 |
|
36898 | 425 |
fun nnf_quant vars qs p ct = |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
426 |
Z3_Proof_Tools.as_meta_eq ct |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
427 |
|> Z3_Proof_Tools.by_tac (nnf_quant_tac_varified vars (meta_eq_of p) qs) |
36898 | 428 |
|
429 |
fun prove_nnf ctxt = try_apply ctxt [] [ |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
430 |
named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq, |
42992
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
431 |
Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' => |
42793 | 432 |
named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))] |
36898 | 433 |
in |
434 |
fun nnf ctxt vars ps ct = |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
435 |
(case SMT_Utils.term_of ct of |
36898 | 436 |
_ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) => |
437 |
if l aconv r |
|
438 |
then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) |
|
439 |
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
|
440 |
| _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) => |
36898 | 441 |
MetaEq (nnf_quant vars quant_rules2 (hd ps) ct) |
442 |
| _ => |
|
443 |
let |
|
444 |
val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
445 |
(Z3_Proof_Tools.unfold_eqs ctxt |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
446 |
(map (Thm.symmetric o meta_eq_of) ps))) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
447 |
in Thm (Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end) |
36898 | 448 |
end |
449 |
||
450 |
||
451 |
||
452 |
(** equality proof rules **) |
|
453 |
||
454 |
(* |- t = t *) |
|
455 |
fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) |
|
456 |
||
457 |
||
458 |
(* s = t ==> t = s *) |
|
459 |
local |
|
460 |
val symm_rule = @{lemma "s = t ==> t == s" by simp} |
|
461 |
in |
|
462 |
fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm) |
|
463 |
| symm p = MetaEq (thm_of p COMP symm_rule) |
|
464 |
end |
|
465 |
||
466 |
||
467 |
(* s = t ==> t = u ==> s = u *) |
|
468 |
local |
|
469 |
val trans1 = @{lemma "s == t ==> t = u ==> s == u" by simp} |
|
470 |
val trans2 = @{lemma "s = t ==> t == u ==> s == u" by simp} |
|
471 |
val trans3 = @{lemma "s = t ==> t = u ==> s == u" by simp} |
|
472 |
in |
|
473 |
fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2) |
|
474 |
| trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1)) |
|
475 |
| trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2)) |
|
476 |
| trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3)) |
|
477 |
end |
|
478 |
||
479 |
||
480 |
(* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn |
|
481 |
(reflexive antecendents are droppped) *) |
|
482 |
local |
|
483 |
exception MONO |
|
484 |
||
485 |
fun prove_refl (ct, _) = Thm.reflexive ct |
|
486 |
fun prove_comb f g cp = |
|
487 |
let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp |
|
488 |
in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end |
|
489 |
fun prove_arg f = prove_comb prove_refl f |
|
490 |
||
491 |
fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp |
|
492 |
||
493 |
fun prove_nary is_comb f = |
|
494 |
let |
|
495 |
fun prove (cp as (ct, _)) = f cp handle MONO => |
|
496 |
if is_comb (Thm.term_of ct) |
|
497 |
then prove_comb (prove_arg prove) prove cp |
|
498 |
else prove_refl cp |
|
499 |
in prove end |
|
500 |
||
501 |
fun prove_list f n cp = |
|
502 |
if n = 0 then prove_refl cp |
|
503 |
else prove_comb (prove_arg f) (prove_list f (n-1)) cp |
|
504 |
||
505 |
fun with_length f (cp as (cl, _)) = |
|
506 |
f (length (HOLogic.dest_list (Thm.term_of cl))) cp |
|
507 |
||
508 |
fun prove_distinct f = prove_arg (with_length (prove_list f)) |
|
509 |
||
510 |
fun prove_eq exn lookup cp = |
|
511 |
(case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of |
|
512 |
SOME eq => eq |
|
513 |
| NONE => if exn then raise MONO else prove_refl cp) |
|
514 |
||
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
515 |
val prove_exn = prove_eq true |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
516 |
and prove_safe = prove_eq false |
36898 | 517 |
|
518 |
fun mono f (cp as (cl, _)) = |
|
519 |
(case Term.head_of (Thm.term_of cl) of |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
520 |
@{const HOL.conj} => prove_nary Z3_Proof_Literals.is_conj (prove_exn f) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
521 |
| @{const HOL.disj} => prove_nary Z3_Proof_Literals.is_disj (prove_exn f) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
522 |
| Const (@{const_name distinct}, _) => prove_distinct (prove_safe f) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
523 |
| _ => prove (prove_safe f)) cp |
36898 | 524 |
in |
525 |
fun monotonicity eqs ct = |
|
526 |
let |
|
40680
02caa72cb950
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
boehmes
parents:
40664
diff
changeset
|
527 |
fun and_symmetric (t, thm) = [(t, thm), (t, Thm.symmetric thm)] |
02caa72cb950
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
boehmes
parents:
40664
diff
changeset
|
528 |
val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs |
02caa72cb950
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
boehmes
parents:
40664
diff
changeset
|
529 |
val lookup = AList.lookup (op aconv) teqs |
36898 | 530 |
val cp = Thm.dest_binop (Thm.dest_arg ct) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
531 |
in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end |
36898 | 532 |
end |
533 |
||
534 |
||
535 |
(* |- f a b = f b a (where f is equality) *) |
|
536 |
local |
|
537 |
val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)} |
|
538 |
in |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
539 |
fun commutativity ct = |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
540 |
MetaEq (Z3_Proof_Tools.match_instantiate I |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
541 |
(Z3_Proof_Tools.as_meta_eq ct) rule) |
36898 | 542 |
end |
543 |
||
544 |
||
545 |
||
546 |
(** quantifier proof rules **) |
|
547 |
||
548 |
(* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x) |
|
549 |
P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x) *) |
|
550 |
local |
|
551 |
val rules = [ |
|
552 |
@{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp}, |
|
553 |
@{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}] |
|
554 |
in |
|
555 |
fun quant_intro vars p ct = |
|
556 |
let |
|
557 |
val thm = meta_eq_of p |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
558 |
val rules' = Z3_Proof_Tools.varify vars thm :: rules |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
559 |
val cu = Z3_Proof_Tools.as_meta_eq ct |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
560 |
val tac = REPEAT_ALL_NEW (Tactic.match_tac rules') |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
561 |
in MetaEq (Z3_Proof_Tools.by_tac tac cu) end |
36898 | 562 |
end |
563 |
||
564 |
||
565 |
(* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *) |
|
566 |
fun pull_quant ctxt = Thm o try_apply ctxt [] [ |
|
42793 | 567 |
named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))] |
36898 | 568 |
(* FIXME: not very well tested *) |
569 |
||
570 |
||
571 |
(* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *) |
|
572 |
fun push_quant ctxt = Thm o try_apply ctxt [] [ |
|
42793 | 573 |
named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))] |
36898 | 574 |
(* FIXME: not very well tested *) |
575 |
||
576 |
||
577 |
(* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *) |
|
578 |
local |
|
42318
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset
|
579 |
val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast} |
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset
|
580 |
val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast} |
36898 | 581 |
|
42318
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset
|
582 |
fun elim_unused_tac i st = ( |
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset
|
583 |
Tactic.match_tac [@{thm refl}] |
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset
|
584 |
ORELSE' (Tactic.match_tac [elim_all, elim_ex] THEN' elim_unused_tac) |
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset
|
585 |
ORELSE' ( |
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset
|
586 |
Tactic.match_tac [@{thm iff_allI}, @{thm iff_exI}] |
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset
|
587 |
THEN' elim_unused_tac)) i st |
36898 | 588 |
in |
42318
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset
|
589 |
|
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset
|
590 |
val elim_unused_vars = Thm o Z3_Proof_Tools.by_tac elim_unused_tac |
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset
|
591 |
|
36898 | 592 |
end |
593 |
||
594 |
||
595 |
(* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *) |
|
596 |
fun dest_eq_res ctxt = Thm o try_apply ctxt [] [ |
|
42793 | 597 |
named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))] |
36898 | 598 |
(* FIXME: not very well tested *) |
599 |
||
600 |
||
601 |
(* |- ~(ALL x1...xn. P x1...xn) | P a1...an *) |
|
602 |
local |
|
603 |
val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast} |
|
604 |
in |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
605 |
val quant_inst = Thm o Z3_Proof_Tools.by_tac ( |
36898 | 606 |
REPEAT_ALL_NEW (Tactic.match_tac [rule]) |
607 |
THEN' Tactic.rtac @{thm excluded_middle}) |
|
608 |
end |
|
609 |
||
610 |
||
42196
9893b2913a44
save reflexivity steps in discharging Z3 Skolemization hypotheses
boehmes
parents:
42191
diff
changeset
|
611 |
(* |- (EX x. P x) = P c |- ~(ALL x. P x) = ~ P c *) |
36898 | 612 |
local |
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
613 |
val forall = |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
614 |
SMT_Utils.mk_const_pat @{theory} @{const_name all} |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
615 |
(SMT_Utils.destT1 o SMT_Utils.destT1) |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
616 |
fun mk_forall cv ct = |
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46464
diff
changeset
|
617 |
Thm.apply (SMT_Utils.instT' cv forall) (Thm.lambda cv ct) |
36898 | 618 |
|
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
619 |
fun get_vars f mk pred ctxt t = |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
620 |
Term.fold_aterms f t [] |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
621 |
|> map_filter (fn v => |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
622 |
if pred v then SOME (SMT_Utils.certify ctxt (mk v)) else NONE) |
36898 | 623 |
|
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
624 |
fun close vars f ct ctxt = |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
625 |
let |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
626 |
val frees_of = get_vars Term.add_frees Free (member (op =) vars o fst) |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
627 |
val vs = frees_of ctxt (Thm.term_of ct) |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
628 |
val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
629 |
val vars_of = get_vars Term.add_vars Var (K true) ctxt' |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
630 |
in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end |
36898 | 631 |
|
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
632 |
val sk_rules = @{lemma |
44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset
|
633 |
"c = (SOME x. P x) ==> (EX x. P x) = P c" |
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset
|
634 |
"c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)" |
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
635 |
by (metis someI_ex)+} |
36898 | 636 |
in |
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
637 |
|
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
638 |
fun skolemize vars = |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
639 |
apfst Thm oo close vars (yield_singleton Assumption.add_assumes) |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
640 |
|
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
641 |
fun discharge_sk_tac i st = ( |
44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset
|
642 |
Tactic.rtac @{thm trans} i |
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset
|
643 |
THEN Tactic.resolve_tac sk_rules i |
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset
|
644 |
THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1) |
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44058
diff
changeset
|
645 |
THEN Tactic.rtac @{thm refl} i) st |
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
646 |
|
36898 | 647 |
end |
648 |
||
649 |
||
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
650 |
|
36898 | 651 |
(** theory proof rules **) |
652 |
||
653 |
(* theory lemmas: linear arithmetic, arrays *) |
|
654 |
fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [ |
|
42992
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
655 |
Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt thms (fn ctxt' => |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
656 |
Z3_Proof_Tools.by_tac ( |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
657 |
NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt') |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
658 |
ORELSE' NAMED ctxt' "simp+arith" ( |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset
|
659 |
Simplifier.asm_full_simp_tac (put_simpset simpset ctxt') |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
660 |
THEN_ALL_NEW Arith_Data.arith_tac ctxt')))] |
36898 | 661 |
|
662 |
||
663 |
(* rewriting: prove equalities: |
|
664 |
* ACI of conjunction/disjunction |
|
665 |
* contradiction, excluded middle |
|
666 |
* logical rewriting rules (for negation, implication, equivalence, |
|
667 |
distinct) |
|
668 |
* normal forms for polynoms (integer/real arithmetic) |
|
669 |
* quantifier elimination over linear arithmetic |
|
670 |
* ... ? **) |
|
671 |
structure Z3_Simps = Named_Thms |
|
672 |
( |
|
45294 | 673 |
val name = @{binding z3_simp} |
36898 | 674 |
val description = "simplification rules for Z3 proof reconstruction" |
675 |
) |
|
676 |
||
677 |
local |
|
678 |
fun spec_meta_eq_of thm = |
|
679 |
(case try (fn th => th RS @{thm spec}) thm of |
|
680 |
SOME thm' => spec_meta_eq_of thm' |
|
681 |
| NONE => mk_meta_eq thm) |
|
682 |
||
683 |
fun prep (Thm thm) = spec_meta_eq_of thm |
|
684 |
| prep (MetaEq thm) = thm |
|
685 |
| prep (Literals (thm, _)) = spec_meta_eq_of thm |
|
686 |
||
687 |
fun unfold_conv ctxt ths = |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
688 |
Conv.arg_conv (Conv.binop_conv (Z3_Proof_Tools.unfold_eqs ctxt |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
689 |
(map prep ths))) |
36898 | 690 |
|
691 |
fun with_conv _ [] prv = prv |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
692 |
| with_conv ctxt ths prv = |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
693 |
Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv |
36898 | 694 |
|
695 |
val unfold_conv = |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
696 |
Conv.arg_conv (Conv.binop_conv |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
697 |
(Conv.try_conv Z3_Proof_Tools.unfold_distinct_conv)) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
698 |
val prove_conj_disj_eq = |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
699 |
Z3_Proof_Tools.with_conv unfold_conv Z3_Proof_Literals.prove_conj_disj_eq |
40663 | 700 |
|
41899
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41426
diff
changeset
|
701 |
fun declare_hyps ctxt thm = |
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41426
diff
changeset
|
702 |
(thm, snd (Assumption.add_assumes (#hyps (Thm.crep_thm thm)) ctxt)) |
36898 | 703 |
in |
704 |
||
42992
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
705 |
val abstraction_depth = 3 |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
706 |
(* |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
707 |
This value was chosen large enough to potentially catch exceptions, |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
708 |
yet small enough to not cause too much harm. The value might be |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
709 |
increased in the future, if reconstructing 'rewrite' fails on problems |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
710 |
that get too much abstracted to be reconstructable. |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
711 |
*) |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
712 |
|
40663 | 713 |
fun rewrite simpset ths ct ctxt = |
41899
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41426
diff
changeset
|
714 |
apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [ |
40663 | 715 |
named ctxt "conj/disj/distinct" prove_conj_disj_eq, |
45392
828e08541cee
replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents:
45294
diff
changeset
|
716 |
named ctxt "pull-ite" Z3_Proof_Methods.prove_ite, |
42992
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
717 |
Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' => |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
718 |
Z3_Proof_Tools.by_tac ( |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset
|
719 |
NAMED ctxt' "simp (logic)" (Simplifier.simp_tac (put_simpset simpset ctxt')) |
42793 | 720 |
THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))), |
42992
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
721 |
Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' => |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
722 |
Z3_Proof_Tools.by_tac ( |
46464 | 723 |
(Tactic.rtac @{thm iff_allI} ORELSE' K all_tac) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset
|
724 |
THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt')) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
725 |
THEN_ALL_NEW ( |
42793 | 726 |
NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt') |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
727 |
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))), |
42992
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
728 |
Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' => |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
729 |
Z3_Proof_Tools.by_tac ( |
46464 | 730 |
(Tactic.rtac @{thm iff_allI} ORELSE' K all_tac) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset
|
731 |
THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt')) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
732 |
THEN_ALL_NEW ( |
42793 | 733 |
NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt') |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
734 |
ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))), |
42992
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
735 |
named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt), |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
736 |
Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt [] |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
737 |
(fn ctxt' => |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
738 |
Z3_Proof_Tools.by_tac ( |
46464 | 739 |
(Tactic.rtac @{thm iff_allI} ORELSE' K all_tac) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49980
diff
changeset
|
740 |
THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt')) |
42992
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
741 |
THEN_ALL_NEW ( |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
742 |
NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt') |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
743 |
ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac |
4fc15e3217eb
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents:
42793
diff
changeset
|
744 |
ctxt'))))]) ct)) |
36898 | 745 |
|
746 |
end |
|
747 |
||
748 |
||
749 |
||
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
750 |
(* proof reconstruction *) |
36898 | 751 |
|
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
752 |
(** tracing and checking **) |
36898 | 753 |
|
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
754 |
fun trace_before ctxt idx = SMT_Config.trace_msg ctxt (fn r => |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
755 |
"Z3: #" ^ string_of_int idx ^ ": " ^ Z3_Proof_Parser.string_of_rule r) |
36898 | 756 |
|
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
757 |
fun check_after idx r ps ct (p, (ctxt, _)) = |
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
758 |
if not (Config.get ctxt SMT_Config.trace) then () |
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
759 |
else |
36898 | 760 |
let val thm = thm_of p |> tap (Thm.join_proofs o single) |
761 |
in |
|
762 |
if (Thm.cprop_of thm) aconvc ct then () |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
763 |
else |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
764 |
z3_exn (Pretty.string_of (Pretty.big_list |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
765 |
("proof step failed: " ^ quote (Z3_Proof_Parser.string_of_rule r) ^ |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
766 |
" (#" ^ string_of_int idx ^ ")") |
36898 | 767 |
(pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @ |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
768 |
[Pretty.block [Pretty.str "expected: ", |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
769 |
Syntax.pretty_term ctxt (Thm.term_of ct)]]))) |
36898 | 770 |
end |
771 |
||
772 |
||
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
773 |
(** overall reconstruction procedure **) |
36898 | 774 |
|
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
|
775 |
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
|
776 |
fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^ |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
777 |
quote (Z3_Proof_Parser.string_of_rule r)) |
36898 | 778 |
|
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
779 |
fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) = |
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 |
(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
|
781 |
(* core rules *) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
782 |
(Z3_Proof_Parser.True_Axiom, _) => (Thm Z3_Proof_Literals.true_thm, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
783 |
| (Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion" |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
784 |
| (Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion" |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
785 |
| (Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) => |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
786 |
(mp q (thm_of p), cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
787 |
| (Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) => |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
788 |
(mp q (thm_of p), cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
789 |
| (Z3_Proof_Parser.And_Elim, [(p, i)]) => |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
790 |
and_elim (p, i) ct ptab ||> pair cx |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
791 |
| (Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) => |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
792 |
not_or_elim (p, i) ct ptab ||> pair cx |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
793 |
| (Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
794 |
| (Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
795 |
| (Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) => |
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
|
796 |
(unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
797 |
| (Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
798 |
| (Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
799 |
| (Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
800 |
| (Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
801 |
| (Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx ||> rpair ptab |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
802 |
| (Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
803 |
| (Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
804 |
| (Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
805 |
| (Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp) |
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 |
(* equality rules *) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
808 |
| (Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
809 |
| (Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
810 |
| (Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
811 |
| (Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
812 |
| (Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp) |
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
|
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 |
(* quantifier rules *) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
815 |
| (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
816 |
| (Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
817 |
| (Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp) |
42318
0fd33b6b22cf
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents:
42196
diff
changeset
|
818 |
| (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars ct, cxp) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
819 |
| (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
820 |
| (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp) |
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
821 |
| (Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx ||> rpair ptab |
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
|
822 |
|
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 |
(* theory rules *) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
824 |
| (Z3_Proof_Parser.Th_Lemma _, _) => (* 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
|
825 |
(th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp) |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
826 |
| (Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
827 |
| (Z3_Proof_Parser.Rewrite_Star, ps) => |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
828 |
rewrite simpset (map fst ps) ct cx ||> rpair ptab |
36898 | 829 |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
830 |
| (Z3_Proof_Parser.Nnf_Star, _) => not_supported r |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
831 |
| (Z3_Proof_Parser.Cnf_Star, _) => not_supported r |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
832 |
| (Z3_Proof_Parser.Transitivity_Star, _) => not_supported r |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
833 |
| (Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r |
36898 | 834 |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
835 |
| _ => raise Fail ("Z3: proof rule " ^ |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
836 |
quote (Z3_Proof_Parser.string_of_rule r) ^ |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
837 |
" has an unexpected number of arguments.")) |
36898 | 838 |
|
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
839 |
fun lookup_proof ptab idx = |
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
840 |
(case Inttab.lookup ptab idx of |
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
841 |
SOME p => (p, idx) |
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
842 |
| NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx))) |
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
843 |
|
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
844 |
fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) = |
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
|
845 |
let |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
846 |
val Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step |
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
847 |
val ps = map (lookup_proof ptab) prems |
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
848 |
val _ = trace_before ctxt idx r |
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
849 |
val (thm, (ctxt', ptab')) = |
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
850 |
cxp |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
851 |
|> prove_step simpset vars r ps prop |
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
852 |
|> tap (check_after idx r ps prop) |
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
853 |
in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end |
36898 | 854 |
|
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
855 |
fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl}, |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
856 |
@{thm reflexive}, Z3_Proof_Literals.true_thm] |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
857 |
|
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
858 |
fun discharge_assms_tac rules = |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
859 |
REPEAT (HEADGOAL ( |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
860 |
Tactic.resolve_tac rules ORELSE' SOLVED' discharge_sk_tac)) |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
861 |
|
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
862 |
fun discharge_assms rules thm = |
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
863 |
if Thm.nprems_of thm = 0 then Goal.norm_result thm |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset
|
864 |
else |
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
865 |
(case Seq.pull (discharge_assms_tac rules thm) of |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
45392
diff
changeset
|
866 |
SOME (thm', _) => Goal.norm_result thm' |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset
|
867 |
| NONE => raise THM ("failed to discharge premise", 1, [thm])) |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset
|
868 |
|
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
869 |
fun discharge rules outer_ctxt (p, (inner_ctxt, _)) = |
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset
|
870 |
thm_of p |
42361 | 871 |
|> singleton (Proof_Context.export inner_ctxt outer_ctxt) |
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
872 |
|> discharge_assms (make_discharge_rules rules) |
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
|
873 |
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
|
874 |
|
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset
|
875 |
fun reconstruct outer_ctxt recon output = |
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
|
876 |
let |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset
|
877 |
val {context=ctxt, typs, terms, rewrite_rules, assms} = recon |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
878 |
val (asserted, steps, vars, ctxt1) = |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
879 |
Z3_Proof_Parser.parse ctxt typs terms output |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
880 |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41172
diff
changeset
|
881 |
val simpset = Z3_Proof_Tools.make_simpset ctxt1 (Z3_Simps.get ctxt1) |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
882 |
|
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
883 |
val ((is, rules), cxp as (ctxt2, _)) = |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
884 |
add_asserted outer_ctxt rewrite_rules assms asserted ctxt1 |
36898 | 885 |
in |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
886 |
if Config.get ctxt2 SMT_Config.filter_only_facts then (is, @{thm TrueI}) |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset
|
887 |
else |
41131
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
888 |
(Thm @{thm TrueI}, cxp) |
fc9d503c3d67
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents:
41130
diff
changeset
|
889 |
|> fold (prove simpset vars) steps |
42191
09377c05c561
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents:
41899
diff
changeset
|
890 |
|> discharge rules outer_ctxt |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset
|
891 |
|> pair [] |
36898 | 892 |
end |
893 |
||
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
|
894 |
end |
36898 | 895 |
|
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
|
896 |
val setup = z3_rules_setup #> Z3_Simps.setup |
36898 | 897 |
|
898 |
end |