documentation for termination_simp attribute
authorkrauss
Tue May 21 11:30:30 2019 +0200 (2 months ago ago)
changeset 70461910dc065b869
parent 70460 91a2f79b546b
child 70462 ac24aaf84a36
documentation for termination_simp attribute
src/Doc/Functions/Functions.thy
src/Doc/Isar_Ref/HOL_Specific.thy
     1.1 --- a/src/Doc/Functions/Functions.thy	Tue May 21 11:47:11 2019 +0200
     1.2 +++ b/src/Doc/Functions/Functions.thy	Tue May 21 11:30:30 2019 +0200
     1.3 @@ -347,6 +347,15 @@
     1.4    method a bit stronger: it can then use multiset orders internally.
     1.5  \<close>
     1.6  
     1.7 +subsection \<open>Configuring simplification rules for termination proofs\<close>
     1.8 +
     1.9 +text \<open>
    1.10 +  Since both \<open>lexicographic_order\<close> and \<open>size_change\<close> rely on the simplifier internally,
    1.11 +  there can sometimes be the need for adding additional simp rules to them.
    1.12 +  This can be done either as arguments to the methods themselves, or globally via the
    1.13 +  theorem attribute \<open>termination_simp\<close>, which is useful in rare cases.
    1.14 +\<close>
    1.15 +
    1.16  section \<open>Mutual Recursion\<close>
    1.17  
    1.18  text \<open>
     2.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Tue May 21 11:47:11 2019 +0200
     2.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Tue May 21 11:30:30 2019 +0200
     2.3 @@ -489,6 +489,7 @@
     2.4      @{method_def (HOL) relation} & : & \<open>method\<close> \\
     2.5      @{method_def (HOL) lexicographic_order} & : & \<open>method\<close> \\
     2.6      @{method_def (HOL) size_change} & : & \<open>method\<close> \\
     2.7 +    @{attribute_def (HOL) termination_simp} & : & \<open>attribute\<close> \\
     2.8      @{method_def (HOL) induction_schema} & : & \<open>method\<close> \\
     2.9    \end{matharray}
    2.10  
    2.11 @@ -535,6 +536,10 @@
    2.12    For local descent proofs, the @{syntax clasimpmod} modifiers are accepted
    2.13    (as for @{method auto}).
    2.14  
    2.15 +  \<^descr> @{attribute (HOL) termination_simp} declares extra rules for the
    2.16 +  simplifier, when invoked in termination proofs. This can be useful, e.g.,
    2.17 +  for special rules involving size estimations.
    2.18 +
    2.19    \<^descr> @{method (HOL) induction_schema} derives user-specified induction rules
    2.20    from well-founded induction and completeness of patterns. This factors out
    2.21    some operations that are done internally by the function package and makes