src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42541 8938507b2054
parent 42539 f6ba908b8b27
child 42544 75cb06eee990
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    type type_system = Sledgehammer_ATP_Translate.type_system
     1.5    type minimize_command = string list -> string
     1.6    type metis_params =
     1.7 -    string * type_system * minimize_command * string proof
     1.8 +    string * type_system * minimize_command * string proof * int
     1.9      * (string * locality) list vector * thm * int
    1.10    type isar_params =
    1.11      string Symtab.table * bool * int * Proof.context * int list list
    1.12 @@ -23,9 +23,11 @@
    1.13      string -> int list list -> (string * locality) list vector
    1.14      -> int list list * (string * locality) list vector
    1.15    val used_facts_in_atp_proof :
    1.16 -    (string * locality) list vector -> string proof -> (string * locality) list
    1.17 +    int -> (string * locality) list vector -> string proof
    1.18 +    -> (string * locality) list
    1.19    val is_unsound_proof :
    1.20 -    int list list -> (string * locality) list vector -> string proof -> bool
    1.21 +    int list list -> int -> (string * locality) list vector -> string proof
    1.22 +    -> bool
    1.23    val apply_on_subgoal : string -> int -> int -> string
    1.24    val command_call : string -> string list -> string
    1.25    val try_command_line : string -> string -> string
    1.26 @@ -50,7 +52,7 @@
    1.27  
    1.28  type minimize_command = string list -> string
    1.29  type metis_params =
    1.30 -  string * type_system * minimize_command * string proof
    1.31 +  string * type_system * minimize_command * string proof * int
    1.32    * (string * locality) list vector * thm * int
    1.33  type isar_params =
    1.34    string Symtab.table * bool * int * Proof.context * int list list
    1.35 @@ -122,7 +124,7 @@
    1.36  
    1.37  val vampire_step_prefix = "f" (* grrr... *)
    1.38  
    1.39 -fun resolve_fact fact_names ((_, SOME s)) =
    1.40 +fun resolve_fact _ fact_names ((_, SOME s)) =
    1.41      (case try (unprefix fact_prefix) s of
    1.42         SOME s' =>
    1.43         let val s' = s' |> unprefix_fact_number |> unascii_of in
    1.44 @@ -131,13 +133,15 @@
    1.45           | NONE => []
    1.46         end
    1.47       | NONE => [])
    1.48 -  | resolve_fact fact_names (num, NONE) =
    1.49 +  | resolve_fact facts_offset fact_names (num, NONE) =
    1.50      case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
    1.51        SOME j =>
    1.52 -      if j > 0 andalso j <= Vector.length fact_names then
    1.53 -        Vector.sub (fact_names, j - 1)
    1.54 -      else
    1.55 -        []
    1.56 +      let val j = j - facts_offset in
    1.57 +        if j > 0 andalso j <= Vector.length fact_names then
    1.58 +          Vector.sub (fact_names, j - 1)
    1.59 +        else
    1.60 +          []
    1.61 +      end
    1.62      | NONE => []
    1.63  
    1.64  fun resolve_conjecture conjecture_shape (num, s_opt) =
    1.65 @@ -150,25 +154,26 @@
    1.66                        | NONE => ~1
    1.67    in if k >= 0 then [k] else [] end
    1.68  
    1.69 -fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape
    1.70 +fun is_fact conjecture_shape = not o null o resolve_fact 0 conjecture_shape
    1.71  fun is_conjecture conjecture_shape =
    1.72    not o null o resolve_conjecture conjecture_shape
    1.73  
    1.74 -fun add_fact fact_names (Inference (name, _, [])) =
    1.75 -    append (resolve_fact fact_names name)
    1.76 -  | add_fact _ _ = I
    1.77 +fun add_fact facts_offset fact_names (Inference (name, _, [])) =
    1.78 +    append (resolve_fact facts_offset fact_names name)
    1.79 +  | add_fact _ _ _ = I
    1.80  
    1.81 -fun used_facts_in_atp_proof fact_names atp_proof =
    1.82 +fun used_facts_in_atp_proof facts_offset fact_names atp_proof =
    1.83    if null atp_proof then Vector.foldl (op @) [] fact_names
    1.84 -  else fold (add_fact fact_names) atp_proof []
    1.85 +  else fold (add_fact facts_offset fact_names) atp_proof []
    1.86  
    1.87  fun is_conjecture_referred_to_in_proof conjecture_shape =
    1.88    exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
    1.89             | _ => false)
    1.90  
    1.91 -fun is_unsound_proof conjecture_shape fact_names =
    1.92 -  (not o is_conjecture_referred_to_in_proof conjecture_shape) andf
    1.93 -  forall (is_global_locality o snd) o used_facts_in_atp_proof fact_names
    1.94 +fun is_unsound_proof conjecture_shape facts_offset fact_names =
    1.95 +  not o is_conjecture_referred_to_in_proof conjecture_shape andf
    1.96 +  forall (is_global_locality o snd)
    1.97 +  o used_facts_in_atp_proof facts_offset fact_names
    1.98  
    1.99  (** Soft-core proof reconstruction: Metis one-liner **)
   1.100  
   1.101 @@ -206,11 +211,12 @@
   1.102    List.partition (curry (op =) Chained o snd)
   1.103    #> pairself (sort_distinct (string_ord o pairself fst))
   1.104  
   1.105 -fun metis_proof_text (banner, type_sys, minimize_command, atp_proof, fact_names,
   1.106 -                      goal, i) =
   1.107 +fun metis_proof_text (banner, type_sys, minimize_command, atp_proof,
   1.108 +                      facts_offset, fact_names, goal, i) =
   1.109    let
   1.110      val (chained_lemmas, other_lemmas) =
   1.111 -      split_used_facts (used_facts_in_atp_proof fact_names atp_proof)
   1.112 +      atp_proof |> used_facts_in_atp_proof facts_offset fact_names
   1.113 +                |> split_used_facts
   1.114      val n = Logic.count_prems (prop_of goal)
   1.115    in
   1.116      (metis_line banner type_sys i n (map fst other_lemmas) ^
   1.117 @@ -606,20 +612,22 @@
   1.118  fun smart_case_split [] facts = ByMetis facts
   1.119    | smart_case_split proofs facts = CaseSplit (proofs, facts)
   1.120  
   1.121 -fun add_fact_from_dependency conjecture_shape fact_names name =
   1.122 +fun add_fact_from_dependency conjecture_shape facts_offset fact_names name =
   1.123    if is_fact fact_names name then
   1.124 -    apsnd (union (op =) (map fst (resolve_fact fact_names name)))
   1.125 +    apsnd (union (op =) (map fst (resolve_fact facts_offset fact_names name)))
   1.126    else
   1.127      apfst (insert (op =) (raw_label_for_name conjecture_shape name))
   1.128  
   1.129 -fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   1.130 -  | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
   1.131 +fun step_for_line _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   1.132 +  | step_for_line conjecture_shape _ _ _ (Inference (name, t, [])) =
   1.133      Assume (raw_label_for_name conjecture_shape name, t)
   1.134 -  | step_for_line conjecture_shape fact_names j (Inference (name, t, deps)) =
   1.135 +  | step_for_line conjecture_shape facts_offset fact_names j
   1.136 +                  (Inference (name, t, deps)) =
   1.137      Have (if j = 1 then [Show] else [],
   1.138            raw_label_for_name conjecture_shape name,
   1.139            fold_rev forall_of (map Var (Term.add_vars t [])) t,
   1.140 -          ByMetis (fold (add_fact_from_dependency conjecture_shape fact_names)
   1.141 +          ByMetis (fold (add_fact_from_dependency conjecture_shape facts_offset
   1.142 +                                                  fact_names)
   1.143                          deps ([], [])))
   1.144  
   1.145  fun repair_name "$true" = "c_True"
   1.146 @@ -633,7 +641,7 @@
   1.147        s
   1.148  
   1.149  fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor
   1.150 -        atp_proof conjecture_shape fact_names params frees =
   1.151 +        atp_proof conjecture_shape facts_offset fact_names params frees =
   1.152    let
   1.153      val lines =
   1.154        atp_proof
   1.155 @@ -647,8 +655,8 @@
   1.156        |> snd
   1.157    in
   1.158      (if null params then [] else [Fix params]) @
   1.159 -    map2 (step_for_line conjecture_shape fact_names) (length lines downto 1)
   1.160 -         lines
   1.161 +    map2 (step_for_line conjecture_shape facts_offset fact_names)
   1.162 +         (length lines downto 1) lines
   1.163    end
   1.164  
   1.165  (* When redirecting proofs, we keep information about the labels seen so far in
   1.166 @@ -939,7 +947,8 @@
   1.167    in do_proof end
   1.168  
   1.169  fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   1.170 -        (metis_params as (_, type_sys, _, atp_proof, fact_names, goal, i)) =
   1.171 +        (metis_params as (_, type_sys, _, atp_proof, facts_offset, fact_names,
   1.172 +                          goal, i)) =
   1.173    let
   1.174      val (params, hyp_ts, concl_t) = strip_subgoal goal i
   1.175      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   1.176 @@ -948,8 +957,8 @@
   1.177      val (one_line_proof, lemma_names) = metis_proof_text metis_params
   1.178      fun isar_proof_for () =
   1.179        case isar_proof_from_atp_proof pool ctxt type_sys tfrees
   1.180 -               isar_shrink_factor atp_proof conjecture_shape fact_names params
   1.181 -               frees
   1.182 +               isar_shrink_factor atp_proof conjecture_shape facts_offset
   1.183 +               fact_names params frees
   1.184             |> redirect_proof hyp_ts concl_t
   1.185             |> kill_duplicate_assumptions_in_proof
   1.186             |> then_chain_proof