# HG changeset patch # User blanchet # Date 1350559184 -7200 # Node ID 23e36a4d28f1dab28c3dd5078052fcf7993f949b # Parent 2e7d0655b176b3aeb91631d03e2803e829514630 refactor code diff -r 2e7d0655b176 -r 23e36a4d28f1 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 18 11:59:45 2012 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 18 13:19:44 2012 +0200 @@ -450,7 +450,7 @@ fun failed failure = ({outcome = SOME failure, used_facts = [], run_time = Time.zeroTime, preplay = - K (ATP_Proof_Reconstruct.Failed_to_Play Sledgehammer_Provers.plain_metis), + K (Sledgehammer_Reconstruct.Failed_to_Play Sledgehammer_Provers.plain_metis), message = K "", message_tail = ""}, ~1) val ({outcome, used_facts, run_time, preplay, message, message_tail} : Sledgehammer_Provers.prover_result, diff -r 2e7d0655b176 -r 23e36a4d28f1 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Oct 18 11:59:45 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Oct 18 13:19:44 2012 +0200 @@ -3,36 +3,15 @@ Author: Claire Quigley, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen -Proof reconstruction from ATP proofs. +Basic proof reconstruction from ATP proofs. *) signature ATP_PROOF_RECONSTRUCT = sig type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula - type 'a proof = 'a ATP_Proof.proof - type stature = ATP_Problem_Generate.stature - - structure String_Redirect : ATP_PROOF_REDIRECT - - datatype reconstructor = - Metis of string * string | - SMT - - datatype play = - Played of reconstructor * Time.time | - Trust_Playable of reconstructor * Time.time option | - Failed_to_Play of reconstructor - - type minimize_command = string list -> string - type one_line_params = - play * string * (string * stature) list * minimize_command * int * int - type isar_params = - bool * int * string Symtab.table * (string * stature) list vector - * int Symtab.table * string proof * thm val metisN : string - val smtN : string val full_typesN : string val partial_typesN : string val no_typesN : string @@ -44,69 +23,14 @@ val partial_type_encs : string list val metis_default_lam_trans : string val metis_call : string -> string -> string - val string_for_reconstructor : reconstructor -> string - val used_facts_in_atp_proof : - Proof.context -> (string * stature) list vector -> string proof - -> (string * stature) list - val lam_trans_from_atp_proof : string proof -> string -> string - val is_typed_helper_used_in_atp_proof : string proof -> bool - val used_facts_in_unsound_atp_proof : - Proof.context -> (string * stature) list vector -> 'a proof - -> string list option val unalias_type_enc : string -> string list - val one_line_proof_text : int -> one_line_params -> string - val make_tvar : string -> typ - val make_tfree : Proof.context -> string -> typ + val forall_of : term -> term -> term val term_from_atp : - Proof.context -> bool -> int Symtab.table -> typ option - -> (string, string) ho_term -> term + Proof.context -> bool -> int Symtab.table -> typ option -> + (string, string) ho_term -> term val prop_from_atp : - Proof.context -> bool -> int Symtab.table - -> (string, string, (string, string) ho_term, string) formula -> term - - type label - type facts = label list * string list - - datatype isar_qualifier = Show | Then | Moreover | Ultimately - - datatype isar_step = - Fix of (string * typ) list | - Let of term * term | - Assume of label * term | - Prove of isar_qualifier list * label * term * byline - and byline = - By_Metis of facts | - Case_Split of isar_step list list * facts - - val string_for_label : label -> string - val decode_lines : - Proof.context -> int Symtab.table - -> (string, string, (string, string) ATP_Problem.ho_term, string) - ATP_Problem.formula ATP_Proof.step list -> term ATP_Proof.step list - val add_line : - (string * 'a) list vector -> term ATP_Proof.step - -> term ATP_Proof.step list -> term ATP_Proof.step list - val repair_waldmeister_endgame : term ATP_Proof.step list -> term ATP_Proof.step list - val add_desired_line : - int -> (string * 'a) list vector -> (string * typ) list -> term ATP_Proof.step - -> int * term ATP_Proof.step list -> int * term ATP_Proof.step list - val add_nontrivial_line : - term ATP_Proof.step -> term ATP_Proof.step list -> term ATP_Proof.step list - val forall_of : term -> term -> term - val raw_label_for_name : string * string list -> string * int - - val no_label : label - val indent_size : int - val reconstructor_command : - reconstructor -> int -> int -> string list -> int - -> (string * int) list * string list -> string - val repair_name : string -> string - val add_fact_from_dependency : - (string * 'a) list vector -> string * string list - -> (string * int) list * string list -> (string * int) list * string list - val kill_duplicate_assumptions_in_proof : isar_step list -> isar_step list - val kill_useless_labels_in_proof : isar_step list -> isar_step list - val relabel_proof : isar_step list -> isar_step list + Proof.context -> bool -> int Symtab.table -> + (string, string, (string, string) ho_term, string) formula -> term end; structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT = @@ -117,31 +41,7 @@ open ATP_Proof open ATP_Problem_Generate -structure String_Redirect = ATP_Proof_Redirect( - type key = step_name - val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') - val string_of = fst) - -open String_Redirect - -datatype reconstructor = - Metis of string * string | - SMT - -datatype play = - Played of reconstructor * Time.time | - Trust_Playable of reconstructor * Time.time option | - Failed_to_Play of reconstructor - -type minimize_command = string list -> string -type one_line_params = - play * string * (string * stature) list * minimize_command * int * int -type isar_params = - bool * int * string Symtab.table * (string * stature) list vector - * int Symtab.table * string proof * thm - val metisN = "metis" -val smtN = "smt" val full_typesN = "full_types" val partial_typesN = "partial_types" @@ -176,212 +76,14 @@ |> lam_trans <> metis_default_lam_trans ? cons lam_trans in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end -fun string_for_reconstructor (Metis (type_enc, lam_trans)) = - metis_call type_enc lam_trans - | string_for_reconstructor SMT = smtN - -fun find_first_in_list_vector vec key = - Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key - | (_, value) => value) NONE vec - -val unprefix_fact_number = space_implode "_" o tl o space_explode "_" - -fun resolve_one_named_fact fact_names s = - case try (unprefix fact_prefix) s of - SOME s' => - let val s' = s' |> unprefix_fact_number |> unascii_of in - s' |> find_first_in_list_vector fact_names |> Option.map (pair s') - end - | NONE => NONE -fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names) -fun is_fact fact_names = not o null o resolve_fact fact_names - -fun resolve_one_named_conjecture s = - case try (unprefix conjecture_prefix) s of - SOME s' => Int.fromString s' - | NONE => NONE - -val resolve_conjecture = map_filter resolve_one_named_conjecture -val is_conjecture = not o null o resolve_conjecture - -fun is_axiom_used_in_proof pred = - exists (fn Inference_Step ((_, ss), _, _, []) => exists pred ss | _ => false) - -val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix) - -val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix - -(* overapproximation (good enough) *) -fun is_lam_lifted s = - String.isPrefix fact_prefix s andalso - String.isSubstring ascii_of_lam_fact_prefix s - -fun lam_trans_from_atp_proof atp_proof default = - case (is_axiom_used_in_proof is_combinator_def atp_proof, - is_axiom_used_in_proof is_lam_lifted atp_proof) of - (false, false) => default - | (false, true) => liftingN -(* | (true, true) => combs_and_liftingN -- not supported by "metis" *) - | (true, _) => combsN - -val is_typed_helper_name = - String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix -fun is_typed_helper_used_in_atp_proof atp_proof = - is_axiom_used_in_proof is_typed_helper_name atp_proof - -val leo2_ext = "extcnf_equal_neg" -val leo2_unfold_def = "unfold_def" - -val isa_ext = Thm.get_name_hint @{thm ext} -val isa_short_ext = Long_Name.base_name isa_ext - -fun ext_name ctxt = - if Thm.eq_thm_prop (@{thm ext}, - singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then - isa_short_ext - else - isa_ext - -fun add_non_rec_defs fact_names accum = - Vector.foldl - (fn (facts, facts') => - union (op =) - (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) - facts') - accum fact_names - -fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) = - (if rule = leo2_ext then - insert (op =) (ext_name ctxt, (Global, General)) - else if rule = leo2_unfold_def then - (* LEO 1.3.3 does not record definitions properly, leading to missing - dependencies in the TSTP proof. Remove the next line once this is - fixed. *) - add_non_rec_defs fact_names - else if rule = satallax_coreN then - (fn [] => - (* Satallax doesn't include definitions in its unsatisfiable cores, - so we assume the worst and include them all here. *) - [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names - | facts => facts) - else - I) - #> (if null deps then union (op =) (resolve_fact fact_names ss) - else I) - | add_fact _ _ _ = I - -fun used_facts_in_atp_proof ctxt fact_names atp_proof = - if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names - else fold (add_fact ctxt fact_names) atp_proof [] - -fun used_facts_in_unsound_atp_proof _ _ [] = NONE - | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof = - let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in - if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso - not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then - SOME (map fst used_facts) - else - NONE - end - - -(** Soft-core proof reconstruction: one-liners **) - -fun string_for_label (s, num) = s ^ string_of_int num - -fun show_time NONE = "" - | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")" - -fun unusing_chained_facts _ 0 = "" - | unusing_chained_facts used_chaineds num_chained = - if length used_chaineds = num_chained then "" - else if null used_chaineds then "(* using no facts *) " - else "(* using only " ^ space_implode " " used_chaineds ^ " *) " - -fun apply_on_subgoal _ 1 = "by " - | apply_on_subgoal 1 _ = "apply " - | apply_on_subgoal i n = - "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n - -fun command_call name [] = - name |> not (Lexicon.is_identifier name) ? enclose "(" ")" - | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" - -fun try_command_line banner time command = - banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^ show_time time ^ "." - -fun using_labels [] = "" - | using_labels ls = - "using " ^ space_implode " " (map string_for_label ls) ^ " " - -fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) = - unusing_chained_facts used_chaineds num_chained ^ - using_labels ls ^ apply_on_subgoal i n ^ - command_call (string_for_reconstructor reconstr) ss - -fun minimize_line _ [] = "" - | minimize_line minimize_command ss = - case minimize_command ss of - "" => "" - | command => - "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "." - -fun split_used_facts facts = - facts |> List.partition (fn (_, (sc, _)) => sc = Chained) - |> pairself (sort_distinct (string_ord o pairself fst)) - -fun one_line_proof_text num_chained - (preplay, banner, used_facts, minimize_command, subgoal, - subgoal_count) = - let - val (chained, extra) = split_used_facts used_facts - val (failed, reconstr, ext_time) = - case preplay of - Played (reconstr, time) => (false, reconstr, (SOME (false, time))) - | Trust_Playable (reconstr, time) => - (false, reconstr, - case time of - NONE => NONE - | SOME time => - if time = Time.zeroTime then NONE else SOME (true, time)) - | Failed_to_Play reconstr => (true, reconstr, NONE) - val try_line = - ([], map fst extra) - |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) - num_chained - |> (if failed then - enclose "One-line proof reconstruction failed: " - ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \ - \solve this.)" - else - try_command_line banner ext_time) - in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end - -(** Hard-core proof reconstruction: structured Isar proofs **) - fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t -fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) fun make_tfree ctxt w = let val ww = "'" ^ w in TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end -val indent_size = 2 -val no_label = ("", ~1) - -val raw_prefix = "x" -val assum_prefix = "a" -val have_prefix = "f" - -fun raw_label_for_name (num, ss) = - case resolve_conjecture ss of - [j] => (conjecture_prefix, j) - | _ => (raw_prefix ^ ascii_of num, 0) - -(**** INTERPRETATION OF TSTP SYNTAX TREES ****) - exception HO_TERM of (string, string) ho_term list exception FORMULA of (string, string, (string, string) ho_term, string) formula list @@ -557,25 +259,6 @@ else pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u) -val combinator_table = - [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}), - (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}), - (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}), - (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}), - (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})] - -fun uncombine_term thy = - let - fun aux (t1 $ t2) = betapply (pairself aux (t1, t2)) - | aux (Abs (s, T, t')) = Abs (s, T, aux t') - | aux (t as Const (x as (s, _))) = - (case AList.lookup (op =) combinator_table s of - SOME thm => thm |> prop_of |> specialize_type thy x - |> Logic.dest_equals |> snd - | NONE => t) - | aux t = t - in aux end - (* Update schematic type variables with detected sort constraints. It's not totally clear whether this code is necessary. *) fun repair_tvar_sorts (t, tvar_tab) = @@ -608,10 +291,9 @@ | AQuant (q, (s, _) :: xs, phi') => do_formula pos (AQuant (q, xs, phi')) (* FIXME: TFF *) - #>> quantify_over_var (case q of - AForall => forall_of - | AExists => exists_of) - (s |> textual ? repair_variable_name Char.toLower) + #>> quantify_over_var + (case q of AForall => forall_of | AExists => exists_of) + (s |> textual ? repair_variable_name Char.toLower) | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not | AConn (c, [phi1, phi2]) => do_formula (pos |> c = AImplies ? not) phi1 @@ -626,253 +308,4 @@ | _ => raise FORMULA [phi] in repair_tvar_sorts (do_formula true phi Vartab.empty) end -fun infer_formula_types ctxt = - Type.constraint HOLogic.boolT - #> Syntax.check_term - (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) - -fun uncombined_etc_prop_from_atp ctxt textual sym_tab = - let val thy = Proof_Context.theory_of ctxt in - prop_from_atp ctxt textual sym_tab - #> textual ? uncombine_term thy #> infer_formula_types ctxt - end - -(**** Translation of TSTP files to Isar proofs ****) - -fun unvarify_term (Var ((s, 0), T)) = Free (s, T) - | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t]) - -fun decode_line sym_tab (Definition_Step (name, phi1, phi2)) ctxt = - let - val thy = Proof_Context.theory_of ctxt - val t1 = prop_from_atp ctxt true sym_tab phi1 - val vars = snd (strip_comb t1) - val frees = map unvarify_term vars - val unvarify_args = subst_atomic (vars ~~ frees) - val t2 = prop_from_atp ctxt true sym_tab phi2 - val (t1, t2) = - HOLogic.eq_const HOLogic.typeT $ t1 $ t2 - |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt - |> HOLogic.dest_eq - in - (Definition_Step (name, t1, t2), - fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt) - end - | decode_line sym_tab (Inference_Step (name, u, rule, deps)) ctxt = - let val t = u |> uncombined_etc_prop_from_atp ctxt true sym_tab in - (Inference_Step (name, t, rule, deps), - fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt) - end -fun decode_lines ctxt sym_tab lines = - fst (fold_map (decode_line sym_tab) lines ctxt) - -fun is_same_inference _ (Definition_Step _) = false - | is_same_inference t (Inference_Step (_, t', _, _)) = t aconv t' - -(* No "real" literals means only type information (tfree_tcs, clsrel, or - clsarity). *) -fun is_only_type_information t = t aconv @{term True} - -fun replace_one_dependency (old, new) dep = - if is_same_atp_step dep old then new else [dep] -fun replace_dependencies_in_line _ (line as Definition_Step _) = line - | replace_dependencies_in_line p (Inference_Step (name, t, rule, deps)) = - Inference_Step (name, t, rule, - fold (union (op =) o replace_one_dependency p) deps []) - -(* Discard facts; consolidate adjacent lines that prove the same formula, since - they differ only in type information.*) -fun add_line _ (line as Definition_Step _) lines = line :: lines - | add_line fact_names (Inference_Step (name as (_, ss), t, rule, [])) lines = - (* No dependencies: fact, conjecture, or (for Vampire) internal facts or - definitions. *) - if is_fact fact_names ss then - (* Facts are not proof lines. *) - if is_only_type_information t then - map (replace_dependencies_in_line (name, [])) lines - (* Is there a repetition? If so, replace later line by earlier one. *) - else case take_prefix (not o is_same_inference t) lines of - (_, []) => lines (* no repetition of proof line *) - | (pre, Inference_Step (name', _, _, _) :: post) => - pre @ map (replace_dependencies_in_line (name', [name])) post - | _ => raise Fail "unexpected inference" - else if is_conjecture ss then - Inference_Step (name, t, rule, []) :: lines - else - map (replace_dependencies_in_line (name, [])) lines - | add_line _ (Inference_Step (name, t, rule, deps)) lines = - (* Type information will be deleted later; skip repetition test. *) - if is_only_type_information t then - Inference_Step (name, t, rule, deps) :: lines - (* Is there a repetition? If so, replace later line by earlier one. *) - else case take_prefix (not o is_same_inference t) lines of - (* FIXME: Doesn't this code risk conflating proofs involving different - types? *) - (_, []) => Inference_Step (name, t, rule, deps) :: lines - | (pre, Inference_Step (name', t', rule, _) :: post) => - Inference_Step (name, t', rule, deps) :: - pre @ map (replace_dependencies_in_line (name', [name])) post - | _ => raise Fail "unexpected inference" - -val waldmeister_conjecture_num = "1.0.0.0" - -val repair_waldmeister_endgame = - let - fun do_tail (Inference_Step (name, t, rule, deps)) = - Inference_Step (name, s_not t, rule, deps) - | do_tail line = line - fun do_body [] = [] - | do_body ((line as Inference_Step ((num, _), _, _, _)) :: lines) = - if num = waldmeister_conjecture_num then map do_tail (line :: lines) - else line :: do_body lines - | do_body (line :: lines) = line :: do_body lines - in do_body end - -(* Recursively delete empty lines (type information) from the proof. *) -fun add_nontrivial_line (line as Inference_Step (name, t, _, [])) lines = - if is_only_type_information t then delete_dependency name lines - else line :: lines - | add_nontrivial_line line lines = line :: lines -and delete_dependency name lines = - fold_rev add_nontrivial_line - (map (replace_dependencies_in_line (name, [])) lines) [] - -(* ATPs sometimes reuse free variable names in the strangest ways. Removing - offending lines often does the trick. *) -fun is_bad_free frees (Free x) = not (member (op =) frees x) - | is_bad_free _ _ = false - -fun add_desired_line _ _ _ (line as Definition_Step (name, _, _)) (j, lines) = - (j, line :: map (replace_dependencies_in_line (name, [])) lines) - | add_desired_line isar_shrink_factor fact_names frees - (Inference_Step (name as (_, ss), t, rule, deps)) (j, lines) = - (j + 1, - if is_fact fact_names ss orelse - is_conjecture ss orelse - (* the last line must be kept *) - j = 0 orelse - (not (is_only_type_information t) andalso - null (Term.add_tvars t []) andalso - not (exists_subterm (is_bad_free frees) t) andalso - length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso - (* kill next to last line, which usually results in a trivial step *) - j <> 1) then - Inference_Step (name, t, rule, deps) :: lines (* keep line *) - else - map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) - -(** Isar proof construction and manipulation **) - -type label = string * int -type facts = label list * string list - -datatype isar_qualifier = Show | Then | Moreover | Ultimately - -datatype isar_step = - Fix of (string * typ) list | - Let of term * term | - Assume of label * term | - Prove of isar_qualifier list * label * term * byline -and byline = - By_Metis of facts | - Case_Split of isar_step list list * facts - -fun add_fact_from_dependency fact_names (name as (_, ss)) = - if is_fact fact_names ss then - apsnd (union (op =) (map fst (resolve_fact fact_names ss))) - else - apfst (insert (op =) (raw_label_for_name name)) - -fun repair_name "$true" = "c_True" - | repair_name "$false" = "c_False" - | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *) - | repair_name s = - if is_tptp_equal s orelse - (* seen in Vampire proofs *) - (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then - tptp_equal - else - s - -(* FIXME: Still needed? Try with SPASS proofs perhaps. *) -val kill_duplicate_assumptions_in_proof = - let - fun relabel_facts subst = - apfst (map (fn l => AList.lookup (op =) subst l |> the_default l)) - fun do_step (step as Assume (l, t)) (proof, subst, assums) = - (case AList.lookup (op aconv) assums t of - SOME l' => (proof, (l, l') :: subst, assums) - | NONE => (step :: proof, subst, (t, l) :: assums)) - | do_step (Prove (qs, l, t, by)) (proof, subst, assums) = - (Prove (qs, l, t, - case by of - By_Metis facts => By_Metis (relabel_facts subst facts) - | Case_Split (proofs, facts) => - Case_Split (map do_proof proofs, - relabel_facts subst facts)) :: - proof, subst, assums) - | do_step step (proof, subst, assums) = (step :: proof, subst, assums) - and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev - in do_proof end - -fun used_labels_of_step (Prove (_, _, _, by)) = - (case by of - By_Metis (ls, _) => ls - | Case_Split (proofs, (ls, _)) => - fold (union (op =) o used_labels_of) proofs ls) - | used_labels_of_step _ = [] -and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] - -fun kill_useless_labels_in_proof proof = - let - val used_ls = used_labels_of proof - fun do_label l = if member (op =) used_ls l then l else no_label - fun do_step (Assume (l, t)) = Assume (do_label l, t) - | do_step (Prove (qs, l, t, by)) = - Prove (qs, do_label l, t, - case by of - Case_Split (proofs, facts) => - Case_Split (map (map do_step) proofs, facts) - | _ => by) - | do_step step = step - in map do_step proof end - -fun prefix_for_depth n = replicate_string (n + 1) - -val relabel_proof = - let - fun aux _ _ _ [] = [] - | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) = - if l = no_label then - Assume (l, t) :: aux subst depth (next_assum, next_fact) proof - else - let val l' = (prefix_for_depth depth assum_prefix, next_assum) in - Assume (l', t) :: - aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof - end - | aux subst depth (next_assum, next_fact) - (Prove (qs, l, t, by) :: proof) = - let - val (l', subst, next_fact) = - if l = no_label then - (l, subst, next_fact) - else - let - val l' = (prefix_for_depth depth have_prefix, next_fact) - in (l', (l, l') :: subst, next_fact + 1) end - val relabel_facts = - apfst (maps (the_list o AList.lookup (op =) subst)) - val by = - case by of - By_Metis facts => By_Metis (relabel_facts facts) - | Case_Split (proofs, facts) => - Case_Split (map (aux subst (depth + 1) (1, 1)) proofs, - relabel_facts facts) - in - Prove (qs, l', t, by) :: aux subst depth (next_assum, next_fact) proof - end - | aux subst depth nextp (step :: proof) = - step :: aux subst depth nextp proof - in aux [] 0 (1, 1) end - end; diff -r 2e7d0655b176 -r 23e36a4d28f1 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 18 11:59:45 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 18 13:19:44 2012 +0200 @@ -8,7 +8,7 @@ signature SLEDGEHAMMER_MINIMIZE = sig type stature = ATP_Problem_Generate.stature - type play = ATP_Proof_Reconstruct.play + type play = Sledgehammer_Reconstruct.play type mode = Sledgehammer_Provers.mode type params = Sledgehammer_Provers.params type prover = Sledgehammer_Provers.prover @@ -34,9 +34,9 @@ open ATP_Util open ATP_Proof open ATP_Problem_Generate -open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Fact +open Sledgehammer_Reconstruct open Sledgehammer_Provers (* wrapper for calling external prover *) diff -r 2e7d0655b176 -r 23e36a4d28f1 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Oct 18 11:59:45 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Oct 18 13:19:44 2012 +0200 @@ -11,9 +11,9 @@ type failure = ATP_Proof.failure type stature = ATP_Problem_Generate.stature type type_enc = ATP_Problem_Generate.type_enc - type reconstructor = ATP_Proof_Reconstruct.reconstructor - type play = ATP_Proof_Reconstruct.play - type minimize_command = ATP_Proof_Reconstruct.minimize_command + type reconstructor = Sledgehammer_Reconstruct.reconstructor + type play = Sledgehammer_Reconstruct.play + type minimize_command = Sledgehammer_Reconstruct.minimize_command datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize diff -r 2e7d0655b176 -r 23e36a4d28f1 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 18 11:59:45 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 18 13:19:44 2012 +0200 @@ -2,12 +2,41 @@ Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen +Isar proof reconstruction from ATP proofs. *) signature SLEDGEHAMMER_PROOF_RECONSTRUCT = sig - type isar_params = ATP_Proof_Reconstruct.isar_params - type one_line_params = ATP_Proof_Reconstruct.one_line_params + type 'a proof = 'a ATP_Proof.proof + type stature = ATP_Problem_Generate.stature + + datatype reconstructor = + Metis of string * string | + SMT + + datatype play = + Played of reconstructor * Time.time | + Trust_Playable of reconstructor * Time.time option | + Failed_to_Play of reconstructor + + type minimize_command = string list -> string + type one_line_params = + play * string * (string * stature) list * minimize_command * int * int + type isar_params = + bool * int * string Symtab.table * (string * stature) list vector + * int Symtab.table * string proof * thm + + val smtN : string + val string_for_reconstructor : reconstructor -> string + val lam_trans_from_atp_proof : string proof -> string -> string + val is_typed_helper_used_in_atp_proof : string proof -> bool + val used_facts_in_atp_proof : + Proof.context -> (string * stature) list vector -> string proof -> + (string * stature) list + val used_facts_in_unsound_atp_proof : + Proof.context -> (string * stature) list vector -> 'a proof -> + string list option + val one_line_proof_text : int -> one_line_params -> string val isar_proof_text : Proof.context -> bool -> isar_params -> one_line_params -> string val proof_text : @@ -18,11 +47,411 @@ struct open ATP_Util +open ATP_Problem open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct + +structure String_Redirect = ATP_Proof_Redirect( + type key = step_name + val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') + val string_of = fst) + open String_Redirect +(** reconstructors **) + +datatype reconstructor = + Metis of string * string | + SMT + +datatype play = + Played of reconstructor * Time.time | + Trust_Playable of reconstructor * Time.time option | + Failed_to_Play of reconstructor + +val smtN = "smt" + +fun string_for_reconstructor (Metis (type_enc, lam_trans)) = + metis_call type_enc lam_trans + | string_for_reconstructor SMT = smtN + + +(** fact extraction from ATP proofs **) + +fun find_first_in_list_vector vec key = + Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key + | (_, value) => value) NONE vec + +val unprefix_fact_number = space_implode "_" o tl o space_explode "_" + +fun resolve_one_named_fact fact_names s = + case try (unprefix fact_prefix) s of + SOME s' => + let val s' = s' |> unprefix_fact_number |> unascii_of in + s' |> find_first_in_list_vector fact_names |> Option.map (pair s') + end + | NONE => NONE +fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names) +fun is_fact fact_names = not o null o resolve_fact fact_names + +fun resolve_one_named_conjecture s = + case try (unprefix conjecture_prefix) s of + SOME s' => Int.fromString s' + | NONE => NONE + +val resolve_conjecture = map_filter resolve_one_named_conjecture +val is_conjecture = not o null o resolve_conjecture + +val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix + +(* overapproximation (good enough) *) +fun is_lam_lifted s = + String.isPrefix fact_prefix s andalso + String.isSubstring ascii_of_lam_fact_prefix s + +val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix) + +fun is_axiom_used_in_proof pred = + exists (fn Inference_Step ((_, ss), _, _, []) => exists pred ss | _ => false) + +fun lam_trans_from_atp_proof atp_proof default = + case (is_axiom_used_in_proof is_combinator_def atp_proof, + is_axiom_used_in_proof is_lam_lifted atp_proof) of + (false, false) => default + | (false, true) => liftingN +(* | (true, true) => combs_and_liftingN -- not supported by "metis" *) + | (true, _) => combsN + +val is_typed_helper_name = + String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix +fun is_typed_helper_used_in_atp_proof atp_proof = + is_axiom_used_in_proof is_typed_helper_name atp_proof + +fun add_non_rec_defs fact_names accum = + Vector.foldl (fn (facts, facts') => + union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) + facts') + accum fact_names + +val isa_ext = Thm.get_name_hint @{thm ext} +val isa_short_ext = Long_Name.base_name isa_ext + +fun ext_name ctxt = + if Thm.eq_thm_prop (@{thm ext}, + singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then + isa_short_ext + else + isa_ext + +val leo2_ext = "extcnf_equal_neg" +val leo2_unfold_def = "unfold_def" + +fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) = + (if rule = leo2_ext then + insert (op =) (ext_name ctxt, (Global, General)) + else if rule = leo2_unfold_def then + (* LEO 1.3.3 does not record definitions properly, leading to missing + dependencies in the TSTP proof. Remove the next line once this is + fixed. *) + add_non_rec_defs fact_names + else if rule = satallax_coreN then + (fn [] => + (* Satallax doesn't include definitions in its unsatisfiable cores, + so we assume the worst and include them all here. *) + [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names + | facts => facts) + else + I) + #> (if null deps then union (op =) (resolve_fact fact_names ss) + else I) + | add_fact _ _ _ = I + +fun used_facts_in_atp_proof ctxt fact_names atp_proof = + if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names + else fold (add_fact ctxt fact_names) atp_proof [] + +fun used_facts_in_unsound_atp_proof _ _ [] = NONE + | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof = + let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in + if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso + not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then + SOME (map fst used_facts) + else + NONE + end + + +(** one-liner reconstructor proofs **) + +fun string_for_label (s, num) = s ^ string_of_int num + +fun show_time NONE = "" + | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")" + +fun unusing_chained_facts _ 0 = "" + | unusing_chained_facts used_chaineds num_chained = + if length used_chaineds = num_chained then "" + else if null used_chaineds then "(* using no facts *) " + else "(* using only " ^ space_implode " " used_chaineds ^ " *) " + +fun apply_on_subgoal _ 1 = "by " + | apply_on_subgoal 1 _ = "apply " + | apply_on_subgoal i n = + "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n + +fun using_labels [] = "" + | using_labels ls = + "using " ^ space_implode " " (map string_for_label ls) ^ " " + +fun command_call name [] = + name |> not (Lexicon.is_identifier name) ? enclose "(" ")" + | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" + +fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) = + unusing_chained_facts used_chaineds num_chained ^ + using_labels ls ^ apply_on_subgoal i n ^ + command_call (string_for_reconstructor reconstr) ss + +fun try_command_line banner time command = + banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^ + show_time time ^ "." + +fun minimize_line _ [] = "" + | minimize_line minimize_command ss = + case minimize_command ss of + "" => "" + | command => + "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "." + +fun split_used_facts facts = + facts |> List.partition (fn (_, (sc, _)) => sc = Chained) + |> pairself (sort_distinct (string_ord o pairself fst)) + +type minimize_command = string list -> string +type one_line_params = + play * string * (string * stature) list * minimize_command * int * int + +fun one_line_proof_text num_chained + (preplay, banner, used_facts, minimize_command, subgoal, + subgoal_count) = + let + val (chained, extra) = split_used_facts used_facts + val (failed, reconstr, ext_time) = + case preplay of + Played (reconstr, time) => (false, reconstr, (SOME (false, time))) + | Trust_Playable (reconstr, time) => + (false, reconstr, + case time of + NONE => NONE + | SOME time => + if time = Time.zeroTime then NONE else SOME (true, time)) + | Failed_to_Play reconstr => (true, reconstr, NONE) + val try_line = + ([], map fst extra) + |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) + num_chained + |> (if failed then + enclose "One-line proof reconstruction failed: " + ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \ + \solve this.)" + else + try_command_line banner ext_time) + in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end + + +(** Isar proof construction and manipulation **) + +type label = string * int +type facts = label list * string list + +datatype isar_qualifier = Show | Then | Moreover | Ultimately + +datatype isar_step = + Fix of (string * typ) list | + Let of term * term | + Assume of label * term | + Prove of isar_qualifier list * label * term * byline +and byline = + By_Metis of facts | + Case_Split of isar_step list list * facts + +val assum_prefix = "a" +val have_prefix = "f" +val raw_prefix = "x" + +fun raw_label_for_name (num, ss) = + case resolve_conjecture ss of + [j] => (conjecture_prefix, j) + | _ => (raw_prefix ^ ascii_of num, 0) + +fun add_fact_from_dependency fact_names (name as (_, ss)) = + if is_fact fact_names ss then + apsnd (union (op =) (map fst (resolve_fact fact_names ss))) + else + apfst (insert (op =) (raw_label_for_name name)) + +fun repair_name "$true" = "c_True" + | repair_name "$false" = "c_False" + | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *) + | repair_name s = + if is_tptp_equal s orelse + (* seen in Vampire proofs *) + (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then + tptp_equal + else + s + +fun unvarify_term (Var ((s, 0), T)) = Free (s, T) + | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t]) + +fun infer_formula_types ctxt = + Type.constraint HOLogic.boolT + #> Syntax.check_term + (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) + +val combinator_table = + [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}), + (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}), + (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}), + (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}), + (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})] + +fun uncombine_term thy = + let + fun aux (t1 $ t2) = betapply (pairself aux (t1, t2)) + | aux (Abs (s, T, t')) = Abs (s, T, aux t') + | aux (t as Const (x as (s, _))) = + (case AList.lookup (op =) combinator_table s of + SOME thm => thm |> prop_of |> specialize_type thy x + |> Logic.dest_equals |> snd + | NONE => t) + | aux t = t + in aux end + +fun decode_line sym_tab (Definition_Step (name, phi1, phi2)) ctxt = + let + val thy = Proof_Context.theory_of ctxt + val t1 = prop_from_atp ctxt true sym_tab phi1 + val vars = snd (strip_comb t1) + val frees = map unvarify_term vars + val unvarify_args = subst_atomic (vars ~~ frees) + val t2 = prop_from_atp ctxt true sym_tab phi2 + val (t1, t2) = + HOLogic.eq_const HOLogic.typeT $ t1 $ t2 + |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt + |> HOLogic.dest_eq + in + (Definition_Step (name, t1, t2), + fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt) + end + | decode_line sym_tab (Inference_Step (name, u, rule, deps)) ctxt = + let + val thy = Proof_Context.theory_of ctxt + val t = u |> prop_from_atp ctxt true sym_tab + |> uncombine_term thy |> infer_formula_types ctxt + in + (Inference_Step (name, t, rule, deps), + fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt) + end +fun decode_lines ctxt sym_tab lines = + fst (fold_map (decode_line sym_tab) lines ctxt) + +fun replace_one_dependency (old, new) dep = + if is_same_atp_step dep old then new else [dep] +fun replace_dependencies_in_line _ (line as Definition_Step _) = line + | replace_dependencies_in_line p (Inference_Step (name, t, rule, deps)) = + Inference_Step (name, t, rule, + fold (union (op =) o replace_one_dependency p) deps []) + +(* No "real" literals means only type information (tfree_tcs, clsrel, or + clsarity). *) +fun is_only_type_information t = t aconv @{term True} + +fun is_same_inference _ (Definition_Step _) = false + | is_same_inference t (Inference_Step (_, t', _, _)) = t aconv t' + +(* Discard facts; consolidate adjacent lines that prove the same formula, since + they differ only in type information.*) +fun add_line _ (line as Definition_Step _) lines = line :: lines + | add_line fact_names (Inference_Step (name as (_, ss), t, rule, [])) lines = + (* No dependencies: fact, conjecture, or (for Vampire) internal facts or + definitions. *) + if is_fact fact_names ss then + (* Facts are not proof lines. *) + if is_only_type_information t then + map (replace_dependencies_in_line (name, [])) lines + (* Is there a repetition? If so, replace later line by earlier one. *) + else case take_prefix (not o is_same_inference t) lines of + (_, []) => lines (* no repetition of proof line *) + | (pre, Inference_Step (name', _, _, _) :: post) => + pre @ map (replace_dependencies_in_line (name', [name])) post + | _ => raise Fail "unexpected inference" + else if is_conjecture ss then + Inference_Step (name, t, rule, []) :: lines + else + map (replace_dependencies_in_line (name, [])) lines + | add_line _ (Inference_Step (name, t, rule, deps)) lines = + (* Type information will be deleted later; skip repetition test. *) + if is_only_type_information t then + Inference_Step (name, t, rule, deps) :: lines + (* Is there a repetition? If so, replace later line by earlier one. *) + else case take_prefix (not o is_same_inference t) lines of + (* FIXME: Doesn't this code risk conflating proofs involving different + types? *) + (_, []) => Inference_Step (name, t, rule, deps) :: lines + | (pre, Inference_Step (name', t', rule, _) :: post) => + Inference_Step (name, t', rule, deps) :: + pre @ map (replace_dependencies_in_line (name', [name])) post + | _ => raise Fail "unexpected inference" + +val waldmeister_conjecture_num = "1.0.0.0" + +val repair_waldmeister_endgame = + let + fun do_tail (Inference_Step (name, t, rule, deps)) = + Inference_Step (name, s_not t, rule, deps) + | do_tail line = line + fun do_body [] = [] + | do_body ((line as Inference_Step ((num, _), _, _, _)) :: lines) = + if num = waldmeister_conjecture_num then map do_tail (line :: lines) + else line :: do_body lines + | do_body (line :: lines) = line :: do_body lines + in do_body end + +(* Recursively delete empty lines (type information) from the proof. *) +fun add_nontrivial_line (line as Inference_Step (name, t, _, [])) lines = + if is_only_type_information t then delete_dependency name lines + else line :: lines + | add_nontrivial_line line lines = line :: lines +and delete_dependency name lines = + fold_rev add_nontrivial_line + (map (replace_dependencies_in_line (name, [])) lines) [] + +(* ATPs sometimes reuse free variable names in the strangest ways. Removing + offending lines often does the trick. *) +fun is_bad_free frees (Free x) = not (member (op =) frees x) + | is_bad_free _ _ = false + +fun add_desired_line _ _ _ (line as Definition_Step (name, _, _)) (j, lines) = + (j, line :: map (replace_dependencies_in_line (name, [])) lines) + | add_desired_line isar_shrink_factor fact_names frees + (Inference_Step (name as (_, ss), t, rule, deps)) (j, lines) = + (j + 1, + if is_fact fact_names ss orelse + is_conjecture ss orelse + (* the last line must be kept *) + j = 0 orelse + (not (is_only_type_information t) andalso + null (Term.add_tvars t []) andalso + not (exists_subterm (is_bad_free frees) t) andalso + length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso + (* kill next to last line, which usually results in a trivial step *) + j <> 1) then + Inference_Step (name, t, rule, deps) :: lines (* keep line *) + else + map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) + (** Type annotations **) fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s @@ -165,6 +594,9 @@ |> sort int_ord in introduce_annotations thy typing_spots t t' end +val indent_size = 2 +val no_label = ("", ~1) + fun string_for_proof ctxt type_enc lam_trans i n = let fun fix_print_mode f x = @@ -221,6 +653,87 @@ (if n <> 1 then "next" else "qed") in do_proof end +(* FIXME: Still needed? Try with SPASS proofs perhaps. *) +val kill_duplicate_assumptions_in_proof = + let + fun relabel_facts subst = + apfst (map (fn l => AList.lookup (op =) subst l |> the_default l)) + fun do_step (step as Assume (l, t)) (proof, subst, assums) = + (case AList.lookup (op aconv) assums t of + SOME l' => (proof, (l, l') :: subst, assums) + | NONE => (step :: proof, subst, (t, l) :: assums)) + | do_step (Prove (qs, l, t, by)) (proof, subst, assums) = + (Prove (qs, l, t, + case by of + By_Metis facts => By_Metis (relabel_facts subst facts) + | Case_Split (proofs, facts) => + Case_Split (map do_proof proofs, + relabel_facts subst facts)) :: + proof, subst, assums) + | do_step step (proof, subst, assums) = (step :: proof, subst, assums) + and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev + in do_proof end + +fun used_labels_of_step (Prove (_, _, _, by)) = + (case by of + By_Metis (ls, _) => ls + | Case_Split (proofs, (ls, _)) => + fold (union (op =) o used_labels_of) proofs ls) + | used_labels_of_step _ = [] +and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] + +fun kill_useless_labels_in_proof proof = + let + val used_ls = used_labels_of proof + fun do_label l = if member (op =) used_ls l then l else no_label + fun do_step (Assume (l, t)) = Assume (do_label l, t) + | do_step (Prove (qs, l, t, by)) = + Prove (qs, do_label l, t, + case by of + Case_Split (proofs, facts) => + Case_Split (map (map do_step) proofs, facts) + | _ => by) + | do_step step = step + in map do_step proof end + +fun prefix_for_depth n = replicate_string (n + 1) + +val relabel_proof = + let + fun aux _ _ _ [] = [] + | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) = + if l = no_label then + Assume (l, t) :: aux subst depth (next_assum, next_fact) proof + else + let val l' = (prefix_for_depth depth assum_prefix, next_assum) in + Assume (l', t) :: + aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof + end + | aux subst depth (next_assum, next_fact) + (Prove (qs, l, t, by) :: proof) = + let + val (l', subst, next_fact) = + if l = no_label then + (l, subst, next_fact) + else + let + val l' = (prefix_for_depth depth have_prefix, next_fact) + in (l', (l, l') :: subst, next_fact + 1) end + val relabel_facts = + apfst (maps (the_list o AList.lookup (op =) subst)) + val by = + case by of + By_Metis facts => By_Metis (relabel_facts facts) + | Case_Split (proofs, facts) => + Case_Split (map (aux subst (depth + 1) (1, 1)) proofs, + relabel_facts facts) + in + Prove (qs, l', t, by) :: aux subst depth (next_assum, next_fact) proof + end + | aux subst depth nextp (step :: proof) = + step :: aux subst depth nextp proof + in aux [] 0 (1, 1) end + fun minimize_locally ctxt type_enc lam_trans proof = let (* Merging spots, greedy algorithm *) @@ -305,6 +818,10 @@ merge_steps proof' (map (fn j => if j > i then j - 1 else j) is) in merge_steps proof merge_spots end +type isar_params = + bool * int * string Symtab.table * (string * stature) list vector + * int Symtab.table * string proof * thm + fun isar_proof_text ctxt isar_proof_requested (debug, isar_shrink_factor, pool, fact_names, sym_tab, atp_proof, goal) (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = diff -r 2e7d0655b176 -r 23e36a4d28f1 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Oct 18 11:59:45 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Oct 18 13:19:44 2012 +0200 @@ -8,8 +8,8 @@ signature SLEDGEHAMMER_RUN = sig - type minimize_command = ATP_Proof_Reconstruct.minimize_command type fact_override = Sledgehammer_Fact.fact_override + type minimize_command = Sledgehammer_Reconstruct.minimize_command type mode = Sledgehammer_Provers.mode type params = Sledgehammer_Provers.params