author nipkow Fri, 20 Oct 2000 14:17:08 +0200 changeset 10283 ff003e2b790c parent 10282 b7d96e94796f child 10284 ec98fc455272
*** empty log message ***
 doc-src/TutorialI/CTL/document/CTLind.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/Inductive/AB.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Inductive/document/AB.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/todo.tobias file | annotate | diff | comparison | revisions
--- a/doc-src/TutorialI/CTL/document/CTLind.tex	Fri Oct 20 13:15:26 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Fri Oct 20 14:17:08 2000 +0200
@@ -6,12 +6,15 @@
%
\begin{isamarkuptext}%
\label{sec:CTL-revisited}
+The purpose of this section is twofold: we want to demonstrate
+some of the induction principles and heuristics discussed above and we want to
+show how inductive definitions can simplify proofs.
In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
model checker for CTL. In particular the proof of the
\isa{infinity{\isacharunderscore}lemma} on the way to \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} is not as
simple as one might intuitively expect, due to the \isa{SOME} operator
-involved. The purpose of this section is to show how an inductive definition
-can help to simplify the proof of \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}.
+involved. Below we give a simpler proof of \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}
+based on an auxiliary inductive definition.

Let us call a (finite or infinite) path \emph{\isa{A}-avoiding} if it does
not touch any node in the set \isa{A}. Then \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} says
--- a/doc-src/TutorialI/Inductive/AB.thy	Fri Oct 20 13:15:26 2000 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy	Fri Oct 20 14:17:08 2000 +0200
@@ -74,7 +74,7 @@

txt{*\noindent
These propositions are expressed with the help of the predefined @{term
-filter} function on lists, which has the convenient syntax @{term"[x\<in>xs. P
+filter} function on lists, which has the convenient syntax @{text"[x\<in>xs. P
x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}
holds. Remember that on lists @{term size} and @{term length} are synonymous.

@@ -97,8 +97,8 @@
following little lemma: every string with two more @{term a}'s than @{term
b}'s can be cut somehwere such that each half has one more @{term a} than
@{term b}. This is best seen by imagining counting the difference between the
-number of @{term a}'s than @{term b}'s starting at the left end of the
-word. We start at 0 and end (at the right end) with 2. Since each move to the
+number of @{term a}'s and @{term b}'s starting at the left end of the
+word. We start with 0 and end (at the right end) with 2. Since each move to the
right increases or decreases the difference by 1, we must have passed through
1 on our way from 0 to 2. Formally, we appeal to the following discrete
intermediate value theorem @{thm[source]nat0_intermed_int_val}
@@ -141,7 +141,7 @@

text{*
Finally we come to the above mentioned lemma about cutting a word with two
-more elements of one sort than of the other sort into two halfs:
+more elements of one sort than of the other sort into two halves:
*}

lemma part1:
--- a/doc-src/TutorialI/Inductive/document/AB.tex	Fri Oct 20 13:15:26 2000 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Fri Oct 20 14:17:08 2000 +0200
@@ -69,7 +69,7 @@
\ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{filter\ P\ xs}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x}
+These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isacharbrackleft}x{\isasymin}xs{\isachardot}\ P\ x{\isacharbrackright}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x}
holds. Remember that on lists \isa{size} and \isa{size} are synonymous.

The proof itself is by rule induction and afterwards automatic:%
@@ -89,8 +89,8 @@
\isa{a}'s and \isa{b}'s? It turns out that this proof requires the
following little lemma: every string with two more \isa{a}'s than \isa{b}'s can be cut somehwere such that each half has one more \isa{a} than
\isa{b}. This is best seen by imagining counting the difference between the
-number of \isa{a}'s than \isa{b}'s starting at the left end of the
-word. We start at 0 and end (at the right end) with 2. Since each move to the
+number of \isa{a}'s and \isa{b}'s starting at the left end of the
+word. We start with 0 and end (at the right end) with 2. Since each move to the
right increases or decreases the difference by 1, we must have passed through
1 on our way from 0 to 2. Formally, we appeal to the following discrete
@@ -133,7 +133,7 @@
\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}%
\begin{isamarkuptext}%
Finally we come to the above mentioned lemma about cutting a word with two
-more elements of one sort than of the other sort into two halfs:%
+more elements of one sort than of the other sort into two halves:%
\end{isamarkuptext}%
\ {\isachardoublequote}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline
--- a/doc-src/TutorialI/todo.tobias	Fri Oct 20 13:15:26 2000 +0200
==============================================