# HG changeset patch # User nipkow # Date 977154317 -3600 # Node ID 76d7f6c9a14c2a42a8ca5c8a381389e55ade35db # Parent ffb153ef636639c1d6ff7d922fed05e57e2bbd55 *** empty log message *** diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Advanced/document/Partial.tex --- a/doc-src/TutorialI/Advanced/document/Partial.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Mon Dec 18 16:45:17 2000 +0100 @@ -173,12 +173,10 @@ \isa{while{\isacharunderscore}rule}, the well known proof rule for total correctness of loops expressed with \isa{while}: \begin{isabelle}% -\ \ \ \ \ P\ s\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ {\isacharparenleft}{\isasymAnd}s{\isachardot}\ P\ s\ {\isasymLongrightarrow}\ b\ s\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ {\isacharparenleft}{\isasymAnd}s{\isachardot}\ P\ s\ {\isasymLongrightarrow}\ {\isasymnot}\ b\ s\ {\isasymLongrightarrow}\ Q\ s{\isacharparenright}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ wf\ r\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ {\isacharparenleft}{\isasymAnd}s{\isachardot}\ P\ s\ {\isasymLongrightarrow}\ b\ s\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isacharparenright}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}% +\ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline +\ \ \ \ \ {\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}% \end{isabelle} \isa{P} needs to be true of the initial state \isa{s} and invariant under \isa{c} (premises 1 and 2).The post-condition \isa{Q} must become true when diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Advanced/document/simp.tex --- a/doc-src/TutorialI/Advanced/document/simp.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Advanced/document/simp.tex Mon Dec 18 16:45:17 2000 +0100 @@ -28,7 +28,7 @@ controlled by so-called \bfindex{congruence rules}. This is the one for \isa{{\isasymlongrightarrow}}: \begin{isabelle}% -\ \ \ \ \ P\ {\isacharequal}\ P{\isacharprime}\ {\isasymLongrightarrow}\ {\isacharparenleft}P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymlongrightarrow}\ Q{\isacharprime}{\isacharparenright}% +\ \ \ \ \ {\isasymlbrakk}P\ {\isacharequal}\ P{\isacharprime}{\isacharsemicolon}\ P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymlongrightarrow}\ Q{\isacharprime}{\isacharparenright}% \end{isabelle} It should be read as follows: In order to simplify \isa{P\ {\isasymlongrightarrow}\ Q} to \isa{P{\isacharprime}\ {\isasymlongrightarrow}\ Q{\isacharprime}}, @@ -38,15 +38,14 @@ Here are some more examples. The congruence rules for bounded quantifiers supply contextual information about the bound variable: \begin{isabelle}% -\ \ \ \ \ A\ {\isacharequal}\ B\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ B\ {\isasymLongrightarrow}\ P\ x\ {\isacharequal}\ Q\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isasymin}A{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}B{\isachardot}\ Q\ x{\isacharparenright}% +\ \ \ \ \ {\isasymlbrakk}A\ {\isacharequal}\ B{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ B\ {\isasymLongrightarrow}\ P\ x\ {\isacharequal}\ Q\ x{\isasymrbrakk}\isanewline +\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isasymin}A{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}B{\isachardot}\ Q\ x{\isacharparenright}% \end{isabelle} The congruence rule for conditional expressions supply contextual information for simplifying the arms: \begin{isabelle}% -\ \ \ \ \ b\ {\isacharequal}\ c\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ {\isacharparenleft}c\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ u{\isacharparenright}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ {\isacharparenleft}{\isasymnot}\ c\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ v{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}if\ b\ then\ x\ else\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ c\ then\ u\ else\ v{\isacharparenright}% +\ \ \ \ \ {\isasymlbrakk}b\ {\isacharequal}\ c{\isacharsemicolon}\ c\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ u{\isacharsemicolon}\ {\isasymnot}\ c\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ v{\isasymrbrakk}\isanewline +\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}if\ b\ then\ x\ else\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ c\ then\ u\ else\ v{\isacharparenright}% \end{isabelle} A congruence rule can also \emph{prevent} simplification of some arguments. Here is an alternative congruence rule for conditional expressions: @@ -73,7 +72,7 @@ \begin{warn} The congruence rule \isa{conj{\isacharunderscore}cong} \begin{isabelle}% -\ \ \ \ \ P\ {\isacharequal}\ P{\isacharprime}\ {\isasymLongrightarrow}\ {\isacharparenleft}P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymand}\ Q{\isacharprime}{\isacharparenright}% +\ \ \ \ \ {\isasymlbrakk}P\ {\isacharequal}\ P{\isacharprime}{\isacharsemicolon}\ P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymand}\ Q{\isacharprime}{\isacharparenright}% \end{isabelle} is occasionally useful but not a default rule; you have to use it explicitly. \end{warn}% diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Mon Dec 18 16:45:17 2000 +0100 @@ -73,11 +73,12 @@ \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ p\ {\isadigit{0}}\ {\isasymin}\ A\ {\isasymor}\isanewline -\ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ {\isadigit{0}}\ {\isasymin}\ A\ {\isasymor}\isanewline +\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A% \end{isabelle} Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:% \end{isamarkuptxt}% @@ -91,10 +92,10 @@ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ {\isadigit{1}}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ \ \ \ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ {\isadigit{1}}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A% \end{isabelle} 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 first element. The rest is practically automatic:% @@ -170,10 +171,9 @@ \noindent After simplification and clarification the subgoal has the following compact form \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ P\ s\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ \ \ \ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ \ \ \ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline -\ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline +\ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}% \end{isabelle} and invites a proof by induction on \isa{i}:% \end{isamarkuptxt}% @@ -183,15 +183,14 @@ \noindent After simplification the base case boils down to \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ P\ s\ {\isasymLongrightarrow}\isanewline -\ \ \ \ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M% +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline +\ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M% \end{isabelle} The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M} holds. However, we first have to show that such a \isa{t} actually exists! This reasoning is embodied in the theorem \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: \begin{isabelle}% -\ \ \ \ \ {\isasymexists}a{\isachardot}\ {\isacharquery}P\ a\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}% +\ \ \ \ \ {\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}% \end{isabelle} When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/CTL/document/CTLind.tex --- a/doc-src/TutorialI/CTL/document/CTLind.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Mon Dec 18 16:45:17 2000 +0100 @@ -121,7 +121,7 @@ into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is, \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now \begin{isabelle}% -\ \ \ \ \ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}% +\ \ \ \ \ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}% \end{isabelle} The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s}, in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/CTL/document/PDL.tex --- a/doc-src/TutorialI/CTL/document/PDL.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Mon Dec 18 16:45:17 2000 +0100 @@ -127,7 +127,7 @@ \noindent After simplification and clarification we are left with \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ t\ {\isasymin}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}% \end{isabelle} This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model checker works backwards (from \isa{t} to \isa{s}), we cannot use the @@ -135,9 +135,9 @@ forward direction. Fortunately the converse induction theorem \isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists: \begin{isabelle}% -\ \ \ \ \ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ P\ b\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ {\isacharparenleft}{\isasymAnd}y\ z{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ P\ z\ {\isasymLongrightarrow}\ P\ y{\isacharparenright}\ {\isasymLongrightarrow}\ P\ a% +\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ {\isasymAnd}y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y{\isasymrbrakk}\isanewline +\ \ \ \ \ {\isasymLongrightarrow}\ P\ a% \end{isabelle} It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer \isa{P\ a} provided each step backwards from a predecessor \isa{z} of diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Inductive/document/AB.tex --- a/doc-src/TutorialI/Inductive/document/AB.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Mon Dec 18 16:45:17 2000 +0100 @@ -96,8 +96,8 @@ 1 on our way from 0 to 2. Formally, we appeal to the following discrete intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val} \begin{isabelle}% -\ \ \ \ \ {\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ f\ {\isadigit{0}}\ {\isasymle}\ k\ {\isasymLongrightarrow}\ k\ {\isasymle}\ f\ n\ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k% +\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline +\ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k% \end{isabelle} where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers, \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Inductive/document/Advanced.tex --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Dec 18 16:45:17 2000 +0100 @@ -36,7 +36,7 @@ We completely forgot about "rule inversion". \begin{isabelle}% -\ \ \ \ \ a\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P% +\ \ \ \ \ {\isasymlbrakk}a\ {\isasymin}\ even{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% \end{isabelle} \rulename{even.cases} @@ -50,7 +50,7 @@ \isacommand{thm}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases% \begin{isamarkuptext}% \begin{isabelle}% -\ \ \ \ \ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P% +\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% \end{isabelle} \rulename{Suc_Suc_cases} @@ -65,7 +65,7 @@ this is what we get: \begin{isabelle}% -\ \ \ \ \ Apply\ f\ args\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ f\ {\isasymin}\ F\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P% +\ \ \ \ \ {\isasymlbrakk}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% \end{isabelle} \rulename{gterm_Apply_elim}% \end{isamarkuptext}% diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Inductive/document/Even.tex --- a/doc-src/TutorialI/Inductive/document/Even.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Mon Dec 18 16:45:17 2000 +0100 @@ -31,7 +31,7 @@ \rulename{even.step} \begin{isabelle}% -\ \ \ \ \ xa\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xa% +\ \ \ \ \ {\isasymlbrakk}xa\ {\isasymin}\ even{\isacharsemicolon}\ P\ {\isadigit{0}}{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ P\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ xa% \end{isabelle} \rulename{even.induct} diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Inductive/document/Star.tex --- a/doc-src/TutorialI/Inductive/document/Star.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Mon Dec 18 16:45:17 2000 +0100 @@ -51,9 +51,9 @@ To prove transitivity, we need rule induction, i.e.\ theorem \isa{rtc{\isachardot}induct}: \begin{isabelle}% -\ \ \ \ \ {\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharparenright}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x\ y\ z{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ y\ z\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa% +\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ {\isasymAnd}x\ y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isacharquery}P\ y\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isasymrbrakk}\isanewline +\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa% \end{isabelle} It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}xb{\isacharcomma}{\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}} if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition, i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the @@ -110,9 +110,8 @@ \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline -\ \ \ \ \ \ \ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ \ \ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% +\ \ \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% \end{isabelle}% \end{isamarkuptxt}% \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline @@ -157,7 +156,7 @@ \begin{exercise}\label{ex:converse-rtc-step} Show that the converse of \isa{rtc{\isacharunderscore}step} also holds: \begin{isabelle}% -\ \ \ \ \ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% +\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% \end{isabelle} \end{exercise} \begin{exercise} diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Misc/document/AdvancedInd.tex --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Dec 18 16:45:17 2000 +0100 @@ -95,7 +95,7 @@ \isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}% \begin{isamarkuptext}% \noindent -yielding \isa{A\ y\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}. +yielding \isa{{\isasymlbrakk}A\ y{\isacharsemicolon}\ B\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}. You can go one step further and include these derivations already in the statement of your original lemma, thus avoiding the intermediate step:% \end{isamarkuptext}% @@ -182,7 +182,8 @@ \begin{isamarkuptxt}% \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline -\ \ \ \ \ \ \ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharparenright}\ {\isasymLongrightarrow}\ i\ {\isacharequal}\ Suc\ nat\ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i% +\ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharparenright}{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i% \end{isabelle}% \end{isamarkuptxt}% \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}% @@ -195,7 +196,7 @@ proved as follows. From \isa{f{\isacharunderscore}ax} we have \isa{f\ {\isacharparenleft}f\ j{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} (by the induction hypothesis). Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by transitivity -(\isa{le{\isacharunderscore}less{\isacharunderscore}trans}: \isa{i\ {\isasymle}\ j\ {\isasymLongrightarrow}\ j\ {\isacharless}\ k\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}). +(\isa{le{\isacharunderscore}less{\isacharunderscore}trans}: \isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}). Using the induction hypothesis once more we obtain \isa{j\ {\isasymle}\ f\ j} which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by \isa{le{\isacharunderscore}less{\isacharunderscore}trans}). @@ -267,7 +268,7 @@ \noindent The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction: \begin{isabelle}% -\ \ \ \ \ m\ {\isacharless}\ Suc\ n\ {\isasymLongrightarrow}\ {\isacharparenleft}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P% +\ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% \end{isabelle} Now it is straightforward to derive the original version of diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Misc/document/simp.tex --- a/doc-src/TutorialI/Misc/document/simp.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Misc/document/simp.tex Mon Dec 18 16:45:17 2000 +0100 @@ -303,8 +303,8 @@ In contrast to splitting the conclusion, this actually creates two separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}): \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline -\ {\isadigit{2}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}% +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}% \end{isabelle} If you need to split both in the assumptions and the conclusion, use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Recdef/document/Nested2.tex --- a/doc-src/TutorialI/Recdef/document/Nested2.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Mon Dec 18 16:45:17 2000 +0100 @@ -61,9 +61,8 @@ \isacommand{recdef} has been supplied with the congruence theorem \isa{map{\isacharunderscore}cong}: \begin{isabelle}% -\ \ \ \ \ xs\ {\isacharequal}\ ys\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ map\ f\ xs\ {\isacharequal}\ map\ g\ ys% +\ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline +\ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys% \end{isabelle} Its second premise expresses (indirectly) that the second argument of \isa{map} is only applied to elements of its third argument. Congruence diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Types/Overloading2.thy --- a/doc-src/TutorialI/Types/Overloading2.thy Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Types/Overloading2.thy Mon Dec 18 16:45:17 2000 +0100 @@ -47,4 +47,15 @@ \label{tab:overloading} \end{center} \end{table} + +In addition there is a special input syntax for bounded quantifiers: +\begin{center} +\begin{tabular}{lcl} +@{text"\x \ y. P x"} & @{text"\"} & @{prop"\x. x \ y \ P x"} \\ +@{text"\x \ y. P x"} & @{text"\"} & @{prop"\x. x \ y \ P x"} +\end{tabular} +\end{center} +And analogously for @{text"<"} instead of @{text"\"}. +The form on the left is translated into the one on the right upon input but it is not +translated back upon output. *}(*<*)end(*>*) diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Types/document/Axioms.tex --- a/doc-src/TutorialI/Types/document/Axioms.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Types/document/Axioms.tex Mon Dec 18 16:45:17 2000 +0100 @@ -68,8 +68,8 @@ specialized to type \isa{bool}, as subgoals: \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}\ z{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymLongrightarrow}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z\isanewline -\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymLongrightarrow}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}\ z{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z\isanewline +\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline \ {\isadigit{4}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}% \end{isabelle} Fortunately, the proof is easy for blast, once we have unfolded the definitions diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Mon Dec 18 16:45:17 2000 +0100 @@ -75,12 +75,12 @@ % \begin{isamarkuptext}% \begin{isabelle}% -\ \ \ \ \ i\ {\isasymle}\ j\ {\isasymLongrightarrow}\ k\ {\isasymle}\ l\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isasymle}\ j\ {\isacharasterisk}\ l% +\ \ \ \ \ {\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ k\ {\isasymle}\ l{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isasymle}\ j\ {\isacharasterisk}\ l% \end{isabelle} \rulename{mult_le_mono} \begin{isabelle}% -\ \ \ \ \ i\ {\isacharless}\ j\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ k\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isacharless}\ j\ {\isacharasterisk}\ k% +\ \ \ \ \ {\isasymlbrakk}i\ {\isacharless}\ j{\isacharsemicolon}\ {\isadigit{0}}\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isacharless}\ j\ {\isacharasterisk}\ k% \end{isabelle} \rulename{mult_less_mono1} @@ -160,12 +160,12 @@ \rulename{DIVISION_BY_ZERO_MOD} \begin{isabelle}% -\ \ \ \ \ m\ dvd\ n\ {\isasymLongrightarrow}\ n\ dvd\ m\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n% +\ \ \ \ \ {\isasymlbrakk}m\ dvd\ n{\isacharsemicolon}\ n\ dvd\ m{\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n% \end{isabelle} \rulename{dvd_anti_sym} \begin{isabelle}% -\ \ \ \ \ k\ dvd\ m\ {\isasymLongrightarrow}\ k\ dvd\ n\ {\isasymLongrightarrow}\ k\ dvd\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}% +\ \ \ \ \ {\isasymlbrakk}k\ dvd\ m{\isacharsemicolon}\ k\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ k\ dvd\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}% \end{isabelle} \rulename{dvd_add} diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Types/document/Overloading2.tex --- a/doc-src/TutorialI/Types/document/Overloading2.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex Mon Dec 18 16:45:17 2000 +0100 @@ -48,7 +48,18 @@ \caption{Overloaded constants in HOL} \label{tab:overloading} \end{center} -\end{table}% +\end{table} + +In addition there is a special input syntax for bounded quantifiers: +\begin{center} +\begin{tabular}{lcl} +\isa{{\isasymforall}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymequiv}} & \isa{{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x} \\ +\isa{{\isasymexists}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymequiv}} & \isa{{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x} +\end{tabular} +\end{center} +And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}. +The form on the left is translated into the one on the right upon input but it is not +translated back upon output.% \end{isamarkuptext}% \end{isabellebody}% %%% Local Variables: diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/Types/document/Typedef.tex --- a/doc-src/TutorialI/Types/document/Typedef.tex Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/Types/document/Typedef.tex Mon Dec 18 16:45:17 2000 +0100 @@ -204,7 +204,7 @@ Expanding \isa{three{\isacharunderscore}def} yields the premise \isa{n\ {\isasymle}\ {\isadigit{2}}}. Repeated elimination with \isa{le{\isacharunderscore}SucE} \begin{isabelle}% -\ \ \ \ \ {\isacharquery}m\ {\isasymle}\ Suc\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharquery}m\ {\isasymle}\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharquery}m\ {\isacharequal}\ Suc\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}R% +\ \ \ \ \ {\isasymlbrakk}{\isacharquery}m\ {\isasymle}\ Suc\ {\isacharquery}n{\isacharsemicolon}\ {\isacharquery}m\ {\isasymle}\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharsemicolon}\ {\isacharquery}m\ {\isacharequal}\ Suc\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R% \end{isabelle} reduces \isa{n\ {\isasymle}\ {\isadigit{2}}} to the three cases \isa{n\ {\isasymle}\ {\isadigit{0}}}, \isa{n\ {\isacharequal}\ {\isadigit{1}}} and \isa{n\ {\isacharequal}\ {\isadigit{2}}} which are trivial for simplification:% @@ -231,10 +231,10 @@ \isacommand{apply}{\isacharparenleft}rule\ cases{\isacharunderscore}lemma{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ P\ A\ {\isasymLongrightarrow}\ P\ B\ {\isasymLongrightarrow}\ P\ C\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{0}}{\isacharparenright}\isanewline -\ {\isadigit{2}}{\isachardot}\ P\ A\ {\isasymLongrightarrow}\ P\ B\ {\isasymLongrightarrow}\ P\ C\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{1}}{\isacharparenright}\isanewline -\ {\isadigit{3}}{\isachardot}\ P\ A\ {\isasymLongrightarrow}\ P\ B\ {\isasymLongrightarrow}\ P\ C\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{2}}{\isacharparenright}\isanewline -\ {\isadigit{4}}{\isachardot}\ P\ A\ {\isasymLongrightarrow}\ P\ B\ {\isasymLongrightarrow}\ P\ C\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ x\ {\isasymin}\ three% +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{0}}{\isacharparenright}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{1}}{\isacharparenright}\isanewline +\ {\isadigit{3}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{2}}{\isacharparenright}\isanewline +\ {\isadigit{4}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ x\ {\isasymin}\ three% \end{isabelle} The resulting subgoals are easily solved by simplification:% \end{isamarkuptxt}% diff -r ffb153ef6366 -r 76d7f6c9a14c doc-src/TutorialI/isabellesym.sty --- a/doc-src/TutorialI/isabellesym.sty Mon Dec 18 16:11:53 2000 +0100 +++ b/doc-src/TutorialI/isabellesym.sty Mon Dec 18 16:45:17 2000 +0100 @@ -134,11 +134,11 @@ \newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}} \newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires latexsym \newcommand{\isasymup}{\isamath{\uparrow}} -\newcommand{\isasymUparrow}{\isamath{\Uparrow}} +\newcommand{\isasymUp}{\isamath{\Uparrow}} \newcommand{\isasymdown}{\isamath{\downarrow}} -\newcommand{\isasymDownarrow}{\isamath{\Downarrow}} -\newcommand{\isasymupdownarrow}{\isamath{\updownarrow}} -\newcommand{\isasymUpdownarrow}{\isamath{\Updownarrow}} +\newcommand{\isasymDown}{\isamath{\Downarrow}} +\newcommand{\isasymupdown}{\isamath{\updownarrow}} +\newcommand{\isasymUpdown}{\isamath{\Updownarrow}} \newcommand{\isasymlangle}{\isamath{\langle}} \newcommand{\isasymrangle}{\isamath{\rangle}} \newcommand{\isasymlceil}{\isamath{\lceil}} @@ -158,9 +158,9 @@ \newcommand{\isasymbottom}{\isamath{\bot}} \newcommand{\isasymtop}{\isamath{\top}} \newcommand{\isasymand}{\isamath{\wedge}} +\newcommand{\isasymAnd}{\isamath{\bigwedge\,}} \newcommand{\isasymor}{\isamath{\vee}} -\newcommand{\isasymAnd}{\isamath{\bigwedge\,}} -\newcommand{\isasymOr}{\isamath{\bigvee}} +\newcommand{\isasymOr}{\isamath{\bigvee\,}} \newcommand{\isasymforall}{\isamath{\forall\,}} \newcommand{\isasymexists}{\isamath{\exists\,}} \newcommand{\isasymbox}{\isamath{\Box}} %requires latexsym @@ -188,15 +188,15 @@ \newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}} \newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}} \newcommand{\isasyminter}{\isamath{\cap}} +\newcommand{\isasymInter}{\isamath{\bigcap\,}} \newcommand{\isasymunion}{\isamath{\cup}} -\newcommand{\isasymInter}{\isamath{\bigcap\,}} \newcommand{\isasymUnion}{\isamath{\bigcup\,}} \newcommand{\isasymsqunion}{\isamath{\sqcup}} +\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}} \newcommand{\isasymsqinter}{\isamath{\sqcap}} -\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}} \newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires stmaryrd \newcommand{\isasymuplus}{\isamath{\uplus}} -\newcommand{\isasymbiguplus}{\isamath{\biguplus}} +\newcommand{\isasymUplus}{\isamath{\biguplus\,}} \newcommand{\isasymnoteq}{\isamath{\not=}} \newcommand{\isasymsim}{\isamath{\sim}} \newcommand{\isasymdoteq}{\isamath{\doteq}} @@ -234,17 +234,21 @@ \newcommand{\isasymtriangle}{\isamath{\triangle}} \newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb \newcommand{\isasymoplus}{\isamath{\oplus}} +\newcommand{\isasymOplus}{\isamath{\bigoplus\,}} +\newcommand{\isasymotimes}{\isamath{\otimes}} +\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}} +\newcommand{\isasymodot}{\isamath{\odot}} +\newcommand{\isasymOdot}{\isamath{\bigodot\,}} \newcommand{\isasymominus}{\isamath{\ominus}} -\newcommand{\isasymotimes}{\isamath{\otimes}} \newcommand{\isasymoslash}{\isamath{\oslash}} -\newcommand{\isasymodot}{\isamath{\odot}} -\newcommand{\isasyminfinity}{\isamath{\infty}} \newcommand{\isasymdots}{\isamath{\dots}} \newcommand{\isasymcdots}{\isamath{\cdots}} \newcommand{\isasymSum}{\isamath{\sum\,}} \newcommand{\isasymProd}{\isamath{\prod\,}} +\newcommand{\isasymCoprod}{\isamath{\coprod\,}} +\newcommand{\isasyminfinity}{\isamath{\infty}} \newcommand{\isasymintegral}{\isamath{\int\,}} -\newcommand{\isasymJoin}{\isamath{\Join}} %requires latexsym +\newcommand{\isasymointegral}{\isamath{\oint\,}} \newcommand{\isasymclubsuit}{\isamath{\clubsuit}} \newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}} \newcommand{\isasymheartsuit}{\isamath{\heartsuit}} @@ -284,4 +288,5 @@ \newcommand{\isasymamalg}{\isamath{\amalg}} \newcommand{\isasymmho}{\isamath{\mho}} %requires latexsym \newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssym +\newcommand{\isasymJoin}{\isamath{\Join}} %requires latexsym \newcommand{\isasymspacespace}{\isamath{~~}}