author nipkow Tue Oct 17 16:59:02 2000 +0200 (2000-10-17) changeset 10237 875bf54b5d74 parent 10236 7626cb4e1407 child 10238 9dc33c6c5df9
*** empty log message ***
 doc-src/TutorialI/CTL/CTL.thy file | annotate | diff | revisions doc-src/TutorialI/CTL/document/CTL.tex file | annotate | diff | revisions doc-src/TutorialI/Inductive/AB.thy file | annotate | diff | revisions doc-src/TutorialI/Inductive/Star.thy file | annotate | diff | revisions doc-src/TutorialI/Inductive/document/AB.tex file | annotate | diff | revisions doc-src/TutorialI/Inductive/document/Star.tex file | annotate | diff | revisions doc-src/TutorialI/fp.tex file | annotate | diff | revisions doc-src/TutorialI/todo.tobias file | annotate | diff | revisions
     1.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Tue Oct 17 13:28:57 2000 +0200
1.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Tue Oct 17 16:59:02 2000 +0200
1.3 @@ -181,9 +181,9 @@
1.4  done;
1.5
1.6  text{*\noindent
1.7 -is proved by a variant of contraposition (@{thm[source]contrapos_np}:
1.8 -@{thm contrapos_np[no_vars]}), i.e.\ assuming the negation of the conclusion
1.9 -and proving @{term"s : lfp(af A)"}. Unfolding @{term lfp} once and
1.10 +is proved by a variant of contraposition:
1.11 +assume the negation of the conclusion and prove @{term"s : lfp(af A)"}.
1.12 +Unfolding @{term lfp} once and
1.13  simplifying with the definition of @{term af} finishes the proof.
1.14
1.15  Now we iterate this process. The following construction of the desired
1.16 @@ -333,8 +333,7 @@
1.17  "{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
1.18
1.19  txt{*\noindent
1.20 -The proof is again pointwise and then by contraposition (@{thm[source]contrapos_pp} is the rule
1.21 -@{thm contrapos_pp}):
1.22 +The proof is again pointwise and then by contraposition:
1.23  *};
1.24
1.25  apply(rule subsetI);

     2.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Tue Oct 17 13:28:57 2000 +0200
2.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Tue Oct 17 16:59:02 2000 +0200
2.3 @@ -117,15 +117,15 @@
2.4  \end{isamarkuptext}%
2.5  \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
2.6  \ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
2.7 -\isacommand{apply}{\isacharparenleft}erule\ swap{\isacharparenright}\isanewline
2.8 +\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}np{\isacharparenright}\isanewline
2.9  \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
2.11  \isacommand{done}%
2.12  \begin{isamarkuptext}%
2.13  \noindent
2.14 -is proved by a variant of contraposition (\isa{swap}:
2.15 -\isa{{\isasymlbrakk}{\isasymnot}\ Q{\isacharsemicolon}\ {\isasymnot}\ P\ {\isasymLongrightarrow}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P}), i.e.\ assuming the negation of the conclusion
2.16 -and proving \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} once and
2.17 +is proved by a variant of contraposition:
2.18 +assume the negation of the conclusion and prove \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}.
2.19 +Unfolding \isa{lfp} once and
2.20  simplifying with the definition of \isa{af} finishes the proof.
2.21
2.22  Now we iterate this process. The following construction of the desired
2.23 @@ -244,11 +244,10 @@
2.24  {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}%
2.25  \begin{isamarkuptxt}%
2.26  \noindent
2.27 -The proof is again pointwise and then by contraposition (\isa{contrapos{\isadigit{2}}} is the rule
2.28 -\isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):%
2.29 +The proof is again pointwise and then by contraposition:%
2.30  \end{isamarkuptxt}%
2.31  \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
2.33 +\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
2.34  \isacommand{apply}\ simp%
2.35  \begin{isamarkuptxt}%
2.36  \begin{isabelle}

     3.1 --- a/doc-src/TutorialI/Inductive/AB.thy	Tue Oct 17 13:28:57 2000 +0200
3.2 +++ b/doc-src/TutorialI/Inductive/AB.thy	Tue Oct 17 16:59:02 2000 +0200
3.3 @@ -68,15 +68,14 @@
3.4
3.5  lemma correctness:
3.6    "(w \<in> S \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b])     \<and>
3.7 -    (w \<in> A \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1) \<and>
3.8 -    (w \<in> B \<longrightarrow> size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1)"
3.9 +   (w \<in> A \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1) \<and>
3.10 +   (w \<in> B \<longrightarrow> size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1)"
3.11
3.12  txt{*\noindent
3.13  These propositions are expressed with the help of the predefined @{term
3.14  filter} function on lists, which has the convenient syntax @{term"[x\<in>xs. P
3.15  x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}
3.16 -holds. The length of a list is usually written @{term length}, and @{term
3.17 -size} is merely a shorthand.
3.18 +holds. Remember that on lists @{term size} and @{term length} are synonymous.
3.19
3.20  The proof itself is by rule induction and afterwards automatic:
3.21  *}
3.22 @@ -193,8 +192,8 @@
3.23
3.24  theorem completeness:
3.25    "(size[x\<in>w. x=a] = size[x\<in>w. x=b]     \<longrightarrow> w \<in> S) \<and>
3.26 -    (size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
3.27 -    (size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1 \<longrightarrow> w \<in> B)";
3.28 +   (size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
3.29 +   (size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1 \<longrightarrow> w \<in> B)";
3.30
3.31  txt{*\noindent
3.32  The proof is by induction on @{term w}. Structural induction would fail here

     4.1 --- a/doc-src/TutorialI/Inductive/Star.thy	Tue Oct 17 13:28:57 2000 +0200
4.2 +++ b/doc-src/TutorialI/Inductive/Star.thy	Tue Oct 17 16:59:02 2000 +0200
4.3 @@ -1,9 +1,9 @@
4.4  (*<*)theory Star = Main:(*>*)
4.5
4.6 -section{*The transitive and reflexive closure*}
4.7 +section{*The reflexive transitive closure*}
4.8
4.9  text{*
4.10 -A perfect example of an inductive definition is the transitive, reflexive
4.11 +A perfect example of an inductive definition is the reflexive transitive
4.12  closure of a relation. This concept was already introduced in
4.13  \S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
4.14  the operator @{text"^*"} is not defined inductively but via a least
4.15 @@ -11,46 +11,52 @@
4.16  inductive definitions are not yet available. But now they are:
4.17  *}
4.18
4.19 -consts trc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"  ("_*"  999)
4.20 +consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"  ("_*"  999)
4.21  inductive "r*"
4.22  intros
4.23 -trc_refl[intro!]:                        "(x,x) \<in> r*"
4.24 -trc_step: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
4.25 +rtc_refl[intro!]:                        "(x,x) \<in> r*"
4.26 +rtc_step: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
4.27
4.28  lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
4.29 -by(blast intro: trc_step);
4.30 +by(blast intro: rtc_step);
4.31
4.32  lemma step2[rule_format]:
4.33    "(y,z) \<in> r*  \<Longrightarrow> (x,y) \<in> r \<longrightarrow> (x,z) \<in> r*"
4.34 -apply(erule trc.induct)
4.35 +apply(erule rtc.induct)
4.36   apply(blast);
4.37 -apply(blast intro: trc_step);
4.38 +apply(blast intro: rtc_step);
4.39  done
4.40
4.41 -lemma trc_trans[rule_format]:
4.42 +lemma rtc_trans[rule_format]:
4.43    "(x,y) \<in> r*  \<Longrightarrow> \<forall>z. (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
4.44 -apply(erule trc.induct)
4.45 +apply(erule rtc.induct)
4.46   apply blast;
4.47  apply(blast intro: step2);
4.48  done
4.49
4.50 -consts trc2 :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"
4.51 -inductive "trc2 r"
4.52 +consts rtc2 :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"
4.53 +inductive "rtc2 r"
4.54  intros
4.55 -"(x,y) \<in> r \<Longrightarrow> (x,y) \<in> trc2 r"
4.56 -"(x,x) \<in> trc2 r"
4.57 -"\<lbrakk> (x,y) \<in> trc2 r; (y,z) \<in> trc2 r \<rbrakk> \<Longrightarrow> (x,z) \<in> trc2 r"
4.58 +"(x,y) \<in> r \<Longrightarrow> (x,y) \<in> rtc2 r"
4.59 +"(x,x) \<in> rtc2 r"
4.60 +"\<lbrakk> (x,y) \<in> rtc2 r; (y,z) \<in> rtc2 r \<rbrakk> \<Longrightarrow> (x,z) \<in> rtc2 r"
4.61
4.62 +text{*
4.63 +The equivalence of the two definitions is easily shown by the obvious rule
4.64 +inductions:
4.65 +*}
4.66
4.67 -lemma "((x,y) \<in> trc2 r) = ((x,y) \<in> r*)"
4.68 -apply(rule iffI);
4.69 - apply(erule trc2.induct);
4.70 -   apply(blast);
4.71 +lemma "(x,y) \<in> rtc2 r \<Longrightarrow> (x,y) \<in> r*"
4.72 +apply(erule rtc2.induct);
4.73    apply(blast);
4.74 - apply(blast intro: trc_trans);
4.75 -apply(erule trc.induct);
4.76 - apply(blast intro: trc2.intros);
4.77 -apply(blast intro: trc2.intros);
4.78 + apply(blast);
4.79 +apply(blast intro: rtc_trans);
4.80 +done
4.81 +
4.82 +lemma "(x,y) \<in> r* \<Longrightarrow> (x,y) \<in> rtc2 r"
4.83 +apply(erule rtc.induct);
4.84 + apply(blast intro: rtc2.intros);
4.85 +apply(blast intro: rtc2.intros);
4.86  done
4.87
4.88  (*<*)end(*>*)

     5.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Tue Oct 17 13:28:57 2000 +0200
5.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Tue Oct 17 16:59:02 2000 +0200
5.3 @@ -63,12 +63,12 @@
5.4  \end{isamarkuptext}%
5.5  \isacommand{lemma}\ correctness{\isacharcolon}\isanewline
5.6  \ \ {\isachardoublequote}{\isacharparenleft}w\ {\isasymin}\ S\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isasymand}\isanewline
5.7 -\ \ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline
5.8 -\ \ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}%
5.9 +\ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline
5.10 +\ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}%
5.11  \begin{isamarkuptxt}%
5.12  \noindent
5.13  These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{filter\ P\ xs}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x}
5.14 -holds. The length of a list is usually written \isa{size}, and \isa{size} is merely a shorthand.
5.15 +holds. Remember that on lists \isa{size} and \isa{size} are synonymous.
5.16
5.17  The proof itself is by rule induction and afterwards automatic:%
5.18  \end{isamarkuptxt}%
5.19 @@ -177,8 +177,8 @@
5.20  \end{isamarkuptext}%
5.21  \isacommand{theorem}\ completeness{\isacharcolon}\isanewline
5.22  \ \ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline
5.23 -\ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline
5.24 -\ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}%
5.25 +\ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline
5.26 +\ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}%
5.27  \begin{isamarkuptxt}%
5.28  \noindent
5.29  The proof is by induction on \isa{w}. Structural induction would fail here

     6.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex	Tue Oct 17 13:28:57 2000 +0200
6.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex	Tue Oct 17 16:59:02 2000 +0200
6.3 @@ -2,56 +2,60 @@
6.4  \begin{isabellebody}%
6.5  \def\isabellecontext{Star}%
6.6  %
6.7 -\isamarkupsection{The transitive and reflexive closure}
6.8 +\isamarkupsection{The reflexive transitive closure}
6.9  %
6.10  \begin{isamarkuptext}%
6.11 -A perfect example of an inductive definition is the transitive, reflexive
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 \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least
6.16  fixpoint because at that point in the theory hierarchy
6.17  inductive definitions are not yet available. But now they are:%
6.18  \end{isamarkuptext}%
6.21  \isacommand{inductive}\ {\isachardoublequote}r{\isacharasterisk}{\isachardoublequote}\isanewline
6.22  \isakeyword{intros}\isanewline
6.23 -trc{\isacharunderscore}refl{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
6.24 -trc{\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
6.25 +rtc{\isacharunderscore}refl{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
6.26 +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
6.27  \isanewline
6.28  \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
6.29 -\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}step{\isacharparenright}\isanewline
6.30 +\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline
6.31  \isanewline
6.33  \ \ {\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
6.34 -\isacommand{apply}{\isacharparenleft}erule\ trc{\isachardot}induct{\isacharparenright}\isanewline
6.35 +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
6.36  \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
6.37 -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}step{\isacharparenright}\isanewline
6.38 +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline
6.39  \isacommand{done}\isanewline
6.40  \isanewline
6.41 -\isacommand{lemma}\ trc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
6.42 +\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
6.43  \ \ {\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
6.44 -\isacommand{apply}{\isacharparenleft}erule\ trc{\isachardot}induct{\isacharparenright}\isanewline
6.45 +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
6.46  \ \isacommand{apply}\ blast\isanewline
6.48  \isacommand{done}\isanewline
6.49  \isanewline
6.50 -\isacommand{consts}\ trc{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline
6.52 +\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
6.54  \isakeyword{intros}\isanewline
6.55 -{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
6.58 -\isanewline
6.59 +{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
6.62 +\begin{isamarkuptext}%
6.63 +The equivalence of the two definitions is easily shown by the obvious rule
6.64 +inductions:%
6.65 +\end{isamarkuptext}%
6.66 +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
6.68 +\ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
6.69 +\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
6.70 +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}trans{\isacharparenright}\isanewline
6.71 +\isacommand{done}\isanewline
6.72  \isanewline
6.73 -\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharparenright}{\isachardoublequote}\isanewline
6.74 -\isacommand{apply}{\isacharparenleft}rule\ iffI{\isacharparenright}\isanewline
6.76 -\ \ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
6.77 -\ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
6.78 -\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}trans{\isacharparenright}\isanewline
6.79 -\isacommand{apply}{\isacharparenleft}erule\ trc{\isachardot}induct{\isacharparenright}\isanewline
6.82 +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
6.83 +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
6.86  \isacommand{done}\isanewline
6.87  \end{isabellebody}%
6.88  %%% Local Variables:

     7.1 --- a/doc-src/TutorialI/fp.tex	Tue Oct 17 13:28:57 2000 +0200
7.2 +++ b/doc-src/TutorialI/fp.tex	Tue Oct 17 16:59:02 2000 +0200
7.3 @@ -188,11 +188,12 @@
7.4  Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
7.5  the natural numbers (see~\S\ref{sec:nat} below). For lists, \isa{size} is
7.6  just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
7.7 -  1}.  In general, \isa{size} returns \isa{0} for all constructors that do
7.8 -not have an argument of type $t$, and for all other constructors \isa{1 +}
7.9 -the sum of the sizes of all arguments of type $t$. Note that because
7.10 +  1}.  In general, \isaindexbold{size} returns \isa{0} for all constructors
7.11 +that do not have an argument of type $t$, and for all other constructors
7.12 +\isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because
7.13  \isa{size} is defined on every datatype, it is overloaded; on lists
7.14 -\isa{size} is also called \isa{length}, which is not overloaded.
7.15 +\isa{size} is also called \isaindexbold{length}, which is not overloaded.
7.16 +Isbelle will always show \isa{size} on lists as \isa{length}.
7.17
7.18
7.19  \subsection{Primitive recursion}

     8.1 --- a/doc-src/TutorialI/todo.tobias	Tue Oct 17 13:28:57 2000 +0200
8.2 +++ b/doc-src/TutorialI/todo.tobias	Tue Oct 17 16:59:02 2000 +0200
8.3 @@ -50,9 +50,6 @@
8.4
8.5  an example of induction: !y. A --> B --> C ??
8.6
8.7 -Advanced Ind expects rule_format incl (no_asm) (which it currently explains!
8.8 -Where explained?
8.9 -
8.10  Appendix: Lexical: long ids.
8.11
8.12  Warning: infixes automatically become reserved words!
8.13 @@ -83,7 +80,8 @@
8.14
8.15  Mention that simp etc (big step tactics) insist on change?
8.16
8.17 -Explain what "by" and "." really do, and introduce "done".
8.18 +Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it
8.19 +does more.)
8.20
8.21  A list of further useful commands (rules? tricks?)
8.22  prefer, defer
8.23 @@ -91,7 +89,11 @@
8.24  An overview of the automatic methods: simp, auto, fast, blast, force,
8.25  clarify, clarsimp (intro, elim?)
8.26
8.27 -explain rulify before induction section?
8.28 +Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
8.29 +Where explained?
8.30 +Inductive also needs rule_format!
8.31 +
8.32 +Where is "simplified" explained? Needed by Inductive/AB.thy
8.33
8.34  demonstrate x : set xs in Sets. Or Tricks chapter?
8.35