author | blanchet |
Tue, 01 Feb 2022 17:33:12 +0100 | |
changeset 75057 | 79b4e711d6a2 |
parent 72585 | 18eb7ec2720f |
child 77919 | 8734ca279e59 |
permissions | -rw-r--r-- |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML |
50263 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Author: Steffen Juilf Smolka, TU Muenchen |
|
4 |
||
5 |
Basic data structures for representing and basic methods |
|
6 |
for dealing with Isar proof texts. |
|
7 |
*) |
|
8 |
||
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
9 |
signature SLEDGEHAMMER_ISAR_PROOF = |
50259 | 10 |
sig |
55287 | 11 |
type proof_method = Sledgehammer_Proof_Methods.proof_method |
55285 | 12 |
|
51239 | 13 |
type label = string * int |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54767
diff
changeset
|
14 |
type facts = label list * string list (* local and global facts *) |
50268 | 15 |
|
51178 | 16 |
datatype isar_qualifier = Show | Then |
50268 | 17 |
|
52454 | 18 |
datatype isar_proof = |
72582 | 19 |
Proof of { |
20 |
fixes : (string * typ) list, |
|
21 |
assumptions: (label * term) list, |
|
22 |
steps : isar_step list |
|
23 |
} |
|
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
|
24 |
and isar_step = |
72584 | 25 |
Let of { |
26 |
lhs : term, |
|
27 |
rhs : term |
|
28 |
} | |
|
29 |
Prove of { |
|
30 |
qualifiers : isar_qualifier list, |
|
31 |
obtains : (string * typ) list, |
|
32 |
label : label, |
|
33 |
goal : term, |
|
34 |
subproofs : isar_proof list, |
|
35 |
facts : facts, |
|
36 |
proof_methods : proof_method list, |
|
37 |
comment : string |
|
38 |
} |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
39 |
|
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
|
40 |
val no_label : label |
50268 | 41 |
|
70586 | 42 |
val label_ord : label ord |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51239
diff
changeset
|
43 |
val string_of_label : label -> string |
57776
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
44 |
val sort_facts : facts -> facts |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
45 |
|
55260 | 46 |
val steps_of_isar_proof : isar_proof -> isar_step list |
72583 | 47 |
val isar_proof_with_steps : isar_proof -> isar_step list -> isar_proof |
72584 | 48 |
|
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
49 |
val label_of_isar_step : isar_step -> label option |
55279 | 50 |
val facts_of_isar_step : isar_step -> facts |
51 |
val proof_methods_of_isar_step : isar_step -> proof_method list |
|
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
|
52 |
|
54765 | 53 |
val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a |
55212 | 54 |
val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof |
55 |
val add_isar_steps : isar_step list -> int -> int |
|
52454 | 56 |
|
55212 | 57 |
structure Canonical_Label_Tab : TABLE |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
58 |
|
70586 | 59 |
val canonical_label_ord : label ord |
55220 | 60 |
|
55299 | 61 |
val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof |
55220 | 62 |
val chain_isar_proof : isar_proof -> isar_proof |
63 |
val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof |
|
55213 | 64 |
val relabel_isar_proof_canonically : isar_proof -> isar_proof |
55282 | 65 |
val relabel_isar_proof_nicely : isar_proof -> isar_proof |
57792 | 66 |
val rationalize_obtains_in_isar_proofs : Proof.context -> isar_proof -> isar_proof |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
67 |
|
55299 | 68 |
val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string |
54504 | 69 |
end; |
50259 | 70 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
71 |
structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF = |
50259 | 72 |
struct |
73 |
||
55211 | 74 |
open ATP_Util |
75 |
open ATP_Proof |
|
76 |
open ATP_Problem_Generate |
|
77 |
open ATP_Proof_Reconstruct |
|
78 |
open Sledgehammer_Util |
|
55287 | 79 |
open Sledgehammer_Proof_Methods |
55211 | 80 |
open Sledgehammer_Isar_Annotate |
81 |
||
50259 | 82 |
type label = string * int |
54534 | 83 |
type facts = label list * string list (* local and global facts *) |
50259 | 84 |
|
51178 | 85 |
datatype isar_qualifier = Show | Then |
50259 | 86 |
|
52454 | 87 |
datatype isar_proof = |
72582 | 88 |
Proof of { |
89 |
fixes : (string * typ) list, |
|
90 |
assumptions: (label * term) list, |
|
91 |
steps : isar_step list |
|
92 |
} |
|
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
|
93 |
and isar_step = |
72584 | 94 |
Let of { |
95 |
lhs : term, |
|
96 |
rhs : term |
|
97 |
} | |
|
98 |
Prove of { |
|
99 |
qualifiers : isar_qualifier list, |
|
100 |
obtains : (string * typ) list, |
|
101 |
label : label, |
|
102 |
goal : term, |
|
103 |
subproofs : isar_proof list, |
|
104 |
facts : facts, |
|
105 |
proof_methods : proof_method list, |
|
106 |
comment : string |
|
107 |
} |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
108 |
|
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
|
109 |
val no_label = ("", ~1) |
50259 | 110 |
|
57776
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
111 |
(* cf. "label_ord" below *) |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
112 |
val assume_prefix = "a" |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
113 |
val have_prefix = "f" |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
114 |
|
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
115 |
fun label_ord ((s1, i1), (s2, i2)) = |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58928
diff
changeset
|
116 |
(case int_ord (apply2 String.size (s1, s2)) of |
57776
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
117 |
EQUAL => |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
118 |
(case string_ord (s1, s2) of |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
119 |
EQUAL => int_ord (i1, i2) |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
120 |
| ord => ord (* "assume" before "have" *)) |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
121 |
| ord => ord) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
122 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51239
diff
changeset
|
123 |
fun string_of_label (s, num) = s ^ string_of_int num |
50259 | 124 |
|
57776
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
125 |
(* Put the nearest local label first, since it's the most likely to be replaced by a "hence". |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
126 |
(Some preplaying proof methods, e.g. "blast", react poorly to fact reorderings.) *) |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
127 |
fun sort_facts (lfs, gfs) = (sort (label_ord o swap) lfs, sort string_ord gfs) |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
128 |
|
72582 | 129 |
fun steps_of_isar_proof (Proof {steps, ...}) = steps |
72583 | 130 |
fun isar_proof_with_steps (Proof {fixes, assumptions, ...}) steps = |
131 |
Proof {fixes = fixes, assumptions = assumptions, steps = steps} |
|
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
|
132 |
|
72584 | 133 |
fun label_of_isar_step (Prove {label, ...}) = SOME label |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
134 |
| label_of_isar_step _ = NONE |
51178 | 135 |
|
72584 | 136 |
fun subproofs_of_isar_step (Prove {subproofs, ...}) = subproofs |
55281 | 137 |
| subproofs_of_isar_step _ = [] |
52454 | 138 |
|
72584 | 139 |
fun facts_of_isar_step (Prove {facts, ...}) = facts |
55279 | 140 |
| facts_of_isar_step _ = ([], []) |
141 |
||
72584 | 142 |
fun proof_methods_of_isar_step (Prove {proof_methods, ...}) = proof_methods |
55279 | 143 |
| proof_methods_of_isar_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
|
144 |
|
55212 | 145 |
fun fold_isar_step f step = |
55281 | 146 |
fold (steps_of_isar_proof #> fold_isar_steps f) (subproofs_of_isar_step step) #> f step |
55212 | 147 |
and fold_isar_steps f = fold (fold_isar_step f) |
52454 | 148 |
|
54765 | 149 |
fun map_isar_steps f = |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
150 |
let |
72583 | 151 |
fun map_proof (proof as Proof {steps, ...}) = isar_proof_with_steps proof (map map_step steps) |
55212 | 152 |
and map_step (step as Let _) = f step |
72584 | 153 |
| map_step (Prove {qualifiers, obtains, label, goal, subproofs, facts, proof_methods, |
154 |
comment}) = |
|
155 |
f (Prove { |
|
156 |
qualifiers = qualifiers, |
|
157 |
obtains = obtains, |
|
158 |
label = label, |
|
159 |
goal = goal, |
|
160 |
subproofs = map map_proof subproofs, |
|
161 |
facts = facts, |
|
162 |
proof_methods = proof_methods, |
|
163 |
comment = comment}) |
|
55212 | 164 |
in map_proof end |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
165 |
|
55212 | 166 |
val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
167 |
|
55211 | 168 |
(* canonical proof labels: 1, 2, 3, ... in post traversal order *) |
52557 | 169 |
fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
170 |
|
55212 | 171 |
structure Canonical_Label_Tab = Table( |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
172 |
type key = label |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
173 |
val ord = canonical_label_ord) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
174 |
|
72584 | 175 |
fun comment_isar_step comment_of (Prove {qualifiers, obtains, label, goal, subproofs, facts, |
176 |
proof_methods, ...}) = |
|
177 |
Prove { |
|
178 |
qualifiers = qualifiers, |
|
179 |
obtains = obtains, |
|
180 |
label = label, |
|
181 |
goal = goal, |
|
182 |
subproofs = subproofs, |
|
183 |
facts = facts, |
|
184 |
proof_methods = proof_methods, |
|
185 |
comment = comment_of label proof_methods} |
|
55299 | 186 |
| comment_isar_step _ step = step |
187 |
fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of) |
|
188 |
||
55220 | 189 |
fun chain_qs_lfs NONE lfs = ([], lfs) |
190 |
| chain_qs_lfs (SOME l0) lfs = |
|
57655 | 191 |
if member (op =) lfs l0 then ([Then], remove (op =) l0 lfs) else ([], lfs) |
192 |
||
72584 | 193 |
fun chain_isar_step lbl (Prove {qualifiers, obtains, label, goal, subproofs, |
194 |
facts = (lfs, gfs), proof_methods, comment}) = |
|
55220 | 195 |
let val (qs', lfs) = chain_qs_lfs lbl lfs in |
72584 | 196 |
Prove { |
197 |
qualifiers = qs' @ qualifiers, |
|
198 |
obtains = obtains, |
|
199 |
label = label, |
|
200 |
goal = goal, |
|
201 |
subproofs = map chain_isar_proof subproofs, |
|
202 |
facts = (lfs, gfs), |
|
203 |
proof_methods = proof_methods, |
|
204 |
comment = comment} |
|
55220 | 205 |
end |
206 |
| chain_isar_step _ step = step |
|
207 |
and chain_isar_steps _ [] = [] |
|
57655 | 208 |
| chain_isar_steps prev (i :: is) = |
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
209 |
chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is |
72583 | 210 |
and chain_isar_proof (proof as Proof {assumptions, steps, ...}) = |
72585 | 211 |
isar_proof_with_steps proof (chain_isar_steps (try (List.last #> fst) assumptions) steps) |
55220 | 212 |
|
213 |
fun kill_useless_labels_in_isar_proof proof = |
|
214 |
let |
|
215 |
val used_ls = |
|
55279 | 216 |
fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) [] |
55220 | 217 |
|
218 |
fun kill_label l = if member (op =) used_ls l then l else no_label |
|
219 |
||
72584 | 220 |
fun kill_step (Prove {qualifiers, obtains, label, goal, subproofs, facts, proof_methods, |
221 |
comment}) = |
|
222 |
Prove { |
|
223 |
qualifiers = qualifiers, |
|
224 |
obtains = obtains, |
|
225 |
label = kill_label label, |
|
226 |
goal = goal, |
|
227 |
subproofs = map kill_proof subproofs, |
|
228 |
facts = facts, |
|
229 |
proof_methods = proof_methods, |
|
230 |
comment = comment} |
|
55220 | 231 |
| kill_step step = step |
72582 | 232 |
and kill_proof (Proof {fixes, assumptions, steps}) = |
233 |
let |
|
234 |
val assumptions' = map (apfst kill_label) assumptions |
|
235 |
val steps' = map kill_step steps |
|
236 |
in |
|
237 |
Proof {fixes = fixes, assumptions = assumptions', steps = steps'} |
|
238 |
end |
|
55220 | 239 |
in |
240 |
kill_proof proof |
|
241 |
end |
|
242 |
||
55213 | 243 |
fun relabel_isar_proof_canonically proof = |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
244 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
245 |
fun next_label l (next, subst) = |
54534 | 246 |
let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
247 |
|
72584 | 248 |
fun relabel_step (Prove {qualifiers, obtains, label, goal, subproofs, facts = (lfs, gfs), |
249 |
proof_methods, comment}) (accum as (_, subst)) = |
|
54534 | 250 |
let |
55281 | 251 |
val lfs' = maps (the_list o AList.lookup (op =) subst) lfs |
252 |
val ((subs', l'), accum') = accum |
|
72584 | 253 |
|> fold_map relabel_proof subproofs |
254 |
||>> next_label label |
|
255 |
val prove = Prove { |
|
256 |
qualifiers = qualifiers, |
|
257 |
obtains = obtains, |
|
258 |
label = l', |
|
259 |
goal = goal, |
|
260 |
subproofs = subs', |
|
261 |
facts = (lfs', gfs), |
|
262 |
proof_methods = proof_methods, |
|
263 |
comment = comment} |
|
54534 | 264 |
in |
72584 | 265 |
(prove, accum') |
54534 | 266 |
end |
55281 | 267 |
| relabel_step step accum = (step, accum) |
72582 | 268 |
and relabel_proof (Proof {fixes, assumptions, steps}) = |
269 |
fold_map (fn (l, t) => next_label l #> apfst (rpair t)) assumptions |
|
55281 | 270 |
##>> fold_map relabel_step steps |
72582 | 271 |
#>> (fn (assumptions', steps') => |
272 |
Proof {fixes = fixes, assumptions = assumptions', steps = steps'}) |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
273 |
in |
55279 | 274 |
fst (relabel_proof proof (0, [])) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
275 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
276 |
|
55282 | 277 |
val relabel_isar_proof_nicely = |
55220 | 278 |
let |
55281 | 279 |
fun next_label depth prefix l (accum as (next, subst)) = |
55220 | 280 |
if l = no_label then |
55281 | 281 |
(l, accum) |
55220 | 282 |
else |
283 |
let val l' = (replicate_string (depth + 1) prefix, next) in |
|
55281 | 284 |
(l', (next + 1, (l, l') :: subst)) |
55220 | 285 |
end |
286 |
||
72584 | 287 |
fun relabel_step depth (Prove {qualifiers, obtains, label, goal, |
288 |
subproofs, facts = (lfs, gfs), proof_methods, comment}) (accum as (_, subst)) = |
|
55220 | 289 |
let |
72584 | 290 |
val (l', accum' as (_, subst')) = next_label depth have_prefix label accum |
291 |
val prove = Prove { |
|
292 |
qualifiers = qualifiers, |
|
293 |
obtains = obtains, |
|
294 |
label = l', |
|
295 |
goal = goal, |
|
296 |
subproofs = map (relabel_proof subst' (depth + 1)) subproofs, |
|
297 |
facts = (maps (the_list o AList.lookup (op =) subst) lfs, gfs), |
|
298 |
proof_methods = proof_methods, |
|
299 |
comment = comment} |
|
55220 | 300 |
in |
72584 | 301 |
(prove, accum') |
55220 | 302 |
end |
55281 | 303 |
| relabel_step _ step accum = (step, accum) |
72582 | 304 |
and relabel_proof subst depth (Proof {fixes, assumptions, steps}) = |
55281 | 305 |
(1, subst) |
72582 | 306 |
|> fold_map (fn (l, t) => next_label depth assume_prefix l #> apfst (rpair t)) assumptions |
55281 | 307 |
||>> fold_map (relabel_step depth) steps |
72582 | 308 |
|> (fn ((assumptions', steps'), _) => |
309 |
Proof {fixes = fixes, assumptions = assumptions', steps = steps'}) |
|
55220 | 310 |
in |
311 |
relabel_proof [] 0 |
|
312 |
end |
|
313 |
||
57793 | 314 |
fun stutter_single_letter s = String.extract (s, 0, SOME 1) ^ s |
315 |
||
57792 | 316 |
fun rationalize_obtains_in_isar_proofs ctxt = |
317 |
let |
|
318 |
fun rename_obtains xs (subst, ctxt) = |
|
319 |
let |
|
320 |
val Ts = map snd xs |
|
57793 | 321 |
val new_names0 = map (stutter_single_letter o var_name_of_typ o body_type) Ts |
57792 | 322 |
val (new_names, ctxt') = Variable.variant_fixes new_names0 ctxt |
323 |
val ys = map2 pair new_names Ts |
|
324 |
in |
|
325 |
(ys, ((map Free xs ~~ map Free ys) @ subst, ctxt')) |
|
326 |
end |
|
327 |
||
72584 | 328 |
fun rationalize_step (Prove {qualifiers, obtains, label, goal, subproofs, facts, proof_methods, |
329 |
comment}) subst_ctxt = |
|
57792 | 330 |
let |
72584 | 331 |
val (obtains', subst_ctxt' as (subst', _)) = rename_obtains obtains subst_ctxt |
332 |
val prove = Prove { |
|
333 |
qualifiers = qualifiers, |
|
334 |
obtains = obtains', |
|
335 |
label = label, |
|
336 |
goal = subst_atomic subst' goal, |
|
337 |
subproofs = map (rationalize_proof false subst_ctxt') subproofs, |
|
338 |
facts = facts, |
|
339 |
proof_methods = proof_methods, |
|
340 |
comment = comment} |
|
57792 | 341 |
in |
72584 | 342 |
(prove, subst_ctxt') |
57792 | 343 |
end |
72582 | 344 |
and rationalize_proof outer (subst_ctxt as (subst, ctxt)) (Proof {fixes, assumptions, steps}) = |
58475
4508b6bff671
rename skolem symbols in the negative case as well
blanchet
parents:
58087
diff
changeset
|
345 |
let |
72582 | 346 |
val (fixes', subst_ctxt' as (subst', _)) = |
58476
6ade4c7109a8
make sure no '__' suffixes make it until Isar proof
blanchet
parents:
58475
diff
changeset
|
347 |
if outer then |
6ade4c7109a8
make sure no '__' suffixes make it until Isar proof
blanchet
parents:
58475
diff
changeset
|
348 |
(* last call: eliminate any remaining skolem names (from SMT proofs) *) |
72582 | 349 |
(fixes, (subst @ map (fn x => (Free (apfst Name.skolem x), Free x)) fixes, ctxt)) |
58476
6ade4c7109a8
make sure no '__' suffixes make it until Isar proof
blanchet
parents:
58475
diff
changeset
|
350 |
else |
72582 | 351 |
rename_obtains fixes subst_ctxt |
352 |
val assumptions' = map (apsnd (subst_atomic subst')) assumptions |
|
353 |
val steps' = fst (fold_map rationalize_step steps subst_ctxt') |
|
58475
4508b6bff671
rename skolem symbols in the negative case as well
blanchet
parents:
58087
diff
changeset
|
354 |
in |
75057
79b4e711d6a2
robustly handle empty proof blocks in Isar proof output
blanchet
parents:
72585
diff
changeset
|
355 |
Proof {fixes = fixes', assumptions = assumptions', steps = steps'} |
58475
4508b6bff671
rename skolem symbols in the negative case as well
blanchet
parents:
58087
diff
changeset
|
356 |
end |
57792 | 357 |
in |
58475
4508b6bff671
rename skolem symbols in the negative case as well
blanchet
parents:
58087
diff
changeset
|
358 |
rationalize_proof true ([], ctxt) |
57792 | 359 |
end |
360 |
||
58087
32d3fa94ebb4
use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
blanchet
parents:
58082
diff
changeset
|
361 |
val thesis_var = ((Auto_Bind.thesisN, 0), HOLogic.boolT) |
32d3fa94ebb4
use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
blanchet
parents:
58082
diff
changeset
|
362 |
|
32d3fa94ebb4
use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
blanchet
parents:
58082
diff
changeset
|
363 |
fun is_thesis ctxt t = |
32d3fa94ebb4
use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
blanchet
parents:
58082
diff
changeset
|
364 |
(case Vartab.lookup (Variable.binds_of ctxt) (fst thesis_var) of |
32d3fa94ebb4
use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
blanchet
parents:
58082
diff
changeset
|
365 |
SOME (_, t') => HOLogic.mk_Trueprop t' aconv t |
32d3fa94ebb4
use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
blanchet
parents:
58082
diff
changeset
|
366 |
| NONE => false) |
32d3fa94ebb4
use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
blanchet
parents:
58082
diff
changeset
|
367 |
|
55211 | 368 |
val indent_size = 2 |
369 |
||
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
370 |
fun string_of_isar_proof ctxt0 i n proof = |
55211 | 371 |
let |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58476
diff
changeset
|
372 |
val keywords = Thy_Header.get_keywords' ctxt0 |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58476
diff
changeset
|
373 |
|
55211 | 374 |
(* Make sure only type constraints inserted by the type annotation code are printed. *) |
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
375 |
val ctxt = ctxt0 |
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
376 |
|> Config.put show_markup false |
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
377 |
|> Config.put Printer.show_type_emphasis false |
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
378 |
|> Config.put show_types false |
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
379 |
|> Config.put show_sorts false |
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
380 |
|> Config.put show_consts false |
55211 | 381 |
|
55216 | 382 |
fun add_str s' = apfst (suffix s') |
55211 | 383 |
|
384 |
fun of_indent ind = replicate_string (ind * indent_size) " " |
|
385 |
fun of_moreover ind = of_indent ind ^ "moreover\n" |
|
386 |
fun of_label l = if l = no_label then "" else string_of_label l ^ ": " |
|
387 |
||
388 |
fun of_obtain qs nr = |
|
67405
e9ab4ad7bd15
uniform use of Standard ML op-infix -- eliminated warnings;
wenzelm
parents:
67399
diff
changeset
|
389 |
(if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " |
e9ab4ad7bd15
uniform use of Standard ML op-infix -- eliminated warnings;
wenzelm
parents:
67399
diff
changeset
|
390 |
else if nr = 1 orelse member (op =) qs Then then "then " |
55211 | 391 |
else "") ^ "obtain" |
392 |
||
67405
e9ab4ad7bd15
uniform use of Standard ML op-infix -- eliminated warnings;
wenzelm
parents:
67399
diff
changeset
|
393 |
fun of_show_have qs = if member (op =) qs Show then "show" else "have" |
e9ab4ad7bd15
uniform use of Standard ML op-infix -- eliminated warnings;
wenzelm
parents:
67399
diff
changeset
|
394 |
fun of_thus_hence qs = if member (op =) qs Show then "then show" else "then have" |
55211 | 395 |
|
396 |
fun of_have qs nr = |
|
67405
e9ab4ad7bd15
uniform use of Standard ML op-infix -- eliminated warnings;
wenzelm
parents:
67399
diff
changeset
|
397 |
if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs |
55211 | 398 |
else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs |
399 |
else of_show_have qs |
|
400 |
||
401 |
fun add_term term (s, ctxt) = |
|
402 |
(s ^ (term |
|
403 |
|> singleton (Syntax.uncheck_terms ctxt) |
|
55213 | 404 |
|> annotate_types_in_term ctxt |
66020 | 405 |
|> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of) |
55211 | 406 |
|> simplify_spaces |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58476
diff
changeset
|
407 |
|> maybe_quote keywords), |
70308 | 408 |
ctxt |> perhaps (try (Proof_Context.augment term))) |
55211 | 409 |
|
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56081
diff
changeset
|
410 |
fun using_facts [] [] = "" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56081
diff
changeset
|
411 |
| using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss)) |
55257 | 412 |
|
55211 | 413 |
(* Local facts are always passed via "using", which affects "meson" and "metis". This is |
414 |
arguably stylistically superior, because it emphasises the structure of the proof. It is also |
|
61756 | 415 |
more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "then" |
416 |
is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *) |
|
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
417 |
fun of_method ls ss meth = |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
418 |
let val direct = is_proof_method_direct meth in |
55281 | 419 |
using_facts ls (if direct then [] else ss) ^ |
72401
2783779b7dd3
removed obsolete unmaintained experimental prover Pirate
blanchet
parents:
70586
diff
changeset
|
420 |
"by " ^ string_of_proof_method (if direct then ss else []) meth |
55281 | 421 |
end |
55211 | 422 |
|
423 |
fun of_free (s, T) = |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58476
diff
changeset
|
424 |
maybe_quote keywords s ^ " :: " ^ |
66020 | 425 |
maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T)) |
55211 | 426 |
|
427 |
fun add_frees xs (s, ctxt) = |
|
70308 | 428 |
(s ^ space_implode " and " (map of_free xs), ctxt |> fold Proof_Context.augment (map Free xs)) |
55211 | 429 |
|
430 |
fun add_fix _ [] = I |
|
55281 | 431 |
| add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n" |
55211 | 432 |
|
433 |
fun add_assm ind (l, t) = |
|
55281 | 434 |
add_str (of_indent ind ^ "assume " ^ of_label l) #> add_term t #> add_str "\n" |
55211 | 435 |
|
436 |
fun of_subproof ind ctxt proof = |
|
437 |
let |
|
438 |
val ind = ind + 1 |
|
439 |
val s = of_proof ind ctxt proof |
|
440 |
val prefix = "{ " |
|
441 |
val suffix = " }" |
|
442 |
in |
|
443 |
replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ |
|
75057
79b4e711d6a2
robustly handle empty proof blocks in Isar proof output
blanchet
parents:
72585
diff
changeset
|
444 |
String.substring (s, ind * indent_size, size s - ind * indent_size - 1) ^ |
55211 | 445 |
suffix ^ "\n" |
446 |
end |
|
447 |
and of_subproofs _ _ _ [] = "" |
|
55281 | 448 |
| of_subproofs ind ctxt qs subs = |
67405
e9ab4ad7bd15
uniform use of Standard ML op-infix -- eliminated warnings;
wenzelm
parents:
67399
diff
changeset
|
449 |
(if member (op =) qs Then then of_moreover ind else "") ^ |
55281 | 450 |
space_implode (of_moreover ind) (map (of_subproof ind ctxt) subs) |
451 |
and add_step_pre ind qs subs (s, ctxt) = |
|
452 |
(s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt) |
|
72584 | 453 |
and add_step ind (Let {lhs = t1, rhs = t2}) = |
57776
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
454 |
add_str (of_indent ind ^ "let ") #> add_term t1 #> add_str " = " #> add_term t2 |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset
|
455 |
#> add_str "\n" |
72584 | 456 |
| add_step ind (Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, ss), |
457 |
proof_methods = meth :: _, comment}) = |
|
458 |
let val num_subproofs = length subproofs in |
|
459 |
add_step_pre ind qualifiers subproofs |
|
460 |
#> (case obtains of |
|
461 |
[] => add_str (of_have qualifiers num_subproofs ^ " ") |
|
462 |
| _ => |
|
463 |
add_str (of_obtain qualifiers num_subproofs ^ " ") |
|
464 |
#> add_frees obtains |
|
465 |
#> add_str (" where\n" ^ of_indent (ind + 1))) |
|
466 |
#> add_str (of_label label) |
|
467 |
#> add_term (if is_thesis ctxt goal then HOLogic.mk_Trueprop (Var thesis_var) else goal) |
|
468 |
#> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^ |
|
469 |
(if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n") |
|
470 |
end |
|
55211 | 471 |
and add_steps ind = fold (add_step ind) |
72582 | 472 |
and of_proof ind ctxt (Proof {fixes, assumptions, steps}) = |
55281 | 473 |
("", ctxt) |
72582 | 474 |
|> add_fix ind fixes |
475 |
|> fold (add_assm ind) assumptions |
|
55281 | 476 |
|> add_steps ind steps |
477 |
|> fst |
|
75057
79b4e711d6a2
robustly handle empty proof blocks in Isar proof output
blanchet
parents:
72585
diff
changeset
|
478 |
|> (fn s => if s = "" then of_indent ind ^ "\n" else s) (* robustness *) |
55211 | 479 |
in |
57286
4868ec62f533
don't generate Isar proof skeleton for what amounts to a one-line proof
blanchet
parents:
57154
diff
changeset
|
480 |
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
481 |
of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
482 |
of_indent 0 ^ (if n = 1 then "qed" else "next") |
55211 | 483 |
end |
484 |
||
54504 | 485 |
end; |