--- a/doc-src/TutorialI/CodeGen/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
@@ -1,1 +1,2 @@
+use "../settings.ML";
use_thy "CodeGen";
--- a/doc-src/TutorialI/Datatype/Fundata.thy Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy Tue Sep 05 09:03:17 2000 +0200
@@ -11,9 +11,7 @@
@{typ"nat"}, we have an infinitely branching tree because each node
has as many subtrees as there are natural numbers. How can we possibly
write down such a tree? Using functional notation! For example, the term
-\begin{quote}
@{term[display]"Branch 0 (%i. Branch i (%n. Tip))"}
-\end{quote}
of type @{typ"(nat,nat)bigtree"} is the tree whose
root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
has merely @{term"Tip"}s as further subtrees.
--- a/doc-src/TutorialI/Datatype/Nested.thy Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Tue Sep 05 09:03:17 2000 +0200
@@ -76,9 +76,7 @@
\begin{exercise}
The fact that substitution distributes over composition can be expressed
roughly as follows:
-\begin{quote}
@{text[display]"subst (f o g) t = subst f (subst g t)"}
-\end{quote}
Correct this statement (you will find that it does not type-check),
strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
its definition is found in theorem @{thm[source]o_def}).
@@ -92,9 +90,7 @@
The experienced functional programmer may feel that our above definition of
@{term"subst"} is unnecessarily complicated in that @{term"substs"} is
completely unnecessary. The @{term"App"}-case can be defined directly as
-\begin{quote}
@{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
-\end{quote}
where @{term"map"} is the standard list function such that
@{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle
insists on the above fixed format. Fortunately, we can easily \emph{prove}
--- a/doc-src/TutorialI/Datatype/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Datatype/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
@@ -1,3 +1,4 @@
+use "../settings.ML";
use_thy "ABexpr";
use_thy "unfoldnested";
use_thy "Nested";
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Sep 05 09:03:17 2000 +0200
@@ -10,13 +10,11 @@
\isa{nat}, we have an infinitely branching tree because each node
has as many subtrees as there are natural numbers. How can we possibly
write down such a tree? Using functional notation! For example, the term
-\begin{quote}
-
+%
\begin{isabelle}%
-Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}
+\ \ \ \ \ Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
\end{isabelle}%
-\end{quote}
of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
has merely \isa{Tip}s as further subtrees.
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Tue Sep 05 09:03:17 2000 +0200
@@ -71,13 +71,11 @@
\begin{exercise}
The fact that substitution distributes over composition can be expressed
roughly as follows:
-\begin{quote}
-
+%
\begin{isabelle}%
-subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}
+\ \ \ \ \ subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
\end{isabelle}%
-\end{quote}
Correct this statement (you will find that it does not type-check),
strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
its definition is found in theorem \isa{o{\isacharunderscore}def}).
@@ -91,13 +89,11 @@
The experienced functional programmer may feel that our above definition of
\isa{subst} is unnecessarily complicated in that \isa{substs} is
completely unnecessary. The \isa{App}-case can be defined directly as
-\begin{quote}
-
+%
\begin{isabelle}%
-subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}
+\ \ \ \ \ subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}%
\end{isabelle}%
-\end{quote}
where \isa{map} is the standard list function such that
\isa{map\ f\ {\isacharbrackleft}x\isadigit{1}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}xn{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}f\ x\isadigit{1}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}f\ xn{\isacharbrackright}}. This is true, but Isabelle
insists on the above fixed format. Fortunately, we can easily \emph{prove}
--- a/doc-src/TutorialI/Ifexpr/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
@@ -1,1 +1,2 @@
+use "../settings.ML";
use_thy "Ifexpr";
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Sep 05 09:03:17 2000 +0200
@@ -135,9 +135,7 @@
usually known as ``mathematical induction''. There is also ``complete
induction'', where you must prove $P(n)$ under the assumption that $P(m)$
holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]less_induct}:
-\begin{quote}
@{thm[display]"less_induct"[no_vars]}
-\end{quote}
Here is an example of its application.
*};
@@ -267,9 +265,7 @@
text{*\noindent
The elimination rule @{thm[source]less_SucE} expresses the case distinction:
-\begin{quote}
@{thm[display]"less_SucE"[no_vars]}
-\end{quote}
Now it is straightforward to derive the original version of
@{thm[source]less_induct} by manipulting the conclusion of the above lemma:
@@ -285,9 +281,7 @@
text{*\noindent
Finally we should mention that HOL already provides the mother of all
inductions, \emph{wellfounded induction} (@{thm[source]wf_induct}):
-\begin{quote}
@{thm[display]"wf_induct"[no_vars]}
-\end{quote}
where @{term"wf r"} means that the relation @{term"r"} is wellfounded.
For example @{thm[source]less_induct} is the special case where @{term"r"} is
@{text"<"} on @{typ"nat"}. For details see the library.
--- a/doc-src/TutorialI/Misc/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
@@ -1,3 +1,4 @@
+use "../settings.ML";
use_thy "Tree";
use_thy "Tree2";
use_thy "case_exprs";
--- a/doc-src/TutorialI/Misc/case_exprs.thy Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/case_exprs.thy Tue Sep 05 09:03:17 2000 +0200
@@ -7,9 +7,7 @@
text{*\label{sec:case-expressions}
HOL also features \isaindexbold{case}-expressions for analyzing
elements of a datatype. For example,
-\begin{quote}
@{term[display]"case xs of [] => 1 | y#ys => y"}
-\end{quote}
evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if
@{term"xs"} is @{term"y#ys"}. (Since the result in both branches must be of
the same type, it follows that @{term"y"} is of type @{typ"nat"} and hence
@@ -34,15 +32,9 @@
\noindent
Nested patterns can be simulated by nested @{text"case"}-expressions: instead
of
-%
-\begin{quote}
-@{text"case xs of [] => 1 | [x] => x | x#(y#zs) => y"}
-%~~~case~xs~of~[]~{\isasymRightarrow}~1~|~[x]~{\isasymRightarrow}~x~|~x~\#~y~\#~zs~{\isasymRightarrow}~y
-\end{quote}
+@{text[display]"case xs of [] => 1 | [x] => x | x # (y # zs) => y"}
write
-\begin{quote}
@{term[display,eta_contract=false,margin=50]"case xs of [] => 1 | x#ys => (case ys of [] => x | y#zs => y)"}
-\end{quote}
Note that @{text"case"}-expressions may need to be enclosed in parentheses to
indicate their scope
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Sep 05 09:03:17 2000 +0200
@@ -120,13 +120,11 @@
usually known as ``mathematical induction''. There is also ``complete
induction'', where you must prove $P(n)$ under the assumption that $P(m)$
holds for all $m<n$. In Isabelle, this is the theorem \isa{less{\isacharunderscore}induct}:
-\begin{quote}
-
+%
\begin{isabelle}%
-{\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n
+\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
\end{isabelle}%
-\end{quote}
Here is an example of its application.%
\end{isamarkuptext}%
\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isanewline
@@ -242,13 +240,11 @@
\begin{isamarkuptext}%
\noindent
The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
-\begin{quote}
-
+%
\begin{isabelle}%
-{\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P
+\ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
\end{isabelle}%
-\end{quote}
Now it is straightforward to derive the original version of
\isa{less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma:
@@ -263,13 +259,11 @@
\noindent
Finally we should mention that HOL already provides the mother of all
inductions, \emph{wellfounded induction} (\isa{wf{\isacharunderscore}induct}):
-\begin{quote}
-
+%
\begin{isabelle}%
-{\isasymlbrakk}wf\ r{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a
+\ \ \ \ \ {\isasymlbrakk}wf\ r{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a%
\end{isabelle}%
-\end{quote}
where \isa{wf\ r} means that the relation \isa{r} is wellfounded.
For example \isa{less{\isacharunderscore}induct} is the special case where \isa{r} is
\isa{{\isacharless}} on \isa{nat}. For details see the library.%
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Tue Sep 05 09:03:17 2000 +0200
@@ -7,13 +7,11 @@
\label{sec:case-expressions}
HOL also features \isaindexbold{case}-expressions for analyzing
elements of a datatype. For example,
-\begin{quote}
-
+%
\begin{isabelle}%
-case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y
+\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
\end{isabelle}%
-\end{quote}
evaluates to \isa{\isadigit{1}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if
\isa{xs} is \isa{y\ {\isacharhash}\ ys}. (Since the result in both branches must be of
the same type, it follows that \isa{y} is of type \isa{nat} and hence
@@ -38,20 +36,18 @@
\noindent
Nested patterns can be simulated by nested \isa{case}-expressions: instead
of
-%
-\begin{quote}
-\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ \isadigit{1}\ {\isacharbar}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ x\ {\isacharbar}\ x{\isacharhash}{\isacharparenleft}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}{\isachargreater}\ y}
-%~~~case~xs~of~[]~{\isasymRightarrow}~1~|~[x]~{\isasymRightarrow}~x~|~x~\#~y~\#~zs~{\isasymRightarrow}~y
-\end{quote}
-write
-\begin{quote}
-
+%
\begin{isabelle}%
-case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\isanewline
-{\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y
+\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ \isadigit{1}\ {\isacharbar}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ x\ {\isacharbar}\ x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}\ {\isacharequal}{\isachargreater}\ y%
\end{isabelle}%
-\end{quote}
+write
+%
+\begin{isabelle}%
+\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\isanewline
+\ \ \ \ \ {\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y%
+\end{isabelle}%
+
Note that \isa{case}-expressions may need to be enclosed in parentheses to
indicate their scope%
--- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Tue Sep 05 09:03:17 2000 +0200
@@ -4,13 +4,11 @@
\begin{isamarkuptext}%
\noindent
In particular, there are \isa{case}-expressions, for example
-\begin{quote}
-
+%
\begin{isabelle}%
-case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m
+\ \ \ \ \ case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
\end{isabelle}%
-\end{quote}
primitive recursion, for example%
\end{isamarkuptext}%
\isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
--- a/doc-src/TutorialI/Misc/natsum.thy Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy Tue Sep 05 09:03:17 2000 +0200
@@ -3,9 +3,7 @@
(*>*)
text{*\noindent
In particular, there are @{text"case"}-expressions, for example
-\begin{quote}
@{term[display]"case n of 0 => 0 | Suc m => m"}
-\end{quote}
primitive recursion, for example
*}
--- a/doc-src/TutorialI/Recdef/Nested1.thy Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Tue Sep 05 09:03:17 2000 +0200
@@ -22,9 +22,7 @@
Remember that function @{term"size"} is defined for each \isacommand{datatype}.
However, the definition does not succeed. Isabelle complains about an
unproved termination condition
-\begin{quote}
@{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
-\end{quote}
where @{term"set"} returns the set of elements of a list (no special
knowledge of sets is required in the following) and @{text"term_list_size ::
term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle
--- a/doc-src/TutorialI/Recdef/Nested2.thy Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy Tue Sep 05 09:03:17 2000 +0200
@@ -28,9 +28,7 @@
apply(induct_tac t rule:trev.induct);
txt{*\noindent
This leaves us with a trivial base case @{term"trev (trev (Var x)) = Var x"} and the step case
-\begin{quote}
@{term[display,margin=60]"ALL t. t : set ts --> trev (trev t) = t ==> trev (trev (App f ts)) = App f ts"}
-\end{quote}
both of which are solved by simplification:
*};
@@ -67,9 +65,7 @@
(term_list_size ts)"}, without any assumption about @{term"t"}. Therefore
\isacommand{recdef} has been supplied with the congruence theorem
@{thm[source]map_cong}:
-\begin{quote}
@{thm[display,margin=50]"map_cong"[no_vars]}
-\end{quote}
Its second premise expresses (indirectly) that the second argument of
@{term"map"} is only applied to elements of its third argument. Congruence
rules for other higher-order functions on lists would look very similar but
--- a/doc-src/TutorialI/Recdef/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
@@ -1,3 +1,4 @@
+use "../settings";
use_thy "termination";
use_thy "Induction";
use_thy "Nested1";
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Tue Sep 05 09:03:17 2000 +0200
@@ -20,13 +20,11 @@
Remember that function \isa{size} is defined for each \isacommand{datatype}.
However, the definition does not succeed. Isabelle complains about an
unproved termination condition
-\begin{quote}
-
+%
\begin{isabelle}%
-t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}
+\ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}%
\end{isabelle}%
-\end{quote}
where \isa{set} returns the set of elements of a list (no special
knowledge of sets is required in the following) and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary function automatically defined by Isabelle
(when \isa{term} was defined). First we have to understand why the
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Sep 05 09:03:17 2000 +0200
@@ -22,14 +22,12 @@
\begin{isamarkuptxt}%
\noindent
This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x} and the step case
-\begin{quote}
-
+%
\begin{isabelle}%
-{\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline
-trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts
+\ \ \ \ \ {\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline
+\ \ \ \ \ trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts%
\end{isabelle}%
-\end{quote}
both of which are solved by simplification:%
\end{isamarkuptxt}%
\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%
@@ -64,14 +62,12 @@
\isacommand{recdef} would try to prove the unprovable \isa{size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}}, without any assumption about \isa{t}. Therefore
\isacommand{recdef} has been supplied with the congruence theorem
\isa{map{\isacharunderscore}cong}:
-\begin{quote}
-
+%
\begin{isabelle}%
-{\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
-{\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys
+\ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
+\ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
\end{isabelle}%
-\end{quote}
Its second premise expresses (indirectly) that the second argument of
\isa{map} is only applied to elements of its third argument. Congruence
rules for other higher-order functions on lists would look very similar but
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Tue Sep 05 09:03:17 2000 +0200
@@ -16,13 +16,11 @@
\noindent
According to the measure function, the second argument should decrease with
each recursive call. The resulting termination condition
-\begin{quote}
-
+%
\begin{isabelle}%
-n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n
+\ \ \ \ \ n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
\end{isabelle}%
-\end{quote}
is provded automatically because it is already present as a lemma in the
arithmetic library. Thus the recursion equation becomes a simplification
rule. Of course the equation is nonterminating if we are allowed to unfold
@@ -31,29 +29,23 @@
something else which leads to the same problem: it splits \isa{if}s if the
condition simplifies to neither \isa{True} nor \isa{False}. For
example, simplification reduces
-\begin{quote}
-
+%
\begin{isabelle}%
-gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k
+\ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
\end{isabelle}%
-\end{quote}
in one step to
-\begin{quote}
-
+%
\begin{isabelle}%
-{\isacharparenleft}if\ n\ {\isacharequal}\ \isadigit{0}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k
+\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ \isadigit{0}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
\end{isabelle}%
-\end{quote}
where the condition cannot be reduced further, and splitting leads to
-\begin{quote}
-
+%
\begin{isabelle}%
-{\isacharparenleft}n\ {\isacharequal}\ \isadigit{0}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}
+\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ \isadigit{0}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
\end{isabelle}%
-\end{quote}
Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
an \isa{if}, it is unfolded again, which leads to an infinite chain of
simplification steps. Fortunately, this problem can be avoided in many
--- a/doc-src/TutorialI/Recdef/simplification.thy Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy Tue Sep 05 09:03:17 2000 +0200
@@ -18,9 +18,7 @@
text{*\noindent
According to the measure function, the second argument should decrease with
each recursive call. The resulting termination condition
-\begin{quote}
@{term[display]"n ~= 0 ==> m mod n < n"}
-\end{quote}
is provded automatically because it is already present as a lemma in the
arithmetic library. Thus the recursion equation becomes a simplification
rule. Of course the equation is nonterminating if we are allowed to unfold
@@ -29,17 +27,11 @@
something else which leads to the same problem: it splits @{text"if"}s if the
condition simplifies to neither @{term"True"} nor @{term"False"}. For
example, simplification reduces
-\begin{quote}
@{term[display]"gcd(m,n) = k"}
-\end{quote}
in one step to
-\begin{quote}
@{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
-\end{quote}
where the condition cannot be reduced further, and splitting leads to
-\begin{quote}
@{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
-\end{quote}
Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
an @{text"if"}, it is unfolded again, which leads to an infinite chain of
simplification steps. Fortunately, this problem can be avoided in many
--- a/doc-src/TutorialI/ToyList/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/ToyList/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
@@ -1,2 +1,3 @@
+use "../settings.ML";
use_thy "ToyList";
--- a/doc-src/TutorialI/Trie/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Trie/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
@@ -1,2 +1,3 @@
+use "../settings.ML";
use_thy "Option2";
use_thy "Trie";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/settings.ML Tue Sep 05 09:03:17 2000 +0200
@@ -0,0 +1,1 @@
+IsarOutput.indent := 5;