fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
authorblanchet
Fri May 27 10:30:07 2011 +0200 (2011-05-27)
changeset 4300420e9caff1f86
parent 43003 5a86009366fc
child 43005 c96f06bffd90
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri May 27 10:30:07 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri May 27 10:30:07 2011 +0200
     1.3 @@ -390,7 +390,7 @@
     1.4      val relevance_fudge =
     1.5        Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
     1.6      val relevance_override = {add = [], del = [], only = false}
     1.7 -    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
     1.8 +    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal ctxt goal i
     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	Fri May 27 10:30:07 2011 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri May 27 10:30:07 2011 +0200
     2.3 @@ -128,7 +128,8 @@
     2.4                 (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover)
     2.5           val relevance_override = {add = [], del = [], only = false}
     2.6           val subgoal = 1
     2.7 -         val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
     2.8 +         val (_, hyp_ts, concl_t) =
     2.9 +           Sledgehammer_Util.strip_subgoal ctxt goal subgoal
    2.10           val facts =
    2.11             Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    2.12                 (the_default default_max_relevant max_relevant)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:07 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:07 2011 +0200
     3.3 @@ -1018,7 +1018,7 @@
     3.4          (metis_params as (_, _, type_sys, atp_proof, facts_offset, fact_names,
     3.5                            typed_helpers, goal, i)) =
     3.6    let
     3.7 -    val (params, hyp_ts, concl_t) = strip_subgoal goal i
     3.8 +    val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal i
     3.9      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
    3.10      val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
    3.11      val full_types = uses_typed_helpers typed_helpers atp_proof
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 10:30:07 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 10:30:07 2011 +0200
     4.3 @@ -47,6 +47,7 @@
     4.4                   isar_shrink_factor, ...} : params)
     4.5          explicit_apply_opt silent (prover : prover) timeout i n state facts =
     4.6    let
     4.7 +    val ctxt = Proof.context_of state
     4.8      val thy = Proof.theory_of state
     4.9      val _ =
    4.10        print silent (fn () =>
    4.11 @@ -58,7 +59,7 @@
    4.12        case explicit_apply_opt of
    4.13          SOME explicit_apply => explicit_apply
    4.14        | NONE =>
    4.15 -        let val (_, hyp_ts, concl_t) = strip_subgoal goal i in
    4.16 +        let val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i in
    4.17            not (forall (Meson.is_fol_term thy)
    4.18                        (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
    4.19          end
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:07 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:07 2011 +0200
     5.3 @@ -479,7 +479,7 @@
     5.4    let
     5.5      val thy = Proof.theory_of state
     5.6      val ctxt = Proof.context_of state
     5.7 -    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
     5.8 +    val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
     5.9      val (dest_dir, problem_prefix) =
    5.10        if overlord then overlord_file_location_for_prover name
    5.11        else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:07 2011 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:07 2011 +0200
     6.3 @@ -184,7 +184,7 @@
     6.4          state |> Proof.map_context (Config.put SMT_Config.verbose debug)
     6.5        val ctxt = Proof.context_of state
     6.6        val {facts = chained_ths, goal, ...} = Proof.goal state
     6.7 -      val (_, hyp_ts, concl_t) = strip_subgoal goal i
     6.8 +      val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
     6.9        val _ = () |> not blocking ? kill_provers
    6.10        val _ = case find_first (not o is_prover_supported ctxt) provers of
    6.11                  SOME name => error ("No such prover: " ^ name ^ ".")
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 10:30:07 2011 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 10:30:07 2011 +0200
     7.3 @@ -28,7 +28,8 @@
     7.4    val transform_elim_prop : term -> term
     7.5    val specialize_type : theory -> (string * typ) -> term -> term
     7.6    val subgoal_count : Proof.state -> int
     7.7 -  val strip_subgoal : thm -> int -> (string * typ) list * term list * term
     7.8 +  val strip_subgoal :
     7.9 +    Proof.context -> thm -> int -> (string * typ) list * term list * term
    7.10    val reserved_isar_keyword_table : unit -> unit Symtab.table
    7.11  end;
    7.12  
    7.13 @@ -237,12 +238,14 @@
    7.14  
    7.15  val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
    7.16  
    7.17 -fun strip_subgoal goal i =
    7.18 +fun strip_subgoal ctxt goal i =
    7.19    let
    7.20 -    val (t, frees) = Logic.goal_params (prop_of goal) i
    7.21 +    val (t, (frees, params)) =
    7.22 +      Logic.goal_params (prop_of goal) i
    7.23 +      ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free))
    7.24      val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
    7.25      val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
    7.26 -  in (rev (map dest_Free frees), hyp_ts, concl_t) end
    7.27 +  in (rev params, hyp_ts, concl_t) end
    7.28  
    7.29  fun reserved_isar_keyword_table () =
    7.30    union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ())
     8.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Fri May 27 10:30:07 2011 +0200
     8.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Fri May 27 10:30:07 2011 +0200
     8.3 @@ -31,7 +31,7 @@
     8.4      val relevance_fudge =
     8.5        Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
     8.6      val relevance_override = {add = [], del = [], only = false}
     8.7 -    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
     8.8 +    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal ctxt goal i
     8.9      val facts =
    8.10        Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    8.11            (the_default default_max_relevant max_relevant) (K true)