1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Jul 01 16:47:10 2014 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Jul 01 16:47:10 2014 +0200
1.3 @@ -84,6 +84,7 @@
1.4 val risky_defs = @{thms Bit0_def Bit1_def}
1.5
1.6 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
1.7 +
1.8 fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
1.9 | is_rec_def (@{const Pure.imp} $ _ $ t2) = is_rec_def t2
1.10 | is_rec_def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
1.11 @@ -114,6 +115,7 @@
1.12 ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum))
1.13 | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum))))
1.14 | normT (T as TFree _) = pair T
1.15 +
1.16 fun norm (t $ u) = norm t ##>> norm u #>> op $
1.17 | norm (Const (s, T)) = normT T #>> curry Const s
1.18 | norm (Var (z as (_, T))) =
1.19 @@ -164,6 +166,7 @@
1.20 val bracket =
1.21 map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
1.22 |> implode
1.23 +
1.24 fun nth_name j =
1.25 (case xref of
1.26 Facts.Fact s => backquote s ^ bracket
1.27 @@ -173,12 +176,15 @@
1.28 | Facts.Named ((name, _), SOME intervals) =>
1.29 make_name reserved true
1.30 (nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket)
1.31 +
1.32 fun add_nth th (j, rest) =
1.33 let val name = nth_name j in
1.34 (j + 1, ((name, stature_of_thm false [] chained css name th), th)
1.35 :: rest)
1.36 end
1.37 - in (0, []) |> fold add_nth ths |> snd end
1.38 + in
1.39 + (0, []) |> fold add_nth ths |> snd
1.40 + end
1.41
1.42 (* Reject theorems with names like "List.filter.filter_list_def" or
1.43 "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
1.44 @@ -222,6 +228,7 @@
1.45
1.46 (* FIXME: make more reliable *)
1.47 val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator
1.48 +
1.49 fun is_low_level_class_const (s, _) =
1.50 s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
1.51
1.52 @@ -250,6 +257,7 @@
1.53 not (member (op =) atp_widely_irrelevant_consts s)
1.54 | is_interesting_subterm (Free _) = true
1.55 | is_interesting_subterm _ = false
1.56 +
1.57 fun interest_of_bool t =
1.58 if exists_Const (is_technical_const orf is_low_level_class_const orf
1.59 type_has_top_sort o snd) t then
1.60 @@ -259,6 +267,7 @@
1.61 Boring
1.62 else
1.63 Interesting
1.64 +
1.65 fun interest_of_prop _ (@{const Trueprop} $ t) = interest_of_bool t
1.66 | interest_of_prop Ts (@{const Pure.imp} $ t $ u) =
1.67 combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
1.68 @@ -269,6 +278,7 @@
1.69 | interest_of_prop _ (Const (@{const_name Pure.eq}, _) $ t $ u) =
1.70 combine_interests (interest_of_bool t) (interest_of_bool u)
1.71 | interest_of_prop _ _ = Deal_Breaker
1.72 +
1.73 val t = prop_of th
1.74 in
1.75 (interest_of_prop [] t <> Interesting andalso
1.76 @@ -277,11 +287,9 @@
1.77 end
1.78
1.79 fun is_blacklisted_or_something ctxt ho_atp =
1.80 - let
1.81 - val blist = multi_base_blacklist ctxt ho_atp
1.82 - fun is_blisted name =
1.83 - is_package_def name orelse exists (fn s => String.isSuffix s name) blist
1.84 - in is_blisted end
1.85 + let val blist = multi_base_blacklist ctxt ho_atp in
1.86 + fn name => is_package_def name orelse exists (fn s => String.isSuffix s name) blist
1.87 + end
1.88
1.89 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
1.90 they are displayed as "M" and we want to avoid clashes with these. But
1.91 @@ -316,6 +324,7 @@
1.92 let
1.93 fun add stature th =
1.94 Termtab.update (normalize_vars (prop_of th), stature)
1.95 +
1.96 val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
1.97 ctxt |> claset_of |> Classical.rep_cs
1.98 val intros = Item_Net.content safeIs @ Item_Net.content hazIs
1.99 @@ -331,18 +340,18 @@
1.100 |> filter_out (member Thm.eq_thm_prop risky_defs)
1.101 |> List.partition (is_rec_def o prop_of)
1.102 val spec_intros =
1.103 - specs |> filter (member (op =) [Spec_Rules.Inductive,
1.104 - Spec_Rules.Co_Inductive] o fst)
1.105 + specs |> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst)
1.106 |> maps (snd o snd)
1.107 in
1.108 - Termtab.empty |> fold (add Simp o snd) simps
1.109 - |> fold (add Rec_Def) rec_defs
1.110 - |> fold (add Non_Rec_Def) nonrec_defs
1.111 + Termtab.empty
1.112 + |> fold (add Simp o snd) simps
1.113 + |> fold (add Rec_Def) rec_defs
1.114 + |> fold (add Non_Rec_Def) nonrec_defs
1.115 (* Add once it is used:
1.116 - |> fold (add Elim) elims
1.117 + |> fold (add Elim) elims
1.118 *)
1.119 - |> fold (add Intro) intros
1.120 - |> fold (add Inductive) spec_intros
1.121 + |> fold (add Intro) intros
1.122 + |> fold (add Inductive) spec_intros
1.123 end
1.124 end
1.125
1.126 @@ -359,9 +368,8 @@
1.127 fun if_thm_before th th' =
1.128 if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
1.129
1.130 -(* Hack: Conflate the facts about a class as seen from the outside with the
1.131 - corresponding low-level facts, so that MaSh can learn from the low-level
1.132 - proofs. *)
1.133 +(* Hack: Conflate the facts about a class as seen from the outside with the corresponding low-level
1.134 + facts, so that MaSh can learn from the low-level proofs. *)
1.135 fun un_class_ify s =
1.136 (case first_field "_class" s of
1.137 SOME (pref, suf) => [s, pref ^ suf]
1.138 @@ -407,6 +415,7 @@
1.139 fun varify_noninducts (t as Free (s, T)) =
1.140 if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
1.141 | varify_noninducts t = t
1.142 +
1.143 val p_inst =
1.144 concl_prop |> map_aterms varify_noninducts |> close_form
1.145 |> lambda (Free ind_x)
1.146 @@ -455,23 +464,25 @@
1.147 val thy = Proof_Context.theory_of ctxt
1.148 val global_facts = Global_Theory.facts_of thy
1.149 val is_too_complex =
1.150 - if generous orelse
1.151 - fact_count global_facts >= max_facts_for_complex_check then
1.152 + if generous orelse fact_count global_facts >= max_facts_for_complex_check then
1.153 K false
1.154 else
1.155 is_too_complex
1.156 val local_facts = Proof_Context.facts_of ctxt
1.157 val named_locals = local_facts |> Facts.dest_static true [global_facts]
1.158 val assms = Assumption.all_assms_of ctxt
1.159 +
1.160 fun is_good_unnamed_local th =
1.161 not (Thm.has_name_hint th) andalso
1.162 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
1.163 +
1.164 val unnamed_locals =
1.165 union Thm.eq_thm_prop (Facts.props local_facts) chained
1.166 |> filter is_good_unnamed_local |> map (pair "" o single)
1.167 val full_space =
1.168 Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
1.169 val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp
1.170 +
1.171 fun add_facts global foldx facts =
1.172 foldx (fn (name0, ths) => fn accum =>
1.173 if name0 <> "" andalso
1.174 @@ -483,6 +494,7 @@
1.175 let
1.176 val n = length ths
1.177 val multi = n > 1
1.178 +
1.179 fun check_thms a =
1.180 (case try (Proof_Context.get_thms ctxt) a of
1.181 NONE => false
1.182 @@ -522,8 +534,7 @@
1.183 |> op @
1.184 end
1.185
1.186 -fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
1.187 - concl_t =
1.188 +fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts concl_t =
1.189 if only andalso null add then
1.190 []
1.191 else