--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 21 22:18:28 2011 +0200
@@ -378,7 +378,7 @@
val relevance_override = {add = [], del = [], only = false}
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
val no_dangerous_types =
- Sledgehammer_ATP_Translate.types_dangerous_types type_sys
+ Sledgehammer_ATP_Translate.type_system_types_dangerous_types type_sys
val time_limit =
(case hard_timeout of
NONE => I
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Apr 21 22:18:28 2011 +0200
@@ -126,7 +126,7 @@
val subgoal = 1
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
val no_dangerous_types =
- Sledgehammer_ATP_Translate.types_dangerous_types type_sys
+ Sledgehammer_ATP_Translate.type_system_types_dangerous_types type_sys
val facts =
Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
relevance_thresholds
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Apr 21 22:18:28 2011 +0200
@@ -171,7 +171,6 @@
end
in add 0 |> apsnd SOME end
-
fun nice_term (ATerm (name, ts)) =
nice_name name ##>> pool_map nice_term ts #>> ATerm
fun nice_formula (AQuant (q, xs, phi)) =
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Apr 21 22:18:28 2011 +0200
@@ -12,10 +12,10 @@
type 'a uniform_formula = 'a ATP_Problem.uniform_formula
datatype failure =
- Unprovable | IncompleteUnprovable | ProofMissing | CantConnect | TimedOut |
- OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
- NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed |
- InternalError | UnknownError of string
+ Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof |
+ CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld |
+ NoPerl | NoLibwwwPerl | NoRealZ3 | MalformedInput | MalformedOutput |
+ Interrupted | Crashed | InternalError | UnknownError of string
type step_name = string * string option
@@ -35,7 +35,7 @@
bool -> bool -> bool -> int -> (string * string) list
-> (failure * string) list -> string -> string * failure option
val is_same_step : step_name * step_name -> bool
- val atp_proof_from_tstplike_string : bool -> string -> string proof
+ val atp_proof_from_tstplike_proof : string -> string proof
val map_term_names_in_atp_proof :
(string -> string) -> string proof -> string proof
val nasty_atp_proof : string Symtab.table -> string proof -> string proof
@@ -47,10 +47,10 @@
open ATP_Problem
datatype failure =
- Unprovable | IncompleteUnprovable | ProofMissing | CantConnect | TimedOut |
- OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
- NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed |
- InternalError | UnknownError of string
+ Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof |
+ CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld |
+ NoPerl | NoLibwwwPerl | NoRealZ3 | MalformedInput | MalformedOutput |
+ Interrupted | Crashed | InternalError | UnknownError of string
fun strip_spaces_in_list _ [] = []
| strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
@@ -95,6 +95,9 @@
"The prover gave up."
| string_for_failure ProofMissing =
"The prover claims the conjecture is a theorem but did not provide a proof."
+ | string_for_failure UnsoundProof =
+ "The prover found a type-incorrect proof. (Or, very unlikely, your axioms \
+ \are inconsistent.)"
| string_for_failure CantConnect = "Cannot connect to remote server."
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "The prover ran out of resources."
@@ -366,11 +369,12 @@
Inference (name, u, map_filter (clean_up_dependency seen) deps) ::
clean_up_dependencies (name :: seen) steps
-fun atp_proof_from_tstplike_string clean =
- suffix "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
- #> parse_proof
- #> clean ? (sort (step_name_ord o pairself step_name)
- #> clean_up_dependencies [])
+fun atp_proof_from_tstplike_proof "" = []
+ | atp_proof_from_tstplike_proof s =
+ s ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
+ |> parse_proof
+ |> sort (step_name_ord o pairself step_name)
+ |> clean_up_dependencies []
fun map_term_names_in_term f (ATerm (s, ts)) =
ATerm (f s, map (map_term_names_in_term f) ts)
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Apr 21 22:18:28 2011 +0200
@@ -243,6 +243,7 @@
known_failures =
[(Unprovable, "UNPROVABLE"),
(IncompleteUnprovable, "CANNOT PROVE"),
+ (IncompleteUnprovable, "SZS status GaveUp"),
(ProofMissing, "[predicate definition introduction]"),
(ProofMissing, "predicate_definition_introduction,[]"), (* TSTP *)
(TimedOut, "SZS status Timeout"),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu Apr 21 22:18:28 2011 +0200
@@ -8,11 +8,12 @@
signature SLEDGEHAMMER_ATP_RECONSTRUCT =
sig
+ type 'a proof = 'a ATP_Proof.proof
type locality = Sledgehammer_Filter.locality
type type_system = Sledgehammer_ATP_Translate.type_system
type minimize_command = string list -> string
type metis_params =
- string * type_system * minimize_command * string
+ string * type_system * minimize_command * string proof
* (string * locality) list vector * thm * int
type isar_params =
string Symtab.table * bool * int * Proof.context * int list list
@@ -21,6 +22,8 @@
val repair_conjecture_shape_and_fact_names :
string -> int list list -> (string * locality) list vector
-> int list list * (string * locality) list vector
+ val is_unsound_proof :
+ int list list -> (string * locality) list vector -> string proof -> bool
val apply_on_subgoal : string -> int -> int -> string
val command_call : string -> string list -> string
val try_command_line : string -> string -> string
@@ -45,7 +48,7 @@
type minimize_command = string list -> string
type metis_params =
- string * type_system * minimize_command * string
+ string * type_system * minimize_command * string proof
* (string * locality) list vector * thm * int
type isar_params =
string Symtab.table * bool * int * Proof.context * int list list
@@ -115,39 +118,6 @@
else
(conjecture_shape, fact_names)
-
-(** Soft-core proof reconstruction: Metis one-liner **)
-
-fun string_for_label (s, num) = s ^ string_of_int num
-
-fun set_settings "" = ""
- | set_settings settings = "using [[" ^ settings ^ "]] "
-fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by "
- | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply "
- | apply_on_subgoal settings i n =
- "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n
-fun command_call name [] = name
- | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
-fun try_command_line banner command =
- banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
-fun using_labels [] = ""
- | using_labels ls =
- "using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun metis_name type_sys =
- if types_dangerous_types type_sys then "metisFT" else "metis"
-fun metis_call type_sys ss = command_call (metis_name type_sys) ss
-fun metis_command type_sys i n (ls, ss) =
- using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss
-fun metis_line banner type_sys i n ss =
- try_command_line banner (metis_command type_sys i n ([], ss))
-fun minimize_line _ [] = ""
- | minimize_line minimize_command ss =
- case minimize_command ss of
- "" => ""
- | command =>
- "\nTo minimize the number of lemmas, try this: " ^
- Markup.markup Markup.sendback command ^ "."
-
val vampire_step_prefix = "f" (* grrr... *)
fun resolve_fact fact_names ((_, SOME s)) =
@@ -168,27 +138,77 @@
[]
| NONE => []
+fun resolve_conjecture conjecture_shape (num, s_opt) =
+ let
+ val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
+ SOME s => Int.fromString s |> the_default ~1
+ | NONE => case Int.fromString num of
+ SOME j => find_index (exists (curry (op =) j))
+ conjecture_shape
+ | NONE => ~1
+ in if k >= 0 then [k] else [] end
+
+fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape
+fun is_conjecture conjecture_shape =
+ not o null o resolve_conjecture conjecture_shape
+
fun add_fact fact_names (Inference (name, _, [])) =
append (resolve_fact fact_names name)
| add_fact _ _ = I
-fun used_facts_in_tstplike_proof fact_names tstplike_proof =
- if tstplike_proof = "" then
- Vector.foldl (op @) [] fact_names
- else
- tstplike_proof
- |> atp_proof_from_tstplike_string false
- |> rpair [] |-> fold (add_fact fact_names)
+fun used_facts_in_atp_proof fact_names atp_proof =
+ if null atp_proof then Vector.foldl (op @) [] fact_names
+ else fold (add_fact fact_names) atp_proof []
+
+fun is_conjecture_referred_to_in_proof conjecture_shape =
+ exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
+ | _ => false)
+
+fun is_unsound_proof conjecture_shape fact_names =
+ (not o is_conjecture_referred_to_in_proof conjecture_shape) andf
+ forall (is_global_locality o snd) o used_facts_in_atp_proof fact_names
+
+(** Soft-core proof reconstruction: Metis one-liner **)
+
+fun string_for_label (s, num) = s ^ string_of_int num
+
+fun set_settings "" = ""
+ | set_settings settings = "using [[" ^ settings ^ "]] "
+fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by "
+ | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply "
+ | apply_on_subgoal settings i n =
+ "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n
+fun command_call name [] = name
+ | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+fun try_command_line banner command =
+ banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
+fun using_labels [] = ""
+ | using_labels ls =
+ "using " ^ space_implode " " (map string_for_label ls) ^ " "
+fun metis_name type_sys =
+ if type_system_types_dangerous_types type_sys then "metisFT" else "metis"
+fun metis_call type_sys ss = command_call (metis_name type_sys) ss
+fun metis_command type_sys i n (ls, ss) =
+ using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss
+fun metis_line banner type_sys i n ss =
+ try_command_line banner (metis_command type_sys i n ([], ss))
+fun minimize_line _ [] = ""
+ | minimize_line minimize_command ss =
+ case minimize_command ss of
+ "" => ""
+ | command =>
+ "\nTo minimize the number of lemmas, try this: " ^
+ Markup.markup Markup.sendback command ^ "."
val split_used_facts =
List.partition (curry (op =) Chained o snd)
#> pairself (sort_distinct (string_ord o pairself fst))
-fun metis_proof_text (banner, type_sys, minimize_command, tstplike_proof,
- fact_names, goal, i) =
+fun metis_proof_text (banner, type_sys, minimize_command, atp_proof, fact_names,
+ goal, i) =
let
val (chained_lemmas, other_lemmas) =
- split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof)
+ split_used_facts (used_facts_in_atp_proof fact_names atp_proof)
val n = Logic.count_prems (prop_of goal)
in
(metis_line banner type_sys i n (map fst other_lemmas) ^
@@ -196,7 +216,6 @@
other_lemmas @ chained_lemmas)
end
-
(** Hard-core proof reconstruction: structured Isar proofs **)
(* Simple simplifications to ensure that sort annotations don't leave a trail of
@@ -241,19 +260,6 @@
val assum_prefix = "A"
val have_prefix = "F"
-fun resolve_conjecture conjecture_shape (num, s_opt) =
- let
- val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
- SOME s => Int.fromString s |> the_default ~1
- | NONE => case Int.fromString num of
- SOME j => find_index (exists (curry (op =) j))
- conjecture_shape
- | NONE => ~1
- in if k >= 0 then [k] else [] end
-
-fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape
-fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
-
fun raw_label_for_name conjecture_shape name =
case resolve_conjecture conjecture_shape name of
[j] => (conjecture_prefix, j)
@@ -621,12 +627,11 @@
else
s
-fun isar_proof_from_tstplike_proof pool ctxt type_sys tfrees isar_shrink_factor
- tstplike_proof conjecture_shape fact_names params frees =
+fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor
+ atp_proof conjecture_shape fact_names params frees =
let
val lines =
- tstplike_proof
- |> atp_proof_from_tstplike_string true
+ atp_proof
|> nasty_atp_proof pool
|> map_term_names_in_atp_proof repair_name
|> decode_lines ctxt type_sys tfrees
@@ -929,8 +934,7 @@
in do_proof end
fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (metis_params as (_, type_sys, _, tstplike_proof,
- fact_names, goal, i)) =
+ (metis_params as (_, type_sys, _, atp_proof, fact_names, goal, i)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal goal i
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
@@ -938,9 +942,9 @@
val n = Logic.count_prems (prop_of goal)
val (one_line_proof, lemma_names) = metis_proof_text metis_params
fun isar_proof_for () =
- case isar_proof_from_tstplike_proof pool ctxt type_sys tfrees
- isar_shrink_factor tstplike_proof conjecture_shape fact_names
- params frees
+ case isar_proof_from_atp_proof pool ctxt type_sys tfrees
+ isar_shrink_factor atp_proof conjecture_shape fact_names params
+ frees
|> redirect_proof hyp_ts concl_t
|> kill_duplicate_assumptions_in_proof
|> then_chain_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Apr 21 22:18:28 2011 +0200
@@ -21,7 +21,8 @@
val precise_overloaded_args : bool Unsynchronized.ref
val fact_prefix : string
val conjecture_prefix : string
- val types_dangerous_types : type_system -> bool
+ val is_type_system_sound : type_system -> bool
+ val type_system_types_dangerous_types : type_system -> bool
val num_atp_type_args : theory -> type_system -> string -> int
val translate_atp_fact :
Proof.context -> bool -> (string * 'a) * thm
@@ -67,8 +68,11 @@
Mangled |
No_Types
-fun types_dangerous_types (Tags _) = true
- | types_dangerous_types _ = false
+fun is_type_system_sound (Tags true) = true
+ | is_type_system_sound _ = false
+
+fun type_system_types_dangerous_types (Tags _) = true
+ | type_system_types_dangerous_types _ = false
(* This is an approximation. If it returns "true" for a constant that isn't
overloaded (i.e., that has one uniform definition), needless clutter is
@@ -289,7 +293,7 @@
fun get_helper_facts ctxt explicit_forall type_sys formulas =
let
- val no_dangerous_types = types_dangerous_types type_sys
+ val no_dangerous_types = type_system_types_dangerous_types type_sys
val ct = init_counters |> fold count_formula formulas
fun is_used s = the (Symtab.lookup ct s) > 0
fun dub c needs_full_types (th, j) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Apr 21 22:18:28 2011 +0200
@@ -36,6 +36,7 @@
only : bool}
val trace : bool Unsynchronized.ref
+ val is_global_locality : locality -> bool
val fact_from_ref :
Proof.context -> unit Symtab.table -> thm list
-> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
@@ -66,6 +67,12 @@
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
+(* (quasi-)underapproximation of the truth *)
+fun is_global_locality Local = false
+ | is_global_locality Assum = false
+ | is_global_locality Chained = false
+ | is_global_locality _ = true
+
type relevance_fudge =
{allow_ext : bool,
local_const_multiplier : real,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 21 22:18:28 2011 +0200
@@ -457,23 +457,37 @@
else
I)
|>> (if measure_run_time then split_time else rpair NONE)
- val (tstplike_proof, outcome) =
+ val (atp_proof, outcome) =
extract_tstplike_proof_and_outcome debug verbose complete
res_code proof_delims known_failures output
+ |>> atp_proof_from_tstplike_proof
+ val (conjecture_shape, fact_names) =
+ if is_none outcome then
+ repair_conjecture_shape_and_fact_names output
+ conjecture_shape fact_names
+ else
+ (conjecture_shape, fact_names) (* don't bother repairing *)
+ val outcome =
+ if is_none outcome andalso
+ not (is_type_system_sound type_sys) andalso
+ is_unsound_proof conjecture_shape fact_names atp_proof then
+ SOME UnsoundProof
+ else
+ outcome
in
((pool, conjecture_shape, fact_names),
- (output, msecs, tstplike_proof, outcome))
+ (output, msecs, atp_proof, outcome))
end
val timer = Timer.startRealTimer ()
fun maybe_run_slice slice (_, (_, msecs0, _, SOME _)) =
run_slice slice (Time.- (timeout, Timer.checkRealTimer timer))
- |> (fn (stuff, (output, msecs, tstplike_proof, outcome)) =>
- (stuff, (output, int_opt_add msecs0 msecs,
- tstplike_proof, outcome)))
+ |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
+ (stuff, (output, int_opt_add msecs0 msecs, atp_proof,
+ outcome)))
| maybe_run_slice _ result = result
in
((Symtab.empty, [], Vector.fromList []),
- ("", SOME 0, "", SOME InternalError))
+ ("", SOME 0, [], SOME InternalError))
|> fold maybe_run_slice actual_slices
end
else
@@ -489,10 +503,8 @@
else
File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
val ((pool, conjecture_shape, fact_names),
- (output, msecs, tstplike_proof, outcome)) =
+ (output, msecs, atp_proof, outcome)) =
with_path cleanup export run_on problem_path_name
- val (conjecture_shape, fact_names) =
- repair_conjecture_shape_and_fact_names output conjecture_shape fact_names
val important_message =
if not auto andalso random () <= atp_important_message_keep_factor then
extract_important_message output
@@ -511,8 +523,8 @@
"")
val isar_params = (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
val metis_params =
- (proof_banner auto, type_sys, minimize_command, tstplike_proof,
- fact_names, goal, subgoal)
+ (proof_banner auto, type_sys, minimize_command, atp_proof, fact_names,
+ goal, subgoal)
val (outcome, (message, used_facts)) =
case outcome of
NONE =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Apr 21 22:18:28 2011 +0200
@@ -183,7 +183,7 @@
val thy = Proof_Context.theory_of ctxt
val {facts = chained_ths, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
- val no_dangerous_types = types_dangerous_types type_sys
+ val no_dangerous_types = type_system_types_dangerous_types type_sys
val _ = () |> not blocking ? kill_provers
val _ = case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name ^ ".")
--- a/src/HOL/ex/sledgehammer_tactics.ML Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Thu Apr 21 22:18:28 2011 +0200
@@ -33,7 +33,7 @@
val relevance_override = {add = [], del = [], only = false}
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
val no_dangerous_types =
- Sledgehammer_ATP_Translate.types_dangerous_types type_sys
+ Sledgehammer_ATP_Translate.type_system_types_dangerous_types type_sys
val facts =
Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
relevance_thresholds