author | smolkas |
Tue, 09 Jul 2013 18:44:59 +0200 | |
changeset 52555 | 6811291d1869 |
parent 52454 | b528a975b256 |
child 52556 | c8357085217c |
permissions | -rw-r--r-- |
49883 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
Author: Steffen Juilf Smolka, TU Muenchen |
|
4 |
||
49914 | 5 |
Isar proof reconstruction from ATP proofs. |
49883 | 6 |
*) |
7 |
||
52374 | 8 |
signature SLEDGEHAMMER_RECONSTRUCT = |
49883 | 9 |
sig |
49914 | 10 |
type 'a proof = 'a ATP_Proof.proof |
11 |
type stature = ATP_Problem_Generate.stature |
|
52555 | 12 |
type one_line_params = Sledgehammer_Print.one_line_params |
49914 | 13 |
|
14 |
type isar_params = |
|
51879 | 15 |
bool * bool * Time.time option * bool * real * string Symtab.table |
52150
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
16 |
* (string * stature) list vector * (string * term) list * int Symtab.table |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
17 |
* string proof * thm |
49914 | 18 |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
19 |
val lam_trans_of_atp_proof : string proof -> string -> string |
49914 | 20 |
val is_typed_helper_used_in_atp_proof : string proof -> bool |
21 |
val used_facts_in_atp_proof : |
|
22 |
Proof.context -> (string * stature) list vector -> string proof -> |
|
23 |
(string * stature) list |
|
24 |
val used_facts_in_unsound_atp_proof : |
|
25 |
Proof.context -> (string * stature) list vector -> 'a proof -> |
|
26 |
string list option |
|
49883 | 27 |
val isar_proof_text : |
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
28 |
Proof.context -> bool option -> isar_params -> one_line_params -> string |
49883 | 29 |
val proof_text : |
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
30 |
Proof.context -> bool option -> isar_params -> int -> one_line_params |
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
31 |
-> string |
49883 | 32 |
end; |
33 |
||
52374 | 34 |
structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT = |
49883 | 35 |
struct |
36 |
||
37 |
open ATP_Util |
|
49914 | 38 |
open ATP_Problem |
49883 | 39 |
open ATP_Proof |
40 |
open ATP_Problem_Generate |
|
41 |
open ATP_Proof_Reconstruct |
|
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset
|
42 |
open Sledgehammer_Util |
52555 | 43 |
open Sledgehammer_Reconstructor |
50264
a9ec48b98734
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
smolkas
parents:
50262
diff
changeset
|
44 |
open Sledgehammer_Proof |
50258 | 45 |
open Sledgehammer_Annotate |
52555 | 46 |
open Sledgehammer_Print |
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
51129
diff
changeset
|
47 |
open Sledgehammer_Compress |
49914 | 48 |
|
49 |
structure String_Redirect = ATP_Proof_Redirect( |
|
50 |
type key = step_name |
|
51 |
val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') |
|
52 |
val string_of = fst) |
|
53 |
||
49883 | 54 |
open String_Redirect |
55 |
||
49914 | 56 |
(** fact extraction from ATP proofs **) |
57 |
||
58 |
fun find_first_in_list_vector vec key = |
|
59 |
Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key |
|
60 |
| (_, value) => value) NONE vec |
|
61 |
||
62 |
val unprefix_fact_number = space_implode "_" o tl o space_explode "_" |
|
63 |
||
64 |
fun resolve_one_named_fact fact_names s = |
|
65 |
case try (unprefix fact_prefix) s of |
|
66 |
SOME s' => |
|
67 |
let val s' = s' |> unprefix_fact_number |> unascii_of in |
|
68 |
s' |> find_first_in_list_vector fact_names |> Option.map (pair s') |
|
69 |
end |
|
70 |
| NONE => NONE |
|
71 |
fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names) |
|
72 |
fun is_fact fact_names = not o null o resolve_fact fact_names |
|
73 |
||
74 |
fun resolve_one_named_conjecture s = |
|
75 |
case try (unprefix conjecture_prefix) s of |
|
76 |
SOME s' => Int.fromString s' |
|
77 |
| NONE => NONE |
|
78 |
||
79 |
val resolve_conjecture = map_filter resolve_one_named_conjecture |
|
80 |
val is_conjecture = not o null o resolve_conjecture |
|
81 |
||
82 |
val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix |
|
83 |
||
84 |
(* overapproximation (good enough) *) |
|
85 |
fun is_lam_lifted s = |
|
86 |
String.isPrefix fact_prefix s andalso |
|
87 |
String.isSubstring ascii_of_lam_fact_prefix s |
|
88 |
||
89 |
val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix) |
|
90 |
||
91 |
fun is_axiom_used_in_proof pred = |
|
51202 | 92 |
exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false) |
49914 | 93 |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
94 |
fun lam_trans_of_atp_proof atp_proof default = |
49914 | 95 |
case (is_axiom_used_in_proof is_combinator_def atp_proof, |
96 |
is_axiom_used_in_proof is_lam_lifted atp_proof) of |
|
97 |
(false, false) => default |
|
98 |
| (false, true) => liftingN |
|
99 |
(* | (true, true) => combs_and_liftingN -- not supported by "metis" *) |
|
100 |
| (true, _) => combsN |
|
101 |
||
102 |
val is_typed_helper_name = |
|
103 |
String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix |
|
51031
63d71b247323
more robustness in Isar proof reconstruction (cf. bug report by Ondrej)
blanchet
parents:
51026
diff
changeset
|
104 |
|
49914 | 105 |
fun is_typed_helper_used_in_atp_proof atp_proof = |
106 |
is_axiom_used_in_proof is_typed_helper_name atp_proof |
|
107 |
||
108 |
fun add_non_rec_defs fact_names accum = |
|
109 |
Vector.foldl (fn (facts, facts') => |
|
110 |
union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) |
|
111 |
facts') |
|
112 |
accum fact_names |
|
113 |
||
114 |
val isa_ext = Thm.get_name_hint @{thm ext} |
|
115 |
val isa_short_ext = Long_Name.base_name isa_ext |
|
116 |
||
117 |
fun ext_name ctxt = |
|
118 |
if Thm.eq_thm_prop (@{thm ext}, |
|
51026 | 119 |
singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then |
49914 | 120 |
isa_short_ext |
121 |
else |
|
122 |
isa_ext |
|
123 |
||
50675 | 124 |
val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" |
125 |
val leo2_unfold_def_rule = "unfold_def" |
|
49914 | 126 |
|
51201 | 127 |
fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) = |
51198 | 128 |
(if rule = leo2_extcnf_equal_neg_rule then |
129 |
insert (op =) (ext_name ctxt, (Global, General)) |
|
130 |
else if rule = leo2_unfold_def_rule then |
|
131 |
(* LEO 1.3.3 does not record definitions properly, leading to missing |
|
132 |
dependencies in the TSTP proof. Remove the next line once this is |
|
133 |
fixed. *) |
|
134 |
add_non_rec_defs fact_names |
|
52077 | 135 |
else if rule = agsyhol_coreN orelse rule = satallax_coreN then |
51198 | 136 |
(fn [] => |
52077 | 137 |
(* agsyHOL and Satallax don't include definitions in their |
138 |
unsatisfiable cores, so we assume the worst and include them all |
|
139 |
here. *) |
|
51198 | 140 |
[(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names |
141 |
| facts => facts) |
|
142 |
else |
|
143 |
I) |
|
144 |
#> (if null deps then union (op =) (resolve_fact fact_names ss) else I) |
|
49914 | 145 |
|
146 |
fun used_facts_in_atp_proof ctxt fact_names atp_proof = |
|
147 |
if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names |
|
148 |
else fold (add_fact ctxt fact_names) atp_proof [] |
|
149 |
||
150 |
fun used_facts_in_unsound_atp_proof _ _ [] = NONE |
|
151 |
| used_facts_in_unsound_atp_proof ctxt fact_names atp_proof = |
|
152 |
let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in |
|
153 |
if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso |
|
154 |
not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then |
|
155 |
SOME (map fst used_facts) |
|
156 |
else |
|
157 |
NONE |
|
158 |
end |
|
159 |
||
160 |
||
161 |
(** Isar proof construction and manipulation **) |
|
162 |
||
50017 | 163 |
val assume_prefix = "a" |
49914 | 164 |
val have_prefix = "f" |
165 |
val raw_prefix = "x" |
|
166 |
||
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51976
diff
changeset
|
167 |
fun raw_label_of_name (num, ss) = |
49914 | 168 |
case resolve_conjecture ss of |
169 |
[j] => (conjecture_prefix, j) |
|
170 |
| _ => (raw_prefix ^ ascii_of num, 0) |
|
171 |
||
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51976
diff
changeset
|
172 |
fun label_of_clause [name] = raw_label_of_name name |
51976
e5303bd748f2
generate valid direct Isar proof also if the facts are contradictory
blanchet
parents:
51879
diff
changeset
|
173 |
| label_of_clause c = |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51976
diff
changeset
|
174 |
(space_implode "___" (map (fst o raw_label_of_name) c), 0) |
50005 | 175 |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
176 |
fun add_fact_of_dependencies fact_names (names as [(_, ss)]) = |
50005 | 177 |
if is_fact fact_names ss then |
178 |
apsnd (union (op =) (map fst (resolve_fact fact_names ss))) |
|
179 |
else |
|
180 |
apfst (insert (op =) (label_of_clause names)) |
|
52034
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset
|
181 |
| add_fact_of_dependencies _ names = |
50005 | 182 |
apfst (insert (op =) (label_of_clause names)) |
49914 | 183 |
|
184 |
fun repair_name "$true" = "c_True" |
|
185 |
| repair_name "$false" = "c_False" |
|
186 |
| repair_name "$$e" = tptp_equal (* seen in Vampire proofs *) |
|
187 |
| repair_name s = |
|
188 |
if is_tptp_equal s orelse |
|
189 |
(* seen in Vampire proofs *) |
|
190 |
(String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then |
|
191 |
tptp_equal |
|
192 |
else |
|
193 |
s |
|
194 |
||
195 |
fun infer_formula_types ctxt = |
|
196 |
Type.constraint HOLogic.boolT |
|
197 |
#> Syntax.check_term |
|
198 |
(Proof_Context.set_mode Proof_Context.mode_schematic ctxt) |
|
199 |
||
200 |
val combinator_table = |
|
201 |
[(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}), |
|
202 |
(@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}), |
|
203 |
(@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}), |
|
204 |
(@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}), |
|
205 |
(@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})] |
|
206 |
||
207 |
fun uncombine_term thy = |
|
208 |
let |
|
209 |
fun aux (t1 $ t2) = betapply (pairself aux (t1, t2)) |
|
210 |
| aux (Abs (s, T, t')) = Abs (s, T, aux t') |
|
211 |
| aux (t as Const (x as (s, _))) = |
|
212 |
(case AList.lookup (op =) combinator_table s of |
|
213 |
SOME thm => thm |> prop_of |> specialize_type thy x |
|
214 |
|> Logic.dest_equals |> snd |
|
215 |
| NONE => t) |
|
216 |
| aux t = t |
|
217 |
in aux end |
|
218 |
||
52150
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
219 |
fun unlift_term lifted = |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
220 |
map_aterms (fn t as Const (s, _) => |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
221 |
if String.isPrefix lam_lifted_prefix s then |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
222 |
case AList.lookup (op =) lifted s of |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
223 |
SOME t => |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
224 |
(* FIXME: do something about the types *) |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
225 |
unlift_term lifted t |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
226 |
| NONE => t |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
227 |
else |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
228 |
t |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
229 |
| t => t) |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
230 |
|
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
231 |
fun decode_line ctxt lifted sym_tab (name, role, u, rule, deps) = |
51198 | 232 |
let |
233 |
val thy = Proof_Context.theory_of ctxt |
|
52125
ac7830871177
improved handling of free variables' types in Isar proofs
blanchet
parents:
52077
diff
changeset
|
234 |
val t = |
ac7830871177
improved handling of free variables' types in Isar proofs
blanchet
parents:
52077
diff
changeset
|
235 |
u |> prop_of_atp ctxt true sym_tab |
ac7830871177
improved handling of free variables' types in Isar proofs
blanchet
parents:
52077
diff
changeset
|
236 |
|> uncombine_term thy |
52150
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
237 |
|> unlift_term lifted |
52125
ac7830871177
improved handling of free variables' types in Isar proofs
blanchet
parents:
52077
diff
changeset
|
238 |
|> infer_formula_types ctxt |
ac7830871177
improved handling of free variables' types in Isar proofs
blanchet
parents:
52077
diff
changeset
|
239 |
in (name, role, t, rule, deps) end |
49914 | 240 |
|
241 |
fun replace_one_dependency (old, new) dep = |
|
242 |
if is_same_atp_step dep old then new else [dep] |
|
51201 | 243 |
fun replace_dependencies_in_line p (name, role, t, rule, deps) = |
244 |
(name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps []) |
|
49914 | 245 |
|
246 |
(* No "real" literals means only type information (tfree_tcs, clsrel, or |
|
247 |
clsarity). *) |
|
248 |
fun is_only_type_information t = t aconv @{term True} |
|
249 |
||
50905 | 250 |
fun s_maybe_not role = role <> Conjecture ? s_not |
251 |
||
51201 | 252 |
fun is_same_inference (role, t) (_, role', t', _, _) = |
253 |
s_maybe_not role t aconv s_maybe_not role' t' |
|
49914 | 254 |
|
255 |
(* Discard facts; consolidate adjacent lines that prove the same formula, since |
|
256 |
they differ only in type information.*) |
|
51201 | 257 |
fun add_line fact_names (name as (_, ss), role, t, rule, []) lines = |
49914 | 258 |
(* No dependencies: fact, conjecture, or (for Vampire) internal facts or |
259 |
definitions. *) |
|
50905 | 260 |
if is_conjecture ss then |
51201 | 261 |
(name, role, t, rule, []) :: lines |
50905 | 262 |
else if is_fact fact_names ss then |
49914 | 263 |
(* Facts are not proof lines. *) |
264 |
if is_only_type_information t then |
|
265 |
map (replace_dependencies_in_line (name, [])) lines |
|
50905 | 266 |
else |
267 |
lines |
|
49914 | 268 |
else |
269 |
map (replace_dependencies_in_line (name, [])) lines |
|
51201 | 270 |
| add_line _ (line as (name, role, t, _, _)) lines = |
49914 | 271 |
(* Type information will be deleted later; skip repetition test. *) |
272 |
if is_only_type_information t then |
|
50675 | 273 |
line :: lines |
49914 | 274 |
(* Is there a repetition? If so, replace later line by earlier one. *) |
50905 | 275 |
else case take_prefix (not o is_same_inference (role, t)) lines of |
50675 | 276 |
(_, []) => line :: lines |
51201 | 277 |
| (pre, (name', _, _, _, _) :: post) => |
50675 | 278 |
line :: pre @ map (replace_dependencies_in_line (name', [name])) post |
49914 | 279 |
|
280 |
val waldmeister_conjecture_num = "1.0.0.0" |
|
281 |
||
51258 | 282 |
fun repair_waldmeister_endgame arg = |
49914 | 283 |
let |
51201 | 284 |
fun do_tail (name, _, t, rule, deps) = |
285 |
(name, Negated_Conjecture, s_not t, rule, deps) |
|
49914 | 286 |
fun do_body [] = [] |
51201 | 287 |
| do_body ((line as ((num, _), _, _, _, _)) :: lines) = |
49914 | 288 |
if num = waldmeister_conjecture_num then map do_tail (line :: lines) |
289 |
else line :: do_body lines |
|
51258 | 290 |
in do_body arg end |
49914 | 291 |
|
292 |
(* Recursively delete empty lines (type information) from the proof. *) |
|
51201 | 293 |
fun add_nontrivial_line (line as (name, _, t, _, [])) lines = |
49914 | 294 |
if is_only_type_information t then delete_dependency name lines |
295 |
else line :: lines |
|
296 |
| add_nontrivial_line line lines = line :: lines |
|
297 |
and delete_dependency name lines = |
|
298 |
fold_rev add_nontrivial_line |
|
299 |
(map (replace_dependencies_in_line (name, [])) lines) [] |
|
300 |
||
50675 | 301 |
val e_skolemize_rule = "skolemize" |
302 |
val vampire_skolemisation_rule = "skolemisation" |
|
303 |
||
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
304 |
val is_skolemize_rule = |
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
305 |
member (op =) [e_skolemize_rule, vampire_skolemisation_rule] |
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
306 |
|
52125
ac7830871177
improved handling of free variables' types in Isar proofs
blanchet
parents:
52077
diff
changeset
|
307 |
fun add_desired_line fact_names (name as (_, ss), role, t, rule, deps) |
51201 | 308 |
(j, lines) = |
51198 | 309 |
(j + 1, |
310 |
if is_fact fact_names ss orelse |
|
311 |
is_conjecture ss orelse |
|
312 |
is_skolemize_rule rule orelse |
|
313 |
(* the last line must be kept *) |
|
314 |
j = 0 orelse |
|
315 |
(not (is_only_type_information t) andalso |
|
316 |
null (Term.add_tvars t []) andalso |
|
317 |
length deps >= 2 andalso |
|
318 |
(* kill next to last line, which usually results in a trivial step *) |
|
319 |
j <> 1) then |
|
51201 | 320 |
(name, role, t, rule, deps) :: lines (* keep line *) |
51198 | 321 |
else |
322 |
map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) |
|
49914 | 323 |
|
49883 | 324 |
|
52454 | 325 |
val add_labels_of_proof = |
326 |
steps_of_proof #> fold_isar_steps |
|
327 |
(byline_of_step #> (fn SOME (By_Metis (ls, _)) => union (op =) ls |
|
328 |
| _ => I)) |
|
49914 | 329 |
|
330 |
fun kill_useless_labels_in_proof proof = |
|
331 |
let |
|
51178 | 332 |
val used_ls = add_labels_of_proof proof [] |
49914 | 333 |
fun do_label l = if member (op =) used_ls l then l else no_label |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
334 |
fun do_assms (Assume assms) = Assume (map (apfst do_label) assms) |
52454 | 335 |
fun do_step (Prove (qs, xs, l, t, subproofs, by)) = |
336 |
Prove (qs, xs, do_label l, t, map do_proof subproofs, by) |
|
49914 | 337 |
| do_step step = step |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
338 |
and do_proof (Proof (fix, assms, steps)) = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
339 |
Proof (fix, do_assms assms, map do_step steps) |
51128
0021ea861129
introduced subblock in isar_step datatype for conjecture herbrandization
smolkas
parents:
51031
diff
changeset
|
340 |
in do_proof proof end |
49914 | 341 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51976
diff
changeset
|
342 |
fun prefix_of_depth n = replicate_string (n + 1) |
49914 | 343 |
|
344 |
val relabel_proof = |
|
345 |
let |
|
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
346 |
fun fresh_label depth prefix (old as (l, subst, next)) = |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
347 |
if l = no_label then |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
348 |
old |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
349 |
else |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51976
diff
changeset
|
350 |
let val l' = (prefix_of_depth depth prefix, next) in |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
351 |
(l', (l, l') :: subst, next + 1) |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
352 |
end |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
353 |
fun do_facts subst = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
354 |
apfst (maps (the_list o AList.lookup (op =) subst)) |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
355 |
fun do_assm depth (l, t) (subst, next) = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
356 |
let |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
357 |
val (l, subst, next) = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
358 |
(l, subst, next) |> fresh_label depth assume_prefix |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
359 |
in |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
360 |
((l, t), (subst, next)) |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
361 |
end |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
362 |
fun do_assms subst depth (Assume assms) = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
363 |
fold_map (do_assm depth) assms (subst, 1) |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
364 |
|> apfst Assume |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
365 |
|> apsnd fst |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
366 |
fun do_steps _ _ _ [] = [] |
52454 | 367 |
| do_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) = |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
368 |
let |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
369 |
val (l, subst, next) = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
370 |
(l, subst, next) |> fresh_label depth have_prefix |
52454 | 371 |
val sub = do_proofs subst depth sub |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
372 |
val by = by |> do_byline subst depth |
52454 | 373 |
in Prove (qs, xs, l, t, sub, by) :: do_steps subst depth next steps end |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
374 |
| do_steps subst depth next (step :: steps) = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
375 |
step :: do_steps subst depth next steps |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
376 |
and do_proof subst depth (Proof (fix, assms, steps)) = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
377 |
let val (assms, subst) = do_assms subst depth assms in |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
378 |
Proof (fix, assms, do_steps subst depth 1 steps) |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
379 |
end |
52454 | 380 |
and do_byline subst depth (By_Metis facts) = |
381 |
By_Metis (do_facts subst facts) |
|
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
382 |
and do_proofs subst depth = map (do_proof subst (depth + 1)) |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
383 |
in do_proof [] 0 end |
49914 | 384 |
|
50004
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset
|
385 |
val chain_direct_proof = |
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset
|
386 |
let |
51178 | 387 |
fun do_qs_lfs NONE lfs = ([], lfs) |
388 |
| do_qs_lfs (SOME l0) lfs = |
|
389 |
if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) |
|
390 |
else ([], lfs) |
|
52454 | 391 |
fun chain_step lbl (Prove (qs, xs, l, t, subproofs, By_Metis (lfs, gfs))) = |
52453 | 392 |
let val (qs', lfs) = do_qs_lfs lbl lfs in |
52454 | 393 |
Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, |
394 |
By_Metis (lfs, gfs)) |
|
52453 | 395 |
end |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset
|
396 |
| chain_step _ step = step |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
397 |
and chain_steps _ [] = [] |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
398 |
| chain_steps (prev as SOME _) (i :: is) = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
399 |
chain_step prev i :: chain_steps (label_of_step i) is |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
400 |
| chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
401 |
and chain_proof (Proof (fix, Assume assms, steps)) = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
402 |
Proof (fix, Assume assms, |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
403 |
chain_steps (try (List.last #> fst) assms) steps) |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
404 |
and chain_proofs proofs = map (chain_proof) proofs |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
405 |
in chain_proof end |
49883 | 406 |
|
49914 | 407 |
type isar_params = |
51879 | 408 |
bool * bool * Time.time option * bool * real * string Symtab.table |
52150
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
409 |
* (string * stature) list vector * (string * term) list * int Symtab.table |
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
410 |
* string proof * thm |
49914 | 411 |
|
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset
|
412 |
fun isar_proof_text ctxt isar_proofs |
51879 | 413 |
(debug, verbose, preplay_timeout, preplay_trace, isar_compress, pool, |
52150
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
414 |
fact_names, lifted, sym_tab, atp_proof, goal) |
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset
|
415 |
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) = |
49883 | 416 |
let |
52196
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52150
diff
changeset
|
417 |
val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt |
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52150
diff
changeset
|
418 |
val (_, ctxt) = |
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52150
diff
changeset
|
419 |
params |
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52150
diff
changeset
|
420 |
|> map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) |
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52150
diff
changeset
|
421 |
|> (fn fixes => |
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52150
diff
changeset
|
422 |
ctxt |> Variable.set_body false |
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52150
diff
changeset
|
423 |
|> Proof_Context.add_fixes fixes) |
49883 | 424 |
val one_line_proof = one_line_proof_text 0 one_line_params |
425 |
val type_enc = |
|
426 |
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN |
|
427 |
else partial_typesN |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
428 |
val lam_trans = lam_trans_of_atp_proof atp_proof metis_default_lam_trans |
50557 | 429 |
val preplay = preplay_timeout <> SOME Time.zeroTime |
49883 | 430 |
|
431 |
fun isar_proof_of () = |
|
432 |
let |
|
433 |
val atp_proof = |
|
434 |
atp_proof |
|
435 |
|> clean_up_atp_proof_dependencies |
|
436 |
|> nasty_atp_proof pool |
|
437 |
|> map_term_names_in_atp_proof repair_name |
|
52150
41c885784e04
handle lambda-lifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset
|
438 |
|> map (decode_line ctxt lifted sym_tab) |
50905 | 439 |
|> repair_waldmeister_endgame |
49883 | 440 |
|> rpair [] |-> fold_rev (add_line fact_names) |
441 |
|> rpair [] |-> fold_rev add_nontrivial_line |
|
442 |
|> rpair (0, []) |
|
52125
ac7830871177
improved handling of free variables' types in Isar proofs
blanchet
parents:
52077
diff
changeset
|
443 |
|-> fold_rev (add_desired_line fact_names) |
49883 | 444 |
|> snd |
445 |
val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts) |
|
446 |
val conjs = |
|
50010
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset
|
447 |
atp_proof |> map_filter |
51201 | 448 |
(fn (name as (_, ss), _, _, _, []) => |
50010
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset
|
449 |
if member (op =) ss conj_name then SOME name else NONE |
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset
|
450 |
| _ => NONE) |
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset
|
451 |
val assms = |
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset
|
452 |
atp_proof |> map_filter |
51201 | 453 |
(fn (name as (_, ss), _, _, _, []) => |
50013
cceec179bdca
use original formulas for hypotheses and conclusion to avoid mismatches
blanchet
parents:
50012
diff
changeset
|
454 |
(case resolve_conjecture ss of |
cceec179bdca
use original formulas for hypotheses and conclusion to avoid mismatches
blanchet
parents:
50012
diff
changeset
|
455 |
[j] => |
cceec179bdca
use original formulas for hypotheses and conclusion to avoid mismatches
blanchet
parents:
50012
diff
changeset
|
456 |
if j = length hyp_ts then NONE |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51976
diff
changeset
|
457 |
else SOME (raw_label_of_name name, nth hyp_ts j) |
50013
cceec179bdca
use original formulas for hypotheses and conclusion to avoid mismatches
blanchet
parents:
50012
diff
changeset
|
458 |
| _ => NONE) |
50010
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset
|
459 |
| _ => NONE) |
51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
460 |
val bot = atp_proof |> List.last |> #1 |
51145 | 461 |
val refute_graph = |
51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
462 |
atp_proof |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
463 |
|> map (fn (name, _, _, _, from) => (from, name)) |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
464 |
|> make_refute_graph bot |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
465 |
|> fold (Atom_Graph.default_node o rpair ()) conjs |
51145 | 466 |
val axioms = axioms_of_refute_graph refute_graph conjs |
467 |
val tainted = tainted_atoms_of_refute_graph refute_graph conjs |
|
51156 | 468 |
val is_clause_tainted = exists (member (op =) tainted) |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
469 |
val steps = |
49883 | 470 |
Symtab.empty |
51201 | 471 |
|> fold (fn (name as (s, _), role, t, rule, _) => |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
472 |
Symtab.update_new (s, (rule, |
51156 | 473 |
t |> (if is_clause_tainted [name] then |
50905 | 474 |
s_maybe_not role |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
475 |
#> fold exists_of (map Var (Term.add_vars t [])) |
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
476 |
else |
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
477 |
I)))) |
49883 | 478 |
atp_proof |
51148
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
479 |
fun is_clause_skolemize_rule [(s, _)] = |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
480 |
Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) = |
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
481 |
SOME true |
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
482 |
| is_clause_skolemize_rule _ = false |
50670
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset
|
483 |
(* The assumptions and conjecture are "prop"s; the other formulas are |
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset
|
484 |
"bool"s. *) |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
485 |
fun prop_of_clause [(s, ss)] = |
50016 | 486 |
(case resolve_conjecture ss of |
487 |
[j] => if j = length hyp_ts then concl_t else nth hyp_ts j |
|
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
488 |
| _ => the_default ("", @{term False}) (Symtab.lookup steps s) |
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
489 |
|> snd |> HOLogic.mk_Trueprop |> close_form) |
50016 | 490 |
| prop_of_clause names = |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
491 |
let |
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
492 |
val lits = map snd (map_filter (Symtab.lookup steps o fst) names) |
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
493 |
in |
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset
|
494 |
case List.partition (can HOLogic.dest_not) lits of |
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset
|
495 |
(negs as _ :: _, pos as _ :: _) => |
51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
496 |
s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
497 |
Library.foldr1 s_disj pos) |
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset
|
498 |
| _ => fold (curry s_disj) lits @{term False} |
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset
|
499 |
end |
50016 | 500 |
|> HOLogic.mk_Trueprop |> close_form |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
501 |
fun isar_proof_of_direct_proof infs = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
502 |
let |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
503 |
fun maybe_show outer c = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
504 |
(outer andalso length c = 1 andalso subset (op =) (c, conjs)) |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
505 |
? cons Show |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
506 |
val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
507 |
fun skolems_of t = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
508 |
Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev |
51976
e5303bd748f2
generate valid direct Isar proof also if the facts are contradictory
blanchet
parents:
51879
diff
changeset
|
509 |
fun do_steps outer predecessor accum [] = |
e5303bd748f2
generate valid direct Isar proof also if the facts are contradictory
blanchet
parents:
51879
diff
changeset
|
510 |
accum |
e5303bd748f2
generate valid direct Isar proof also if the facts are contradictory
blanchet
parents:
51879
diff
changeset
|
511 |
|> (if tainted = [] then |
52453 | 512 |
cons (Prove (if outer then [Show] else [], |
52454 | 513 |
Fix [], no_label, concl_t, [], |
514 |
By_Metis ([the predecessor], []))) |
|
51976
e5303bd748f2
generate valid direct Isar proof also if the facts are contradictory
blanchet
parents:
51879
diff
changeset
|
515 |
else |
e5303bd748f2
generate valid direct Isar proof also if the facts are contradictory
blanchet
parents:
51879
diff
changeset
|
516 |
I) |
e5303bd748f2
generate valid direct Isar proof also if the facts are contradictory
blanchet
parents:
51879
diff
changeset
|
517 |
|> rev |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
518 |
| do_steps outer _ accum (Have (gamma, c) :: infs) = |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
519 |
let |
51148
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
520 |
val l = label_of_clause c |
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
521 |
val t = prop_of_clause c |
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
522 |
val by = |
52454 | 523 |
By_Metis |
524 |
(fold (add_fact_of_dependencies fact_names) gamma no_facts) |
|
525 |
fun prove sub by = |
|
526 |
Prove (maybe_show outer c [], Fix [], l, t, sub, by) |
|
51976
e5303bd748f2
generate valid direct Isar proof also if the facts are contradictory
blanchet
parents:
51879
diff
changeset
|
527 |
fun do_rest l step = |
e5303bd748f2
generate valid direct Isar proof also if the facts are contradictory
blanchet
parents:
51879
diff
changeset
|
528 |
do_steps outer (SOME l) (step :: accum) infs |
51148
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
529 |
in |
51156 | 530 |
if is_clause_tainted c then |
51149 | 531 |
case gamma of |
532 |
[g] => |
|
51156 | 533 |
if is_clause_skolemize_rule g andalso |
534 |
is_clause_tainted g then |
|
51149 | 535 |
let |
51178 | 536 |
val subproof = |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
537 |
Proof (Fix (skolems_of (prop_of_clause g)), |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
538 |
Assume [], rev accum) |
51149 | 539 |
in |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
540 |
do_steps outer (SOME l) |
52454 | 541 |
[prove [subproof] (By_Metis no_facts)] [] |
51149 | 542 |
end |
543 |
else |
|
52454 | 544 |
do_rest l (prove [] by) |
545 |
| _ => do_rest l (prove [] by) |
|
51148
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
546 |
else |
51149 | 547 |
if is_clause_skolemize_rule c then |
52454 | 548 |
do_rest l (Prove ([], Fix (skolems_of t), l, t, [], by)) |
51149 | 549 |
else |
52454 | 550 |
do_rest l (prove [] by) |
51148
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
551 |
end |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
552 |
| do_steps outer predecessor accum (Cases cases :: infs) = |
51148
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
553 |
let |
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
554 |
fun do_case (c, infs) = |
51976
e5303bd748f2
generate valid direct Isar proof also if the facts are contradictory
blanchet
parents:
51879
diff
changeset
|
555 |
do_proof false [] [(label_of_clause c, prop_of_clause c)] |
e5303bd748f2
generate valid direct Isar proof also if the facts are contradictory
blanchet
parents:
51879
diff
changeset
|
556 |
infs |
51148
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
557 |
val c = succedent_of_cases cases |
51178 | 558 |
val l = label_of_clause c |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
559 |
val t = prop_of_clause c |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
560 |
val step = |
52453 | 561 |
Prove (maybe_show outer c [], Fix [], l, t, |
52454 | 562 |
map do_case cases, By_Metis (the_list predecessor, [])) |
51149 | 563 |
in |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
564 |
do_steps outer (SOME l) (step :: accum) infs |
51149 | 565 |
end |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
566 |
and do_proof outer fix assms infs = |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
567 |
Proof (Fix fix, Assume assms, do_steps outer NONE [] infs) |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
568 |
in |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
569 |
do_proof true params assms infs |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
570 |
end |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
571 |
|
51741 | 572 |
val clean_up_labels_in_proof = |
51165 | 573 |
chain_direct_proof |
574 |
#> kill_useless_labels_in_proof |
|
575 |
#> relabel_proof |
|
50924 | 576 |
val (isar_proof, (preplay_fail, preplay_time)) = |
51145 | 577 |
refute_graph |
51031
63d71b247323
more robustness in Isar proof reconstruction (cf. bug report by Ondrej)
blanchet
parents:
51026
diff
changeset
|
578 |
|> redirect_graph axioms tainted bot |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
579 |
|> isar_proof_of_direct_proof |
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
51129
diff
changeset
|
580 |
|> (if not preplay andalso isar_compress <= 1.0 then |
50677 | 581 |
rpair (false, (true, seconds 0.0)) |
50557 | 582 |
else |
51741 | 583 |
compress_and_preplay_proof debug ctxt type_enc lam_trans preplay |
51879 | 584 |
preplay_timeout preplay_trace |
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
585 |
(if isar_proofs = SOME true then isar_compress else 1000.0)) |
51741 | 586 |
|>> clean_up_labels_in_proof |
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset
|
587 |
val isar_text = |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51976
diff
changeset
|
588 |
string_of_proof ctxt type_enc lam_trans subgoal subgoal_count |
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51976
diff
changeset
|
589 |
isar_proof |
49883 | 590 |
in |
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset
|
591 |
case isar_text of |
49883 | 592 |
"" => |
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
593 |
if isar_proofs = SOME true then |
50671 | 594 |
"\nNo structured proof available (proof too simple)." |
49883 | 595 |
else |
596 |
"" |
|
597 |
| _ => |
|
50670
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset
|
598 |
let |
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset
|
599 |
val msg = |
51203 | 600 |
(if verbose then |
601 |
let |
|
602 |
val num_steps = add_metis_steps (steps_of_proof isar_proof) 0 |
|
603 |
in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end |
|
604 |
else |
|
605 |
[]) @ |
|
50670
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset
|
606 |
(if preplay then |
50924 | 607 |
[(if preplay_fail then "may fail, " else "") ^ |
608 |
Sledgehammer_Preplay.string_of_preplay_time preplay_time] |
|
50670
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset
|
609 |
else |
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset
|
610 |
[]) |
50277 | 611 |
in |
51741 | 612 |
"\n\nStructured proof" |
613 |
^ (commas msg |> not (null msg) ? enclose " (" ")") |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50410
diff
changeset
|
614 |
^ ":\n" ^ Active.sendback_markup isar_text |
50277 | 615 |
end |
49883 | 616 |
end |
617 |
val isar_proof = |
|
618 |
if debug then |
|
619 |
isar_proof_of () |
|
620 |
else case try isar_proof_of () of |
|
621 |
SOME s => s |
|
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
622 |
| NONE => if isar_proofs = SOME true then |
49883 | 623 |
"\nWarning: The Isar proof construction failed." |
624 |
else |
|
625 |
"" |
|
626 |
in one_line_proof ^ isar_proof end |
|
627 |
||
51187
c344cf148e8f
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
blanchet
parents:
51179
diff
changeset
|
628 |
fun isar_proof_would_be_a_good_idea preplay = |
c344cf148e8f
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
blanchet
parents:
51179
diff
changeset
|
629 |
case preplay of |
c344cf148e8f
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
blanchet
parents:
51179
diff
changeset
|
630 |
Played (reconstr, _) => reconstr = SMT |
51215
9ee38fc0bc81
generate Isar proof if Metis appears to be too slow
blanchet
parents:
51212
diff
changeset
|
631 |
| Trust_Playable _ => true |
51187
c344cf148e8f
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
blanchet
parents:
51179
diff
changeset
|
632 |
| Failed_to_Play _ => true |
c344cf148e8f
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
blanchet
parents:
51179
diff
changeset
|
633 |
|
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset
|
634 |
fun proof_text ctxt isar_proofs isar_params num_chained |
49883 | 635 |
(one_line_params as (preplay, _, _, _, _, _)) = |
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
636 |
(if isar_proofs = SOME true orelse |
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
637 |
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then |
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset
|
638 |
isar_proof_text ctxt isar_proofs isar_params |
49883 | 639 |
else |
640 |
one_line_proof_text num_chained) one_line_params |
|
641 |
||
642 |
end; |