distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
authorblanchet
Thu May 10 16:56:23 2012 +0200 (2012-05-10)
changeset 4790467663c968d70
parent 47903 920ea85e7426
child 47905 9b6afe0eb69c
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 10 12:23:20 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 10 16:56:23 2012 +0200
     1.3 @@ -190,10 +190,16 @@
     1.4    else if is_assum assms th then Assum
     1.5    else Local
     1.6  
     1.7 +val may_be_induction =
     1.8 +  exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
     1.9 +                     body_type T = @{typ bool}
    1.10 +                   | _ => false)
    1.11 +
    1.12  fun status_of_thm css_table name th =
    1.13    (* FIXME: use structured name *)
    1.14 -  if String.isSubstring ".induct" name orelse
    1.15 -     String.isSubstring ".inducts" name then
    1.16 +  if (String.isSubstring ".induct" name orelse
    1.17 +      String.isSubstring ".inducts" name) andalso
    1.18 +     may_be_induction (prop_of th) then
    1.19      Induction
    1.20    else case Termtab.lookup css_table (prop_of th) of
    1.21      SOME status => status
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu May 10 12:23:20 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu May 10 16:56:23 2012 +0200
     2.3 @@ -172,9 +172,6 @@
     2.4    get_prover ctxt mode name params minimize_command problem
     2.5    |> minimize ctxt mode name params problem
     2.6  
     2.7 -fun is_induction_fact (Untranslated_Fact ((_, (_, Induction)), _)) = true
     2.8 -  | is_induction_fact _ = false
     2.9 -
    2.10  fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
    2.11                                timeout, expect, ...})
    2.12          mode minimize_command only {state, goal, subgoal, subgoal_count, facts}
    2.13 @@ -191,14 +188,13 @@
    2.14      fun desc () =
    2.15        prover_description ctxt params name num_facts subgoal subgoal_count goal
    2.16      val problem =
    2.17 -      let
    2.18 -        val filter_induction = filter_out is_induction_fact
    2.19 -      in {state = state, goal = goal, subgoal = subgoal,
    2.20 -         subgoal_count = subgoal_count, facts =
    2.21 -          ((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction)
    2.22 -            facts
    2.23 -          |> take num_facts}
    2.24 -      end
    2.25 +      {state = state, goal = goal, subgoal = subgoal,
    2.26 +       subgoal_count = subgoal_count,
    2.27 +       facts = facts
    2.28 +               |> not (Sledgehammer_Provers.is_ho_atp ctxt name)
    2.29 +                  ? filter_out (curry (op =) Induction o snd o snd o fst
    2.30 +                                o untranslated_fact)
    2.31 +               |> take num_facts}
    2.32      fun really_go () =
    2.33        problem
    2.34        |> get_minimizing_prover ctxt mode name params minimize_command