src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 40723 a82badd0e6ef
parent 40627 becf5d5187cc
child 41136 30bedf58b177
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Nov 26 18:07:00 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Nov 26 22:22:07 2010 +0100
     1.3 @@ -24,7 +24,9 @@
     1.4    val command_call : string -> string list -> string
     1.5    val try_command_line : string -> string -> string
     1.6    val minimize_line : ('a list -> string) -> 'a list -> string
     1.7 -  val metis_proof_text : metis_params -> text_result
     1.8 +  val split_used_facts :
     1.9 +    (string * locality) list
    1.10 +    -> (string * locality) list * (string * locality) list
    1.11    val isar_proof_text : isar_params -> metis_params -> text_result
    1.12    val proof_text : bool -> isar_params -> metis_params -> text_result
    1.13  end;
    1.14 @@ -159,15 +161,15 @@
    1.15  fun used_facts_in_tstplike_proof fact_names =
    1.16    atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names)
    1.17  
    1.18 -fun used_facts fact_names =
    1.19 -  used_facts_in_tstplike_proof fact_names
    1.20 -  #> List.partition (curry (op =) Chained o snd)
    1.21 +val split_used_facts =
    1.22 +  List.partition (curry (op =) Chained o snd)
    1.23    #> pairself (sort_distinct (string_ord o pairself fst))
    1.24  
    1.25  fun metis_proof_text (banner, full_types, minimize_command,
    1.26                        tstplike_proof, fact_names, goal, i) =
    1.27    let
    1.28 -    val (chained_lemmas, other_lemmas) = used_facts fact_names tstplike_proof
    1.29 +    val (chained_lemmas, other_lemmas) =
    1.30 +      split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof)
    1.31      val n = Logic.count_prems (prop_of goal)
    1.32    in
    1.33      (metis_line banner full_types i n (map fst other_lemmas) ^
    1.34 @@ -912,14 +914,14 @@
    1.35    in do_proof end
    1.36  
    1.37  fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
    1.38 -                    (other_params as (_, full_types, _, tstplike_proof,
    1.39 +                    (metis_params as (_, full_types, _, tstplike_proof,
    1.40                                        fact_names, goal, i)) =
    1.41    let
    1.42      val (params, hyp_ts, concl_t) = strip_subgoal goal i
    1.43      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
    1.44      val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
    1.45      val n = Logic.count_prems (prop_of goal)
    1.46 -    val (one_line_proof, lemma_names) = metis_proof_text other_params
    1.47 +    val (one_line_proof, lemma_names) = metis_proof_text metis_params
    1.48      fun isar_proof_for () =
    1.49        case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
    1.50                 isar_shrink_factor tstplike_proof conjecture_shape fact_names
    1.51 @@ -940,8 +942,8 @@
    1.52          |> the_default "\nWarning: The Isar proof construction failed."
    1.53    in (one_line_proof ^ isar_proof, lemma_names) end
    1.54  
    1.55 -fun proof_text isar_proof isar_params other_params =
    1.56 +fun proof_text isar_proof isar_params metis_params =
    1.57    (if isar_proof then isar_proof_text isar_params else metis_proof_text)
    1.58 -      other_params
    1.59 +      metis_params
    1.60  
    1.61  end;