# HG changeset patch # User paulson # Date 979313294 -3600 # Node ID 2995639c6a099ad1529a47aa75cc331563cc9cd7 # Parent 2b9f87bf91131b3fcb0887a1e8469556403fa2d2 renaming of some files diff -r 2b9f87bf9113 -r 2995639c6a09 doc-src/TutorialI/Inductive/AB.thy --- a/doc-src/TutorialI/Inductive/AB.thy Fri Jan 12 16:19:44 2001 +0100 +++ b/doc-src/TutorialI/Inductive/AB.thy Fri Jan 12 16:28:14 2001 +0100 @@ -1,25 +1,25 @@ (*<*)theory AB = Main:(*>*) -section{*Case study: A context free grammar*} +section{*Case Study: A Context Free Grammar*} text{*\label{sec:CFG} Grammars are nothing but shorthands for inductive definitions of nonterminals which represent sets of strings. For example, the production $A \to B c$ is short for \[ w \in B \Longrightarrow wc \in A \] -This section demonstrates this idea with a standard example -\cite[p.\ 81]{HopcroftUllman}, a grammar for generating all words with an -equal number of $a$'s and $b$'s: +This section demonstrates this idea with an example +due to Hopcroft and Ullman, a grammar for generating all words with an +equal number of $a$'s and~$b$'s: \begin{eqnarray} S &\to& \epsilon \mid b A \mid a B \nonumber\\ A &\to& a S \mid b A A \nonumber\\ B &\to& b S \mid a B B \nonumber \end{eqnarray} -At the end we say a few words about the relationship of the formalization -and the text in the book~\cite[p.\ 81]{HopcroftUllman}. +At the end we say a few words about the relationship between +the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version. We start by fixing the alphabet, which consists only of @{term a}'s -and @{term b}'s: +and~@{term b}'s: *} datatype alfa = a | b; @@ -29,12 +29,11 @@ *} lemma [simp]: "(x \ a) = (x = b) \ (x \ b) = (x = a)"; -apply(case_tac x); -by(auto); +by (case_tac x, auto) text{*\noindent Words over this alphabet are of type @{typ"alfa list"}, and -the three nonterminals are declare as sets of such words: +the three nonterminals are declared as sets of such words: *} consts S :: "alfa list set" @@ -42,9 +41,9 @@ B :: "alfa list set"; text{*\noindent -The above productions are recast as a \emph{simultaneous} inductive +The productions above are recast as a \emph{mutual} inductive definition\index{inductive definition!simultaneous} -of @{term S}, @{term A} and @{term B}: +of @{term S}, @{term A} and~@{term B}: *} inductive S A B @@ -61,8 +60,8 @@ text{*\noindent First we show that all words in @{term S} contain the same number of @{term -a}'s and @{term b}'s. Since the definition of @{term S} is by simultaneous -induction, so is this proof: we show at the same time that all words in +a}'s and @{term b}'s. Since the definition of @{term S} is by mutual +induction, so is the proof: we show at the same time that all words in @{term A} contain one more @{term a} than @{term b} and all words in @{term B} contains one more @{term b} than @{term a}. *} @@ -76,26 +75,25 @@ These propositions are expressed with the help of the predefined @{term 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. +holds. Remember that on lists @{text size} and @{text length} are synonymous. The proof itself is by rule induction and afterwards automatic: *} -apply(rule S_A_B.induct); -by(auto); +by (rule S_A_B.induct, auto) text{*\noindent This may seem surprising at first, and is indeed an indication of the power of inductive definitions. But it is also quite straightforward. For example, consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$ -contain one more $a$ than $b$'s, then $bvw$ must again contain one more $a$ -than $b$'s. +contain one more $a$ than~$b$'s, then $bvw$ must again contain one more $a$ +than~$b$'s. As usual, the correctness of syntactic descriptions is easy, but completeness is hard: does @{term S} contain \emph{all} words with an equal number of @{term a}'s and @{term b}'s? It turns out that this proof requires the -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 +following lemma: every string with two more @{term a}'s than @{term +b}'s can be cut somewhere 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 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 @@ -122,9 +120,9 @@ txt{*\noindent The lemma is a bit hard to read because of the coercion function @{term[source]"int :: nat \ int"}. It is required because @{term size} returns -a natural number, but @{text-} on @{typ nat} will do the wrong thing. +a natural number, but subtraction on type~@{typ nat} will do the wrong thing. Function @{term take} is predefined and @{term"take i xs"} is the prefix of -length @{term i} of @{term xs}; below we als need @{term"drop i xs"}, which +length @{term i} of @{term xs}; below we also need @{term"drop i xs"}, which is what remains after that prefix has been dropped from @{term xs}. The proof is by induction on @{term w}, with a trivial base case, and a not @@ -137,8 +135,8 @@ by(force simp add:zabs_def take_Cons split:nat.split if_splits); 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 halves: +Finally we come to the above mentioned lemma about cutting in half a word with two +more elements of one sort than of the other sort: *} lemma part1: @@ -146,7 +144,7 @@ \i\size w. size[x\take i w. P x] = size[x\take i w. \P x]+1"; txt{*\noindent -This is proved by force with the help of the intermediate value theorem, +This is proved by @{text force} with the help of the intermediate value theorem, instantiated appropriately and with its first premise disposed of by lemma @{thm[source]step1}: *} @@ -157,7 +155,7 @@ text{*\noindent Lemma @{thm[source]part1} tells us only about the prefix @{term"take i w"}. -The suffix @{term"drop i w"} is dealt with in the following easy lemma: +An easy lemma deals with the suffix @{term"drop i w"}: *} @@ -169,8 +167,11 @@ by(simp del:append_take_drop_id); text{*\noindent -Lemma @{thm[source]append_take_drop_id}, @{thm append_take_drop_id[no_vars]}, -which is generally useful, needs to be disabled for once. +In the proof, we have had to disable a normally useful lemma: +\begin{isabelle} +@{thm append_take_drop_id[no_vars]} +\rulename{append_take_drop_id} +\end{isabelle} To dispose of trivial cases automatically, the rules of the inductive definition are declared simplification rules: @@ -182,8 +183,8 @@ This could have been done earlier but was not necessary so far. The completeness theorem tells us that if a word has the same number of -@{term a}'s and @{term b}'s, then it is in @{term S}, and similarly and -simultaneously for @{term A} and @{term B}: +@{term a}'s and @{term b}'s, then it is in @{term S}, and similarly +for @{term A} and @{term B}: *} theorem completeness: @@ -218,7 +219,7 @@ txt{*\noindent Simplification disposes of the base case and leaves only two step cases to be proved: -if @{prop"w = a#v"} and @{prop"size[x\v. x=a] = size[x\v. x=b]+2"} then +if @{prop"w = a#v"} and @{prop[display]"size[x\v. x=a] = size[x\v. x=b]+2"} then @{prop"b#v \ A"}, and similarly for @{prop"w = b#v"}. We only consider the first case in detail. @@ -235,9 +236,9 @@ txt{*\noindent This yields an index @{prop"i \ length v"} such that -@{prop"length [x\take i v . x = a] = length [x\take i v . x = b] + 1"}. +@{prop[display]"length [x\take i v . x = a] = length [x\take i v . x = b] + 1"} With the help of @{thm[source]part1} it follows that -@{prop"length [x\drop i v . x = a] = length [x\drop i v . x = b] + 1"}. +@{prop[display]"length [x\drop i v . x = a] = length [x\drop i v . x = b] + 1"} *} apply(drule part2[of "\x. x=a", simplified]); @@ -266,7 +267,7 @@ substitution step above come from the derived theorem @{text"subst[OF append_take_drop_id]"}. -The case @{prop"w = b#v"} is proved completely analogously: +The case @{prop"w = b#v"} is proved analogously: *} apply(clarify); @@ -281,9 +282,9 @@ by(force simp add:min_less_iff_disj split add: nat_diff_split); text{* -We conclude this section with a comparison of the above proof and the one -in the textbook \cite[p.\ 81]{HopcroftUllman}. For a start, the texbook -grammar, for no good reason, excludes the empty word, which complicates +We conclude this section with a comparison of our proof with +Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the texbook +grammar, for no good reason, excludes the empty word. That complicates matters just a little bit because we now have 8 instead of our 7 productions. More importantly, the proof itself is different: rather than separating the diff -r 2b9f87bf9113 -r 2995639c6a09 doc-src/TutorialI/Inductive/Mutual.thy --- a/doc-src/TutorialI/Inductive/Mutual.thy Fri Jan 12 16:19:44 2001 +0100 +++ b/doc-src/TutorialI/Inductive/Mutual.thy Fri Jan 12 16:28:14 2001 +0100 @@ -1,6 +1,6 @@ (*<*)theory Mutual = Main:(*>*) -subsection{*Mutually inductive definitions*} +subsection{*Mutually Inductive Definitions*} text{* Just as there are datatypes defined by mutual recursion, there are sets defined diff -r 2b9f87bf9113 -r 2995639c6a09 doc-src/TutorialI/Inductive/inductive.tex --- a/doc-src/TutorialI/Inductive/inductive.tex Fri Jan 12 16:19:44 2001 +0100 +++ b/doc-src/TutorialI/Inductive/inductive.tex Fri Jan 12 16:28:14 2001 +0100 @@ -13,12 +13,12 @@ from the realm of context-free grammars. The chapter closes with a discussion of advanced forms of inductive definitions. -\input{Inductive/Even} +\input{Inductive/even-example} \input{Inductive/document/Mutual} \input{Inductive/document/Star} \section{Advanced inductive definitions} -\input{Inductive/Advanced} +\input{Inductive/advanced-examples} \input{Inductive/document/AB}