author | blanchet |
Wed, 03 Sep 2014 00:06:24 +0200 | |
changeset 58152 | 6fe60a9a5bad |
parent 58058 | 1a0b18176548 |
child 59586 | ddf6deaadfe8 |
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_tools.ML |
36898 | 2 |
Author: Sascha Boehme, TU Muenchen |
3 |
||
4 |
Helper functions required for Z3 proof reconstruction. |
|
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_TOOLS = |
36898 | 8 |
sig |
41172
a17c2d669c40
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents:
41123
diff
changeset
|
9 |
(*modifying terms*) |
36898 | 10 |
val as_meta_eq: cterm -> cterm |
11 |
||
41123 | 12 |
(*theorem nets*) |
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
38864
diff
changeset
|
13 |
val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net |
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
44241
diff
changeset
|
14 |
val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list |
36898 | 15 |
val net_instance: thm Net.net -> cterm -> thm option |
16 |
||
41123 | 17 |
(*proof combinators*) |
36898 | 18 |
val under_assumption: (thm -> thm) -> cterm -> thm |
19 |
val with_conv: conv -> (cterm -> thm) -> cterm -> thm |
|
20 |
val discharge: thm -> thm -> thm |
|
21 |
val varify: string list -> thm -> thm |
|
22 |
val unfold_eqs: Proof.context -> thm list -> conv |
|
23 |
val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm |
|
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
51717
diff
changeset
|
24 |
val by_tac: Proof.context -> (int -> tactic) -> cterm -> thm |
36898 | 25 |
val make_hyp_def: thm -> Proof.context -> thm * Proof.context |
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:
42322
diff
changeset
|
26 |
val by_abstraction: int -> bool * bool -> Proof.context -> thm list -> |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
27 |
(Proof.context -> cterm -> thm) -> cterm -> thm |
36898 | 28 |
|
41123 | 29 |
(*a faster COMP*) |
36898 | 30 |
type compose_data |
31 |
val precompose: (cterm -> cterm list) -> thm -> compose_data |
|
32 |
val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data |
|
33 |
val compose: compose_data -> thm -> thm |
|
34 |
||
41123 | 35 |
(*unfolding of 'distinct'*) |
36898 | 36 |
val unfold_distinct_conv: conv |
37 |
||
41123 | 38 |
(*simpset*) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
39 |
val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic |
36898 | 40 |
val make_simpset: Proof.context -> thm list -> simpset |
41 |
end |
|
42 |
||
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
43 |
structure Old_Z3_Proof_Tools: OLD_Z3_PROOF_TOOLS = |
36898 | 44 |
struct |
45 |
||
46 |
||
47 |
||
41172
a17c2d669c40
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents:
41123
diff
changeset
|
48 |
(* modifying terms *) |
36898 | 49 |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
50 |
fun as_meta_eq ct = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
51 |
uncurry Old_SMT_Utils.mk_cequals (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct)) |
36898 | 52 |
|
53 |
||
54 |
||
55 |
(* theorem nets *) |
|
56 |
||
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
38864
diff
changeset
|
57 |
fun thm_net_of f xthms = |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
38864
diff
changeset
|
58 |
let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm) |
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
38864
diff
changeset
|
59 |
in fold insert xthms Net.empty end |
36898 | 60 |
|
61 |
fun maybe_instantiate ct thm = |
|
62 |
try Thm.first_order_match (Thm.cprop_of thm, ct) |
|
63 |
|> Option.map (fn inst => Thm.instantiate inst thm) |
|
64 |
||
42322
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset
|
65 |
local |
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset
|
66 |
fun instances_from_net match f net ct = |
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset
|
67 |
let |
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset
|
68 |
val lookup = if match then Net.match_term else Net.unify_term |
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset
|
69 |
val xthms = lookup net (Thm.term_of 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:
44241
diff
changeset
|
70 |
fun select ct = map_filter (f (maybe_instantiate ct)) xthms |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
44241
diff
changeset
|
71 |
fun select' ct = |
42322
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset
|
72 |
let val thm = Thm.trivial 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:
44241
diff
changeset
|
73 |
in map_filter (f (try (fn rule => rule COMP thm))) xthms end |
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
44241
diff
changeset
|
74 |
in (case select ct of [] => select' ct | xthms' => xthms') end |
42322
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset
|
75 |
in |
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset
|
76 |
|
45410 | 77 |
fun net_instances net = |
45393
13ab80eafd71
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents:
44241
diff
changeset
|
78 |
instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm)) |
45410 | 79 |
net |
42322
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset
|
80 |
|
45410 | 81 |
fun net_instance net = try hd o instances_from_net true I net |
42322
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset
|
82 |
|
be1c32069daa
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents:
41899
diff
changeset
|
83 |
end |
36898 | 84 |
|
85 |
||
86 |
||
87 |
(* proof combinators *) |
|
88 |
||
89 |
fun under_assumption f ct = |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
90 |
let val ct' = Old_SMT_Utils.mk_cprop ct |
36898 | 91 |
in Thm.implies_intr ct' (f (Thm.assume ct')) end |
92 |
||
93 |
fun with_conv conv prove ct = |
|
94 |
let val eq = Thm.symmetric (conv ct) |
|
95 |
in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end |
|
96 |
||
97 |
fun discharge p pq = Thm.implies_elim pq p |
|
98 |
||
99 |
fun varify vars = Drule.generalize ([], vars) |
|
100 |
||
101 |
fun unfold_eqs _ [] = Conv.all_conv |
|
102 |
| unfold_eqs ctxt eqs = |
|
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset
|
103 |
Conv.top_sweep_conv (K (Conv.rewrs_conv eqs)) ctxt |
36898 | 104 |
|
105 |
fun match_instantiate f ct thm = |
|
106 |
Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm |
|
107 |
||
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
51717
diff
changeset
|
108 |
fun by_tac ctxt tac ct = Goal.norm_result ctxt (Goal.prove_internal ctxt [] ct (K (tac 1))) |
36898 | 109 |
|
41123 | 110 |
(* |
111 |
|- c x == t x ==> P (c x) |
|
112 |
--------------------------- |
|
113 |
c == t |- P (c x) |
|
114 |
*) |
|
36898 | 115 |
fun make_hyp_def thm ctxt = |
116 |
let |
|
117 |
val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1) |
|
118 |
val (cf, cvs) = Drule.strip_comb lhs |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
119 |
val eq = Old_SMT_Utils.mk_cequals cf (fold_rev Thm.lambda cvs rhs) |
36898 | 120 |
fun apply cv th = |
121 |
Thm.combination th (Thm.reflexive cv) |
|
122 |
|> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false)) |
|
123 |
in |
|
124 |
yield_singleton Assumption.add_assumes eq ctxt |
|
125 |
|>> Thm.implies_elim thm o fold apply cvs |
|
126 |
end |
|
127 |
||
128 |
||
129 |
||
130 |
(* abstraction *) |
|
131 |
||
132 |
local |
|
133 |
||
134 |
fun abs_context ctxt = (ctxt, Termtab.empty, 1, false) |
|
135 |
||
136 |
fun context_of (ctxt, _, _, _) = ctxt |
|
137 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
138 |
fun replace (_, (cv, ct)) = Thm.forall_elim ct o Thm.forall_intr cv |
36898 | 139 |
|
140 |
fun abs_instantiate (_, tab, _, beta_norm) = |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
141 |
fold replace (Termtab.dest tab) #> |
36898 | 142 |
beta_norm ? Conv.fconv_rule (Thm.beta_conversion true) |
143 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
144 |
fun lambda_abstract cvs t = |
36898 | 145 |
let |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
146 |
val frees = map Free (Term.add_frees t []) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
147 |
val cvs' = filter (fn cv => member (op aconv) frees (Thm.term_of cv)) cvs |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
148 |
val vs = map (Term.dest_Free o Thm.term_of) cvs' |
44241 | 149 |
in (fold_rev absfree vs t, cvs') end |
36898 | 150 |
|
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:
42322
diff
changeset
|
151 |
fun fresh_abstraction (_, cvs) ct (cx as (ctxt, tab, idx, beta_norm)) = |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
152 |
let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct) |
36898 | 153 |
in |
154 |
(case Termtab.lookup tab t of |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
155 |
SOME (cv, _) => (Drule.list_comb (cv, cvs'), cx) |
36898 | 156 |
| NONE => |
157 |
let |
|
158 |
val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
159 |
val cv = Old_SMT_Utils.certify ctxt' |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
160 |
(Free (n, map Old_SMT_Utils.typ_of cvs' ---> Old_SMT_Utils.typ_of ct)) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
161 |
val cu = Drule.list_comb (cv, cvs') |
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45410
diff
changeset
|
162 |
val e = (t, (cv, fold_rev Thm.lambda cvs' ct)) |
36898 | 163 |
val beta_norm' = beta_norm orelse not (null cvs') |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
164 |
in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end) |
36898 | 165 |
end |
166 |
||
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:
42322
diff
changeset
|
167 |
fun abs_comb f g dcvs ct = |
36898 | 168 |
let val (cf, cu) = Thm.dest_comb ct |
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45410
diff
changeset
|
169 |
in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.apply end |
36898 | 170 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
171 |
fun abs_arg f = abs_comb (K pair) f |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
172 |
|
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:
42322
diff
changeset
|
173 |
fun abs_args f dcvs ct = |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
174 |
(case Thm.term_of ct of |
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:
42322
diff
changeset
|
175 |
_ $ _ => abs_comb (abs_args f) f dcvs ct |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
176 |
| _ => pair ct) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
177 |
|
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:
42322
diff
changeset
|
178 |
fun abs_list f g dcvs ct = |
36898 | 179 |
(case Thm.term_of ct of |
180 |
Const (@{const_name Nil}, _) => pair ct |
|
181 |
| Const (@{const_name Cons}, _) $ _ $ _ => |
|
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:
42322
diff
changeset
|
182 |
abs_comb (abs_arg f) (abs_list f g) dcvs ct |
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:
42322
diff
changeset
|
183 |
| _ => g dcvs ct) |
36898 | 184 |
|
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:
42322
diff
changeset
|
185 |
fun abs_abs f (depth, cvs) ct = |
36898 | 186 |
let val (cv, cu) = Thm.dest_abs NONE ct |
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45410
diff
changeset
|
187 |
in f (depth, cv :: cvs) cu #>> Thm.lambda cv end |
36898 | 188 |
|
41899
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41328
diff
changeset
|
189 |
val is_atomic = |
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41328
diff
changeset
|
190 |
(fn Free _ => true | Var _ => true | Bound _ => true | _ => false) |
36898 | 191 |
|
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:
42322
diff
changeset
|
192 |
fun abstract depth (ext_logic, with_theories) = |
36898 | 193 |
let |
194 |
fun abstr1 cvs ct = abs_arg abstr cvs ct |
|
195 |
and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct |
|
196 |
and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct |
|
197 |
and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct |
|
198 |
||
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:
42322
diff
changeset
|
199 |
and abstr (dcvs as (d, cvs)) ct = |
36898 | 200 |
(case Thm.term_of ct of |
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:
42322
diff
changeset
|
201 |
@{const Trueprop} $ _ => abstr1 dcvs ct |
56245 | 202 |
| @{const Pure.imp} $ _ $ _ => abstr2 dcvs 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:
40274
diff
changeset
|
203 |
| @{const True} => pair ct |
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:
40274
diff
changeset
|
204 |
| @{const False} => pair ct |
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:
42322
diff
changeset
|
205 |
| @{const Not} $ _ => abstr1 dcvs ct |
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:
42322
diff
changeset
|
206 |
| @{const HOL.conj} $ _ $ _ => abstr2 dcvs ct |
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:
42322
diff
changeset
|
207 |
| @{const HOL.disj} $ _ $ _ => abstr2 dcvs ct |
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:
42322
diff
changeset
|
208 |
| @{const HOL.implies} $ _ $ _ => abstr2 dcvs ct |
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:
42322
diff
changeset
|
209 |
| Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 dcvs ct |
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
210 |
| Const (@{const_name distinct}, _) $ _ => |
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:
42322
diff
changeset
|
211 |
if ext_logic then abs_arg (abs_list abstr fresh_abstraction) dcvs ct |
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:
42322
diff
changeset
|
212 |
else fresh_abstraction dcvs ct |
36898 | 213 |
| Const (@{const_name If}, _) $ _ $ _ $ _ => |
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:
42322
diff
changeset
|
214 |
if ext_logic then abstr3 dcvs ct else fresh_abstraction dcvs ct |
36898 | 215 |
| Const (@{const_name All}, _) $ _ => |
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:
42322
diff
changeset
|
216 |
if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct |
36898 | 217 |
| Const (@{const_name Ex}, _) $ _ => |
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:
42322
diff
changeset
|
218 |
if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
219 |
| t => (fn cx => |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
220 |
if is_atomic t orelse can HOLogic.dest_number t then (ct, cx) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
221 |
else if with_theories andalso |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
222 |
Old_Z3_Interface.is_builtin_theory_term (context_of cx) t |
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:
42322
diff
changeset
|
223 |
then abs_args abstr dcvs ct cx |
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:
42322
diff
changeset
|
224 |
else if d = 0 then fresh_abstraction dcvs ct cx |
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:
42322
diff
changeset
|
225 |
else |
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:
42322
diff
changeset
|
226 |
(case Term.strip_comb t of |
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:
42322
diff
changeset
|
227 |
(Const _, _) => abs_args abstr (d-1, cvs) ct cx |
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:
42322
diff
changeset
|
228 |
| (Free _, _) => abs_args abstr (d-1, cvs) ct cx |
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:
42322
diff
changeset
|
229 |
| _ => fresh_abstraction dcvs ct cx))) |
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:
42322
diff
changeset
|
230 |
in abstr (depth, []) end |
36898 | 231 |
|
56245 | 232 |
val cimp = Thm.cterm_of @{theory} @{const Pure.imp} |
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:
40274
diff
changeset
|
233 |
|
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:
42322
diff
changeset
|
234 |
fun deepen depth f x = |
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:
42322
diff
changeset
|
235 |
if depth = 0 then f depth x |
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:
42322
diff
changeset
|
236 |
else (case try (f depth) x of SOME y => y | NONE => deepen (depth - 1) f x) |
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:
42322
diff
changeset
|
237 |
|
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:
42322
diff
changeset
|
238 |
fun with_prems depth thms f 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:
40274
diff
changeset
|
239 |
fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct |
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:
42322
diff
changeset
|
240 |
|> deepen depth f |
36898 | 241 |
|> fold (fn prem => fn th => Thm.implies_elim th prem) thms |
242 |
||
243 |
in |
|
244 |
||
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:
42322
diff
changeset
|
245 |
fun by_abstraction depth mode ctxt thms prove = |
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:
42322
diff
changeset
|
246 |
with_prems depth thms (fn d => fn ct => |
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:
42322
diff
changeset
|
247 |
let val (cu, cx) = abstract d mode ct (abs_context 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:
42322
diff
changeset
|
248 |
in abs_instantiate cx (prove (context_of cx) cu) end) |
36898 | 249 |
|
250 |
end |
|
251 |
||
252 |
||
253 |
||
254 |
(* a faster COMP *) |
|
255 |
||
256 |
type compose_data = cterm list * (cterm -> cterm list) * thm |
|
257 |
||
258 |
fun list2 (x, y) = [x, y] |
|
259 |
||
260 |
fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule) |
|
261 |
fun precompose2 f rule = precompose (list2 o f) rule |
|
262 |
||
263 |
fun compose (cvs, f, rule) thm = |
|
264 |
discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule) |
|
265 |
||
266 |
||
267 |
||
268 |
(* unfolding of 'distinct' *) |
|
269 |
||
270 |
local |
|
271 |
val set1 = @{lemma "x ~: set [] == ~False" by simp} |
|
272 |
val set2 = @{lemma "x ~: set [x] == False" by simp} |
|
273 |
val set3 = @{lemma "x ~: set [y] == x ~= y" by simp} |
|
274 |
val set4 = @{lemma "x ~: set (x # ys) == False" by simp} |
|
275 |
val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp} |
|
276 |
||
277 |
fun set_conv ct = |
|
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset
|
278 |
(Conv.rewrs_conv [set1, set2, set3, set4] else_conv |
36898 | 279 |
(Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct |
280 |
||
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
281 |
val dist1 = @{lemma "distinct [] == ~False" by (simp add: distinct_def)} |
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
282 |
val dist2 = @{lemma "distinct [x] == ~False" by (simp add: distinct_def)} |
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
283 |
val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs" |
40274
6486c610a549
introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40164
diff
changeset
|
284 |
by (simp add: distinct_def)} |
36898 | 285 |
|
286 |
fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 |
|
287 |
in |
|
288 |
fun unfold_distinct_conv ct = |
|
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset
|
289 |
(Conv.rewrs_conv [dist1, dist2] else_conv |
36898 | 290 |
(Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct |
291 |
end |
|
292 |
||
293 |
||
294 |
||
295 |
(* simpset *) |
|
296 |
||
297 |
local |
|
298 |
val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv} |
|
299 |
val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2} |
|
300 |
val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1} |
|
301 |
val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3} |
|
302 |
||
303 |
fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm |
|
304 |
fun dest_binop ((c as Const _) $ t $ u) = (c, t, u) |
|
305 |
| dest_binop t = raise TERM ("dest_binop", [t]) |
|
306 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
307 |
fun prove_antisym_le ctxt t = |
36898 | 308 |
let |
309 |
val (le, r, s) = dest_binop t |
|
310 |
val less = Const (@{const_name less}, Term.fastype_of le) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
311 |
val prems = Simplifier.prems_of ctxt |
36898 | 312 |
in |
313 |
(case find_first (eq_prop (le $ s $ r)) prems of |
|
314 |
NONE => |
|
315 |
find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems |
|
316 |
|> Option.map (fn thm => thm RS antisym_less1) |
|
317 |
| SOME thm => SOME (thm RS antisym_le1)) |
|
318 |
end |
|
319 |
handle THM _ => NONE |
|
320 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
321 |
fun prove_antisym_less ctxt t = |
36898 | 322 |
let |
323 |
val (less, r, s) = dest_binop (HOLogic.dest_not t) |
|
324 |
val le = Const (@{const_name less_eq}, Term.fastype_of less) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
325 |
val prems = Simplifier.prems_of ctxt |
36898 | 326 |
in |
327 |
(case find_first (eq_prop (le $ r $ s)) prems of |
|
328 |
NONE => |
|
329 |
find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems |
|
330 |
|> Option.map (fn thm => thm RS antisym_less2) |
|
331 |
| SOME thm => SOME (thm RS antisym_le2)) |
|
332 |
end |
|
333 |
handle THM _ => NONE |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
334 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
335 |
val basic_simpset = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
336 |
simpset_of (put_simpset HOL_ss @{context} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
337 |
addsimps @{thms field_simps} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
338 |
addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}] |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
339 |
addsimps @{thms arith_special} addsimps @{thms arith_simps} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
340 |
addsimps @{thms rel_simps} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
341 |
addsimps @{thms array_rules} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
342 |
addsimps @{thms term_true_def} addsimps @{thms term_false_def} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
343 |
addsimps @{thms z3div_def} addsimps @{thms z3mod_def} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
344 |
addsimprocs [@{simproc binary_int_div}, @{simproc binary_int_mod}] |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
345 |
addsimprocs [ |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
346 |
Simplifier.simproc_global @{theory} "fast_int_arith" [ |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
347 |
"(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
348 |
Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"] |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
349 |
prove_antisym_le, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
350 |
Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"] |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
351 |
prove_antisym_less]) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
352 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
353 |
structure Simpset = Generic_Data |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
354 |
( |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
355 |
type T = simpset |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
356 |
val empty = basic_simpset |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
357 |
val extend = I |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
358 |
val merge = Simplifier.merge_ss |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
359 |
) |
36898 | 360 |
in |
361 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
362 |
fun add_simproc simproc context = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
363 |
Simpset.map (simpset_map (Context.proof_of context) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
364 |
(fn ctxt => ctxt addsimprocs [simproc])) context |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
365 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
366 |
fun make_simpset ctxt rules = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
367 |
simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules) |
36898 | 368 |
|
369 |
end |
|
370 |
||
371 |
end |