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