merged
authorblanchet
Fri Aug 27 16:05:46 2010 +0200 (2010-08-27)
changeset 38829c18e8f90f4dc
parent 38815 d0196406ee32
parent 38828 91ad85f962c4
child 38830 51efa72555bb
child 38889 d0e3f68dde63
merged
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 27 14:25:29 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 27 16:05:46 2010 +0200
     1.3 @@ -357,15 +357,16 @@
     1.4      case result of
     1.5        SH_OK (time_isa, time_atp, names) =>
     1.6          let
     1.7 -          fun get_thms (name, loc) =
     1.8 -            ((name, loc), thms_of_name (Proof.context_of st) name)
     1.9 +          fun get_thms (name, Sledgehammer_Fact_Filter.Chained) = NONE
    1.10 +            | get_thms (name, loc) =
    1.11 +              SOME ((name, loc), thms_of_name (Proof.context_of st) name)
    1.12          in
    1.13            change_data id inc_sh_success;
    1.14            change_data id (inc_sh_lemmas (length names));
    1.15            change_data id (inc_sh_max_lems (length names));
    1.16            change_data id (inc_sh_time_isa time_isa);
    1.17            change_data id (inc_sh_time_atp time_atp);
    1.18 -          named_thms := SOME (map get_thms names);
    1.19 +          named_thms := SOME (map_filter get_thms names);
    1.20            log (sh_tag id ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
    1.21              string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
    1.22          end
     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Aug 27 14:25:29 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Aug 27 16:05:46 2010 +0200
     2.3 @@ -293,7 +293,7 @@
     2.4    (remotify_name name, remotify_config system_name system_versions config)
     2.5  
     2.6  val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
     2.7 -val remote_vampire = remotify_prover vampire "Vampire" ["9.9", "0.6", "1.0"]
     2.8 +val remote_vampire = remotify_prover vampire "Vampire" ["9.0", "1.0", "0.6"]
     2.9  val remote_sine_e =
    2.10    remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
    2.11                  1000 (* FUDGE *) false true
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 27 14:25:29 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 27 16:05:46 2010 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4       atp_run_time_in_msecs: int,
     3.5       output: string,
     3.6       proof: string,
     3.7 -     axiom_names: (string * locality) vector,
     3.8 +     axiom_names: (string * locality) list vector,
     3.9       conjecture_shape: int list list}
    3.10    type prover = params -> minimize_command -> problem -> prover_result
    3.11  
    3.12 @@ -107,7 +107,7 @@
    3.13     atp_run_time_in_msecs: int,
    3.14     output: string,
    3.15     proof: string,
    3.16 -   axiom_names: (string * locality) vector,
    3.17 +   axiom_names: (string * locality) list vector,
    3.18     conjecture_shape: int list list}
    3.19  
    3.20  type prover = params -> minimize_command -> problem -> prover_result
    3.21 @@ -175,6 +175,7 @@
    3.22    #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
    3.23    #> explode #> parse_clause_formula_relation #> fst
    3.24  
    3.25 +(* TODO: move to "Sledgehammer_Proof_Reconstruct.ML" *)
    3.26  fun repair_conjecture_shape_and_theorem_names output conjecture_shape
    3.27                                                axiom_names =
    3.28    if String.isSubstring set_ClauseFormulaRelationN output then
    3.29 @@ -189,19 +190,17 @@
    3.30          conjecture_prefix ^ string_of_int (j - j0)
    3.31          |> AList.find (fn (s, ss) => member (op =) ss s) name_map
    3.32          |> map (fn s => find_index (curry (op =) s) seq + 1)
    3.33 -      fun name_for_number j =
    3.34 -        let
    3.35 -          val axioms =
    3.36 -            j |> AList.lookup (op =) name_map |> these
    3.37 -              |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
    3.38 -          val loc =
    3.39 -            case axioms of
    3.40 -              [axiom] => find_first_in_vector axiom_names axiom General
    3.41 -            | _ => General
    3.42 -        in (axioms |> space_implode " ", loc) end
    3.43 +      fun names_for_number j =
    3.44 +        j |> AList.lookup (op =) name_map |> these
    3.45 +          |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
    3.46 +          |> map (fn name =>
    3.47 +                     (name, name |> find_first_in_list_vector axiom_names
    3.48 +                                 |> the)
    3.49 +                     handle Option.Option =>
    3.50 +                            error ("No such fact: " ^ quote name ^ "."))
    3.51      in
    3.52        (conjecture_shape |> map (maps renumber_conjecture),
    3.53 -       seq |> map name_for_number |> Vector.fromList)
    3.54 +       seq |> map names_for_number |> Vector.fromList)
    3.55      end
    3.56    else
    3.57      (conjecture_shape, axiom_names)
    3.58 @@ -253,7 +252,7 @@
    3.59          if the_dest_dir = "" then File.tmp_path probfile
    3.60          else if File.exists (Path.explode the_dest_dir)
    3.61          then Path.append (Path.explode the_dest_dir) probfile
    3.62 -        else error ("No such directory: " ^ the_dest_dir ^ ".")
    3.63 +        else error ("No such directory: " ^ quote the_dest_dir ^ ".")
    3.64        end;
    3.65  
    3.66      val measure_run_time = verbose orelse Config.get ctxt measure_runtime
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 14:25:29 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 16:05:46 2010 +0200
     4.3 @@ -13,6 +13,7 @@
     4.4       only: bool}
     4.5  
     4.6    val trace : bool Unsynchronized.ref
     4.7 +  val term_patterns : bool Unsynchronized.ref
     4.8    val name_thm_pairs_from_ref :
     4.9      Proof.context -> unit Symtab.table -> thm list -> Facts.ref
    4.10      -> ((string * locality) * thm) list
    4.11 @@ -30,6 +31,9 @@
    4.12  val trace = Unsynchronized.ref false
    4.13  fun trace_msg msg = if !trace then tracing (msg ()) else ()
    4.14  
    4.15 +(* experimental feature *)
    4.16 +val term_patterns = Unsynchronized.ref false
    4.17 +
    4.18  val respect_no_atp = true
    4.19  
    4.20  datatype locality = General | Theory | Local | Chained
    4.21 @@ -65,82 +69,92 @@
    4.22  
    4.23  (*** constants with types ***)
    4.24  
    4.25 -(*An abstraction of Isabelle types*)
    4.26 -datatype pseudotype = PVar | PType of string * pseudotype list
    4.27 +(* An abstraction of Isabelle types and first-order terms *)
    4.28 +datatype pattern = PVar | PApp of string * pattern list
    4.29  
    4.30 -fun string_for_pseudotype PVar = "?"
    4.31 -  | string_for_pseudotype (PType (s, Ts)) =
    4.32 -    (case Ts of
    4.33 -       [] => ""
    4.34 -     | [T] => string_for_pseudotype T
    4.35 -     | Ts => string_for_pseudotypes Ts ^ " ") ^ s
    4.36 -and string_for_pseudotypes Ts =
    4.37 -  "(" ^ commas (map string_for_pseudotype Ts) ^ ")"
    4.38 +fun string_for_pattern PVar = "_"
    4.39 +  | string_for_pattern (PApp (s, ps)) =
    4.40 +    if null ps then s else s ^ string_for_patterns ps
    4.41 +and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
    4.42  
    4.43  (*Is the second type an instance of the first one?*)
    4.44 -fun match_pseudotype (PType (a, T), PType (b, U)) =
    4.45 -    a = b andalso match_pseudotypes (T, U)
    4.46 -  | match_pseudotype (PVar, _) = true
    4.47 -  | match_pseudotype (_, PVar) = false
    4.48 -and match_pseudotypes ([], []) = true
    4.49 -  | match_pseudotypes (T :: Ts, U :: Us) =
    4.50 -    match_pseudotype (T, U) andalso match_pseudotypes (Ts, Us)
    4.51 +fun match_pattern (PVar, _) = true
    4.52 +  | match_pattern (PApp _, PVar) = false
    4.53 +  | match_pattern (PApp (s, ps), PApp (t, qs)) =
    4.54 +    s = t andalso match_patterns (ps, qs)
    4.55 +and match_patterns (_, []) = true
    4.56 +  | match_patterns ([], _) = false
    4.57 +  | match_patterns (p :: ps, q :: qs) =
    4.58 +    match_pattern (p, q) andalso match_patterns (ps, qs)
    4.59  
    4.60 -(*Is there a unifiable constant?*)
    4.61 -fun pseudoconst_mem f const_tab (c, c_typ) =
    4.62 -  exists (curry (match_pseudotypes o f) c_typ)
    4.63 -         (these (Symtab.lookup const_tab c))
    4.64 +(* Is there a unifiable constant? *)
    4.65 +fun pconst_mem f consts (s, ps) =
    4.66 +  exists (curry (match_patterns o f) ps)
    4.67 +         (map snd (filter (curry (op =) s o fst) consts))
    4.68 +fun pconst_hyper_mem f const_tab (s, ps) =
    4.69 +  exists (curry (match_patterns o f) ps) (these (Symtab.lookup const_tab s))
    4.70  
    4.71 -fun pseudotype_for (Type (c,typs)) = PType (c, map pseudotype_for typs)
    4.72 -  | pseudotype_for (TFree _) = PVar
    4.73 -  | pseudotype_for (TVar _) = PVar
    4.74 -(* Pairs a constant with the list of its type instantiations. *)
    4.75 -fun pseudoconst_for thy (c, T) =
    4.76 -  (c, map pseudotype_for (Sign.const_typargs thy (c, T)))
    4.77 -  handle TYPE _ => (c, [])  (* Variable (locale constant): monomorphic *)
    4.78 +fun ptype (Type (s, Ts)) = PApp (s, map ptype Ts)
    4.79 +  | ptype (TFree (s, _)) = PApp (s, [])
    4.80 +  | ptype (TVar _) = PVar
    4.81  
    4.82 -fun string_for_pseudoconst (s, []) = s
    4.83 -  | string_for_pseudoconst (s, Ts) = s ^ string_for_pseudotypes Ts
    4.84 -fun string_for_super_pseudoconst (s, [[]]) = s
    4.85 -  | string_for_super_pseudoconst (s, Tss) =
    4.86 -    s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
    4.87 +fun pterm thy t =
    4.88 +  case strip_comb t of
    4.89 +    (Const x, ts) => PApp (pconst thy true x ts)
    4.90 +  | (Free x, ts) => PApp (pconst thy false x ts)
    4.91 +  | (Var x, []) => PVar
    4.92 +  | _ => PApp ("?", [])  (* equivalence class of higher-order constructs *)
    4.93 +(* Pairs a constant with the list of its type instantiations. *)
    4.94 +and pconst_args thy const (s, T) ts =
    4.95 +  (if const then map ptype (these (try (Sign.const_typargs thy) (s, T)))
    4.96 +   else []) @
    4.97 +  (if !term_patterns then map (pterm thy) ts else [])
    4.98 +and pconst thy const (s, T) ts = (s, pconst_args thy const (s, T) ts)
    4.99  
   4.100 -val abs_prefix = "Sledgehammer.abs"
   4.101 +fun string_for_hyper_pconst (s, pss) =
   4.102 +  s ^ "{" ^ commas (map string_for_patterns pss) ^ "}"
   4.103 +
   4.104 +val abs_name = "Sledgehammer.abs"
   4.105  val skolem_prefix = "Sledgehammer.sko"
   4.106  
   4.107 -(* Add a pseudoconstant to the table, but a [] entry means a standard
   4.108 +(* These are typically simplified away by "Meson.presimplify". Equality is
   4.109 +   handled specially via "fequal". *)
   4.110 +val boring_consts =
   4.111 +  [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
   4.112 +   @{const_name "op ="}]
   4.113 +
   4.114 +(* Add a pconstant to the table, but a [] entry means a standard
   4.115     connective, which we ignore.*)
   4.116 -fun add_pseudoconst_to_table also_skolem (c, ctyps) =
   4.117 -  if also_skolem orelse not (String.isPrefix skolem_prefix c) then
   4.118 -    Symtab.map_default (c, [ctyps])
   4.119 -                       (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
   4.120 +fun add_pconst_to_table also_skolem (c, ps) =
   4.121 +  if member (op =) boring_consts c orelse
   4.122 +     (not also_skolem andalso String.isPrefix skolem_prefix c) then
   4.123 +    I
   4.124    else
   4.125 -    I
   4.126 +    Symtab.map_default (c, [ps]) (insert (op =) ps)
   4.127  
   4.128  fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
   4.129  
   4.130 -val flip = Option.map not
   4.131 -(* These are typically simplified away by "Meson.presimplify". *)
   4.132 -val boring_consts =
   4.133 -  [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}]
   4.134 -
   4.135 -fun get_pseudoconsts thy also_skolems pos ts =
   4.136 +fun get_pconsts thy also_skolems pos ts =
   4.137    let
   4.138 +    val flip = Option.map not
   4.139      (* We include free variables, as well as constants, to handle locales. For
   4.140         each quantifiers that must necessarily be skolemized by the ATP, we
   4.141         introduce a fresh constant to simulate the effect of Skolemization. *)
   4.142 -    fun do_term t =
   4.143 -      case t of
   4.144 -        Const x => add_pseudoconst_to_table also_skolems (pseudoconst_for thy x)
   4.145 -      | Free (s, _) => add_pseudoconst_to_table also_skolems (s, [])
   4.146 -      | t1 $ t2 => fold do_term [t1, t2]
   4.147 -      | Abs (_, _, t') =>
   4.148 -        do_term t' #> add_pseudoconst_to_table true (abs_prefix, [])
   4.149 -      | _ => I
   4.150 +    fun do_const const (s, T) ts =
   4.151 +      add_pconst_to_table also_skolems (pconst thy const (s, T) ts)
   4.152 +      #> fold do_term ts
   4.153 +    and do_term t =
   4.154 +      case strip_comb t of
   4.155 +        (Const x, ts) => do_const true x ts
   4.156 +      | (Free x, ts) => do_const false x ts
   4.157 +      | (Abs (_, _, t'), ts) =>
   4.158 +        null ts ? add_pconst_to_table true (abs_name, [])
   4.159 +        #> fold do_term (t' :: ts)
   4.160 +      | (_, ts) => fold do_term ts
   4.161      fun do_quantifier will_surely_be_skolemized body_t =
   4.162        do_formula pos body_t
   4.163        #> (if also_skolems andalso will_surely_be_skolemized then
   4.164 -            add_pseudoconst_to_table true (gensym skolem_prefix, [])
   4.165 +            add_pconst_to_table true (gensym skolem_prefix, [])
   4.166            else
   4.167              I)
   4.168      and do_term_or_formula T =
   4.169 @@ -179,10 +193,7 @@
   4.170        | (t0 as Const (_, @{typ bool})) $ t1 =>
   4.171          do_term t0 #> do_formula pos t1  (* theory constant *)
   4.172        | _ => do_term t
   4.173 -  in
   4.174 -    Symtab.empty |> fold (Symtab.update o rpair []) boring_consts
   4.175 -                 |> fold (do_formula pos) ts
   4.176 -  end
   4.177 +  in Symtab.empty |> fold (do_formula pos) ts end
   4.178  
   4.179  (*Inserts a dummy "constant" referring to the theory name, so that relevance
   4.180    takes the given theory into account.*)
   4.181 @@ -199,43 +210,41 @@
   4.182  
   4.183  (* A two-dimensional symbol table counts frequencies of constants. It's keyed
   4.184     first by constant name and second by its list of type instantiations. For the
   4.185 -   latter, we need a linear ordering on "pseudotype list". *)
   4.186 +   latter, we need a linear ordering on "pattern list". *)
   4.187  
   4.188 -fun pseudotype_ord p =
   4.189 +fun pattern_ord p =
   4.190    case p of
   4.191      (PVar, PVar) => EQUAL
   4.192 -  | (PVar, PType _) => LESS
   4.193 -  | (PType _, PVar) => GREATER
   4.194 -  | (PType q1, PType q2) =>
   4.195 -    prod_ord fast_string_ord (dict_ord pseudotype_ord) (q1, q2)
   4.196 +  | (PVar, PApp _) => LESS
   4.197 +  | (PApp _, PVar) => GREATER
   4.198 +  | (PApp q1, PApp q2) =>
   4.199 +    prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
   4.200  
   4.201  structure CTtab =
   4.202 -  Table(type key = pseudotype list val ord = dict_ord pseudotype_ord)
   4.203 +  Table(type key = pattern list val ord = dict_ord pattern_ord)
   4.204  
   4.205 -fun count_axiom_consts theory_relevant thy (_, th) =
   4.206 +fun count_axiom_consts theory_relevant thy =
   4.207    let
   4.208 -    fun do_const (a, T) =
   4.209 -      let val (c, cts) = pseudoconst_for thy (a, T) in
   4.210 -        (* Two-dimensional table update. Constant maps to types maps to
   4.211 -           count. *)
   4.212 -        CTtab.map_default (cts, 0) (Integer.add 1)
   4.213 -        |> Symtab.map_default (c, CTtab.empty)
   4.214 -      end
   4.215 -    fun do_term (Const x) = do_const x
   4.216 -      | do_term (Free x) = do_const x
   4.217 -      | do_term (t $ u) = do_term t #> do_term u
   4.218 -      | do_term (Abs (_, _, t)) = do_term t
   4.219 -      | do_term _ = I
   4.220 -  in th |> theory_const_prop_of theory_relevant |> do_term end
   4.221 +    fun do_const const (s, T) ts =
   4.222 +      (* Two-dimensional table update. Constant maps to types maps to count. *)
   4.223 +      CTtab.map_default (pconst_args thy const (s, T) ts, 0) (Integer.add 1)
   4.224 +      |> Symtab.map_default (s, CTtab.empty)
   4.225 +      #> fold do_term ts
   4.226 +    and do_term t =
   4.227 +      case strip_comb t of
   4.228 +        (Const x, ts) => do_const true x ts
   4.229 +      | (Free x, ts) => do_const false x ts
   4.230 +      | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
   4.231 +      | (_, ts) => fold do_term ts
   4.232 +  in do_term o theory_const_prop_of theory_relevant o snd end
   4.233  
   4.234  
   4.235  (**** Actual Filtering Code ****)
   4.236  
   4.237  (*The frequency of a constant is the sum of those of all instances of its type.*)
   4.238 -fun pseudoconst_freq match const_tab (c, cts) =
   4.239 -  CTtab.fold (fn (cts', m) => match (cts, cts') ? Integer.add m)
   4.240 +fun pconst_freq match const_tab (c, ps) =
   4.241 +  CTtab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
   4.242               (the (Symtab.lookup const_tab c)) 0
   4.243 -  handle Option.Option => 0
   4.244  
   4.245  
   4.246  (* A surprising number of theorems contain only a few significant constants.
   4.247 @@ -244,24 +253,23 @@
   4.248  (* "log" seems best in practice. A constant function of one ignores the constant
   4.249     frequencies. *)
   4.250  fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0)
   4.251 -(* TODO: experiment
   4.252 -fun irrel_log n = 0.5 + 1.0 / Math.ln (Real.fromInt n + 1.0)
   4.253 -*)
   4.254  fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
   4.255  
   4.256  (* FUDGE *)
   4.257 -val skolem_weight = 1.0
   4.258 -val abs_weight = 2.0
   4.259 +val abs_rel_weight = 0.5
   4.260 +val abs_irrel_weight = 2.0
   4.261 +val skolem_rel_weight = 2.0  (* impossible *)
   4.262 +val skolem_irrel_weight = 0.5
   4.263  
   4.264  (* Computes a constant's weight, as determined by its frequency. *)
   4.265 -val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
   4.266 -fun irrel_weight const_tab (c as (s, _)) =
   4.267 -  if String.isPrefix skolem_prefix s then skolem_weight
   4.268 -  else if String.isPrefix abs_prefix s then abs_weight
   4.269 -  else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
   4.270 -(* TODO: experiment
   4.271 -fun irrel_weight _ _ = 1.0
   4.272 -*)
   4.273 +fun generic_weight abs_weight skolem_weight logx f const_tab (c as (s, _)) =
   4.274 +  if s = abs_name then abs_weight
   4.275 +  else if String.isPrefix skolem_prefix s then skolem_weight
   4.276 +  else logx (pconst_freq (match_patterns o f) const_tab c)
   4.277 +
   4.278 +val rel_weight = generic_weight abs_rel_weight skolem_rel_weight rel_log I
   4.279 +val irrel_weight = generic_weight abs_irrel_weight skolem_irrel_weight irrel_log
   4.280 +                                  swap
   4.281  
   4.282  (* FUDGE *)
   4.283  fun locality_multiplier General = 1.0
   4.284 @@ -270,43 +278,33 @@
   4.285    | locality_multiplier Chained = 2.0
   4.286  
   4.287  fun axiom_weight loc const_tab relevant_consts axiom_consts =
   4.288 -  case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
   4.289 -                    ||> filter_out (pseudoconst_mem swap relevant_consts) of
   4.290 -    ([], []) => 0.0
   4.291 -  | (_, []) => 1.0
   4.292 +  case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
   4.293 +                    ||> filter_out (pconst_hyper_mem swap relevant_consts) of
   4.294 +    ([], _) => 0.0
   4.295    | (rel, irrel) =>
   4.296 -    let
   4.297 -      val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
   4.298 -                       |> curry Real.* (locality_multiplier loc)
   4.299 -      val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
   4.300 -      val res = rel_weight / (rel_weight + irrel_weight)
   4.301 -    in if Real.isFinite res then res else 0.0 end
   4.302 +    case irrel |> filter_out (pconst_mem swap rel) of
   4.303 +      [] => 1.0
   4.304 +    | irrel =>
   4.305 +      let
   4.306 +        val rel_weight =
   4.307 +          fold (curry Real.+ o rel_weight const_tab) rel 0.0
   4.308 +          |> curry Real.* (locality_multiplier loc)
   4.309 +        val irrel_weight =
   4.310 +          fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
   4.311 +        val res = rel_weight / (rel_weight + irrel_weight)
   4.312 +      in if Real.isFinite res then res else 0.0 end
   4.313  
   4.314 -(* TODO: experiment
   4.315 -fun debug_axiom_weight const_tab relevant_consts axiom_consts =
   4.316 -  case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
   4.317 -                    ||> filter_out (pseudoconst_mem swap relevant_consts) of
   4.318 -    ([], []) => 0.0
   4.319 -  | (_, []) => 1.0
   4.320 -  | (rel, irrel) =>
   4.321 -    let
   4.322 -val _ = tracing (PolyML.makestring ("REL: ", rel))
   4.323 -val _ = tracing (PolyML.makestring ("IRREL: ", irrel))
   4.324 -      val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
   4.325 -      val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
   4.326 -      val res = rel_weight / (rel_weight + irrel_weight)
   4.327 -    in if Real.isFinite res then res else 0.0 end
   4.328 -*)
   4.329 -
   4.330 -fun pseudoconsts_of_term thy t =
   4.331 -  Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
   4.332 -              (get_pseudoconsts thy true (SOME true) [t]) []
   4.333 +fun pconsts_in_axiom thy t =
   4.334 +  Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
   4.335 +              (get_pconsts thy true (SOME true) [t]) []
   4.336  fun pair_consts_axiom theory_relevant thy axiom =
   4.337 -  (axiom, axiom |> snd |> theory_const_prop_of theory_relevant
   4.338 -                |> pseudoconsts_of_term thy)
   4.339 +  case axiom |> snd |> theory_const_prop_of theory_relevant
   4.340 +             |> pconsts_in_axiom thy of
   4.341 +    [] => NONE
   4.342 +  | consts => SOME ((axiom, consts), NONE)
   4.343  
   4.344  type annotated_thm =
   4.345 -  (((unit -> string) * locality) * thm) * (string * pseudotype list) list
   4.346 +  (((unit -> string) * locality) * thm) * (string * pattern list) list
   4.347  
   4.348  fun take_most_relevant max_max_imperfect max_relevant remaining_max
   4.349                         (candidates : (annotated_thm * real) list) =
   4.350 @@ -321,18 +319,22 @@
   4.351      val ((accepts, more_rejects), rejects) =
   4.352        chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
   4.353    in
   4.354 -    trace_msg (fn () => "Number of candidates: " ^
   4.355 -                        string_of_int (length candidates));
   4.356 -    trace_msg (fn () => "Effective threshold: " ^
   4.357 -                        Real.toString (#2 (hd accepts)));
   4.358      trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^
   4.359 -        "): " ^ (accepts
   4.360 +        " of " ^ Int.toString (length candidates) ^ "): " ^ (accepts
   4.361                   |> map (fn ((((name, _), _), _), weight) =>
   4.362                              name () ^ " [" ^ Real.toString weight ^ "]")
   4.363                   |> commas));
   4.364      (accepts, more_rejects @ rejects)
   4.365    end
   4.366  
   4.367 +fun if_empty_replace_with_locality thy axioms loc tab =
   4.368 +  if Symtab.is_empty tab then
   4.369 +    get_pconsts thy false (SOME false)
   4.370 +        (map_filter (fn ((_, loc'), th) =>
   4.371 +                        if loc' = loc then SOME (prop_of th) else NONE) axioms)
   4.372 +  else
   4.373 +    tab
   4.374 +
   4.375  (* FUDGE *)
   4.376  val threshold_divisor = 2.0
   4.377  val ridiculous_threshold = 0.1
   4.378 @@ -342,8 +344,12 @@
   4.379                       ({add, del, ...} : relevance_override) axioms goal_ts =
   4.380    let
   4.381      val thy = ProofContext.theory_of ctxt
   4.382 -    val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
   4.383 -                         Symtab.empty
   4.384 +    val const_tab =
   4.385 +      fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
   4.386 +    val goal_const_tab =
   4.387 +      get_pconsts thy false (SOME false) goal_ts
   4.388 +      |> fold (if_empty_replace_with_locality thy axioms)
   4.389 +              [Chained, Local, Theory]
   4.390      val add_thms = maps (ProofContext.get_fact ctxt) add
   4.391      val del_thms = maps (ProofContext.get_fact ctxt) del
   4.392      val max_max_imperfect =
   4.393 @@ -373,7 +379,7 @@
   4.394                                     candidates
   4.395                val rel_const_tab' =
   4.396                  rel_const_tab
   4.397 -                |> fold (add_pseudoconst_to_table false)
   4.398 +                |> fold (add_pconst_to_table false)
   4.399                          (maps (snd o fst) accepts)
   4.400                fun is_dirty (c, _) =
   4.401                  Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
   4.402 @@ -389,14 +395,14 @@
   4.403                                          (ax, if exists is_dirty consts then NONE
   4.404                                               else SOME old_weight)))
   4.405                val threshold =
   4.406 -                threshold + (1.0 - threshold)
   4.407 -                * Math.pow (decay, Real.fromInt (length accepts))
   4.408 +                1.0 - (1.0 - threshold)
   4.409 +                      * Math.pow (decay, Real.fromInt (length accepts))
   4.410                val remaining_max = remaining_max - length accepts
   4.411              in
   4.412                trace_msg (fn () => "New or updated constants: " ^
   4.413                    commas (rel_const_tab' |> Symtab.dest
   4.414 -                          |> subtract (op =) (Symtab.dest rel_const_tab)
   4.415 -                          |> map string_for_super_pseudoconst));
   4.416 +                          |> subtract (op =) (rel_const_tab |> Symtab.dest)
   4.417 +                          |> map string_for_hyper_pconst));
   4.418                map (fst o fst) accepts @
   4.419                (if remaining_max = 0 then
   4.420                   game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects)
   4.421 @@ -431,14 +437,13 @@
   4.422                Real.toString threshold ^ ", constants: " ^
   4.423                commas (rel_const_tab |> Symtab.dest
   4.424                        |> filter (curry (op <>) [] o snd)
   4.425 -                      |> map string_for_super_pseudoconst));
   4.426 +                      |> map string_for_hyper_pconst));
   4.427            relevant [] [] hopeless hopeful
   4.428          end
   4.429    in
   4.430      axioms |> filter_out (member Thm.eq_thm del_thms o snd)
   4.431 -           |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
   4.432 -           |> iter 0 max_relevant threshold0
   4.433 -                   (get_pseudoconsts thy false (SOME false) goal_ts) []
   4.434 +           |> map_filter (pair_consts_axiom theory_relevant thy)
   4.435 +           |> iter 0 max_relevant threshold0 goal_const_tab []
   4.436             |> tap (fn res => trace_msg (fn () =>
   4.437                                  "Total relevant: " ^ Int.toString (length res)))
   4.438    end
   4.439 @@ -503,12 +508,17 @@
   4.440  val exists_sledgehammer_const =
   4.441    exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
   4.442  
   4.443 -fun is_strange_theorem th =
   4.444 +fun is_metastrange_theorem th =
   4.445    case head_of (concl_of th) of
   4.446        Const (a, _) => (a <> @{const_name Trueprop} andalso
   4.447                         a <> @{const_name "=="})
   4.448      | _ => false
   4.449  
   4.450 +fun is_that_fact th =
   4.451 +  String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
   4.452 +  andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
   4.453 +                           | _ => false) (prop_of th)
   4.454 +
   4.455  val type_has_top_sort =
   4.456    exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
   4.457  
   4.458 @@ -578,7 +588,7 @@
   4.459    let val t = prop_of thm in
   4.460      is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
   4.461      is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
   4.462 -    is_strange_theorem thm
   4.463 +    is_metastrange_theorem thm orelse is_that_fact thm
   4.464    end
   4.465  
   4.466  fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
   4.467 @@ -589,15 +599,15 @@
   4.468      val local_facts = ProofContext.facts_of ctxt
   4.469      val named_locals = local_facts |> Facts.dest_static []
   4.470      val is_chained = member Thm.eq_thm chained_ths
   4.471 -    (* Unnamed, not chained formulas with schematic variables are omitted,
   4.472 -       because they are rejected by the backticks (`...`) parser for some
   4.473 -       reason. *)
   4.474 +    (* Unnamed nonchained formulas with schematic variables are omitted, because
   4.475 +       they are rejected by the backticks (`...`) parser for some reason. *)
   4.476      fun is_good_unnamed_local th =
   4.477 +      not (Thm.has_name_hint th) andalso
   4.478 +      (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) andalso
   4.479        forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
   4.480 -      andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th))
   4.481      val unnamed_locals =
   4.482 -      local_facts |> Facts.props |> filter is_good_unnamed_local
   4.483 -                  |> map (pair "" o single)
   4.484 +      union Thm.eq_thm (Facts.props local_facts) chained_ths
   4.485 +      |> filter is_good_unnamed_local |> map (pair "" o single)
   4.486      val full_space =
   4.487        Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
   4.488      fun add_facts global foldx facts =
   4.489 @@ -667,8 +677,8 @@
   4.490                     theory_relevant (relevance_override as {add, del, only})
   4.491                     (ctxt, (chained_ths, _)) hyp_ts concl_t =
   4.492    let
   4.493 -    val decay = 1.0 - Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
   4.494 -                                1.0 / Real.fromInt (max_relevant + 1))
   4.495 +    val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
   4.496 +                          1.0 / Real.fromInt (max_relevant + 1))
   4.497      val add_thms = maps (ProofContext.get_fact ctxt) add
   4.498      val reserved = reserved_isar_keyword_table ()
   4.499      val axioms =
   4.500 @@ -689,7 +699,7 @@
   4.501       else
   4.502         relevance_filter ctxt threshold0 decay max_relevant theory_relevant
   4.503                          relevance_override axioms (concl_t :: hyp_ts))
   4.504 -    |> map (apfst (apfst (fn f => f ()))) |> sort_wrt (fst o fst)
   4.505 +    |> map (apfst (apfst (fn f => f ())))
   4.506    end
   4.507  
   4.508  end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Aug 27 14:25:29 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Aug 27 16:05:46 2010 +0200
     5.3 @@ -10,18 +10,16 @@
     5.4  sig
     5.5    type locality = Sledgehammer_Fact_Filter.locality
     5.6    type minimize_command = string list -> string
     5.7 -
     5.8 -  val metis_proof_text:
     5.9 -    bool * minimize_command * string * (string * locality) vector * thm * int
    5.10 -    -> string * (string * locality) list
    5.11 -  val isar_proof_text:
    5.12 +  type metis_params =
    5.13 +    bool * minimize_command * string * (string * locality) list vector * thm
    5.14 +    * int
    5.15 +  type isar_params =
    5.16      string Symtab.table * bool * int * Proof.context * int list list
    5.17 -    -> bool * minimize_command * string * (string * locality) vector * thm * int
    5.18 -    -> string * (string * locality) list
    5.19 -  val proof_text:
    5.20 -    bool -> string Symtab.table * bool * int * Proof.context * int list list
    5.21 -    -> bool * minimize_command * string * (string * locality) vector * thm * int
    5.22 -    -> string * (string * locality) list
    5.23 +  type text_result = string * (string * locality) list
    5.24 +
    5.25 +  val metis_proof_text : metis_params -> text_result
    5.26 +  val isar_proof_text : isar_params -> metis_params -> text_result
    5.27 +  val proof_text : bool -> isar_params -> metis_params -> text_result
    5.28  end;
    5.29  
    5.30  structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
    5.31 @@ -34,6 +32,11 @@
    5.32  open Sledgehammer_Translate
    5.33  
    5.34  type minimize_command = string list -> string
    5.35 +type metis_params =
    5.36 +  bool * minimize_command * string * (string * locality) list vector * thm * int
    5.37 +type isar_params =
    5.38 +  string Symtab.table * bool * int * Proof.context * int list list
    5.39 +type text_result = string * (string * locality) list
    5.40  
    5.41  (* Simple simplifications to ensure that sort annotations don't leave a trail of
    5.42     spurious "True"s. *)
    5.43 @@ -61,7 +64,7 @@
    5.44  fun index_in_shape x = find_index (exists (curry (op =) x))
    5.45  fun is_axiom_number axiom_names num =
    5.46    num > 0 andalso num <= Vector.length axiom_names andalso
    5.47 -  fst (Vector.sub (axiom_names, num - 1)) <> ""
    5.48 +  not (null (Vector.sub (axiom_names, num - 1)))
    5.49  fun is_conjecture_number conjecture_shape num =
    5.50    index_in_shape num conjecture_shape >= 0
    5.51  
    5.52 @@ -565,12 +568,10 @@
    5.53     "108. ... [input]". *)
    5.54  fun used_facts_in_atp_proof axiom_names atp_proof =
    5.55    let
    5.56 -    fun axiom_name_at_index num =
    5.57 +    fun axiom_names_at_index num =
    5.58        let val j = Int.fromString num |> the_default ~1 in
    5.59 -        if is_axiom_number axiom_names j then
    5.60 -          SOME (Vector.sub (axiom_names, j - 1))
    5.61 -        else
    5.62 -          NONE
    5.63 +        if is_axiom_number axiom_names j then Vector.sub (axiom_names, j - 1)
    5.64 +        else []
    5.65        end
    5.66      val tokens_of =
    5.67        String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
    5.68 @@ -579,17 +580,19 @@
    5.69            (case strip_prefix_and_unascii axiom_prefix (List.last rest) of
    5.70               SOME name =>
    5.71               if member (op =) rest "file" then
    5.72 -               SOME (name, find_first_in_vector axiom_names name General)
    5.73 +               ([(name, name |> find_first_in_list_vector axiom_names |> the)]
    5.74 +                handle Option.Option =>
    5.75 +                       error ("No such fact: " ^ quote name ^ "."))
    5.76               else
    5.77 -               axiom_name_at_index num
    5.78 -           | NONE => axiom_name_at_index num)
    5.79 +               axiom_names_at_index num
    5.80 +           | NONE => axiom_names_at_index num)
    5.81          else
    5.82 -          NONE
    5.83 -      | do_line (num :: "0" :: "Inp" :: _) = axiom_name_at_index num
    5.84 +          []
    5.85 +      | do_line (num :: "0" :: "Inp" :: _) = axiom_names_at_index num
    5.86        | do_line (num :: rest) =
    5.87 -        (case List.last rest of "input" => axiom_name_at_index num | _ => NONE)
    5.88 -      | do_line _ = NONE
    5.89 -  in atp_proof |> split_proof_lines |> map_filter (do_line o tokens_of) end
    5.90 +        (case List.last rest of "input" => axiom_names_at_index num | _ => [])
    5.91 +      | do_line _ = []
    5.92 +  in atp_proof |> split_proof_lines |> maps (do_line o tokens_of) end
    5.93  
    5.94  val indent_size = 2
    5.95  val no_label = ("", ~1)
    5.96 @@ -663,7 +666,7 @@
    5.97  
    5.98  fun add_fact_from_dep axiom_names num =
    5.99    if is_axiom_number axiom_names num then
   5.100 -    apsnd (insert (op =) (fst (Vector.sub (axiom_names, num - 1))))
   5.101 +    apsnd (union (op =) (map fst (Vector.sub (axiom_names, num - 1))))
   5.102    else
   5.103      apfst (insert (op =) (raw_prefix, num))
   5.104  
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 27 14:25:29 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 27 16:05:46 2010 +0200
     6.3 @@ -19,7 +19,7 @@
     6.4    val prepare_problem :
     6.5      Proof.context -> bool -> bool -> bool -> bool -> term list -> term
     6.6      -> ((string * 'a) * thm) list
     6.7 -    -> string problem * string Symtab.table * int * (string * 'a) vector
     6.8 +    -> string problem * string Symtab.table * int * (string * 'a) list vector
     6.9  end;
    6.10  
    6.11  structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
    6.12 @@ -271,7 +271,7 @@
    6.13      val (supers', arity_clauses) = make_arity_clauses thy tycons supers
    6.14      val class_rel_clauses = make_class_rel_clauses thy subs supers'
    6.15    in
    6.16 -    (Vector.fromList axiom_names,
    6.17 +    (axiom_names |> map single |> Vector.fromList,
    6.18       (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
    6.19    end
    6.20  
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Aug 27 14:25:29 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Aug 27 16:05:46 2010 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  
     7.5  signature SLEDGEHAMMER_UTIL =
     7.6  sig
     7.7 -  val find_first_in_vector : (''a * 'b) vector -> ''a -> 'b -> 'b
     7.8 +  val find_first_in_list_vector : (''a * 'b) list vector -> ''a -> 'b option
     7.9    val plural_s : int -> string
    7.10    val serial_commas : string -> string list -> string list
    7.11    val simplify_spaces : string -> string
    7.12 @@ -29,9 +29,9 @@
    7.13  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    7.14  struct
    7.15  
    7.16 -fun find_first_in_vector vec key default =
    7.17 -  Vector.foldl (fn ((key', value'), value) =>
    7.18 -                   if key' = key then value' else value) default vec
    7.19 +fun find_first_in_list_vector vec key =
    7.20 +  Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
    7.21 +                 | (_, value) => value) NONE vec
    7.22  
    7.23  fun plural_s n = if n = 1 then "" else "s"
    7.24