# HG changeset patch # User nipkow # Date 1008266710 -3600 # Node ID a4dd02e744e0cb0f725feb6d716a8d864886b3ff # Parent e28870d8b223181219bd9608f8b16c56bc0b6e80 *** empty log message *** diff -r e28870d8b223 -r a4dd02e744e0 doc-src/TutorialI/CTL/CTLind.thy --- a/doc-src/TutorialI/CTL/CTLind.thy Thu Dec 13 17:57:55 2001 +0100 +++ b/doc-src/TutorialI/CTL/CTLind.thy Thu Dec 13 19:05:10 2001 +0100 @@ -31,10 +31,10 @@ text{* It is easy to see that for any infinite @{term A}-avoiding path @{term f} -with @{prop"f 0 \ Avoid s A"} there is an infinite @{term A}-avoiding path +with @{prop"f(0::nat) \ Avoid s A"} there is an infinite @{term A}-avoiding path starting with @{term s} because (by definition of @{term Avoid}) there is a -finite @{term A}-avoiding path from @{term s} to @{term"f 0"}. -The proof is by induction on @{prop"f 0 \ Avoid s A"}. However, +finite @{term A}-avoiding path from @{term s} to @{term"f(0::nat)"}. +The proof is by induction on @{prop"f(0::nat) \ Avoid s A"}. However, this requires the following reformulation, as explained in \S\ref{sec:ind-var-in-prems} above; the @{text rule_format} directive undoes the reformulation after the proof. diff -r e28870d8b223 -r a4dd02e744e0 doc-src/TutorialI/CTL/document/CTLind.tex --- a/doc-src/TutorialI/CTL/document/CTLind.tex Thu Dec 13 17:57:55 2001 +0100 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Thu Dec 13 19:05:10 2001 +0100 @@ -37,10 +37,10 @@ % \begin{isamarkuptext}% It is easy to see that for any infinite \isa{A}-avoiding path \isa{f} -with \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path +with \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path starting with \isa{s} because (by definition of \isa{Avoid}) there is a -finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}b{\isacharparenright}}. -The proof is by induction on \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A}. However, +finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}. +The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A}. However, this requires the following reformulation, as explained in \S\ref{sec:ind-var-in-prems} above; the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.% diff -r e28870d8b223 -r a4dd02e744e0 doc-src/TutorialI/Misc/AdvancedInd.thy --- a/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Dec 13 17:57:55 2001 +0100 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Dec 13 19:05:10 2001 +0100 @@ -70,18 +70,7 @@ which can yield a fairly complex conclusion. However, @{text rule_format} can remove any number of occurrences of @{text"\"} and @{text"\"}. -*} -(*<*) -by auto; -(*>*) -(* -Here is a simple example (which is proved by @{text"blast"}): -lemma simple[rule_format]: "\y. A y \ B y \ B y \ A y"; -by blast; -*) - -text{* \index{induction!on a term}% A second reason why your proposition may not be amenable to induction is that you want to induct on a complex term, rather than a variable. In @@ -122,6 +111,7 @@ single theorem because it depends on the number of free variables in $t$ --- the notation $\overline{y}$ is merely an informal device. *} +(*<*)by auto(*>*) subsection{*Beyond Structural and Recursion Induction*}; diff -r e28870d8b223 -r a4dd02e744e0 doc-src/TutorialI/Misc/document/AdvancedInd.tex --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Dec 13 17:57:55 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Dec 13 19:05:10 2001 +0100 @@ -81,12 +81,8 @@ Additionally, you may also have to universally quantify some other variables, which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format} can remove any number of occurrences of \isa{{\isasymforall}} and -\isa{{\isasymlongrightarrow}}.% -\end{isamarkuptxt}% -\isamarkuptrue% -\isamarkupfalse% -% -\begin{isamarkuptext}% +\isa{{\isasymlongrightarrow}}. + \index{induction!on a term}% A second reason why your proposition may not be amenable to induction is that you want to induct on a complex term, rather than a variable. In @@ -126,8 +122,9 @@ Unfortunately, this induction schema cannot be expressed as a single theorem because it depends on the number of free variables in $t$ --- the notation $\overline{y}$ is merely an informal device.% -\end{isamarkuptext}% +\end{isamarkuptxt}% \isamarkuptrue% +\isamarkupfalse% % \isamarkupsubsection{Beyond Structural and Recursion Induction% } diff -r e28870d8b223 -r a4dd02e744e0 doc-src/TutorialI/isabellesym.sty --- a/doc-src/TutorialI/isabellesym.sty Thu Dec 13 17:57:55 2001 +0100 +++ b/doc-src/TutorialI/isabellesym.sty Thu Dec 13 19:05:10 2001 +0100 @@ -345,10 +345,10 @@ \newcommand{\isasymJoin}{\isamath{\Join}} %requires latexsym \newcommand{\isasymwp}{\isamath{\wp}} \newcommand{\isasymwrong}{\isamath{\wr}} -\newcommand{\isasymspacespace}{\isamath{~~}} +\newcommand{\isasymstruct}{\isamath{\diamond}} \newcommand{\isasymacute}{\isatext{\'\relax}} +\newcommand{\isasymindex}{\isatext{\i}} \newcommand{\isasymdieresis}{\isatext{\"\relax}} -\newcommand{\isasymstruct}{\isamath{\diamond}} -\newcommand{\isasymindex}{\isamath{\i}} \newcommand{\isasymcedilla}{\isatext{\c\relax}} \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}} +\newcommand{\isasymspacespace}{\isamath{~~}} diff -r e28870d8b223 -r a4dd02e744e0 doc-src/TutorialI/todo.tobias --- a/doc-src/TutorialI/todo.tobias Thu Dec 13 17:57:55 2001 +0100 +++ b/doc-src/TutorialI/todo.tobias Thu Dec 13 19:05:10 2001 +0100 @@ -1,5 +1,3 @@ -"You know my methods. Apply them!" - Implementation ==============