*** empty log message ***
authornipkow
Tue Oct 17 13:28:57 2000 +0200 (2000-10-17)
changeset 102367626cb4e1407
parent 10235 20cf817f3b4a
child 10237 875bf54b5d74
*** empty log message ***
doc-src/TutorialI/Inductive/AB.thy
doc-src/TutorialI/Inductive/document/AB.tex
doc-src/TutorialI/Misc/AdvancedInd.thy
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/todo.tobias
doc-src/TutorialI/tutorial.tex
     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.116 - apply(simp add:zabs_def split:split_if_asm);
   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.175 -apply(simp add:take_Cons split:nat.split);
   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.331 -  apply(force simp add:min_less_iff_disj);
   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.339   apply(force split add: nat_diff_split);
   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.360   apply(force simp add:min_less_iff_disj);
   1.361  by(force simp add:min_less_iff_disj split add: nat_diff_split);
   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.379 +that the authors are at least cavalier about this point and may even have
   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.81 -\ {\isachardoublequote}{\isacharparenleft}{\isacharbang}i{\isacharless}n{\isachardot}\ abs{\isacharparenleft}f{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isacharparenright}\ {\isacharminus}{\isacharminus}{\isachargreater}\ \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.92 -\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequote}k\ {\isacharequal}\ f{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isanewline
    2.93 -\ \isacommand{apply}{\isacharparenleft}force{\isacharparenright}\isanewline
    2.94 -\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
    2.95 -\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ split{\isacharcolon}split{\isacharunderscore}if{\isacharunderscore}asm{\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.140 +intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
   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.177 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split{\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.184 +\isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
   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.191 +\isa{step{\isadigit{1}}}.%
   2.192 +\end{isamarkuptxt}%
   2.193 +\isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline
   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.203 +\isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline
   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.308 -\isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\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.311 -\isacommand{apply}{\isacharparenleft}insert\ intermed{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\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.316 -\isacommand{apply}{\isacharparenleft}rule\ int{\isacharunderscore}int{\isacharunderscore}eq{\isacharbrackleft}THEN\ iffD{\isadigit{1}}{\isacharbrackright}{\isacharparenright}\isanewline
   2.317 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   2.318 -\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
   2.319 -\isanewline
   2.320 -\isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\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.357  \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
   2.358 -\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
   2.359 +\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
   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.375 +that the authors are at least cavalier about this point and may even have
   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}
    8.10  \input{Advanced/advanced}