normalize the result of case_rwlist and cache it.

A huge amount of time is spent calling SPEC_ALL when adding the results of
case_rwlist to the rewrites or simpset. By caching this expensive operation
is now only done whenever the TypeBase is updated.

Author: ordinarymath

src/basicProof/BasicProvers.sml

@@ -693,17 +693,37 @@ fun PURE_FULL_CASE_TAC (g as (asl,w)) =
  in Cases_on `^t` end g;
 
 local
-  fun tot f x = f x handle HOL_ERR _ => NONE
-in
+
+fun tot f x = f x handle HOL_ERR _ => NONE
+
 fun case_rws tyi =
     List.mapPartial I
        [Lib.total TypeBasePure.case_def_of tyi,
         tot TypeBasePure.distinct_of tyi,
         tot TypeBasePure.one_one_of tyi]
 
-fun case_rwlist () =
- itlist (fn tyi => fn rws => case_rws tyi @ rws)
-        (TypeBase.elts()) [];
+fun decompose (th::res) =
+   let val th = SPEC_ALL th
+       val t = concl th
+   in
+     if is_conj t then (let val (th1,th2) = CONJ_PAIR th
+                        in decompose (th1::th2::res) end)
+     else (th::decompose res)
+   end
+  | decompose [] = []
+
+val cache = ref (List.concat (map case_rws (TypeBase.elts ())))
+
+fun update_cache tyinfo =
+   let val thms = decompose (case_rws tyinfo)
+   in
+     cache := List.revAppend (thms,!cache)
+   end
+in
+
+val _ = TypeBase.register_update_fn (fn tyinfo => (update_cache tyinfo;tyinfo))
+
+fun case_rwlist () = !cache
 
 (* Add the rewrites into a simpset to avoid re-processing them when
  * (PURE_CASE_SIMP_CONV rws) is called multiple times by EVERY_CASE_TAC.  This