1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jul 28 17:38:40 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jul 28 18:07:25 2010 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4       output: string,
     1.5       proof: string,
     1.6       internal_thm_names: string Vector.vector,
     1.7 -     conjecture_shape: int list,
     1.8 +     conjecture_shape: int list list,
     1.9       filtered_clauses: (string * thm) list}
    1.10    type prover =
    1.11      params -> minimize_command -> Time.time -> problem -> prover_result
    1.12 @@ -112,7 +112,7 @@
    1.13     output: string,
    1.14     proof: string,
    1.15     internal_thm_names: string Vector.vector,
    1.16 -   conjecture_shape: int list,
    1.17 +   conjecture_shape: int list list,
    1.18     filtered_clauses: (string * thm) list}
    1.19  
    1.20  type prover =
    1.21 @@ -681,15 +681,14 @@
    1.22         clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
    1.23         of this hack. *)
    1.24      let
    1.25 -      val j0 = hd conjecture_shape
    1.26 +      val j0 = hd (hd conjecture_shape)
    1.27        val seq = extract_clause_sequence output
    1.28        val name_map = extract_clause_formula_relation output
    1.29        fun renumber_conjecture j =
    1.30          AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
    1.31 -        |> the_single
    1.32 -        |> (fn s => find_index (curry (op =) s) seq + 1)
    1.33 +        |> map (fn s => find_index (curry (op =) s) seq + 1)
    1.34      in
    1.35 -      (conjecture_shape |> map renumber_conjecture,
    1.36 +      (conjecture_shape |> map (maps renumber_conjecture),
    1.37         seq |> map (the o AList.lookup (op =) name_map)
    1.38             |> map (fn s => case try (unprefix axiom_prefix) s of
    1.39                               SOME s' => undo_ascii_of s'
    1.40 @@ -800,6 +799,7 @@
    1.41                                explicit_apply probfile clauses
    1.42              val conjecture_shape =
    1.43                conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
    1.44 +              |> map single
    1.45              val result =
    1.46                do_run false
    1.47                |> (fn (_, msecs0, _, SOME _) =>

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 17:38:40 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 18:07:25 2010 +0200
     2.3 @@ -19,11 +19,11 @@
     2.4      bool * minimize_command * string * string vector * thm * int
     2.5      -> string * string list
     2.6    val isar_proof_text:
     2.7 -    string Symtab.table * bool * int * Proof.context * int list
     2.8 +    string Symtab.table * bool * int * Proof.context * int list list
     2.9      -> bool * minimize_command * string * string vector * thm * int
    2.10      -> string * string list
    2.11    val proof_text:
    2.12 -    bool -> string Symtab.table * bool * int * Proof.context * int list
    2.13 +    bool -> string Symtab.table * bool * int * Proof.context * int list list
    2.14      -> bool * minimize_command * string * string vector * thm * int
    2.15      -> string * string list
    2.16  end;
    2.17 @@ -66,7 +66,8 @@
    2.18    | mk_anot phi = AConn (ANot, [phi])
    2.19  fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
    2.20  
    2.21 -val index_in_shape : int -> int list -> int = find_index o curry (op =)
    2.22 +val index_in_shape : int -> int list list -> int =
    2.23 +  find_index o exists o curry (op =)
    2.24  fun is_axiom_clause_number thm_names num =
    2.25    num > 0 andalso num <= Vector.length thm_names andalso
    2.26    Vector.sub (thm_names, num - 1) <> ""
    2.27 @@ -745,27 +746,33 @@
    2.28        nth hyp_ts (index_in_shape num conjecture_shape)
    2.29        handle Subscript =>
    2.30               raise Fail ("Cannot find hypothesis " ^ Int.toString num)
    2.31 -    val concl_l = (raw_prefix, List.last conjecture_shape)
    2.32 -    fun first_pass ([], contra) = ([], contra)
    2.33 -      | first_pass ((step as Fix _) :: proof, contra) =
    2.34 -        first_pass (proof, contra) |>> cons step
    2.35 -      | first_pass ((step as Let _) :: proof, contra) =
    2.36 -        first_pass (proof, contra) |>> cons step
    2.37 -      | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
    2.38 -        if l = concl_l then
    2.39 -          first_pass (proof, contra ||> l = concl_l ? cons step)
    2.40 -        else
    2.41 -          first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
    2.42 -      | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
    2.43 -        let val step = Have (qs, l, t, ByMetis (ls, ss)) in
    2.44 -          if exists (member (op =) (fst contra)) ls then
    2.45 -            first_pass (proof, contra |>> cons l ||> cons step)
    2.46 -          else
    2.47 -            first_pass (proof, contra) |>> cons step
    2.48 -        end
    2.49 -      | first_pass _ = raise Fail "malformed proof"
    2.50 +     val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
    2.51 +     val canonicalize_labels =
    2.52 +       map (fn l => if member (op =) concl_ls l then hd concl_ls else l)
    2.53 +       #> distinct (op =)
    2.54 +     fun first_pass ([], contra) = ([], contra)
    2.55 +       | first_pass ((step as Fix _) :: proof, contra) =
    2.56 +         first_pass (proof, contra) |>> cons step
    2.57 +       | first_pass ((step as Let _) :: proof, contra) =
    2.58 +         first_pass (proof, contra) |>> cons step
    2.59 +       | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
    2.60 +         if member (op =) concl_ls l then
    2.61 +           first_pass (proof, contra ||> l = hd concl_ls ? cons step)
    2.62 +         else
    2.63 +           first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
    2.64 +       | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
    2.65 +         let
    2.66 +           val ls = canonicalize_labels ls
    2.67 +           val step = Have (qs, l, t, ByMetis (ls, ss))
    2.68 +         in
    2.69 +           if exists (member (op =) (fst contra)) ls then
    2.70 +             first_pass (proof, contra |>> cons l ||> cons step)
    2.71 +           else
    2.72 +             first_pass (proof, contra) |>> cons step
    2.73 +         end
    2.74 +       | first_pass _ = raise Fail "malformed proof"
    2.75      val (proof_top, (contra_ls, contra_proof)) =
    2.76 -      first_pass (proof, ([concl_l], []))
    2.77 +      first_pass (proof, (concl_ls, []))
    2.78      val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
    2.79      fun backpatch_labels patches ls =
    2.80        fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
    2.81 @@ -800,7 +807,7 @@
    2.82                 val proofs =
    2.83                   map_filter
    2.84                       (fn l =>
    2.85 -                         if l = concl_l then
    2.86 +                         if member (op =) concl_ls l then
    2.87                             NONE
    2.88                           else
    2.89                             let