author nipkow Thu Jun 14 07:27:55 2007 +0200 (2007-06-14) changeset 23380 15f7a6745cce parent 23379 d0e3f790bd73 child 23381 da53d861d106
fixed filter syntax
     1.1 --- a/doc-src/TutorialI/Inductive/AB.thy	Thu Jun 14 00:48:42 2007 +0200
1.2 +++ b/doc-src/TutorialI/Inductive/AB.thy	Thu Jun 14 07:27:55 2007 +0200
1.3 @@ -68,13 +68,13 @@
1.4  *}
1.5
1.6  lemma correctness:
1.7 -  "(w \<in> S \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b])     \<and>
1.8 -   (w \<in> A \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1) \<and>
1.9 -   (w \<in> B \<longrightarrow> size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1)"
1.10 +  "(w \<in> S \<longrightarrow> size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b])     \<and>
1.11 +   (w \<in> A \<longrightarrow> size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] + 1) \<and>
1.12 +   (w \<in> B \<longrightarrow> size[x\<leftarrow>w. x=b] = size[x\<leftarrow>w. x=a] + 1)"
1.13
1.14  txt{*\noindent
1.15  These propositions are expressed with the help of the predefined @{term
1.16 -filter} function on lists, which has the convenient syntax @{text"[x\<in>xs. P
1.17 +filter} function on lists, which has the convenient syntax @{text"[x\<leftarrow>xs. P
1.18  x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}
1.19  holds. Remember that on lists @{text size} and @{text length} are synonymous.
1.20
1.21 @@ -116,8 +116,8 @@
1.22  *}
1.23
1.24  lemma step1: "\<forall>i < size w.
1.25 -  \<bar>(int(size[x\<in>take (i+1) w. P x])-int(size[x\<in>take (i+1) w. \<not>P x]))
1.26 -   - (int(size[x\<in>take i w. P x])-int(size[x\<in>take i w. \<not>P x]))\<bar> \<le> 1"
1.27 +  \<bar>(int(size[x\<leftarrow>take (i+1) w. P x])-int(size[x\<leftarrow>take (i+1) w. \<not>P x]))
1.28 +   - (int(size[x\<leftarrow>take i w. P x])-int(size[x\<leftarrow>take i w. \<not>P x]))\<bar> \<le> 1"
1.29
1.30  txt{*\noindent
1.31  The lemma is a bit hard to read because of the coercion function
1.32 @@ -141,8 +141,8 @@
1.33  *}
1.34
1.35  lemma part1:
1.36 - "size[x\<in>w. P x] = size[x\<in>w. \<not>P x]+2 \<Longrightarrow>
1.37 -  \<exists>i\<le>size w. size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1"
1.38 + "size[x\<leftarrow>w. P x] = size[x\<leftarrow>w. \<not>P x]+2 \<Longrightarrow>
1.39 +  \<exists>i\<le>size w. size[x\<leftarrow>take i w. P x] = size[x\<leftarrow>take i w. \<not>P x]+1"
1.40
1.41  txt{*\noindent
1.42  This is proved by @{text force} with the help of the intermediate value theorem,
1.43 @@ -161,10 +161,10 @@
1.44
1.45
1.46  lemma part2:
1.47 -  "\<lbrakk>size[x\<in>take i w @ drop i w. P x] =
1.48 -    size[x\<in>take i w @ drop i w. \<not>P x]+2;
1.49 -    size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1\<rbrakk>
1.50 -   \<Longrightarrow> size[x\<in>drop i w. P x] = size[x\<in>drop i w. \<not>P x]+1"
1.51 +  "\<lbrakk>size[x\<leftarrow>take i w @ drop i w. P x] =
1.52 +    size[x\<leftarrow>take i w @ drop i w. \<not>P x]+2;
1.53 +    size[x\<leftarrow>take i w. P x] = size[x\<leftarrow>take i w. \<not>P x]+1\<rbrakk>
1.54 +   \<Longrightarrow> size[x\<leftarrow>drop i w. P x] = size[x\<leftarrow>drop i w. \<not>P x]+1"
1.55  by(simp del: append_take_drop_id)
1.56
1.57  text{*\noindent
1.58 @@ -191,9 +191,9 @@
1.59  *}
1.60
1.61  theorem completeness:
1.62 -  "(size[x\<in>w. x=a] = size[x\<in>w. x=b]     \<longrightarrow> w \<in> S) \<and>
1.63 -   (size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
1.64 -   (size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1 \<longrightarrow> w \<in> B)"
1.65 +  "(size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b]     \<longrightarrow> w \<in> S) \<and>
1.66 +   (size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
1.67 +   (size[x\<leftarrow>w. x=b] = size[x\<leftarrow>w. x=a] + 1 \<longrightarrow> w \<in> B)"
1.68
1.69  txt{*\noindent
1.70  The proof is by induction on @{term w}. Structural induction would fail here
1.71 @@ -237,9 +237,9 @@
1.72   apply(clarify)
1.73  txt{*\noindent
1.74  This yields an index @{prop"i \<le> length v"} such that
1.75 -@{prop[display]"length [x\<in>take i v . x = a] = length [x\<in>take i v . x = b] + 1"}
1.76 +@{prop[display]"length [x\<leftarrow>take i v . x = a] = length [x\<leftarrow>take i v . x = b] + 1"}
1.77  With the help of @{thm[source]part2} it follows that
1.78 -@{prop[display]"length [x\<in>drop i v . x = a] = length [x\<in>drop i v . x = b] + 1"}
1.79 +@{prop[display]"length [x\<leftarrow>drop i v . x = a] = length [x\<leftarrow>drop i v . x = b] + 1"}
1.80  *}
1.81
1.82   apply(drule part2[of "\<lambda>x. x=a", simplified])

     2.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Thu Jun 14 00:48:42 2007 +0200
2.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Thu Jun 14 07:27:55 2007 +0200
2.3 @@ -103,9 +103,9 @@
2.4  \isamarkuptrue%
2.5  \isacommand{lemma}\isamarkupfalse%
2.6  \ correctness{\isacharcolon}\isanewline
2.7 -\ \ {\isachardoublequoteopen}{\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.8 -\ \ \ {\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.9 -\ \ \ {\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}{\isachardoublequoteclose}%
2.10 +\ \ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymin}\ S\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isasymand}\isanewline
2.11 +\ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline
2.12 +\ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}%
2.14  %
2.16 @@ -114,7 +114,7 @@
2.17  %
2.18  \begin{isamarkuptxt}%
2.19  \noindent
2.20 -These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isacharbrackleft}x{\isasymin}xs{\isachardot}\ P\ x{\isacharbrackright}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x}
2.21 +These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isacharbrackleft}x{\isasymleftarrow}xs{\isachardot}\ P\ x{\isacharbrackright}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x}
2.22  holds. Remember that on lists \isa{size} and \isa{length} are synonymous.
2.23
2.24  The proof itself is by rule induction and afterwards automatic:%
2.25 @@ -166,8 +166,8 @@
2.26  \isamarkuptrue%
2.27  \isacommand{lemma}\isamarkupfalse%
2.28  \ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
2.29 -\ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
2.30 -\ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isachardoublequoteclose}%
2.31 +\ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
2.32 +\ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isachardoublequoteclose}%
2.34  %
2.36 @@ -207,8 +207,8 @@
2.37  \isamarkuptrue%
2.38  \isacommand{lemma}\isamarkupfalse%
2.40 -\ {\isachardoublequoteopen}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.41 -\ \ {\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}}{\isachardoublequoteclose}%
2.42 +\ {\isachardoublequoteopen}size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline
2.43 +\ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequoteclose}%
2.45  %
2.47 @@ -242,10 +242,10 @@
2.48  \isamarkuptrue%
2.49  \isacommand{lemma}\isamarkupfalse%
2.51 -\ \ {\isachardoublequoteopen}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline
2.52 -\ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
2.53 -\ \ \ \ 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.54 -\ \ \ {\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}}{\isachardoublequoteclose}\isanewline
2.55 +\ \ {\isachardoublequoteopen}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline
2.56 +\ \ \ \ size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
2.57 +\ \ \ \ size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isasymrbrakk}\isanewline
2.58 +\ \ \ {\isasymLongrightarrow}\ size{\isacharbrackleft}x{\isasymleftarrow}drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequoteclose}\isanewline
2.59  %
2.61  %
2.62 @@ -290,9 +290,9 @@
2.63  \isamarkuptrue%
2.64  \isacommand{theorem}\isamarkupfalse%
2.65  \ completeness{\isacharcolon}\isanewline
2.66 -\ \ {\isachardoublequoteopen}{\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.67 -\ \ \ {\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.68 -\ \ \ {\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}{\isachardoublequoteclose}%
2.69 +\ \ {\isachardoublequoteopen}{\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline
2.70 +\ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline
2.71 +\ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequoteclose}%
2.73  %
2.75 @@ -329,7 +329,8 @@
2.76  Simplification disposes of the base case and leaves only a conjunction
2.77  of two step cases to be proved:
2.78  if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \begin{isabelle}%
2.79 -\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{2}}%
2.80 +\ \ \ \ \ length\ {\isacharparenleft}if\ x\ {\isacharequal}\ a\ then\ {\isacharbrackleft}x\ {\isasymin}\ v{\isacharbrackright}\ else\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
2.81 +\isaindent{\ \ \ \ \ }length\ {\isacharparenleft}if\ x\ {\isacharequal}\ b\ then\ {\isacharbrackleft}x\ {\isasymin}\ v{\isacharbrackright}\ else\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharplus}\ {\isadigit{2}}%
2.82  \end{isabelle} then
2.83  \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}.
2.84  We only consider the first case in detail.
2.85 @@ -350,11 +351,11 @@
2.86  \noindent
2.87  This yields an index \isa{i\ {\isasymle}\ length\ v} such that
2.88  \begin{isabelle}%
2.89 -\ \ \ \ \ 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.90 +\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymleftarrow}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymleftarrow}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}%
2.91  \end{isabelle}
2.92  With the help of \isa{part{\isadigit{2}}} it follows that
2.93  \begin{isabelle}%
2.94 -\ \ \ \ \ 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.95 +\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymleftarrow}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymleftarrow}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}%
2.96  \end{isabelle}%
2.97  \end{isamarkuptxt}%
2.98  \isamarkuptrue%