*** empty log message ***
authornipkow
Wed Oct 18 17:19:18 2000 +0200 (2000-10-18)
changeset 10242028f54cd2cc9
parent 10241 e0428c2778f1
child 10243 f11d37d4472d
*** empty log message ***
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/PDL.thy
doc-src/TutorialI/CTL/document/CTL.tex
doc-src/TutorialI/CTL/document/PDL.tex
doc-src/TutorialI/Inductive/AB.thy
doc-src/TutorialI/Inductive/Star.thy
doc-src/TutorialI/Inductive/document/AB.tex
doc-src/TutorialI/Inductive/document/Star.tex
doc-src/TutorialI/Inductive/inductive.tex
doc-src/TutorialI/Misc/AdvancedInd.thy
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/Recdef/Nested1.thy
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/todo.tobias
     1.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Wed Oct 18 12:30:59 2000 +0200
     1.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Wed Oct 18 17:19:18 2000 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4  
     1.5  text{*\noindent
     1.6  Because @{term af} is monotone in its second argument (and also its first, but
     1.7 -that is irrelevant) @{term"af A"} has a least fixpoint:
     1.8 +that is irrelevant) @{term"af A"} has a least fixed point:
     1.9  *};
    1.10  
    1.11  lemma mono_af: "mono(af A)";
    1.12 @@ -108,7 +108,7 @@
    1.13  
    1.14  txt{*\noindent
    1.15  In contrast to the analogous property for @{term EF}, and just
    1.16 -for a change, we do not use fixpoint induction but a weaker theorem,
    1.17 +for a change, we do not use fixed point induction but a weaker theorem,
    1.18  @{thm[source]lfp_lowerbound}:
    1.19  @{thm[display]lfp_lowerbound[of _ "S",no_vars]}
    1.20  The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
    1.21 @@ -403,7 +403,7 @@
    1.22  set operations are easily implemented. Only @{term lfp} requires a little thought.
    1.23  Fortunately the HOL library proves that in the case of finite sets and a monotone @{term F},
    1.24  @{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until
    1.25 -a fixpoint is reached. It is actually possible to generate executable functional programs
    1.26 +a fixed point is reached. It is actually possible to generate executable functional programs
    1.27  from HOL definitions, but that is beyond the scope of the tutorial.
    1.28  *}
    1.29  (*<*)end(*>*)
     2.1 --- a/doc-src/TutorialI/CTL/PDL.thy	Wed Oct 18 12:30:59 2000 +0200
     2.2 +++ b/doc-src/TutorialI/CTL/PDL.thy	Wed Oct 18 17:19:18 2000 +0200
     2.3 @@ -65,7 +65,7 @@
     2.4  postfix @{text"^-1"} and the infix @{text"^^"} are predefined and denote the
     2.5  converse of a relation and the application of a relation to a set. Thus
     2.6  @{term "M^-1 ^^ T"} is the set of all predecessors of @{term T} and the least
     2.7 -fixpoint (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M^-1 ^^ T"} is the least set
     2.8 +fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M^-1 ^^ T"} is the least set
     2.9  @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
    2.10  find it hard to see that @{term"mc(EF f)"} contains exactly those states from
    2.11  which there is a path to a state where @{term f} is true, do not worry---that
    2.12 @@ -80,7 +80,7 @@
    2.13  done
    2.14  
    2.15  text{*\noindent
    2.16 -in order to make sure it really has a least fixpoint.
    2.17 +in order to make sure it really has a least fixed point.
    2.18  
    2.19  Now we can relate model checking and semantics. For the @{text EF} case we need
    2.20  a separate lemma:
     3.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Wed Oct 18 12:30:59 2000 +0200
     3.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Wed Oct 18 17:19:18 2000 +0200
     3.3 @@ -44,7 +44,7 @@
     3.4  \begin{isamarkuptext}%
     3.5  \noindent
     3.6  Because \isa{af} is monotone in its second argument (and also its first, but
     3.7 -that is irrelevant) \isa{af\ A} has a least fixpoint:%
     3.8 +that is irrelevant) \isa{af\ A} has a least fixed point:%
     3.9  \end{isamarkuptext}%
    3.10  \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
    3.11  \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
    3.12 @@ -60,7 +60,7 @@
    3.13  \begin{isamarkuptxt}%
    3.14  \noindent
    3.15  In contrast to the analogous property for \isa{EF}, and just
    3.16 -for a change, we do not use fixpoint induction but a weaker theorem,
    3.17 +for a change, we do not use fixed point induction but a weaker theorem,
    3.18  \isa{lfp{\isacharunderscore}lowerbound}:
    3.19  \begin{isabelle}%
    3.20  \ \ \ \ \ f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S%
    3.21 @@ -310,7 +310,7 @@
    3.22  set operations are easily implemented. Only \isa{lfp} requires a little thought.
    3.23  Fortunately the HOL library proves that in the case of finite sets and a monotone \isa{F},
    3.24  \isa{lfp\ F} can be computed by iterated application of \isa{F} to \isa{{\isacharbraceleft}{\isacharbraceright}} until
    3.25 -a fixpoint is reached. It is actually possible to generate executable functional programs
    3.26 +a fixed point is reached. It is actually possible to generate executable functional programs
    3.27  from HOL definitions, but that is beyond the scope of the tutorial.%
    3.28  \end{isamarkuptext}%
    3.29  \end{isabellebody}%
     4.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Wed Oct 18 12:30:59 2000 +0200
     4.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Wed Oct 18 17:19:18 2000 +0200
     4.3 @@ -64,7 +64,7 @@
     4.4  postfix \isa{{\isacharcircum}{\isacharminus}{\isadigit{1}}} and the infix \isa{{\isacharcircum}{\isacharcircum}} are predefined and denote the
     4.5  converse of a relation and the application of a relation to a set. Thus
     4.6  \isa{M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the set of all predecessors of \isa{T} and the least
     4.7 -fixpoint (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the least set
     4.8 +fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the least set
     4.9  \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
    4.10  find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from
    4.11  which there is a path to a state where \isa{f} is true, do not worry---that
    4.12 @@ -78,7 +78,7 @@
    4.13  \isacommand{done}%
    4.14  \begin{isamarkuptext}%
    4.15  \noindent
    4.16 -in order to make sure it really has a least fixpoint.
    4.17 +in order to make sure it really has a least fixed point.
    4.18  
    4.19  Now we can relate model checking and semantics. For the \isa{EF} case we need
    4.20  a separate lemma:%
     5.1 --- a/doc-src/TutorialI/Inductive/AB.thy	Wed Oct 18 12:30:59 2000 +0200
     5.2 +++ b/doc-src/TutorialI/Inductive/AB.thy	Wed Oct 18 17:19:18 2000 +0200
     5.3 @@ -1,8 +1,8 @@
     5.4  (*<*)theory AB = Main:(*>*)
     5.5  
     5.6 -section{*A context free grammar*}
     5.7 +section{*Case study: A context free grammar*}
     5.8  
     5.9 -text{*
    5.10 +text{*\label{sec:CFG}
    5.11  Grammars are nothing but shorthands for inductive definitions of nonterminals
    5.12  which represent sets of strings. For example, the production
    5.13  $A \to B c$ is short for
    5.14 @@ -43,7 +43,8 @@
    5.15  
    5.16  text{*\noindent
    5.17  The above productions are recast as a \emph{simultaneous} inductive
    5.18 -definition of @{term S}, @{term A} and @{term B}:
    5.19 +definition\index{inductive definition!simultaneous}
    5.20 +of @{term S}, @{term A} and @{term B}:
    5.21  *}
    5.22  
    5.23  inductive S A B
     6.1 --- a/doc-src/TutorialI/Inductive/Star.thy	Wed Oct 18 12:30:59 2000 +0200
     6.2 +++ b/doc-src/TutorialI/Inductive/Star.thy	Wed Oct 18 17:19:18 2000 +0200
     6.3 @@ -2,37 +2,120 @@
     6.4  
     6.5  section{*The reflexive transitive closure*}
     6.6  
     6.7 -text{*
     6.8 +text{*\label{sec:rtc}
     6.9 +{\bf Say something about inductive relations as opposed to sets? Or has that
    6.10 +been said already? If not, explain induction!}
    6.11 +
    6.12  A perfect example of an inductive definition is the reflexive transitive
    6.13  closure of a relation. This concept was already introduced in
    6.14  \S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
    6.15  the operator @{text"^*"} is not defined inductively but via a least
    6.16 -fixpoint because at that point in the theory hierarchy
    6.17 +fixed point because at that point in the theory hierarchy
    6.18  inductive definitions are not yet available. But now they are:
    6.19  *}
    6.20  
    6.21 -consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"  ("_*" [1000] 999)
    6.22 +consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
    6.23  inductive "r*"
    6.24  intros
    6.25 -rtc_refl[intro!]:                        "(x,x) \<in> r*"
    6.26 -rtc_step: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
    6.27 +rtc_refl[iff]:  "(x,x) \<in> r*"
    6.28 +rtc_step:       "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
    6.29 +
    6.30 +text{*\noindent
    6.31 +The function @{term rtc} is annotated with concrete syntax: instead of
    6.32 +@{text"rtc r"} we can read and write {term"r*"}. The actual definition
    6.33 +consists of two rules. Reflexivity is obvious and is immediately declared an
    6.34 +equivalence rule.  Thus the automatic tools will apply it automatically. The
    6.35 +second rule, @{thm[source]rtc_step}, says that we can always add one more
    6.36 +@{term r}-step to the left. Although we could make @{thm[source]rtc_step} an
    6.37 +introduction rule, this is dangerous: the recursion slows down and may
    6.38 +even kill the automatic tactics.
    6.39 +
    6.40 +The above definition of the concept of reflexive transitive closure may
    6.41 +be sufficiently intuitive but it is certainly not the only possible one:
    6.42 +for a start, it does not even mention transitivity explicitly.
    6.43 +The rest of this section is devoted to proving that it is equivalent to
    6.44 +the ``standard'' definition. We start with a simple lemma:
    6.45 +*}
    6.46  
    6.47  lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
    6.48  by(blast intro: rtc_step);
    6.49  
    6.50 -lemma step2[rule_format]:
    6.51 -  "(y,z) \<in> r*  \<Longrightarrow> (x,y) \<in> r \<longrightarrow> (x,z) \<in> r*"
    6.52 -apply(erule rtc.induct)
    6.53 +text{*\noindent
    6.54 +Although the lemma itself is an unremarkable consequence of the basic rules,
    6.55 +it has the advantage that it can be declared an introduction rule without the
    6.56 +danger of killing the automatic tactics because @{term"r*"} occurs only in
    6.57 +the conclusion and not in the premise. Thus some proofs that would otherwise
    6.58 +need @{thm[source]rtc_step} can now be found automatically. The proof also
    6.59 +shows that @{term blast} is quite able to handle @{thm[source]rtc_step}. But
    6.60 +some of the other automatic tactics are more sensitive, and even @{text
    6.61 +blast} can be lead astray in the presence of large numbers of rules.
    6.62 +
    6.63 +Let us now turn to transitivity. It should be a consequence of the definition.
    6.64 +*}
    6.65 +
    6.66 +lemma rtc_trans:
    6.67 +  "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
    6.68 +
    6.69 +txt{*\noindent
    6.70 +The proof starts canonically by rule induction:
    6.71 +*}
    6.72 +
    6.73 +apply(erule rtc.induct)(*pr(latex xsymbols symbols);*)(*<*)oops(*>*)
    6.74 +text{*\noindent
    6.75 +However, even the resulting base case is a problem
    6.76 +\begin{isabelle}
    6.77 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}
    6.78 +\end{isabelle}
    6.79 +and maybe not what you had expected. We have to abandon this proof attempt.
    6.80 +To understand what is going on,
    6.81 +let us look at the induction rule @{thm[source]rtc.induct}:
    6.82 +\[ \frac{(x,y) \in r^* \qquad \bigwedge x.~P~x~x \quad \dots}{P~x~y} \]
    6.83 +When applying this rule, $x$ becomes @{term x}, $y$ becomes
    6.84 +@{term y} and $P~x~y$ becomes @{prop"(x,z) : r*"}, thus
    6.85 +yielding the above subgoal. So what went wrong?
    6.86 +
    6.87 +When looking at the instantiation of $P~x~y$ we see
    6.88 +that $P$ does not depend on its second parameter at
    6.89 +all. The reason is that in our original goal, of the pair @{term"(x,y)"} only
    6.90 +@{term x} appears also in the conclusion, but not @{term y}. Thus our
    6.91 +induction statement is too weak. Fortunately, it can easily be strengthened:
    6.92 +transfer the additional premise @{prop"(y,z):r*"} into the conclusion:
    6.93 +*}
    6.94 +
    6.95 +lemma rtc_trans[rule_format]:
    6.96 +  "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
    6.97 +
    6.98 +txt{*\noindent
    6.99 +This is not an obscure trick but a generally applicable heuristic:
   6.100 +\begin{quote}\em
   6.101 +Whe proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
   6.102 +pull all other premises containing any of the $x@i$ into the conclusion
   6.103 +using $\longrightarrow$.
   6.104 +\end{quote}
   6.105 +A similar heuristic for other kinds of inductions is formulated in
   6.106 +\S\ref{sec:ind-var-in-prems}. The @{text rule_format} directive turns
   6.107 +@{text"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}. Thus in the end we obtain the original
   6.108 +statement of our lemma.
   6.109 +
   6.110 +Now induction produces two subgoals which are both proved automatically:
   6.111 +\begin{isabelle}
   6.112 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline
   6.113 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline
   6.114 +\ \ \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isasymrbrakk}\isanewline
   6.115 +\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}
   6.116 +\end{isabelle}
   6.117 +*}
   6.118 +
   6.119 +apply(erule rtc.induct)(*pr(latex xsymbols symbols);*)
   6.120   apply(blast);
   6.121  apply(blast intro: rtc_step);
   6.122  done
   6.123  
   6.124 -lemma rtc_trans[rule_format]:
   6.125 -  "(x,y) \<in> r*  \<Longrightarrow> \<forall>z. (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
   6.126 -apply(erule rtc.induct)
   6.127 - apply blast;
   6.128 -apply(blast intro: step2);
   6.129 -done
   6.130 +text{*
   6.131 +Let us now prove that @{term"r*"} is really the reflexive transitive closure
   6.132 +of @{term r}, i.e.\ the least reflexive and transitive
   6.133 +relation containing @{term r}. The latter is easily formalized
   6.134 +*}
   6.135  
   6.136  consts rtc2 :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"
   6.137  inductive "rtc2 r"
   6.138 @@ -41,8 +124,8 @@
   6.139  "(x,x) \<in> rtc2 r"
   6.140  "\<lbrakk> (x,y) \<in> rtc2 r; (y,z) \<in> rtc2 r \<rbrakk> \<Longrightarrow> (x,z) \<in> rtc2 r"
   6.141  
   6.142 -text{*
   6.143 -The equivalence of the two definitions is easily shown by the obvious rule
   6.144 +text{*\noindent
   6.145 +and the equivalence of the two definitions is easily shown by the obvious rule
   6.146  inductions:
   6.147  *}
   6.148  
   6.149 @@ -59,4 +142,25 @@
   6.150  apply(blast intro: rtc2.intros);
   6.151  done
   6.152  
   6.153 -(*<*)end(*>*)
   6.154 +text{*
   6.155 +So why did we start with the first definition? Because it is simpler. It
   6.156 +contains only two rules, and the single step rule is simpler than
   6.157 +transitivity.  As a consequence, @{thm[source]rtc.induct} is simpler than
   6.158 +@{thm[source]rtc2.induct}. Since inductive proofs are hard enough, we should
   6.159 +certainly pick the simplest induction schema available for any concept.
   6.160 +Hence @{term rtc} is the definition of choice.
   6.161 +
   6.162 +\begin{exercise}
   6.163 +Show that the converse of @{thm[source]rtc_step} also holds:
   6.164 +@{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
   6.165 +\end{exercise}
   6.166 +*}
   6.167 +(*<*)
   6.168 +lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*"
   6.169 +apply(erule rtc.induct);
   6.170 + apply blast;
   6.171 +apply(blast intro:rtc_step)
   6.172 +done
   6.173 +
   6.174 +end
   6.175 +(*>*)
     7.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Wed Oct 18 12:30:59 2000 +0200
     7.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Wed Oct 18 17:19:18 2000 +0200
     7.3 @@ -2,9 +2,10 @@
     7.4  \begin{isabellebody}%
     7.5  \def\isabellecontext{AB}%
     7.6  %
     7.7 -\isamarkupsection{A context free grammar}
     7.8 +\isamarkupsection{Case study: A context free grammar}
     7.9  %
    7.10  \begin{isamarkuptext}%
    7.11 +\label{sec:CFG}
    7.12  Grammars are nothing but shorthands for inductive definitions of nonterminals
    7.13  which represent sets of strings. For example, the production
    7.14  $A \to B c$ is short for
    7.15 @@ -42,7 +43,8 @@
    7.16  \begin{isamarkuptext}%
    7.17  \noindent
    7.18  The above productions are recast as a \emph{simultaneous} inductive
    7.19 -definition of \isa{S}, \isa{A} and \isa{B}:%
    7.20 +definition\index{inductive definition!simultaneous}
    7.21 +of \isa{S}, \isa{A} and \isa{B}:%
    7.22  \end{isamarkuptext}%
    7.23  \isacommand{inductive}\ S\ A\ B\isanewline
    7.24  \isakeyword{intros}\isanewline
     8.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex	Wed Oct 18 12:30:59 2000 +0200
     8.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex	Wed Oct 18 17:19:18 2000 +0200
     8.3 @@ -5,36 +5,113 @@
     8.4  \isamarkupsection{The reflexive transitive closure}
     8.5  %
     8.6  \begin{isamarkuptext}%
     8.7 +\label{sec:rtc}
     8.8 +{\bf Say something about inductive relations as opposed to sets? Or has that
     8.9 +been said already? If not, explain induction!}
    8.10 +
    8.11  A perfect example of an inductive definition is the reflexive transitive
    8.12  closure of a relation. This concept was already introduced in
    8.13  \S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
    8.14  the operator \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least
    8.15 -fixpoint because at that point in the theory hierarchy
    8.16 +fixed point because at that point in the theory hierarchy
    8.17  inductive definitions are not yet available. But now they are:%
    8.18  \end{isamarkuptext}%
    8.19 -\isacommand{consts}\ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\ \ {\isacharparenleft}{\isachardoublequote}{\isacharunderscore}{\isacharasterisk}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
    8.20 +\isacommand{consts}\ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharunderscore}{\isacharasterisk}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
    8.21  \isacommand{inductive}\ {\isachardoublequote}r{\isacharasterisk}{\isachardoublequote}\isanewline
    8.22  \isakeyword{intros}\isanewline
    8.23 -rtc{\isacharunderscore}refl{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
    8.24 -rtc{\isacharunderscore}step{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
    8.25 -\isanewline
    8.26 +rtc{\isacharunderscore}refl{\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
    8.27 +rtc{\isacharunderscore}step{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}%
    8.28 +\begin{isamarkuptext}%
    8.29 +\noindent
    8.30 +The function \isa{rtc} is annotated with concrete syntax: instead of
    8.31 +\isa{rtc\ r} we can read and write {term"r*"}. The actual definition
    8.32 +consists of two rules. Reflexivity is obvious and is immediately declared an
    8.33 +equivalence rule.  Thus the automatic tools will apply it automatically. The
    8.34 +second rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more
    8.35 +\isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an
    8.36 +introduction rule, this is dangerous: the recursion slows down and may
    8.37 +even kill the automatic tactics.
    8.38 +
    8.39 +The above definition of the concept of reflexive transitive closure may
    8.40 +be sufficiently intuitive but it is certainly not the only possible one:
    8.41 +for a start, it does not even mention transitivity explicitly.
    8.42 +The rest of this section is devoted to proving that it is equivalent to
    8.43 +the ``standard'' definition. We start with a simple lemma:%
    8.44 +\end{isamarkuptext}%
    8.45  \isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharcolon}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
    8.46 -\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline
    8.47 -\isanewline
    8.48 -\isacommand{lemma}\ step{\isadigit{2}}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
    8.49 -\ \ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ \ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
    8.50 +\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}%
    8.51 +\begin{isamarkuptext}%
    8.52 +\noindent
    8.53 +Although the lemma itself is an unremarkable consequence of the basic rules,
    8.54 +it has the advantage that it can be declared an introduction rule without the
    8.55 +danger of killing the automatic tactics because \isa{r{\isacharasterisk}} occurs only in
    8.56 +the conclusion and not in the premise. Thus some proofs that would otherwise
    8.57 +need \isa{rtc{\isacharunderscore}step} can now be found automatically. The proof also
    8.58 +shows that \isa{blast} is quite able to handle \isa{rtc{\isacharunderscore}step}. But
    8.59 +some of the other automatic tactics are more sensitive, and even \isa{blast} can be lead astray in the presence of large numbers of rules.
    8.60 +
    8.61 +Let us now turn to transitivity. It should be a consequence of the definition.%
    8.62 +\end{isamarkuptext}%
    8.63 +\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharcolon}\isanewline
    8.64 +\ \ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}%
    8.65 +\begin{isamarkuptxt}%
    8.66 +\noindent
    8.67 +The proof starts canonically by rule induction:%
    8.68 +\end{isamarkuptxt}%
    8.69 +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%
    8.70 +\begin{isamarkuptext}%
    8.71 +\noindent
    8.72 +However, even the resulting base case is a problem
    8.73 +\begin{isabelle}
    8.74 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}
    8.75 +\end{isabelle}
    8.76 +and maybe not what you had expected. We have to abandon this proof attempt.
    8.77 +To understand what is going on,
    8.78 +let us look at the induction rule \isa{rtc{\isachardot}induct}:
    8.79 +\[ \frac{(x,y) \in r^* \qquad \bigwedge x.~P~x~x \quad \dots}{P~x~y} \]
    8.80 +When applying this rule, $x$ becomes \isa{x}, $y$ becomes
    8.81 +\isa{y} and $P~x~y$ becomes \isa{{\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}, thus
    8.82 +yielding the above subgoal. So what went wrong?
    8.83 +
    8.84 +When looking at the instantiation of $P~x~y$ we see
    8.85 +that $P$ does not depend on its second parameter at
    8.86 +all. The reason is that in our original goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only
    8.87 +\isa{x} appears also in the conclusion, but not \isa{y}. Thus our
    8.88 +induction statement is too weak. Fortunately, it can easily be strengthened:
    8.89 +transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%
    8.90 +\end{isamarkuptext}%
    8.91 +\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
    8.92 +\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}%
    8.93 +\begin{isamarkuptxt}%
    8.94 +\noindent
    8.95 +This is not an obscure trick but a generally applicable heuristic:
    8.96 +\begin{quote}\em
    8.97 +Whe proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
    8.98 +pull all other premises containing any of the $x@i$ into the conclusion
    8.99 +using $\longrightarrow$.
   8.100 +\end{quote}
   8.101 +A similar heuristic for other kinds of inductions is formulated in
   8.102 +\S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns
   8.103 +\isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}. Thus in the end we obtain the original
   8.104 +statement of our lemma.
   8.105 +
   8.106 +Now induction produces two subgoals which are both proved automatically:
   8.107 +\begin{isabelle}
   8.108 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline
   8.109 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline
   8.110 +\ \ \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isasymrbrakk}\isanewline
   8.111 +\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}
   8.112 +\end{isabelle}%
   8.113 +\end{isamarkuptxt}%
   8.114  \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
   8.115  \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   8.116  \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline
   8.117 -\isacommand{done}\isanewline
   8.118 -\isanewline
   8.119 -\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
   8.120 -\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ \ {\isasymLongrightarrow}\ {\isasymforall}z{\isachardot}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
   8.121 -\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
   8.122 -\ \isacommand{apply}\ blast\isanewline
   8.123 -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ step{\isadigit{2}}{\isacharparenright}\isanewline
   8.124 -\isacommand{done}\isanewline
   8.125 -\isanewline
   8.126 +\isacommand{done}%
   8.127 +\begin{isamarkuptext}%
   8.128 +Let us now prove that \isa{r{\isacharasterisk}} is really the reflexive transitive closure
   8.129 +of \isa{r}, i.e.\ the least reflexive and transitive
   8.130 +relation containing \isa{r}. The latter is easily formalized%
   8.131 +\end{isamarkuptext}%
   8.132  \isacommand{consts}\ rtc{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline
   8.133  \isacommand{inductive}\ {\isachardoublequote}rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
   8.134  \isakeyword{intros}\isanewline
   8.135 @@ -42,7 +119,8 @@
   8.136  {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
   8.137  {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}%
   8.138  \begin{isamarkuptext}%
   8.139 -The equivalence of the two definitions is easily shown by the obvious rule
   8.140 +\noindent
   8.141 +and the equivalence of the two definitions is easily shown by the obvious rule
   8.142  inductions:%
   8.143  \end{isamarkuptext}%
   8.144  \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
   8.145 @@ -56,7 +134,22 @@
   8.146  \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
   8.147  \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
   8.148  \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
   8.149 -\isacommand{done}\isanewline
   8.150 +\isacommand{done}%
   8.151 +\begin{isamarkuptext}%
   8.152 +So why did we start with the first definition? Because it is simpler. It
   8.153 +contains only two rules, and the single step rule is simpler than
   8.154 +transitivity.  As a consequence, \isa{rtc{\isachardot}induct} is simpler than
   8.155 +\isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough, we should
   8.156 +certainly pick the simplest induction schema available for any concept.
   8.157 +Hence \isa{rtc} is the definition of choice.
   8.158 +
   8.159 +\begin{exercise}
   8.160 +Show that the converse of \isa{rtc{\isacharunderscore}step} also holds:
   8.161 +\begin{isabelle}%
   8.162 +\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
   8.163 +\end{isabelle}
   8.164 +\end{exercise}%
   8.165 +\end{isamarkuptext}%
   8.166  \end{isabellebody}%
   8.167  %%% Local Variables:
   8.168  %%% mode: latex
     9.1 --- a/doc-src/TutorialI/Inductive/inductive.tex	Wed Oct 18 12:30:59 2000 +0200
     9.2 +++ b/doc-src/TutorialI/Inductive/inductive.tex	Wed Oct 18 17:19:18 2000 +0200
     9.3 @@ -1,4 +1,21 @@
     9.4  \chapter{Inductively Defined Sets}
     9.5 +\index{inductive definition|(}
     9.6 +\index{*inductive|(}
     9.7 +
     9.8 +This chapter is dedicated to the most important definition principle after
     9.9 +recursive functions and datatypes: inductively defined sets.
    9.10 +
    9.11 +We start with a simple example \ldots . A slightly more complicated example, the
    9.12 +reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular,
    9.13 +some standard induction heuristics are discussed. To demonstrate the
    9.14 +versatility of inductive definitions, {\S}\ref{sec:CFG} presents a case study
    9.15 +from the realm of context-free grammars. The chapter closes with a discussion
    9.16 +of advanced forms of inductive definitions.
    9.17  
    9.18  \input{Inductive/document/Star}
    9.19  \input{Inductive/document/AB}
    9.20 +
    9.21 +\index{inductive definition|)}
    9.22 +\index{*inductive|)}
    9.23 +
    9.24 +\section{Advanced inductive definitions}
    10.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Wed Oct 18 12:30:59 2000 +0200
    10.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Wed Oct 18 17:19:18 2000 +0200
    10.3 @@ -34,13 +34,14 @@
    10.4  \begin{isabelle}
    10.5  \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
    10.6  \end{isabelle}
    10.7 -We cannot prove this equality because we do not know what @{term"hd"} and
    10.8 -@{term"last"} return when applied to @{term"[]"}.
    10.9 +We cannot prove this equality because we do not know what @{term hd} and
   10.10 +@{term last} return when applied to @{term"[]"}.
   10.11  
   10.12  The point is that we have violated the above warning. Because the induction
   10.13 -formula is only the conclusion, the occurrence of @{term"xs"} in the premises is
   10.14 +formula is only the conclusion, the occurrence of @{term xs} in the premises is
   10.15  not modified by induction. Thus the case that should have been trivial
   10.16 -becomes unprovable. Fortunately, the solution is easy:
   10.17 +becomes unprovable. Fortunately, the solution is easy:\footnote{A very similar
   10.18 +heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
   10.19  \begin{quote}
   10.20  \emph{Pull all occurrences of the induction variable into the conclusion
   10.21  using @{text"\<longrightarrow>"}.}
    11.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Oct 18 12:30:59 2000 +0200
    11.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Oct 18 17:19:18 2000 +0200
    11.3 @@ -41,7 +41,8 @@
    11.4  The point is that we have violated the above warning. Because the induction
    11.5  formula is only the conclusion, the occurrence of \isa{xs} in the premises is
    11.6  not modified by induction. Thus the case that should have been trivial
    11.7 -becomes unprovable. Fortunately, the solution is easy:
    11.8 +becomes unprovable. Fortunately, the solution is easy:\footnote{A very similar
    11.9 +heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
   11.10  \begin{quote}
   11.11  \emph{Pull all occurrences of the induction variable into the conclusion
   11.12  using \isa{{\isasymlongrightarrow}}.}
   11.13 @@ -268,18 +269,18 @@
   11.14  \isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
   11.15  \begin{isamarkuptext}%
   11.16  Finally we should mention that HOL already provides the mother of all
   11.17 -inductions, \textbf{wellfounded
   11.18 -induction}\indexbold{induction!wellfounded}\index{wellfounded
   11.19 -induction|see{induction, wellfounded}} (\isa{wf{\isacharunderscore}induct}):
   11.20 +inductions, \textbf{well-founded
   11.21 +induction}\indexbold{induction!well-founded}\index{well-founded
   11.22 +induction|see{induction, well-founded}} (\isa{wf{\isacharunderscore}induct}):
   11.23  \begin{isabelle}%
   11.24  \ \ \ \ \ {\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.25  \end{isabelle}
   11.26 -where \isa{wf\ r} means that the relation \isa{r} is wellfounded
   11.27 -(see \S\ref{sec:wellfounded}).
   11.28 +where \isa{wf\ r} means that the relation \isa{r} is well-founded
   11.29 +(see \S\ref{sec:well-founded}).
   11.30  For example, theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} can be viewed (and
   11.31  derived) as a special case of \isa{wf{\isacharunderscore}induct} where 
   11.32  \isa{r} is \isa{{\isacharless}} on \isa{nat}. The details can be found in the HOL library.
   11.33 -For a mathematical account of wellfounded induction see, for example, \cite{Baader-Nipkow}.%
   11.34 +For a mathematical account of well-founded induction see, for example, \cite{Baader-Nipkow}.%
   11.35  \end{isamarkuptext}%
   11.36  \end{isabellebody}%
   11.37  %%% Local Variables:
    12.1 --- a/doc-src/TutorialI/Recdef/Nested1.thy	Wed Oct 18 12:30:59 2000 +0200
    12.2 +++ b/doc-src/TutorialI/Recdef/Nested1.thy	Wed Oct 18 17:19:18 2000 +0200
    12.3 @@ -21,7 +21,7 @@
    12.4  Remember that function @{term size} is defined for each \isacommand{datatype}.
    12.5  However, the definition does not succeed. Isabelle complains about an
    12.6  unproved termination condition
    12.7 -@{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
    12.8 +@{prop[display]"t : set ts --> size t < Suc (term_list_size ts)"}
    12.9  where @{term set} returns the set of elements of a list
   12.10  and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
   12.11  function automatically defined by Isabelle
    13.1 --- a/doc-src/TutorialI/appendix.tex	Wed Oct 18 12:30:59 2000 +0200
    13.2 +++ b/doc-src/TutorialI/appendix.tex	Wed Oct 18 17:19:18 2000 +0200
    13.3 @@ -64,25 +64,26 @@
    13.4  \indexboldpos{\isasymtimes}{$IsaFun}&
    13.5  \ttindexboldpos{*}{$HOL2arithfun} &
    13.6  \verb$\<times>$\\
    13.7 -\indexboldpos{\isasymin}{$HOL3Set}&
    13.8 -\ttindexboldpos{:}{$HOL3Set} &
    13.9 +\indexboldpos{\isasymin}{$HOL3Set0a}&
   13.10 +\ttindexboldpos{:}{$HOL3Set0b} &
   13.11  \verb$\<in>$\\
   13.12 -? & %\indexboldpos{\isasymnotin}{$HOL3Set} fails for some strange reason
   13.13 -\verb$~:$\index{$HOL3Set@\verb$~:$|bold} &
   13.14 +\isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} &
   13.15 +\verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} &
   13.16  \verb$\<notin>$\\
   13.17 -\indexboldpos{\isasymsubseteq}{$HOL3Set}&
   13.18 -\verb$<=$ &
   13.19 -\verb$\<subseteq>$\\
   13.20 -\indexboldpos{\isasymunion}{$HOL3Set}&
   13.21 +\indexboldpos{\isasymsubseteq}{$HOL3Set0e}&
   13.22 +\verb$<=$ & \verb$\<subseteq>$\\
   13.23 +\indexboldpos{\isasymsubset}{$HOL3Set0f}&
   13.24 +\verb$<$ & \verb$\<subset>$\\
   13.25 +\indexboldpos{\isasymunion}{$HOL3Set1}&
   13.26  \ttindexbold{Un} &
   13.27  \verb$\<union>$\\
   13.28 -\indexboldpos{\isasyminter}{$HOL3Set}&
   13.29 +\indexboldpos{\isasyminter}{$HOL3Set1}&
   13.30  \ttindexbold{Int} &
   13.31  \verb$\<inter>$\\
   13.32 -\indexboldpos{\isasymUnion}{$HOL3Set}&
   13.33 +\indexboldpos{\isasymUnion}{$HOL3Set2}&
   13.34  \ttindexbold{UN}, \ttindexbold{Union} &
   13.35  \verb$\<Union>$\\
   13.36 -\indexboldpos{\isasymInter}{$HOL3Set}&
   13.37 +\indexboldpos{\isasymInter}{$HOL3Set2}&
   13.38  \ttindexbold{INT}, \ttindexbold{Inter} &
   13.39  \verb$\<Inter>$\\
   13.40  \hline
    14.1 --- a/doc-src/TutorialI/todo.tobias	Wed Oct 18 12:30:59 2000 +0200
    14.2 +++ b/doc-src/TutorialI/todo.tobias	Wed Oct 18 17:19:18 2000 +0200
    14.3 @@ -21,8 +21,6 @@
    14.4  Add map_cong?? (upto 10% slower)
    14.5  But we should install UN_cong and INT_cong too.
    14.6  
    14.7 -recdef: funny behaviour with map (see email to Konrad.Slind, Recdef/Nested1)
    14.8 -
    14.9  defs with = and pattern matching
   14.10  
   14.11  use arith_tac in recdef to solve termination conditions?
   14.12 @@ -90,8 +88,8 @@
   14.13  clarify, clarsimp (intro, elim?)
   14.14  
   14.15  Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
   14.16 -Where explained?
   14.17 -Inductive also needs rule_format!
   14.18 +Where explained? Should go into a separate section as Inductive needs it as
   14.19 +well.
   14.20  
   14.21  Where is "simplified" explained? Needed by Inductive/AB.thy
   14.22  
   14.23 @@ -189,44 +187,6 @@
   14.24  
   14.25  
   14.26  ==============================================================
   14.27 -Nested inductive datatypes: better recursion and induction
   14.28 -
   14.29 -Show how to derive simpler primrec functions using eg map. Text:
   14.30 -
   14.31 -Returning to the definition of \texttt{subst}, we have to admit that it does
   14.32 -not really need the auxiliary \texttt{substs} function. The \texttt{App}-case
   14.33 -can directly be expressed as
   14.34 -\begin{ttbox}
   14.35 -\input{Datatype/appmap}\end{ttbox}
   14.36 -Although Isabelle insists on the more verbose version, we can easily {\em
   14.37 -  prove} that the \texttt{map}-equation holds: simply by induction on
   14.38 -\texttt{ts} followed by \texttt{Auto_tac}.
   14.39 -lemma "subst s (App f ts) = App f (map (subst s) ts)";
   14.40 -by(induct_tac ts, auto);
   14.41 -
   14.42 -Now explain how to remove old eqns from simpset by naming them.
   14.43 -But: the new eqn only helps if the induction schema is also modified
   14.44 -accordingly:
   14.45 -
   14.46 -val prems =
   14.47 -Goal "[| !!v. P(Var v); !!f ts. (!!t. t : set ts ==> P t) ==> P(App f ts) |] \
   14.48 -\     ==> P t & (!t: set ts. P t)";
   14.49 -by(induct_tac "t ts" 1);
   14.50 -brs prems 1;
   14.51 -brs prems 1;
   14.52 -by(Blast_tac 1);
   14.53 -by(Simp_tac 1);
   14.54 -by(Asm_simp_tac 1);
   14.55 -
   14.56 -Now the following exercise has an easy proof:
   14.57 -
   14.58 -\begin{exercise}
   14.59 -  Define a function \texttt{rev_term} of type \texttt{term -> term} that
   14.60 -  recursively reverses the order of arguments of all function symbols in a
   14.61 -  term. Prove that \texttt{rev_term(rev_term t) = t}.
   14.62 -\end{exercise}
   14.63 -
   14.64 -==============================================================
   14.65  Recdef:
   14.66  
   14.67  nested recursion
   14.68 @@ -237,10 +197,6 @@
   14.69   Trie?
   14.70  a case study?
   14.71  
   14.72 -A separate subsection on recdef beyond measure, eg <*lex*> and psubset.
   14.73 -Example: some finite fixpoint computation? MC, Grammar?
   14.74 -How to modify wf-prover?
   14.75 -
   14.76  ----------
   14.77  
   14.78  Partial rekursive functions / Nontermination