757 |
757 |
758 \item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}} attempts a fully |
758 \item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}} attempts a fully |
759 automated termination proof by searching for a lexicographic |
759 automated termination proof by searching for a lexicographic |
760 combination of size measures on the arguments of the function. The |
760 combination of size measures on the arguments of the function. The |
761 method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method, |
761 method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method, |
762 which it uses internally to prove local descents. The same context |
762 which it uses internally to prove local descents. The \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}} modifiers are accepted (as for \hyperlink{method.auto}{\mbox{\isa{auto}}}). |
763 modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see |
|
764 \secref{sec:clasimp}. |
|
765 |
763 |
766 In case of failure, extensive information is printed, which can help |
764 In case of failure, extensive information is printed, which can help |
767 to analyse the situation (cf.\ \cite{isabelle-function}). |
765 to analyse the situation (cf.\ \cite{isabelle-function}). |
768 |
766 |
769 \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}} also works on termination goals, |
767 \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}} also works on termination goals, |
773 and \isa{ms} (multiset), which is only available when the theory |
771 and \isa{ms} (multiset), which is only available when the theory |
774 \isa{Multiset} is loaded. When no order kinds are given, they are |
772 \isa{Multiset} is loaded. When no order kinds are given, they are |
775 tried in order. The search for a termination proof uses SAT solving |
773 tried in order. The search for a termination proof uses SAT solving |
776 internally. |
774 internally. |
777 |
775 |
778 For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}. |
776 For local descent proofs, the \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}} modifiers are |
|
777 accepted (as for \hyperlink{method.auto}{\mbox{\isa{auto}}}). |
779 |
778 |
780 \end{description}% |
779 \end{description}% |
781 \end{isamarkuptext}% |
780 \end{isamarkuptext}% |
782 \isamarkuptrue% |
781 \isamarkuptrue% |
783 % |
782 % |
953 recursive functions (using the TFL package), see also |
952 recursive functions (using the TFL package), see also |
954 \cite{isabelle-HOL}. The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}permissive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option tells |
953 \cite{isabelle-HOL}. The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}permissive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option tells |
955 TFL to recover from failed proof attempts, returning unfinished |
954 TFL to recover from failed proof attempts, returning unfinished |
956 results. The \isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}, \isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}, and \isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf} hints refer to auxiliary rules to be used in the internal |
955 results. The \isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}, \isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}, and \isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf} hints refer to auxiliary rules to be used in the internal |
957 automated proof process of TFL. Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}} |
956 automated proof process of TFL. Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}} |
958 declarations (cf.\ \secref{sec:clasimp}) may be given to tune the |
957 declarations may be given to tune the context of the Simplifier |
959 context of the Simplifier (cf.\ \secref{sec:simplifier}) and |
958 (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\ |
960 Classical reasoner (cf.\ \secref{sec:classical}). |
959 \secref{sec:classical}). |
961 |
960 |
962 \item \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} recommences the |
961 \item \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} recommences the |
963 proof for leftover termination condition number \isa{i} (default |
962 proof for leftover termination condition number \isa{i} (default |
964 1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of |
963 1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of |
965 constant \isa{c}. |
964 constant \isa{c}. |