src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 40204 da97d75e20e6
parent 40114 acb75271cdce
child 40627 becf5d5187cc
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Tue Oct 26 20:12:33 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Tue Oct 26 21:01:28 2010 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4      string Symtab.table * bool * int * Proof.context * int list list
     1.5    type text_result = string * (string * locality) list
     1.6  
     1.7 -  val repair_conjecture_shape_and_axiom_names :
     1.8 +  val repair_conjecture_shape_and_fact_names :
     1.9      string -> int list list -> (string * locality) list vector
    1.10      -> int list list * (string * locality) list vector
    1.11    val apply_on_subgoal : int -> int -> string
    1.12 @@ -57,7 +57,7 @@
    1.13  
    1.14  (** SPASS's Flotter hack **)
    1.15  
    1.16 -(* This is a hack required for keeping track of axioms after they have been
    1.17 +(* This is a hack required for keeping track of facts after they have been
    1.18     clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
    1.19     part of this hack. *)
    1.20  
    1.21 @@ -84,8 +84,7 @@
    1.22    #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
    1.23    #> fst
    1.24  
    1.25 -fun repair_conjecture_shape_and_axiom_names output conjecture_shape
    1.26 -                                            axiom_names =
    1.27 +fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names =
    1.28    if String.isSubstring set_ClauseFormulaRelationN output then
    1.29      let
    1.30        val j0 = hd (hd conjecture_shape)
    1.31 @@ -97,10 +96,9 @@
    1.32          |> map (fn s => find_index (curry (op =) s) seq + 1)
    1.33        fun names_for_number j =
    1.34          j |> AList.lookup (op =) name_map |> these
    1.35 -          |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
    1.36 +          |> map_filter (try (unprefix fact_prefix)) |> map unascii_of
    1.37            |> map (fn name =>
    1.38 -                     (name, name |> find_first_in_list_vector axiom_names
    1.39 -                                 |> the)
    1.40 +                     (name, name |> find_first_in_list_vector fact_names |> the)
    1.41                       handle Option.Option =>
    1.42                              error ("No such fact: " ^ quote name ^ "."))
    1.43      in
    1.44 @@ -108,7 +106,7 @@
    1.45         seq |> map names_for_number |> Vector.fromList)
    1.46      end
    1.47    else
    1.48 -    (conjecture_shape, axiom_names)
    1.49 +    (conjecture_shape, fact_names)
    1.50  
    1.51  
    1.52  (** Soft-core proof reconstruction: Metis one-liner **)
    1.53 @@ -139,38 +137,37 @@
    1.54        "\nTo minimize the number of lemmas, try this: " ^
    1.55        Markup.markup Markup.sendback command ^ "."
    1.56  
    1.57 -fun resolve_axiom axiom_names ((_, SOME s)) =
    1.58 -    (case strip_prefix_and_unascii axiom_prefix s of
    1.59 -       SOME s' => (case find_first_in_list_vector axiom_names s' of
    1.60 +fun resolve_fact fact_names ((_, SOME s)) =
    1.61 +    (case strip_prefix_and_unascii fact_prefix s of
    1.62 +       SOME s' => (case find_first_in_list_vector fact_names s' of
    1.63                       SOME x => [(s', x)]
    1.64                     | NONE => [])
    1.65       | NONE => [])
    1.66 -  | resolve_axiom axiom_names (num, NONE) =
    1.67 +  | resolve_fact fact_names (num, NONE) =
    1.68      case Int.fromString num of
    1.69        SOME j =>
    1.70 -      if j > 0 andalso j <= Vector.length axiom_names then
    1.71 -        Vector.sub (axiom_names, j - 1)
    1.72 +      if j > 0 andalso j <= Vector.length fact_names then
    1.73 +        Vector.sub (fact_names, j - 1)
    1.74        else
    1.75          []
    1.76      | NONE => []
    1.77  
    1.78 -fun add_fact axiom_names (Inference (name, _, [])) =
    1.79 -    append (resolve_axiom axiom_names name)
    1.80 +fun add_fact fact_names (Inference (name, _, [])) =
    1.81 +    append (resolve_fact fact_names name)
    1.82    | add_fact _ _ = I
    1.83  
    1.84 -fun used_facts_in_tstplike_proof axiom_names =
    1.85 -  atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names)
    1.86 +fun used_facts_in_tstplike_proof fact_names =
    1.87 +  atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names)
    1.88  
    1.89 -fun used_facts axiom_names =
    1.90 -  used_facts_in_tstplike_proof axiom_names
    1.91 +fun used_facts fact_names =
    1.92 +  used_facts_in_tstplike_proof fact_names
    1.93    #> List.partition (curry (op =) Chained o snd)
    1.94    #> pairself (sort_distinct (string_ord o pairself fst))
    1.95  
    1.96  fun metis_proof_text (banner, full_types, minimize_command,
    1.97 -                      tstplike_proof, axiom_names, goal, i) =
    1.98 +                      tstplike_proof, fact_names, goal, i) =
    1.99    let
   1.100 -    val (chained_lemmas, other_lemmas) =
   1.101 -      used_facts axiom_names tstplike_proof
   1.102 +    val (chained_lemmas, other_lemmas) = used_facts fact_names tstplike_proof
   1.103      val n = Logic.count_prems (prop_of goal)
   1.104    in
   1.105      (metis_line banner full_types i n (map fst other_lemmas) ^
   1.106 @@ -233,7 +230,7 @@
   1.107                        | NONE => ~1
   1.108    in if k >= 0 then [k] else [] end
   1.109  
   1.110 -fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
   1.111 +fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape
   1.112  fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
   1.113  
   1.114  fun raw_label_for_name conjecture_shape name =
   1.115 @@ -491,14 +488,14 @@
   1.116    | replace_dependencies_in_line p (Inference (name, t, deps)) =
   1.117      Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
   1.118  
   1.119 -(* Discard axioms; consolidate adjacent lines that prove the same formula, since
   1.120 +(* Discard facts; consolidate adjacent lines that prove the same formula, since
   1.121     they differ only in type information.*)
   1.122  fun add_line _ _ (line as Definition _) lines = line :: lines
   1.123 -  | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines =
   1.124 -    (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
   1.125 +  | add_line conjecture_shape fact_names (Inference (name, t, [])) lines =
   1.126 +    (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
   1.127         definitions. *)
   1.128 -    if is_axiom axiom_names name then
   1.129 -      (* Axioms are not proof lines. *)
   1.130 +    if is_fact fact_names name then
   1.131 +      (* Facts are not proof lines. *)
   1.132        if is_only_type_information t then
   1.133          map (replace_dependencies_in_line (name, [])) lines
   1.134        (* Is there a repetition? If so, replace later line by earlier one. *)
   1.135 @@ -541,10 +538,10 @@
   1.136  
   1.137  fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
   1.138      (j, line :: map (replace_dependencies_in_line (name, [])) lines)
   1.139 -  | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
   1.140 +  | add_desired_line isar_shrink_factor conjecture_shape fact_names frees
   1.141                       (Inference (name, t, deps)) (j, lines) =
   1.142      (j + 1,
   1.143 -     if is_axiom axiom_names name orelse
   1.144 +     if is_fact fact_names name orelse
   1.145          is_conjecture conjecture_shape name orelse
   1.146          (* the last line must be kept *)
   1.147          j = 0 orelse
   1.148 @@ -580,20 +577,20 @@
   1.149  fun smart_case_split [] facts = ByMetis facts
   1.150    | smart_case_split proofs facts = CaseSplit (proofs, facts)
   1.151  
   1.152 -fun add_fact_from_dependency conjecture_shape axiom_names name =
   1.153 -  if is_axiom axiom_names name then
   1.154 -    apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
   1.155 +fun add_fact_from_dependency conjecture_shape fact_names name =
   1.156 +  if is_fact fact_names name then
   1.157 +    apsnd (union (op =) (map fst (resolve_fact fact_names name)))
   1.158    else
   1.159      apfst (insert (op =) (raw_label_for_name conjecture_shape name))
   1.160  
   1.161  fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   1.162    | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
   1.163      Assume (raw_label_for_name conjecture_shape name, t)
   1.164 -  | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
   1.165 +  | step_for_line conjecture_shape fact_names j (Inference (name, t, deps)) =
   1.166      Have (if j = 1 then [Show] else [],
   1.167            raw_label_for_name conjecture_shape name,
   1.168            fold_rev forall_of (map Var (Term.add_vars t [])) t,
   1.169 -          ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
   1.170 +          ByMetis (fold (add_fact_from_dependency conjecture_shape fact_names)
   1.171                          deps ([], [])))
   1.172  
   1.173  fun repair_name "$true" = "c_True"
   1.174 @@ -606,8 +603,9 @@
   1.175      else
   1.176        s
   1.177  
   1.178 -fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
   1.179 -        tstplike_proof conjecture_shape axiom_names params frees =
   1.180 +fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   1.181 +        isar_shrink_factor tstplike_proof conjecture_shape fact_names params
   1.182 +        frees =
   1.183    let
   1.184      val lines =
   1.185        tstplike_proof
   1.186 @@ -615,14 +613,14 @@
   1.187        |> nasty_atp_proof pool
   1.188        |> map_term_names_in_atp_proof repair_name
   1.189        |> decode_lines ctxt full_types tfrees
   1.190 -      |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
   1.191 +      |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names)
   1.192        |> rpair [] |-> fold_rev add_nontrivial_line
   1.193        |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
   1.194 -                                             conjecture_shape axiom_names frees)
   1.195 +                                             conjecture_shape fact_names frees)
   1.196        |> snd
   1.197    in
   1.198      (if null params then [] else [Fix params]) @
   1.199 -    map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1)
   1.200 +    map2 (step_for_line conjecture_shape fact_names) (length lines downto 1)
   1.201           lines
   1.202    end
   1.203  
   1.204 @@ -915,7 +913,7 @@
   1.205  
   1.206  fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   1.207                      (other_params as (_, full_types, _, tstplike_proof,
   1.208 -                                      axiom_names, goal, i)) =
   1.209 +                                      fact_names, goal, i)) =
   1.210    let
   1.211      val (params, hyp_ts, concl_t) = strip_subgoal goal i
   1.212      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   1.213 @@ -924,7 +922,7 @@
   1.214      val (one_line_proof, lemma_names) = metis_proof_text other_params
   1.215      fun isar_proof_for () =
   1.216        case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   1.217 -               isar_shrink_factor tstplike_proof conjecture_shape axiom_names
   1.218 +               isar_shrink_factor tstplike_proof conjecture_shape fact_names
   1.219                 params frees
   1.220             |> redirect_proof hyp_ts concl_t
   1.221             |> kill_duplicate_assumptions_in_proof