1.1 --- a/doc-src/TutorialI/Advanced/document/Partial.tex Wed Dec 13 17:43:33 2000 +0100
1.2 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Wed Dec 13 17:46:49 2000 +0100
1.3 @@ -173,10 +173,12 @@
1.4 \isa{while{\isacharunderscore}rule}, the well known proof rule for total
1.5 correctness of loops expressed with \isa{while}:
1.6 \begin{isabelle}%
1.7 -\ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline
1.8 -\ \ \ \ \ \ \ \ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline
1.9 -\ \ \ \ \ \ \ \ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline
1.10 -\ \ \ \ \ {\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}%
1.11 +\ \ \ \ \ P\ s\ {\isasymLongrightarrow}\isanewline
1.12 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}s{\isachardot}\ P\ s\ {\isasymLongrightarrow}\ b\ s\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
1.13 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}s{\isachardot}\ P\ s\ {\isasymLongrightarrow}\ {\isasymnot}\ b\ s\ {\isasymLongrightarrow}\ Q\ s{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
1.14 +\ \ \ \ \ wf\ r\ {\isasymLongrightarrow}\isanewline
1.15 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}s{\isachardot}\ P\ s\ {\isasymLongrightarrow}\ b\ s\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
1.16 +\ \ \ \ \ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}%
1.17 \end{isabelle} \isa{P} needs to be
1.18 true of the initial state \isa{s} and invariant under \isa{c}
1.19 (premises 1 and 2).The post-condition \isa{Q} must become true when
2.1 --- a/doc-src/TutorialI/Advanced/document/simp.tex Wed Dec 13 17:43:33 2000 +0100
2.2 +++ b/doc-src/TutorialI/Advanced/document/simp.tex Wed Dec 13 17:46:49 2000 +0100
2.3 @@ -28,7 +28,7 @@
2.4 controlled by so-called \bfindex{congruence rules}. This is the one for
2.5 \isa{{\isasymlongrightarrow}}:
2.6 \begin{isabelle}%
2.7 -\ \ \ \ \ {\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}%
2.8 +\ \ \ \ \ 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}%
2.9 \end{isabelle}
2.10 It should be read as follows:
2.11 In order to simplify \isa{P\ {\isasymlongrightarrow}\ Q} to \isa{P{\isacharprime}\ {\isasymlongrightarrow}\ Q{\isacharprime}},
2.12 @@ -38,14 +38,15 @@
2.13 Here are some more examples. The congruence rules for bounded
2.14 quantifiers supply contextual information about the bound variable:
2.15 \begin{isabelle}%
2.16 -\ \ \ \ \ {\isasymlbrakk}A\ {\isacharequal}\ B{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ B\ {\isasymLongrightarrow}\ P\ x\ {\isacharequal}\ Q\ x{\isasymrbrakk}\isanewline
2.17 -\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isasymin}A{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}B{\isachardot}\ Q\ x{\isacharparenright}%
2.18 +\ \ \ \ \ A\ {\isacharequal}\ B\ {\isasymLongrightarrow}\isanewline
2.19 +\ \ \ \ \ {\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}%
2.20 \end{isabelle}
2.21 The congruence rule for conditional expressions supply contextual
2.22 information for simplifying the arms:
2.23 \begin{isabelle}%
2.24 -\ \ \ \ \ {\isasymlbrakk}b\ {\isacharequal}\ c{\isacharsemicolon}\ c\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ u{\isacharsemicolon}\ {\isasymnot}\ c\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ v{\isasymrbrakk}\isanewline
2.25 -\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}if\ b\ then\ x\ else\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ c\ then\ u\ else\ v{\isacharparenright}%
2.26 +\ \ \ \ \ b\ {\isacharequal}\ c\ {\isasymLongrightarrow}\isanewline
2.27 +\ \ \ \ \ {\isacharparenleft}c\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ u{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
2.28 +\ \ \ \ \ {\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}%
2.29 \end{isabelle}
2.30 A congruence rule can also \emph{prevent} simplification of some arguments.
2.31 Here is an alternative congruence rule for conditional expressions:
2.32 @@ -72,7 +73,7 @@
2.33 \begin{warn}
2.34 The congruence rule \isa{conj{\isacharunderscore}cong}
2.35 \begin{isabelle}%
2.36 -\ \ \ \ \ {\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}%
2.37 +\ \ \ \ \ 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}%
2.38 \end{isabelle}
2.39 is occasionally useful but not a default rule; you have to use it explicitly.
2.40 \end{warn}%
3.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex Wed Dec 13 17:43:33 2000 +0100
3.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed Dec 13 17:46:49 2000 +0100
3.3 @@ -73,12 +73,11 @@
3.4 \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
3.5 \begin{isamarkuptxt}%
3.6 \begin{isabelle}%
3.7 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ {\isadigit{0}}\ {\isasymin}\ A\ {\isasymor}\isanewline
3.8 -\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
3.9 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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
3.10 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
3.11 -\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
3.12 -\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
3.13 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ p\ {\isadigit{0}}\ {\isasymin}\ A\ {\isasymor}\isanewline
3.14 +\ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
3.15 +\ \ \ \ \ \ \ \ \ \ \ \ \ {\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
3.16 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
3.17 +\ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
3.18 \end{isabelle}
3.19 Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:%
3.20 \end{isamarkuptxt}%
3.21 @@ -92,10 +91,10 @@
3.22 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
3.23 \begin{isamarkuptxt}%
3.24 \begin{isabelle}%
3.25 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline
3.26 -\ \ \ \ \ \ \ \ \ \ \ {\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
3.27 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
3.28 -\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
3.29 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymLongrightarrow}\isanewline
3.30 +\ \ \ \ \ \ \ \ {\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
3.31 +\ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
3.32 +\ \ \ \ \ \ \ \ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
3.33 \end{isabelle}
3.34 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
3.35 first element. The rest is practically automatic:%
3.36 @@ -171,9 +170,10 @@
3.37 \noindent
3.38 After simplification and clarification the subgoal has the following compact form
3.39 \begin{isabelle}%
3.40 -\ {\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
3.41 -\ \ \ \ \ \ \ \ {\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
3.42 -\ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}%
3.43 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ P\ s\ {\isasymLongrightarrow}\isanewline
3.44 +\ \ \ \ \ \ \ \ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
3.45 +\ \ \ \ \ \ \ \ {\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
3.46 +\ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}%
3.47 \end{isabelle}
3.48 and invites a proof by induction on \isa{i}:%
3.49 \end{isamarkuptxt}%
3.50 @@ -183,14 +183,15 @@
3.51 \noindent
3.52 After simplification the base case boils down to
3.53 \begin{isabelle}%
3.54 -\ {\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
3.55 -\ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M%
3.56 +\ {\isadigit{1}}{\isachardot}\ P\ s\ {\isasymLongrightarrow}\isanewline
3.57 +\ \ \ \ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
3.58 +\ \ \ \ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M%
3.59 \end{isabelle}
3.60 The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M}
3.61 holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
3.62 is embodied in the theorem \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:
3.63 \begin{isabelle}%
3.64 -\ \ \ \ \ {\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}%
3.65 +\ \ \ \ \ {\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}%
3.66 \end{isabelle}
3.67 When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
3.68 \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
4.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex Wed Dec 13 17:43:33 2000 +0100
4.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Wed Dec 13 17:46:49 2000 +0100
4.3 @@ -121,7 +121,7 @@
4.4 into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
4.5 \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
4.6 \begin{isabelle}%
4.7 -\ \ \ \ \ {\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}%
4.8 +\ \ \ \ \ {\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}%
4.9 \end{isabelle}
4.10 The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s},
4.11 in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true
5.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex Wed Dec 13 17:43:33 2000 +0100
5.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Wed Dec 13 17:46:49 2000 +0100
5.3 @@ -127,7 +127,7 @@
5.4 \noindent
5.5 After simplification and clarification we are left with
5.6 \begin{isabelle}%
5.7 -\ {\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}%
5.8 +\ {\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}%
5.9 \end{isabelle}
5.10 This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model
5.11 checker works backwards (from \isa{t} to \isa{s}), we cannot use the
5.12 @@ -135,9 +135,9 @@
5.13 forward direction. Fortunately the converse induction theorem
5.14 \isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists:
5.15 \begin{isabelle}%
5.16 -\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline
5.17 -\ \ \ \ \ \ \ \ {\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
5.18 -\ \ \ \ \ {\isasymLongrightarrow}\ P\ a%
5.19 +\ \ \ \ \ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\isanewline
5.20 +\ \ \ \ \ P\ b\ {\isasymLongrightarrow}\isanewline
5.21 +\ \ \ \ \ {\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%
5.22 \end{isabelle}
5.23 It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer
5.24 \isa{P\ a} provided each step backwards from a predecessor \isa{z} of
6.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex Wed Dec 13 17:43:33 2000 +0100
6.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Wed Dec 13 17:46:49 2000 +0100
6.3 @@ -96,8 +96,8 @@
6.4 1 on our way from 0 to 2. Formally, we appeal to the following discrete
6.5 intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
6.6 \begin{isabelle}%
6.7 -\ \ \ \ \ {\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
6.8 -\ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
6.9 +\ \ \ \ \ {\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
6.10 +\ \ \ \ \ f\ {\isadigit{0}}\ {\isasymle}\ k\ {\isasymLongrightarrow}\ k\ {\isasymle}\ f\ n\ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
6.11 \end{isabelle}
6.12 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
6.13 \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
7.1 --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Wed Dec 13 17:43:33 2000 +0100
7.2 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Wed Dec 13 17:46:49 2000 +0100
7.3 @@ -36,7 +36,7 @@
7.4 We completely forgot about "rule inversion".
7.5
7.6 \begin{isabelle}%
7.7 -\ \ \ \ \ {\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%
7.8 +\ \ \ \ \ 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%
7.9 \end{isabelle}
7.10 \rulename{even.cases}
7.11
7.12 @@ -50,7 +50,7 @@
7.13 \isacommand{thm}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases%
7.14 \begin{isamarkuptext}%
7.15 \begin{isabelle}%
7.16 -\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
7.17 +\ \ \ \ \ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P%
7.18 \end{isabelle}
7.19 \rulename{Suc_Suc_cases}
7.20
7.21 @@ -65,7 +65,7 @@
7.22 this is what we get:
7.23
7.24 \begin{isabelle}%
7.25 -\ \ \ \ \ {\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%
7.26 +\ \ \ \ \ 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%
7.27 \end{isabelle}
7.28 \rulename{gterm_Apply_elim}%
7.29 \end{isamarkuptext}%
8.1 --- a/doc-src/TutorialI/Inductive/document/Even.tex Wed Dec 13 17:43:33 2000 +0100
8.2 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Wed Dec 13 17:46:49 2000 +0100
8.3 @@ -31,7 +31,7 @@
8.4 \rulename{even.step}
8.5
8.6 \begin{isabelle}%
8.7 -\ \ \ \ \ {\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%
8.8 +\ \ \ \ \ 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%
8.9 \end{isabelle}
8.10 \rulename{even.induct}
8.11
9.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex Wed Dec 13 17:43:33 2000 +0100
9.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Wed Dec 13 17:46:49 2000 +0100
9.3 @@ -51,9 +51,9 @@
9.4 To prove transitivity, we need rule induction, i.e.\ theorem
9.5 \isa{rtc{\isachardot}induct}:
9.6 \begin{isabelle}%
9.7 -\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline
9.8 -\ \ \ \ \ \ \ \ {\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
9.9 -\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa%
9.10 +\ \ \ \ \ {\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}\ {\isasymLongrightarrow}\isanewline
9.11 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
9.12 +\ \ \ \ \ {\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%
9.13 \end{isabelle}
9.14 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,
9.15 i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the
9.16 @@ -110,8 +110,9 @@
9.17 \begin{isabelle}%
9.18 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline
9.19 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline
9.20 -\ \ \ \ \ \ \ {\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
9.21 -\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
9.22 +\ \ \ \ \ \ \ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\isanewline
9.23 +\ \ \ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\isanewline
9.24 +\ \ \ \ \ \ \ {\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}%
9.25 \end{isabelle}%
9.26 \end{isamarkuptxt}%
9.27 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
9.28 @@ -156,7 +157,7 @@
9.29 \begin{exercise}\label{ex:converse-rtc-step}
9.30 Show that the converse of \isa{rtc{\isacharunderscore}step} also holds:
9.31 \begin{isabelle}%
9.32 -\ \ \ \ \ {\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}%
9.33 +\ \ \ \ \ {\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}%
9.34 \end{isabelle}
9.35 \end{exercise}
9.36 \begin{exercise}
10.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Dec 13 17:43:33 2000 +0100
10.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Dec 13 17:46:49 2000 +0100
10.3 @@ -95,7 +95,7 @@
10.4 \isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}%
10.5 \begin{isamarkuptext}%
10.6 \noindent
10.7 -yielding \isa{{\isasymlbrakk}A\ y{\isacharsemicolon}\ B\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}.
10.8 +yielding \isa{A\ y\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}.
10.9 You can go one step further and include these derivations already in the
10.10 statement of your original lemma, thus avoiding the intermediate step:%
10.11 \end{isamarkuptext}%
10.12 @@ -182,8 +182,7 @@
10.13 \begin{isamarkuptxt}%
10.14 \begin{isabelle}%
10.15 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline
10.16 -\ \ \ \ \ \ \ {\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
10.17 -\ \ \ \ \ \ \ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
10.18 +\ \ \ \ \ \ \ {\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%
10.19 \end{isabelle}%
10.20 \end{isamarkuptxt}%
10.21 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
10.22 @@ -196,7 +195,7 @@
10.23 proved as follows. From \isa{f{\isacharunderscore}ax} we have \isa{f\ {\isacharparenleft}f\ j{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}
10.24 (1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} (by the induction hypothesis).
10.25 Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by transitivity
10.26 -(\isa{le{\isacharunderscore}less{\isacharunderscore}trans}: \isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}).
10.27 +(\isa{le{\isacharunderscore}less{\isacharunderscore}trans}: \isa{i\ {\isasymle}\ j\ {\isasymLongrightarrow}\ j\ {\isacharless}\ k\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}).
10.28 Using the induction hypothesis once more we obtain \isa{j\ {\isasymle}\ f\ j}
10.29 which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by
10.30 \isa{le{\isacharunderscore}less{\isacharunderscore}trans}).
10.31 @@ -268,7 +267,7 @@
10.32 \noindent
10.33 The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
10.34 \begin{isabelle}%
10.35 -\ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
10.36 +\ \ \ \ \ m\ {\isacharless}\ Suc\ n\ {\isasymLongrightarrow}\ {\isacharparenleft}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P%
10.37 \end{isabelle}
10.38
10.39 Now it is straightforward to derive the original version of
11.1 --- a/doc-src/TutorialI/Misc/document/simp.tex Wed Dec 13 17:43:33 2000 +0100
11.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex Wed Dec 13 17:46:49 2000 +0100
11.3 @@ -228,33 +228,31 @@
11.4 }
11.5 %
11.6 \begin{isamarkuptext}%
11.7 -\indexbold{case splits}\index{*split|(}
11.8 +\indexbold{case splits}\index{*split (method, attr.)|(}
11.9 Goals containing \isa{if}-expressions are usually proved by case
11.10 distinction on the condition of the \isa{if}. For example the goal%
11.11 \end{isamarkuptext}%
11.12 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
11.13 \begin{isamarkuptxt}%
11.14 \noindent
11.15 -can be split by a degenerate form of simplification%
11.16 +can be split by a special method \isa{split}:%
11.17 \end{isamarkuptxt}%
11.18 -\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
11.19 +\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}if{\isacharparenright}%
11.20 \begin{isamarkuptxt}%
11.21 \noindent
11.22 \begin{isabelle}%
11.23 \ {\isadigit{1}}{\isachardot}\ {\isasymforall}xs{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}%
11.24 \end{isabelle}
11.25 -where no simplification rules are included (\isa{only{\isacharcolon}} is followed by the
11.26 -empty list of theorems) but the rule \isaindexbold{split_if} for
11.27 -splitting \isa{if}s is added (via the modifier \isa{split{\isacharcolon}}). Because
11.28 +where \isaindexbold{split_if} is a theorem that expresses splitting of
11.29 +\isa{if}s. Because
11.30 case-splitting on \isa{if}s is almost always the right proof strategy, the
11.31 simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}}
11.32 on the initial goal above.
11.33
11.34 This splitting idea generalizes from \isa{if} to \isaindex{case}:%
11.35 \end{isamarkuptxt}%
11.36 -\isanewline
11.37 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
11.38 -\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
11.39 +\isacommand{apply}{\isacharparenleft}split\ list{\isachardot}split{\isacharparenright}%
11.40 \begin{isamarkuptxt}%
11.41 \begin{isabelle}%
11.42 \ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}\ {\isasymand}\isanewline
11.43 @@ -262,13 +260,14 @@
11.44 \end{isabelle}
11.45 In contrast to \isa{if}-expressions, the simplifier does not split
11.46 \isa{case}-expressions by default because this can lead to nontermination
11.47 -in case of recursive datatypes. Again, if the \isa{only{\isacharcolon}} modifier is
11.48 -dropped, the above goal is solved,%
11.49 +in case of recursive datatypes. Therefore the simplifier has a modifier
11.50 +\isa{split} for adding further splitting rules explicitly. This means the
11.51 +above lemma can be proved in one step by%
11.52 \end{isamarkuptxt}%
11.53 \isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
11.54 \begin{isamarkuptext}%
11.55 -\noindent%
11.56 -which \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not do.
11.57 +\noindent
11.58 +whereas \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not succeed.
11.59
11.60 In general, every datatype $t$ comes with a theorem
11.61 $t$\isa{{\isachardot}split} which can be declared to be a \bfindex{split rule} either
11.62 @@ -287,20 +286,25 @@
11.63 \end{isamarkuptext}%
11.64 \isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split\ del{\isacharbrackright}%
11.65 \begin{isamarkuptext}%
11.66 +In polished proofs the \isa{split} method is rarely used on its own
11.67 +but always as part of the simplifier. However, if a goal contains
11.68 +multiple splittable constructs, the \isa{split} method can be
11.69 +helpful in selectively exploring the effects of splitting.
11.70 +
11.71 The above split rules intentionally only affect the conclusion of a
11.72 subgoal. If you want to split an \isa{if} or \isa{case}-expression in
11.73 the assumptions, you have to apply \isa{split{\isacharunderscore}if{\isacharunderscore}asm} or
11.74 $t$\isa{{\isachardot}split{\isacharunderscore}asm}:%
11.75 \end{isamarkuptext}%
11.76 -\isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharat}\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
11.77 -\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}%
11.78 +\isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
11.79 +\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}%
11.80 \begin{isamarkuptxt}%
11.81 \noindent
11.82 In contrast to splitting the conclusion, this actually creates two
11.83 separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}):
11.84 \begin{isabelle}%
11.85 -\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
11.86 -\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}%
11.87 +\ {\isadigit{1}}{\isachardot}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
11.88 +\ {\isadigit{2}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}%
11.89 \end{isabelle}
11.90 If you need to split both in the assumptions and the conclusion,
11.91 use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and
11.92 @@ -313,9 +317,7 @@
11.93 same is true for \isaindex{case}-expressions: only the selector is
11.94 simplified at first, until either the expression reduces to one of the
11.95 cases or it is split.
11.96 -\end{warn}
11.97 -
11.98 -\index{*split|)}%
11.99 +\end{warn}\index{*split (method, attr.)|)}%
11.100 \end{isamarkuptxt}%
11.101 %
11.102 \isamarkupsubsubsection{Arithmetic%
12.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex Wed Dec 13 17:43:33 2000 +0100
12.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Wed Dec 13 17:46:49 2000 +0100
12.3 @@ -61,8 +61,9 @@
12.4 \isacommand{recdef} has been supplied with the congruence theorem
12.5 \isa{map{\isacharunderscore}cong}:
12.6 \begin{isabelle}%
12.7 -\ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
12.8 -\ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
12.9 +\ \ \ \ \ xs\ {\isacharequal}\ ys\ {\isasymLongrightarrow}\isanewline
12.10 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
12.11 +\ \ \ \ \ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
12.12 \end{isabelle}
12.13 Its second premise expresses (indirectly) that the second argument of
12.14 \isa{map} is only applied to elements of its third argument. Congruence
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/doc-src/TutorialI/Rules/document/root.tex Wed Dec 13 17:46:49 2000 +0100
13.3 @@ -0,0 +1,4 @@
13.4 +\documentclass{article}
13.5 +\begin{document}
13.6 +xxx
13.7 +\end{document}
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/doc-src/TutorialI/Sets/document/root.tex Wed Dec 13 17:46:49 2000 +0100
14.3 @@ -0,0 +1,4 @@
14.4 +\documentclass{article}
14.5 +\begin{document}
14.6 +xxx
14.7 +\end{document}
15.1 --- a/doc-src/TutorialI/Types/document/Axioms.tex Wed Dec 13 17:43:33 2000 +0100
15.2 +++ b/doc-src/TutorialI/Types/document/Axioms.tex Wed Dec 13 17:46:49 2000 +0100
15.3 @@ -68,8 +68,8 @@
15.4 specialized to type \isa{bool}, as subgoals:
15.5 \begin{isabelle}%
15.6 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline
15.7 -\ {\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
15.8 -\ {\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
15.9 +\ {\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
15.10 +\ {\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
15.11 \ {\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}%
15.12 \end{isabelle}
15.13 Fortunately, the proof is easy for blast, once we have unfolded the definitions
16.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex Wed Dec 13 17:43:33 2000 +0100
16.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Wed Dec 13 17:46:49 2000 +0100
16.3 @@ -75,12 +75,12 @@
16.4 %
16.5 \begin{isamarkuptext}%
16.6 \begin{isabelle}%
16.7 -\ \ \ \ \ {\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ k\ {\isasymle}\ l{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isasymle}\ j\ {\isacharasterisk}\ l%
16.8 +\ \ \ \ \ i\ {\isasymle}\ j\ {\isasymLongrightarrow}\ k\ {\isasymle}\ l\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isasymle}\ j\ {\isacharasterisk}\ l%
16.9 \end{isabelle}
16.10 \rulename{mult_le_mono}
16.11
16.12 \begin{isabelle}%
16.13 -\ \ \ \ \ {\isasymlbrakk}i\ {\isacharless}\ j{\isacharsemicolon}\ {\isadigit{0}}\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isacharless}\ j\ {\isacharasterisk}\ k%
16.14 +\ \ \ \ \ i\ {\isacharless}\ j\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ k\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isacharless}\ j\ {\isacharasterisk}\ k%
16.15 \end{isabelle}
16.16 \rulename{mult_less_mono1}
16.17
16.18 @@ -160,12 +160,12 @@
16.19 \rulename{DIVISION_BY_ZERO_MOD}
16.20
16.21 \begin{isabelle}%
16.22 -\ \ \ \ \ {\isasymlbrakk}m\ dvd\ n{\isacharsemicolon}\ n\ dvd\ m{\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n%
16.23 +\ \ \ \ \ m\ dvd\ n\ {\isasymLongrightarrow}\ n\ dvd\ m\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n%
16.24 \end{isabelle}
16.25 \rulename{dvd_anti_sym}
16.26
16.27 \begin{isabelle}%
16.28 -\ \ \ \ \ {\isasymlbrakk}k\ dvd\ m{\isacharsemicolon}\ k\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ k\ dvd\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}%
16.29 +\ \ \ \ \ k\ dvd\ m\ {\isasymLongrightarrow}\ k\ dvd\ n\ {\isasymLongrightarrow}\ k\ dvd\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}%
16.30 \end{isabelle}
16.31 \rulename{dvd_add}
16.32
17.1 --- a/doc-src/TutorialI/Types/document/Typedef.tex Wed Dec 13 17:43:33 2000 +0100
17.2 +++ b/doc-src/TutorialI/Types/document/Typedef.tex Wed Dec 13 17:46:49 2000 +0100
17.3 @@ -204,7 +204,7 @@
17.4 Expanding \isa{three{\isacharunderscore}def} yields the premise \isa{n\ {\isasymle}\ {\isadigit{2}}}. Repeated
17.5 elimination with \isa{le{\isacharunderscore}SucE}
17.6 \begin{isabelle}%
17.7 -\ \ \ \ \ {\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%
17.8 +\ \ \ \ \ {\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%
17.9 \end{isabelle}
17.10 reduces \isa{n\ {\isasymle}\ {\isadigit{2}}} to the three cases \isa{n\ {\isasymle}\ {\isadigit{0}}}, \isa{n\ {\isacharequal}\ {\isadigit{1}}} and
17.11 \isa{n\ {\isacharequal}\ {\isadigit{2}}} which are trivial for simplification:%
17.12 @@ -231,10 +231,10 @@
17.13 \isacommand{apply}{\isacharparenleft}rule\ cases{\isacharunderscore}lemma{\isacharparenright}%
17.14 \begin{isamarkuptxt}%
17.15 \begin{isabelle}%
17.16 -\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{0}}{\isacharparenright}\isanewline
17.17 -\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{1}}{\isacharparenright}\isanewline
17.18 -\ {\isadigit{3}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{2}}{\isacharparenright}\isanewline
17.19 -\ {\isadigit{4}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ x\ {\isasymin}\ three%
17.20 +\ {\isadigit{1}}{\isachardot}\ P\ A\ {\isasymLongrightarrow}\ P\ B\ {\isasymLongrightarrow}\ P\ C\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{0}}{\isacharparenright}\isanewline
17.21 +\ {\isadigit{2}}{\isachardot}\ P\ A\ {\isasymLongrightarrow}\ P\ B\ {\isasymLongrightarrow}\ P\ C\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{1}}{\isacharparenright}\isanewline
17.22 +\ {\isadigit{3}}{\isachardot}\ P\ A\ {\isasymLongrightarrow}\ P\ B\ {\isasymLongrightarrow}\ P\ C\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{2}}{\isacharparenright}\isanewline
17.23 +\ {\isadigit{4}}{\isachardot}\ P\ A\ {\isasymLongrightarrow}\ P\ B\ {\isasymLongrightarrow}\ P\ C\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ x\ {\isasymin}\ three%
17.24 \end{isabelle}
17.25 The resulting subgoals are easily solved by simplification:%
17.26 \end{isamarkuptxt}%