Implement new scheme to allow simple addition of theorems to theorem …

…"sets".

When saving or storing theorems, simply add [name1,name2] strings to the
end of the binding, and the theorem being saved will be added to the
theorem set with that name.

Manual/Description/libraries.tex

@@ -2170,6 +2170,18 @@ \subsubsection{The ``stateful'' \simpset---\ml{srw\_ss()}}
 \end{verbatim}
 \end{session}
 
+Alternatively, the user may also flag theorems directly when using \ml{store\_thm} or \ml{save\_thm} by appending the \ml{simp} attribute to the name of the theorem.
+Thus:
+\begin{session}
+\begin{verbatim}
+val useful_rwt = store_thm(
+  "useful_rwt[simp]",
+  ...term...,
+  ...tactic...);
+\end{verbatim}
+\end{session}
+is a way of avoiding having to write a call to \ml{export\_rewrites}.
+
 As a general rule, \ml{(srw\_ss())} includes all of its context's
 ``obvious rewrites'', as well as code to do standard calculations
 (such as the arithmetic performed in the above example).  It does not

src/1/ThmSetData.sig

@@ -8,10 +8,15 @@ sig
                       export : string -> unit,
                       mk : string list -> data * (string * Thm.thm) list}
 
+  val new_storage_attribute : string -> unit
+  val store_attribute : {attribute: string, thm_name : string} -> unit
+
   val current_data : string -> (string * Thm.thm) list
   val theory_data : {settype : string, thy: string} ->
                     (string * Thm.thm) list
   val all_data : string -> (string * (string * Thm.thm) list) list
+  val data_storefn : string -> (string -> unit) option
+  val data_exportfn : string -> (string -> Thm.thm list -> unit) option
 
   val all_set_types : unit -> string list
 

src/1/ThmSetData.sml

@@ -41,14 +41,30 @@ in
   String.concatWith " " list
 end
 
+(* ----------------------------------------------------------------------
+    destfn: takes polymorphic theory data and turns it into the
+            structured theorem data we want to use
+    storefn: takes a theorem name and stores the associated theorem into
+             the theory data.  Doesn't perform any associated update in
+             the run-time memory
+    exportfn: takes a string and a list of theorems and does something with
+              them at runtime (adds them to a simpset, say).  The string is
+              expected to be the name of the theory with which these
+              theorems are associated.
+   ---------------------------------------------------------------------- *)
 type destfn = data -> (string * thm) list option
-val destmap = let
+type storefn = string -> unit
+type exportfn = (string -> thm list -> unit) option
+val data_map = let
   open Binarymap
 in
-  ref (mkDict String.compare : (string,destfn) dict)
+  ref (mkDict String.compare : (string,destfn * storefn * exportfn) dict)
 end
 
-fun all_set_types () = Binarymap.foldr (fn (k,_,acc) => k::acc) [] (!destmap)
+fun data_storefn s = Option.map #2 (Binarymap.peek(!data_map,s))
+fun data_exportfn s = Option.join (Option.map #3 (Binarymap.peek(!data_map,s)))
+
+fun all_set_types () = Binarymap.foldr (fn (k,_,acc) => k::acc) [] (!data_map)
 
 fun foldli f a l = let
   fun recurse a i l =
@@ -75,7 +91,6 @@ fun new ty = let
   val (mk,dest) = LoadableThyData.new {merge = set_alist_merge,
                                        read = read ty,
                                        write = writeset, thydataty = ty}
-  val _ = destmap := Binarymap.insert(!destmap,ty,dest)
   fun foldthis (nm,set) =
       case lookup ty ("<internal>: "^nm) nm of
         SOME r => (nm, r) :: set
@@ -85,15 +100,22 @@ fun new ty = let
       in
         (mk unencoded, unencoded)
       end
+  fun store s = let
+    val (data, _) = mk' [s]
+  in
+    LoadableThyData.write_data_update {thydataty = ty, data = data}
+  end
+
+  val _ = data_map := Binarymap.insert(!data_map,ty,(dest,store,NONE))
 in
   (mk',dest)
 end
 
 fun theory_data {settype = key, thy} =
-    case Binarymap.peek(!destmap, key) of
+    case Binarymap.peek(!data_map, key) of
       NONE => raise mk_HOL_ERR "ThmSetData" "theory_data"
                     ("No ThmSetData with name "^Lib.quote key)
-    | SOME df => let
+    | SOME (df,_,_) => let
         open LoadableThyData
       in
         case segment_data {thy = thy, thydataty = key} of
@@ -153,11 +175,30 @@ fun new_exporter name addfn = let
     addfn (current_theory()) thms;
     write_data_update {thydataty = name, data = data}
   end
+  val store = #2 (Binarymap.find(!data_map,name))
 in
+  Binarymap.insert(!data_map,name,(dest,store,SOME addfn));
   register_hook ("ThmSetData.onload." ^ name, hook);
   List.app onload (ancestry "-");
   {export = export, mk = mk, dest = dest}
 end
 
+fun new_storage_attribute s = let
+in
+  new_exporter s (fn _ => fn _ => ());
+  Theory.adjoin_to_theory {
+    sig_ps = NONE,
+    struct_ps = SOME (fn pps =>
+                         PP.add_string pps
+                                       ("val _ = new_exporter "^Lib.mlquote s^
+                                        "(fn _ => fn _ => ())"))
+  }
+end
+
+fun store_attribute {attribute, thm_name} =
+    case data_storefn attribute of
+        NONE => raise mk_HOL_ERR "ThmSetData" "store_attribute"
+                      ("Unknown attribute: "^attribute)
+      | SOME f => f thm_name
 
 end (* struct *)

src/1/boolLib.sml

@@ -8,7 +8,7 @@ struct
 
 open boolTheory boolSyntax Hol_pp ParseExtras
      Drule Tactical Tactic Thm_cont Conv Rewrite Prim_rec Abbrev DB
-     BoundedRewrites TexTokenMap
+     BoundedRewrites TexTokenMap ThmSetData
 
 local open DefnBase TypeBase Ho_Rewrite Psyntax Rsyntax in end
 
@@ -111,4 +111,51 @@ end (* local open *)
 
 val def_suffix = ref "_def"
 
+local
+open Feedback Theory
+fun resolve_storename s = let
+  open Substring
+  val (bracketl,rest) = position "[" (full s)
+in
+  if isEmpty rest then (s,[])
+  else let
+    val (names,bracketr) = position "]" (slice(rest,1,NONE))
+  in
+    if size bracketr <> 1 then
+      raise mk_HOL_ERR "boolLib" "resolve_storename"
+            ("Malformed theorem-binding specifier: "^s)
+    else
+      (string bracketl, String.fields (fn c => c = #",") (string names))
+  end
+end
+in
+fun save_thm_attrs fname (n, attrs, th) = let
+  fun do_attr a = let
+    val storefn = valOf (ThmSetData.data_storefn a)
+                        handle Option => raise mk_HOL_ERR "boolLib" fname
+                                               ("No attribute with name "^a)
+    val exportfn = ThmSetData.data_exportfn a
+  in
+    storefn n;
+    case exportfn of
+        NONE => ()
+      | SOME ef => ef (current_theory()) [th]
+  end
+in
+  Theory.save_thm(n,th) before app do_attr attrs
+end
+fun store_thm(n0,t,tac) = let
+  val (n, attrs) = resolve_storename n0
+  val th = Tactical.prove(t,tac)
+              handle e => (print ("Failed to prove theorem " ^ n ^ ".\n");
+                           Raise e)
+in
+  save_thm_attrs "store_thm" (n,attrs,th)
+end
+fun save_thm(n0,th) = let
+  val (n,attrs) = resolve_storename n0
+in
+  save_thm_attrs "save_thm" (n,attrs,th)
+end
+end (* local *)
 end;

src/basicProof/BasicProvers.sml

@@ -927,7 +927,7 @@ in
 end
 
 val {mk,dest,export} =
-    ThmSetData.new_exporter "BasicProvers.stateful_simpset" add_rewrites
+    ThmSetData.new_exporter "simp" add_rewrites
 
 fun export_rewrites slist = List.app export slist
 

src/q/Q.sml

@@ -56,7 +56,7 @@ end
 
 val mk_type_rsubst = map (fn {redex,residue} => (pty redex |-> pty residue));
 
-fun store_thm(s,q,t) = Tactical.store_thm(s,btm q,t);
+fun store_thm(s,q,t) = boolLib.store_thm(s,btm q,t);
 fun prove (q, t) = Tactical.prove(btm q,t);
 fun new_definition(s,q) = Definition.new_definition(s,btm q);
 fun new_infixl_definition(s,q,f) = boolLib.new_infixl_definition(s,btm q,f);

src/relation/relationScript.sml

@@ -171,11 +171,10 @@ val RTC_RTC = store_thm(
   GEN_TAC THEN HO_MATCH_MP_TAC RTC_STRONG_INDUCT THEN MESON_TAC [RTC_RULES]);
 
 val RTC_TRANSITIVE = store_thm(
-  "RTC_TRANSITIVE",
+  "RTC_TRANSITIVE[simp]",
   ``!R:'a->'a->bool. transitive (RTC R)``,
   REWRITE_TAC [transitive_def] THEN MESON_TAC [RTC_RTC]);
 val transitive_RTC = save_thm("transitive_RTC", RTC_TRANSITIVE);
-val _ = export_rewrites ["transitive_RTC"]
 
 val RTC_REFLEXIVE = store_thm(
   "RTC_REFLEXIVE",
@@ -197,11 +196,10 @@ val RC_lifts_monotonicities = store_thm(
   METIS_TAC [RC_DEF]);
 
 val RC_MONOTONE = store_thm(
-  "RC_MONOTONE",
+  "RC_MONOTONE[mono]",
   ``(!x y. R x y ==> Q x y) ==> RC R x y ==> RC Q x y``,
   STRIP_TAC THEN REWRITE_TAC [RC_DEF] THEN STRIP_TAC THEN
   ASM_REWRITE_TAC [] THEN RES_TAC THEN ASM_REWRITE_TAC [])
-val _ = IndDefLib.export_mono "RC_MONOTONE"
 
 val RC_lifts_invariants = store_thm(
   "RC_lifts_invariants",
@@ -224,11 +222,10 @@ val SC_lifts_equalities = store_thm(
   METIS_TAC [SC_DEF]);
 
 val SC_MONOTONE = store_thm(
-  "SC_MONOTONE",
+  "SC_MONOTONE[mono]",
   ``(!x:'a y. R x y ==> Q x y) ==> SC R x y ==> SC Q x y``,
   STRIP_TAC THEN REWRITE_TAC [SC_DEF] THEN STRIP_TAC THEN RES_TAC THEN
   ASM_REWRITE_TAC [])
-val _ = IndDefLib.export_mono "SC_MONOTONE"
 
 val symmetric_RC = store_thm(
   "symmetric_RC",
@@ -664,18 +661,16 @@ val TC_CASES2 = store_thm(
   MESON_TAC [TC_RULES, TC_CASES2_E]);
 
 val TC_MONOTONE = store_thm(
-  "TC_MONOTONE",
+  "TC_MONOTONE[mono]",
   ``(!x y. R x y ==> Q x y) ==> TC R x y ==> TC Q x y``,
   REPEAT GEN_TAC THEN STRIP_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN
   TC_INDUCT_TAC THEN ASM_MESON_TAC [TC_RULES]);
-val _ = IndDefLib.export_mono "TC_MONOTONE"
 
 val RTC_MONOTONE = store_thm(
-  "RTC_MONOTONE",
+  "RTC_MONOTONE[mono]",
   ``(!x y. R x y ==> Q x y) ==> RTC R x y ==> RTC Q x y``,
   REPEAT GEN_TAC THEN STRIP_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN
   HO_MATCH_MP_TAC RTC_INDUCT THEN ASM_MESON_TAC [RTC_RULES]);
-val _ = IndDefLib.export_mono "RTC_MONOTONE"
 
 val EQC_INDUCTION = store_thm(
   "EQC_INDUCTION",
@@ -776,12 +771,11 @@ val ALT_equivalence = store_thm(
   MESON_TAC []);
 
 val EQC_MONOTONE = store_thm(
-  "EQC_MONOTONE",
+  "EQC_MONOTONE[mono]",
   ``(!x y. R x y ==> R' x y) ==> EQC R x y ==> EQC R' x y``,
   STRIP_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN
   HO_MATCH_MP_TAC STRONG_EQC_INDUCTION THEN
   METIS_TAC [EQC_R, EQC_TRANS, EQC_SYM, EQC_REFL]);
-val _ = IndDefLib.export_mono "EQC_MONOTONE"
 
 val RTC_EQC = store_thm(
   "RTC_EQC",