*** empty log message ***
authorwenzelm
Mon Oct 08 12:13:56 2001 +0200 (2001-10-08)
changeset 11706885e053ae664
parent 11705 ac8ca15c556c
child 11707 6c45813c2db1
*** empty log message ***
doc-src/TutorialI/Advanced/document/WFrec.tex
doc-src/TutorialI/CTL/document/CTL.tex
doc-src/TutorialI/CTL/document/CTLind.tex
doc-src/TutorialI/Datatype/document/Fundata.tex
doc-src/TutorialI/Recdef/document/examples.tex
doc-src/TutorialI/Recdef/document/simplification.tex
     1.1 --- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Mon Oct 08 12:13:34 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Mon Oct 08 12:13:56 2001 +0200
     1.3 @@ -65,8 +65,8 @@
     1.4  of a recursive function that calls itself with increasing values up to ten:%
     1.5  \end{isamarkuptext}%
     1.6  \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
     1.7 -\isacommand{recdef}\ f\ {\isachardoublequote}{\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}{\isacharhash}{\isadigit{1}}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}\isanewline
     1.8 -{\isachardoublequote}f\ i\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharhash}{\isadigit{1}}{\isadigit{0}}\ {\isasymle}\ i\ then\ {\isadigit{0}}\ else\ i\ {\isacharasterisk}\ f{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
     1.9 +\isacommand{recdef}\ f\ {\isachardoublequote}{\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}\isanewline
    1.10 +{\isachardoublequote}f\ i\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{1}}{\isadigit{0}}\ {\isasymle}\ i\ then\ {\isadigit{0}}\ else\ i\ {\isacharasterisk}\ f{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
    1.11  \begin{isamarkuptext}%
    1.12  \noindent
    1.13  Since \isacommand{recdef} is not prepared for the relation supplied above,
    1.14 @@ -108,7 +108,7 @@
    1.15  {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}%
    1.16  \begin{isamarkuptext}%
    1.17  \noindent
    1.18 -Alternatively, we could have given \isa{measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isacharhash}{\isadigit{1}}{\isadigit{0}}{\isacharminus}k{\isacharparenright}} for the
    1.19 +Alternatively, we could have given \isa{measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isadigit{1}}{\isadigit{0}}{\isacharminus}k{\isacharparenright}} for the
    1.20  well-founded relation in our \isacommand{recdef}.  However, the arithmetic
    1.21  goal in the lemma above would have arisen instead in the \isacommand{recdef}
    1.22  termination proof, where we have less control.  A tailor-made termination
     2.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Mon Oct 08 12:13:34 2001 +0200
     2.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Mon Oct 08 12:13:56 2001 +0200
     2.3 @@ -83,24 +83,24 @@
     2.4  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ }{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
     2.5  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
     2.6  \end{isabelle}
     2.7 -Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:%
     2.8 +Now we eliminate the disjunction. The case \isa{p\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ A} is trivial:%
     2.9  \end{isamarkuptxt}%
    2.10  \isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
    2.11  \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}%
    2.12  \begin{isamarkuptxt}%
    2.13  \noindent
    2.14 -In the other case we set \isa{t} to \isa{p\ {\isadigit{1}}} and simplify matters:%
    2.15 +In the other case we set \isa{t} to \isa{p\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}b{\isacharparenright}} and simplify matters:%
    2.16  \end{isamarkuptxt}%
    2.17  \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
    2.18  \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
    2.19  \begin{isamarkuptxt}%
    2.20  \begin{isabelle}%
    2.21  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline
    2.22 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ }{\isasymforall}pa{\isachardot}\ p\ {\isadigit{1}}{\isacharprime}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
    2.23 +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ }{\isasymforall}pa{\isachardot}\ p\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
    2.24  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ {\isasymforall}pa{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
    2.25  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
    2.26  \end{isabelle}
    2.27 -It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, that is, 
    2.28 +It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}}, that is, 
    2.29  \isa{p} without its first element.  The rest is automatic:%
    2.30  \end{isamarkuptxt}%
    2.31  \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
    2.32 @@ -139,7 +139,7 @@
    2.33  {\isachardoublequote}path\ s\ Q\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ Q\ n{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isachardoublequote}%
    2.34  \begin{isamarkuptext}%
    2.35  \noindent
    2.36 -Element \isa{n\ {\isacharplus}\ {\isadigit{1}}} on this path is some arbitrary successor
    2.37 +Element \isa{n\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}} on this path is some arbitrary successor
    2.38  \isa{t} of element \isa{n} such that \isa{Q\ t} holds.  Remember that \isa{SOME\ t{\isachardot}\ R\ t}
    2.39  is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec:SOME}). Of
    2.40  course, such a \isa{t} need not exist, but that is of no
    2.41 @@ -157,7 +157,7 @@
    2.42  First we rephrase the conclusion slightly because we need to prove simultaneously
    2.43  both the path property and the fact that \isa{Q} holds:%
    2.44  \end{isamarkuptxt}%
    2.45 -\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%
    2.46 +\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%
    2.47  \begin{isamarkuptxt}%
    2.48  \noindent
    2.49  From this proposition the original goal follows easily:%
     3.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex	Mon Oct 08 12:13:34 2001 +0200
     3.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Mon Oct 08 12:13:56 2001 +0200
     3.3 @@ -32,10 +32,10 @@
     3.4  \ \ \ \ \ \ \ {\isachardoublequote}{\isasymlbrakk}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\ t\ {\isasymnotin}\ A{\isacharsemicolon}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}\ {\isasymin}\ M\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ u\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}%
     3.5  \begin{isamarkuptext}%
     3.6  It is easy to see that for any infinite \isa{A}-avoiding path \isa{f}
     3.7 -with \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
     3.8 +with \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
     3.9  starting with \isa{s} because (by definition of \isa{Avoid}) there is a
    3.10 -finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}.
    3.11 -The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A}. However,
    3.12 +finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}b{\isacharparenright}}.
    3.13 +The proof is by induction on \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A}. However,
    3.14  this requires the following
    3.15  reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
    3.16  the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.%
     4.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Oct 08 12:13:34 2001 +0200
     4.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Oct 08 12:13:56 2001 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4  has as many subtrees as there are natural numbers. How can we possibly
     4.5  write down such a tree? Using functional notation! For example, the term
     4.6  \begin{isabelle}%
     4.7 -\ \ \ \ \ Br\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
     4.8 +\ \ \ \ \ Br\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
     4.9  \end{isabelle}
    4.10  of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
    4.11  root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
     5.1 --- a/doc-src/TutorialI/Recdef/document/examples.tex	Mon Oct 08 12:13:34 2001 +0200
     5.2 +++ b/doc-src/TutorialI/Recdef/document/examples.tex	Mon Oct 08 12:13:56 2001 +0200
     5.3 @@ -8,7 +8,7 @@
     5.4  \isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
     5.5  \isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
     5.6  \ \ {\isachardoublequote}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
     5.7 -\ \ {\isachardoublequote}fib\ {\isadigit{1}}{\isacharprime}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
     5.8 +\ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
     5.9  \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}%
    5.10  \begin{isamarkuptext}%
    5.11  \noindent
     6.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Oct 08 12:13:34 2001 +0200
     6.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Oct 08 12:13:56 2001 +0200
     6.3 @@ -19,7 +19,7 @@
     6.4  According to the measure function, the second argument should decrease with
     6.5  each recursive call. The resulting termination condition
     6.6  \begin{isabelle}%
     6.7 -\ \ \ \ \ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
     6.8 +\ \ \ \ \ n\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
     6.9  \end{isabelle}
    6.10  is proved automatically because it is already present as a lemma in
    6.11  HOL\@.  Thus the recursion equation becomes a simplification
    6.12 @@ -63,7 +63,7 @@
    6.13  \begin{isamarkuptext}%
    6.14  \noindent
    6.15  The order of equations is important: it hides the side condition
    6.16 -\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}.  Unfortunately, in general the case distinction
    6.17 +\isa{n\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}}.  Unfortunately, in general the case distinction
    6.18  may not be expressible by pattern matching.
    6.19  
    6.20  A simple alternative is to replace \isa{if} by \isa{case},