1.1 --- a/doc-src/TutorialI/CodeGen/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
1.2 +++ b/doc-src/TutorialI/CodeGen/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
1.3 @@ -1,1 +1,2 @@
1.4 +use "../settings.ML";
1.5 use_thy "CodeGen";
2.1 --- a/doc-src/TutorialI/Datatype/Fundata.thy Mon Sep 04 21:20:14 2000 +0200
2.2 +++ b/doc-src/TutorialI/Datatype/Fundata.thy Tue Sep 05 09:03:17 2000 +0200
2.3 @@ -11,9 +11,7 @@
2.4 @{typ"nat"}, we have an infinitely branching tree because each node
2.5 has as many subtrees as there are natural numbers. How can we possibly
2.6 write down such a tree? Using functional notation! For example, the term
2.7 -\begin{quote}
2.8 @{term[display]"Branch 0 (%i. Branch i (%n. Tip))"}
2.9 -\end{quote}
2.10 of type @{typ"(nat,nat)bigtree"} is the tree whose
2.11 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
2.12 has merely @{term"Tip"}s as further subtrees.
3.1 --- a/doc-src/TutorialI/Datatype/Nested.thy Mon Sep 04 21:20:14 2000 +0200
3.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy Tue Sep 05 09:03:17 2000 +0200
3.3 @@ -76,9 +76,7 @@
3.4 \begin{exercise}
3.5 The fact that substitution distributes over composition can be expressed
3.6 roughly as follows:
3.7 -\begin{quote}
3.8 @{text[display]"subst (f o g) t = subst f (subst g t)"}
3.9 -\end{quote}
3.10 Correct this statement (you will find that it does not type-check),
3.11 strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
3.12 its definition is found in theorem @{thm[source]o_def}).
3.13 @@ -92,9 +90,7 @@
3.14 The experienced functional programmer may feel that our above definition of
3.15 @{term"subst"} is unnecessarily complicated in that @{term"substs"} is
3.16 completely unnecessary. The @{term"App"}-case can be defined directly as
3.17 -\begin{quote}
3.18 @{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
3.19 -\end{quote}
3.20 where @{term"map"} is the standard list function such that
3.21 @{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle
3.22 insists on the above fixed format. Fortunately, we can easily \emph{prove}
4.1 --- a/doc-src/TutorialI/Datatype/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
4.2 +++ b/doc-src/TutorialI/Datatype/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
4.3 @@ -1,3 +1,4 @@
4.4 +use "../settings.ML";
4.5 use_thy "ABexpr";
4.6 use_thy "unfoldnested";
4.7 use_thy "Nested";
5.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Mon Sep 04 21:20:14 2000 +0200
5.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Sep 05 09:03:17 2000 +0200
5.3 @@ -10,13 +10,11 @@
5.4 \isa{nat}, we have an infinitely branching tree because each node
5.5 has as many subtrees as there are natural numbers. How can we possibly
5.6 write down such a tree? Using functional notation! For example, the term
5.7 -\begin{quote}
5.8 -
5.9 +%
5.10 \begin{isabelle}%
5.11 -Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}
5.12 +\ \ \ \ \ Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
5.13 \end{isabelle}%
5.14
5.15 -\end{quote}
5.16 of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
5.17 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
5.18 has merely \isa{Tip}s as further subtrees.
6.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex Mon Sep 04 21:20:14 2000 +0200
6.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Tue Sep 05 09:03:17 2000 +0200
6.3 @@ -71,13 +71,11 @@
6.4 \begin{exercise}
6.5 The fact that substitution distributes over composition can be expressed
6.6 roughly as follows:
6.7 -\begin{quote}
6.8 -
6.9 +%
6.10 \begin{isabelle}%
6.11 -subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}
6.12 +\ \ \ \ \ subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
6.13 \end{isabelle}%
6.14
6.15 -\end{quote}
6.16 Correct this statement (you will find that it does not type-check),
6.17 strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
6.18 its definition is found in theorem \isa{o{\isacharunderscore}def}).
6.19 @@ -91,13 +89,11 @@
6.20 The experienced functional programmer may feel that our above definition of
6.21 \isa{subst} is unnecessarily complicated in that \isa{substs} is
6.22 completely unnecessary. The \isa{App}-case can be defined directly as
6.23 -\begin{quote}
6.24 -
6.25 +%
6.26 \begin{isabelle}%
6.27 -subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}
6.28 +\ \ \ \ \ subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}%
6.29 \end{isabelle}%
6.30
6.31 -\end{quote}
6.32 where \isa{map} is the standard list function such that
6.33 \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
6.34 insists on the above fixed format. Fortunately, we can easily \emph{prove}
7.1 --- a/doc-src/TutorialI/Ifexpr/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
7.2 +++ b/doc-src/TutorialI/Ifexpr/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
7.3 @@ -1,1 +1,2 @@
7.4 +use "../settings.ML";
7.5 use_thy "Ifexpr";
8.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy Mon Sep 04 21:20:14 2000 +0200
8.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Sep 05 09:03:17 2000 +0200
8.3 @@ -135,9 +135,7 @@
8.4 usually known as ``mathematical induction''. There is also ``complete
8.5 induction'', where you must prove $P(n)$ under the assumption that $P(m)$
8.6 holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]less_induct}:
8.7 -\begin{quote}
8.8 @{thm[display]"less_induct"[no_vars]}
8.9 -\end{quote}
8.10 Here is an example of its application.
8.11 *};
8.12
8.13 @@ -267,9 +265,7 @@
8.14
8.15 text{*\noindent
8.16 The elimination rule @{thm[source]less_SucE} expresses the case distinction:
8.17 -\begin{quote}
8.18 @{thm[display]"less_SucE"[no_vars]}
8.19 -\end{quote}
8.20
8.21 Now it is straightforward to derive the original version of
8.22 @{thm[source]less_induct} by manipulting the conclusion of the above lemma:
8.23 @@ -285,9 +281,7 @@
8.24 text{*\noindent
8.25 Finally we should mention that HOL already provides the mother of all
8.26 inductions, \emph{wellfounded induction} (@{thm[source]wf_induct}):
8.27 -\begin{quote}
8.28 @{thm[display]"wf_induct"[no_vars]}
8.29 -\end{quote}
8.30 where @{term"wf r"} means that the relation @{term"r"} is wellfounded.
8.31 For example @{thm[source]less_induct} is the special case where @{term"r"} is
8.32 @{text"<"} on @{typ"nat"}. For details see the library.
9.1 --- a/doc-src/TutorialI/Misc/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
9.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
9.3 @@ -1,3 +1,4 @@
9.4 +use "../settings.ML";
9.5 use_thy "Tree";
9.6 use_thy "Tree2";
9.7 use_thy "case_exprs";
10.1 --- a/doc-src/TutorialI/Misc/case_exprs.thy Mon Sep 04 21:20:14 2000 +0200
10.2 +++ b/doc-src/TutorialI/Misc/case_exprs.thy Tue Sep 05 09:03:17 2000 +0200
10.3 @@ -7,9 +7,7 @@
10.4 text{*\label{sec:case-expressions}
10.5 HOL also features \isaindexbold{case}-expressions for analyzing
10.6 elements of a datatype. For example,
10.7 -\begin{quote}
10.8 @{term[display]"case xs of [] => 1 | y#ys => y"}
10.9 -\end{quote}
10.10 evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if
10.11 @{term"xs"} is @{term"y#ys"}. (Since the result in both branches must be of
10.12 the same type, it follows that @{term"y"} is of type @{typ"nat"} and hence
10.13 @@ -34,15 +32,9 @@
10.14 \noindent
10.15 Nested patterns can be simulated by nested @{text"case"}-expressions: instead
10.16 of
10.17 -%
10.18 -\begin{quote}
10.19 -@{text"case xs of [] => 1 | [x] => x | x#(y#zs) => y"}
10.20 -%~~~case~xs~of~[]~{\isasymRightarrow}~1~|~[x]~{\isasymRightarrow}~x~|~x~\#~y~\#~zs~{\isasymRightarrow}~y
10.21 -\end{quote}
10.22 +@{text[display]"case xs of [] => 1 | [x] => x | x # (y # zs) => y"}
10.23 write
10.24 -\begin{quote}
10.25 @{term[display,eta_contract=false,margin=50]"case xs of [] => 1 | x#ys => (case ys of [] => x | y#zs => y)"}
10.26 -\end{quote}
10.27
10.28 Note that @{text"case"}-expressions may need to be enclosed in parentheses to
10.29 indicate their scope
11.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Sep 04 21:20:14 2000 +0200
11.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Sep 05 09:03:17 2000 +0200
11.3 @@ -120,13 +120,11 @@
11.4 usually known as ``mathematical induction''. There is also ``complete
11.5 induction'', where you must prove $P(n)$ under the assumption that $P(m)$
11.6 holds for all $m<n$. In Isabelle, this is the theorem \isa{less{\isacharunderscore}induct}:
11.7 -\begin{quote}
11.8 -
11.9 +%
11.10 \begin{isabelle}%
11.11 -{\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n
11.12 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
11.13 \end{isabelle}%
11.14
11.15 -\end{quote}
11.16 Here is an example of its application.%
11.17 \end{isamarkuptext}%
11.18 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isanewline
11.19 @@ -242,13 +240,11 @@
11.20 \begin{isamarkuptext}%
11.21 \noindent
11.22 The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
11.23 -\begin{quote}
11.24 -
11.25 +%
11.26 \begin{isabelle}%
11.27 -{\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P
11.28 +\ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
11.29 \end{isabelle}%
11.30
11.31 -\end{quote}
11.32
11.33 Now it is straightforward to derive the original version of
11.34 \isa{less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma:
11.35 @@ -263,13 +259,11 @@
11.36 \noindent
11.37 Finally we should mention that HOL already provides the mother of all
11.38 inductions, \emph{wellfounded induction} (\isa{wf{\isacharunderscore}induct}):
11.39 -\begin{quote}
11.40 -
11.41 +%
11.42 \begin{isabelle}%
11.43 -{\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
11.44 +\ \ \ \ \ {\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%
11.45 \end{isabelle}%
11.46
11.47 -\end{quote}
11.48 where \isa{wf\ r} means that the relation \isa{r} is wellfounded.
11.49 For example \isa{less{\isacharunderscore}induct} is the special case where \isa{r} is
11.50 \isa{{\isacharless}} on \isa{nat}. For details see the library.%
12.1 --- a/doc-src/TutorialI/Misc/document/case_exprs.tex Mon Sep 04 21:20:14 2000 +0200
12.2 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Tue Sep 05 09:03:17 2000 +0200
12.3 @@ -7,13 +7,11 @@
12.4 \label{sec:case-expressions}
12.5 HOL also features \isaindexbold{case}-expressions for analyzing
12.6 elements of a datatype. For example,
12.7 -\begin{quote}
12.8 -
12.9 +%
12.10 \begin{isabelle}%
12.11 -case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y
12.12 +\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
12.13 \end{isabelle}%
12.14
12.15 -\end{quote}
12.16 evaluates to \isa{\isadigit{1}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if
12.17 \isa{xs} is \isa{y\ {\isacharhash}\ ys}. (Since the result in both branches must be of
12.18 the same type, it follows that \isa{y} is of type \isa{nat} and hence
12.19 @@ -38,20 +36,18 @@
12.20 \noindent
12.21 Nested patterns can be simulated by nested \isa{case}-expressions: instead
12.22 of
12.23 -%
12.24 -\begin{quote}
12.25 -\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}
12.26 -%~~~case~xs~of~[]~{\isasymRightarrow}~1~|~[x]~{\isasymRightarrow}~x~|~x~\#~y~\#~zs~{\isasymRightarrow}~y
12.27 -\end{quote}
12.28 -write
12.29 -\begin{quote}
12.30 -
12.31 +%
12.32 \begin{isabelle}%
12.33 -case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\isanewline
12.34 -{\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y
12.35 +\ \ \ \ \ 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%
12.36 \end{isabelle}%
12.37
12.38 -\end{quote}
12.39 +write
12.40 +%
12.41 +\begin{isabelle}%
12.42 +\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\isanewline
12.43 +\ \ \ \ \ {\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y%
12.44 +\end{isabelle}%
12.45 +
12.46
12.47 Note that \isa{case}-expressions may need to be enclosed in parentheses to
12.48 indicate their scope%
13.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Sep 04 21:20:14 2000 +0200
13.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Tue Sep 05 09:03:17 2000 +0200
13.3 @@ -4,13 +4,11 @@
13.4 \begin{isamarkuptext}%
13.5 \noindent
13.6 In particular, there are \isa{case}-expressions, for example
13.7 -\begin{quote}
13.8 -
13.9 +%
13.10 \begin{isabelle}%
13.11 -case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m
13.12 +\ \ \ \ \ case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
13.13 \end{isabelle}%
13.14
13.15 -\end{quote}
13.16 primitive recursion, for example%
13.17 \end{isamarkuptext}%
13.18 \isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
14.1 --- a/doc-src/TutorialI/Misc/natsum.thy Mon Sep 04 21:20:14 2000 +0200
14.2 +++ b/doc-src/TutorialI/Misc/natsum.thy Tue Sep 05 09:03:17 2000 +0200
14.3 @@ -3,9 +3,7 @@
14.4 (*>*)
14.5 text{*\noindent
14.6 In particular, there are @{text"case"}-expressions, for example
14.7 -\begin{quote}
14.8 @{term[display]"case n of 0 => 0 | Suc m => m"}
14.9 -\end{quote}
14.10 primitive recursion, for example
14.11 *}
14.12
15.1 --- a/doc-src/TutorialI/Recdef/Nested1.thy Mon Sep 04 21:20:14 2000 +0200
15.2 +++ b/doc-src/TutorialI/Recdef/Nested1.thy Tue Sep 05 09:03:17 2000 +0200
15.3 @@ -22,9 +22,7 @@
15.4 Remember that function @{term"size"} is defined for each \isacommand{datatype}.
15.5 However, the definition does not succeed. Isabelle complains about an
15.6 unproved termination condition
15.7 -\begin{quote}
15.8 @{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
15.9 -\end{quote}
15.10 where @{term"set"} returns the set of elements of a list (no special
15.11 knowledge of sets is required in the following) and @{text"term_list_size ::
15.12 term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle
16.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy Mon Sep 04 21:20:14 2000 +0200
16.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy Tue Sep 05 09:03:17 2000 +0200
16.3 @@ -28,9 +28,7 @@
16.4 apply(induct_tac t rule:trev.induct);
16.5 txt{*\noindent
16.6 This leaves us with a trivial base case @{term"trev (trev (Var x)) = Var x"} and the step case
16.7 -\begin{quote}
16.8 @{term[display,margin=60]"ALL t. t : set ts --> trev (trev t) = t ==> trev (trev (App f ts)) = App f ts"}
16.9 -\end{quote}
16.10 both of which are solved by simplification:
16.11 *};
16.12
16.13 @@ -67,9 +65,7 @@
16.14 (term_list_size ts)"}, without any assumption about @{term"t"}. Therefore
16.15 \isacommand{recdef} has been supplied with the congruence theorem
16.16 @{thm[source]map_cong}:
16.17 -\begin{quote}
16.18 @{thm[display,margin=50]"map_cong"[no_vars]}
16.19 -\end{quote}
16.20 Its second premise expresses (indirectly) that the second argument of
16.21 @{term"map"} is only applied to elements of its third argument. Congruence
16.22 rules for other higher-order functions on lists would look very similar but
17.1 --- a/doc-src/TutorialI/Recdef/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
17.2 +++ b/doc-src/TutorialI/Recdef/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
17.3 @@ -1,3 +1,4 @@
17.4 +use "../settings";
17.5 use_thy "termination";
17.6 use_thy "Induction";
17.7 use_thy "Nested1";
18.1 --- a/doc-src/TutorialI/Recdef/document/Nested1.tex Mon Sep 04 21:20:14 2000 +0200
18.2 +++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Tue Sep 05 09:03:17 2000 +0200
18.3 @@ -20,13 +20,11 @@
18.4 Remember that function \isa{size} is defined for each \isacommand{datatype}.
18.5 However, the definition does not succeed. Isabelle complains about an
18.6 unproved termination condition
18.7 -\begin{quote}
18.8 -
18.9 +%
18.10 \begin{isabelle}%
18.11 -t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}
18.12 +\ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}%
18.13 \end{isabelle}%
18.14
18.15 -\end{quote}
18.16 where \isa{set} returns the set of elements of a list (no special
18.17 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
18.18 (when \isa{term} was defined). First we have to understand why the
19.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex Mon Sep 04 21:20:14 2000 +0200
19.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Sep 05 09:03:17 2000 +0200
19.3 @@ -22,14 +22,12 @@
19.4 \begin{isamarkuptxt}%
19.5 \noindent
19.6 This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x} and the step case
19.7 -\begin{quote}
19.8 -
19.9 +%
19.10 \begin{isabelle}%
19.11 -{\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline
19.12 -trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts
19.13 +\ \ \ \ \ {\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline
19.14 +\ \ \ \ \ trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts%
19.15 \end{isabelle}%
19.16
19.17 -\end{quote}
19.18 both of which are solved by simplification:%
19.19 \end{isamarkuptxt}%
19.20 \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%
19.21 @@ -64,14 +62,12 @@
19.22 \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
19.23 \isacommand{recdef} has been supplied with the congruence theorem
19.24 \isa{map{\isacharunderscore}cong}:
19.25 -\begin{quote}
19.26 -
19.27 +%
19.28 \begin{isabelle}%
19.29 -{\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
19.30 -{\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys
19.31 +\ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
19.32 +\ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
19.33 \end{isabelle}%
19.34
19.35 -\end{quote}
19.36 Its second premise expresses (indirectly) that the second argument of
19.37 \isa{map} is only applied to elements of its third argument. Congruence
19.38 rules for other higher-order functions on lists would look very similar but
20.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex Mon Sep 04 21:20:14 2000 +0200
20.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Tue Sep 05 09:03:17 2000 +0200
20.3 @@ -16,13 +16,11 @@
20.4 \noindent
20.5 According to the measure function, the second argument should decrease with
20.6 each recursive call. The resulting termination condition
20.7 -\begin{quote}
20.8 -
20.9 +%
20.10 \begin{isabelle}%
20.11 -n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n
20.12 +\ \ \ \ \ n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
20.13 \end{isabelle}%
20.14
20.15 -\end{quote}
20.16 is provded automatically because it is already present as a lemma in the
20.17 arithmetic library. Thus the recursion equation becomes a simplification
20.18 rule. Of course the equation is nonterminating if we are allowed to unfold
20.19 @@ -31,29 +29,23 @@
20.20 something else which leads to the same problem: it splits \isa{if}s if the
20.21 condition simplifies to neither \isa{True} nor \isa{False}. For
20.22 example, simplification reduces
20.23 -\begin{quote}
20.24 -
20.25 +%
20.26 \begin{isabelle}%
20.27 -gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k
20.28 +\ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
20.29 \end{isabelle}%
20.30
20.31 -\end{quote}
20.32 in one step to
20.33 -\begin{quote}
20.34 -
20.35 +%
20.36 \begin{isabelle}%
20.37 -{\isacharparenleft}if\ n\ {\isacharequal}\ \isadigit{0}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k
20.38 +\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ \isadigit{0}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
20.39 \end{isabelle}%
20.40
20.41 -\end{quote}
20.42 where the condition cannot be reduced further, and splitting leads to
20.43 -\begin{quote}
20.44 -
20.45 +%
20.46 \begin{isabelle}%
20.47 -{\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}
20.48 +\ \ \ \ \ {\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}%
20.49 \end{isabelle}%
20.50
20.51 -\end{quote}
20.52 Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
20.53 an \isa{if}, it is unfolded again, which leads to an infinite chain of
20.54 simplification steps. Fortunately, this problem can be avoided in many
21.1 --- a/doc-src/TutorialI/Recdef/simplification.thy Mon Sep 04 21:20:14 2000 +0200
21.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy Tue Sep 05 09:03:17 2000 +0200
21.3 @@ -18,9 +18,7 @@
21.4 text{*\noindent
21.5 According to the measure function, the second argument should decrease with
21.6 each recursive call. The resulting termination condition
21.7 -\begin{quote}
21.8 @{term[display]"n ~= 0 ==> m mod n < n"}
21.9 -\end{quote}
21.10 is provded automatically because it is already present as a lemma in the
21.11 arithmetic library. Thus the recursion equation becomes a simplification
21.12 rule. Of course the equation is nonterminating if we are allowed to unfold
21.13 @@ -29,17 +27,11 @@
21.14 something else which leads to the same problem: it splits @{text"if"}s if the
21.15 condition simplifies to neither @{term"True"} nor @{term"False"}. For
21.16 example, simplification reduces
21.17 -\begin{quote}
21.18 @{term[display]"gcd(m,n) = k"}
21.19 -\end{quote}
21.20 in one step to
21.21 -\begin{quote}
21.22 @{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
21.23 -\end{quote}
21.24 where the condition cannot be reduced further, and splitting leads to
21.25 -\begin{quote}
21.26 @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
21.27 -\end{quote}
21.28 Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
21.29 an @{text"if"}, it is unfolded again, which leads to an infinite chain of
21.30 simplification steps. Fortunately, this problem can be avoided in many
22.1 --- a/doc-src/TutorialI/ToyList/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
22.2 +++ b/doc-src/TutorialI/ToyList/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
22.3 @@ -1,2 +1,3 @@
22.4 +use "../settings.ML";
22.5 use_thy "ToyList";
22.6
23.1 --- a/doc-src/TutorialI/Trie/ROOT.ML Mon Sep 04 21:20:14 2000 +0200
23.2 +++ b/doc-src/TutorialI/Trie/ROOT.ML Tue Sep 05 09:03:17 2000 +0200
23.3 @@ -1,2 +1,3 @@
23.4 +use "../settings.ML";
23.5 use_thy "Option2";
23.6 use_thy "Trie";
24.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
24.2 +++ b/doc-src/TutorialI/settings.ML Tue Sep 05 09:03:17 2000 +0200
24.3 @@ -0,0 +1,1 @@
24.4 +IsarOutput.indent := 5;