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