author  blanchet 
Thu, 28 Aug 2014 00:40:37 +0200  
changeset 58054  1d9edd486479 
parent 57793  d1cf76cef93b 
child 58071  62ec5b1d2f2f 
permissions  rwrr 
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 = 
54700  19 
Proof of (string * typ) list * (label * term) list * isar_step 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

20 
and isar_step = 
50268  21 
Let of term * term  
55280  22 
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list 
55299  23 
* facts * proof_method list * string 
52592
8a25b17e3d79
optimize isarproofs by trying different proof methods
smolkas
parents:
52590
diff
changeset

24 

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

25 
val no_label : label 
50268  26 

52592
8a25b17e3d79
optimize isarproofs by trying different proof methods
smolkas
parents:
52590
diff
changeset

27 
val label_ord : label * label > order 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51239
diff
changeset

28 
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

29 
val sort_facts : facts > facts 
52592
8a25b17e3d79
optimize isarproofs by trying different proof methods
smolkas
parents:
52590
diff
changeset

30 

55260  31 
val steps_of_isar_proof : isar_proof > isar_step list 
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset

32 
val label_of_isar_step : isar_step > label option 
55279  33 
val facts_of_isar_step : isar_step > facts 
34 
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

35 

54765  36 
val fold_isar_steps : (isar_step > 'a > 'a) > isar_step list > 'a > 'a 
55212  37 
val map_isar_steps : (isar_step > isar_step) > isar_proof > isar_proof 
38 
val add_isar_steps : isar_step list > int > int 

52454  39 

55212  40 
structure Canonical_Label_Tab : TABLE 
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset

41 

c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset

42 
val canonical_label_ord : (label * label) > order 
55220  43 

55299  44 
val comment_isar_proof : (label > proof_method list > string) > isar_proof > isar_proof 
55220  45 
val chain_isar_proof : isar_proof > isar_proof 
46 
val kill_useless_labels_in_isar_proof : isar_proof > isar_proof 

55213  47 
val relabel_isar_proof_canonically : isar_proof > isar_proof 
55282  48 
val relabel_isar_proof_nicely : isar_proof > isar_proof 
57792  49 
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

50 

55299  51 
val string_of_isar_proof : Proof.context > int > int > isar_proof > string 
54504  52 
end; 
50259  53 

55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

54 
structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF = 
50259  55 
struct 
56 

55211  57 
open ATP_Util 
58 
open ATP_Proof 

59 
open ATP_Problem_Generate 

60 
open ATP_Proof_Reconstruct 

61 
open Sledgehammer_Util 

55287  62 
open Sledgehammer_Proof_Methods 
55211  63 
open Sledgehammer_Isar_Annotate 
64 

50259  65 
type label = string * int 
54534  66 
type facts = label list * string list (* local and global facts *) 
50259  67 

51178  68 
datatype isar_qualifier = Show  Then 
50259  69 

52454  70 
datatype isar_proof = 
54700  71 
Proof of (string * typ) list * (label * term) list * isar_step 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

72 
and isar_step = 
50259  73 
Let of term * term  
55280  74 
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list 
55299  75 
* facts * proof_method list * string 
52592
8a25b17e3d79
optimize isarproofs by trying different proof methods
smolkas
parents:
52590
diff
changeset

76 

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

77 
val no_label = ("", ~1) 
50259  78 

57776
1111a9a328fe
rationalized sorting of facts  so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset

79 
(* 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

80 
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

81 
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

82 

1111a9a328fe
rationalized sorting of facts  so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset

83 
fun label_ord ((s1, i1), (s2, i2)) = 
1111a9a328fe
rationalized sorting of facts  so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset

84 
(case int_ord (pairself String.size (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

85 
EQUAL => 
1111a9a328fe
rationalized sorting of facts  so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset

86 
(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

87 
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

88 
 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

89 
 ord => ord) 
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset

90 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51239
diff
changeset

91 
fun string_of_label (s, num) = s ^ string_of_int num 
50259  92 

57776
1111a9a328fe
rationalized sorting of facts  so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset

93 
(* 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

94 
(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

95 
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

96 

55260  97 
fun steps_of_isar_proof (Proof (_, _, 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

98 

55299  99 
fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l 
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset

100 
 label_of_isar_step _ = NONE 
51178  101 

55299  102 
fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs 
55281  103 
 subproofs_of_isar_step _ = [] 
52454  104 

55299  105 
fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts 
55279  106 
 facts_of_isar_step _ = ([], []) 
107 

55299  108 
fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths 
55279  109 
 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

110 

55212  111 
fun fold_isar_step f step = 
55281  112 
fold (steps_of_isar_proof #> fold_isar_steps f) (subproofs_of_isar_step step) #> f step 
55212  113 
and fold_isar_steps f = fold (fold_isar_step f) 
52454  114 

54765  115 
fun map_isar_steps f = 
52592
8a25b17e3d79
optimize isarproofs by trying different proof methods
smolkas
parents:
52590
diff
changeset

116 
let 
55212  117 
fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps) 
118 
and map_step (step as Let _) = f step 

55299  119 
 map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) = 
120 
f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment)) 

55212  121 
in map_proof end 
52592
8a25b17e3d79
optimize isarproofs by trying different proof methods
smolkas
parents:
52590
diff
changeset

122 

55212  123 
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

124 

55211  125 
(* canonical proof labels: 1, 2, 3, ... in post traversal order *) 
52557  126 
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

127 

55212  128 
structure Canonical_Label_Tab = Table( 
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset

129 
type key = label 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset

130 
val ord = canonical_label_ord) 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset

131 

55299  132 
fun comment_isar_step comment_of (Prove (qs, xs, l, t, subs, facts, meths, _)) = 
133 
Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths) 

134 
 comment_isar_step _ step = step 

135 
fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of) 

136 

55220  137 
fun chain_qs_lfs NONE lfs = ([], lfs) 
138 
 chain_qs_lfs (SOME l0) lfs = 

57655  139 
if member (op =) lfs l0 then ([Then], remove (op =) l0 lfs) else ([], lfs) 
140 

57286
4868ec62f533
don't generate Isar proof skeleton for what amounts to a oneline proof
blanchet
parents:
57154
diff
changeset

141 
fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) = 
55220  142 
let val (qs', lfs) = chain_qs_lfs lbl lfs in 
55299  143 
Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment) 
55220  144 
end 
145 
 chain_isar_step _ step = step 

146 
and chain_isar_steps _ [] = [] 

57655  147 
 chain_isar_steps prev (i :: is) = 
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset

148 
chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is 
55220  149 
and chain_isar_proof (Proof (fix, assms, steps)) = 
150 
Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps) 

151 

152 
fun kill_useless_labels_in_isar_proof proof = 

153 
let 

154 
val used_ls = 

55279  155 
fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) [] 
55220  156 

157 
fun kill_label l = if member (op =) used_ls l then l else no_label 

158 

55299  159 
fun kill_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) = 
160 
Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment) 

55220  161 
 kill_step step = step 
162 
and kill_proof (Proof (fix, assms, steps)) = 

163 
Proof (fix, map (apfst kill_label) assms, map kill_step steps) 

164 
in 

165 
kill_proof proof 

166 
end 

167 

55213  168 
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

169 
let 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset

170 
fun next_label l (next, subst) = 
54534  171 
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

172 

55299  173 
fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths, comment)) 
174 
(accum as (_, subst)) = 

54534  175 
let 
55281  176 
val lfs' = maps (the_list o AList.lookup (op =) subst) lfs 
177 
val ((subs', l'), accum') = accum 

178 
> fold_map relabel_proof subs 

179 
>> next_label l 

54534  180 
in 
55299  181 
(Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum') 
54534  182 
end 
55281  183 
 relabel_step step accum = (step, accum) 
184 
and relabel_proof (Proof (fix, assms, steps)) = 

185 
fold_map (fn (l, t) => next_label l #> apfst (rpair t)) assms 

186 
##>> fold_map relabel_step steps 

187 
#>> (fn (assms, steps) => Proof (fix, assms, steps)) 

52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset

188 
in 
55279  189 
fst (relabel_proof proof (0, [])) 
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset

190 
end 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset

191 

55282  192 
val relabel_isar_proof_nicely = 
55220  193 
let 
55281  194 
fun next_label depth prefix l (accum as (next, subst)) = 
55220  195 
if l = no_label then 
55281  196 
(l, accum) 
55220  197 
else 
198 
let val l' = (replicate_string (depth + 1) prefix, next) in 

55281  199 
(l', (next + 1, (l, l') :: subst)) 
55220  200 
end 
201 

55299  202 
fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) 
203 
(accum as (_, subst)) = 

55220  204 
let 
55281  205 
val lfs' = maps (the_list o AList.lookup (op =) subst) lfs 
55309  206 
val (l', accum' as (_, subst')) = next_label depth have_prefix l accum 
55281  207 
val subs' = map (relabel_proof subst' (depth + 1)) subs 
55220  208 
in 
55299  209 
(Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum') 
55220  210 
end 
55281  211 
 relabel_step _ step accum = (step, accum) 
55220  212 
and relabel_proof subst depth (Proof (fix, assms, steps)) = 
55281  213 
(1, subst) 
214 
> fold_map (fn (l, t) => next_label depth assume_prefix l #> apfst (rpair t)) assms 

215 
>> fold_map (relabel_step depth) steps 

216 
> (fn ((assms, steps), _) => Proof (fix, assms, steps)) 

55220  217 
in 
218 
relabel_proof [] 0 

219 
end 

220 

57793  221 
fun stutter_single_letter s = String.extract (s, 0, SOME 1) ^ s 
222 

57792  223 
fun rationalize_obtains_in_isar_proofs ctxt = 
224 
let 

225 
fun rename_obtains xs (subst, ctxt) = 

226 
let 

227 
val Ts = map snd xs 

57793  228 
val new_names0 = map (stutter_single_letter o var_name_of_typ o body_type) Ts 
57792  229 
val (new_names, ctxt') = Variable.variant_fixes new_names0 ctxt 
230 
val ys = map2 pair new_names Ts 

231 
in 

232 
(ys, ((map Free xs ~~ map Free ys) @ subst, ctxt')) 

233 
end 

234 

235 
fun rationalize_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) subst_ctxt = 

236 
let 

237 
val (xs', subst_ctxt' as (subst', _)) = rename_obtains xs subst_ctxt 

238 
val t' = subst_atomic subst' t 

239 
val subs' = map (rationalize_proof subst_ctxt') subs 

240 
in 

241 
(Prove (qs, xs', l, t', subs', facts, meths, comment), subst_ctxt') 

242 
end 

243 
and rationalize_proof (subst_ctxt as (subst, _)) (Proof (fix, assms, steps)) = 

244 
Proof (fix, map (apsnd (subst_atomic subst)) assms, 

245 
fst (fold_map rationalize_step steps subst_ctxt)) 

246 
in 

247 
rationalize_proof ([], ctxt) 

248 
end 

249 

55211  250 
val indent_size = 2 
251 

56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset

252 
fun string_of_isar_proof ctxt0 i n proof = 
55211  253 
let 
254 
(* 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

255 
val ctxt = ctxt0 
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset

256 
> 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

257 
> 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

258 
> 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

259 
> 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

260 
> Config.put show_consts false 
55211  261 

55216  262 
fun add_str s' = apfst (suffix s') 
55211  263 

264 
fun of_indent ind = replicate_string (ind * indent_size) " " 

265 
fun of_moreover ind = of_indent ind ^ "moreover\n" 

266 
fun of_label l = if l = no_label then "" else string_of_label l ^ ": " 

267 

268 
fun of_obtain qs nr = 

269 
(if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " 

270 
else if nr = 1 orelse member (op =) qs Then then "then " 

271 
else "") ^ "obtain" 

272 

273 
fun of_show_have qs = if member (op =) qs Show then "show" else "have" 

274 
fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence" 

275 

276 
fun of_have qs nr = 

277 
if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs 

278 
else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs 

279 
else of_show_have qs 

280 

281 
fun add_term term (s, ctxt) = 

282 
(s ^ (term 

283 
> singleton (Syntax.uncheck_terms ctxt) 

55213  284 
> annotate_types_in_term ctxt 
55211  285 
> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of) 
286 
> simplify_spaces 

287 
> maybe_quote), 

57669  288 
ctxt > perhaps (try (Variable.auto_fixes term))) 
55211  289 

56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56081
diff
changeset

290 
fun using_facts [] [] = "" 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56081
diff
changeset

291 
 using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss)) 
55257  292 

55211  293 
(* Local facts are always passed via "using", which affects "meson" and "metis". This is 
294 
arguably stylistically superior, because it emphasises the structure of the proof. It is also 

295 
more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence" 

296 
and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *) 

57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

297 
fun of_method ls ss meth = 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

298 
let val direct = is_proof_method_direct meth in 
55281  299 
using_facts ls (if direct then [] else ss) ^ 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

300 
"by " ^ string_of_proof_method ctxt (if direct then ss else []) meth 
55281  301 
end 
55211  302 

303 
fun of_free (s, T) = 

304 
maybe_quote s ^ " :: " ^ 

305 
maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T)) 

306 

307 
fun add_frees xs (s, ctxt) = 

57669  308 
(s ^ space_implode " and " (map of_free xs), ctxt > fold Variable.auto_fixes (map Free xs)) 
55211  309 

310 
fun add_fix _ [] = I 

55281  311 
 add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n" 
55211  312 

313 
fun add_assm ind (l, t) = 

55281  314 
add_str (of_indent ind ^ "assume " ^ of_label l) #> add_term t #> add_str "\n" 
55211  315 

316 
fun of_subproof ind ctxt proof = 

317 
let 

318 
val ind = ind + 1 

319 
val s = of_proof ind ctxt proof 

320 
val prefix = "{ " 

321 
val suffix = " }" 

322 
in 

323 
replicate_string (ind * indent_size  size prefix) " " ^ prefix ^ 

324 
String.extract (s, ind * indent_size, SOME (size s  ind * indent_size  1)) ^ 

325 
suffix ^ "\n" 

326 
end 

327 
and of_subproofs _ _ _ [] = "" 

55281  328 
 of_subproofs ind ctxt qs subs = 
55211  329 
(if member (op =) qs Then then of_moreover ind else "") ^ 
55281  330 
space_implode (of_moreover ind) (map (of_subproof ind ctxt) subs) 
331 
and add_step_pre ind qs subs (s, ctxt) = 

332 
(s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt) 

55211  333 
and add_step ind (Let (t1, 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

334 
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

335 
#> add_str "\n" 
55309  336 
 add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meth :: _, comment)) = 
55281  337 
add_step_pre ind qs subs 
55211  338 
#> (case xs 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

339 
[] => add_str (of_have qs (length subs) ^ " ") 
1111a9a328fe
rationalized sorting of facts  so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset

340 
 _ => add_str (of_obtain qs (length subs) ^ " ") #> add_frees xs #> add_str " where ") 
55217  341 
#> add_str (of_label l) 
342 
#> add_term t 

58054
1d9edd486479
reintroduced twolineperinference Isar proof format
blanchet
parents:
57793
diff
changeset

343 
#> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^ 
57776
1111a9a328fe
rationalized sorting of facts  so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57765
diff
changeset

344 
(if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n") 
55211  345 
and add_steps ind = fold (add_step ind) 
346 
and of_proof ind ctxt (Proof (xs, assms, steps)) = 

55281  347 
("", ctxt) 
348 
> add_fix ind xs 

349 
> fold (add_assm ind) assms 

350 
> add_steps ind steps 

351 
> fst 

55211  352 
in 
57286
4868ec62f533
don't generate Isar proof skeleton for what amounts to a oneline proof
blanchet
parents:
57154
diff
changeset

353 
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

354 
of_indent 0 ^ "proof \n" ^ of_proof 1 ctxt proof ^ 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

355 
of_indent 0 ^ (if n = 1 then "qed" else "next") 
55211  356 
end 
357 

54504  358 
end; 