summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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 -that the authors are at least cavalier about this point and may even have -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 +Isabelle). The authors are at least cavalier about this point and may +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. -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. 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} \section{Advanced inductive definitions} +\label{sec:adv-ind-def} \input{Inductive/advanced-examples} \input{Inductive/document/AB}