1.1 --- a/doc-src/TutorialI/Misc/simp.thy	Mon Oct 30 18:28:00 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Tue Oct 31 08:53:12 2000 +0100
     1.3 @@ -154,9 +154,7 @@
     1.4  
     1.5  txt{*\noindent
     1.6  In this particular case, the resulting goal
     1.7 -\begin{isabelle}
     1.8 -~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
     1.9 -\end{isabelle}
    1.10 +@{subgoals[display,indent=0]}
    1.11  can be proved by simplification. Thus we could have proved the lemma outright by
    1.12  *}(*<*)oops;lemma "exor A (\<not>A)";(*>*)
    1.13  apply(simp add: exor_def)
    1.14 @@ -237,17 +235,13 @@
    1.15  lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";
    1.16  
    1.17  txt{*\noindent
    1.18 -can be split into
    1.19 -\begin{isabelle}
    1.20 -~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
    1.21 -\end{isabelle}
    1.22 -by a degenerate form of simplification
    1.23 +can be split by a degenerate form of simplification
    1.24  *}
    1.25  
    1.26  apply(simp only: split: split_if);
    1.27 -(*<*)oops;(*>*)
    1.28  
    1.29 -text{*\noindent
    1.30 +txt{*\noindent
    1.31 +@{subgoals[display,indent=0]}
    1.32  where no simplification rules are included (@{text"only:"} is followed by the
    1.33  empty list of theorems) but the rule \isaindexbold{split_if} for
    1.34  splitting @{text"if"}s is added (via the modifier @{text"split:"}). Because
    1.35 @@ -256,28 +250,19 @@
    1.36  on the initial goal above.
    1.37  
    1.38  This splitting idea generalizes from @{text"if"} to \isaindex{case}:
    1.39 -*}
    1.40 +*}(*<*)oops;(*>*)
    1.41  
    1.42  lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
    1.43 -txt{*\noindent
    1.44 -becomes
    1.45 -\begin{isabelle}\makeatother
    1.46 -~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
    1.47 -~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
    1.48 -\end{isabelle}
    1.49 -by typing
    1.50 -*}
    1.51 +apply(simp only: split: list.split);
    1.52  
    1.53 -apply(simp only: split: list.split);
    1.54 -(*<*)oops;(*>*)
    1.55 -
    1.56 -text{*\noindent
    1.57 +txt{*
    1.58 +@{subgoals[display,indent=0]}
    1.59  In contrast to @{text"if"}-expressions, the simplifier does not split
    1.60  @{text"case"}-expressions by default because this can lead to nontermination
    1.61  in case of recursive datatypes. Again, if the @{text"only:"} modifier is
    1.62  dropped, the above goal is solved,
    1.63  *}
    1.64 -(*<*)
    1.65 +(*<*)oops;
    1.66  lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
    1.67  (*>*)
    1.68  apply(simp split: list.split);
    1.69 @@ -317,17 +302,11 @@
    1.70  
    1.71  lemma "if xs = [] then ys ~= [] else ys = [] ==> xs @ ys ~= []"
    1.72  apply(simp only: split: split_if_asm);
    1.73 -(*<*)
    1.74 -by(simp_all)
    1.75 -(*>*)
    1.76  
    1.77 -text{*\noindent
    1.78 +txt{*\noindent
    1.79  In contrast to splitting the conclusion, this actually creates two
    1.80  separate subgoals (which are solved by @{text"simp_all"}):
    1.81 -\begin{isabelle}
    1.82 -\ \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
    1.83 -\ \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}
    1.84 -\end{isabelle}
    1.85 +@{subgoals[display,indent=0]}
    1.86  If you need to split both in the assumptions and the conclusion,
    1.87  use $t$@{text".splits"} which subsumes $t$@{text".split"} and
    1.88  $t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}.
    1.89 @@ -343,6 +322,9 @@
    1.90  
    1.91  \index{*split|)}
    1.92  *}
    1.93 +(*<*)
    1.94 +by(simp_all)
    1.95 +(*>*)
    1.96  
    1.97  
    1.98  subsubsection{*Arithmetic*}