*** empty log message ***
authornipkow
Tue Oct 17 16:59:02 2000 +0200 (2000-10-17)
changeset 10237875bf54b5d74
parent 10236 7626cb4e1407
child 10238 9dc33c6c5df9
*** empty log message ***
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/document/CTL.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/fp.tex
doc-src/TutorialI/todo.tobias
     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.10  \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\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.32 -\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isadigit{2}}{\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"  ("_*" [1000] 999)
    4.20 +consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"  ("_*" [1000] 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.19 -\isacommand{consts}\ trc\ {\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
    6.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
    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.32  \isacommand{lemma}\ step{\isadigit{2}}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\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.47  \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ step{\isadigit{2}}{\isacharparenright}\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.51 -\isacommand{inductive}\ {\isachardoublequote}trc{\isadigit{2}}\ r{\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.53 +\isacommand{inductive}\ {\isachardoublequote}rtc{\isadigit{2}}\ r{\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.56 -{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
    6.57 -{\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\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.60 +{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
    6.61 +{\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}%
    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.67 +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\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.75 -\ \isacommand{apply}{\isacharparenleft}erule\ trc{\isadigit{2}}{\isachardot}induct{\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.80 -\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
    6.81 -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isadigit{2}}{\isachardot}intros{\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.84 +\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
    6.85 +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\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