simplified code
authorblanchet
Mon Jun 16 19:40:59 2014 +0200 (2014-06-16)
changeset 572632b6a96cc64c9
parent 57262 b2c629647a14
child 57264 13db1d078743
simplified code
src/HOL/ATP.thy
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/Metis/metis_generate.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
     1.1 --- a/src/HOL/ATP.thy	Mon Jun 16 19:40:04 2014 +0200
     1.2 +++ b/src/HOL/ATP.thy	Mon Jun 16 19:40:59 2014 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  imports Meson
     1.5  begin
     1.6  
     1.7 -ML_file "Tools/lambda_lifting.ML"
     1.8 -ML_file "Tools/monomorph.ML"
     1.9 +subsection {* ATP problems and proofs *}
    1.10 +
    1.11  ML_file "Tools/ATP/atp_util.ML"
    1.12  ML_file "Tools/ATP/atp_problem.ML"
    1.13  ML_file "Tools/ATP/atp_proof.ML"
    1.14 @@ -137,8 +137,10 @@
    1.15    eq_ac disj_comms disj_assoc conj_comms conj_assoc
    1.16  
    1.17  
    1.18 -subsection {* Setup *}
    1.19 +subsection {* Basic connection between ATPs and HOL *}
    1.20  
    1.21 +ML_file "Tools/lambda_lifting.ML"
    1.22 +ML_file "Tools/monomorph.ML"
    1.23  ML_file "Tools/ATP/atp_problem_generate.ML"
    1.24  ML_file "Tools/ATP/atp_proof_reconstruct.ML"
    1.25  ML_file "Tools/ATP/atp_systems.ML"
     2.1 --- a/src/HOL/Sledgehammer.thy	Mon Jun 16 19:40:04 2014 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Mon Jun 16 19:40:59 2014 +0200
     2.3 @@ -33,4 +33,8 @@
     2.4  ML_file "Tools/Sledgehammer/sledgehammer.ML"
     2.5  ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
     2.6  
     2.7 +lemma "1 + 1 = (2::nat)"
     2.8 +sledgehammer [vampire, max_facts = 3]
     2.9 +oops
    2.10 +
    2.11  end
     3.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jun 16 19:40:04 2014 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jun 16 19:40:59 2014 +0200
     3.3 @@ -110,12 +110,9 @@
     3.4      Proof.context -> type_enc -> string -> term list -> term list * term list
     3.5    val string_of_status : status -> string
     3.6    val factsN : string
     3.7 -  val prepare_atp_problem :
     3.8 -    Proof.context -> atp_format -> atp_formula_role -> type_enc -> mode
     3.9 -    -> string -> bool -> bool -> bool -> term list -> term
    3.10 -    -> ((string * stature) * term) list
    3.11 -    -> string atp_problem * string Symtab.table * (string * stature) list vector
    3.12 -       * (string * term) list * int Symtab.table
    3.13 +  val generate_atp_problem : Proof.context -> atp_format -> atp_formula_role -> type_enc -> mode ->
    3.14 +    string -> bool -> bool -> bool -> term list -> term -> ((string * stature) * term) list ->
    3.15 +    string atp_problem * string Symtab.table * (string * term) list * int Symtab.table
    3.16    val atp_problem_selection_weights : string atp_problem -> (string * real) list
    3.17    val atp_problem_term_order_info : string atp_problem -> (string * int) list
    3.18  end;
    3.19 @@ -1279,8 +1276,7 @@
    3.20        iformula_of_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t []
    3.21        |>> close_universally add_iterm_vars
    3.22    in
    3.23 -    {name = name, stature = stature, role = role, iformula = iformula,
    3.24 -     atomic_types = atomic_Ts}
    3.25 +    {name = name, stature = stature, role = role, iformula = iformula, atomic_types = atomic_Ts}
    3.26    end
    3.27  
    3.28  fun is_format_with_defs (THF _) = true
    3.29 @@ -1295,7 +1291,7 @@
    3.30        else
    3.31          Axiom
    3.32    in
    3.33 -    (case t |> make_formula ctxt format type_enc iff_for_eq name stature role of
    3.34 +    (case make_formula ctxt format type_enc iff_for_eq name stature role t of
    3.35        formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
    3.36        if s = tptp_true then NONE else SOME formula
    3.37      | formula => SOME formula)
    3.38 @@ -1303,13 +1299,10 @@
    3.39  
    3.40  fun make_conjecture ctxt format type_enc =
    3.41    map (fn ((name, stature), (role, t)) =>
    3.42 -          let
    3.43 -            val role =
    3.44 -              if role <> Conjecture andalso is_legitimate_tptp_def t then Definition else role
    3.45 -          in
    3.46 -            t |> role = Conjecture ? s_not
    3.47 -              |> make_formula ctxt format type_enc true name stature role
    3.48 -          end)
    3.49 +    let
    3.50 +      val role' = if role <> Conjecture andalso is_legitimate_tptp_def t then Definition else role
    3.51 +      val t' = t |> role' = Conjecture ? s_not
    3.52 +    in make_formula ctxt format type_enc true name stature role' t' end)
    3.53  
    3.54  (** Finite and infinite type inference **)
    3.55  
    3.56 @@ -1907,10 +1900,8 @@
    3.57        conjs |> make_conjecture ctxt format type_enc
    3.58              |> pull_and_reorder_definitions
    3.59      val facts =
    3.60 -      facts |> map_filter (fn (name, (_, t)) =>
    3.61 -                              make_fact ctxt format type_enc true (name, t))
    3.62 +      facts |> map_filter (fn (name, (_, t)) => make_fact ctxt format type_enc true (name, t))
    3.63              |> pull_and_reorder_definitions
    3.64 -    val fact_names = facts |> map (fn {name, stature, ...} : ifact => (name, stature))
    3.65      val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
    3.66      val lam_facts = lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
    3.67      val all_ts = concl_t :: hyp_ts @ fact_ts
    3.68 @@ -1922,8 +1913,7 @@
    3.69        else make_tcon_clauses thy tycons supers
    3.70      val subclass_pairs = make_subclass_pairs thy subs supers
    3.71    in
    3.72 -    (fact_names |> map single, union (op =) subs supers, conjs,
    3.73 -     facts @ lam_facts, subclass_pairs, tcon_clauses, lifted)
    3.74 +    (union (op =) subs supers, conjs, facts @ lam_facts, subclass_pairs, tcon_clauses, lifted)
    3.75    end
    3.76  
    3.77  val type_guard = `(make_fixed_const NONE) type_guard_name
    3.78 @@ -2616,7 +2606,7 @@
    3.79  
    3.80  val app_op_and_predicator_threshold = 45
    3.81  
    3.82 -fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases
    3.83 +fun generate_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases
    3.84      readable_names presimp hyp_ts concl_t facts =
    3.85    let
    3.86      val thy = Proof_Context.theory_of ctxt
    3.87 @@ -2636,7 +2626,7 @@
    3.88      val lam_trans =
    3.89        if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN
    3.90        else lam_trans
    3.91 -    val (fact_names, classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
    3.92 +    val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
    3.93        translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts
    3.94      val (_, sym_tab0) = sym_table_of_facts ctxt type_enc app_op_level conjs facts
    3.95      val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish
    3.96 @@ -2700,8 +2690,8 @@
    3.97      val (problem, pool) = problem |> nice_atp_problem readable_names format
    3.98      fun add_sym_ary (s, {min_ary, ...} : sym_info) = min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
    3.99    in
   3.100 -    (problem, pool |> Option.map snd |> the_default Symtab.empty, fact_names |> Vector.fromList,
   3.101 -     lifted, Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
   3.102 +    (problem, Option.map snd pool |> the_default Symtab.empty, lifted,
   3.103 +     Symtab.fold add_sym_ary sym_tab Symtab.empty)
   3.104    end
   3.105  
   3.106  (* FUDGE *)
     4.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jun 16 19:40:04 2014 +0200
     4.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jun 16 19:40:59 2014 +0200
     4.3 @@ -38,10 +38,10 @@
     4.4      bool -> int Symtab.table ->
     4.5      (string, string, (string, string atp_type) atp_term, string) atp_formula -> term
     4.6  
     4.7 -  val used_facts_in_atp_proof :
     4.8 -    Proof.context -> (string * stature) list vector -> string atp_proof -> (string * stature) list
     4.9 -  val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list vector ->
    4.10 -    'a atp_proof -> string list option
    4.11 +  val used_facts_in_atp_proof : Proof.context -> (string * stature) list -> string atp_proof ->
    4.12 +    (string * stature) list
    4.13 +  val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list -> 'a atp_proof ->
    4.14 +    string list option
    4.15    val atp_proof_prefers_lifting : string atp_proof -> bool
    4.16    val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
    4.17    val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step ->
    4.18 @@ -50,8 +50,8 @@
    4.19      ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list ->
    4.20      int Symtab.table -> string atp_proof -> (term, string) atp_step list
    4.21    val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list
    4.22 -  val factify_atp_proof : (string * 'a) list vector -> term list -> term ->
    4.23 -    (term, string) atp_step list -> (term, string) atp_step list
    4.24 +  val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list ->
    4.25 +    (term, string) atp_step list
    4.26  end;
    4.27  
    4.28  structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =
    4.29 @@ -452,66 +452,58 @@
    4.30      repair_tvar_sorts (do_formula true phi Vartab.empty)
    4.31    end
    4.32  
    4.33 -fun find_first_in_list_vector vec key =
    4.34 -  Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
    4.35 -                 | (_, value) => value) NONE vec
    4.36 -
    4.37  val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
    4.38  
    4.39 -fun resolve_one_named_fact fact_names s =
    4.40 +fun resolve_fact facts s =
    4.41    (case try (unprefix fact_prefix) s of
    4.42      SOME s' =>
    4.43      let val s' = s' |> unprefix_fact_number |> unascii_of in
    4.44 -      s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
    4.45 +      AList.lookup (op =) facts s' |> Option.map (pair s')
    4.46      end
    4.47    | NONE => NONE)
    4.48  
    4.49 -fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)
    4.50 -
    4.51 -fun resolve_one_named_conjecture s =
    4.52 +fun resolve_conjecture s =
    4.53    (case try (unprefix conjecture_prefix) s of
    4.54      SOME s' => Int.fromString s'
    4.55    | NONE => NONE)
    4.56  
    4.57 -val resolve_conjecture = map_filter resolve_one_named_conjecture
    4.58 +fun resolve_facts facts = map_filter (resolve_fact facts)
    4.59 +val resolve_conjectures = map_filter resolve_conjecture
    4.60  
    4.61  fun is_axiom_used_in_proof pred =
    4.62    exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
    4.63  
    4.64 -fun add_non_rec_defs fact_names accum =
    4.65 -  Vector.foldl (fn (facts, facts') =>
    4.66 -      union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) facts')
    4.67 -    accum fact_names
    4.68 +fun add_non_rec_defs facts =
    4.69 +  fold (fn fact as (_, (_, status)) => status = Non_Rec_Def ? insert (op =) fact) facts
    4.70  
    4.71  val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
    4.72  val leo2_unfold_def_rule = "unfold_def"
    4.73  
    4.74 -fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) =
    4.75 +fun add_fact ctxt facts ((_, ss), _, _, rule, deps) =
    4.76    (if rule = leo2_extcnf_equal_neg_rule then
    4.77       insert (op =) (short_thm_name ctxt ext, (Global, General))
    4.78     else if rule = leo2_unfold_def_rule then
    4.79       (* LEO 1.3.3 does not record definitions properly, leading to missing dependencies in the TSTP
    4.80          proof. Remove the next line once this is fixed. *)
    4.81 -     add_non_rec_defs fact_names
    4.82 +     add_non_rec_defs facts
    4.83     else if rule = agsyhol_core_rule orelse rule = satallax_core_rule then
    4.84       (fn [] =>
    4.85           (* agsyHOL and Satallax don't include definitions in their unsatisfiable cores, so we
    4.86              assume the worst and include them all here. *)
    4.87 -         [(short_thm_name ctxt ext, (Global, General))] |> add_non_rec_defs fact_names
    4.88 +         [(short_thm_name ctxt ext, (Global, General))] |> add_non_rec_defs facts
    4.89         | facts => facts)
    4.90     else
    4.91       I)
    4.92 -  #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)
    4.93 +  #> (if null deps then union (op =) (resolve_facts facts ss) else I)
    4.94  
    4.95 -fun used_facts_in_atp_proof ctxt fact_names atp_proof =
    4.96 -  if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
    4.97 -  else fold (add_fact ctxt fact_names) atp_proof []
    4.98 +fun used_facts_in_atp_proof ctxt facts atp_proof =
    4.99 +  if null atp_proof then facts else fold (add_fact ctxt facts) atp_proof []
   4.100  
   4.101  fun used_facts_in_unsound_atp_proof _ _ [] = NONE
   4.102 -  | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
   4.103 -    let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in
   4.104 +  | used_facts_in_unsound_atp_proof ctxt facts atp_proof =
   4.105 +    let val used_facts = used_facts_in_atp_proof ctxt facts atp_proof in
   4.106        if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
   4.107 -         not (is_axiom_used_in_proof (not o null o resolve_conjecture o single) atp_proof) then
   4.108 +         not (is_axiom_used_in_proof (is_some o resolve_conjecture) atp_proof) then
   4.109          SOME (map fst used_facts)
   4.110        else
   4.111          NONE
   4.112 @@ -716,16 +708,16 @@
   4.113    else
   4.114      proof
   4.115  
   4.116 -fun factify_atp_proof fact_names hyp_ts concl_t atp_proof =
   4.117 +fun factify_atp_proof facts hyp_ts concl_t atp_proof =
   4.118    let
   4.119      fun factify_step ((num, ss), _, t, rule, deps) =
   4.120        let
   4.121          val (ss', role', t') =
   4.122 -          (case resolve_conjecture ss of
   4.123 +          (case resolve_conjectures ss of
   4.124              [j] =>
   4.125              if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, nth hyp_ts j)
   4.126            | _ =>
   4.127 -            (case resolve_fact fact_names ss of
   4.128 +            (case resolve_facts facts ss of
   4.129                [] => (ss, Plain, t)
   4.130              | facts => (map fst facts, Axiom, t)))
   4.131        in
     5.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Mon Jun 16 19:40:04 2014 +0200
     5.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Mon Jun 16 19:40:59 2014 +0200
     5.3 @@ -29,11 +29,9 @@
     5.4    val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
     5.5    val reveal_old_skolem_terms : (string * term) list -> term -> term
     5.6    val reveal_lam_lifted : (string * term) list -> term -> term
     5.7 -  val prepare_metis_problem :
     5.8 -    Proof.context -> type_enc -> string -> thm list -> thm list
     5.9 -    -> int Symtab.table * (Metis_Thm.thm * isa_thm) list
    5.10 -       * (unit -> (string * int) list)
    5.11 -       * ((string * term) list * (string * term) list)
    5.12 +  val generate_metis_problem : Proof.context -> type_enc -> string -> thm list -> thm list ->
    5.13 +    int Symtab.table * (Metis_Thm.thm * isa_thm) list * (unit -> (string * int) list)
    5.14 +    * ((string * term) list * (string * term) list)
    5.15  end
    5.16  
    5.17  structure Metis_Generate : METIS_GENERATE =
    5.18 @@ -172,42 +170,33 @@
    5.19        else if String.isPrefix conjecture_prefix ident then
    5.20          NONE
    5.21        else if String.isPrefix helper_prefix ident then
    5.22 -        case (String.isSuffix typed_helper_suffix ident,
    5.23 -              space_explode "_" ident) of
    5.24 +        case (String.isSuffix typed_helper_suffix ident, space_explode "_" ident) of
    5.25            (needs_fairly_sound, _ :: const :: j :: _) =>
    5.26 -          nth (AList.lookup (op =) helper_table (const, needs_fairly_sound)
    5.27 -               |> the)
    5.28 -              (the (Int.fromString j) - 1)
    5.29 +          nth (AList.lookup (op =) helper_table (const, needs_fairly_sound) |> the)
    5.30 +            (the (Int.fromString j) - 1)
    5.31            |> snd |> prepare_helper ctxt
    5.32            |> Isa_Raw |> some
    5.33          | _ => raise Fail ("malformed helper identifier " ^ quote ident)
    5.34        else case try (unprefix fact_prefix) ident of
    5.35          SOME s =>
    5.36 -        let val s = s |> space_explode "_" |> tl |> space_implode "_"
    5.37 -          in
    5.38 +        let val s = s |> space_explode "_" |> tl |> space_implode "_" in
    5.39            case Int.fromString s of
    5.40 -            SOME j =>
    5.41 -            Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
    5.42 +            SOME j => Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
    5.43            | NONE =>
    5.44 -            if String.isPrefix lam_fact_prefix (unascii_of s) then
    5.45 -              Isa_Lambda_Lifted |> some
    5.46 -            else
    5.47 -              raise Fail ("malformed fact identifier " ^ quote ident)
    5.48 +            if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some
    5.49 +            else raise Fail ("malformed fact identifier " ^ quote ident)
    5.50          end
    5.51        | NONE => TrueI |> Isa_Raw |> some
    5.52      end
    5.53    | metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula"
    5.54  
    5.55 -fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =
    5.56 -    eliminate_lam_wrappers t
    5.57 -  | eliminate_lam_wrappers (t $ u) =
    5.58 -    eliminate_lam_wrappers t $ eliminate_lam_wrappers u
    5.59 -  | eliminate_lam_wrappers (Abs (s, T, t)) =
    5.60 -    Abs (s, T, eliminate_lam_wrappers t)
    5.61 +fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) = eliminate_lam_wrappers t
    5.62 +  | eliminate_lam_wrappers (t $ u) = eliminate_lam_wrappers t $ eliminate_lam_wrappers u
    5.63 +  | eliminate_lam_wrappers (Abs (s, T, t)) = Abs (s, T, eliminate_lam_wrappers t)
    5.64    | eliminate_lam_wrappers t = t
    5.65  
    5.66  (* Function to generate metis clauses, including comb and type clauses *)
    5.67 -fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
    5.68 +fun generate_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
    5.69    let
    5.70      val (conj_clauses, fact_clauses) =
    5.71        if is_type_enc_polymorphic type_enc then
    5.72 @@ -221,34 +210,31 @@
    5.73      val num_conjs = length conj_clauses
    5.74      (* Pretend every clause is a "simp" rule, to guide the term ordering. *)
    5.75      val clauses =
    5.76 -      map2 (fn j => pair (Int.toString j, (Local, Simp)))
    5.77 -           (0 upto num_conjs - 1) conj_clauses @
    5.78 +      map2 (fn j => pair (Int.toString j, (Local, Simp))) (0 upto num_conjs - 1) conj_clauses @
    5.79        map2 (fn j => pair (Int.toString (num_conjs + j), (Local, Simp)))
    5.80 -           (0 upto length fact_clauses - 1) fact_clauses
    5.81 +        (0 upto length fact_clauses - 1) fact_clauses
    5.82      val (old_skolems, props) =
    5.83        fold_rev (fn (name, th) => fn (old_skolems, props) =>
    5.84 -                   th |> prop_of |> Logic.strip_imp_concl
    5.85 -                      |> conceal_old_skolem_terms (length clauses) old_skolems
    5.86 -                      ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN)
    5.87 -                          ? eliminate_lam_wrappers
    5.88 -                      ||> (fn prop => (name, prop) :: props))
    5.89 -               clauses ([], [])
    5.90 +           th |> prop_of |> Logic.strip_imp_concl
    5.91 +              |> conceal_old_skolem_terms (length clauses) old_skolems
    5.92 +              ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? eliminate_lam_wrappers
    5.93 +              ||> (fn prop => (name, prop) :: props))
    5.94 +         clauses ([], [])
    5.95      (*
    5.96      val _ =
    5.97        tracing ("PROPS:\n" ^
    5.98                 cat_lines (map (Syntax.string_of_term ctxt o snd) props))
    5.99      *)
   5.100      val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
   5.101 -    val (atp_problem, _, _, lifted, sym_tab) =
   5.102 -      prepare_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false
   5.103 -                          false false [] @{prop False} props
   5.104 +    val (atp_problem, _, lifted, sym_tab) =
   5.105 +      generate_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false false false []
   5.106 +        @{prop False} props
   5.107      (*
   5.108      val _ = tracing ("ATP PROBLEM: " ^
   5.109                       cat_lines (lines_of_atp_problem CNF atp_problem))
   5.110      *)
   5.111      (* "rev" is for compatibility with existing proof scripts. *)
   5.112 -    val axioms =
   5.113 -      atp_problem
   5.114 +    val axioms = atp_problem
   5.115        |> maps (map_filter (metis_axiom_of_atp ctxt type_enc clauses) o snd) |> rev
   5.116      fun ord_info () = atp_problem_term_order_info atp_problem
   5.117    in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end
     6.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jun 16 19:40:04 2014 +0200
     6.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jun 16 19:40:59 2014 +0200
     6.3 @@ -156,8 +156,7 @@
     6.4          map2 (fn j => fn th =>
     6.5                  (Thm.get_name_hint th,
     6.6                   th |> Drule.eta_contraction_rule
     6.7 -                    |> Meson_Clausify.cnf_axiom ctxt new_skolem
     6.8 -                                                (lam_trans = combsN) j
     6.9 +                    |> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j
    6.10                      ||> map do_lams))
    6.11               (0 upto length ths0 - 1) ths0
    6.12        val ths = maps (snd o snd) th_cls_pairs
    6.13 @@ -168,7 +167,7 @@
    6.14        val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
    6.15        val type_enc = type_enc_of_string Strict type_enc
    6.16        val (sym_tab, axioms, ord_info, concealed) =
    6.17 -        prepare_metis_problem ctxt type_enc lam_trans cls ths
    6.18 +        generate_metis_problem ctxt type_enc lam_trans cls ths
    6.19        fun get_isa_thm mth Isa_Reflexive_or_Trivial =
    6.20            reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth
    6.21          | get_isa_thm mth Isa_Lambda_Lifted =
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Jun 16 19:40:04 2014 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Jun 16 19:40:59 2014 +0200
     7.3 @@ -252,7 +252,7 @@
     7.4              val readable_names = not (Config.get ctxt atp_full_names)
     7.5              val lam_trans = lam_trans |> the_default best_lam_trans
     7.6              val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases
     7.7 -            val value as (atp_problem, _, fact_names, _, _) =
     7.8 +            val value as (atp_problem, _, _, _) =
     7.9                if cache_key = SOME key then
    7.10                  cache_value
    7.11                else
    7.12 @@ -261,8 +261,8 @@
    7.13                  |> take num_facts
    7.14                  |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
    7.15                  |> map (apsnd prop_of)
    7.16 -                |> prepare_atp_problem ctxt format prem_role type_enc atp_mode lam_trans
    7.17 -                     uncurried_aliases readable_names true hyp_ts concl_t
    7.18 +                |> generate_atp_problem ctxt format prem_role type_enc atp_mode lam_trans
    7.19 +                  uncurried_aliases readable_names true hyp_ts concl_t
    7.20  
    7.21              fun sel_weights () = atp_problem_selection_weights atp_problem
    7.22              fun ord_info () = atp_problem_term_order_info atp_problem
    7.23 @@ -275,11 +275,13 @@
    7.24              val command =
    7.25                "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
    7.26                |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
    7.27 +
    7.28              val _ =
    7.29                atp_problem
    7.30                |> lines_of_atp_problem format ord ord_info
    7.31                |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
    7.32                |> File.write_list prob_path
    7.33 +
    7.34              val ((output, run_time), (atp_proof, outcome)) =
    7.35                TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
    7.36                |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
    7.37 @@ -290,10 +292,11 @@
    7.38                        |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) atp_problem
    7.39                        handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
    7.40                handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
    7.41 +
    7.42              val outcome =
    7.43                (case outcome of
    7.44                  NONE =>
    7.45 -                (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
    7.46 +                (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof
    7.47                        |> Option.map (sort string_ord) of
    7.48                    SOME facts =>
    7.49                    let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in
    7.50 @@ -321,7 +324,7 @@
    7.51              end
    7.52            | maybe_run_slice _ result = result
    7.53        in
    7.54 -        ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
    7.55 +        ((NONE, ([], Symtab.empty, [], Symtab.empty)),
    7.56           ("", Time.zeroTime, [], [], SOME InternalError), NONE)
    7.57          |> fold maybe_run_slice actual_slices
    7.58        end
    7.59 @@ -333,8 +336,8 @@
    7.60        if dest_dir = "" then ()
    7.61        else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
    7.62  
    7.63 -    val ((_, (_, pool, fact_names, lifted, sym_tab)),
    7.64 -         (output, run_time, used_from, atp_proof, outcome), SOME (format, type_enc)) =
    7.65 +    val ((_, (_, pool, lifted, sym_tab)), (output, run_time, used_from, atp_proof, outcome),
    7.66 +         SOME (format, type_enc)) =
    7.67        with_cleanup clean_up run () |> tap export
    7.68  
    7.69      val important_message =
    7.70 @@ -347,7 +350,7 @@
    7.71        (case outcome of
    7.72          NONE =>
    7.73          let
    7.74 -          val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
    7.75 +          val used_facts = used_facts_in_atp_proof ctxt (map fst used_from) atp_proof
    7.76            val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
    7.77            val meths =
    7.78              bunch_of_proof_methods (smt_proofs <> SOME false) needs_full_types
    7.79 @@ -362,6 +365,7 @@
    7.80             fn preplay =>
    7.81                let
    7.82                  val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
    7.83 +
    7.84                  fun isar_params () =
    7.85                    let
    7.86                      val metis_type_enc =
    7.87 @@ -372,11 +376,12 @@
    7.88                        atp_proof
    7.89                        |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab
    7.90                        |> introduce_spass_skolem
    7.91 -                      |> factify_atp_proof fact_names hyp_ts concl_t
    7.92 +                      |> factify_atp_proof (map fst used_from) hyp_ts concl_t
    7.93                    in
    7.94                      (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
    7.95                       minimize <> SOME false, atp_proof, goal)
    7.96                    end
    7.97 +
    7.98                  val one_line_params =
    7.99                    (preplay, proof_banner mode name, used_facts,
   7.100                     choose_minimize_command thy params minimize_command name preplay, subgoal,