--- a/doc-src/TutorialI/CTL/Base.thy Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/CTL/Base.thy Tue Oct 31 08:53:12 2000 +0100
@@ -2,7 +2,7 @@
section{*Case study: Verified model checking*}
-text{*
+text{*\label{sec:VMC}
Model checking is a very popular technique for the verification of finite
state systems (implementations) w.r.t.\ temporal logic formulae
(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
--- a/doc-src/TutorialI/CTL/document/Base.tex Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex Tue Oct 31 08:53:12 2000 +0100
@@ -5,6 +5,7 @@
\isamarkupsection{Case study: Verified model checking}
%
\begin{isamarkuptext}%
+\label{sec:VMC}
Model checking is a very popular technique for the verification of finite
state systems (implementations) w.r.t.\ temporal logic formulae
(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
--- a/doc-src/TutorialI/IsaMakefile Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/IsaMakefile Tue Oct 31 08:53:12 2000 +0100
@@ -142,7 +142,7 @@
HOL-Types: HOL $(LOG)/HOL-Types.gz
-$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
+$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML Types/Typedef.thy \
Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
Types/Overloading.thy Types/Axioms.thy
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Types
--- a/doc-src/TutorialI/Misc/Itrev.thy Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Misc/Itrev.thy Tue Oct 31 08:53:12 2000 +0100
@@ -35,7 +35,7 @@
gradually, using only @{text"#"}:
*}
-consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
+consts itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list";
primrec
"itrev [] ys = ys"
"itrev (x#xs) ys = itrev xs (x#ys)";
@@ -75,7 +75,7 @@
*};
(*<*)oops;(*>*)
lemma "itrev xs ys = rev xs @ ys";
-
+(*<*)apply(induct_tac xs, simp_all)(*>*)
txt{*\noindent
If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
@{term"rev xs"}, just as required.
@@ -87,11 +87,7 @@
Although we now have two variables, only @{term"xs"} is suitable for
induction, and we repeat our above proof attempt. Unfortunately, we are still
not there:
-\begin{isabelle}\makeatother
-~1.~{\isasymAnd}a~list.\isanewline
-~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
-~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
-\end{isabelle}
+@{subgoals[display,indent=0,goals_limit=1]}
The induction hypothesis is still too weak, but this time it takes no
intuition to generalize: the problem is that @{term"ys"} is fixed throughout
the subgoal, but the induction hypothesis needs to be applied with
@@ -99,7 +95,7 @@
for all @{term"ys"} instead of a fixed one:
*};
(*<*)oops;(*>*)
-lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
+lemma "\<forall>ys. itrev xs ys = rev xs @ ys";
(*<*)
by(induct_tac xs, simp_all);
(*>*)
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Tue Oct 31 08:53:12 2000 +0100
@@ -84,10 +84,10 @@
Although we now have two variables, only \isa{xs} is suitable for
induction, and we repeat our above proof attempt. Unfortunately, we are still
not there:
-\begin{isabelle}\makeatother
-~1.~{\isasymAnd}a~list.\isanewline
-~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
-~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
+\ \ \ \ \ \ \ itrev\ list\ ys\ {\isacharequal}\ rev\ list\ {\isacharat}\ ys\ {\isasymLongrightarrow}\isanewline
+\ \ \ \ \ \ \ itrev\ list\ {\isacharparenleft}a\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ ys%
\end{isabelle}
The induction hypothesis is still too weak, but this time it takes no
intuition to generalize: the problem is that \isa{ys} is fixed throughout
--- a/doc-src/TutorialI/Misc/document/simp.tex Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Tue Oct 31 08:53:12 2000 +0100
@@ -151,8 +151,8 @@
\begin{isamarkuptxt}%
\noindent
In this particular case, the resulting goal
-\begin{isabelle}
-~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ A\ {\isasymand}\ {\isasymnot}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ A\ {\isasymand}\ {\isasymnot}\ A%
\end{isabelle}
can be proved by simplification. Thus we could have proved the lemma outright by%
\end{isamarkuptxt}%
@@ -227,15 +227,14 @@
\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}~[])
-\end{isabelle}
-by a degenerate form of simplification%
+can be split by a degenerate form of simplification%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
-\begin{isamarkuptext}%
+\begin{isamarkuptxt}%
\noindent
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymforall}xs{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}%
+\end{isabelle}
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{\isacharcolon}}). Because
@@ -244,25 +243,20 @@
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}%
+\end{isamarkuptxt}%
+\isanewline
+\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}\isanewline
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
\begin{isamarkuptxt}%
-\noindent
-becomes
-\begin{isabelle}\makeatother
-~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
-~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}\ {\isasymand}\isanewline
+\ \ \ \ {\isacharparenleft}{\isasymforall}a\ list{\isachardot}\ xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymlongrightarrow}\ a\ {\isacharhash}\ list\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}%
\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{\isacharcolon}} modifier is
dropped, the above goal is solved,%
-\end{isamarkuptext}%
+\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
\begin{isamarkuptext}%
\noindent%
@@ -292,13 +286,13 @@
\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{isamarkuptext}%
+\begin{isamarkuptxt}%
\noindent
In contrast to splitting the conclusion, this actually creates two
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}
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}%
\end{isabelle}
If you need to split both in the assumptions and the conclusion,
use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and
@@ -314,7 +308,7 @@
\end{warn}
\index{*split|)}%
-\end{isamarkuptext}%
+\end{isamarkuptxt}%
%
\isamarkupsubsubsection{Arithmetic}
%
--- a/doc-src/TutorialI/Misc/simp.thy Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy Tue Oct 31 08:53:12 2000 +0100
@@ -154,9 +154,7 @@
txt{*\noindent
In this particular case, the resulting goal
-\begin{isabelle}
-~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
-\end{isabelle}
+@{subgoals[display,indent=0]}
can be proved by simplification. Thus we could have proved the lemma outright by
*}(*<*)oops;lemma "exor A (\<not>A)";(*>*)
apply(simp add: exor_def)
@@ -237,17 +235,13 @@
lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";
txt{*\noindent
-can be split into
-\begin{isabelle}
-~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
-\end{isabelle}
-by a degenerate form of simplification
+can be split by a degenerate form of simplification
*}
apply(simp only: split: split_if);
-(*<*)oops;(*>*)
-text{*\noindent
+txt{*\noindent
+@{subgoals[display,indent=0]}
where no simplification rules are included (@{text"only:"} is followed by the
empty list of theorems) but the rule \isaindexbold{split_if} for
splitting @{text"if"}s is added (via the modifier @{text"split:"}). Because
@@ -256,28 +250,19 @@
on the initial goal above.
This splitting idea generalizes from @{text"if"} to \isaindex{case}:
-*}
+*}(*<*)oops;(*>*)
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
-txt{*\noindent
-becomes
-\begin{isabelle}\makeatother
-~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
-~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
-\end{isabelle}
-by typing
-*}
+apply(simp only: split: list.split);
-apply(simp only: split: list.split);
-(*<*)oops;(*>*)
-
-text{*\noindent
+txt{*
+@{subgoals[display,indent=0]}
In contrast to @{text"if"}-expressions, the simplifier does not split
@{text"case"}-expressions by default because this can lead to nontermination
in case of recursive datatypes. Again, if the @{text"only:"} modifier is
dropped, the above goal is solved,
*}
-(*<*)
+(*<*)oops;
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
(*>*)
apply(simp split: list.split);
@@ -317,17 +302,11 @@
lemma "if xs = [] then ys ~= [] else ys = [] ==> xs @ ys ~= []"
apply(simp only: split: split_if_asm);
-(*<*)
-by(simp_all)
-(*>*)
-text{*\noindent
+txt{*\noindent
In contrast to splitting the conclusion, this actually creates two
separate subgoals (which are solved by @{text"simp_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}
+@{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}.
@@ -343,6 +322,9 @@
\index{*split|)}
*}
+(*<*)
+by(simp_all)
+(*>*)
subsubsection{*Arithmetic*}
--- a/doc-src/TutorialI/Recdef/Induction.thy Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Recdef/Induction.thy Tue Oct 31 08:53:12 2000 +0100
@@ -31,13 +31,7 @@
txt{*\noindent
The resulting proof state has three subgoals corresponding to the three
clauses for @{term"sep"}:
-\begin{isabelle}
-~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
-~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
-~3.~{\isasymAnd}a~x~y~zs.\isanewline
-~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
-~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
-\end{isabelle}
+@{subgoals[display,indent=0]}
The rest is pure simplification:
*}
--- a/doc-src/TutorialI/Recdef/document/Induction.tex Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Oct 31 08:53:12 2000 +0100
@@ -29,12 +29,12 @@
\noindent
The resulting proof state has three subgoals corresponding to the three
clauses for \isa{sep}:
-\begin{isabelle}
-~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
-~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
-~3.~{\isasymAnd}a~x~y~zs.\isanewline
-~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
-~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ x{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\isanewline
+\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}a\ x\ y\ zs{\isachardot}\isanewline
+\ \ \ \ \ \ \ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
+\ \ \ \ \ \ \ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}%
\end{isabelle}
The rest is pure simplification:%
\end{isamarkuptxt}%
--- a/doc-src/TutorialI/Recdef/document/examples.tex Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Recdef/document/examples.tex Tue Oct 31 08:53:12 2000 +0100
@@ -64,7 +64,7 @@
\end{isamarkuptext}%
\isacommand{consts}\ sep{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
\isacommand{recdef}\ sep{\isadigit{2}}\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
-\ \ {\isachardoublequote}sep{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{2}}\ zs\ a{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{2}}\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}\ a{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}sep{\isadigit{2}}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
Because of its pattern-matching syntax, \isacommand{recdef} is also useful
--- a/doc-src/TutorialI/Recdef/examples.thy Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Recdef/examples.thy Tue Oct 31 08:53:12 2000 +0100
@@ -69,7 +69,7 @@
*}
consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list";
recdef sep2 "measure length"
- "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 zs a)"
+ "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 (y#zs) a)"
"sep2 xs = (\<lambda>a. xs)";
text{*
--- a/doc-src/TutorialI/ToyList/ToyList.thy Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Tue Oct 31 08:53:12 2000 +0100
@@ -248,13 +248,10 @@
apply(auto);
txt{*
-\begin{isabelle}
-~1.~rev~ys~=~rev~ys~@~[]\isanewline
-~2. \dots
-\end{isabelle}
-Again, we need to abandon this proof attempt and prove another simple lemma first.
-In the future the step of abandoning an incomplete proof before embarking on
-the proof of a lemma usually remains implicit.
+@{subgoals[display,indent=0,goals_limit=1]}
+Again, we need to abandon this proof attempt and prove another simple lemma
+first. In the future the step of abandoning an incomplete proof before
+embarking on the proof of a lemma usually remains implicit.
*}
(*<*)
oops
@@ -273,11 +270,7 @@
txt{*
\noindent
leads to the desired message @{text"No subgoals!"}:
-\begin{isabelle}
-xs~@~[]~=~xs\isanewline
-No~subgoals!
-\end{isabelle}
-
+@{goals[display,indent=0]}
We still need to confirm that the proof is now finished:
*}
@@ -306,11 +299,7 @@
\noindent
we find that this time @{text"auto"} solves the base case, but the
induction step merely simplifies to
-\begin{isabelle}
-~1.~{\isasymAnd}a~list.\isanewline
-~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
-~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
-\end{isabelle}
+@{subgoals[display,indent=0,goals_limit=1]}
Now we need to remember that @{text"@"} associates to the right, and that
@{text"#"} and @{text"@"} have the same priority (namely the @{text"65"}
in their \isacommand{infixr} annotation). Thus the conclusion really is
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Oct 31 08:53:12 2000 +0100
@@ -234,13 +234,12 @@
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
\begin{isamarkuptxt}%
-\begin{isabelle}
-~1.~rev~ys~=~rev~ys~@~[]\isanewline
-~2. \dots
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ rev\ ys\ {\isacharequal}\ rev\ ys\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}%
\end{isabelle}
-Again, we need to abandon this proof attempt and prove another simple lemma first.
-In the future the step of abandoning an incomplete proof before embarking on
-the proof of a lemma usually remains implicit.%
+Again, we need to abandon this proof attempt and prove another simple lemma
+first. In the future the step of abandoning an incomplete proof before
+embarking on the proof of a lemma usually remains implicit.%
\end{isamarkuptxt}%
%
\isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}}
@@ -254,11 +253,10 @@
\begin{isamarkuptxt}%
\noindent
leads to the desired message \isa{No\ subgoals{\isacharbang}}:
-\begin{isabelle}
-xs~@~[]~=~xs\isanewline
-No~subgoals!
+\begin{isabelle}%
+xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
+No\ subgoals{\isacharbang}%
\end{isabelle}
-
We still need to confirm that the proof is now finished:%
\end{isamarkuptxt}%
\isacommand{done}%
@@ -284,10 +282,10 @@
\noindent
we find that this time \isa{auto} solves the base case, but the
induction step merely simplifies to
-\begin{isabelle}
-~1.~{\isasymAnd}a~list.\isanewline
-~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
-~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
+\ \ \ \ \ \ \ rev\ {\isacharparenleft}list\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isasymLongrightarrow}\isanewline
+\ \ \ \ \ \ \ {\isacharparenleft}rev\ ys\ {\isacharat}\ rev\ list{\isacharparenright}\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}%
\end{isabelle}
Now we need to remember that \isa{{\isacharat}} associates to the right, and that
\isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}}
--- a/doc-src/TutorialI/Types/Axioms.thy Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Types/Axioms.thy Tue Oct 31 08:53:12 2000 +0100
@@ -59,7 +59,7 @@
txt{*\noindent
This time @{text intro_classes} leaves us with the four axioms,
specialized to type @{typ bool}, as subgoals:
-@{goals[display,show_types,indent=0]}
+@{subgoals[display,show_types,indent=0]}
Fortunately, the proof is easy for blast, once we have unfolded the definitions
of @{text"<<"} and @{text"<<="} at @{typ bool}:
*}
--- a/doc-src/TutorialI/Types/ROOT.ML Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Types/ROOT.ML Tue Oct 31 08:53:12 2000 +0100
@@ -1,4 +1,5 @@
use "../settings.ML";
+use_thy "Typedef";
use_thy "Overloading0";
use_thy "Overloading2";
use_thy "Axioms";
--- a/doc-src/TutorialI/Types/document/Axioms.tex Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Tue Oct 31 08:53:12 2000 +0100
@@ -59,7 +59,6 @@
This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms,
specialized to type \isa{bool}, as subgoals:
\begin{isabelle}%
-OFCLASS{\isacharparenleft}bool{\isacharcomma}\ parord{\isacharunderscore}class{\isacharparenright}\isanewline
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}\ z{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z\isanewline
\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline
--- a/doc-src/TutorialI/Types/types.tex Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Types/types.tex Tue Oct 31 08:53:12 2000 +0100
@@ -9,11 +9,13 @@
({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to reason
about them.
\item Introducing your own types: how to introduce your own new types that
- cannot be constructed with any of the basic methods ({\S}\ref{sec:typedef}).
+ cannot be constructed with any of the basic methods ({\S}\ref{sec:adv-typedef}).
\item Type classes: how to specify and reason about axiomatic collections of
types ({\S}\ref{sec:axclass}).
\end{itemize}
+\input{Types/document/Typedef}
+
\section{Axiomatic type classes}
\label{sec:axclass}
\index{axiomatic type class|(}
@@ -42,7 +44,7 @@
\index{overloading|)}
-\input{Types/document/Axioms0}
+\input{Types/document/Axioms}
\index{axiomatic type class|)}
\index{*axclass|)}