doc-src/TutorialI/Misc/document/case_splits.tex

 %
 \begin{isabellebody}%
 %
 \begin{isamarkuptext}%
-Goals containing \isaindex{if}-expressions are usually proved by case
+Goals containing \isa{if}-expressions are usually proved by case
 distinction on the condition of the \isa{if}. For example the goal%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 can be split into
 \begin{isabelle}
-~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])%
+~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
 \end{isabelle}
 by a degenerate form of simplification%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
-where no simplification rules are included (\isa{only:} is followed by the
+where no simplification rules are included (\isa{only{\isacharcolon}} is followed by the
 empty list of theorems) but the rule \isaindexbold{split_if} for
-splitting \isa{if}s is added (via the modifier \isa{split:}). Because
+splitting \isa{if}s is added (via the modifier \isa{split{\isacharcolon}}). Because
 case-splitting on \isa{if}s is almost always the right proof strategy, the
-simplifier performs it automatically. Try \isacommand{apply}\isa{(simp)}
+simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}}
 on the initial goal above.
 
 This splitting idea generalizes from \isa{if} to \isaindex{case}:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 becomes
 \begin{isabelle}
 ~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
-~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)%
+~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
 \end{isabelle}
 by typing%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 In contrast to \isa{if}-expressions, the simplifier does not split
 \isa{case}-expressions by default because this can lead to nontermination
-in case of recursive datatypes. Again, if the \isa{only:} modifier is
+in case of recursive datatypes. Again, if the \isa{only{\isacharcolon}} modifier is
 dropped, the above goal is solved,%
 \end{isamarkuptext}%
 \isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent%
-which \isacommand{apply}\isa{(simp)} alone will not do.
+which \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not do.
 
 In general, every datatype $t$ comes with a theorem
-\isa{$t$.split} which can be declared to be a \bfindex{split rule} either
+$t$\isa{{\isachardot}split} which can be declared to be a \bfindex{split rule} either
 locally as above, or by giving it the \isa{split} attribute globally:%
 \end{isamarkuptext}%
 \isacommand{lemmas}\ {\isacharbrackleft}split{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split%
 \begin{isamarkuptext}%
 \noindent

 \end{isamarkuptext}%
 \isacommand{lemmas}\ {\isacharbrackleft}split\ del{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split%
 \begin{isamarkuptext}%
 The above split rules intentionally only affect the conclusion of a
 subgoal.  If you want to split an \isa{if} or \isa{case}-expression in
-the assumptions, you have to apply \isa{split\_if\_asm} or $t$\isa{.split_asm}:%
+the assumptions, you have to apply \isa{split{\isacharunderscore}if{\isacharunderscore}asm} or
+$t$\isa{{\isachardot}split{\isacharunderscore}asm}:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharat}\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 In contrast to splitting the conclusion, this actually creates two
-separate subgoals (which are solved by \isa{simp\_all}):
+separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}):
 \begin{isabelle}
 \ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
 \ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}
 \end{isabelle}
 If you need to split both in the assumptions and the conclusion,
-use $t$\isa{.splits} which subsumes $t$\isa{.split} and $t$\isa{.split_asm}.%
+use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and
+$t$\isa{{\isachardot}split{\isacharunderscore}asm}. Analogously, there is \isa{if{\isacharunderscore}splits}.%
 \end{isamarkuptxt}%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"