added generation of induction rules
authornik
Tue Aug 30 14:12:55 2011 +0200 (2011-08-30)
changeset 44585cfe7f4a68e51
parent 44584 08ad27488983
child 44586 eeba1eedf32d
added generation of induction rules
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 29 13:50:47 2011 -0700
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 14:12:55 2011 +0200
     1.3 @@ -55,6 +55,7 @@
     1.4    val get_atp : theory -> string -> atp_config
     1.5    val supported_atps : theory -> string list
     1.6    val is_atp_installed : theory -> string -> bool
     1.7 +  val is_ho_atp: string -> bool
     1.8    val refresh_systems_on_tptp : unit -> unit
     1.9    val setup : theory -> theory
    1.10  end;
    1.11 @@ -499,6 +500,15 @@
    1.12      forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
    1.13    end
    1.14  
    1.15 +fun is_ho_atp name =
    1.16 +  let
    1.17 +    val local_ho_atps = [leo2N, satallaxN]
    1.18 +    val ho_atps = map (fn n => remote_prefix ^ n) local_ho_atps
    1.19 +  in List.filter (fn n => n = name) ho_atps
    1.20 +     |> List.null
    1.21 +     |> not
    1.22 +  end
    1.23 +
    1.24  fun refresh_systems_on_tptp () =
    1.25    Synchronized.change systems (fn _ => get_systems ())
    1.26  
     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 29 13:50:47 2011 -0700
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 14:12:55 2011 +0200
     2.3 @@ -16,8 +16,8 @@
     2.4    type 'a problem = 'a ATP_Problem.problem
     2.5  
     2.6    datatype locality =
     2.7 -    General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
     2.8 -    Chained
     2.9 +    General | Helper | Induction | Extensionality | Intro | Elim | Simp |
    2.10 +    Local | Assum | Chained
    2.11  
    2.12    datatype order = First_Order | Higher_Order
    2.13    datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    2.14 @@ -527,8 +527,8 @@
    2.15      in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
    2.16  
    2.17  datatype locality =
    2.18 -  General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
    2.19 -  Chained
    2.20 +  General | Helper | Induction | Extensionality | Intro | Elim | Simp |
    2.21 +  Local | Assum | Chained
    2.22  
    2.23  datatype order = First_Order | Higher_Order
    2.24  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Aug 29 13:50:47 2011 -0700
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Aug 30 14:12:55 2011 +0200
     3.3 @@ -46,13 +46,13 @@
     3.4      Proof.context -> unit Symtab.table -> thm list
     3.5      -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
     3.6    val all_facts :
     3.7 -    Proof.context -> 'a Symtab.table -> bool -> thm list -> thm list
     3.8 +    Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list
     3.9      -> (((unit -> string) * locality) * thm) list
    3.10    val nearly_all_facts :
    3.11 -    Proof.context -> relevance_override -> thm list -> term list -> term
    3.12 +    Proof.context -> bool -> relevance_override -> thm list -> term list -> term
    3.13      -> (((unit -> string) * locality) * thm) list
    3.14    val relevant_facts :
    3.15 -    Proof.context -> real * real -> int
    3.16 +    Proof.context -> bool -> real * real -> int
    3.17      -> (string * typ -> term list -> bool * term list) -> relevance_fudge
    3.18      -> relevance_override -> thm list -> term list -> term
    3.19      -> (((unit -> string) * locality) * thm) list
    3.20 @@ -586,7 +586,7 @@
    3.21     facts are included. *)
    3.22  val special_fact_index = 75
    3.23  
    3.24 -fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
    3.25 +fun relevance_filter ctxt ho_atp threshold0 decay max_relevant is_built_in_const
    3.26          (fudge as {threshold_divisor, ridiculous_threshold, ...})
    3.27          ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
    3.28    let
    3.29 @@ -729,14 +729,15 @@
    3.30                 (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
    3.31  
    3.32  (* FIXME: put other record thms here, or declare as "no_atp" *)
    3.33 -fun multi_base_blacklist ctxt =
    3.34 +fun multi_base_blacklist ctxt ho_atp =
    3.35    ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
    3.36     "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
    3.37     "weak_case_cong"]
    3.38 -  |> not (Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"]
    3.39 +  |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
    3.40 +        append ["induct", "inducts"]
    3.41    |> map (prefix ".")
    3.42  
    3.43 -val max_lambda_nesting = 3
    3.44 +val max_lambda_nesting = 3 (*only applies if not ho_atp*)
    3.45  
    3.46  fun term_has_too_many_lambdas max (t1 $ t2) =
    3.47      exists (term_has_too_many_lambdas max) [t1, t2]
    3.48 @@ -746,11 +747,12 @@
    3.49  
    3.50  (* Don't count nested lambdas at the level of formulas, since they are
    3.51     quantifiers. *)
    3.52 -fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
    3.53 -    formula_has_too_many_lambdas (T :: Ts) t
    3.54 -  | formula_has_too_many_lambdas Ts t =
    3.55 +fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
    3.56 +  | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
    3.57 +      formula_has_too_many_lambdas false (T :: Ts) t
    3.58 +  | formula_has_too_many_lambdas _ Ts t =
    3.59      if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
    3.60 -      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
    3.61 +      exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
    3.62      else
    3.63        term_has_too_many_lambdas max_lambda_nesting t
    3.64  
    3.65 @@ -762,8 +764,8 @@
    3.66    | apply_depth (Abs (_, _, t)) = apply_depth t
    3.67    | apply_depth _ = 0
    3.68  
    3.69 -fun is_formula_too_complex t =
    3.70 -  apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t
    3.71 +fun is_formula_too_complex ho_atp t =
    3.72 +  apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
    3.73  
    3.74  (* FIXME: Extend to "Meson" and "Metis" *)
    3.75  val exists_sledgehammer_const =
    3.76 @@ -791,11 +793,11 @@
    3.77  (**** Predicates to detect unwanted facts (prolific or likely to cause
    3.78        unsoundness) ****)
    3.79  
    3.80 -fun is_theorem_bad_for_atps exporter thm =
    3.81 +fun is_theorem_bad_for_atps ho_atp exporter thm =
    3.82    is_metastrange_theorem thm orelse
    3.83    (not exporter andalso
    3.84     let val t = prop_of thm in
    3.85 -     is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
    3.86 +     is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
    3.87       exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
    3.88       is_that_fact thm
    3.89     end)
    3.90 @@ -824,7 +826,7 @@
    3.91                    |> add Simp normalize_simp_prop snd simps
    3.92    end
    3.93  
    3.94 -fun all_facts ctxt reserved exporter add_ths chained_ths =
    3.95 +fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths =
    3.96    let
    3.97      val thy = Proof_Context.theory_of ctxt
    3.98      val global_facts = Global_Theory.facts_of thy
    3.99 @@ -834,16 +836,18 @@
   3.100      fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
   3.101      val is_chained = member Thm.eq_thm_prop chained_ths
   3.102      val clasimpset_table = clasimpset_rule_table_of ctxt
   3.103 -    fun locality_of_theorem global th =
   3.104 -      if is_chained th then
   3.105 +    fun locality_of_theorem global (name: string) th =
   3.106 +      if (String.isSubstring ".induct" name) orelse(*FIXME: use structured name*)
   3.107 +         (String.isSubstring ".inducts" name) then
   3.108 +           Induction
   3.109 +      else if is_chained th then
   3.110          Chained
   3.111        else if global then
   3.112          case Termtab.lookup clasimpset_table (prop_of th) of
   3.113            SOME loc => loc
   3.114          | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
   3.115                    else General
   3.116 -      else
   3.117 -        if is_assum th then Assum else Local
   3.118 +      else if is_assum th then Assum else Local
   3.119      fun is_good_unnamed_local th =
   3.120        not (Thm.has_name_hint th) andalso
   3.121        forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
   3.122 @@ -860,7 +864,7 @@
   3.123              (not (Config.get ctxt ignore_no_atp) andalso
   3.124               is_package_def name0) orelse
   3.125              exists (fn s => String.isSuffix s name0)
   3.126 -                   (multi_base_blacklist ctxt) orelse
   3.127 +                   (multi_base_blacklist ctxt ho_atp) orelse
   3.128              String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then
   3.129            I
   3.130          else
   3.131 @@ -877,7 +881,7 @@
   3.132              #> fold (fn th => fn (j, (multis, unis)) =>
   3.133                          (j + 1,
   3.134                           if not (member Thm.eq_thm_prop add_ths th) andalso
   3.135 -                            is_theorem_bad_for_atps exporter th then
   3.136 +                            is_theorem_bad_for_atps ho_atp exporter th then
   3.137                             (multis, unis)
   3.138                           else
   3.139                             let
   3.140 @@ -893,7 +897,7 @@
   3.141                                     |> (fn SOME name =>
   3.142                                            make_name reserved multi j name
   3.143                                          | NONE => "")),
   3.144 -                                locality_of_theorem global th), th)
   3.145 +                                locality_of_theorem global name0 th), th)
   3.146                             in
   3.147                               if multi then (new :: multis, unis)
   3.148                               else (multis, new :: unis)
   3.149 @@ -911,8 +915,8 @@
   3.150  fun external_frees t =
   3.151    [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
   3.152  
   3.153 -fun nearly_all_facts ctxt ({add, only, ...} : relevance_override) chained_ths
   3.154 -                     hyp_ts concl_t =
   3.155 +fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
   3.156 +                     chained_ths hyp_ts concl_t =
   3.157    let
   3.158      val thy = Proof_Context.theory_of ctxt
   3.159      val reserved = reserved_isar_keyword_table ()
   3.160 @@ -926,7 +930,7 @@
   3.161         maps (map (fn ((name, loc), th) => ((K name, loc), th))
   3.162               o fact_from_ref ctxt reserved chained_ths) add
   3.163       else
   3.164 -       all_facts ctxt reserved false add_ths chained_ths)
   3.165 +       all_facts ctxt ho_atp reserved false add_ths chained_ths)
   3.166      |> Config.get ctxt instantiate_inducts
   3.167         ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
   3.168      |> (not (Config.get ctxt ignore_no_atp) andalso not only)
   3.169 @@ -934,7 +938,7 @@
   3.170      |> uniquify
   3.171    end
   3.172  
   3.173 -fun relevant_facts ctxt (threshold0, threshold1) max_relevant
   3.174 +fun relevant_facts ctxt ho_atp (threshold0, threshold1) max_relevant
   3.175                     is_built_in_const fudge (override as {only, ...}) chained_ths
   3.176                     hyp_ts concl_t facts =
   3.177    let
   3.178 @@ -950,9 +954,9 @@
   3.179               max_relevant = 0 then
   3.180         []
   3.181       else
   3.182 -       relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
   3.183 -           fudge override facts (chained_ths |> map prop_of) hyp_ts
   3.184 -           (concl_t |> theory_constify fudge (Context.theory_name thy)))
   3.185 +       relevance_filter ctxt ho_atp threshold0 decay max_relevant
   3.186 +           is_built_in_const fudge override facts (chained_ths |> map prop_of)
   3.187 +           hyp_ts (concl_t |> theory_constify fudge (Context.theory_name thy)))
   3.188      |> map (apfst (apfst (fn f => f ())))
   3.189    end
   3.190  
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Aug 29 13:50:47 2011 -0700
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 30 14:12:55 2011 +0200
     4.3 @@ -91,6 +91,7 @@
     4.4    val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool
     4.5    val is_built_in_const_for_prover :
     4.6      Proof.context -> string -> string * typ -> term list -> bool * term list
     4.7 +  val is_induction_fact: prover_fact -> bool
     4.8    val atp_relevance_fudge : relevance_fudge
     4.9    val smt_relevance_fudge : relevance_fudge
    4.10    val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
    4.11 @@ -329,6 +330,10 @@
    4.12  type prover =
    4.13    params -> (string -> minimize_command) -> prover_problem -> prover_result
    4.14  
    4.15 +(* checking facts' locality *)
    4.16 +
    4.17 +fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true
    4.18 +  | is_induction_fact _ = false
    4.19  
    4.20  (* configuration attributes *)
    4.21  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Aug 29 13:50:47 2011 -0700
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Aug 30 14:12:55 2011 +0200
     5.3 @@ -160,9 +160,16 @@
     5.4      fun desc () =
     5.5        prover_description ctxt params name num_facts subgoal subgoal_count goal
     5.6      val problem =
     5.7 -      {state = state, goal = goal, subgoal = subgoal,
     5.8 -       subgoal_count = subgoal_count, facts = facts |> take num_facts,
     5.9 -       smt_filter = smt_filter}
    5.10 +      let
    5.11 +        val filter_induction =
    5.12 +          List.filter (fn fact =>
    5.13 +                         not (Sledgehammer_Provers.is_induction_fact fact))
    5.14 +      in {state = state, goal = goal, subgoal = subgoal,
    5.15 +         subgoal_count = subgoal_count, facts =
    5.16 +          ((ATP_Systems.is_ho_atp name |> not) ? filter_induction) facts
    5.17 +          |> take num_facts,
    5.18 +         smt_filter = smt_filter}
    5.19 +      end
    5.20      fun really_go () =
    5.21        problem
    5.22        |> get_minimizing_prover ctxt mode name params minimize_command
    5.23 @@ -260,9 +267,12 @@
    5.24        val {facts = chained_ths, goal, ...} = Proof.goal state
    5.25        val chained_ths = chained_ths |> normalize_chained_theorems
    5.26        val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
    5.27 -      val facts = nearly_all_facts ctxt relevance_override chained_ths hyp_ts
    5.28 -                                   concl_t
    5.29 -      val _ = () |> not blocking ? kill_provers
    5.30 +      val targetting_ho_provers =
    5.31 +        List.foldr (fn (name, so_far) => (ATP_Systems.is_ho_atp name) orelse
    5.32 +                     so_far)
    5.33 +          false provers
    5.34 +      val facts = nearly_all_facts ctxt targetting_ho_provers relevance_override
    5.35 +                                   chained_ths hyp_ts concl_t      val _ = () |> not blocking ? kill_provers
    5.36        val _ = case find_first (not o is_prover_supported ctxt) provers of
    5.37                  SOME name => error ("No such prover: " ^ name ^ ".")
    5.38                | NONE => ()
    5.39 @@ -313,9 +323,9 @@
    5.40            |> (case is_appropriate_prop of
    5.41                  SOME is_app => filter (is_app o prop_of o snd)
    5.42                | NONE => I)
    5.43 -          |> relevant_facts ctxt relevance_thresholds max_max_relevant
    5.44 -                            is_built_in_const relevance_fudge relevance_override
    5.45 -                            chained_ths hyp_ts concl_t
    5.46 +          |> relevant_facts ctxt targetting_ho_provers relevance_thresholds
    5.47 +                            max_max_relevant is_built_in_const relevance_fudge
    5.48 +                            relevance_override chained_ths hyp_ts concl_t
    5.49            |> tap (fn facts =>
    5.50                       if debug then
    5.51                         label ^ plural_s (length provers) ^ ": " ^