author nipkow Tue Oct 17 13:28:57 2000 +0200 (2000-10-17) changeset 10236 7626cb4e1407 parent 10235 20cf817f3b4a child 10237 875bf54b5d74
*** empty log message ***
     1.1 --- a/doc-src/TutorialI/Inductive/AB.thy	Tue Oct 17 10:45:51 2000 +0200
1.2 +++ b/doc-src/TutorialI/Inductive/AB.thy	Tue Oct 17 13:28:57 2000 +0200
1.3 @@ -2,122 +2,307 @@
1.4
1.5  section{*A context free grammar*}
1.6
1.7 +text{*
1.8 +Grammars are nothing but shorthands for inductive definitions of nonterminals
1.9 +which represent sets of strings. For example, the production
1.10 +$A \to B c$ is short for
1.11 +$w \in B \Longrightarrow wc \in A$
1.12 +This section demonstrates this idea with a standard example
1.13 +\cite[p.\ 81]{HopcroftUllman}, a grammar for generating all words with an
1.14 +equal number of $a$'s and $b$'s:
1.15 +\begin{eqnarray}
1.16 +S &\to& \epsilon \mid b A \mid a B \nonumber\\
1.17 +A &\to& a S \mid b A A \nonumber\\
1.18 +B &\to& b S \mid a B B \nonumber
1.19 +\end{eqnarray}
1.20 +At the end we say a few words about the relationship of the formalization
1.21 +and the text in the book~\cite[p.\ 81]{HopcroftUllman}.
1.22 +
1.23 +We start by fixing the alpgabet, which consists only of @{term a}'s
1.24 +and @{term b}'s:
1.25 +*}
1.26 +
1.27  datatype alfa = a | b;
1.28
1.29 -lemma [simp]: "(x ~= a) = (x = b) & (x ~= b) = (x = a)";
1.30 +text{*\noindent
1.31 +For convenience we includ the following easy lemmas as simplification rules:
1.32 +*}
1.33 +
1.34 +lemma [simp]: "(x \<noteq> a) = (x = b) \<and> (x \<noteq> b) = (x = a)";
1.35  apply(case_tac x);
1.36  by(auto);
1.37
1.38 +text{*\noindent
1.39 +Words over this alphabet are of type @{typ"alfa list"}, and
1.40 +the three nonterminals are declare as sets of such words:
1.41 +*}
1.42 +
1.43  consts S :: "alfa list set"
1.44         A :: "alfa list set"
1.45         B :: "alfa list set";
1.46
1.47 +text{*\noindent
1.48 +The above productions are recast as a \emph{simultaneous} inductive
1.49 +definition of @{term S}, @{term A} and @{term B}:
1.50 +*}
1.51 +
1.52  inductive S A B
1.53  intros
1.54 -"[] : S"
1.55 -"w : A ==> b#w : S"
1.56 -"w : B ==> a#w : S"
1.57 +  "[] \<in> S"
1.58 +  "w \<in> A \<Longrightarrow> b#w \<in> S"
1.59 +  "w \<in> B \<Longrightarrow> a#w \<in> S"
1.60
1.61 -"w : S ==> a#w : A"
1.62 -"[| v:A; w:A |] ==> b#v@w : A"
1.63 +  "w \<in> S        \<Longrightarrow> a#w   \<in> A"
1.64 +  "\<lbrakk> v\<in>A; w\<in>A \<rbrakk> \<Longrightarrow> b#v@w \<in> A"
1.65 +
1.66 +  "w \<in> S            \<Longrightarrow> b#w   \<in> B"
1.67 +  "\<lbrakk> v \<in> B; w \<in> B \<rbrakk> \<Longrightarrow> a#v@w \<in> B";
1.68
1.69 -"w : S ==> b#w : B"
1.70 -"[| v:B; w:B |] ==> a#v@w : B";
1.71 +text{*\noindent
1.72 +First we show that all words in @{term S} contain the same number of @{term
1.73 +a}'s and @{term b}'s. Since the definition of @{term S} is by simultaneous
1.74 +induction, so is this proof: we show at the same time that all words in
1.75 +@{term A} contain one more @{term a} than @{term b} and all words in @{term
1.76 +B} contains one more @{term b} than @{term a}.
1.77 +*}
1.78
1.79 -thm S_A_B.induct[no_vars];
1.80 +lemma correctness:
1.81 +  "(w \<in> S \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b])     \<and>
1.82 +    (w \<in> A \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1) \<and>
1.83 +    (w \<in> B \<longrightarrow> size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1)"
1.84
1.85 -lemma "(w : S --> size[x:w. x=a] = size[x:w. x=b]) &
1.86 -       (w : A --> size[x:w. x=a] = size[x:w. x=b] + 1) &
1.87 -       (w : B --> size[x:w. x=b] = size[x:w. x=a] + 1)";
1.88 +txt{*\noindent
1.89 +These propositions are expressed with the help of the predefined @{term
1.90 +filter} function on lists, which has the convenient syntax @{term"[x\<in>xs. P
1.91 +x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}
1.92 +holds. The length of a list is usually written @{term length}, and @{term
1.93 +size} is merely a shorthand.
1.94 +
1.95 +The proof itself is by rule induction and afterwards automatic:
1.96 +*}
1.97 +
1.98  apply(rule S_A_B.induct);
1.99  by(auto);
1.100
1.101 -lemma intermed_val[rule_format(no_asm)]:
1.102 - "(!i<n. abs(f(i+1) - f i) <= #1) -->
1.103 -  f 0 <= k & k <= f n --> (? i <= n. f i = (k::int))";
1.104 -apply(induct n);
1.105 - apply(simp);
1.106 - apply(arith);
1.107 -apply(rule);
1.108 -apply(erule impE);
1.109 - apply(simp);
1.110 -apply(rule);
1.111 -apply(erule_tac x = n in allE);
1.112 -apply(simp);
1.113 -apply(case_tac "k = f(n+1)");
1.114 - apply(force);
1.115 -apply(erule impE);
1.117 - apply(arith);
1.118 -by(blast intro:le_SucI);
1.119 +text{*\noindent
1.120 +This may seem surprising at first, and is indeed an indication of the power
1.121 +of inductive definitions. But it is also quite straightforward. For example,
1.122 +consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
1.123 +contain one more $a$ than $b$'s, then $bvw$ must again contain one more $a$
1.124 +than $b$'s.
1.125 +
1.126 +As usual, the correctness of syntactic descriptions is easy, but completeness
1.127 +is hard: does @{term S} contain \emph{all} words with an equal number of
1.128 +@{term a}'s and @{term b}'s? It turns out that this proof requires the
1.129 +following little lemma: every string with two more @{term a}'s than @{term
1.130 +b}'s can be cut somehwere such that each half has one more @{term a} than
1.131 +@{term b}. This is best seen by imagining counting the difference between the
1.132 +number of @{term a}'s than @{term b}'s starting at the left end of the
1.133 +word. We start at 0 and end (at the right end) with 2. Since each move to the
1.134 +right increases or decreases the difference by 1, we must have passed through
1.135 +1 on our way from 0 to 2. Formally, we appeal to the following discrete
1.136 +intermediate value theorem @{thm[source]nat0_intermed_int_val}
1.137 +@{thm[display]nat0_intermed_int_val[no_vars]}
1.138 +where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
1.139 +@{term abs} is the absolute value function, and @{term"#1::int"} is the
1.140 +integer 1 (see \S\ref{sec:int}).
1.141
1.142 -lemma step1: "ALL i < size w.
1.143 -  abs((int(size[x:take (i+1) w . P x]) - int(size[x:take (i+1) w . ~P x])) -
1.144 -      (int(size[x:take i w . P x]) - int(size[x:take i w . ~P x]))) <= #1";
1.145 +First we show that the our specific function, the difference between the
1.146 +numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every
1.147 +move to the right. At this point we also start generalizing from @{term a}'s
1.148 +and @{term b}'s to an arbitrary property @{term P}. Otherwise we would have
1.149 +to prove the desired lemma twice, once as stated above and once with the
1.150 +roles of @{term a}'s and @{term b}'s interchanged.
1.151 +*}
1.152 +
1.153 +lemma step1: "\<forall>i < size w.
1.154 +  abs((int(size[x\<in>take (i+1) w.  P x]) -
1.155 +       int(size[x\<in>take (i+1) w. \<not>P x]))
1.156 +      -
1.157 +      (int(size[x\<in>take i w.  P x]) -
1.158 +       int(size[x\<in>take i w. \<not>P x]))) <= #1";
1.159 +
1.160 +txt{*\noindent
1.161 +The lemma is a bit hard to read because of the coercion function
1.162 +@{term[source]"int::nat \<Rightarrow> int"}. It is required because @{term size} returns
1.163 +a natural number, but @{text-} on @{typ nat} will do the wrong thing.
1.164 +Function @{term take} is predefined and @{term"take i xs"} is the prefix of
1.165 +length @{term i} of @{term xs}; below we als need @{term"drop i xs"}, which
1.166 +is what remains after that prefix has been dropped from @{term xs}.
1.167 +
1.168 +The proof is by induction on @{term w}, with a trivial base case, and a not
1.169 +so trivial induction step. Since it is essentially just arithmetic, we do not
1.170 +discuss it.
1.171 +*}
1.172 +
1.173  apply(induct w);
1.174   apply(simp);
1.176 -apply(clarsimp);
1.177 -apply(rule conjI);
1.178 - apply(clarify);
1.179 - apply(erule allE);
1.180 - apply(erule impE);
1.181 -  apply(assumption);
1.182 - apply(arith);
1.183 -apply(clarify);
1.184 -apply(erule allE);
1.185 -apply(erule impE);
1.186 - apply(assumption);
1.187 -by(arith);
1.188 +by(force simp add:zabs_def take_Cons split:nat.split if_splits);
1.189
1.190 +text{*
1.191 +Finally we come to the above mentioned lemma about cutting a word with two
1.192 +more elements of one sort than of the other sort into two halfs:
1.193 +*}
1.194
1.195  lemma part1:
1.196 - "size[x:w. P x] = Suc(Suc(size[x:w. ~P x])) ==>
1.197 -  EX i<=size w. size[x:take i w. P x] = size[x:take i w. ~P x]+1";
1.198 -apply(insert intermed_val[OF step1, of "P" "w" "#1"]);
1.199 -apply(simp);
1.200 -apply(erule exE);
1.201 -apply(rule_tac x=i in exI);
1.202 -apply(simp);
1.203 -apply(rule int_int_eq[THEN iffD1]);
1.204 -apply(simp);
1.205 -by(arith);
1.206 + "size[x\<in>w. P x] = size[x\<in>w. \<not>P x]+2 \<Longrightarrow>
1.207 +  \<exists>i\<le>size w. size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1";
1.208 +
1.209 +txt{*\noindent
1.210 +This is proved with the help of the intermediate value theorem, instantiated
1.211 +appropriately and with its first premise disposed of by lemma
1.212 +@{thm[source]step1}.
1.213 +*}
1.214 +
1.215 +apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "#1"]);
1.216 +apply simp;
1.217 +by(simp del:int_Suc add:zdiff_eq_eq sym[OF int_Suc]);
1.218 +
1.219 +text{*\noindent
1.220 +The additional lemmas are needed to mediate between @{typ nat} and @{typ int}.
1.221 +
1.222 +Lemma @{thm[source]part1} tells us only about the prefix @{term"take i w"}.
1.223 +The suffix @{term"drop i w"} is dealt with in the following easy lemma:
1.224 +*}
1.225 +
1.226
1.227  lemma part2:
1.228 -"[| size[x:take i xs @ drop i xs. P x] = size[x:take i xs @ drop i xs. ~P x]+2;
1.229 -    size[x:take i xs. P x] = size[x:take i xs. ~P x]+1 |]
1.230 - ==> size[x:drop i xs. P x] = size[x:drop i xs. ~P x]+1";
1.231 +  "\<lbrakk>size[x\<in>take i w @ drop i w. P x] =
1.232 +    size[x\<in>take i w @ drop i w. \<not>P x]+2;
1.233 +    size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1\<rbrakk>
1.234 +   \<Longrightarrow> size[x\<in>drop i w. P x] = size[x\<in>drop i w. \<not>P x]+1";
1.235  by(simp del:append_take_drop_id);
1.236
1.237 -lemmas [simp] = S_A_B.intros;
1.238 +text{*\noindent
1.239 +Lemma @{thm[source]append_take_drop_id}, @{thm append_take_drop_id[no_vars]},
1.240 +which is generally useful, needs to be disabled for once.
1.241 +
1.242 +To dispose of trivial cases automatically, the rules of the inductive
1.243 +definition are declared simplification rules:
1.244 +*}
1.245 +
1.246 +declare S_A_B.intros[simp];
1.247 +
1.248 +text{*\noindent
1.249 +This could have been done earlier but was not necessary so far.
1.250 +
1.251 +The completeness theorem tells us that if a word has the same number of
1.252 +@{term a}'s and @{term b}'s, then it is in @{term S}, and similarly and
1.253 +simultaneously for @{term A} and @{term B}:
1.254 +*}
1.255 +
1.256 +theorem completeness:
1.257 +  "(size[x\<in>w. x=a] = size[x\<in>w. x=b]     \<longrightarrow> w \<in> S) \<and>
1.258 +    (size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
1.259 +    (size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1 \<longrightarrow> w \<in> B)";
1.260 +
1.261 +txt{*\noindent
1.262 +The proof is by induction on @{term w}. Structural induction would fail here
1.263 +because, as we can see from the grammar, we need to make bigger steps than
1.264 +merely appending a single letter at the front. Hence we induct on the length
1.265 +of @{term w}, using the induction rule @{thm[source]length_induct}:
1.266 +*}
1.267
1.268 -lemma "(size[x:w. x=a] = size[x:w. x=b] --> w : S) &
1.269 -       (size[x:w. x=a] = size[x:w. x=b] + 1 --> w : A) &
1.270 -       (size[x:w. x=b] = size[x:w. x=a] + 1 --> w : B)";
1.271  apply(induct_tac w rule: length_induct);
1.272 -apply(case_tac "xs");
1.273 - apply(simp);
1.274 -apply(simp);
1.275 +(*<*)apply(rename_tac w)(*>*)
1.276 +
1.277 +txt{*\noindent
1.278 +The @{text rule} parameter tells @{text induct_tac} explicitly which induction
1.279 +rule to use. For details see \S\ref{sec:complete-ind} below.
1.280 +In this case the result is that we may assume the lemma already
1.281 +holds for all words shorter than @{term w}.
1.282 +
1.283 +The proof continues with a case distinction on @{term w},
1.284 +i.e.\ if @{term w} is empty or not.
1.285 +*}
1.286 +
1.287 +apply(case_tac w);
1.288 + apply(simp_all);
1.289 +(*<*)apply(rename_tac x v)(*>*)
1.290 +
1.291 +txt{*\noindent
1.292 +Simplification disposes of the base case and leaves only two step
1.293 +cases to be proved:
1.294 +if @{prop"w = a#v"} and @{prop"size[x\<in>v. x=a] = size[x\<in>v. x=b]+2"} then
1.295 +@{prop"b#v \<in> A"}, and similarly for @{prop"w = b#v"}.
1.296 +We only consider the first case in detail.
1.297 +
1.298 +After breaking the conjuction up into two cases, we can apply
1.299 +@{thm[source]part1} to the assumption that @{term w} contains two more @{term
1.300 +a}'s than @{term b}'s.
1.301 +*}
1.302 +
1.303  apply(rule conjI);
1.304   apply(clarify);
1.305 - apply(frule part1[of "%x. x=a", simplified]);
1.306 + apply(frule part1[of "\<lambda>x. x=a", simplified]);
1.307   apply(erule exE);
1.308   apply(erule conjE);
1.309 - apply(drule part2[of "%x. x=a", simplified]);
1.310 +
1.311 +txt{*\noindent
1.312 +This yields an index @{prop"i \<le> length v"} such that
1.313 +@{prop"length [x\<in>take i v . x = a] = length [x\<in>take i v . x = b] + 1"}.
1.314 +With the help of @{thm[source]part1} it follows that
1.315 +@{prop"length [x\<in>drop i v . x = a] = length [x\<in>drop i v . x = b] + 1"}.
1.316 +*}
1.317 +
1.318 + apply(drule part2[of "\<lambda>x. x=a", simplified]);
1.319    apply(assumption);
1.320 - apply(rule_tac n1=i and t=list in subst[OF append_take_drop_id]);
1.321 +
1.322 +txt{*\noindent
1.323 +Now it is time to decompose @{term v} in the conclusion @{prop"b#v \<in> A"}
1.324 +into @{term"take i v @ drop i v"},
1.325 +after which the appropriate rule of the grammar reduces the goal
1.326 +to the two subgoals @{prop"take i v \<in> A"} and @{prop"drop i v \<in> A"}:
1.327 +*}
1.328 +
1.329 + apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id]);
1.330   apply(rule S_A_B.intros);
1.332 +
1.333 +txt{*\noindent
1.334 +Both subgoals follow from the induction hypothesis because both @{term"take i
1.335 +v"} and @{term"drop i v"} are shorter than @{term w}:
1.336 +*}
1.337 +
1.338 +  apply(force simp add: min_less_iff_disj);
1.340 +
1.341 +txt{*\noindent
1.342 +Note that the variables @{term n1} and @{term t} referred to in the
1.343 +substitution step above come from the derived theorem @{text"subst[OF
1.344 +append_take_drop_id]"}.
1.345 +
1.346 +The case @{prop"w = b#v"} is proved completely analogously:
1.347 +*}
1.348 +
1.349  apply(clarify);
1.350 -apply(frule part1[of "%x. x=b", simplified]);
1.351 +apply(frule part1[of "\<lambda>x. x=b", simplified]);
1.352  apply(erule exE);
1.353  apply(erule conjE);
1.354 -apply(drule part2[of "%x. x=b", simplified]);
1.355 +apply(drule part2[of "\<lambda>x. x=b", simplified]);
1.356   apply(assumption);
1.357 -apply(rule_tac n1=i and t=list in subst[OF append_take_drop_id]);
1.358 +apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id]);
1.359  apply(rule S_A_B.intros);
1.362
1.363 +text{*
1.364 +We conclude this section with a comparison of the above proof and the one
1.365 +in the textbook \cite[p.\ 81]{HopcroftUllman}. For a start, the texbook
1.366 +grammar, for no good reason, excludes the empty word, which complicates
1.367 +matters just a little bit because we now have 8 instead of our 7 productions.
1.368 +
1.369 +More importantly, the proof itself is different: rather than separating the
1.370 +two directions, they perform one induction on the length of a word. This
1.371 +deprives them of the beauty of rule induction and in the easy direction
1.372 +(correctness) their reasoning is more detailed than our @{text auto}. For the
1.373 +hard part (completeness), they consider just one of the cases that our @{text
1.374 +simp_all} disposes of automatically. Then they conclude the proof by saying
1.375 +about the remaining cases: We do this in a manner similar to our method of
1.376 +proof for part (1); this part is left to the reader''. But this is precisely
1.377 +the part that requires the intermediate value theorem and thus is not at all
1.378 +similar to the other cases (which are automatic in Isabelle). We conclude
1.380 +overlooked the slight difficulty lurking in the omitted cases. This is not
1.381 +atypical for pen-and-paper proofs, once analysed in detail.  *}
1.382 +
1.383  (*<*)end(*>*)

     2.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Tue Oct 17 10:45:51 2000 +0200
2.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Tue Oct 17 13:28:57 2000 +0200
2.3 @@ -3,123 +3,278 @@
2.4  \def\isabellecontext{AB}%
2.5  %
2.6  \isamarkupsection{A context free grammar}
2.7 -\isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b\isanewline
2.8 -\isanewline
2.9 -\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isachartilde}{\isacharequal}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isacharampersand}\ {\isacharparenleft}x\ {\isachartilde}{\isacharequal}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline
2.10 +%
2.11 +\begin{isamarkuptext}%
2.12 +Grammars are nothing but shorthands for inductive definitions of nonterminals
2.13 +which represent sets of strings. For example, the production
2.14 +$A \to B c$ is short for
2.15 +$w \in B \Longrightarrow wc \in A$
2.16 +This section demonstrates this idea with a standard example
2.17 +\cite[p.\ 81]{HopcroftUllman}, a grammar for generating all words with an
2.18 +equal number of $a$'s and $b$'s:
2.19 +\begin{eqnarray}
2.20 +S &\to& \epsilon \mid b A \mid a B \nonumber\\
2.21 +A &\to& a S \mid b A A \nonumber\\
2.22 +B &\to& b S \mid a B B \nonumber
2.23 +\end{eqnarray}
2.24 +At the end we say a few words about the relationship of the formalization
2.25 +and the text in the book~\cite[p.\ 81]{HopcroftUllman}.
2.26 +
2.27 +We start by fixing the alpgabet, which consists only of \isa{a}'s
2.28 +and \isa{b}'s:%
2.29 +\end{isamarkuptext}%
2.30 +\isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b%
2.31 +\begin{isamarkuptext}%
2.32 +\noindent
2.33 +For convenience we includ the following easy lemmas as simplification rules:%
2.34 +\end{isamarkuptext}%
2.35 +\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}x\ {\isasymnoteq}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline
2.36  \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharparenright}\isanewline
2.37 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
2.38 -\isanewline
2.39 +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
2.40 +\begin{isamarkuptext}%
2.41 +\noindent
2.42 +Words over this alphabet are of type \isa{alfa\ list}, and
2.43 +the three nonterminals are declare as sets of such words:%
2.44 +\end{isamarkuptext}%
2.45  \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
2.46  \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
2.47 -\ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
2.48 -\isanewline
2.49 +\ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}%
2.50 +\begin{isamarkuptext}%
2.51 +\noindent
2.52 +The above productions are recast as a \emph{simultaneous} inductive
2.53 +definition of \isa{S}, \isa{A} and \isa{B}:%
2.54 +\end{isamarkuptext}%
2.55  \isacommand{inductive}\ S\ A\ B\isanewline
2.56  \isakeyword{intros}\isanewline
2.57 -{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}\ S{\isachardoublequote}\isanewline
2.58 -{\isachardoublequote}w\ {\isacharcolon}\ A\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}w\ {\isacharcolon}\ S{\isachardoublequote}\isanewline
2.59 -{\isachardoublequote}w\ {\isacharcolon}\ B\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}w\ {\isacharcolon}\ S{\isachardoublequote}\isanewline
2.60 -\isanewline
2.61 -{\isachardoublequote}w\ {\isacharcolon}\ S\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}w\ {\isacharcolon}\ A{\isachardoublequote}\isanewline
2.62 -{\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ v{\isacharcolon}A{\isacharsemicolon}\ w{\isacharcolon}A\ {\isacharbar}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}v{\isacharat}w\ {\isacharcolon}\ A{\isachardoublequote}\isanewline
2.63 +\ \ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequote}\isanewline
2.64 +\ \ {\isachardoublequote}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
2.65 +\ \ {\isachardoublequote}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
2.66  \isanewline
2.67 -{\isachardoublequote}w\ {\isacharcolon}\ S\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}w\ {\isacharcolon}\ B{\isachardoublequote}\isanewline
2.68 -{\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ v{\isacharcolon}B{\isacharsemicolon}\ w{\isacharcolon}B\ {\isacharbar}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}v{\isacharat}w\ {\isacharcolon}\ B{\isachardoublequote}\isanewline
2.69 -\isanewline
2.70 -\isacommand{thm}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharbrackleft}no{\isacharunderscore}vars{\isacharbrackright}\isanewline
2.71 -\isanewline
2.72 -\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}w\ {\isacharcolon}\ S\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ {\isacharampersand}\isanewline
2.73 -\ \ \ \ \ \ \ {\isacharparenleft}w\ {\isacharcolon}\ A\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharampersand}\isanewline
2.74 -\ \ \ \ \ \ \ {\isacharparenleft}w\ {\isacharcolon}\ B\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
2.75 -\isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline
2.76 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
2.77 +\ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequote}\isanewline
2.78 +\ \ {\isachardoublequote}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequote}\isanewline
2.79  \isanewline
2.80 -\isacommand{lemma}\ intermed{\isacharunderscore}val{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
2.82 -\ \ f\ {\isadigit{0}}\ {\isacharless}{\isacharequal}\ k\ {\isacharampersand}\ k\ {\isacharless}{\isacharequal}\ f\ n\ {\isacharminus}{\isacharminus}{\isachargreater}\ {\isacharparenleft}{\isacharquery}\ i\ {\isacharless}{\isacharequal}\ n{\isachardot}\ f\ i\ {\isacharequal}\ {\isacharparenleft}k{\isacharcolon}{\isacharcolon}int{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
2.83 -\isacommand{apply}{\isacharparenleft}induct\ n{\isacharparenright}\isanewline
2.84 -\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
2.85 -\ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
2.86 -\isacommand{apply}{\isacharparenleft}rule{\isacharparenright}\isanewline
2.87 -\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
2.88 -\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
2.89 -\isacommand{apply}{\isacharparenleft}rule{\isacharparenright}\isanewline
2.90 -\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ n\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
2.91 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
2.93 -\ \isacommand{apply}{\isacharparenleft}force{\isacharparenright}\isanewline
2.94 -\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
2.96 -\ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
2.97 -\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}le{\isacharunderscore}SucI{\isacharparenright}\isanewline
2.98 -\isanewline
2.99 -\isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}ALL\ i\ {\isacharless}\ size\ w{\isachardot}\isanewline
2.100 -\ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w\ {\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\ int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w\ {\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharminus}\isanewline
2.101 -\ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ i\ w\ {\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\ int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ i\ w\ {\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}\isanewline
2.102 +\ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequote}\isanewline
2.103 +\ \ {\isachardoublequote}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequote}%
2.104 +\begin{isamarkuptext}%
2.105 +\noindent
2.106 +First we show that all words in \isa{S} contain the same number of \isa{a}'s and \isa{b}'s. Since the definition of \isa{S} is by simultaneous
2.107 +induction, so is this proof: we show at the same time that all words in
2.108 +\isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.%
2.109 +\end{isamarkuptext}%
2.110 +\isacommand{lemma}\ correctness{\isacharcolon}\isanewline
2.111 +\ \ {\isachardoublequote}{\isacharparenleft}w\ {\isasymin}\ S\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isasymand}\isanewline
2.112 +\ \ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline
2.113 +\ \ \ \ {\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}%
2.114 +\begin{isamarkuptxt}%
2.115 +\noindent
2.116 +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}
2.117 +holds. The length of a list is usually written \isa{size}, and \isa{size} is merely a shorthand.
2.118 +
2.119 +The proof itself is by rule induction and afterwards automatic:%
2.120 +\end{isamarkuptxt}%
2.121 +\isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline
2.122 +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
2.123 +\begin{isamarkuptext}%
2.124 +\noindent
2.125 +This may seem surprising at first, and is indeed an indication of the power
2.126 +of inductive definitions. But it is also quite straightforward. For example,
2.127 +consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
2.128 +contain one more $a$ than $b$'s, then $bvw$ must again contain one more $a$
2.129 +than $b$'s.
2.130 +
2.131 +As usual, the correctness of syntactic descriptions is easy, but completeness
2.132 +is hard: does \isa{S} contain \emph{all} words with an equal number of
2.133 +\isa{a}'s and \isa{b}'s? It turns out that this proof requires the
2.134 +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
2.135 +\isa{b}. This is best seen by imagining counting the difference between the
2.136 +number of \isa{a}'s than \isa{b}'s starting at the left end of the
2.137 +word. We start at 0 and end (at the right end) with 2. Since each move to the
2.138 +right increases or decreases the difference by 1, we must have passed through
2.139 +1 on our way from 0 to 2. Formally, we appeal to the following discrete
2.141 +\begin{isabelle}%
2.142 +\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ abs\ {\isacharparenleft}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
2.143 +\ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
2.144 +\end{isabelle}
2.145 +where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
2.146 +\isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
2.147 +integer 1 (see \S\ref{sec:int}).
2.148 +
2.149 +First we show that the our specific function, the difference between the
2.150 +numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
2.151 +move to the right. At this point we also start generalizing from \isa{a}'s
2.152 +and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
2.153 +to prove the desired lemma twice, once as stated above and once with the
2.154 +roles of \isa{a}'s and \isa{b}'s interchanged.%
2.155 +\end{isamarkuptext}%
2.156 +\isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
2.157 +\ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
2.158 +\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
2.159 +\ \ \ \ \ \ {\isacharminus}\isanewline
2.160 +\ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
2.161 +\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
2.162 +\begin{isamarkuptxt}%
2.163 +\noindent
2.164 +The lemma is a bit hard to read because of the coercion function
2.165 +\isa{{\isachardoublequote}int{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
2.166 +a natural number, but \isa{{\isacharminus}} on \isa{nat} will do the wrong thing.
2.167 +Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
2.168 +length \isa{i} of \isa{xs}; below we als need \isa{drop\ i\ xs}, which
2.169 +is what remains after that prefix has been dropped from \isa{xs}.
2.170 +
2.171 +The proof is by induction on \isa{w}, with a trivial base case, and a not
2.172 +so trivial induction step. Since it is essentially just arithmetic, we do not
2.173 +discuss it.%
2.174 +\end{isamarkuptxt}%
2.175  \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline
2.176  \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
2.178 -\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline
2.179 +\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}%
2.180 +\begin{isamarkuptext}%
2.181 +Finally we come to the above mentioned lemma about cutting a word with two
2.182 +more elements of one sort than of the other sort into two halfs:%
2.183 +\end{isamarkuptext}%
2.185 +\ {\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
2.186 +\ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}%
2.187 +\begin{isamarkuptxt}%
2.188 +\noindent
2.189 +This is proved with the help of the intermediate value theorem, instantiated
2.190 +appropriately and with its first premise disposed of by lemma
2.192 +\end{isamarkuptxt}%
2.194 +\isacommand{apply}\ simp\isanewline
2.195 +\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}int{\isacharunderscore}Suc\ add{\isacharcolon}zdiff{\isacharunderscore}eq{\isacharunderscore}eq\ sym{\isacharbrackleft}OF\ int{\isacharunderscore}Suc{\isacharbrackright}{\isacharparenright}%
2.196 +\begin{isamarkuptext}%
2.197 +\noindent
2.198 +The additional lemmas are needed to mediate between \isa{nat} and \isa{int}.
2.199 +
2.200 +Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
2.201 +The suffix \isa{drop\ i\ w} is dealt with in the following easy lemma:%
2.202 +\end{isamarkuptext}%
2.204 +\ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline
2.205 +\ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
2.206 +\ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isasymrbrakk}\isanewline
2.207 +\ \ \ {\isasymLongrightarrow}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline
2.208 +\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}%
2.209 +\begin{isamarkuptext}%
2.210 +\noindent
2.211 +Lemma \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}, \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs},
2.212 +which is generally useful, needs to be disabled for once.
2.213 +
2.214 +To dispose of trivial cases automatically, the rules of the inductive
2.215 +definition are declared simplification rules:%
2.216 +\end{isamarkuptext}%
2.217 +\isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}%
2.218 +\begin{isamarkuptext}%
2.219 +\noindent
2.220 +This could have been done earlier but was not necessary so far.
2.221 +
2.222 +The completeness theorem tells us that if a word has the same number of
2.223 +\isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly and
2.224 +simultaneously for \isa{A} and \isa{B}:%
2.225 +\end{isamarkuptext}%
2.226 +\isacommand{theorem}\ completeness{\isacharcolon}\isanewline
2.227 +\ \ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline
2.228 +\ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline
2.229 +\ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}%
2.230 +\begin{isamarkuptxt}%
2.231 +\noindent
2.232 +The proof is by induction on \isa{w}. Structural induction would fail here
2.233 +because, as we can see from the grammar, we need to make bigger steps than
2.234 +merely appending a single letter at the front. Hence we induct on the length
2.235 +of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:%
2.236 +\end{isamarkuptxt}%
2.237 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}%
2.238 +\begin{isamarkuptxt}%
2.239 +\noindent
2.240 +The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction
2.241 +rule to use. For details see \S\ref{sec:complete-ind} below.
2.242 +In this case the result is that we may assume the lemma already
2.243 +holds for all words shorter than \isa{w}.
2.244 +
2.245 +The proof continues with a case distinction on \isa{w},
2.246 +i.e.\ if \isa{w} is empty or not.%
2.247 +\end{isamarkuptxt}%
2.248 +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
2.249 +\ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
2.250 +\begin{isamarkuptxt}%
2.251 +\noindent
2.252 +Simplification disposes of the base case and leaves only two step
2.253 +cases to be proved:
2.254 +if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \isa{length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{2}}} then
2.255 +\isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}.
2.256 +We only consider the first case in detail.
2.257 +
2.258 +After breaking the conjuction up into two cases, we can apply
2.259 +\isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.%
2.260 +\end{isamarkuptxt}%
2.261  \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
2.262  \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
2.263 -\ \isacommand{apply}{\isacharparenleft}erule\ allE{\isacharparenright}\isanewline
2.264 -\ \isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
2.265 -\ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
2.266 -\ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
2.267 +\ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
2.268 +\ \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
2.269 +\ \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}%
2.270 +\begin{isamarkuptxt}%
2.271 +\noindent
2.272 +This yields an index \isa{i\ {\isasymle}\ length\ v} such that
2.273 +\isa{length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}}.
2.274 +With the help of \isa{part{\isadigit{1}}} it follows that
2.275 +\isa{length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}}.%
2.276 +\end{isamarkuptxt}%
2.277 +\ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
2.278 +\ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}%
2.279 +\begin{isamarkuptxt}%
2.280 +\noindent
2.281 +Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}
2.282 +into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},
2.283 +after which the appropriate rule of the grammar reduces the goal
2.284 +to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:%
2.285 +\end{isamarkuptxt}%
2.286 +\ \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline
2.287 +\ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}%
2.288 +\begin{isamarkuptxt}%
2.289 +\noindent
2.290 +Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:%
2.291 +\end{isamarkuptxt}%
2.292 +\ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
2.293 +\ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
2.294 +\begin{isamarkuptxt}%
2.295 +\noindent
2.296 +Note that the variables \isa{n{\isadigit{1}}} and \isa{t} referred to in the
2.297 +substitution step above come from the derived theorem \isa{subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}}.
2.298 +
2.299 +The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved completely analogously:%
2.300 +\end{isamarkuptxt}%
2.301  \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
2.302 -\isacommand{apply}{\isacharparenleft}erule\ allE{\isacharparenright}\isanewline
2.303 -\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
2.304 -\ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
2.305 -\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
2.306 -\isanewline
2.307 -\isanewline
2.309 -\ {\isachardoublequote}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ Suc{\isacharparenleft}Suc{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}{\isacharequal}{\isachargreater}\isanewline
2.310 -\ \ EX\ i{\isacharless}{\isacharequal}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ w{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline
2.312 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
2.313 -\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
2.314 -\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}i\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
2.315 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
2.317 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
2.318 -\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
2.319 -\isanewline
2.321 -{\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs\ {\isacharat}\ drop\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs\ {\isacharat}\ drop\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
2.322 -\ \ \ \ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}\ {\isacharbar}{\isacharbrackright}\isanewline
2.323 -\ {\isacharequal}{\isacharequal}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}drop\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}drop\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline
2.324 -\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}\isanewline
2.325 -\isanewline
2.326 -\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros\isanewline
2.327 -\isanewline
2.328 -\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ S{\isacharparenright}\ {\isacharampersand}\isanewline
2.329 -\ \ \ \ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ A{\isacharparenright}\ {\isacharampersand}\isanewline
2.330 -\ \ \ \ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ B{\isacharparenright}{\isachardoublequote}\isanewline
2.331 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isanewline
2.332 -\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequote}xs{\isachardoublequote}{\isacharparenright}\isanewline
2.333 -\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
2.334 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
2.335 -\isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
2.336 -\ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
2.337 -\ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
2.338 -\ \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
2.339 -\ \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline
2.340 -\ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
2.341 -\ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
2.342 -\ \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}list\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline
2.343 -\ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
2.344 -\ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
2.345 -\ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
2.346 -\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
2.347 -\isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
2.348 +\isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
2.349  \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
2.350  \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline
2.351 -\isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
2.352 +\isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
2.353  \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
2.354 -\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}list\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline
2.355 +\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline
2.356  \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
2.360 +\begin{isamarkuptext}%
2.361 +We conclude this section with a comparison of the above proof and the one
2.362 +in the textbook \cite[p.\ 81]{HopcroftUllman}. For a start, the texbook
2.363 +grammar, for no good reason, excludes the empty word, which complicates
2.364 +matters just a little bit because we now have 8 instead of our 7 productions.
2.365 +
2.366 +More importantly, the proof itself is different: rather than separating the
2.367 +two directions, they perform one induction on the length of a word. This
2.368 +deprives them of the beauty of rule induction and in the easy direction
2.369 +(correctness) their reasoning is more detailed than our \isa{auto}. For the
2.370 +hard part (completeness), they consider just one of the cases that our \isa{simp{\isacharunderscore}all} disposes of automatically. Then they conclude the proof by saying
2.371 +about the remaining cases: We do this in a manner similar to our method of
2.372 +proof for part (1); this part is left to the reader''. But this is precisely
2.373 +the part that requires the intermediate value theorem and thus is not at all
2.374 +similar to the other cases (which are automatic in Isabelle). We conclude
2.376 +overlooked the slight difficulty lurking in the omitted cases. This is not
2.377 +atypical for pen-and-paper proofs, once analysed in detail.%
2.378 +\end{isamarkuptext}%
2.379  \end{isabellebody}%
2.380  %%% Local Variables:
2.381  %%% mode: latex

     3.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Oct 17 10:45:51 2000 +0200
3.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Oct 17 13:28:57 2000 +0200
3.3 @@ -231,13 +231,17 @@
3.4  identity.
3.5  \end{exercise}
3.6
3.7 -In general, @{text"induct_tac"} can be applied with any rule $r$
3.8 +In general, @{text induct_tac} can be applied with any rule $r$
3.9  whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
3.10  format is
3.11  \begin{quote}
3.12  \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}
3.13  \end{quote}\index{*induct_tac}%
3.14  where $y@1, \dots, y@n$ are variables in the first subgoal.
3.15 +A further example of a useful induction rule is @{thm[source]length_induct},
3.16 +induction on the length of a list:\indexbold{*length_induct}
3.17 +@{thm[display]length_induct[no_vars]}
3.18 +
3.19  In fact, @{text"induct_tac"} even allows the conclusion of
3.20  $r$ to be an (iterated) conjunction of formulae of the above form, in
3.21  which case the application is

     4.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Oct 17 10:45:51 2000 +0200
4.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Oct 17 13:28:57 2000 +0200
4.3 @@ -216,6 +216,12 @@
4.4  \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
4.5  \end{quote}\index{*induct_tac}%
4.6  where $y@1, \dots, y@n$ are variables in the first subgoal.
4.7 +A further example of a useful induction rule is \isa{length{\isacharunderscore}induct},
4.8 +induction on the length of a list:\indexbold{*length_induct}
4.9 +\begin{isabelle}%
4.10 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}xs{\isachardot}\ {\isasymforall}ys{\isachardot}\ length\ ys\ {\isacharless}\ length\ xs\ {\isasymlongrightarrow}\ P\ ys\ {\isasymLongrightarrow}\ P\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xs%
4.11 +\end{isabelle}
4.12 +
4.13  In fact, \isa{induct{\isacharunderscore}tac} even allows the conclusion of
4.14  $r$ to be an (iterated) conjunction of formulae of the above form, in
4.15  which case the application is

     5.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Tue Oct 17 10:45:51 2000 +0200
5.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Tue Oct 17 13:28:57 2000 +0200
5.3 @@ -40,8 +40,8 @@
5.4  Next, two functions @{text"app"} and \isaindexbold{rev} are declared:
5.5  *}
5.6
5.7 -consts app :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list"   (infixr "@" 65)
5.8 -       rev :: "'a list \\<Rightarrow> 'a list";
5.9 +consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"   (infixr "@" 65)
5.10 +       rev :: "'a list \<Rightarrow> 'a list";
5.11
5.12  text{*
5.13  \noindent
5.14 @@ -100,7 +100,7 @@
5.15  dropped, unless the identifier happens to be a keyword, as in
5.16  *}
5.17
5.18 -consts "end" :: "'a list \\<Rightarrow> 'a"
5.19 +consts "end" :: "'a list \<Rightarrow> 'a"
5.20
5.21  text{*\noindent
5.22  When Isabelle prints a syntax error message, it refers to the HOL syntax as
5.23 @@ -188,7 +188,7 @@
5.24  \end{isabelle}
5.25  The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
5.26  ignored most of the time, or simply treated as a list of variables local to
5.27 -this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.
5.28 +this subgoal. Their deeper significance is explained in Chapter~\ref{ch:Rules}.
5.29  The {\it assumptions} are the local assumptions for this subgoal and {\it
5.30    conclusion} is the actual proposition to be proved. Typical proof steps
5.31  that add new assumptions are induction or case distinction. In our example

     6.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Oct 17 10:45:51 2000 +0200
6.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Oct 17 13:28:57 2000 +0200
6.3 @@ -183,7 +183,7 @@
6.4  \end{isabelle}
6.5  The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
6.6  ignored most of the time, or simply treated as a list of variables local to
6.7 -this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.
6.8 +this subgoal. Their deeper significance is explained in Chapter~\ref{ch:Rules}.
6.9  The {\it assumptions} are the local assumptions for this subgoal and {\it
6.10    conclusion} is the actual proposition to be proved. Typical proof steps
6.11  that add new assumptions are induction or case distinction. In our example

     7.1 --- a/doc-src/TutorialI/todo.tobias	Tue Oct 17 10:45:51 2000 +0200
7.2 +++ b/doc-src/TutorialI/todo.tobias	Tue Oct 17 13:28:57 2000 +0200
7.3 @@ -36,6 +36,8 @@
7.4
7.5  it would be nice if one could get id to the enclosing quotes in the [source] option.
7.6
7.7 +arithmetic: allow mixed nat/int formulae
7.8 +-> simplify proof of part1 in Inductive/AB.thy
7.9
7.10  Minor fixes in the tutorial
7.11  ===========================

     8.1 --- a/doc-src/TutorialI/tutorial.tex	Tue Oct 17 10:45:51 2000 +0200
8.2 +++ b/doc-src/TutorialI/tutorial.tex	Tue Oct 17 13:28:57 2000 +0200
8.3 @@ -66,6 +66,7 @@
8.4  \input{basics}
8.5  \input{fp}
8.6  \chapter{The Rules of the Game}
8.7 +\label{ch:Rules}
8.8  \input{sets}
8.9  \input{Inductive/inductive}