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) ^ ": " ^