# HG changeset patch
# User blanchet
# Date 1378821411 -7200
# Node ID b49bfa77958aff9a5cc2ef24e96779bdc8a685e9
# Parent  53b9326196fed904a0e61b4fb68eb33e0118fe74
speed up detection of simp rules

diff -r 53b9326196fe -r b49bfa77958a src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
@@ -106,15 +106,49 @@
                      body_type T = @{typ bool}
                    | _ => false)
 
+fun normalize_vars t =
+  let
+    fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s
+      | normT (TVar (z as (_, S))) =
+        (fn ((knownT, nT), accum) =>
+            case find_index (equal z) knownT of
+              ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum))
+            | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum)))
+      | normT (T as TFree _) = pair T
+    fun norm (t $ u) = norm t ##>> norm u #>> op $
+      | norm (Const (s, T)) = normT T #>> curry Const s
+      | norm (Var (z as (_, T))) =
+        normT T
+        #> (fn (T, (accumT, (known, n))) =>
+               case find_index (equal z) known of
+                 ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1)))
+               | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))
+      | norm (Abs (_, T, t)) =
+        norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t))
+      | norm (Bound j) = pair (Bound j)
+      | norm (Free (s, T)) = normT T #>> curry Free s
+  in fst (norm t (([], 0), ([], 0))) end
+
 fun status_of_thm css name th =
-  (* FIXME: use structured name *)
-  if (String.isSubstring ".induct" name orelse
-      String.isSubstring ".inducts" name) andalso
-     may_be_induction (prop_of th) then
-    Induction
-  else case Termtab.lookup css (prop_of th) of
-    SOME status => status
-  | NONE => General
+  let val t = normalize_vars (prop_of th) in
+    (* FIXME: use structured name *)
+    if String.isSubstring ".induct" name andalso may_be_induction t then
+      Induction
+    else case Termtab.lookup css t of
+      SOME status => status
+    | NONE =>
+      let val concl = Logic.strip_imp_concl t in
+        case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
+          SOME lrhss =>
+          let
+            val prems = Logic.strip_imp_prems t
+            val t' = Logic.list_implies (prems, Logic.mk_equals lrhss)
+          in
+            Termtab.lookup css t' |> the_default General
+          end
+        | NONE => General
+      end
+  end
 
 fun stature_of_thm global assms chained css name th =
   (scope_of_thm global assms chained th, status_of_thm css name th)
@@ -274,18 +308,8 @@
 
 fun clasimpset_rule_table_of ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
-    fun add stature normalizers get_th =
-      fold (fn rule =>
-               let
-                 val th = rule |> get_th
-                 val t =
-                   th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
-               in
-                 fold (fn normalize => Termtab.update (normalize t, stature))
-                      (I :: normalizers)
-               end)
+    fun add stature th =
+      Termtab.update (normalize_vars (prop_of th), stature)
     val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
       ctxt |> claset_of |> Classical.rep_cs
     val intros = Item_Net.content safeIs @ Item_Net.content hazIs
@@ -306,14 +330,14 @@
                                       Spec_Rules.Co_Inductive] o fst)
             |> maps (snd o snd)
   in
-    Termtab.empty |> add Simp [atomize] snd simps
-                  |> add Rec_Def [] I rec_defs
-                  |> add Non_Rec_Def [] I nonrec_defs
+    Termtab.empty |> fold (add Simp o snd) simps
+                  |> fold (add Rec_Def) rec_defs
+                  |> fold (add Non_Rec_Def) nonrec_defs
 (* Add once it is used:
-                  |> add Elim [] I elims
+                  |> fold (add Elim) elims
 *)
-                  |> add Intro [] I intros
-                  |> add Inductive [] I spec_intros
+                  |> fold (add Intro) intros
+                  |> fold (add Inductive) spec_intros
   end
 
 fun normalize_eq (t as @{const Trueprop}