# HG changeset patch # User nipkow # Date 972044228 -7200 # Node ID ff003e2b790c1f09fe2c534ada25689f06b36752 # Parent b7d96e94796fd7c10fd65b853f39289d36abd5c6 *** empty log message *** diff -r b7d96e94796f -r ff003e2b790c doc-src/TutorialI/CTL/document/CTLind.tex --- 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 diff -r b7d96e94796f -r ff003e2b790c doc-src/TutorialI/Inductive/AB.thy --- 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\xs. P +filter} function on lists, which has the convenient syntax @{text"[x\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: diff -r b7d96e94796f -r ff003e2b790c doc-src/TutorialI/Inductive/document/AB.tex --- 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 intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val} @@ -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}% \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline \ {\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 diff -r b7d96e94796f -r ff003e2b790c doc-src/TutorialI/todo.tobias --- a/doc-src/TutorialI/todo.tobias Fri Oct 20 13:15:26 2000 +0200 +++ b/doc-src/TutorialI/todo.tobias Fri Oct 20 14:17:08 2000 +0200 @@ -59,6 +59,8 @@ Syntax section: syntax annotations nor just for consts but also for constdefs and datatype. +Appendix with list functions. + Minor additions to the tutorial, unclear where ==============================================