1.1 --- a/doc-src/TutorialI/Inductive/AB.thy Fri Feb 16 00:36:21 2001 +0100
1.2 +++ b/doc-src/TutorialI/Inductive/AB.thy Fri Feb 16 06:46:20 2001 +0100
1.3 @@ -105,7 +105,7 @@
1.4 @{text"\<bar>.\<bar>"} is the absolute value function, and @{term"#1::int"} is the
1.5 integer 1 (see \S\ref{sec:numbers}).
1.6
1.7 -First we show that the our specific function, the difference between the
1.8 +First we show that our specific function, the difference between the
1.9 numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every
1.10 move to the right. At this point we also start generalizing from @{term a}'s
1.11 and @{term b}'s to an arbitrary property @{term P}. Otherwise we would have
1.12 @@ -119,7 +119,7 @@
1.13
1.14 txt{*\noindent
1.15 The lemma is a bit hard to read because of the coercion function
1.16 -@{term[source]"int :: nat \<Rightarrow> int"}. It is required because @{term size} returns
1.17 +@{text"int :: nat \<Rightarrow> int"}. It is required because @{term size} returns
1.18 a natural number, but subtraction on type~@{typ nat} will do the wrong thing.
1.19 Function @{term take} is predefined and @{term"take i xs"} is the prefix of
1.20 length @{term i} of @{term xs}; below we also need @{term"drop i xs"}, which
1.21 @@ -237,7 +237,7 @@
1.22 txt{*\noindent
1.23 This yields an index @{prop"i \<le> length v"} such that
1.24 @{prop[display]"length [x\<in>take i v . x = a] = length [x\<in>take i v . x = b] + 1"}
1.25 -With the help of @{thm[source]part1} it follows that
1.26 +With the help of @{thm[source]part2} it follows that
1.27 @{prop[display]"length [x\<in>drop i v . x = a] = length [x\<in>drop i v . x = b] + 1"}
1.28 *}
1.29
1.30 @@ -287,18 +287,20 @@
1.31 grammar, for no good reason, excludes the empty word. That complicates
1.32 matters just a little bit because we now have 8 instead of our 7 productions.
1.33
1.34 -More importantly, the proof itself is different: rather than separating the
1.35 -two directions, they perform one induction on the length of a word. This
1.36 -deprives them of the beauty of rule induction and in the easy direction
1.37 -(correctness) their reasoning is more detailed than our @{text auto}. For the
1.38 -hard part (completeness), they consider just one of the cases that our @{text
1.39 -simp_all} disposes of automatically. Then they conclude the proof by saying
1.40 -about the remaining cases: ``We do this in a manner similar to our method of
1.41 -proof for part (1); this part is left to the reader''. But this is precisely
1.42 -the part that requires the intermediate value theorem and thus is not at all
1.43 -similar to the other cases (which are automatic in Isabelle). We conclude
1.44 -that the authors are at least cavalier about this point and may even have
1.45 -overlooked the slight difficulty lurking in the omitted cases. This is not
1.46 -atypical for pen-and-paper proofs, once analysed in detail. *}
1.47 +More importantly, the proof itself is different: rather than
1.48 +separating the two directions, they perform one induction on the
1.49 +length of a word. This deprives them of the beauty of rule induction,
1.50 +and in the easy direction (correctness) their reasoning is more
1.51 +detailed than our @{text auto}. For the hard part (completeness), they
1.52 +consider just one of the cases that our @{text simp_all} disposes of
1.53 +automatically. Then they conclude the proof by saying about the
1.54 +remaining cases: ``We do this in a manner similar to our method of
1.55 +proof for part (1); this part is left to the reader''. But this is
1.56 +precisely the part that requires the intermediate value theorem and
1.57 +thus is not at all similar to the other cases (which are automatic in
1.58 +Isabelle). The authors are at least cavalier about this point and may
1.59 +even have overlooked the slight difficulty lurking in the omitted
1.60 +cases. This is not atypical for pen-and-paper proofs, once analysed in
1.61 +detail. *}
1.62
1.63 (*<*)end(*>*)
2.1 --- a/doc-src/TutorialI/Inductive/Star.thy Fri Feb 16 00:36:21 2001 +0100
2.2 +++ b/doc-src/TutorialI/Inductive/Star.thy Fri Feb 16 06:46:20 2001 +0100
2.3 @@ -8,7 +8,7 @@
2.4 Relations too can be defined inductively, since they are just sets of pairs.
2.5 A perfect example is the function that maps a relation to its
2.6 reflexive transitive closure. This concept was already
2.7 -introduced in \S\ref{sec:Relations}, where the operator @{text"^*"} was
2.8 +introduced in \S\ref{sec:Relations}, where the operator @{text"\<^sup>*"} was
2.9 defined as a least fixed point because inductive definitions were not yet
2.10 available. But now they are:
2.11 *}
2.12 @@ -97,7 +97,7 @@
2.13 \end{quote}
2.14 A similar heuristic for other kinds of inductions is formulated in
2.15 \S\ref{sec:ind-var-in-prems}. The @{text rule_format} directive turns
2.16 -@{text"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}. Thus in the end we obtain the original
2.17 +@{text"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}: in the end we obtain the original
2.18 statement of our lemma.
2.19 *}
2.20
2.21 @@ -148,8 +148,7 @@
2.22 contains only two rules, and the single step rule is simpler than
2.23 transitivity. As a consequence, @{thm[source]rtc.induct} is simpler than
2.24 @{thm[source]rtc2.induct}. Since inductive proofs are hard enough
2.25 -anyway, we should
2.26 -certainly pick the simplest induction schema available.
2.27 +anyway, we should always pick the simplest induction schema available.
2.28 Hence @{term rtc} is the definition of choice.
2.29
2.30 \begin{exercise}\label{ex:converse-rtc-step}
3.1 --- a/doc-src/TutorialI/Inductive/advanced-examples.tex Fri Feb 16 00:36:21 2001 +0100
3.2 +++ b/doc-src/TutorialI/Inductive/advanced-examples.tex Fri Feb 16 06:46:20 2001 +0100
3.3 @@ -65,7 +65,7 @@
3.4 enlarging the set of function symbols enlarges the set of ground
3.5 terms. The proof is a trivial rule induction.
3.6 First we use the \isa{clarify} method to assume the existence of an element of
3.7 -\isa{terms~F}. (We could have used \isa{intro subsetI}.) We then
3.8 +\isa{gterms~F}. (We could have used \isa{intro subsetI}.) We then
3.9 apply rule induction. Here is the resulting subgoal:
3.10 \begin{isabelle}
3.11 \ 1.\ \isasymAnd x\ args\ f.\isanewline
3.12 @@ -96,14 +96,14 @@
3.13 Recall that \isa{even} is the minimal set closed under these two rules:
3.14 \begin{isabelle}
3.15 0\ \isasymin \ even\isanewline
3.16 -n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin
3.17 +n\ \isasymin \ even\ \isasymLongrightarrow \ Suc\ (Suc\ n)\ \isasymin
3.18 \ even
3.19 \end{isabelle}
3.20 Minimality means that \isa{even} contains only the elements that these
3.21 rules force it to contain. If we are told that \isa{a}
3.22 belongs to
3.23 \isa{even} then there are only two possibilities. Either \isa{a} is \isa{0}
3.24 -or else \isa{a} has the form \isa{Suc(Suc~n)}, for an arbitrary \isa{n}
3.25 +or else \isa{a} has the form \isa{Suc(Suc~n)}, for some suitable \isa{n}
3.26 that belongs to
3.27 \isa{even}. That is the gist of the \isa{cases} rule, which Isabelle proves
3.28 for us when it accepts an inductive definition:
4.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex Fri Feb 16 00:36:21 2001 +0100
4.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Fri Feb 16 06:46:20 2001 +0100
4.3 @@ -101,7 +101,7 @@
4.4 \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
4.5 integer 1 (see \S\ref{sec:numbers}).
4.6
4.7 -First we show that the our specific function, the difference between the
4.8 +First we show that our specific function, the difference between the
4.9 numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
4.10 move to the right. At this point we also start generalizing from \isa{a}'s
4.11 and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
4.12 @@ -114,7 +114,7 @@
4.13 \begin{isamarkuptxt}%
4.14 \noindent
4.15 The lemma is a bit hard to read because of the coercion function
4.16 -\isa{{\isachardoublequote}int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
4.17 +\isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns
4.18 a natural number, but subtraction on type~\isa{nat} will do the wrong thing.
4.19 Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
4.20 length \isa{i} of \isa{xs}; below we also need \isa{drop\ i\ xs}, which
4.21 @@ -222,7 +222,7 @@
4.22 \begin{isabelle}%
4.23 \ \ \ \ \ 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}}%
4.24 \end{isabelle}
4.25 -With the help of \isa{part{\isadigit{1}}} it follows that
4.26 +With the help of \isa{part{\isadigit{2}}} it follows that
4.27 \begin{isabelle}%
4.28 \ \ \ \ \ 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}}%
4.29 \end{isabelle}%
5.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex Fri Feb 16 00:36:21 2001 +0100
5.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Fri Feb 16 06:46:20 2001 +0100
5.3 @@ -12,7 +12,7 @@
5.4 Relations too can be defined inductively, since they are just sets of pairs.
5.5 A perfect example is the function that maps a relation to its
5.6 reflexive transitive closure. This concept was already
5.7 -introduced in \S\ref{sec:Relations}, where the operator \isa{{\isacharcircum}{\isacharasterisk}} was
5.8 +introduced in \S\ref{sec:Relations}, where the operator \isa{\isactrlsup {\isacharasterisk}} was
5.9 defined as a least fixed point because inductive definitions were not yet
5.10 available. But now they are:%
5.11 \end{isamarkuptext}%
5.12 @@ -102,7 +102,7 @@
5.13 \end{quote}
5.14 A similar heuristic for other kinds of inductions is formulated in
5.15 \S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns
5.16 -\isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}. Thus in the end we obtain the original
5.17 +\isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}: in the end we obtain the original
5.18 statement of our lemma.%
5.19 \end{isamarkuptxt}%
5.20 \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%
5.21 @@ -152,8 +152,7 @@
5.22 contains only two rules, and the single step rule is simpler than
5.23 transitivity. As a consequence, \isa{rtc{\isachardot}induct} is simpler than
5.24 \isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough
5.25 -anyway, we should
5.26 -certainly pick the simplest induction schema available.
5.27 +anyway, we should always pick the simplest induction schema available.
5.28 Hence \isa{rtc} is the definition of choice.
5.29
5.30 \begin{exercise}\label{ex:converse-rtc-step}
6.1 --- a/doc-src/TutorialI/Inductive/inductive.tex Fri Feb 16 00:36:21 2001 +0100
6.2 +++ b/doc-src/TutorialI/Inductive/inductive.tex Fri Feb 16 06:46:20 2001 +0100
6.3 @@ -5,19 +5,21 @@
6.4 This chapter is dedicated to the most important definition principle after
6.5 recursive functions and datatypes: inductively defined sets.
6.6
6.7 -We start with a simple example: the set of even numbers.
6.8 -A slightly more complicated example, the
6.9 -reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular,
6.10 -some standard induction heuristics are discussed. To demonstrate the
6.11 -versatility of inductive definitions, {\S}\ref{sec:CFG} presents a case study
6.12 -from the realm of context-free grammars. The chapter closes with a discussion
6.13 -of advanced forms of inductive definitions.
6.14 +We start with a simple example: the set of even numbers. A slightly more
6.15 +complicated example, the reflexive transitive closure, is the subject of
6.16 +{\S}\ref{sec:rtc}. In particular, some standard induction heuristics are
6.17 +discussed. Advanced forms of inductive definitions are discussed in
6.18 +{\S}\ref{sec:adv-ind-def}. To demonstrate the versatility of inductive
6.19 +definitions, the chapter closes with a case study from the realm of
6.20 +context-free grammars. The first two sections are required reading for anybody
6.21 +interested in mathematical modelling.
6.22
6.23 \input{Inductive/even-example}
6.24 \input{Inductive/document/Mutual}
6.25 \input{Inductive/document/Star}
6.26
6.27 \section{Advanced inductive definitions}
6.28 +\label{sec:adv-ind-def}
6.29 \input{Inductive/advanced-examples}
6.30
6.31 \input{Inductive/document/AB}