updated documentation concerning 'named_theorems';
authorwenzelm
Sat Aug 16 12:10:36 2014 +0200 (2014-08-16)
changeset 579466a26aa5fa65e
parent 57945 cacb00a569e0
child 57947 189d421ca72d
updated documentation concerning 'named_theorems';
NEWS
src/Doc/Implementation/Isar.thy
src/Doc/Isar_Ref/Spec.thy
     1.1 --- a/NEWS	Sat Aug 16 11:35:33 2014 +0200
     1.2 +++ b/NEWS	Sat Aug 16 12:10:36 2014 +0200
     1.3 @@ -9,6 +9,11 @@
     1.4  * Commands 'method_setup' and 'attribute_setup' now work within a
     1.5  local theory context.
     1.6  
     1.7 +* Command 'named_theorems' declares a dynamic fact within the context,
     1.8 +together with an attribute to maintain the content incrementally.
     1.9 +This supersedes functor Named_Thms, but with a subtle change of
    1.10 +semantics due to external visual order vs. internal reverse order.
    1.11 +
    1.12  
    1.13  *** HOL ***
    1.14  
     2.1 --- a/src/Doc/Implementation/Isar.thy	Sat Aug 16 11:35:33 2014 +0200
     2.2 +++ b/src/Doc/Implementation/Isar.thy	Sat Aug 16 12:10:36 2014 +0200
     2.3 @@ -436,32 +436,25 @@
     2.4  end
     2.5  
     2.6  text {* \medskip Apart from explicit arguments, common proof methods
     2.7 -  typically work with a default configuration provided by the context.
     2.8 -  As a shortcut to rule management we use a cheap solution via the
     2.9 -  functor @{ML_functor Named_Thms} (see also @{file
    2.10 -  "~~/src/Pure/Tools/named_thms.ML"}).  *}
    2.11 +  typically work with a default configuration provided by the context. As a
    2.12 +  shortcut to rule management we use a cheap solution via the @{command
    2.13 +  named_theorems} command to declare a dynamic fact in the context. *}
    2.14  
    2.15 -ML {*
    2.16 -  structure My_Simps =
    2.17 -    Named_Thms(
    2.18 -      val name = @{binding my_simp}
    2.19 -      val description = "my_simp rule"
    2.20 -    )
    2.21 -*}
    2.22 -setup My_Simps.setup
    2.23 +named_theorems my_simp
    2.24  
    2.25 -text {* This provides ML access to a list of theorems in canonical
    2.26 -  declaration order via @{ML My_Simps.get}.  The user can add or
    2.27 -  delete rules via the attribute @{attribute my_simp}.  The actual
    2.28 -  proof method is now defined as before, but we append the explicit
    2.29 -  arguments and the rules from the context.  *}
    2.30 +text {* The proof method is now defined as before, but we append the
    2.31 +  explicit arguments and the rules from the context. *}
    2.32  
    2.33  method_setup my_simp' =
    2.34    \<open>Attrib.thms >> (fn thms => fn ctxt =>
    2.35 -    SIMPLE_METHOD' (fn i =>
    2.36 -      CHANGED (asm_full_simp_tac
    2.37 -        (put_simpset HOL_basic_ss ctxt
    2.38 -          addsimps (thms @ My_Simps.get ctxt)) i)))\<close>
    2.39 +    let
    2.40 +      val my_simps = Named_Theorems.get ctxt @{named_theorems my_simp}
    2.41 +    in
    2.42 +      SIMPLE_METHOD' (fn i =>
    2.43 +        CHANGED (asm_full_simp_tac
    2.44 +          (put_simpset HOL_basic_ss ctxt
    2.45 +            addsimps (thms @ my_simps)) i))
    2.46 +    end)\<close>
    2.47    "rewrite subgoal by given rules and my_simp rules from the context"
    2.48  
    2.49  text {*
    2.50 @@ -500,7 +493,7 @@
    2.51    theory library, for example.
    2.52  
    2.53    This is an inherent limitation of the simplistic rule management via
    2.54 -  functor @{ML_functor Named_Thms}, because it lacks tool-specific
    2.55 +  @{command named_theorems}, because it lacks tool-specific
    2.56    storage and retrieval.  More realistic applications require
    2.57    efficient index-structures that organize theorems in a customized
    2.58    manner, such as a discrimination net that is indexed by the
     3.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sat Aug 16 11:35:33 2014 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sat Aug 16 12:10:36 2014 +0200
     3.3 @@ -1305,12 +1305,16 @@
     3.4    \begin{matharray}{rcll}
     3.5      @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     3.6      @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     3.7 +    @{command_def "named_theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     3.8    \end{matharray}
     3.9  
    3.10    @{rail \<open>
    3.11      (@@{command lemmas} | @@{command theorems}) @{syntax target}? \<newline>
    3.12        (@{syntax thmdef}? @{syntax thmrefs} + @'and')
    3.13        (@'for' (@{syntax vars} + @'and'))?
    3.14 +    ;
    3.15 +    @@{command named_theorems} @{syntax target}?
    3.16 +      @{syntax name} @{syntax text}?
    3.17    \<close>}
    3.18  
    3.19    \begin{description}
    3.20 @@ -1324,6 +1328,12 @@
    3.21    \item @{command "theorems"} is the same as @{command "lemmas"}, but
    3.22    marks the result as a different kind of facts.
    3.23  
    3.24 +  \item @{command "named_theorems"}~@{text "name description"} declares a
    3.25 +  dynamic fact within the context. The same @{text name} is used to define
    3.26 +  an attribute with the usual @{text add}/@{text del} syntax (e.g.\ see
    3.27 +  \secref{sec:simp-rules}) to maintain the content incrementally, in
    3.28 +  canonical declaration order of the text structure.
    3.29 +
    3.30    \end{description}
    3.31  *}
    3.32