author nipkow Fri, 16 Feb 2001 06:46:20 +0100 changeset 11147 d848c6693185 parent 11146 449e1a1bb7a8 child 11148 79aa2932b2d7
*** empty log message ***
--- a/doc-src/TutorialI/Inductive/AB.thy	Fri Feb 16 00:36:21 2001 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy	Fri Feb 16 06:46:20 2001 +0100
@@ -105,7 +105,7 @@
@{text"\<bar>.\<bar>"} is the absolute value function, and @{term"#1::int"} is the
integer 1 (see \S\ref{sec:numbers}).

-First we show that the our specific function, the difference between the
+First we show that our specific function, the difference between the
numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every
move to the right. At this point we also start generalizing from @{term a}'s
and @{term b}'s to an arbitrary property @{term P}. Otherwise we would have
@@ -119,7 +119,7 @@

txt{*\noindent
The lemma is a bit hard to read because of the coercion function
-@{term[source]"int :: nat \<Rightarrow> int"}. It is required because @{term size} returns
+@{text"int :: nat \<Rightarrow> int"}. It is required because @{term size} returns
a natural number, but subtraction on type~@{typ nat} will do the wrong thing.
Function @{term take} is predefined and @{term"take i xs"} is the prefix of
length @{term i} of @{term xs}; below we also need @{term"drop i xs"}, which
@@ -237,7 +237,7 @@
txt{*\noindent
This yields an index @{prop"i \<le> length v"} such that
@{prop[display]"length [x\<in>take i v . x = a] = length [x\<in>take i v . x = b] + 1"}
-With the help of @{thm[source]part1} it follows that
+With the help of @{thm[source]part2} it follows that
@{prop[display]"length [x\<in>drop i v . x = a] = length [x\<in>drop i v . x = b] + 1"}
*}

@@ -287,18 +287,20 @@
grammar, for no good reason, excludes the empty word.  That complicates
matters just a little bit because we now have 8 instead of our 7 productions.

-More importantly, the proof itself is different: rather than separating the
-two directions, they perform one induction on the length of a word. This
-deprives them of the beauty of rule induction and in the easy direction
-(correctness) their reasoning is more detailed than our @{text auto}. For the
-hard part (completeness), they consider just one of the cases that our @{text
-simp_all} disposes of automatically. Then they conclude the proof by saying
-about the remaining cases: We do this in a manner similar to our method of
-proof for part (1); this part is left to the reader''. But this is precisely
-the part that requires the intermediate value theorem and thus is not at all
-similar to the other cases (which are automatic in Isabelle). We conclude
-overlooked the slight difficulty lurking in the omitted cases. This is not
-atypical for pen-and-paper proofs, once analysed in detail.  *}
+More importantly, the proof itself is different: rather than
+separating the two directions, they perform one induction on the
+length of a word. This deprives them of the beauty of rule induction,
+and in the easy direction (correctness) their reasoning is more
+detailed than our @{text auto}. For the hard part (completeness), they
+consider just one of the cases that our @{text simp_all} disposes of
+automatically. Then they conclude the proof by saying about the
+remaining cases: We do this in a manner similar to our method of
+proof for part (1); this part is left to the reader''. But this is
+precisely the part that requires the intermediate value theorem and
+thus is not at all similar to the other cases (which are automatic in
+even have overlooked the slight difficulty lurking in the omitted
+cases. This is not atypical for pen-and-paper proofs, once analysed in
+detail.  *}

(*<*)end(*>*)
--- a/doc-src/TutorialI/Inductive/Star.thy	Fri Feb 16 00:36:21 2001 +0100
+++ b/doc-src/TutorialI/Inductive/Star.thy	Fri Feb 16 06:46:20 2001 +0100
@@ -8,7 +8,7 @@
Relations too can be defined inductively, since they are just sets of pairs.
A perfect example is the function that maps a relation to its
reflexive transitive closure.  This concept was already
-introduced in \S\ref{sec:Relations}, where the operator @{text"^*"} was
+introduced in \S\ref{sec:Relations}, where the operator @{text"\<^sup>*"} was
defined as a least fixed point because inductive definitions were not yet
available. But now they are:
*}
@@ -97,7 +97,7 @@
\end{quote}
A similar heuristic for other kinds of inductions is formulated in
\S\ref{sec:ind-var-in-prems}. The @{text rule_format} directive turns
-@{text"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}. Thus in the end we obtain the original
+@{text"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}: in the end we obtain the original
statement of our lemma.
*}

@@ -148,8 +148,7 @@
contains only two rules, and the single step rule is simpler than
transitivity.  As a consequence, @{thm[source]rtc.induct} is simpler than
@{thm[source]rtc2.induct}. Since inductive proofs are hard enough
-anyway, we should
-certainly pick the simplest induction schema available.
+anyway, we should always pick the simplest induction schema available.
Hence @{term rtc} is the definition of choice.

\begin{exercise}\label{ex:converse-rtc-step}
--- a/doc-src/TutorialI/Inductive/advanced-examples.tex	Fri Feb 16 00:36:21 2001 +0100
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex	Fri Feb 16 06:46:20 2001 +0100
@@ -65,7 +65,7 @@
enlarging the set of function symbols enlarges the set of ground
terms. The proof is a trivial rule induction.
First we use the \isa{clarify} method to assume the existence of an element of
-\isa{terms~F}.  (We could have used \isa{intro subsetI}.)  We then
+\isa{gterms~F}.  (We could have used \isa{intro subsetI}.)  We then
apply rule induction. Here is the resulting subgoal:
\begin{isabelle}
\ 1.\ \isasymAnd x\ args\ f.\isanewline
@@ -96,14 +96,14 @@
Recall that \isa{even} is the minimal set closed under these two rules:
\begin{isabelle}
0\ \isasymin \ even\isanewline
-n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin
+n\ \isasymin \ even\ \isasymLongrightarrow \ Suc\ (Suc\ n)\ \isasymin
\ even
\end{isabelle}
Minimality means that \isa{even} contains only the elements that these
rules force it to contain.  If we are told that \isa{a}
belongs to
\isa{even} then there are only two possibilities.  Either \isa{a} is \isa{0}
-or else \isa{a} has the form \isa{Suc(Suc~n)}, for an arbitrary \isa{n}
+or else \isa{a} has the form \isa{Suc(Suc~n)}, for some suitable \isa{n}
that belongs to
\isa{even}.  That is the gist of the \isa{cases} rule, which Isabelle proves
for us when it accepts an inductive definition:
--- a/doc-src/TutorialI/Inductive/document/AB.tex	Fri Feb 16 00:36:21 2001 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Fri Feb 16 06:46:20 2001 +0100
@@ -101,7 +101,7 @@
\isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
integer 1 (see \S\ref{sec:numbers}).

-First we show that the our specific function, the difference between the
+First we show that our specific function, the difference between the
numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
move to the right. At this point we also start generalizing from \isa{a}'s
and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
@@ -114,7 +114,7 @@
\begin{isamarkuptxt}%
\noindent
The lemma is a bit hard to read because of the coercion function
-\isa{{\isachardoublequote}int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
+\isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns
a natural number, but subtraction on type~\isa{nat} will do the wrong thing.
Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
length \isa{i} of \isa{xs}; below we also need \isa{drop\ i\ xs}, which
@@ -222,7 +222,7 @@
\begin{isabelle}%
\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}%
\end{isabelle}
-With the help of \isa{part{\isadigit{1}}} it follows that
+With the help of \isa{part{\isadigit{2}}} it follows that
\begin{isabelle}%
\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}%
\end{isabelle}%
--- a/doc-src/TutorialI/Inductive/document/Star.tex	Fri Feb 16 00:36:21 2001 +0100
+++ b/doc-src/TutorialI/Inductive/document/Star.tex	Fri Feb 16 06:46:20 2001 +0100
@@ -12,7 +12,7 @@
Relations too can be defined inductively, since they are just sets of pairs.
A perfect example is the function that maps a relation to its
reflexive transitive closure.  This concept was already
-introduced in \S\ref{sec:Relations}, where the operator \isa{{\isacharcircum}{\isacharasterisk}} was
+introduced in \S\ref{sec:Relations}, where the operator \isa{\isactrlsup {\isacharasterisk}} was
defined as a least fixed point because inductive definitions were not yet
available. But now they are:%
\end{isamarkuptext}%
@@ -102,7 +102,7 @@
\end{quote}
A similar heuristic for other kinds of inductions is formulated in
\S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns
-\isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}. Thus in the end we obtain the original
+\isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}: in the end we obtain the original
statement of our lemma.%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%
@@ -152,8 +152,7 @@
contains only two rules, and the single step rule is simpler than
transitivity.  As a consequence, \isa{rtc{\isachardot}induct} is simpler than
\isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough
-anyway, we should
-certainly pick the simplest induction schema available.
+anyway, we should always pick the simplest induction schema available.
Hence \isa{rtc} is the definition of choice.

\begin{exercise}\label{ex:converse-rtc-step}
--- a/doc-src/TutorialI/Inductive/inductive.tex	Fri Feb 16 00:36:21 2001 +0100
+++ b/doc-src/TutorialI/Inductive/inductive.tex	Fri Feb 16 06:46:20 2001 +0100
@@ -5,19 +5,21 @@
This chapter is dedicated to the most important definition principle after
recursive functions and datatypes: inductively defined sets.

-A slightly more complicated example, the
-reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular,
-some standard induction heuristics are discussed. To demonstrate the
-versatility of inductive definitions, {\S}\ref{sec:CFG} presents a case study
-from the realm of context-free grammars. The chapter closes with a discussion
-of advanced forms of inductive definitions.
+We start with a simple example: the set of even numbers.  A slightly more
+complicated example, the reflexive transitive closure, is the subject of
+{\S}\ref{sec:rtc}. In particular, some standard induction heuristics are
+discussed. Advanced forms of inductive definitions are discussed in
+{\S}\ref{sec:adv-ind-def}. To demonstrate the versatility of inductive
+definitions, the chapter closes with a case study from the realm of
+context-free grammars. The first two sections are required reading for anybody
+interested in mathematical modelling.

\input{Inductive/even-example}
\input{Inductive/document/Mutual}
\input{Inductive/document/Star}

\input{Inductive/document/AB}