1.1 --- a/doc-src/TutorialI/Advanced/ROOT.ML Wed Oct 11 09:09:06 2000 +0200
1.2 +++ b/doc-src/TutorialI/Advanced/ROOT.ML Wed Oct 11 10:44:42 2000 +0200
1.3 @@ -1,2 +1,3 @@
1.4 use "../settings.ML";
1.5 use_thy "simp";
1.6 +use_thy "WFrec";
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Wed Oct 11 10:44:42 2000 +0200
2.3 @@ -0,0 +1,46 @@
2.4 +(*<*)theory WFrec = Main:(*>*)
2.5 +
2.6 +text{*\noindent
2.7 +So far, all recursive definitions where shown to terminate via measure
2.8 +functions. Sometimes this can be quite inconvenient or even
2.9 +impossible. Fortunately, \isacommand{recdef} supports much more
2.10 +general definitions. For example, termination of Ackermann's function
2.11 +can be shown by means of the lexicographic product @{text"<*lex*>"}:
2.12 +*}
2.13 +
2.14 +consts ack :: "nat\<times>nat \<Rightarrow> nat";
2.15 +recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"
2.16 + "ack(0,n) = Suc n"
2.17 + "ack(Suc m,0) = ack(m, 1)"
2.18 + "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";
2.19 +
2.20 +text{*\noindent
2.21 +The lexicographic product decreases if either its first component
2.22 +decreases (as in the second equation and in the outer call in the
2.23 +third equation) or its first component stays the same and the second
2.24 +component decreases (as in the inner call in the third equation).
2.25 +
2.26 +In general, \isacommand{recdef} supports termination proofs based on
2.27 +arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded
2.28 +recursion}\indexbold{recursion!wellfounded}\index{wellfounded
2.29 +recursion|see{recursion, wellfounded}}. A relation $<$ is
2.30 +\bfindex{wellfounded} if it has no infinite descending chain $\cdots <
2.31 +a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
2.32 +of all pairs $(r,l)$, where $l$ is the argument on the left-hand side of an equation
2.33 +and $r$ the argument of some recursive call on the corresponding
2.34 +right-hand side, induces a wellfounded relation. For a systematic
2.35 +account of termination proofs via wellfounded relations see, for
2.36 +example, \cite{Baader-Nipkow}.
2.37 +
2.38 +Each \isacommand{recdef} definition should be accompanied (after the
2.39 +name of the function) by a wellfounded relation on the argument type
2.40 +of the function. For example, @{term measure} is defined by
2.41 +@{prop[display]"measure(f::'a \<Rightarrow> nat) \<equiv> {(y,x). f y < f x}"}
2.42 +and it has been proved that @{term"measure f"} is always wellfounded.
2.43 +
2.44 +In addition to @{term measure}, the library provides
2.45 +a number of further constructions for obtaining wellfounded relations.
2.46 +
2.47 +wf proof auto if stndard constructions.
2.48 +*}
2.49 +(*<*)end(*>*)
2.50 \ No newline at end of file
3.1 --- a/doc-src/TutorialI/Advanced/advanced.tex Wed Oct 11 09:09:06 2000 +0200
3.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex Wed Oct 11 10:44:42 2000 +0200
3.3 @@ -14,6 +14,10 @@
3.4 \section{Advanced forms of recursion}
3.5 \index{*recdef|(}
3.6
3.7 +The purpose of this section is to introduce advanced forms of \isacommand{recdef}. It
3.8 +covers two topics: how to define recursive function over nested recursive datatypes
3.9 +and how to establish termination by means other than measure functions.
3.10 +
3.11 \subsection{Recursion over nested datatypes}
3.12 \label{sec:nested-recdef}
3.13 \input{Recdef/document/Nested0.tex}
3.14 @@ -23,7 +27,7 @@
3.15
3.16 \subsection{Beyond measure}
3.17 \label{sec:wellfounded}
3.18 -\input{Recdef/document/WFrec.tex}
3.19 +\input{Advanced/document/WFrec.tex}
3.20
3.21 \section{Advanced induction techniques}
3.22 \label{sec:advanced-ind}
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Wed Oct 11 10:44:42 2000 +0200
4.3 @@ -0,0 +1,54 @@
4.4 +%
4.5 +\begin{isabellebody}%
4.6 +\def\isabellecontext{WFrec}%
4.7 +%
4.8 +\begin{isamarkuptext}%
4.9 +\noindent
4.10 +So far, all recursive definitions where shown to terminate via measure
4.11 +functions. Sometimes this can be quite inconvenient or even
4.12 +impossible. Fortunately, \isacommand{recdef} supports much more
4.13 +general definitions. For example, termination of Ackermann's function
4.14 +can be shown by means of the lexicographic product \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:%
4.15 +\end{isamarkuptext}%
4.16 +\isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
4.17 +\isacommand{recdef}\ ack\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
4.18 +\ \ {\isachardoublequote}ack{\isacharparenleft}{\isadigit{0}}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline
4.19 +\ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
4.20 +\ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
4.21 +\begin{isamarkuptext}%
4.22 +\noindent
4.23 +The lexicographic product decreases if either its first component
4.24 +decreases (as in the second equation and in the outer call in the
4.25 +third equation) or its first component stays the same and the second
4.26 +component decreases (as in the inner call in the third equation).
4.27 +
4.28 +In general, \isacommand{recdef} supports termination proofs based on
4.29 +arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded
4.30 +recursion}\indexbold{recursion!wellfounded}\index{wellfounded
4.31 +recursion|see{recursion, wellfounded}}. A relation $<$ is
4.32 +\bfindex{wellfounded} if it has no infinite descending chain $\cdots <
4.33 +a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
4.34 +of all pairs $(r,l)$, where $l$ is the argument on the left-hand side of an equation
4.35 +and $r$ the argument of some recursive call on the corresponding
4.36 +right-hand side, induces a wellfounded relation. For a systematic
4.37 +account of termination proofs via wellfounded relations see, for
4.38 +example, \cite{Baader-Nipkow}.
4.39 +
4.40 +Each \isacommand{recdef} definition should be accompanied (after the
4.41 +name of the function) by a wellfounded relation on the argument type
4.42 +of the function. For example, \isa{measure} is defined by
4.43 +\begin{isabelle}%
4.44 +\ \ \ \ \ measure\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ f\ y\ {\isacharless}\ f\ x{\isacharbraceright}%
4.45 +\end{isabelle}
4.46 +and it has been proved that \isa{measure\ f} is always wellfounded.
4.47 +
4.48 +In addition to \isa{measure}, the library provides
4.49 +a number of further constructions for obtaining wellfounded relations.
4.50 +
4.51 +wf proof auto if stndard constructions.%
4.52 +\end{isamarkuptext}%
4.53 +\end{isabellebody}%
4.54 +%%% Local Variables:
4.55 +%%% mode: latex
4.56 +%%% TeX-master: "root"
4.57 +%%% End:
5.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex Wed Oct 11 09:09:06 2000 +0200
5.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed Oct 11 10:44:42 2000 +0200
5.3 @@ -18,7 +18,7 @@
5.4 in HOL: it is simply a function from \isa{nat} to \isa{state}.%
5.5 \end{isamarkuptext}%
5.6 \isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline
5.7 -\ \ \ \ \ \ \ \ \ {\isachardoublequote}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}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{\isacharparenright}{\isacharbraceright}{\isachardoublequote}%
5.8 +\ \ \ \ \ \ \ \ \ {\isachardoublequote}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}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{\isacharparenright}{\isacharbraceright}{\isachardoublequote}%
5.9 \begin{isamarkuptext}%
5.10 \noindent
5.11 This definition allows a very succinct statement of the semantics of \isa{AF}:
5.12 @@ -54,7 +54,7 @@
5.13 agree for \isa{AF}, i.e.\ that \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}. This time we prove the two containments separately, starting
5.14 with the easy one:%
5.15 \end{isamarkuptext}%
5.16 -\isacommand{theorem}\ AF{\isacharunderscore}lemma\isadigit{1}{\isacharcolon}\isanewline
5.17 +\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline
5.18 \ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}%
5.19 \begin{isamarkuptxt}%
5.20 \noindent
5.21 @@ -76,15 +76,15 @@
5.22 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
5.23 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
5.24 \end{isabelle}
5.25 -Now we eliminate the disjunction. The case \isa{p\ \isadigit{0}\ {\isasymin}\ A} is trivial:%
5.26 +Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:%
5.27 \end{isamarkuptxt}%
5.28 \isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
5.29 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}%
5.30 \begin{isamarkuptxt}%
5.31 \noindent
5.32 -In the other case we set \isa{t} to \isa{p\ \isadigit{1}} and simplify matters:%
5.33 +In the other case we set \isa{t} to \isa{p\ {\isadigit{1}}} and simplify matters:%
5.34 \end{isamarkuptxt}%
5.35 -\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ \isadigit{1}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
5.36 +\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
5.37 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
5.38 \begin{isamarkuptxt}%
5.39 \begin{isabelle}
5.40 @@ -93,10 +93,10 @@
5.41 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
5.42 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
5.43 \end{isabelle}
5.44 -It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ \isadigit{1}{\isacharparenright}}, i.e.\ \isa{p} without its
5.45 +It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, i.e.\ \isa{p} without its
5.46 first element. The rest is practically automatic:%
5.47 \end{isamarkuptxt}%
5.48 -\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
5.49 +\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
5.50 \isacommand{apply}\ simp\isanewline
5.51 \isacommand{apply}\ blast\isanewline
5.52 \isacommand{done}%
5.53 @@ -129,11 +129,11 @@
5.54 \end{isamarkuptext}%
5.55 \isacommand{consts}\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequote}\isanewline
5.56 \isacommand{primrec}\isanewline
5.57 -{\isachardoublequote}path\ s\ P\ \isadigit{0}\ {\isacharequal}\ s{\isachardoublequote}\isanewline
5.58 +{\isachardoublequote}path\ s\ P\ {\isadigit{0}}\ {\isacharequal}\ s{\isachardoublequote}\isanewline
5.59 {\isachardoublequote}path\ s\ P\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ n{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isachardoublequote}%
5.60 \begin{isamarkuptext}%
5.61 \noindent
5.62 -Element \isa{n\ {\isacharplus}\ \isadigit{1}} on this path is some arbitrary successor
5.63 +Element \isa{n\ {\isacharplus}\ {\isadigit{1}}} on this path is some arbitrary successor
5.64 \isa{t} of element \isa{n} such that \isa{P\ t} holds. Remember that \isa{SOME\ t{\isachardot}\ R\ t}
5.65 is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec-SOME}). Of
5.66 course, such a \isa{t} may in general not exist, but that is of no
5.67 @@ -151,7 +151,7 @@
5.68 First we rephrase the conclusion slightly because we need to prove both the path property
5.69 and the fact that \isa{P} holds simultaneously:%
5.70 \end{isamarkuptxt}%
5.71 -\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}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%
5.72 +\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}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%
5.73 \begin{isamarkuptxt}%
5.74 \noindent
5.75 From this proposition the original goal follows easily:%
5.76 @@ -184,7 +184,7 @@
5.77 \end{isabelle}
5.78 The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M}
5.79 holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
5.80 -is embodied in the theorem \isa{someI\isadigit{2}{\isacharunderscore}ex}:
5.81 +is embodied in the theorem \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:
5.82 \begin{isabelle}%
5.83 \ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}%
5.84 \end{isabelle}
5.85 @@ -194,11 +194,11 @@
5.86 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x\ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M}, which is trivial. Thus it is not surprising that
5.87 \isa{fast} can prove the base case quickly:%
5.88 \end{isamarkuptxt}%
5.89 -\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}%
5.90 +\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}%
5.91 \begin{isamarkuptxt}%
5.92 \noindent
5.93 What is worth noting here is that we have used \isa{fast} rather than \isa{blast}.
5.94 -The reason is that \isa{blast} would fail because it cannot cope with \isa{someI\isadigit{2}{\isacharunderscore}ex}:
5.95 +The reason is that \isa{blast} would fail because it cannot cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:
5.96 unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
5.97 variables. For efficiency reasons \isa{blast} does not even attempt such unifications.
5.98 Although \isa{fast} can in principle cope with complicated unification problems, in practice
5.99 @@ -209,9 +209,9 @@
5.100 \isa{SOME}. We merely show the proof commands but do not describe th details:%
5.101 \end{isamarkuptxt}%
5.102 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
5.103 -\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
5.104 +\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
5.105 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
5.106 -\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
5.107 +\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
5.108 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
5.109 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
5.110 \isacommand{done}%
5.111 @@ -230,17 +230,17 @@
5.112 \end{isamarkuptext}%
5.113 %
5.114 \begin{isamarkuptext}%
5.115 -At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma\isadigit{1}}:%
5.116 +At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma{\isadigit{1}}}:%
5.117 \end{isamarkuptext}%
5.118 -\isacommand{theorem}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharcolon}\isanewline
5.119 +\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\isanewline
5.120 {\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}%
5.121 \begin{isamarkuptxt}%
5.122 \noindent
5.123 -The proof is again pointwise and then by contraposition (\isa{contrapos\isadigit{2}} is the rule
5.124 +The proof is again pointwise and then by contraposition (\isa{contrapos{\isadigit{2}}} is the rule
5.125 \isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):%
5.126 \end{isamarkuptxt}%
5.127 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
5.128 -\isacommand{apply}{\isacharparenleft}erule\ contrapos\isadigit{2}{\isacharparenright}\isanewline
5.129 +\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isadigit{2}}{\isacharparenright}\isanewline
5.130 \isacommand{apply}\ simp%
5.131 \begin{isamarkuptxt}%
5.132 \begin{isabelle}
5.133 @@ -262,12 +262,12 @@
5.134 \isacommand{done}%
5.135 \begin{isamarkuptext}%
5.136 The main theorem is proved as for PDL, except that we also derive the necessary equality
5.137 -\isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining \isa{AF{\isacharunderscore}lemma\isadigit{1}} and \isa{AF{\isacharunderscore}lemma\isadigit{2}}
5.138 +\isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining \isa{AF{\isacharunderscore}lemma{\isadigit{1}}} and \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}
5.139 on the spot:%
5.140 \end{isamarkuptext}%
5.141 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
5.142 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
5.143 -\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma\isadigit{1}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharbrackright}{\isacharparenright}\isanewline
5.144 +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma{\isadigit{1}}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharbrackright}{\isacharparenright}\isanewline
5.145 \isacommand{done}%
5.146 \begin{isamarkuptext}%
5.147 The above language is not quite CTL. The latter also includes an
5.148 @@ -281,7 +281,7 @@
5.149 \end{isabelle}
5.150 and model checking algorithm
5.151 \begin{isabelle}%
5.152 -\ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isacharparenright}%
5.153 +\ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isacharparenright}%
5.154 \end{isabelle}
5.155 Prove the equivalence between semantics and model checking, i.e.\ that
5.156 \begin{isabelle}%
6.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex Wed Oct 11 09:09:06 2000 +0200
6.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Wed Oct 11 10:44:42 2000 +0200
6.3 @@ -25,7 +25,7 @@
6.4 The meaning of these formulae is given by saying which formula is true in
6.5 which state:%
6.6 \end{isamarkuptext}%
6.7 -\isacommand{consts}\ valid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ formula\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}\ {\isasymTurnstile}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}\isadigit{8}\isadigit{0}{\isacharcomma}\isadigit{8}\isadigit{0}{\isacharbrackright}\ \isadigit{8}\isadigit{0}{\isacharparenright}%
6.8 +\isacommand{consts}\ valid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ formula\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}\ {\isasymTurnstile}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{0}}{\isacharcomma}{\isadigit{8}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}%
6.9 \begin{isamarkuptext}%
6.10 \noindent
6.11 The concrete syntax annotation allows us to write \isa{s\ {\isasymTurnstile}\ f} instead of
6.12 @@ -57,14 +57,14 @@
6.13 {\isachardoublequote}mc{\isacharparenleft}Neg\ f{\isacharparenright}\ \ \ {\isacharequal}\ {\isacharminus}mc\ f{\isachardoublequote}\isanewline
6.14 {\isachardoublequote}mc{\isacharparenleft}And\ f\ g{\isacharparenright}\ {\isacharequal}\ mc\ f\ {\isasyminter}\ mc\ g{\isachardoublequote}\isanewline
6.15 {\isachardoublequote}mc{\isacharparenleft}AX\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ \ {\isasymlongrightarrow}\ t\ {\isasymin}\ mc\ f{\isacharbraceright}{\isachardoublequote}\isanewline
6.16 -{\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isachardoublequote}%
6.17 +{\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isachardoublequote}%
6.18 \begin{isamarkuptext}%
6.19 \noindent
6.20 Only the equation for \isa{EF} deserves some comments. Remember that the
6.21 -postfix \isa{{\isacharcircum}{\isacharminus}\isadigit{1}} and the infix \isa{{\isacharcircum}{\isacharcircum}} are predefined and denote the
6.22 +postfix \isa{{\isacharcircum}{\isacharminus}{\isadigit{1}}} and the infix \isa{{\isacharcircum}{\isacharcircum}} are predefined and denote the
6.23 converse of a relation and the application of a relation to a set. Thus
6.24 -\isa{M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T} is the set of all predecessors of \isa{T} and the least
6.25 -fixpoint (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T} is the least set
6.26 +\isa{M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the set of all predecessors of \isa{T} and the least
6.27 +fixpoint (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the least set
6.28 \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
6.29 find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from
6.30 which there is a path to a state where \isa{f} is true, do not worry---that
6.31 @@ -72,7 +72,7 @@
6.32
6.33 First we prove monotonicity of the function inside \isa{lfp}%
6.34 \end{isamarkuptext}%
6.35 -\isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isachardoublequote}\isanewline
6.36 +\isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isachardoublequote}\isanewline
6.37 \isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline
6.38 \isacommand{apply}\ blast\isanewline
6.39 \isacommand{done}%
6.40 @@ -84,7 +84,7 @@
6.41 a separate lemma:%
6.42 \end{isamarkuptext}%
6.43 \isacommand{lemma}\ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline
6.44 -\ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}%
6.45 +\ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}%
6.46 \begin{isamarkuptxt}%
6.47 \noindent
6.48 The equality is proved in the canonical fashion by proving that each set
7.1 --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed Oct 11 09:09:06 2000 +0200
7.2 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed Oct 11 10:44:42 2000 +0200
7.3 @@ -30,7 +30,7 @@
7.4 \isacommand{primrec}\isanewline
7.5 {\isachardoublequote}value\ {\isacharparenleft}Cex\ v{\isacharparenright}\ env\ {\isacharequal}\ v{\isachardoublequote}\isanewline
7.6 {\isachardoublequote}value\ {\isacharparenleft}Vex\ a{\isacharparenright}\ env\ {\isacharequal}\ env\ a{\isachardoublequote}\isanewline
7.7 -{\isachardoublequote}value\ {\isacharparenleft}Bex\ f\ e\isadigit{1}\ e\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ f\ {\isacharparenleft}value\ e\isadigit{1}\ env{\isacharparenright}\ {\isacharparenleft}value\ e\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}%
7.8 +{\isachardoublequote}value\ {\isacharparenleft}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ f\ {\isacharparenleft}value\ e{\isadigit{1}}\ env{\isacharparenright}\ {\isacharparenleft}value\ e{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequote}%
7.9 \begin{isamarkuptext}%
7.10 The stack machine has three instructions: load a constant value onto the
7.11 stack, load the contents of a certain address onto the stack, and apply a
7.12 @@ -72,7 +72,7 @@
7.13 \isacommand{primrec}\isanewline
7.14 {\isachardoublequote}comp\ {\isacharparenleft}Cex\ v{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Const\ v{\isacharbrackright}{\isachardoublequote}\isanewline
7.15 {\isachardoublequote}comp\ {\isacharparenleft}Vex\ a{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Load\ a{\isacharbrackright}{\isachardoublequote}\isanewline
7.16 -{\isachardoublequote}comp\ {\isacharparenleft}Bex\ f\ e\isadigit{1}\ e\isadigit{2}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}comp\ e\isadigit{2}{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}comp\ e\isadigit{1}{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}Apply\ f{\isacharbrackright}{\isachardoublequote}%
7.17 +{\isachardoublequote}comp\ {\isacharparenleft}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}comp\ e{\isadigit{2}}{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}comp\ e{\isadigit{1}}{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}Apply\ f{\isacharbrackright}{\isachardoublequote}%
7.18 \begin{isamarkuptext}%
7.19 Now we have to prove the correctness of the compiler, i.e.\ that the
7.20 execution of a compiled expression results in the value of the expression:%
8.1 --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Wed Oct 11 09:09:06 2000 +0200
8.2 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Wed Oct 11 10:44:42 2000 +0200
8.3 @@ -42,15 +42,15 @@
8.4 section:%
8.5 \end{isamarkuptext}%
8.6 \isacommand{primrec}\isanewline
8.7 -\ \ {\isachardoublequote}evala\ {\isacharparenleft}IF\ b\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\isanewline
8.8 -\ \ \ \ \ {\isacharparenleft}if\ evalb\ b\ env\ then\ evala\ a\isadigit{1}\ env\ else\ evala\ a\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}\isanewline
8.9 -\ \ {\isachardoublequote}evala\ {\isacharparenleft}Sum\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a\isadigit{1}\ env\ {\isacharplus}\ evala\ a\isadigit{2}\ env{\isachardoublequote}\isanewline
8.10 -\ \ {\isachardoublequote}evala\ {\isacharparenleft}Diff\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a\isadigit{1}\ env\ {\isacharminus}\ evala\ a\isadigit{2}\ env{\isachardoublequote}\isanewline
8.11 +\ \ {\isachardoublequote}evala\ {\isacharparenleft}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\isanewline
8.12 +\ \ \ \ \ {\isacharparenleft}if\ evalb\ b\ env\ then\ evala\ a{\isadigit{1}}\ env\ else\ evala\ a{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequote}\isanewline
8.13 +\ \ {\isachardoublequote}evala\ {\isacharparenleft}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a{\isadigit{1}}\ env\ {\isacharplus}\ evala\ a{\isadigit{2}}\ env{\isachardoublequote}\isanewline
8.14 +\ \ {\isachardoublequote}evala\ {\isacharparenleft}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a{\isadigit{1}}\ env\ {\isacharminus}\ evala\ a{\isadigit{2}}\ env{\isachardoublequote}\isanewline
8.15 \ \ {\isachardoublequote}evala\ {\isacharparenleft}Var\ v{\isacharparenright}\ env\ {\isacharequal}\ env\ v{\isachardoublequote}\isanewline
8.16 \ \ {\isachardoublequote}evala\ {\isacharparenleft}Num\ n{\isacharparenright}\ env\ {\isacharequal}\ n{\isachardoublequote}\isanewline
8.17 \isanewline
8.18 -\ \ {\isachardoublequote}evalb\ {\isacharparenleft}Less\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}evala\ a\isadigit{1}\ env\ {\isacharless}\ evala\ a\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}\isanewline
8.19 -\ \ {\isachardoublequote}evalb\ {\isacharparenleft}And\ b\isadigit{1}\ b\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}evalb\ b\isadigit{1}\ env\ {\isasymand}\ evalb\ b\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}\isanewline
8.20 +\ \ {\isachardoublequote}evalb\ {\isacharparenleft}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}evala\ a{\isadigit{1}}\ env\ {\isacharless}\ evala\ a{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequote}\isanewline
8.21 +\ \ {\isachardoublequote}evalb\ {\isacharparenleft}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}evalb\ b{\isadigit{1}}\ env\ {\isasymand}\ evalb\ b{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequote}\isanewline
8.22 \ \ {\isachardoublequote}evalb\ {\isacharparenleft}Neg\ b{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ evalb\ b\ env{\isacharparenright}{\isachardoublequote}%
8.23 \begin{isamarkuptext}%
8.24 \noindent
8.25 @@ -66,15 +66,15 @@
8.26 to \isa{{\isacharprime}b}. Note that there are only arithmetic and no boolean variables.%
8.27 \end{isamarkuptext}%
8.28 \isacommand{primrec}\isanewline
8.29 -\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}IF\ b\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\isanewline
8.30 -\ \ \ \ \ IF\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline
8.31 -\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Sum\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\ Sum\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline
8.32 -\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Diff\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\ Diff\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline
8.33 +\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\isanewline
8.34 +\ \ \ \ \ IF\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{2}}{\isacharparenright}{\isachardoublequote}\isanewline
8.35 +\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ Sum\ {\isacharparenleft}substa\ s\ a{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{2}}{\isacharparenright}{\isachardoublequote}\isanewline
8.36 +\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ Diff\ {\isacharparenleft}substa\ s\ a{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{2}}{\isacharparenright}{\isachardoublequote}\isanewline
8.37 \ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Var\ v{\isacharparenright}\ {\isacharequal}\ s\ v{\isachardoublequote}\isanewline
8.38 \ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Num\ n{\isacharparenright}\ {\isacharequal}\ Num\ n{\isachardoublequote}\isanewline
8.39 \isanewline
8.40 -\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}Less\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\ Less\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline
8.41 -\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}And\ b\isadigit{1}\ b\isadigit{2}{\isacharparenright}\ {\isacharequal}\ And\ {\isacharparenleft}substb\ s\ b\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substb\ s\ b\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline
8.42 +\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ Less\ {\isacharparenleft}substa\ s\ a{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{2}}{\isacharparenright}{\isachardoublequote}\isanewline
8.43 +\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ And\ {\isacharparenleft}substb\ s\ b{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substb\ s\ b{\isadigit{2}}{\isacharparenright}{\isachardoublequote}\isanewline
8.44 \ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}Neg\ b{\isacharparenright}\ {\isacharequal}\ Neg\ {\isacharparenleft}substb\ s\ b{\isacharparenright}{\isachardoublequote}%
8.45 \begin{isamarkuptext}%
8.46 Now we can prove a fundamental theorem about the interaction between
9.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Wed Oct 11 09:09:06 2000 +0200
9.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Wed Oct 11 10:44:42 2000 +0200
9.3 @@ -12,7 +12,7 @@
9.4 has as many subtrees as there are natural numbers. How can we possibly
9.5 write down such a tree? Using functional notation! For example, the term
9.6 \begin{isabelle}%
9.7 -\ \ \ \ \ Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
9.8 +\ \ \ \ \ Branch\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
9.9 \end{isabelle}
9.10 of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
9.11 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
10.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex Wed Oct 11 09:09:06 2000 +0200
10.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Wed Oct 11 10:44:42 2000 +0200
10.3 @@ -94,7 +94,7 @@
10.4 \ \ \ \ \ subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}%
10.5 \end{isabelle}
10.6 where \isa{map} is the standard list function such that
10.7 -\isa{map\ f\ {\isacharbrackleft}x\isadigit{1}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}xn{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}f\ x\isadigit{1}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}f\ xn{\isacharbrackright}}. This is true, but Isabelle
10.8 +\isa{map\ f\ {\isacharbrackleft}x{\isadigit{1}}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}xn{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}f\ x{\isadigit{1}}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}f\ xn{\isacharbrackright}}. This is true, but Isabelle
10.9 insists on the above fixed format. Fortunately, we can easily \emph{prove}
10.10 that the suggested equation holds:%
10.11 \end{isamarkuptext}%
11.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed Oct 11 09:09:06 2000 +0200
11.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed Oct 11 10:44:42 2000 +0200
11.3 @@ -26,7 +26,7 @@
11.4 \isa{Const\ False}. Variables are represented by terms of the form
11.5 \isa{Var\ n}, where \isa{n} is a natural number (type \isa{nat}).
11.6 For example, the formula $P@0 \land \neg P@1$ is represented by the term
11.7 -\isa{And\ {\isacharparenleft}Var\ \isadigit{0}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ \isadigit{1}{\isacharparenright}{\isacharparenright}}.
11.8 +\isa{And\ {\isacharparenleft}Var\ {\isadigit{0}}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}}.
11.9
11.10 \subsubsection{What is the value of a boolean expression?}
11.11
11.12 @@ -68,18 +68,18 @@
11.13 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
11.14 translate from \isa{boolex} into \isa{ifex}:%
11.15 \end{isamarkuptext}%
11.16 -\isacommand{consts}\ bool\isadigit{2}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline
11.17 +\isacommand{consts}\ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline
11.18 \isacommand{primrec}\isanewline
11.19 -{\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline
11.20 -{\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline
11.21 -{\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ {\isacharequal}\ IF\ {\isacharparenleft}bool\isadigit{2}if\ b{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}\ {\isacharparenleft}CIF\ True{\isacharparenright}{\isachardoublequote}\isanewline
11.22 -{\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ {\isacharequal}\ IF\ {\isacharparenleft}bool\isadigit{2}if\ b{\isacharparenright}\ {\isacharparenleft}bool\isadigit{2}if\ c{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}{\isachardoublequote}%
11.23 +{\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline
11.24 +{\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline
11.25 +{\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ {\isacharequal}\ IF\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}\ {\isacharparenleft}CIF\ True{\isacharparenright}{\isachardoublequote}\isanewline
11.26 +{\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ {\isacharequal}\ IF\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ {\isacharparenleft}bool{\isadigit{2}}if\ c{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}{\isachardoublequote}%
11.27 \begin{isamarkuptext}%
11.28 \noindent
11.29 -At last, we have something we can verify: that \isa{bool\isadigit{2}if} preserves the
11.30 +At last, we have something we can verify: that \isa{bool{\isadigit{2}}if} preserves the
11.31 value of its argument:%
11.32 \end{isamarkuptext}%
11.33 -\isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool\isadigit{2}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}%
11.34 +\isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}%
11.35 \begin{isamarkuptxt}%
11.36 \noindent
11.37 The proof is canonical:%
12.1 --- a/doc-src/TutorialI/IsaMakefile Wed Oct 11 09:09:06 2000 +0200
12.2 +++ b/doc-src/TutorialI/IsaMakefile Wed Oct 11 10:44:42 2000 +0200
12.3 @@ -89,7 +89,7 @@
12.4
12.5 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \
12.6 Recdef/simplification.thy Recdef/Induction.thy \
12.7 - Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy Recdef/WFrec.thy
12.8 + Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy
12.9 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef
12.10 @rm -f tutorial.dvi
12.11
12.12 @@ -98,7 +98,7 @@
12.13
12.14 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
12.15
12.16 -$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML
12.17 +$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy
12.18 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Advanced
12.19 @rm -f tutorial.dvi
12.20
13.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Oct 11 09:09:06 2000 +0200
13.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Oct 11 10:44:42 2000 +0200
13.3 @@ -154,7 +154,7 @@
13.4 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
13.5 \end{isabelle}
13.6 After stripping the \isa{{\isasymforall}i}, the proof continues with a case
13.7 -distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ \isadigit{0}} is trivial and we focus on
13.8 +distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on
13.9 the other case:
13.10 \begin{isabelle}
13.11 \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline
14.1 --- a/doc-src/TutorialI/Misc/document/Tree2.tex Wed Oct 11 09:09:06 2000 +0200
14.2 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex Wed Oct 11 10:44:42 2000 +0200
14.3 @@ -9,11 +9,11 @@
14.4 quadratic. A linear time version of \isa{flatten} again reqires an extra
14.5 argument, the accumulator:%
14.6 \end{isamarkuptext}%
14.7 -\isacommand{consts}\ flatten\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}%
14.8 +\isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}%
14.9 \begin{isamarkuptext}%
14.10 -\noindent Define \isa{flatten\isadigit{2}} and prove%
14.11 +\noindent Define \isa{flatten{\isadigit{2}}} and prove%
14.12 \end{isamarkuptext}%
14.13 -\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}%
14.14 +\isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}%
14.15 %%% Local Variables:
14.16 %%% mode: latex
14.17 %%% TeX-master: "root"
15.1 --- a/doc-src/TutorialI/Misc/document/arith1.tex Wed Oct 11 09:09:06 2000 +0200
15.2 +++ b/doc-src/TutorialI/Misc/document/arith1.tex Wed Oct 11 10:44:42 2000 +0200
15.3 @@ -1,7 +1,7 @@
15.4 %
15.5 \begin{isabellebody}%
15.6 \def\isabellecontext{arith1}%
15.7 -\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
15.8 +\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
15.9 \end{isabellebody}%
15.10 %%% Local Variables:
15.11 %%% mode: latex
16.1 --- a/doc-src/TutorialI/Misc/document/arith3.tex Wed Oct 11 09:09:06 2000 +0200
16.2 +++ b/doc-src/TutorialI/Misc/document/arith3.tex Wed Oct 11 10:44:42 2000 +0200
16.3 @@ -1,7 +1,7 @@
16.4 %
16.5 \begin{isabellebody}%
16.6 \def\isabellecontext{arith3}%
16.7 -\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}\isadigit{0}\ {\isasymor}\ n{\isacharequal}\isadigit{1}{\isachardoublequote}\isanewline
16.8 +\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isanewline
16.9 \end{isabellebody}%
16.10 %%% Local Variables:
16.11 %%% mode: latex
17.1 --- a/doc-src/TutorialI/Misc/document/case_exprs.tex Wed Oct 11 09:09:06 2000 +0200
17.2 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Wed Oct 11 10:44:42 2000 +0200
17.3 @@ -9,9 +9,9 @@
17.4 HOL also features \isaindexbold{case}-expressions for analyzing
17.5 elements of a datatype. For example,
17.6 \begin{isabelle}%
17.7 -\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
17.8 +\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
17.9 \end{isabelle}
17.10 -evaluates to \isa{\isadigit{1}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if
17.11 +evaluates to \isa{{\isadigit{1}}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if
17.12 \isa{xs} is \isa{y\ {\isacharhash}\ ys}. (Since the result in both branches must be of
17.13 the same type, it follows that \isa{y} is of type \isa{nat} and hence
17.14 that \isa{xs} is of type \isa{nat\ list}.)
17.15 @@ -36,11 +36,11 @@
17.16 Nested patterns can be simulated by nested \isa{case}-expressions: instead
17.17 of
17.18 \begin{isabelle}%
17.19 -\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ \isadigit{1}\ {\isacharbar}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ x\ {\isacharbar}\ x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}\ {\isacharequal}{\isachargreater}\ y%
17.20 +\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ {\isadigit{1}}\ {\isacharbar}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ x\ {\isacharbar}\ x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}\ {\isacharequal}{\isachargreater}\ y%
17.21 \end{isabelle}
17.22 write
17.23 \begin{isabelle}%
17.24 -\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\isanewline
17.25 +\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\isanewline
17.26 \ \ \ \ \ {\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y%
17.27 \end{isabelle}
17.28
18.1 --- a/doc-src/TutorialI/Misc/document/fakenat.tex Wed Oct 11 09:09:06 2000 +0200
18.2 +++ b/doc-src/TutorialI/Misc/document/fakenat.tex Wed Oct 11 10:44:42 2000 +0200
18.3 @@ -7,7 +7,7 @@
18.4 The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural
18.5 numbers is predefined and behaves like%
18.6 \end{isamarkuptext}%
18.7 -\isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabellebody}%
18.8 +\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat\end{isabellebody}%
18.9 %%% Local Variables:
18.10 %%% mode: latex
18.11 %%% TeX-master: "root"
19.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex Wed Oct 11 09:09:06 2000 +0200
19.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed Oct 11 10:44:42 2000 +0200
19.3 @@ -6,12 +6,12 @@
19.4 \noindent
19.5 In particular, there are \isa{case}-expressions, for example
19.6 \begin{isabelle}%
19.7 -\ \ \ \ \ case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
19.8 +\ \ \ \ \ case\ n\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
19.9 \end{isabelle}
19.10 primitive recursion, for example%
19.11 \end{isamarkuptext}%
19.12 \isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
19.13 -\isacommand{primrec}\ {\isachardoublequote}sum\ \isadigit{0}\ {\isacharequal}\ \isadigit{0}{\isachardoublequote}\isanewline
19.14 +\isacommand{primrec}\ {\isachardoublequote}sum\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
19.15 \ \ \ \ \ \ \ \ {\isachardoublequote}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequote}%
19.16 \begin{isamarkuptext}%
19.17 \noindent
20.1 --- a/doc-src/TutorialI/Misc/document/pairs.tex Wed Oct 11 09:09:06 2000 +0200
20.2 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Wed Oct 11 10:44:42 2000 +0200
20.3 @@ -19,7 +19,7 @@
20.4 most variable binding constructs. Typical examples are
20.5 \begin{quote}
20.6 \isa{let\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ f\ z\ in\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}}\\
20.7 -\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}
20.8 +\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}
20.9 \end{quote}
20.10 Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).%
20.11 \end{isamarkuptext}%
21.1 --- a/doc-src/TutorialI/Misc/document/prime_def.tex Wed Oct 11 09:09:06 2000 +0200
21.2 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex Wed Oct 11 10:44:42 2000 +0200
21.3 @@ -7,14 +7,14 @@
21.4 A common mistake when writing definitions is to introduce extra free
21.5 variables on the right-hand side as in the following fictitious definition:
21.6 \begin{isabelle}%
21.7 -\ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ \isadigit{1}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
21.8 +\ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ {\isadigit{1}}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
21.9 \end{isabelle}
21.10 where \isa{dvd} means ``divides''.
21.11 Isabelle rejects this ``definition'' because of the extra \isa{m} on the
21.12 right-hand side, which would introduce an inconsistency (why?). What you
21.13 should have written is
21.14 \begin{isabelle}%
21.15 -\ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ \isadigit{1}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
21.16 +\ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ {\isadigit{1}}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
21.17 \end{isabelle}
21.18 \end{warn}%
21.19 \end{isamarkuptext}%
22.1 --- a/doc-src/TutorialI/Misc/document/simp.tex Wed Oct 11 09:09:06 2000 +0200
22.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex Wed Oct 11 10:44:42 2000 +0200
22.3 @@ -325,12 +325,12 @@
22.4 assumptions and conclusions that are (possibly negated) (in)equalities
22.5 (\isa{{\isacharequal}}, \isasymle, \isa{{\isacharless}}) and it only knows about addition. Thus%
22.6 \end{isamarkuptext}%
22.7 -\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
22.8 +\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
22.9 \begin{isamarkuptext}%
22.10 \noindent
22.11 is proved by simplification, whereas the only slightly more complex%
22.12 \end{isamarkuptext}%
22.13 -\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
22.14 +\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
22.15 \begin{isamarkuptext}%
22.16 \noindent
22.17 is not proved by simplification and requires \isa{arith}.%
23.1 --- a/doc-src/TutorialI/Misc/document/types.tex Wed Oct 11 09:09:06 2000 +0200
23.2 +++ b/doc-src/TutorialI/Misc/document/types.tex Wed Oct 11 10:44:42 2000 +0200
23.3 @@ -33,8 +33,8 @@
23.4 \end{isamarkuptext}%
23.5 \isacommand{constdefs}\ nor\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
23.6 \ \ \ \ \ \ \ \ \ {\isachardoublequote}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isanewline
23.7 -\ \ \ \ \ \ \ \ \ \ exor\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
23.8 -\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor\isadigit{2}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}%
23.9 +\ \ \ \ \ \ \ \ \ \ exor{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
23.10 +\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor{\isadigit{2}}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}%
23.11 \begin{isamarkuptext}%
23.12 \noindent\indexbold{*constdefs}%
23.13 in which case the default name of each definition is $f$\isa{{\isacharunderscore}def}, where
24.1 --- a/doc-src/TutorialI/Recdef/ROOT.ML Wed Oct 11 09:09:06 2000 +0200
24.2 +++ b/doc-src/TutorialI/Recdef/ROOT.ML Wed Oct 11 10:44:42 2000 +0200
24.3 @@ -3,4 +3,3 @@
24.4 use_thy "Induction";
24.5 use_thy "Nested1";
24.6 use_thy "Nested2";
24.7 -use_thy "WFrec";
25.1 --- a/doc-src/TutorialI/Recdef/document/examples.tex Wed Oct 11 09:09:06 2000 +0200
25.2 +++ b/doc-src/TutorialI/Recdef/document/examples.tex Wed Oct 11 10:44:42 2000 +0200
25.3 @@ -7,8 +7,8 @@
25.4 \end{isamarkuptext}%
25.5 \isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
25.6 \isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
25.7 -\ \ {\isachardoublequote}fib\ \isadigit{0}\ {\isacharequal}\ \isadigit{0}{\isachardoublequote}\isanewline
25.8 -\ \ {\isachardoublequote}fib\ \isadigit{1}\ {\isacharequal}\ \isadigit{1}{\isachardoublequote}\isanewline
25.9 +\ \ {\isachardoublequote}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
25.10 +\ \ {\isachardoublequote}fib\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
25.11 \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}%
25.12 \begin{isamarkuptext}%
25.13 \noindent
25.14 @@ -44,14 +44,14 @@
25.15 Overlapping patterns are disambiguated by taking the order of equations into
25.16 account, just as in functional programming:%
25.17 \end{isamarkuptext}%
25.18 -\isacommand{consts}\ sep\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
25.19 -\isacommand{recdef}\ sep\isadigit{1}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
25.20 -\ \ {\isachardoublequote}sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}\isanewline
25.21 -\ \ {\isachardoublequote}sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}%
25.22 +\isacommand{consts}\ sep{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
25.23 +\isacommand{recdef}\ sep{\isadigit{1}}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
25.24 +\ \ {\isachardoublequote}sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}\isanewline
25.25 +\ \ {\isachardoublequote}sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}%
25.26 \begin{isamarkuptext}%
25.27 \noindent
25.28 This defines exactly the same function as \isa{sep} above, i.e.\
25.29 -\isa{sep\isadigit{1}\ {\isacharequal}\ sep}.
25.30 +\isa{sep{\isadigit{1}}\ {\isacharequal}\ sep}.
25.31
25.32 \begin{warn}
25.33 \isacommand{recdef} only takes the first argument of a (curried)
25.34 @@ -62,18 +62,18 @@
25.35 arguments as in the following definition:
25.36 \end{warn}%
25.37 \end{isamarkuptext}%
25.38 -\isacommand{consts}\ sep\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
25.39 -\isacommand{recdef}\ sep\isadigit{2}\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
25.40 -\ \ {\isachardoublequote}sep\isadigit{2}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\isadigit{2}\ zs\ a{\isacharparenright}{\isachardoublequote}\isanewline
25.41 -\ \ {\isachardoublequote}sep\isadigit{2}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}%
25.42 +\isacommand{consts}\ sep{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
25.43 +\isacommand{recdef}\ sep{\isadigit{2}}\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
25.44 +\ \ {\isachardoublequote}sep{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{2}}\ zs\ a{\isacharparenright}{\isachardoublequote}\isanewline
25.45 +\ \ {\isachardoublequote}sep{\isadigit{2}}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}%
25.46 \begin{isamarkuptext}%
25.47 Because of its pattern-matching syntax, \isacommand{recdef} is also useful
25.48 for the definition of non-recursive functions:%
25.49 \end{isamarkuptext}%
25.50 -\isacommand{consts}\ swap\isadigit{1}\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
25.51 -\isacommand{recdef}\ swap\isadigit{1}\isadigit{2}\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline
25.52 -\ \ {\isachardoublequote}swap\isadigit{1}\isadigit{2}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequote}\isanewline
25.53 -\ \ {\isachardoublequote}swap\isadigit{1}\isadigit{2}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}%
25.54 +\isacommand{consts}\ swap{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
25.55 +\isacommand{recdef}\ swap{\isadigit{1}}{\isadigit{2}}\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline
25.56 +\ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequote}\isanewline
25.57 +\ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}%
25.58 \begin{isamarkuptext}%
25.59 \noindent
25.60 For non-recursive functions the termination measure degenerates to the empty
26.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex Wed Oct 11 09:09:06 2000 +0200
26.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Wed Oct 11 10:44:42 2000 +0200
26.3 @@ -12,13 +12,13 @@
26.4 \end{isamarkuptext}%
26.5 \isacommand{consts}\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
26.6 \isacommand{recdef}\ gcd\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
26.7 -\ \ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n{\isacharequal}\isadigit{0}\ then\ m\ else\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
26.8 +\ \ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n{\isacharequal}{\isadigit{0}}\ then\ m\ else\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
26.9 \begin{isamarkuptext}%
26.10 \noindent
26.11 According to the measure function, the second argument should decrease with
26.12 each recursive call. The resulting termination condition
26.13 \begin{isabelle}%
26.14 -\ \ \ \ \ n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
26.15 +\ \ \ \ \ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
26.16 \end{isabelle}
26.17 is provded automatically because it is already present as a lemma in the
26.18 arithmetic library. Thus the recursion equation becomes a simplification
26.19 @@ -33,11 +33,11 @@
26.20 \end{isabelle}
26.21 in one step to
26.22 \begin{isabelle}%
26.23 -\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ \isadigit{0}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
26.24 +\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
26.25 \end{isabelle}
26.26 where the condition cannot be reduced further, and splitting leads to
26.27 \begin{isabelle}%
26.28 -\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ \isadigit{0}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
26.29 +\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
26.30 \end{isabelle}
26.31 Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
26.32 an \isa{if}, it is unfolded again, which leads to an infinite chain of
26.33 @@ -54,22 +54,22 @@
26.34 rather than \isa{if} on the right. In the case of \isa{gcd} the
26.35 following alternative definition suggests itself:%
26.36 \end{isamarkuptext}%
26.37 -\isacommand{consts}\ gcd\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
26.38 -\isacommand{recdef}\ gcd\isadigit{1}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
26.39 -\ \ {\isachardoublequote}gcd\isadigit{1}\ {\isacharparenleft}m{\isacharcomma}\ \isadigit{0}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
26.40 -\ \ {\isachardoublequote}gcd\isadigit{1}\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd\isadigit{1}{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}%
26.41 +\isacommand{consts}\ gcd{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
26.42 +\isacommand{recdef}\ gcd{\isadigit{1}}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
26.43 +\ \ {\isachardoublequote}gcd{\isadigit{1}}\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
26.44 +\ \ {\isachardoublequote}gcd{\isadigit{1}}\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isadigit{1}}{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}%
26.45 \begin{isamarkuptext}%
26.46 \noindent
26.47 Note that the order of equations is important and hides the side condition
26.48 -\isa{n\ {\isasymnoteq}\ \isadigit{0}}. Unfortunately, in general the case distinction
26.49 +\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}. Unfortunately, in general the case distinction
26.50 may not be expressible by pattern matching.
26.51
26.52 A very simple alternative is to replace \isa{if} by \isa{case}, which
26.53 is also available for \isa{bool} but is not split automatically:%
26.54 \end{isamarkuptext}%
26.55 -\isacommand{consts}\ gcd\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
26.56 -\isacommand{recdef}\ gcd\isadigit{2}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
26.57 -\ \ {\isachardoublequote}gcd\isadigit{2}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ n{\isacharequal}\isadigit{0}\ of\ True\ {\isasymRightarrow}\ m\ {\isacharbar}\ False\ {\isasymRightarrow}\ gcd\isadigit{2}{\isacharparenleft}n{\isacharcomma}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
26.58 +\isacommand{consts}\ gcd{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
26.59 +\isacommand{recdef}\ gcd{\isadigit{2}}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
26.60 +\ \ {\isachardoublequote}gcd{\isadigit{2}}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ n{\isacharequal}{\isadigit{0}}\ of\ True\ {\isasymRightarrow}\ m\ {\isacharbar}\ False\ {\isasymRightarrow}\ gcd{\isadigit{2}}{\isacharparenleft}n{\isacharcomma}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
26.61 \begin{isamarkuptext}%
26.62 \noindent
26.63 In fact, this is probably the neatest solution next to pattern matching.
26.64 @@ -77,10 +77,10 @@
26.65 A final alternative is to replace the offending simplification rules by
26.66 derived conditional ones. For \isa{gcd} it means we have to prove%
26.67 \end{isamarkuptext}%
26.68 -\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ \isadigit{0}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
26.69 +\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
26.70 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
26.71 \isacommand{done}\isanewline
26.72 -\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline
26.73 +\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline
26.74 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
26.75 \isacommand{done}%
26.76 \begin{isamarkuptext}%
27.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex Wed Oct 11 09:09:06 2000 +0200
27.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Wed Oct 11 10:44:42 2000 +0200
27.3 @@ -9,7 +9,7 @@
27.4 measure of the argument goes down in each recursive call. As a result,
27.5 $f$\isa{{\isachardot}simps} will contain the defining equations (or variants derived
27.6 from them) as theorems. For example, look (via \isacommand{thm}) at
27.7 -\isa{sep{\isachardot}simps} and \isa{sep\isadigit{1}{\isachardot}simps} to see that they define
27.8 +\isa{sep{\isachardot}simps} and \isa{sep{\isadigit{1}}{\isachardot}simps} to see that they define
27.9 the same function. What is more, those equations are automatically declared as
27.10 simplification rules.
27.11
27.12 @@ -19,7 +19,7 @@
27.13 \end{isamarkuptext}%
27.14 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
27.15 \isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
27.16 -\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
27.17 +\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
27.18 \begin{isamarkuptext}%
27.19 \noindent
27.20 is not proved automatically (although maybe it should be). Isabelle prints a
27.21 @@ -43,7 +43,7 @@
27.22 \end{isamarkuptext}%
27.23 \isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
27.24 \isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
27.25 -\ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
27.26 +\ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
27.27 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}%
27.28 \begin{isamarkuptext}%
27.29 \noindent
27.30 @@ -51,7 +51,7 @@
27.31 the stated recursion equation for \isa{g} and they are simplification
27.32 rules. Thus we can automatically prove%
27.33 \end{isamarkuptext}%
27.34 -\isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
27.35 +\isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
27.36 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
27.37 \isacommand{done}%
27.38 \begin{isamarkuptext}%
28.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Oct 11 09:09:06 2000 +0200
28.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Oct 11 10:44:42 2000 +0200
28.3 @@ -12,7 +12,7 @@
28.4 ambiguities caused by defining lists twice.%
28.5 \end{isamarkuptext}%
28.6 \isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}{\isacharparenright}\isanewline
28.7 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ list{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharhash}{\isachardoublequote}\ \isadigit{6}\isadigit{5}{\isacharparenright}%
28.8 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ list{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharhash}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}%
28.9 \begin{isamarkuptext}%
28.10 \noindent
28.11 The datatype\index{*datatype} \isaindexbold{list} introduces two
28.12 @@ -41,7 +41,7 @@
28.13 \end{warn}
28.14 Next, two functions \isa{app} and \isaindexbold{rev} are declared:%
28.15 \end{isamarkuptext}%
28.16 -\isacommand{consts}\ app\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharat}{\isachardoublequote}\ \isadigit{6}\isadigit{5}{\isacharparenright}\isanewline
28.17 +\isacommand{consts}\ app\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharat}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\isanewline
28.18 \ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}%
28.19 \begin{isamarkuptext}%
28.20 \noindent
28.21 @@ -156,7 +156,7 @@
28.22 where $G$
28.23 is the overall goal that we are trying to prove, and the numbered lines
28.24 contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
28.25 -establish $G$. At \isa{step\ \isadigit{0}} there is only one subgoal, which is
28.26 +establish $G$. At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is
28.27 identical with the overall goal. Normally $G$ is constant and only serves as
28.28 a reminder. Hence we rarely show it in this tutorial.
28.29
28.30 @@ -248,7 +248,7 @@
28.31 \begin{isamarkuptext}%
28.32 This time the canonical proof procedure%
28.33 \end{isamarkuptext}%
28.34 -\isacommand{lemma}\ app{\isacharunderscore}Nil\isadigit{2}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
28.35 +\isacommand{lemma}\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
28.36 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
28.37 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
28.38 \begin{isamarkuptxt}%
28.39 @@ -270,7 +270,7 @@
28.40
28.41 % Instead of \isacommand{apply} followed by a dot, you can simply write
28.42 % \isacommand{by}\indexbold{by}, which we do most of the time.
28.43 -Notice that in lemma \isa{app{\isacharunderscore}Nil\isadigit{2}}
28.44 +Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}}
28.45 (as printed out after the final \isacommand{done}) the free variable \isa{xs} has been
28.46 replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
28.47 \S\ref{sec:variables}.
28.48 @@ -290,7 +290,7 @@
28.49 ~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
28.50 \end{isabelle}
28.51 Now we need to remember that \isa{{\isacharat}} associates to the right, and that
28.52 -\isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{\isadigit{6}\isadigit{5}}
28.53 +\isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}}
28.54 in their \isacommand{infixr} annotation). Thus the conclusion really is
28.55 \begin{isabelle}
28.56 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
29.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex Wed Oct 11 09:09:06 2000 +0200
29.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Wed Oct 11 10:44:42 2000 +0200
29.3 @@ -114,8 +114,8 @@
29.4 \noindent
29.5 All methods ending in \isa{tac} take an optional first argument that
29.6 specifies the range of subgoals they are applied to, where \isa{{\isacharbrackleft}{\isacharbang}{\isacharbrackright}} means
29.7 -all subgoals, i.e.\ \isa{{\isacharbrackleft}\isadigit{1}{\isacharminus}\isadigit{3}{\isacharbrackright}} in our case. Individual subgoal numbers,
29.8 -e.g. \isa{{\isacharbrackleft}\isadigit{2}{\isacharbrackright}} are also allowed.
29.9 +all subgoals, i.e.\ \isa{{\isacharbrackleft}{\isadigit{1}}{\isacharminus}{\isadigit{3}}{\isacharbrackright}} in our case. Individual subgoal numbers,
29.10 +e.g. \isa{{\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}} are also allowed.
29.11
29.12 This proof may look surprisingly straightforward. However, note that this
29.13 comes at a cost: the proof script is unreadable because the intermediate