# HG changeset patch # User blanchet # Date 1306485007 -7200 # Node ID 20e9caff1f862aa2d0228e9cb5443f633aedbbd6 # Parent 5a86009366fcb42e695524a0173f51dbc8dd73c7 fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context diff -r 5a86009366fc -r 20e9caff1f86 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 27 10:30:07 2011 +0200 @@ -390,7 +390,7 @@ val relevance_fudge = Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name val relevance_override = {add = [], del = [], only = false} - val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i + val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal ctxt goal i val time_limit = (case hard_timeout of NONE => I diff -r 5a86009366fc -r 20e9caff1f86 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri May 27 10:30:07 2011 +0200 @@ -128,7 +128,8 @@ (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover) val relevance_override = {add = [], del = [], only = false} val subgoal = 1 - val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal + val (_, hyp_ts, concl_t) = + Sledgehammer_Util.strip_subgoal ctxt goal subgoal val facts = Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds (the_default default_max_relevant max_relevant) diff -r 5a86009366fc -r 20e9caff1f86 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 27 10:30:07 2011 +0200 @@ -1018,7 +1018,7 @@ (metis_params as (_, _, type_sys, atp_proof, facts_offset, fact_names, typed_helpers, goal, i)) = let - val (params, hyp_ts, concl_t) = strip_subgoal goal i + val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal i val frees = fold Term.add_frees (concl_t :: hyp_ts) [] val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] val full_types = uses_typed_helpers typed_helpers atp_proof diff -r 5a86009366fc -r 20e9caff1f86 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri May 27 10:30:07 2011 +0200 @@ -47,6 +47,7 @@ isar_shrink_factor, ...} : params) explicit_apply_opt silent (prover : prover) timeout i n state facts = let + val ctxt = Proof.context_of state val thy = Proof.theory_of state val _ = print silent (fn () => @@ -58,7 +59,7 @@ case explicit_apply_opt of SOME explicit_apply => explicit_apply | NONE => - let val (_, hyp_ts, concl_t) = strip_subgoal goal i in + let val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i in not (forall (Meson.is_fol_term thy) (concl_t :: hyp_ts @ maps (map prop_of o snd) facts)) end diff -r 5a86009366fc -r 20e9caff1f86 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:07 2011 +0200 @@ -479,7 +479,7 @@ let val thy = Proof.theory_of state val ctxt = Proof.context_of state - val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal + val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal val (dest_dir, problem_prefix) = if overlord then overlord_file_location_for_prover name else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix) diff -r 5a86009366fc -r 20e9caff1f86 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:07 2011 +0200 @@ -184,7 +184,7 @@ state |> Proof.map_context (Config.put SMT_Config.verbose debug) val ctxt = Proof.context_of state val {facts = chained_ths, goal, ...} = Proof.goal state - val (_, hyp_ts, concl_t) = strip_subgoal goal i + val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i val _ = () |> not blocking ? kill_provers val _ = case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") diff -r 5a86009366fc -r 20e9caff1f86 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 27 10:30:07 2011 +0200 @@ -28,7 +28,8 @@ val transform_elim_prop : term -> term val specialize_type : theory -> (string * typ) -> term -> term val subgoal_count : Proof.state -> int - val strip_subgoal : thm -> int -> (string * typ) list * term list * term + val strip_subgoal : + Proof.context -> thm -> int -> (string * typ) list * term list * term val reserved_isar_keyword_table : unit -> unit Symtab.table end; @@ -237,12 +238,14 @@ val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal -fun strip_subgoal goal i = +fun strip_subgoal ctxt goal i = let - val (t, frees) = Logic.goal_params (prop_of goal) i + val (t, (frees, params)) = + Logic.goal_params (prop_of goal) i + ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free)) val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees - in (rev (map dest_Free frees), hyp_ts, concl_t) end + in (rev params, hyp_ts, concl_t) end fun reserved_isar_keyword_table () = union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ()) diff -r 5a86009366fc -r 20e9caff1f86 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Fri May 27 10:30:07 2011 +0200 @@ -31,7 +31,7 @@ val relevance_fudge = Sledgehammer_Provers.relevance_fudge_for_prover ctxt name val relevance_override = {add = [], del = [], only = false} - val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i + val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal ctxt goal i val facts = Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds (the_default default_max_relevant max_relevant) (K true)