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 


8 
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =


9 
sig

49914

10 
type 'a proof = 'a ATP_Proof.proof


11 
type stature = ATP_Problem_Generate.stature


12 


13 
datatype reconstructor =


14 
Metis of string * string 


15 
SMT


16 


17 
datatype play =


18 
Played of reconstructor * Time.time 


19 
Trust_Playable of reconstructor * Time.time option 


20 
Failed_to_Play of reconstructor


21 


22 
type minimize_command = string list > string


23 
type one_line_params =


24 
play * string * (string * stature) list * minimize_command * int * int


25 
type isar_params =


26 
bool * int * string Symtab.table * (string * stature) list vector


27 
* int Symtab.table * string proof * thm


28 


29 
val smtN : string


30 
val string_for_reconstructor : reconstructor > string


31 
val lam_trans_from_atp_proof : string proof > string > string


32 
val is_typed_helper_used_in_atp_proof : string proof > bool


33 
val used_facts_in_atp_proof :


34 
Proof.context > (string * stature) list vector > string proof >


35 
(string * stature) list


36 
val used_facts_in_unsound_atp_proof :


37 
Proof.context > (string * stature) list vector > 'a proof >


38 
string list option


39 
val one_line_proof_text : int > one_line_params > string

49883

40 
val isar_proof_text :

49913

41 
Proof.context > bool > isar_params > one_line_params > string

49883

42 
val proof_text :

49913

43 
Proof.context > bool > isar_params > int > one_line_params > string

49883

44 
end;


45 


46 
structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =


47 
struct


48 


49 
open ATP_Util

49914

50 
open ATP_Problem

49883

51 
open ATP_Proof


52 
open ATP_Problem_Generate


53 
open ATP_Proof_Reconstruct

49914

54 


55 
structure String_Redirect = ATP_Proof_Redirect(


56 
type key = step_name


57 
val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')


58 
val string_of = fst)


59 

49883

60 
open String_Redirect


61 

49914

62 
(** reconstructors **)


63 


64 
datatype reconstructor =


65 
Metis of string * string 


66 
SMT


67 


68 
datatype play =


69 
Played of reconstructor * Time.time 


70 
Trust_Playable of reconstructor * Time.time option 


71 
Failed_to_Play of reconstructor


72 


73 
val smtN = "smt"


74 


75 
fun string_for_reconstructor (Metis (type_enc, lam_trans)) =


76 
metis_call type_enc lam_trans


77 
 string_for_reconstructor SMT = smtN


78 


79 


80 
(** fact extraction from ATP proofs **)


81 


82 
fun find_first_in_list_vector vec key =


83 
Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key


84 
 (_, value) => value) NONE vec


85 


86 
val unprefix_fact_number = space_implode "_" o tl o space_explode "_"


87 


88 
fun resolve_one_named_fact fact_names s =


89 
case try (unprefix fact_prefix) s of


90 
SOME s' =>


91 
let val s' = s' > unprefix_fact_number > unascii_of in


92 
s' > find_first_in_list_vector fact_names > Option.map (pair s')


93 
end


94 
 NONE => NONE


95 
fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)


96 
fun is_fact fact_names = not o null o resolve_fact fact_names


97 


98 
fun resolve_one_named_conjecture s =


99 
case try (unprefix conjecture_prefix) s of


100 
SOME s' => Int.fromString s'


101 
 NONE => NONE


102 


103 
val resolve_conjecture = map_filter resolve_one_named_conjecture


104 
val is_conjecture = not o null o resolve_conjecture


105 


106 
val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix


107 


108 
(* overapproximation (good enough) *)


109 
fun is_lam_lifted s =


110 
String.isPrefix fact_prefix s andalso


111 
String.isSubstring ascii_of_lam_fact_prefix s


112 


113 
val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)


114 


115 
fun is_axiom_used_in_proof pred =


116 
exists (fn Inference_Step ((_, ss), _, _, []) => exists pred ss  _ => false)


117 


118 
fun lam_trans_from_atp_proof atp_proof default =


119 
case (is_axiom_used_in_proof is_combinator_def atp_proof,


120 
is_axiom_used_in_proof is_lam_lifted atp_proof) of


121 
(false, false) => default


122 
 (false, true) => liftingN


123 
(*  (true, true) => combs_and_liftingN  not supported by "metis" *)


124 
 (true, _) => combsN


125 


126 
val is_typed_helper_name =


127 
String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix


128 
fun is_typed_helper_used_in_atp_proof atp_proof =


129 
is_axiom_used_in_proof is_typed_helper_name atp_proof


130 


131 
fun add_non_rec_defs fact_names accum =


132 
Vector.foldl (fn (facts, facts') =>


133 
union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)


134 
facts')


135 
accum fact_names


136 


137 
val isa_ext = Thm.get_name_hint @{thm ext}


138 
val isa_short_ext = Long_Name.base_name isa_ext


139 


140 
fun ext_name ctxt =


141 
if Thm.eq_thm_prop (@{thm ext},


142 
singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then


143 
isa_short_ext


144 
else


145 
isa_ext


146 


147 
val leo2_ext = "extcnf_equal_neg"


148 
val leo2_unfold_def = "unfold_def"


149 


150 
fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) =


151 
(if rule = leo2_ext then


152 
insert (op =) (ext_name ctxt, (Global, General))


153 
else if rule = leo2_unfold_def then


154 
(* LEO 1.3.3 does not record definitions properly, leading to missing


155 
dependencies in the TSTP proof. Remove the next line once this is


156 
fixed. *)


157 
add_non_rec_defs fact_names


158 
else if rule = satallax_coreN then


159 
(fn [] =>


160 
(* Satallax doesn't include definitions in its unsatisfiable cores,


161 
so we assume the worst and include them all here. *)


162 
[(ext_name ctxt, (Global, General))] > add_non_rec_defs fact_names


163 
 facts => facts)


164 
else


165 
I)


166 
#> (if null deps then union (op =) (resolve_fact fact_names ss)


167 
else I)


168 
 add_fact _ _ _ = I


169 


170 
fun used_facts_in_atp_proof ctxt fact_names atp_proof =


171 
if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names


172 
else fold (add_fact ctxt fact_names) atp_proof []


173 


174 
fun used_facts_in_unsound_atp_proof _ _ [] = NONE


175 
 used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =


176 
let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in


177 
if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso


178 
not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then


179 
SOME (map fst used_facts)


180 
else


181 
NONE


182 
end


183 


184 


185 
(** oneliner reconstructor proofs **)


186 


187 
fun string_for_label (s, num) = s ^ string_of_int num


188 


189 
fun show_time NONE = ""


190 
 show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"


191 


192 
fun unusing_chained_facts _ 0 = ""


193 
 unusing_chained_facts used_chaineds num_chained =


194 
if length used_chaineds = num_chained then ""


195 
else if null used_chaineds then "(* using no facts *) "


196 
else "(* using only " ^ space_implode " " used_chaineds ^ " *) "


197 


198 
fun apply_on_subgoal _ 1 = "by "


199 
 apply_on_subgoal 1 _ = "apply "


200 
 apply_on_subgoal i n =


201 
"prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n


202 


203 
fun using_labels [] = ""


204 
 using_labels ls =


205 
"using " ^ space_implode " " (map string_for_label ls) ^ " "


206 


207 
fun command_call name [] =


208 
name > not (Lexicon.is_identifier name) ? enclose "(" ")"


209 
 command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"


210 


211 
fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =


212 
unusing_chained_facts used_chaineds num_chained ^


213 
using_labels ls ^ apply_on_subgoal i n ^


214 
command_call (string_for_reconstructor reconstr) ss


215 


216 
fun try_command_line banner time command =


217 
banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^


218 
show_time time ^ "."


219 


220 
fun minimize_line _ [] = ""


221 
 minimize_line minimize_command ss =


222 
case minimize_command ss of


223 
"" => ""


224 
 command =>


225 
"\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."


226 


227 
fun split_used_facts facts =


228 
facts > List.partition (fn (_, (sc, _)) => sc = Chained)


229 
> pairself (sort_distinct (string_ord o pairself fst))


230 


231 
type minimize_command = string list > string


232 
type one_line_params =


233 
play * string * (string * stature) list * minimize_command * int * int


234 


235 
fun one_line_proof_text num_chained


236 
(preplay, banner, used_facts, minimize_command, subgoal,


237 
subgoal_count) =


238 
let


239 
val (chained, extra) = split_used_facts used_facts


240 
val (failed, reconstr, ext_time) =


241 
case preplay of


242 
Played (reconstr, time) => (false, reconstr, (SOME (false, time)))


243 
 Trust_Playable (reconstr, time) =>


244 
(false, reconstr,


245 
case time of


246 
NONE => NONE


247 
 SOME time =>


248 
if time = Time.zeroTime then NONE else SOME (true, time))


249 
 Failed_to_Play reconstr => (true, reconstr, NONE)


250 
val try_line =


251 
([], map fst extra)


252 
> reconstructor_command reconstr subgoal subgoal_count (map fst chained)


253 
num_chained


254 
> (if failed then


255 
enclose "Oneline proof reconstruction failed: "


256 
".\n(Invoking \"sledgehammer\" with \"[strict]\" might \


257 
\solve this.)"


258 
else


259 
try_command_line banner ext_time)


260 
in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end


261 


262 


263 
(** Isar proof construction and manipulation **)


264 


265 
type label = string * int


266 
type facts = label list * string list


267 


268 
datatype isar_qualifier = Show  Then  Moreover  Ultimately


269 


270 
datatype isar_step =


271 
Fix of (string * typ) list 


272 
Let of term * term 


273 
Assume of label * term 


274 
Prove of isar_qualifier list * label * term * byline


275 
and byline =


276 
By_Metis of facts 


277 
Case_Split of isar_step list list * facts


278 


279 
val assum_prefix = "a"


280 
val have_prefix = "f"


281 
val raw_prefix = "x"


282 


283 
fun raw_label_for_name (num, ss) =


284 
case resolve_conjecture ss of


285 
[j] => (conjecture_prefix, j)


286 
 _ => (raw_prefix ^ ascii_of num, 0)


287 


288 
fun add_fact_from_dependency fact_names (name as (_, ss)) =


289 
if is_fact fact_names ss then


290 
apsnd (union (op =) (map fst (resolve_fact fact_names ss)))


291 
else


292 
apfst (insert (op =) (raw_label_for_name name))


293 


294 
fun repair_name "$true" = "c_True"


295 
 repair_name "$false" = "c_False"


296 
 repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)


297 
 repair_name s =


298 
if is_tptp_equal s orelse


299 
(* seen in Vampire proofs *)


300 
(String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then


301 
tptp_equal


302 
else


303 
s


304 


305 
fun unvarify_term (Var ((s, 0), T)) = Free (s, T)


306 
 unvarify_term t = raise TERM ("unvarify_term: nonVar", [t])


307 


308 
fun infer_formula_types ctxt =


309 
Type.constraint HOLogic.boolT


310 
#> Syntax.check_term


311 
(Proof_Context.set_mode Proof_Context.mode_schematic ctxt)


312 


313 
val combinator_table =


314 
[(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),


315 
(@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),


316 
(@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),


317 
(@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),


318 
(@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]


319 


320 
fun uncombine_term thy =


321 
let


322 
fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))


323 
 aux (Abs (s, T, t')) = Abs (s, T, aux t')


324 
 aux (t as Const (x as (s, _))) =


325 
(case AList.lookup (op =) combinator_table s of


326 
SOME thm => thm > prop_of > specialize_type thy x


327 
> Logic.dest_equals > snd


328 
 NONE => t)


329 
 aux t = t


330 
in aux end


331 


332 
fun decode_line sym_tab (Definition_Step (name, phi1, phi2)) ctxt =


333 
let


334 
val thy = Proof_Context.theory_of ctxt


335 
val t1 = prop_from_atp ctxt true sym_tab phi1


336 
val vars = snd (strip_comb t1)


337 
val frees = map unvarify_term vars


338 
val unvarify_args = subst_atomic (vars ~~ frees)


339 
val t2 = prop_from_atp ctxt true sym_tab phi2


340 
val (t1, t2) =


341 
HOLogic.eq_const HOLogic.typeT $ t1 $ t2


342 
> unvarify_args > uncombine_term thy > infer_formula_types ctxt


343 
> HOLogic.dest_eq


344 
in


345 
(Definition_Step (name, t1, t2),


346 
fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt)


347 
end


348 
 decode_line sym_tab (Inference_Step (name, u, rule, deps)) ctxt =


349 
let


350 
val thy = Proof_Context.theory_of ctxt


351 
val t = u > prop_from_atp ctxt true sym_tab


352 
> uncombine_term thy > infer_formula_types ctxt


353 
in


354 
(Inference_Step (name, t, rule, deps),


355 
fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)


356 
end


357 
fun decode_lines ctxt sym_tab lines =


358 
fst (fold_map (decode_line sym_tab) lines ctxt)


359 


360 
fun replace_one_dependency (old, new) dep =


361 
if is_same_atp_step dep old then new else [dep]


362 
fun replace_dependencies_in_line _ (line as Definition_Step _) = line


363 
 replace_dependencies_in_line p (Inference_Step (name, t, rule, deps)) =


364 
Inference_Step (name, t, rule,


365 
fold (union (op =) o replace_one_dependency p) deps [])


366 


367 
(* No "real" literals means only type information (tfree_tcs, clsrel, or


368 
clsarity). *)


369 
fun is_only_type_information t = t aconv @{term True}


370 


371 
fun is_same_inference _ (Definition_Step _) = false


372 
 is_same_inference t (Inference_Step (_, t', _, _)) = t aconv t'


373 


374 
(* Discard facts; consolidate adjacent lines that prove the same formula, since


375 
they differ only in type information.*)


376 
fun add_line _ (line as Definition_Step _) lines = line :: lines


377 
 add_line fact_names (Inference_Step (name as (_, ss), t, rule, [])) lines =


378 
(* No dependencies: fact, conjecture, or (for Vampire) internal facts or


379 
definitions. *)


380 
if is_fact fact_names ss then


381 
(* Facts are not proof lines. *)


382 
if is_only_type_information t then


383 
map (replace_dependencies_in_line (name, [])) lines


384 
(* Is there a repetition? If so, replace later line by earlier one. *)


385 
else case take_prefix (not o is_same_inference t) lines of


386 
(_, []) => lines (* no repetition of proof line *)


387 
 (pre, Inference_Step (name', _, _, _) :: post) =>


388 
pre @ map (replace_dependencies_in_line (name', [name])) post


389 
 _ => raise Fail "unexpected inference"


390 
else if is_conjecture ss then


391 
Inference_Step (name, t, rule, []) :: lines


392 
else


393 
map (replace_dependencies_in_line (name, [])) lines


394 
 add_line _ (Inference_Step (name, t, rule, deps)) lines =


395 
(* Type information will be deleted later; skip repetition test. *)


396 
if is_only_type_information t then


397 
Inference_Step (name, t, rule, deps) :: lines


398 
(* Is there a repetition? If so, replace later line by earlier one. *)


399 
else case take_prefix (not o is_same_inference t) lines of


400 
(* FIXME: Doesn't this code risk conflating proofs involving different


401 
types? *)


402 
(_, []) => Inference_Step (name, t, rule, deps) :: lines


403 
 (pre, Inference_Step (name', t', rule, _) :: post) =>


404 
Inference_Step (name, t', rule, deps) ::


405 
pre @ map (replace_dependencies_in_line (name', [name])) post


406 
 _ => raise Fail "unexpected inference"


407 


408 
val waldmeister_conjecture_num = "1.0.0.0"


409 


410 
val repair_waldmeister_endgame =


411 
let


412 
fun do_tail (Inference_Step (name, t, rule, deps)) =


413 
Inference_Step (name, s_not t, rule, deps)


414 
 do_tail line = line


415 
fun do_body [] = []


416 
 do_body ((line as Inference_Step ((num, _), _, _, _)) :: lines) =


417 
if num = waldmeister_conjecture_num then map do_tail (line :: lines)


418 
else line :: do_body lines


419 
 do_body (line :: lines) = line :: do_body lines


420 
in do_body end


421 


422 
(* Recursively delete empty lines (type information) from the proof. *)


423 
fun add_nontrivial_line (line as Inference_Step (name, t, _, [])) lines =


424 
if is_only_type_information t then delete_dependency name lines


425 
else line :: lines


426 
 add_nontrivial_line line lines = line :: lines


427 
and delete_dependency name lines =


428 
fold_rev add_nontrivial_line


429 
(map (replace_dependencies_in_line (name, [])) lines) []


430 


431 
(* ATPs sometimes reuse free variable names in the strangest ways. Removing


432 
offending lines often does the trick. *)


433 
fun is_bad_free frees (Free x) = not (member (op =) frees x)


434 
 is_bad_free _ _ = false


435 


436 
fun add_desired_line _ _ _ (line as Definition_Step (name, _, _)) (j, lines) =


437 
(j, line :: map (replace_dependencies_in_line (name, [])) lines)


438 
 add_desired_line isar_shrink_factor fact_names frees


439 
(Inference_Step (name as (_, ss), t, rule, deps)) (j, lines) =


440 
(j + 1,


441 
if is_fact fact_names ss orelse


442 
is_conjecture ss orelse


443 
(* the last line must be kept *)


444 
j = 0 orelse


445 
(not (is_only_type_information t) andalso


446 
null (Term.add_tvars t []) andalso


447 
not (exists_subterm (is_bad_free frees) t) andalso


448 
length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso


449 
(* kill next to last line, which usually results in a trivial step *)


450 
j <> 1) then


451 
Inference_Step (name, t, rule, deps) :: lines (* keep line *)


452 
else


453 
map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)


454 

49883

455 
(** Type annotations **)


456 


457 
fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s


458 
 post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s


459 
 post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s


460 
 post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s


461 
 post_traverse_term_type' f env (Abs (x, T1, b)) s =


462 
let


463 
val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s


464 
in f (Abs (x, T1, b')) (T1 > T2) s' end


465 
 post_traverse_term_type' f env (u $ v) s =


466 
let


467 
val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s


468 
val ((v', s''), _) = post_traverse_term_type' f env v s'


469 
in f (u' $ v') T s'' end


470 


471 
fun post_traverse_term_type f s t =


472 
post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s > fst


473 
fun post_fold_term_type f s t =


474 
post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t > snd


475 


476 
(* Data structures, orders *)


477 
val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)


478 


479 
structure Var_Set_Tab = Table(


480 
type key = indexname list


481 
val ord = list_ord Term_Ord.fast_indexname_ord)


482 


483 
(* (1) Generalize Types *)


484 
fun generalize_types ctxt t =


485 
t > map_types (fn _ => dummyT)


486 
> Syntax.check_term


487 
(Proof_Context.set_mode Proof_Context.mode_pattern ctxt)


488 


489 
(* (2) Typingspot Table *)


490 
local


491 
fun key_of_atype (TVar (idxn, _)) =


492 
Ord_List.insert Term_Ord.fast_indexname_ord idxn


493 
 key_of_atype _ = I


494 
fun key_of_type T = fold_atyps key_of_atype T []


495 
fun update_tab t T (tab, pos) =


496 
(case key_of_type T of


497 
[] => tab


498 
 key =>


499 
let val cost = (size_of_typ T, (size_of_term t, pos)) in


500 
case Var_Set_Tab.lookup tab key of


501 
NONE => Var_Set_Tab.update_new (key, cost) tab


502 
 SOME old_cost =>


503 
(case cost_ord (cost, old_cost) of


504 
LESS => Var_Set_Tab.update (key, cost) tab


505 
 _ => tab)


506 
end,


507 
pos + 1)


508 
in


509 
val typing_spot_table =


510 
post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst


511 
end


512 


513 
(* (3) ReverseGreedy *)


514 
fun reverse_greedy typing_spot_tab =


515 
let


516 
fun update_count z =


517 
fold (fn tvar => fn tab =>


518 
let val c = Vartab.lookup tab tvar > the_default 0 in


519 
Vartab.update (tvar, c + z) tab


520 
end)


521 
fun superfluous tcount =


522 
forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)


523 
fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =


524 
if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)


525 
else (spot :: spots, tcount)


526 
val (typing_spots, tvar_count_tab) =


527 
Var_Set_Tab.fold


528 
(fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))


529 
typing_spot_tab ([], Vartab.empty)


530 
>> sort_distinct (rev_order o cost_ord o pairself snd)


531 
in fold drop_superfluous typing_spots ([], tvar_count_tab) > fst end


532 


533 
(* (4) Introduce Annotations *)


534 
fun introduce_annotations thy spots t t' =


535 
let


536 
val get_types = post_fold_term_type (K cons) []


537 
fun match_types tp =


538 
fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty


539 
fun unica' b x [] = if b then [x] else []


540 
 unica' b x (y :: ys) =


541 
if x = y then unica' false x ys


542 
else unica' true y ys > b ? cons x


543 
fun unica ord xs =


544 
case sort ord xs of x :: ys => unica' true x ys  [] => []


545 
val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x  _ => I)


546 
fun erase_unica_tfrees env =


547 
let


548 
val unica =


549 
Vartab.fold (add_all_tfree_namesT o snd o snd) env []


550 
> unica fast_string_ord


551 
val erase_unica = map_atyps


552 
(fn T as TFree (s, _) =>


553 
if Ord_List.member fast_string_ord unica s then dummyT else T


554 
 T => T)


555 
in Vartab.map (K (apsnd erase_unica)) env end


556 
val env = match_types (t', t) > erase_unica_tfrees


557 
fun get_annot env (TFree _) = (false, (env, dummyT))


558 
 get_annot env (T as TVar (v, S)) =


559 
let val T' = Envir.subst_type env T in


560 
if T' = dummyT then (false, (env, dummyT))


561 
else (true, (Vartab.update (v, (S, dummyT)) env, T'))


562 
end


563 
 get_annot env (Type (S, Ts)) =


564 
(case fold_rev (fn T => fn (b, (env, Ts)) =>


565 
let


566 
val (b', (env', T)) = get_annot env T


567 
in (b orelse b', (env', T :: Ts)) end)


568 
Ts (false, (env, [])) of


569 
(true, (env', Ts)) => (true, (env', Type (S, Ts)))


570 
 (false, (env', _)) => (false, (env', dummyT)))


571 
fun post1 _ T (env, cp, ps as p :: ps', annots) =


572 
if p <> cp then


573 
(env, cp + 1, ps, annots)


574 
else


575 
let val (_, (env', T')) = get_annot env T in


576 
(env', cp + 1, ps', (p, T') :: annots)


577 
end


578 
 post1 _ _ accum = accum


579 
val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t'


580 
fun post2 t _ (cp, annots as (p, T) :: annots') =


581 
if p <> cp then (t, (cp + 1, annots))


582 
else (Type.constraint T t, (cp + 1, annots'))


583 
 post2 t _ x = (t, x)


584 
in post_traverse_term_type post2 (0, rev annots) t > fst end


585 


586 
(* (5) Annotate *)


587 
fun annotate_types ctxt t =


588 
let


589 
val thy = Proof_Context.theory_of ctxt


590 
val t' = generalize_types ctxt t


591 
val typing_spots =


592 
t' > typing_spot_table


593 
> reverse_greedy


594 
> sort int_ord


595 
in introduce_annotations thy typing_spots t t' end


596 

49914

597 
val indent_size = 2


598 
val no_label = ("", ~1)


599 

49883

600 
fun string_for_proof ctxt type_enc lam_trans i n =


601 
let


602 
fun fix_print_mode f x =


603 
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)


604 
(print_mode_value ())) f x


605 
fun do_indent ind = replicate_string (ind * indent_size) " "


606 
fun do_free (s, T) =


607 
maybe_quote s ^ " :: " ^


608 
maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)


609 
fun do_label l = if l = no_label then "" else string_for_label l ^ ": "


610 
fun do_have qs =


611 
(if member (op =) qs Moreover then "moreover " else "") ^


612 
(if member (op =) qs Ultimately then "ultimately " else "") ^


613 
(if member (op =) qs Then then


614 
if member (op =) qs Show then "thus" else "hence"


615 
else


616 
if member (op =) qs Show then "show" else "have")


617 
val do_term =


618 
maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)


619 
o annotate_types ctxt


620 
val reconstr = Metis (type_enc, lam_trans)


621 
fun do_facts (ls, ss) =


622 
reconstructor_command reconstr 1 1 [] 0


623 
(ls > sort_distinct (prod_ord string_ord int_ord),


624 
ss > sort_distinct string_ord)


625 
and do_step ind (Fix xs) =


626 
do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"


627 
 do_step ind (Let (t1, t2)) =


628 
do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"


629 
 do_step ind (Assume (l, t)) =


630 
do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"


631 
 do_step ind (Prove (qs, l, t, By_Metis facts)) =


632 
do_indent ind ^ do_have qs ^ " " ^


633 
do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"


634 
 do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =


635 
implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)


636 
proofs) ^


637 
do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^


638 
do_facts facts ^ "\n"


639 
and do_steps prefix suffix ind steps =


640 
let val s = implode (map (do_step ind) steps) in


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


642 
String.extract (s, ind * indent_size,


643 
SOME (size s  ind * indent_size  1)) ^


644 
suffix ^ "\n"


645 
end


646 
and do_block ind proof = do_steps "{ " " }" (ind + 1) proof


647 
(* Onestep proofs are pointless; better use the Metis oneliner


648 
directly. *)


649 
and do_proof [Prove (_, _, _, By_Metis _)] = ""


650 
 do_proof proof =


651 
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^


652 
do_indent 0 ^ "proof \n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^


653 
(if n <> 1 then "next" else "qed")


654 
in do_proof end


655 

49914

656 
(* FIXME: Still needed? Try with SPASS proofs perhaps. *)


657 
val kill_duplicate_assumptions_in_proof =


658 
let


659 
fun relabel_facts subst =


660 
apfst (map (fn l => AList.lookup (op =) subst l > the_default l))


661 
fun do_step (step as Assume (l, t)) (proof, subst, assums) =


662 
(case AList.lookup (op aconv) assums t of


663 
SOME l' => (proof, (l, l') :: subst, assums)


664 
 NONE => (step :: proof, subst, (t, l) :: assums))


665 
 do_step (Prove (qs, l, t, by)) (proof, subst, assums) =


666 
(Prove (qs, l, t,


667 
case by of


668 
By_Metis facts => By_Metis (relabel_facts subst facts)


669 
 Case_Split (proofs, facts) =>


670 
Case_Split (map do_proof proofs,


671 
relabel_facts subst facts)) ::


672 
proof, subst, assums)


673 
 do_step step (proof, subst, assums) = (step :: proof, subst, assums)


674 
and do_proof proof = fold do_step proof ([], [], []) > #1 > rev


675 
in do_proof end


676 


677 
fun used_labels_of_step (Prove (_, _, _, by)) =


678 
(case by of


679 
By_Metis (ls, _) => ls


680 
 Case_Split (proofs, (ls, _)) =>


681 
fold (union (op =) o used_labels_of) proofs ls)


682 
 used_labels_of_step _ = []


683 
and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []


684 


685 
fun kill_useless_labels_in_proof proof =


686 
let


687 
val used_ls = used_labels_of proof


688 
fun do_label l = if member (op =) used_ls l then l else no_label


689 
fun do_step (Assume (l, t)) = Assume (do_label l, t)


690 
 do_step (Prove (qs, l, t, by)) =


691 
Prove (qs, do_label l, t,


692 
case by of


693 
Case_Split (proofs, facts) =>


694 
Case_Split (map (map do_step) proofs, facts)


695 
 _ => by)


696 
 do_step step = step


697 
in map do_step proof end


698 


699 
fun prefix_for_depth n = replicate_string (n + 1)


700 


701 
val relabel_proof =


702 
let


703 
fun aux _ _ _ [] = []


704 
 aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =


705 
if l = no_label then


706 
Assume (l, t) :: aux subst depth (next_assum, next_fact) proof


707 
else


708 
let val l' = (prefix_for_depth depth assum_prefix, next_assum) in


709 
Assume (l', t) ::


710 
aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof


711 
end


712 
 aux subst depth (next_assum, next_fact)


713 
(Prove (qs, l, t, by) :: proof) =


714 
let


715 
val (l', subst, next_fact) =


716 
if l = no_label then


717 
(l, subst, next_fact)


718 
else


719 
let


720 
val l' = (prefix_for_depth depth have_prefix, next_fact)


721 
in (l', (l, l') :: subst, next_fact + 1) end


722 
val relabel_facts =


723 
apfst (maps (the_list o AList.lookup (op =) subst))


724 
val by =


725 
case by of


726 
By_Metis facts => By_Metis (relabel_facts facts)


727 
 Case_Split (proofs, facts) =>


728 
Case_Split (map (aux subst (depth + 1) (1, 1)) proofs,


729 
relabel_facts facts)


730 
in


731 
Prove (qs, l', t, by) :: aux subst depth (next_assum, next_fact) proof


732 
end


733 
 aux subst depth nextp (step :: proof) =


734 
step :: aux subst depth nextp proof


735 
in aux [] 0 (1, 1) end


736 

49913

737 
fun minimize_locally ctxt type_enc lam_trans proof =

49883

738 
let


739 
(* Merging spots, greedy algorithm *)


740 
fun cost (Prove (_, _ , t, _)) = Term.size_of_term t


741 
 cost _ = ~1

49913

742 
fun can_merge (Prove (_, lbl, _, By_Metis _))


743 
(Prove (_, _, _, By_Metis _)) =


744 
(lbl = no_label)

49883

745 
 can_merge _ _ = false


746 
val merge_spots =

49913

747 
fold_index (fn (i, s2) => fn (s1, pile) =>


748 
(s2, pile > can_merge s1 s2 ? cons (i, cost s1)))

49883

749 
(tl proof) (hd proof, [])


750 
> snd > sort (rev_order o int_ord o pairself snd) > map fst


751 


752 
(* Enrich context with facts *)


753 
val thy = Proof_Context.theory_of ctxt


754 
fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *)


755 
fun enrich_ctxt' (Prove (_, lbl, t, _)) ctxt =

49913

756 
ctxt > lbl <> no_label


757 
? Proof_Context.put_thms false (string_for_label lbl, SOME [sorry t])

49883

758 
 enrich_ctxt' _ ctxt = ctxt


759 
val rich_ctxt = fold enrich_ctxt' proof ctxt


760 


761 
(* Timing *)


762 
fun take_time tac arg =


763 
let


764 
val t_start = Timing.start ()


765 
in


766 
(tac arg ; Timing.result t_start > #cpu)


767 
end


768 
fun try_metis (Prove (qs, _, t, By_Metis fact_names)) s0 =


769 
let


770 
fun thmify (Prove (_, _, t, _)) = sorry t

49913

771 
val facts =


772 
fact_names


773 
>> map string_for_label


774 
> op @


775 
> map (Proof_Context.get_thm rich_ctxt)


776 
> (if member (op =) qs Then then cons (the s0 > thmify) else I)

49883

777 
val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *)


778 
fun tac {context = ctxt, prems = _} =


779 
Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1


780 
in


781 
take_time (fn () => goal tac)


782 
end


783 


784 
(* Merging *)


785 
fun merge (Prove (qs1, _, _, By_Metis (ls1, ss1)))


786 
(Prove (qs2, lbl , t, By_Metis (ls2, ss2))) =


787 
let

49913

788 
val qs =


789 
inter (op =) qs1 qs2 (* FIXME: Is this correct? *)


790 
> member (op =) (union (op =) qs1 qs2) Ultimately ? cons Ultimately


791 
> member (op =) qs2 Show ? cons Show


792 
in Prove (qs, lbl, t, By_Metis (ls1 @ ls2, ss1 @ ss2)) end

49883

793 
fun try_merge proof i =


794 
let


795 
val (front, s0, s1, s2, tail) =


796 
case (proof, i) of

49913

797 
((s1 :: s2 :: proof), 0) => ([], NONE, s1, s2, proof)


798 
 _ =>


799 
let val (front, s0 :: s1 :: s2 :: tail) = chop (i  1) proof in


800 
(front, SOME s0, s1, s2, tail)


801 
end

49883

802 
val s12 = merge s1 s2


803 
val t1 = try_metis s1 s0 ()


804 
val t2 = try_metis s2 (SOME s1) ()


805 
val tlimit = t1 + t2 > Time.toReal > curry Real.* 1.2 > Time.fromReal


806 
in


807 
(TimeLimit.timeLimit tlimit (try_metis s12 s0) ();

49913

808 
SOME (front @ (case s0 of


809 
NONE => s12 :: tail


810 
 SOME s => s :: s12 :: tail)))

49883

811 
handle _ => NONE


812 
end


813 
fun merge_steps proof [] = proof

49913

814 
 merge_steps proof (i :: is) =

49883

815 
case try_merge proof i of


816 
NONE => merge_steps proof is

49913

817 
 SOME proof' =>


818 
merge_steps proof' (map (fn j => if j > i then j  1 else j) is)

49883

819 
in merge_steps proof merge_spots end


820 

49914

821 
type isar_params =


822 
bool * int * string Symtab.table * (string * stature) list vector


823 
* int Symtab.table * string proof * thm


824 

49883

825 
fun isar_proof_text ctxt isar_proof_requested


826 
(debug, isar_shrink_factor, pool, fact_names, sym_tab, atp_proof, goal)


827 
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =


828 
let


829 
val isar_shrink_factor =


830 
(if isar_proof_requested then 1 else 2) * isar_shrink_factor


831 
val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal


832 
val frees = fold Term.add_frees (concl_t :: hyp_ts) []


833 
val one_line_proof = one_line_proof_text 0 one_line_params


834 
val type_enc =


835 
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN


836 
else partial_typesN


837 
val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans


838 


839 
fun isar_proof_of () =


840 
let


841 
val atp_proof =


842 
atp_proof


843 
> clean_up_atp_proof_dependencies


844 
> nasty_atp_proof pool


845 
> map_term_names_in_atp_proof repair_name


846 
> decode_lines ctxt sym_tab


847 
> rpair [] > fold_rev (add_line fact_names)


848 
> repair_waldmeister_endgame


849 
> rpair [] > fold_rev add_nontrivial_line


850 
> rpair (0, [])


851 
> fold_rev (add_desired_line isar_shrink_factor fact_names frees)


852 
> snd


853 
val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)


854 
val conjs =


855 
atp_proof


856 
> map_filter (fn Inference_Step (name as (_, ss), _, _, []) =>


857 
if member (op =) ss conj_name then SOME name else NONE


858 
 _ => NONE)


859 
fun dep_of_step (Definition_Step _) = NONE


860 
 dep_of_step (Inference_Step (name, _, _, from)) = SOME (from, name)


861 
val ref_graph = atp_proof > map_filter dep_of_step > make_ref_graph


862 
val axioms = axioms_of_ref_graph ref_graph conjs


863 
val tainted = tainted_atoms_of_ref_graph ref_graph conjs


864 
val props =


865 
Symtab.empty


866 
> fold (fn Definition_Step _ => I (* FIXME *)


867 
 Inference_Step ((s, _), t, _, _) =>


868 
Symtab.update_new (s,


869 
t > fold forall_of (map Var (Term.add_vars t []))


870 
> member (op = o apsnd fst) tainted s ? s_not))


871 
atp_proof


872 
fun prop_of_clause c =


873 
fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)


874 
@{term False}


875 
fun label_of_clause [name] = raw_label_for_name name


876 
 label_of_clause c = (space_implode "___" (map fst c), 0)


877 
fun maybe_show outer c =


878 
(outer andalso length c = 1 andalso subset (op =) (c, conjs))


879 
? cons Show


880 
fun do_have outer qs (gamma, c) =


881 
Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,


882 
By_Metis (fold (add_fact_from_dependency fact_names


883 
o the_single) gamma ([], [])))


884 
fun do_inf outer (Have z) = do_have outer [] z


885 
 do_inf outer (Hence z) = do_have outer [Then] z


886 
 do_inf outer (Cases cases) =


887 
let val c = succedent_of_cases cases in


888 
Prove (maybe_show outer c [Ultimately], label_of_clause c,


889 
prop_of_clause c,


890 
Case_Split (map (do_case false) cases, ([], [])))


891 
end


892 
and do_case outer (c, infs) =


893 
Assume (label_of_clause c, prop_of_clause c) ::


894 
map (do_inf outer) infs


895 
val isar_proof =


896 
(if null params then [] else [Fix params]) @


897 
(ref_graph


898 
> redirect_graph axioms tainted


899 
> chain_direct_proof


900 
> map (do_inf true)


901 
> kill_duplicate_assumptions_in_proof


902 
> kill_useless_labels_in_proof


903 
> relabel_proof

49913

904 
> minimize_locally ctxt type_enc lam_trans)

49883

905 
> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count


906 
in


907 
case isar_proof of


908 
"" =>


909 
if isar_proof_requested then


910 
"\nNo structured proof available (proof too short)."


911 
else


912 
""


913 
 _ =>


914 
"\n\n" ^ (if isar_proof_requested then "Structured proof"


915 
else "Perhaps this will work") ^


916 
":\n" ^ Markup.markup Isabelle_Markup.sendback isar_proof


917 
end


918 
val isar_proof =


919 
if debug then


920 
isar_proof_of ()


921 
else case try isar_proof_of () of


922 
SOME s => s


923 
 NONE => if isar_proof_requested then


924 
"\nWarning: The Isar proof construction failed."


925 
else


926 
""


927 
in one_line_proof ^ isar_proof end


928 


929 
fun proof_text ctxt isar_proof isar_params num_chained


930 
(one_line_params as (preplay, _, _, _, _, _)) =


931 
(if case preplay of Failed_to_Play _ => true  _ => isar_proof then


932 
isar_proof_text ctxt isar_proof isar_params


933 
else


934 
one_line_proof_text num_chained) one_line_params


935 


936 
end;
