src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
changeset 38040 174568533593
parent 38039 e2d546a07fa2
child 38066 9cb8f5432dfc
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 17:38:40 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 18:07:25 2010 +0200
     1.3 @@ -19,11 +19,11 @@
     1.4      bool * minimize_command * string * string vector * thm * int
     1.5      -> string * string list
     1.6    val isar_proof_text:
     1.7 -    string Symtab.table * bool * int * Proof.context * int list
     1.8 +    string Symtab.table * bool * int * Proof.context * int list list
     1.9      -> bool * minimize_command * string * string vector * thm * int
    1.10      -> string * string list
    1.11    val proof_text:
    1.12 -    bool -> string Symtab.table * bool * int * Proof.context * int list
    1.13 +    bool -> string Symtab.table * bool * int * Proof.context * int list list
    1.14      -> bool * minimize_command * string * string vector * thm * int
    1.15      -> string * string list
    1.16  end;
    1.17 @@ -66,7 +66,8 @@
    1.18    | mk_anot phi = AConn (ANot, [phi])
    1.19  fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
    1.20  
    1.21 -val index_in_shape : int -> int list -> int = find_index o curry (op =)
    1.22 +val index_in_shape : int -> int list list -> int =
    1.23 +  find_index o exists o curry (op =)
    1.24  fun is_axiom_clause_number thm_names num =
    1.25    num > 0 andalso num <= Vector.length thm_names andalso
    1.26    Vector.sub (thm_names, num - 1) <> ""
    1.27 @@ -745,27 +746,33 @@
    1.28        nth hyp_ts (index_in_shape num conjecture_shape)
    1.29        handle Subscript =>
    1.30               raise Fail ("Cannot find hypothesis " ^ Int.toString num)
    1.31 -    val concl_l = (raw_prefix, List.last conjecture_shape)
    1.32 -    fun first_pass ([], contra) = ([], contra)
    1.33 -      | first_pass ((step as Fix _) :: proof, contra) =
    1.34 -        first_pass (proof, contra) |>> cons step
    1.35 -      | first_pass ((step as Let _) :: proof, contra) =
    1.36 -        first_pass (proof, contra) |>> cons step
    1.37 -      | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
    1.38 -        if l = concl_l then
    1.39 -          first_pass (proof, contra ||> l = concl_l ? cons step)
    1.40 -        else
    1.41 -          first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
    1.42 -      | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
    1.43 -        let val step = Have (qs, l, t, ByMetis (ls, ss)) in
    1.44 -          if exists (member (op =) (fst contra)) ls then
    1.45 -            first_pass (proof, contra |>> cons l ||> cons step)
    1.46 -          else
    1.47 -            first_pass (proof, contra) |>> cons step
    1.48 -        end
    1.49 -      | first_pass _ = raise Fail "malformed proof"
    1.50 +     val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
    1.51 +     val canonicalize_labels =
    1.52 +       map (fn l => if member (op =) concl_ls l then hd concl_ls else l)
    1.53 +       #> distinct (op =)
    1.54 +     fun first_pass ([], contra) = ([], contra)
    1.55 +       | first_pass ((step as Fix _) :: proof, contra) =
    1.56 +         first_pass (proof, contra) |>> cons step
    1.57 +       | first_pass ((step as Let _) :: proof, contra) =
    1.58 +         first_pass (proof, contra) |>> cons step
    1.59 +       | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
    1.60 +         if member (op =) concl_ls l then
    1.61 +           first_pass (proof, contra ||> l = hd concl_ls ? cons step)
    1.62 +         else
    1.63 +           first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
    1.64 +       | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
    1.65 +         let
    1.66 +           val ls = canonicalize_labels ls
    1.67 +           val step = Have (qs, l, t, ByMetis (ls, ss))
    1.68 +         in
    1.69 +           if exists (member (op =) (fst contra)) ls then
    1.70 +             first_pass (proof, contra |>> cons l ||> cons step)
    1.71 +           else
    1.72 +             first_pass (proof, contra) |>> cons step
    1.73 +         end
    1.74 +       | first_pass _ = raise Fail "malformed proof"
    1.75      val (proof_top, (contra_ls, contra_proof)) =
    1.76 -      first_pass (proof, ([concl_l], []))
    1.77 +      first_pass (proof, (concl_ls, []))
    1.78      val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
    1.79      fun backpatch_labels patches ls =
    1.80        fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
    1.81 @@ -800,7 +807,7 @@
    1.82                 val proofs =
    1.83                   map_filter
    1.84                       (fn l =>
    1.85 -                         if l = concl_l then
    1.86 +                         if member (op =) concl_ls l then
    1.87                             NONE
    1.88                           else
    1.89                             let