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