1.1 --- a/doc-src/TutorialI/CTL/CTLind.thy Thu Dec 13 17:57:55 2001 +0100
1.2 +++ b/doc-src/TutorialI/CTL/CTLind.thy Thu Dec 13 19:05:10 2001 +0100
1.3 @@ -31,10 +31,10 @@
1.4
1.5 text{*
1.6 It is easy to see that for any infinite @{term A}-avoiding path @{term f}
1.7 -with @{prop"f 0 \<in> Avoid s A"} there is an infinite @{term A}-avoiding path
1.8 +with @{prop"f(0::nat) \<in> Avoid s A"} there is an infinite @{term A}-avoiding path
1.9 starting with @{term s} because (by definition of @{term Avoid}) there is a
1.10 -finite @{term A}-avoiding path from @{term s} to @{term"f 0"}.
1.11 -The proof is by induction on @{prop"f 0 \<in> Avoid s A"}. However,
1.12 +finite @{term A}-avoiding path from @{term s} to @{term"f(0::nat)"}.
1.13 +The proof is by induction on @{prop"f(0::nat) \<in> Avoid s A"}. However,
1.14 this requires the following
1.15 reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
1.16 the @{text rule_format} directive undoes the reformulation after the proof.
2.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex Thu Dec 13 17:57:55 2001 +0100
2.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Thu Dec 13 19:05:10 2001 +0100
2.3 @@ -37,10 +37,10 @@
2.4 %
2.5 \begin{isamarkuptext}%
2.6 It is easy to see that for any infinite \isa{A}-avoiding path \isa{f}
2.7 -with \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
2.8 +with \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
2.9 starting with \isa{s} because (by definition of \isa{Avoid}) there is a
2.10 -finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}b{\isacharparenright}}.
2.11 -The proof is by induction on \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A}. However,
2.12 +finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}.
2.13 +The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A}. However,
2.14 this requires the following
2.15 reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
2.16 the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.%
3.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Dec 13 17:57:55 2001 +0100
3.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Dec 13 19:05:10 2001 +0100
3.3 @@ -70,18 +70,7 @@
3.4 which can yield a fairly complex conclusion. However, @{text rule_format}
3.5 can remove any number of occurrences of @{text"\<forall>"} and
3.6 @{text"\<longrightarrow>"}.
3.7 -*}
3.8
3.9 -(*<*)
3.10 -by auto;
3.11 -(*>*)
3.12 -(*
3.13 -Here is a simple example (which is proved by @{text"blast"}):
3.14 -lemma simple[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
3.15 -by blast;
3.16 -*)
3.17 -
3.18 -text{*
3.19 \index{induction!on a term}%
3.20 A second reason why your proposition may not be amenable to induction is that
3.21 you want to induct on a complex term, rather than a variable. In
3.22 @@ -122,6 +111,7 @@
3.23 single theorem because it depends on the number of free variables in $t$ ---
3.24 the notation $\overline{y}$ is merely an informal device.
3.25 *}
3.26 +(*<*)by auto(*>*)
3.27
3.28 subsection{*Beyond Structural and Recursion Induction*};
3.29
4.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Dec 13 17:57:55 2001 +0100
4.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Dec 13 19:05:10 2001 +0100
4.3 @@ -81,12 +81,8 @@
4.4 Additionally, you may also have to universally quantify some other variables,
4.5 which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format}
4.6 can remove any number of occurrences of \isa{{\isasymforall}} and
4.7 -\isa{{\isasymlongrightarrow}}.%
4.8 -\end{isamarkuptxt}%
4.9 -\isamarkuptrue%
4.10 -\isamarkupfalse%
4.11 -%
4.12 -\begin{isamarkuptext}%
4.13 +\isa{{\isasymlongrightarrow}}.
4.14 +
4.15 \index{induction!on a term}%
4.16 A second reason why your proposition may not be amenable to induction is that
4.17 you want to induct on a complex term, rather than a variable. In
4.18 @@ -126,8 +122,9 @@
4.19 Unfortunately, this induction schema cannot be expressed as a
4.20 single theorem because it depends on the number of free variables in $t$ ---
4.21 the notation $\overline{y}$ is merely an informal device.%
4.22 -\end{isamarkuptext}%
4.23 +\end{isamarkuptxt}%
4.24 \isamarkuptrue%
4.25 +\isamarkupfalse%
4.26 %
4.27 \isamarkupsubsection{Beyond Structural and Recursion Induction%
4.28 }
5.1 --- a/doc-src/TutorialI/isabellesym.sty Thu Dec 13 17:57:55 2001 +0100
5.2 +++ b/doc-src/TutorialI/isabellesym.sty Thu Dec 13 19:05:10 2001 +0100
5.3 @@ -345,10 +345,10 @@
5.4 \newcommand{\isasymJoin}{\isamath{\Join}} %requires latexsym
5.5 \newcommand{\isasymwp}{\isamath{\wp}}
5.6 \newcommand{\isasymwrong}{\isamath{\wr}}
5.7 -\newcommand{\isasymspacespace}{\isamath{~~}}
5.8 +\newcommand{\isasymstruct}{\isamath{\diamond}}
5.9 \newcommand{\isasymacute}{\isatext{\'\relax}}
5.10 +\newcommand{\isasymindex}{\isatext{\i}}
5.11 \newcommand{\isasymdieresis}{\isatext{\"\relax}}
5.12 -\newcommand{\isasymstruct}{\isamath{\diamond}}
5.13 -\newcommand{\isasymindex}{\isamath{\i}}
5.14 \newcommand{\isasymcedilla}{\isatext{\c\relax}}
5.15 \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
5.16 +\newcommand{\isasymspacespace}{\isamath{~~}}
6.1 --- a/doc-src/TutorialI/todo.tobias Thu Dec 13 17:57:55 2001 +0100
6.2 +++ b/doc-src/TutorialI/todo.tobias Thu Dec 13 19:05:10 2001 +0100
6.3 @@ -1,5 +1,3 @@
6.4 -"You know my methods. Apply them!"
6.5 -
6.6 Implementation
6.7 ==============
6.8