--- a/NEWS Sat Aug 16 11:35:33 2014 +0200
+++ b/NEWS Sat Aug 16 12:10:36 2014 +0200
@@ -9,6 +9,11 @@
* Commands 'method_setup' and 'attribute_setup' now work within a
local theory context.
+* Command 'named_theorems' declares a dynamic fact within the context,
+together with an attribute to maintain the content incrementally.
+This supersedes functor Named_Thms, but with a subtle change of
+semantics due to external visual order vs. internal reverse order.
+
*** HOL ***
--- a/src/Doc/Implementation/Isar.thy Sat Aug 16 11:35:33 2014 +0200
+++ b/src/Doc/Implementation/Isar.thy Sat Aug 16 12:10:36 2014 +0200
@@ -436,32 +436,25 @@
end
text {* \medskip Apart from explicit arguments, common proof methods
- typically work with a default configuration provided by the context.
- As a shortcut to rule management we use a cheap solution via the
- functor @{ML_functor Named_Thms} (see also @{file
- "~~/src/Pure/Tools/named_thms.ML"}). *}
+ typically work with a default configuration provided by the context. As a
+ shortcut to rule management we use a cheap solution via the @{command
+ named_theorems} command to declare a dynamic fact in the context. *}
-ML {*
- structure My_Simps =
- Named_Thms(
- val name = @{binding my_simp}
- val description = "my_simp rule"
- )
-*}
-setup My_Simps.setup
+named_theorems my_simp
-text {* This provides ML access to a list of theorems in canonical
- declaration order via @{ML My_Simps.get}. The user can add or
- delete rules via the attribute @{attribute my_simp}. The actual
- proof method is now defined as before, but we append the explicit
- arguments and the rules from the context. *}
+text {* The proof method is now defined as before, but we append the
+ explicit arguments and the rules from the context. *}
method_setup my_simp' =
\<open>Attrib.thms >> (fn thms => fn ctxt =>
- SIMPLE_METHOD' (fn i =>
- CHANGED (asm_full_simp_tac
- (put_simpset HOL_basic_ss ctxt
- addsimps (thms @ My_Simps.get ctxt)) i)))\<close>
+ let
+ val my_simps = Named_Theorems.get ctxt @{named_theorems my_simp}
+ in
+ SIMPLE_METHOD' (fn i =>
+ CHANGED (asm_full_simp_tac
+ (put_simpset HOL_basic_ss ctxt
+ addsimps (thms @ my_simps)) i))
+ end)\<close>
"rewrite subgoal by given rules and my_simp rules from the context"
text {*
@@ -500,7 +493,7 @@
theory library, for example.
This is an inherent limitation of the simplistic rule management via
- functor @{ML_functor Named_Thms}, because it lacks tool-specific
+ @{command named_theorems}, because it lacks tool-specific
storage and retrieval. More realistic applications require
efficient index-structures that organize theorems in a customized
manner, such as a discrimination net that is indexed by the
--- a/src/Doc/Isar_Ref/Spec.thy Sat Aug 16 11:35:33 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Sat Aug 16 12:10:36 2014 +0200
@@ -1305,12 +1305,16 @@
\begin{matharray}{rcll}
@{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "named_theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
\end{matharray}
@{rail \<open>
(@@{command lemmas} | @@{command theorems}) @{syntax target}? \<newline>
(@{syntax thmdef}? @{syntax thmrefs} + @'and')
(@'for' (@{syntax vars} + @'and'))?
+ ;
+ @@{command named_theorems} @{syntax target}?
+ @{syntax name} @{syntax text}?
\<close>}
\begin{description}
@@ -1324,6 +1328,12 @@
\item @{command "theorems"} is the same as @{command "lemmas"}, but
marks the result as a different kind of facts.
+ \item @{command "named_theorems"}~@{text "name description"} declares a
+ dynamic fact within the context. The same @{text name} is used to define
+ an attribute with the usual @{text add}/@{text del} syntax (e.g.\ see
+ \secref{sec:simp-rules}) to maintain the content incrementally, in
+ canonical declaration order of the text structure.
+
\end{description}
*}