1\DOC srw_ss
2
3\TYPE {srw_ss : unit -> simpset}
4
5\SYNOPSIS
6Returns the "stateful rewriting" system's underlying {simpset}.
7
8\KEYWORDS
9simplification
10
11\LIBRARY bossLib
12
13\DESCRIBE
14A call to {srw_ss()} returns a {simpset} value that is internally
15maintained and updated by the system.  Its value changes as new types
16enter the {TypeBase}, and as theories are loaded.  For this reason, it
17can't be accessed as a simple value, but is instead hidden behind a
18function.
19
20The value behind {srw_ss()} can change in three ways.  Firstly, whenever
21a type enters the {TypeBase}, the type's associated simplification
22theorems (accessible directly using the function {TypeBase.simpls_of})
23are all added to the {simpset}.  This ensures that the "obvious"
24rewrite theorems for a type (such as the disjointness of constructors)
25need never be explicitly specified.
26
27Secondly, users can interactively add {simpset} fragments to the
28{srw_ss()} value by using the function {augment_srw_ss}.  This
29function might be used after a definition is made to ensure that a
30particular constant always has its definition expanded.  (Whether or
31not a constant warrants this is something that needs to be determined
32on a case-by-case basis.)
33
34Thirdly, theories can augment the {srw_ss()} value as they load.  This
35is set up in a theory's script file with the function
36{export_rewrites}.  This causes a list of appropriate theorems to be
37added when the theory loads.  It is up to the author of the theory to
38ensure that the theorems added to the {simpset} are sensible.
39
40\FAILURE
41Never fails.
42
43\SEEALSO
44bossLib.augment_srw_ss, BasicProvers.export_rewrites, bossLib.SRW_TAC.
45
46\ENDDOC
47