# HG changeset patch
# User krauss
# Date 1558431030 -7200
# Node ID 910dc065b869de93ed79b3e6d3ac52c3419916e2
# Parent  91a2f79b546becad42423e6bcfb2db99db0d40d5
documentation for termination_simp attribute

diff -r 91a2f79b546b -r 910dc065b869 src/Doc/Functions/Functions.thy
--- a/src/Doc/Functions/Functions.thy	Tue May 21 11:47:11 2019 +0200
+++ b/src/Doc/Functions/Functions.thy	Tue May 21 11:30:30 2019 +0200
@@ -347,6 +347,15 @@
   method a bit stronger: it can then use multiset orders internally.
 \<close>
 
+subsection \<open>Configuring simplification rules for termination proofs\<close>
+
+text \<open>
+  Since both \<open>lexicographic_order\<close> and \<open>size_change\<close> rely on the simplifier internally,
+  there can sometimes be the need for adding additional simp rules to them.
+  This can be done either as arguments to the methods themselves, or globally via the
+  theorem attribute \<open>termination_simp\<close>, which is useful in rare cases.
+\<close>
+
 section \<open>Mutual Recursion\<close>
 
 text \<open>
diff -r 91a2f79b546b -r 910dc065b869 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Tue May 21 11:47:11 2019 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Tue May 21 11:30:30 2019 +0200
@@ -489,6 +489,7 @@
     @{method_def (HOL) relation} & : & \<open>method\<close> \\
     @{method_def (HOL) lexicographic_order} & : & \<open>method\<close> \\
     @{method_def (HOL) size_change} & : & \<open>method\<close> \\
+    @{attribute_def (HOL) termination_simp} & : & \<open>attribute\<close> \\
     @{method_def (HOL) induction_schema} & : & \<open>method\<close> \\
   \end{matharray}
 
@@ -535,6 +536,10 @@
   For local descent proofs, the @{syntax clasimpmod} modifiers are accepted
   (as for @{method auto}).
 
+  \<^descr> @{attribute (HOL) termination_simp} declares extra rules for the
+  simplifier, when invoked in termination proofs. This can be useful, e.g.,
+  for special rules involving size estimations.
+
   \<^descr> @{method (HOL) induction_schema} derives user-specified induction rules
   from well-founded induction and completeness of patterns. This factors out
   some operations that are done internally by the function package and makes