diff -r bda7527ccf05 -r cc2d676d5395 src/Doc/Tutorial/Misc/simp.thy --- a/src/Doc/Tutorial/Misc/simp.thy Wed Dec 26 16:07:28 2018 +0100 +++ b/src/Doc/Tutorial/Misc/simp.thy Wed Dec 26 16:25:20 2018 +0100 @@ -6,7 +6,7 @@ text\\index{simplification rules} To facilitate simplification, -the attribute @{text"[simp]"}\index{*simp (attribute)} +the attribute \[simp]\\index{*simp (attribute)} declares theorems to be simplification rules, which the simplifier will use automatically. In addition, \isacommand{datatype} and \isacommand{primrec} declarations (and a few others) @@ -23,8 +23,8 @@ The simplification attribute of theorems can be turned on and off:% \index{*simp del (attribute)} \begin{quote} -\isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\ -\isacommand{declare} \textit{theorem-name}@{text"[simp del]"} +\isacommand{declare} \textit{theorem-name}\[simp]\\\ +\isacommand{declare} \textit{theorem-name}\[simp del]\ \end{quote} Only equations that really simplify, like \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and @@ -56,15 +56,15 @@ text\\index{*simp (method)|bold} The general format of the simplification method is \begin{quote} -@{text simp} \textit{list of modifiers} +\simp\ \textit{list of modifiers} \end{quote} where the list of \emph{modifiers} fine tunes the behaviour and may be empty. Specific modifiers are discussed below. Most if not all of the proofs seen so far could have been performed -with @{text simp} instead of \isa{auto}, except that @{text simp} attacks +with \simp\ instead of \isa{auto}, except that \simp\ attacks only the first subgoal and may thus need to be repeated --- use \methdx{simp_all} to simplify all subgoals. -If nothing changes, @{text simp} fails. +If nothing changes, \simp\ fails. \ subsection\Adding and Deleting Simplification Rules\ @@ -76,17 +76,17 @@ the set of simplification rules used in a simplification step by adding rules to it and/or deleting rules from it. The two modifiers for this are \begin{quote} -@{text"add:"} \textit{list of theorem names}\index{*add (modifier)}\\ -@{text"del:"} \textit{list of theorem names}\index{*del (modifier)} +\add:\ \textit{list of theorem names}\index{*add (modifier)}\\ +\del:\ \textit{list of theorem names}\index{*del (modifier)} \end{quote} Or you can use a specific list of theorems and omit all others: \begin{quote} -@{text"only:"} \textit{list of theorem names}\index{*only (modifier)} +\only:\ \textit{list of theorem names}\index{*only (modifier)} \end{quote} In this example, we invoke the simplifier, adding two distributive laws: \begin{quote} -\isacommand{apply}@{text"(simp add: mod_mult_distrib add_mult_distrib)"} +\isacommand{apply}\(simp add: mod_mult_distrib add_mult_distrib)\ \end{quote} \ @@ -112,7 +112,7 @@ lemma "\x. f x = g (f (g x)) \ f [] = f [] @ []" txt\\noindent -An unmodified application of @{text"simp"} loops. The culprit is the +An unmodified application of \simp\ loops. The culprit is the simplification rule @{term"f x = g (f (g x))"}, which is extracted from the assumption. (Isabelle notices certain simple forms of nontermination but not this one.) The problem can be circumvented by @@ -125,12 +125,12 @@ text\\noindent Three modifiers influence the treatment of assumptions: \begin{description} -\item[@{text"(no_asm)"}]\index{*no_asm (modifier)} +\item[\(no_asm)\]\index{*no_asm (modifier)} means that assumptions are completely ignored. -\item[@{text"(no_asm_simp)"}]\index{*no_asm_simp (modifier)} +\item[\(no_asm_simp)\]\index{*no_asm_simp (modifier)} means that the assumptions are not simplified but are used in the simplification of the conclusion. -\item[@{text"(no_asm_use)"}]\index{*no_asm_use (modifier)} +\item[\(no_asm_use)\]\index{*no_asm_use (modifier)} means that the assumptions are simplified but are not used in the simplification of each other or the conclusion. \end{description} @@ -205,9 +205,9 @@ text\\index{simplification!of \isa{let}-expressions}\index{*let expressions}% Proving a goal containing \isa{let}-expressions almost invariably requires the -@{text"let"}-con\-structs to be expanded at some point. Since -@{text"let"}\ldots\isa{=}\ldots@{text"in"}{\ldots} is just syntactic sugar for -the predefined constant @{term"Let"}, expanding @{text"let"}-constructs +\let\-con\-structs to be expanded at some point. Since +\let\\ldots\isa{=}\ldots\in\{\ldots} is just syntactic sugar for +the predefined constant @{term"Let"}, expanding \let\-constructs means rewriting with \tdx{Let_def}:\ lemma "(let xs = [] in xs@ys@xs) = ys" @@ -216,7 +216,7 @@ text\ If, in a particular context, there is no danger of a combinatorial explosion -of nested @{text"let"}s, you could even simplify with @{thm[source]Let_def} by +of nested \let\s, you could even simplify with @{thm[source]Let_def} by default: \ declare Let_def [simp] @@ -257,7 +257,7 @@ subsection\Automatic Case Splits\ text\\label{sec:AutoCaseSplits}\indexbold{case splits}% -Goals containing @{text"if"}-expressions\index{*if expressions!splitting of} +Goals containing \if\-expressions\index{*if expressions!splitting of} are usually proved by case distinction on the boolean condition. Here is an example: \ @@ -273,12 +273,12 @@ txt\\noindent @{subgoals[display,indent=0]} where \tdx{if_split} is a theorem that expresses splitting of -@{text"if"}s. Because -splitting the @{text"if"}s is usually the right proof strategy, the -simplifier does it automatically. Try \isacommand{apply}@{text"(simp)"} +\if\s. Because +splitting the \if\s is usually the right proof strategy, the +simplifier does it automatically. Try \isacommand{apply}\(simp)\ on the initial goal above. -This splitting idea generalizes from @{text"if"} to \sdx{case}. +This splitting idea generalizes from \if\ to \sdx{case}. Let us simplify a case analysis over lists:\index{*list.split (theorem)} \(*<*)by simp(*>*) lemma "(case xs of [] \ zs | y#ys \ y#(ys@zs)) = xs@zs" @@ -287,10 +287,10 @@ txt\ @{subgoals[display,indent=0]} The simplifier does not split -@{text"case"}-expressions, as it does @{text"if"}-expressions, +\case\-expressions, as it does \if\-expressions, because with recursive datatypes it could lead to nontermination. Instead, the simplifier has a modifier -@{text split}\index{*split (modifier)} +\split\\index{*split (modifier)} for adding splitting rules explicitly. The lemma above can be proved in one step by \ @@ -300,17 +300,17 @@ apply(simp split: list.split) (*<*)done(*>*) text\\noindent -whereas \isacommand{apply}@{text"(simp)"} alone will not succeed. +whereas \isacommand{apply}\(simp)\ alone will not succeed. Every datatype $t$ comes with a theorem -$t$@{text".split"} which can be declared to be a \bfindex{split rule} either +$t$\.split\ which can be declared to be a \bfindex{split rule} either locally as above, or by giving it the \attrdx{split} attribute globally: \ declare list.split [split] text\\noindent -The @{text"split"} attribute can be removed with the @{text"del"} modifier, +The \split\ attribute can be removed with the \del\ modifier, either locally \ (*<*) @@ -326,27 +326,27 @@ declare list.split [split del] text\ -Polished proofs typically perform splitting within @{text simp} rather than -invoking the @{text split} method. However, if a goal contains -several @{text "if"} and @{text case} expressions, -the @{text split} method can be +Polished proofs typically perform splitting within \simp\ rather than +invoking the \split\ method. However, if a goal contains +several \if\ and \case\ expressions, +the \split\ method can be helpful in selectively exploring the effects of splitting. The split rules shown above are intended to affect only the subgoal's -conclusion. If you want to split an @{text"if"} or @{text"case"}-expression +conclusion. If you want to split an \if\ or \case\-expression in the assumptions, you have to apply \tdx{if_split_asm} or -$t$@{text".split_asm"}:\ +$t$\.split_asm\:\ lemma "if xs = [] then ys \ [] else ys = [] \ xs @ ys \ []" apply(split if_split_asm) txt\\noindent Unlike splitting the conclusion, this step creates two -separate subgoals, which here can be solved by @{text"simp_all"}: +separate subgoals, which here can be solved by \simp_all\: @{subgoals[display,indent=0]} If you need to split both in the assumptions and the conclusion, -use $t$@{text".splits"} which subsumes $t$@{text".split"} and -$t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}. +use $t$\.splits\ which subsumes $t$\.split\ and +$t$\.split_asm\. Analogously, there is @{thm[source]if_splits}. \begin{warn} The simplifier merely simplifies the condition of an @@ -476,7 +476,7 @@ @{text[display]"_ * (_ + _) = \"} It only finds equations that can simplify the given pattern at the root, not somewhere inside: for example, equations of the form -@{text"_ + _ = \"} do not match. +\_ + _ = \\ do not match. You may also search for theorems by name---you merely need to specify a substring. For example, you could search for all @@ -502,7 +502,7 @@ "_ + _" -"_ - _" -simp: "_ * (_ + _)" name: assoc \end{ttbox} looks for theorems containing plus but not minus, and which do not simplify -\mbox{@{text"_ * (_ + _)"}} at the root, and whose name contains \texttt{assoc}. +\mbox{\_ * (_ + _)\} at the root, and whose name contains \texttt{assoc}. Further search criteria are explained in \S\ref{sec:find2}.