# HG changeset patch
# User blanchet
# Date 1304369535 -7200
# Node ID 2cd4e64638424da4adb85113bae9ae6f6db1857a
# Parent  879d2d6b05ce630283fbc4f10dd0f6b9a9a3dbe6
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)

diff -r 879d2d6b05ce -r 2cd4e6463842 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon May 02 22:52:15 2011 +0200
@@ -41,8 +41,8 @@
     Proof.context -> unit Symtab.table -> thm list
     -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
   val all_facts :
-    Proof.context -> 'a Symtab.table -> bool -> relevance_fudge -> thm list
-    -> thm list -> (((unit -> string) * locality) * (bool * thm)) list
+    Proof.context -> 'a Symtab.table -> bool -> thm list -> thm list
+    -> (((unit -> string) * locality) * (bool * thm)) list
   val const_names_in_fact :
     theory -> (string * typ -> term list -> bool * term list) -> term
     -> string list
@@ -659,9 +659,9 @@
      String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
   end
 
-fun mk_fact_table f xs =
-  fold (Termtab.update o `(prop_of o f)) xs Termtab.empty
-fun uniquify xs = Termtab.fold (cons o snd) (mk_fact_table snd xs) []
+fun mk_fact_table g f xs =
+  fold (Termtab.update o `(g o prop_of o f)) xs Termtab.empty
+fun uniquify xs = Termtab.fold (cons o snd) (mk_fact_table I snd xs) []
 
 (* FIXME: put other record thms here, or declare as "no_atp" *)
 val multi_base_blacklist =
@@ -789,17 +789,29 @@
     is_metastrange_theorem thm orelse is_that_fact thm
   end
 
+fun meta_equify (@{const Trueprop}
+                 $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2)) =
+    Const (@{const_name "=="}, T --> T --> @{typ prop}) $ t1 $ t2
+  | meta_equify t = t
+
+val normalize_simp_prop =
+  meta_equify
+  #> map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t)
+  #> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S)))
+
 fun clasimpset_rules_of ctxt =
   let
     val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> rep_cs
     val intros = safeIs @ hazIs
     val elims = map Classical.classical_rule (safeEs @ hazEs)
-    val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
-  in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
+    val simps = ctxt |> simpset_of |> dest_ss |> #simps
+  in
+    (mk_fact_table I I intros,
+     mk_fact_table I I elims,
+     mk_fact_table normalize_simp_prop snd simps)
+  end
 
-fun all_facts ctxt reserved really_all
-              ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge)
-              add_ths chained_ths =
+fun all_facts ctxt reserved really_all add_ths chained_ths =
   let
     val thy = Proof_Context.theory_of ctxt
     val global_facts = Global_Theory.facts_of thy
@@ -808,11 +820,19 @@
     val assms = Assumption.all_assms_of ctxt
     fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
     val is_chained = member Thm.eq_thm chained_ths
-    val (intros, elims, simps) =
-      if exists (curry (op <) 0.0) [intro_bonus, elim_bonus, simp_bonus] then
-        clasimpset_rules_of ctxt
+    val (intros, elims, simps) = clasimpset_rules_of ctxt
+    fun locality_of_theorem global th =
+      if is_chained th then
+        Chained
+      else if global then
+        let val t = prop_of th in
+          if Termtab.defined intros t then Intro
+          else if Termtab.defined elims t then Elim
+          else if Termtab.defined simps (normalize_simp_prop t) then Simp
+          else General
+        end
       else
-        (Termtab.empty, Termtab.empty, Termtab.empty)
+        if is_assum th then Assum else Local
     fun is_good_unnamed_local th =
       not (Thm.has_name_hint th) andalso
       forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
@@ -842,35 +862,24 @@
           in
             pair 1
             #> fold (fn th => fn (j, rest) =>
-                 (j + 1,
-                  if is_theorem_bad_for_atps th andalso
-                     not (member Thm.eq_thm add_ths th) then
-                    rest
-                  else
-                    (((fn () =>
-                          if name0 = "" then
-                            th |> backquote_thm
-                          else
-                            let
-                              val name1 = Facts.extern ctxt facts name0
-                              val name2 = Name_Space.extern ctxt full_space name0
-                            in
-                              case find_first check_thms [name1, name2, name0] of
-                                SOME name => make_name reserved multi j name
-                              | NONE => ""
-                            end),
-                      let val t = prop_of th in
-                        if is_chained th then
-                          Chained
-                        else if global then
-                          if Termtab.defined intros t then Intro
-                          else if Termtab.defined elims t then Elim
-                          else if Termtab.defined simps t then Simp
-                          else General
-                        else
-                          if is_assum th then Assum else Local
-                      end),
-                      (multi, th)) :: rest)) ths
+                        (j + 1,
+                         if is_theorem_bad_for_atps th andalso
+                            not (member Thm.eq_thm add_ths th) then
+                           rest
+                         else
+                           (((fn () =>
+                                 if name0 = "" then
+                                   th |> backquote_thm
+                                 else
+                                   [Facts.extern ctxt facts name0,
+                                    Name_Space.extern ctxt full_space name0,
+                                    name0]
+                                   |> find_first check_thms
+                                   |> (fn SOME name =>
+                                          make_name reserved multi j name
+                                        | NONE => "")),
+                              locality_of_theorem global th),
+                              (multi, th)) :: rest)) ths
             #> snd
           end)
   in
@@ -905,7 +914,7 @@
          maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
                o fact_from_ref ctxt reserved chained_ths) add
        else
-         all_facts ctxt reserved false fudge add_ths chained_ths)
+         all_facts ctxt reserved false add_ths chained_ths)
       |> instantiate_inducts
          ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
       |> rearrange_facts ctxt (respect_no_atp andalso not only)