detect some unsound proofs before showing them to the user
authorblanchet
Thu Apr 21 22:18:28 2011 +0200 (2011-04-21)
changeset 42449494e4ac5b0f8
parent 42448 95b2626c75a8
child 42450 2765d4fb2b9c
detect some unsound proofs before showing them to the user
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Apr 21 21:14:06 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Apr 21 22:18:28 2011 +0200
     1.3 @@ -378,7 +378,7 @@
     1.4      val relevance_override = {add = [], del = [], only = false}
     1.5      val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
     1.6      val no_dangerous_types =
     1.7 -      Sledgehammer_ATP_Translate.types_dangerous_types type_sys
     1.8 +      Sledgehammer_ATP_Translate.type_system_types_dangerous_types type_sys
     1.9      val time_limit =
    1.10        (case hard_timeout of
    1.11          NONE => I
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Apr 21 21:14:06 2011 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Apr 21 22:18:28 2011 +0200
     2.3 @@ -126,7 +126,7 @@
     2.4           val subgoal = 1
     2.5           val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
     2.6           val no_dangerous_types =
     2.7 -           Sledgehammer_ATP_Translate.types_dangerous_types type_sys
     2.8 +           Sledgehammer_ATP_Translate.type_system_types_dangerous_types type_sys
     2.9           val facts =
    2.10             Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
    2.11                 relevance_thresholds
     3.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Apr 21 21:14:06 2011 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Apr 21 22:18:28 2011 +0200
     3.3 @@ -171,7 +171,6 @@
     3.4            end
     3.5        in add 0 |> apsnd SOME end
     3.6  
     3.7 -
     3.8  fun nice_term (ATerm (name, ts)) =
     3.9    nice_name name ##>> pool_map nice_term ts #>> ATerm
    3.10  fun nice_formula (AQuant (q, xs, phi)) =
     4.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Apr 21 21:14:06 2011 +0200
     4.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Apr 21 22:18:28 2011 +0200
     4.3 @@ -12,10 +12,10 @@
     4.4    type 'a uniform_formula = 'a ATP_Problem.uniform_formula
     4.5  
     4.6    datatype failure =
     4.7 -    Unprovable | IncompleteUnprovable | ProofMissing | CantConnect | TimedOut |
     4.8 -    OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
     4.9 -    NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed |
    4.10 -    InternalError | UnknownError of string
    4.11 +    Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof |
    4.12 +    CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld |
    4.13 +    NoPerl | NoLibwwwPerl | NoRealZ3 | MalformedInput | MalformedOutput |
    4.14 +    Interrupted | Crashed | InternalError | UnknownError of string
    4.15  
    4.16    type step_name = string * string option
    4.17  
    4.18 @@ -35,7 +35,7 @@
    4.19      bool -> bool -> bool -> int -> (string * string) list
    4.20      -> (failure * string) list -> string -> string * failure option
    4.21    val is_same_step : step_name * step_name -> bool
    4.22 -  val atp_proof_from_tstplike_string : bool -> string -> string proof
    4.23 +  val atp_proof_from_tstplike_proof : string -> string proof
    4.24    val map_term_names_in_atp_proof :
    4.25      (string -> string) -> string proof -> string proof
    4.26    val nasty_atp_proof : string Symtab.table -> string proof -> string proof
    4.27 @@ -47,10 +47,10 @@
    4.28  open ATP_Problem
    4.29  
    4.30  datatype failure =
    4.31 -  Unprovable | IncompleteUnprovable | ProofMissing | CantConnect | TimedOut |
    4.32 -  OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
    4.33 -  NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed |
    4.34 -  InternalError | UnknownError of string
    4.35 +  Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof |
    4.36 +  CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld |
    4.37 +  NoPerl | NoLibwwwPerl | NoRealZ3 | MalformedInput | MalformedOutput |
    4.38 +  Interrupted | Crashed | InternalError | UnknownError of string
    4.39  
    4.40  fun strip_spaces_in_list _ [] = []
    4.41    | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
    4.42 @@ -95,6 +95,9 @@
    4.43      "The prover gave up."
    4.44    | string_for_failure ProofMissing =
    4.45      "The prover claims the conjecture is a theorem but did not provide a proof."
    4.46 +  | string_for_failure UnsoundProof =
    4.47 +    "The prover found a type-incorrect proof. (Or, very unlikely, your axioms \
    4.48 +    \are inconsistent.)"
    4.49    | string_for_failure CantConnect = "Cannot connect to remote server."
    4.50    | string_for_failure TimedOut = "Timed out."
    4.51    | string_for_failure OutOfResources = "The prover ran out of resources."
    4.52 @@ -366,11 +369,12 @@
    4.53      Inference (name, u, map_filter (clean_up_dependency seen) deps) ::
    4.54      clean_up_dependencies (name :: seen) steps
    4.55  
    4.56 -fun atp_proof_from_tstplike_string clean =
    4.57 -  suffix "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
    4.58 -  #> parse_proof
    4.59 -  #> clean ? (sort (step_name_ord o pairself step_name)
    4.60 -              #> clean_up_dependencies [])
    4.61 +fun atp_proof_from_tstplike_proof "" = []
    4.62 +  | atp_proof_from_tstplike_proof s =
    4.63 +    s ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
    4.64 +    |> parse_proof
    4.65 +    |> sort (step_name_ord o pairself step_name)
    4.66 +    |> clean_up_dependencies []
    4.67  
    4.68  fun map_term_names_in_term f (ATerm (s, ts)) =
    4.69    ATerm (f s, map (map_term_names_in_term f) ts)
     5.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 21 21:14:06 2011 +0200
     5.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 21 22:18:28 2011 +0200
     5.3 @@ -243,6 +243,7 @@
     5.4     known_failures =
     5.5       [(Unprovable, "UNPROVABLE"),
     5.6        (IncompleteUnprovable, "CANNOT PROVE"),
     5.7 +      (IncompleteUnprovable, "SZS status GaveUp"),
     5.8        (ProofMissing, "[predicate definition introduction]"),
     5.9        (ProofMissing, "predicate_definition_introduction,[]"), (* TSTP *)
    5.10        (TimedOut, "SZS status Timeout"),
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Apr 21 21:14:06 2011 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Apr 21 22:18:28 2011 +0200
     6.3 @@ -8,11 +8,12 @@
     6.4  
     6.5  signature SLEDGEHAMMER_ATP_RECONSTRUCT =
     6.6  sig
     6.7 +  type 'a proof = 'a ATP_Proof.proof
     6.8    type locality = Sledgehammer_Filter.locality
     6.9    type type_system = Sledgehammer_ATP_Translate.type_system
    6.10    type minimize_command = string list -> string
    6.11    type metis_params =
    6.12 -    string * type_system * minimize_command * string
    6.13 +    string * type_system * minimize_command * string proof
    6.14      * (string * locality) list vector * thm * int
    6.15    type isar_params =
    6.16      string Symtab.table * bool * int * Proof.context * int list list
    6.17 @@ -21,6 +22,8 @@
    6.18    val repair_conjecture_shape_and_fact_names :
    6.19      string -> int list list -> (string * locality) list vector
    6.20      -> int list list * (string * locality) list vector
    6.21 +  val is_unsound_proof :
    6.22 +    int list list -> (string * locality) list vector -> string proof -> bool
    6.23    val apply_on_subgoal : string -> int -> int -> string
    6.24    val command_call : string -> string list -> string
    6.25    val try_command_line : string -> string -> string
    6.26 @@ -45,7 +48,7 @@
    6.27  
    6.28  type minimize_command = string list -> string
    6.29  type metis_params =
    6.30 -  string * type_system * minimize_command * string
    6.31 +  string * type_system * minimize_command * string proof
    6.32    * (string * locality) list vector * thm * int
    6.33  type isar_params =
    6.34    string Symtab.table * bool * int * Proof.context * int list list
    6.35 @@ -115,39 +118,6 @@
    6.36    else
    6.37      (conjecture_shape, fact_names)
    6.38  
    6.39 -
    6.40 -(** Soft-core proof reconstruction: Metis one-liner **)
    6.41 -
    6.42 -fun string_for_label (s, num) = s ^ string_of_int num
    6.43 -
    6.44 -fun set_settings "" = ""
    6.45 -  | set_settings settings = "using [[" ^ settings ^ "]] "
    6.46 -fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by "
    6.47 -  | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply "
    6.48 -  | apply_on_subgoal settings i n =
    6.49 -    "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n
    6.50 -fun command_call name [] = name
    6.51 -  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
    6.52 -fun try_command_line banner command =
    6.53 -  banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
    6.54 -fun using_labels [] = ""
    6.55 -  | using_labels ls =
    6.56 -    "using " ^ space_implode " " (map string_for_label ls) ^ " "
    6.57 -fun metis_name type_sys =
    6.58 -  if types_dangerous_types type_sys then "metisFT" else "metis"
    6.59 -fun metis_call type_sys ss = command_call (metis_name type_sys) ss
    6.60 -fun metis_command type_sys i n (ls, ss) =
    6.61 -  using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss
    6.62 -fun metis_line banner type_sys i n ss =
    6.63 -  try_command_line banner (metis_command type_sys i n ([], ss))
    6.64 -fun minimize_line _ [] = ""
    6.65 -  | minimize_line minimize_command ss =
    6.66 -    case minimize_command ss of
    6.67 -      "" => ""
    6.68 -    | command =>
    6.69 -      "\nTo minimize the number of lemmas, try this: " ^
    6.70 -      Markup.markup Markup.sendback command ^ "."
    6.71 -
    6.72  val vampire_step_prefix = "f" (* grrr... *)
    6.73  
    6.74  fun resolve_fact fact_names ((_, SOME s)) =
    6.75 @@ -168,27 +138,77 @@
    6.76          []
    6.77      | NONE => []
    6.78  
    6.79 +fun resolve_conjecture conjecture_shape (num, s_opt) =
    6.80 +  let
    6.81 +    val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
    6.82 +              SOME s => Int.fromString s |> the_default ~1
    6.83 +            | NONE => case Int.fromString num of
    6.84 +                        SOME j => find_index (exists (curry (op =) j))
    6.85 +                                             conjecture_shape
    6.86 +                      | NONE => ~1
    6.87 +  in if k >= 0 then [k] else [] end
    6.88 +
    6.89 +fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape
    6.90 +fun is_conjecture conjecture_shape =
    6.91 +  not o null o resolve_conjecture conjecture_shape
    6.92 +
    6.93  fun add_fact fact_names (Inference (name, _, [])) =
    6.94      append (resolve_fact fact_names name)
    6.95    | add_fact _ _ = I
    6.96  
    6.97 -fun used_facts_in_tstplike_proof fact_names tstplike_proof =
    6.98 -  if tstplike_proof = "" then
    6.99 -    Vector.foldl (op @) [] fact_names
   6.100 -  else
   6.101 -    tstplike_proof
   6.102 -    |> atp_proof_from_tstplike_string false
   6.103 -    |> rpair [] |-> fold (add_fact fact_names)
   6.104 +fun used_facts_in_atp_proof fact_names atp_proof =
   6.105 +  if null atp_proof then Vector.foldl (op @) [] fact_names
   6.106 +  else fold (add_fact fact_names) atp_proof []
   6.107 +
   6.108 +fun is_conjecture_referred_to_in_proof conjecture_shape =
   6.109 +  exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
   6.110 +           | _ => false)
   6.111 +
   6.112 +fun is_unsound_proof conjecture_shape fact_names =
   6.113 +  (not o is_conjecture_referred_to_in_proof conjecture_shape) andf
   6.114 +  forall (is_global_locality o snd) o used_facts_in_atp_proof fact_names
   6.115 +
   6.116 +(** Soft-core proof reconstruction: Metis one-liner **)
   6.117 +
   6.118 +fun string_for_label (s, num) = s ^ string_of_int num
   6.119 +
   6.120 +fun set_settings "" = ""
   6.121 +  | set_settings settings = "using [[" ^ settings ^ "]] "
   6.122 +fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by "
   6.123 +  | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply "
   6.124 +  | apply_on_subgoal settings i n =
   6.125 +    "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n
   6.126 +fun command_call name [] = name
   6.127 +  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
   6.128 +fun try_command_line banner command =
   6.129 +  banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
   6.130 +fun using_labels [] = ""
   6.131 +  | using_labels ls =
   6.132 +    "using " ^ space_implode " " (map string_for_label ls) ^ " "
   6.133 +fun metis_name type_sys =
   6.134 +  if type_system_types_dangerous_types type_sys then "metisFT" else "metis"
   6.135 +fun metis_call type_sys ss = command_call (metis_name type_sys) ss
   6.136 +fun metis_command type_sys i n (ls, ss) =
   6.137 +  using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss
   6.138 +fun metis_line banner type_sys i n ss =
   6.139 +  try_command_line banner (metis_command type_sys i n ([], ss))
   6.140 +fun minimize_line _ [] = ""
   6.141 +  | minimize_line minimize_command ss =
   6.142 +    case minimize_command ss of
   6.143 +      "" => ""
   6.144 +    | command =>
   6.145 +      "\nTo minimize the number of lemmas, try this: " ^
   6.146 +      Markup.markup Markup.sendback command ^ "."
   6.147  
   6.148  val split_used_facts =
   6.149    List.partition (curry (op =) Chained o snd)
   6.150    #> pairself (sort_distinct (string_ord o pairself fst))
   6.151  
   6.152 -fun metis_proof_text (banner, type_sys, minimize_command, tstplike_proof,
   6.153 -                      fact_names, goal, i) =
   6.154 +fun metis_proof_text (banner, type_sys, minimize_command, atp_proof, fact_names,
   6.155 +                      goal, i) =
   6.156    let
   6.157      val (chained_lemmas, other_lemmas) =
   6.158 -      split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof)
   6.159 +      split_used_facts (used_facts_in_atp_proof fact_names atp_proof)
   6.160      val n = Logic.count_prems (prop_of goal)
   6.161    in
   6.162      (metis_line banner type_sys i n (map fst other_lemmas) ^
   6.163 @@ -196,7 +216,6 @@
   6.164       other_lemmas @ chained_lemmas)
   6.165    end
   6.166  
   6.167 -
   6.168  (** Hard-core proof reconstruction: structured Isar proofs **)
   6.169  
   6.170  (* Simple simplifications to ensure that sort annotations don't leave a trail of
   6.171 @@ -241,19 +260,6 @@
   6.172  val assum_prefix = "A"
   6.173  val have_prefix = "F"
   6.174  
   6.175 -fun resolve_conjecture conjecture_shape (num, s_opt) =
   6.176 -  let
   6.177 -    val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
   6.178 -              SOME s => Int.fromString s |> the_default ~1
   6.179 -            | NONE => case Int.fromString num of
   6.180 -                        SOME j => find_index (exists (curry (op =) j))
   6.181 -                                             conjecture_shape
   6.182 -                      | NONE => ~1
   6.183 -  in if k >= 0 then [k] else [] end
   6.184 -
   6.185 -fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape
   6.186 -fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
   6.187 -
   6.188  fun raw_label_for_name conjecture_shape name =
   6.189    case resolve_conjecture conjecture_shape name of
   6.190      [j] => (conjecture_prefix, j)
   6.191 @@ -621,12 +627,11 @@
   6.192      else
   6.193        s
   6.194  
   6.195 -fun isar_proof_from_tstplike_proof pool ctxt type_sys tfrees isar_shrink_factor
   6.196 -        tstplike_proof conjecture_shape fact_names params frees =
   6.197 +fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor
   6.198 +        atp_proof conjecture_shape fact_names params frees =
   6.199    let
   6.200      val lines =
   6.201 -      tstplike_proof
   6.202 -      |> atp_proof_from_tstplike_string true
   6.203 +      atp_proof
   6.204        |> nasty_atp_proof pool
   6.205        |> map_term_names_in_atp_proof repair_name
   6.206        |> decode_lines ctxt type_sys tfrees
   6.207 @@ -929,8 +934,7 @@
   6.208    in do_proof end
   6.209  
   6.210  fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   6.211 -                    (metis_params as (_, type_sys, _, tstplike_proof,
   6.212 -                                      fact_names, goal, i)) =
   6.213 +        (metis_params as (_, type_sys, _, atp_proof, fact_names, goal, i)) =
   6.214    let
   6.215      val (params, hyp_ts, concl_t) = strip_subgoal goal i
   6.216      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   6.217 @@ -938,9 +942,9 @@
   6.218      val n = Logic.count_prems (prop_of goal)
   6.219      val (one_line_proof, lemma_names) = metis_proof_text metis_params
   6.220      fun isar_proof_for () =
   6.221 -      case isar_proof_from_tstplike_proof pool ctxt type_sys tfrees
   6.222 -               isar_shrink_factor tstplike_proof conjecture_shape fact_names
   6.223 -               params frees
   6.224 +      case isar_proof_from_atp_proof pool ctxt type_sys tfrees
   6.225 +               isar_shrink_factor atp_proof conjecture_shape fact_names params
   6.226 +               frees
   6.227             |> redirect_proof hyp_ts concl_t
   6.228             |> kill_duplicate_assumptions_in_proof
   6.229             |> then_chain_proof
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Apr 21 21:14:06 2011 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Apr 21 22:18:28 2011 +0200
     7.3 @@ -21,7 +21,8 @@
     7.4    val precise_overloaded_args : bool Unsynchronized.ref
     7.5    val fact_prefix : string
     7.6    val conjecture_prefix : string
     7.7 -  val types_dangerous_types : type_system -> bool
     7.8 +  val is_type_system_sound : type_system -> bool
     7.9 +  val type_system_types_dangerous_types : type_system -> bool
    7.10    val num_atp_type_args : theory -> type_system -> string -> int
    7.11    val translate_atp_fact :
    7.12      Proof.context -> bool -> (string * 'a) * thm
    7.13 @@ -67,8 +68,11 @@
    7.14    Mangled |
    7.15    No_Types
    7.16  
    7.17 -fun types_dangerous_types (Tags _) = true
    7.18 -  | types_dangerous_types _ = false
    7.19 +fun is_type_system_sound (Tags true) = true
    7.20 +  | is_type_system_sound _ = false
    7.21 +
    7.22 +fun type_system_types_dangerous_types (Tags _) = true
    7.23 +  | type_system_types_dangerous_types _ = false
    7.24  
    7.25  (* This is an approximation. If it returns "true" for a constant that isn't
    7.26     overloaded (i.e., that has one uniform definition), needless clutter is
    7.27 @@ -289,7 +293,7 @@
    7.28  
    7.29  fun get_helper_facts ctxt explicit_forall type_sys formulas =
    7.30    let
    7.31 -    val no_dangerous_types = types_dangerous_types type_sys
    7.32 +    val no_dangerous_types = type_system_types_dangerous_types type_sys
    7.33      val ct = init_counters |> fold count_formula formulas
    7.34      fun is_used s = the (Symtab.lookup ct s) > 0
    7.35      fun dub c needs_full_types (th, j) =
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Apr 21 21:14:06 2011 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Apr 21 22:18:28 2011 +0200
     8.3 @@ -36,6 +36,7 @@
     8.4       only : bool}
     8.5  
     8.6    val trace : bool Unsynchronized.ref
     8.7 +  val is_global_locality : locality -> bool
     8.8    val fact_from_ref :
     8.9      Proof.context -> unit Symtab.table -> thm list
    8.10      -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
    8.11 @@ -66,6 +67,12 @@
    8.12  
    8.13  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
    8.14  
    8.15 +(* (quasi-)underapproximation of the truth *)
    8.16 +fun is_global_locality Local = false
    8.17 +  | is_global_locality Assum = false
    8.18 +  | is_global_locality Chained = false
    8.19 +  | is_global_locality _ = true
    8.20 +
    8.21  type relevance_fudge =
    8.22    {allow_ext : bool,
    8.23     local_const_multiplier : real,
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 21:14:06 2011 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 22:18:28 2011 +0200
     9.3 @@ -457,23 +457,37 @@
     9.4                         else
     9.5                           I)
     9.6                    |>> (if measure_run_time then split_time else rpair NONE)
     9.7 -                val (tstplike_proof, outcome) =
     9.8 +                val (atp_proof, outcome) =
     9.9                    extract_tstplike_proof_and_outcome debug verbose complete
    9.10                        res_code proof_delims known_failures output
    9.11 +                  |>> atp_proof_from_tstplike_proof
    9.12 +                val (conjecture_shape, fact_names) =
    9.13 +                  if is_none outcome then
    9.14 +                    repair_conjecture_shape_and_fact_names output
    9.15 +                        conjecture_shape fact_names
    9.16 +                  else
    9.17 +                    (conjecture_shape, fact_names) (* don't bother repairing *)
    9.18 +                val outcome =
    9.19 +                  if is_none outcome andalso
    9.20 +                     not (is_type_system_sound type_sys) andalso
    9.21 +                     is_unsound_proof conjecture_shape fact_names atp_proof then
    9.22 +                    SOME UnsoundProof
    9.23 +                  else
    9.24 +                    outcome
    9.25                in
    9.26                  ((pool, conjecture_shape, fact_names),
    9.27 -                 (output, msecs, tstplike_proof, outcome))
    9.28 +                 (output, msecs, atp_proof, outcome))
    9.29                end
    9.30              val timer = Timer.startRealTimer ()
    9.31              fun maybe_run_slice slice (_, (_, msecs0, _, SOME _)) =
    9.32                  run_slice slice (Time.- (timeout, Timer.checkRealTimer timer))
    9.33 -                |> (fn (stuff, (output, msecs, tstplike_proof, outcome)) =>
    9.34 -                       (stuff, (output, int_opt_add msecs0 msecs,
    9.35 -                                tstplike_proof, outcome)))
    9.36 +                |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
    9.37 +                       (stuff, (output, int_opt_add msecs0 msecs, atp_proof,
    9.38 +                                outcome)))
    9.39                | maybe_run_slice _ result = result
    9.40            in
    9.41              ((Symtab.empty, [], Vector.fromList []),
    9.42 -             ("", SOME 0, "", SOME InternalError))
    9.43 +             ("", SOME 0, [], SOME InternalError))
    9.44              |> fold maybe_run_slice actual_slices
    9.45            end
    9.46          else
    9.47 @@ -489,10 +503,8 @@
    9.48        else
    9.49          File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
    9.50      val ((pool, conjecture_shape, fact_names),
    9.51 -         (output, msecs, tstplike_proof, outcome)) =
    9.52 +         (output, msecs, atp_proof, outcome)) =
    9.53        with_path cleanup export run_on problem_path_name
    9.54 -    val (conjecture_shape, fact_names) =
    9.55 -      repair_conjecture_shape_and_fact_names output conjecture_shape fact_names
    9.56      val important_message =
    9.57        if not auto andalso random () <= atp_important_message_keep_factor then
    9.58          extract_important_message output
    9.59 @@ -511,8 +523,8 @@
    9.60           "")
    9.61      val isar_params = (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
    9.62      val metis_params =
    9.63 -      (proof_banner auto, type_sys, minimize_command, tstplike_proof,
    9.64 -       fact_names, goal, subgoal)
    9.65 +      (proof_banner auto, type_sys, minimize_command, atp_proof, fact_names,
    9.66 +       goal, subgoal)
    9.67      val (outcome, (message, used_facts)) =
    9.68        case outcome of
    9.69          NONE =>
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Apr 21 21:14:06 2011 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Apr 21 22:18:28 2011 +0200
    10.3 @@ -183,7 +183,7 @@
    10.4        val thy = Proof_Context.theory_of ctxt
    10.5        val {facts = chained_ths, goal, ...} = Proof.goal state
    10.6        val (_, hyp_ts, concl_t) = strip_subgoal goal i
    10.7 -      val no_dangerous_types = types_dangerous_types type_sys
    10.8 +      val no_dangerous_types = type_system_types_dangerous_types type_sys
    10.9        val _ = () |> not blocking ? kill_provers
   10.10        val _ = case find_first (not o is_prover_supported ctxt) provers of
   10.11                  SOME name => error ("No such prover: " ^ name ^ ".")
    11.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 21 21:14:06 2011 +0200
    11.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 21 22:18:28 2011 +0200
    11.3 @@ -33,7 +33,7 @@
    11.4      val relevance_override = {add = [], del = [], only = false}
    11.5      val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
    11.6      val no_dangerous_types =
    11.7 -      Sledgehammer_ATP_Translate.types_dangerous_types type_sys
    11.8 +      Sledgehammer_ATP_Translate.type_system_types_dangerous_types type_sys
    11.9      val facts =
   11.10        Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
   11.11            relevance_thresholds