1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200
1.3 @@ -85,10 +85,10 @@
1.4 | is_rec_def _ = false
1.5
1.6 fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
1.7 -fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths
1.8 +fun is_chained chained = member Thm.eq_thm_prop chained
1.9
1.10 -fun scope_of_thm global assms chained_ths th =
1.11 - if is_chained chained_ths th then Chained
1.12 +fun scope_of_thm global assms chained th =
1.13 + if is_chained chained th then Chained
1.14 else if global then Global
1.15 else if is_assum assms th then Assum
1.16 else Local
1.17 @@ -98,20 +98,20 @@
1.18 body_type T = @{typ bool}
1.19 | _ => false)
1.20
1.21 -fun status_of_thm css_table name th =
1.22 +fun status_of_thm css name th =
1.23 (* FIXME: use structured name *)
1.24 if (String.isSubstring ".induct" name orelse
1.25 String.isSubstring ".inducts" name) andalso
1.26 may_be_induction (prop_of th) then
1.27 Induction
1.28 - else case Termtab.lookup css_table (prop_of th) of
1.29 + else case Termtab.lookup css (prop_of th) of
1.30 SOME status => status
1.31 | NONE => General
1.32
1.33 -fun stature_of_thm global assms chained_ths css_table name th =
1.34 - (scope_of_thm global assms chained_ths th, status_of_thm css_table name th)
1.35 +fun stature_of_thm global assms chained css name th =
1.36 + (scope_of_thm global assms chained th, status_of_thm css name th)
1.37
1.38 -fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) =
1.39 +fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) =
1.40 let
1.41 val ths = Attrib.eval_thms ctxt [xthm]
1.42 val bracket =
1.43 @@ -127,15 +127,12 @@
1.44 make_name reserved true
1.45 (nth (maps (explode_interval (length ths)) intervals) j) name ^
1.46 bracket
1.47 - in
1.48 - (ths, (0, []))
1.49 - |-> fold (fn th => fn (j, rest) =>
1.50 - let val name = nth_name j in
1.51 - (j + 1, ((name, stature_of_thm false [] chained_ths
1.52 - css_table name th), th) :: rest)
1.53 - end)
1.54 - |> snd
1.55 - end
1.56 + fun add_nth th (j, rest) =
1.57 + let val name = nth_name j in
1.58 + (j + 1, ((name, stature_of_thm false [] chained css name th), th)
1.59 + :: rest)
1.60 + end
1.61 + in (0, []) |> fold add_nth ths |> snd end
1.62
1.63 (* Reject theorems with names like "List.filter.filter_list_def" or
1.64 "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
1.65 @@ -352,7 +349,7 @@
1.66 fun maybe_filter_no_atps ctxt =
1.67 not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
1.68
1.69 -fun all_facts ctxt ho_atp reserved add_ths chained_ths css_table =
1.70 +fun all_facts ctxt ho_atp reserved add_ths chained css =
1.71 let
1.72 val thy = Proof_Context.theory_of ctxt
1.73 val global_facts = Global_Theory.facts_of thy
1.74 @@ -363,7 +360,7 @@
1.75 not (Thm.has_name_hint th) andalso
1.76 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
1.77 val unnamed_locals =
1.78 - union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
1.79 + union Thm.eq_thm_prop (Facts.props local_facts) chained
1.80 |> filter is_good_unnamed_local |> map (pair "" o single)
1.81 val full_space =
1.82 Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
1.83 @@ -404,8 +401,8 @@
1.84 |> find_first check_thms
1.85 |> the_default name0
1.86 |> make_name reserved multi j),
1.87 - stature_of_thm global assms chained_ths
1.88 - css_table name0 th), th)
1.89 + stature_of_thm global assms chained css name0
1.90 + th), th)
1.91 in
1.92 if multi then (new :: multis, unis)
1.93 else (multis, new :: unis)
1.94 @@ -420,26 +417,26 @@
1.95 |> op @
1.96 end
1.97
1.98 -fun all_facts_of ctxt css_table =
1.99 - all_facts ctxt false Symtab.empty [] [] css_table
1.100 - |> rev (* try to restore the original order of facts, for MaSh *)
1.101 +fun all_facts_of ctxt css =
1.102 + all_facts ctxt false Symtab.empty [] [] css
1.103 + |> rev (* partly restore the original order of facts, for MaSh *)
1.104
1.105 -fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css_table chained_ths
1.106 - hyp_ts concl_t =
1.107 +fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
1.108 + concl_t =
1.109 if only andalso null add then
1.110 []
1.111 else
1.112 let
1.113 - val chained_ths =
1.114 - chained_ths
1.115 + val chained =
1.116 + chained
1.117 |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
1.118 in
1.119 (if only then
1.120 maps (map (fn ((name, stature), th) => ((K name, stature), th))
1.121 - o fact_from_ref ctxt reserved chained_ths css_table) add
1.122 + o fact_from_ref ctxt reserved chained css) add
1.123 else
1.124 let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
1.125 - all_facts ctxt ho_atp reserved add chained_ths css_table
1.126 + all_facts ctxt ho_atp reserved add chained css
1.127 |> filter_out (member Thm.eq_thm_prop del o snd)
1.128 |> maybe_filter_no_atps ctxt
1.129 |> uniquify