src/HOL/ex/Sublist.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 29920 b95f5b8b93dd permissions -rw-r--r--
```     1 (* \$Id\$ *)
```
```     2
```
```     3 header {* Slices of lists *}
```
```     4
```
```     5 theory Sublist
```
```     6 imports Multiset
```
```     7 begin
```
```     8
```
```     9
```
```    10 lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}"
```
```    11 apply (induct xs arbitrary: i j k)
```
```    12 apply simp
```
```    13 apply (simp only: sublist_Cons)
```
```    14 apply simp
```
```    15 apply safe
```
```    16 apply simp
```
```    17 apply (erule_tac x="0" in meta_allE)
```
```    18 apply (erule_tac x="j - 1" in meta_allE)
```
```    19 apply (erule_tac x="k - 1" in meta_allE)
```
```    20 apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
```
```    21 apply simp
```
```    22 apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
```
```    23 apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
```
```    24 apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
```
```    25 apply simp
```
```    26 apply fastsimp
```
```    27 apply fastsimp
```
```    28 apply fastsimp
```
```    29 apply fastsimp
```
```    30 apply (erule_tac x="i - 1" in meta_allE)
```
```    31 apply (erule_tac x="j - 1" in meta_allE)
```
```    32 apply (erule_tac x="k - 1" in meta_allE)
```
```    33 apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
```
```    34 apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
```
```    35 apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
```
```    36 apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
```
```    37 apply simp
```
```    38 apply fastsimp
```
```    39 apply fastsimp
```
```    40 apply fastsimp
```
```    41 apply fastsimp
```
```    42 done
```
```    43
```
```    44 lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
```
```    45 apply (induct xs arbitrary: i inds)
```
```    46 apply simp
```
```    47 apply (case_tac i)
```
```    48 apply (simp add: sublist_Cons)
```
```    49 apply (simp add: sublist_Cons)
```
```    50 done
```
```    51
```
```    52 lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
```
```    53 proof (induct xs arbitrary: i inds)
```
```    54   case Nil thus ?case by simp
```
```    55 next
```
```    56   case (Cons x xs)
```
```    57   thus ?case
```
```    58   proof (cases i)
```
```    59     case 0 with Cons show ?thesis by (simp add: sublist_Cons)
```
```    60   next
```
```    61     case (Suc i')
```
```    62     with Cons show ?thesis
```
```    63       apply simp
```
```    64       apply (simp add: sublist_Cons)
```
```    65       apply auto
```
```    66       apply (auto simp add: nat.split)
```
```    67       apply (simp add: card_less_Suc[symmetric])
```
```    68       apply (simp add: card_less_Suc2)
```
```    69       done
```
```    70   qed
```
```    71 qed
```
```    72
```
```    73 lemma sublist_update: "sublist (xs[i := v]) inds = (if i \<in> inds then (sublist xs inds)[(card {k \<in> inds. k < i}) := v] else sublist xs inds)"
```
```    74 by (simp add: sublist_update1 sublist_update2)
```
```    75
```
```    76 lemma sublist_take: "sublist xs {j. j < m} = take m xs"
```
```    77 apply (induct xs arbitrary: m)
```
```    78 apply simp
```
```    79 apply (case_tac m)
```
```    80 apply simp
```
```    81 apply (simp add: sublist_Cons)
```
```    82 done
```
```    83
```
```    84 lemma sublist_take': "sublist xs {0..<m} = take m xs"
```
```    85 apply (induct xs arbitrary: m)
```
```    86 apply simp
```
```    87 apply (case_tac m)
```
```    88 apply simp
```
```    89 apply (simp add: sublist_Cons sublist_take)
```
```    90 done
```
```    91
```
```    92 lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
```
```    93 apply (induct xs)
```
```    94 apply simp
```
```    95 apply (simp add: sublist_Cons)
```
```    96 done
```
```    97
```
```    98 lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
```
```    99 apply (induct xs)
```
```   100 apply simp
```
```   101 apply (simp add: sublist_Cons)
```
```   102 done
```
```   103
```
```   104 lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
```
```   105 apply (induct xs arbitrary: a)
```
```   106 apply simp
```
```   107 apply(case_tac aa)
```
```   108 apply simp
```
```   109 apply (simp add: sublist_Cons)
```
```   110 apply simp
```
```   111 apply (simp add: sublist_Cons)
```
```   112 done
```
```   113
```
```   114 lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []"
```
```   115 apply (induct xs arbitrary: inds)
```
```   116 apply simp
```
```   117 apply (simp add: sublist_Cons)
```
```   118 apply auto
```
```   119 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
```
```   120 apply auto
```
```   121 done
```
```   122
```
```   123 lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
```
```   124 apply (induct xs arbitrary: inds)
```
```   125 apply simp
```
```   126 apply (simp add: sublist_Cons)
```
```   127 apply (auto split: if_splits)
```
```   128 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
```
```   129 apply (case_tac x, auto)
```
```   130 done
```
```   131
```
```   132 lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
```
```   133 apply (induct xs arbitrary: inds)
```
```   134 apply simp
```
```   135 apply (simp add: sublist_Cons)
```
```   136 apply auto
```
```   137 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
```
```   138 apply (case_tac x, auto)
```
```   139 done
```
```   140
```
```   141 lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
```
```   142 apply (induct xs arbitrary: ys inds inds')
```
```   143 apply simp
```
```   144 apply (drule sym, rule sym)
```
```   145 apply (simp add: sublist_Nil, fastsimp)
```
```   146 apply (case_tac ys)
```
```   147 apply (simp add: sublist_Nil, fastsimp)
```
```   148 apply (auto simp add: sublist_Cons)
```
```   149 apply (erule_tac x="list" in meta_allE)
```
```   150 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
```
```   151 apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
```
```   152 apply fastsimp
```
```   153 apply (erule_tac x="list" in meta_allE)
```
```   154 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
```
```   155 apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
```
```   156 apply fastsimp
```
```   157 done
```
```   158
```
```   159 lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
```
```   160 apply (induct xs arbitrary: ys inds)
```
```   161 apply simp
```
```   162 apply (rule sym, simp add: sublist_Nil)
```
```   163 apply (case_tac ys)
```
```   164 apply (simp add: sublist_Nil)
```
```   165 apply (auto simp add: sublist_Cons)
```
```   166 apply (erule_tac x="list" in meta_allE)
```
```   167 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
```
```   168 apply fastsimp
```
```   169 apply (erule_tac x="list" in meta_allE)
```
```   170 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
```
```   171 apply fastsimp
```
```   172 done
```
```   173
```
```   174 lemma sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
```
```   175 by (rule sublist_eq, auto)
```
```   176
```
```   177 lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
```
```   178 apply (induct xs arbitrary: ys inds)
```
```   179 apply simp
```
```   180 apply (rule sym, simp add: sublist_Nil)
```
```   181 apply (case_tac ys)
```
```   182 apply (simp add: sublist_Nil)
```
```   183 apply (auto simp add: sublist_Cons)
```
```   184 apply (case_tac i)
```
```   185 apply auto
```
```   186 apply (case_tac i)
```
```   187 apply auto
```
```   188 done
```
```   189
```
```   190 section {* Another sublist function *}
```
```   191
```
```   192 function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
```
```   193 where
```
```   194   "sublist' n m [] = []"
```
```   195 | "sublist' n 0 xs = []"
```
```   196 | "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
```
```   197 | "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
```
```   198 by pat_completeness auto
```
```   199 termination by lexicographic_order
```
```   200
```
```   201 subsection {* Proving equivalence to the other sublist command *}
```
```   202
```
```   203 lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
```
```   204 apply (induct xs arbitrary: n m)
```
```   205 apply simp
```
```   206 apply (case_tac n)
```
```   207 apply (case_tac m)
```
```   208 apply simp
```
```   209 apply (simp add: sublist_Cons)
```
```   210 apply (case_tac m)
```
```   211 apply simp
```
```   212 apply (simp add: sublist_Cons)
```
```   213 done
```
```   214
```
```   215
```
```   216 lemma "sublist' n m xs = sublist xs {n..<m}"
```
```   217 apply (induct xs arbitrary: n m)
```
```   218 apply simp
```
```   219 apply (case_tac n, case_tac m)
```
```   220 apply simp
```
```   221 apply simp
```
```   222 apply (simp add: sublist_take')
```
```   223 apply (case_tac m)
```
```   224 apply simp
```
```   225 apply (simp add: sublist_Cons sublist'_sublist)
```
```   226 done
```
```   227
```
```   228
```
```   229 subsection {* Showing equivalence to use of drop and take for definition *}
```
```   230
```
```   231 lemma "sublist' n m xs = take (m - n) (drop n xs)"
```
```   232 apply (induct xs arbitrary: n m)
```
```   233 apply simp
```
```   234 apply (case_tac m)
```
```   235 apply simp
```
```   236 apply (case_tac n)
```
```   237 apply simp
```
```   238 apply simp
```
```   239 done
```
```   240
```
```   241 subsection {* General lemma about sublist *}
```
```   242
```
```   243 lemma sublist'_Nil[simp]: "sublist' i j [] = []"
```
```   244 by simp
```
```   245
```
```   246 lemma sublist'_Cons[simp]: "sublist' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # sublist' 0 j xs) | Suc i' \<Rightarrow>  sublist' i' j xs)"
```
```   247 by (cases i) auto
```
```   248
```
```   249 lemma sublist'_Cons2[simp]: "sublist' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ sublist' (i - 1) (j - 1) xs))"
```
```   250 apply (cases j)
```
```   251 apply auto
```
```   252 apply (cases i)
```
```   253 apply auto
```
```   254 done
```
```   255
```
```   256 lemma sublist_n_0: "sublist' n 0 xs = []"
```
```   257 by (induct xs, auto)
```
```   258
```
```   259 lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
```
```   260 apply (induct xs arbitrary: n m)
```
```   261 apply simp
```
```   262 apply (case_tac m)
```
```   263 apply simp
```
```   264 apply (case_tac n)
```
```   265 apply simp
```
```   266 apply simp
```
```   267 done
```
```   268
```
```   269 lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
```
```   270 apply (induct xs arbitrary: n m)
```
```   271 apply simp
```
```   272 apply (case_tac m)
```
```   273 apply simp
```
```   274 apply (case_tac n)
```
```   275 apply simp
```
```   276 apply simp
```
```   277 done
```
```   278
```
```   279 lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
```
```   280 apply (induct xs arbitrary: n m)
```
```   281 apply simp
```
```   282 apply (case_tac m)
```
```   283 apply simp
```
```   284 apply (case_tac n)
```
```   285 apply simp
```
```   286 apply simp
```
```   287 done
```
```   288
```
```   289 lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
```
```   290 apply (induct xs arbitrary: n m)
```
```   291 apply simp
```
```   292 apply (case_tac m)
```
```   293 apply simp
```
```   294 apply (case_tac n)
```
```   295 apply simp
```
```   296 apply simp
```
```   297 done
```
```   298
```
```   299 lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
```
```   300 apply (induct xs arbitrary: n)
```
```   301 apply simp
```
```   302 apply simp
```
```   303 apply (case_tac n)
```
```   304 apply (simp add: sublist_n_0)
```
```   305 apply simp
```
```   306 done
```
```   307
```
```   308 lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
```
```   309 apply (induct xs arbitrary: n m i)
```
```   310 apply simp
```
```   311 apply simp
```
```   312 apply (case_tac i)
```
```   313 apply simp
```
```   314 apply simp
```
```   315 done
```
```   316
```
```   317 lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
```
```   318 apply (induct xs arbitrary: n m i)
```
```   319 apply simp
```
```   320 apply simp
```
```   321 apply (case_tac i)
```
```   322 apply simp
```
```   323 apply simp
```
```   324 done
```
```   325
```
```   326 lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]"
```
```   327 proof (induct xs arbitrary: n m i)
```
```   328   case Nil thus ?case by auto
```
```   329 next
```
```   330   case (Cons x xs)
```
```   331   thus ?case
```
```   332     apply -
```
```   333     apply auto
```
```   334     apply (cases i)
```
```   335     apply auto
```
```   336     apply (cases i)
```
```   337     apply auto
```
```   338     done
```
```   339 qed
```
```   340
```
```   341 lemma "\<lbrakk> sublist' i j xs = sublist' i j ys; n \<ge> i; m \<le> j \<rbrakk> \<Longrightarrow> sublist' n m xs = sublist' n m ys"
```
```   342 proof (induct xs arbitrary: i j ys n m)
```
```   343   case Nil
```
```   344   thus ?case
```
```   345     apply -
```
```   346     apply (rule sym, drule sym)
```
```   347     apply (simp add: sublist'_Nil)
```
```   348     apply (simp add: sublist'_Nil3)
```
```   349     apply arith
```
```   350     done
```
```   351 next
```
```   352   case (Cons x xs i j ys n m)
```
```   353   note c = this
```
```   354   thus ?case
```
```   355   proof (cases m)
```
```   356     case 0 thus ?thesis by (simp add: sublist_n_0)
```
```   357   next
```
```   358     case (Suc m')
```
```   359     note a = this
```
```   360     thus ?thesis
```
```   361     proof (cases n)
```
```   362       case 0 note b = this
```
```   363       show ?thesis
```
```   364       proof (cases ys)
```
```   365 	case Nil  with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
```
```   366       next
```
```   367 	case (Cons y ys)
```
```   368 	show ?thesis
```
```   369 	proof (cases j)
```
```   370 	  case 0 with a b Cons.prems show ?thesis by simp
```
```   371 	next
```
```   372 	  case (Suc j') with a b Cons.prems Cons show ?thesis
```
```   373 	    apply -
```
```   374 	    apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
```
```   375 	    done
```
```   376 	qed
```
```   377       qed
```
```   378     next
```
```   379       case (Suc n')
```
```   380       show ?thesis
```
```   381       proof (cases ys)
```
```   382 	case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
```
```   383       next
```
```   384 	case (Cons y ys) with Suc a Cons.prems show ?thesis
```
```   385 	  apply -
```
```   386 	  apply simp
```
```   387 	  apply (cases j)
```
```   388 	  apply simp
```
```   389 	  apply (cases i)
```
```   390 	  apply simp
```
```   391 	  apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
```
```   392 	  apply simp
```
```   393 	  apply simp
```
```   394 	  apply simp
```
```   395 	  apply simp
```
```   396 	  apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
```
```   397 	  apply simp
```
```   398 	  apply simp
```
```   399 	  apply simp
```
```   400 	  done
```
```   401       qed
```
```   402     qed
```
```   403   qed
```
```   404 qed
```
```   405
```
```   406 lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
```
```   407 by (induct xs arbitrary: i j, auto)
```
```   408
```
```   409 lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
```
```   410 apply (induct xs arbitrary: a i j)
```
```   411 apply simp
```
```   412 apply (case_tac j)
```
```   413 apply simp
```
```   414 apply (case_tac i)
```
```   415 apply simp
```
```   416 apply simp
```
```   417 done
```
```   418
```
```   419 lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
```
```   420 apply (induct xs arbitrary: a i j)
```
```   421 apply simp
```
```   422 apply simp
```
```   423 apply (case_tac j)
```
```   424 apply simp
```
```   425 apply auto
```
```   426 apply (case_tac nat)
```
```   427 apply auto
```
```   428 done
```
```   429
```
```   430 (* suffices that j \<le> length xs and length ys *)
```
```   431 lemma sublist'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist' i j xs  = sublist' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')"
```
```   432 proof (induct xs arbitrary: ys i j)
```
```   433   case Nil thus ?case by simp
```
```   434 next
```
```   435   case (Cons x xs)
```
```   436   thus ?case
```
```   437     apply -
```
```   438     apply (cases ys)
```
```   439     apply simp
```
```   440     apply simp
```
```   441     apply auto
```
```   442     apply (case_tac i', auto)
```
```   443     apply (erule_tac x="Suc i'" in allE, auto)
```
```   444     apply (erule_tac x="i' - 1" in allE, auto)
```
```   445     apply (case_tac i', auto)
```
```   446     apply (erule_tac x="Suc i'" in allE, auto)
```
```   447     done
```
```   448 qed
```
```   449
```
```   450 lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
```
```   451 by (induct xs, auto)
```
```   452
```
```   453 lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs"
```
```   454 by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
```
```   455
```
```   456 lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
```
```   457 by (induct xs arbitrary: i j k) auto
```
```   458
```
```   459 lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
```
```   460 apply (induct xs arbitrary: i j k)
```
```   461 apply auto
```
```   462 apply (case_tac k)
```
```   463 apply auto
```
```   464 apply (case_tac i)
```
```   465 apply auto
```
```   466 done
```
```   467
```
```   468 lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
```
```   469 apply (simp add: sublist'_sublist)
```
```   470 apply (simp add: set_sublist)
```
```   471 apply auto
```
```   472 done
```
```   473
```
```   474 lemma all_in_set_sublist'_conv: "(\<forall>j. j \<in> set (sublist' l r xs) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
```
```   475 unfolding set_sublist' by blast
```
```   476
```
```   477 lemma ball_in_set_sublist'_conv: "(\<forall>j \<in> set (sublist' l r xs). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
```
```   478 unfolding set_sublist' by blast
```
```   479
```
```   480
```
```   481 lemma multiset_of_sublist:
```
```   482 assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
```
```   483 assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
```
```   484 assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
```
```   485 assumes multiset: "multiset_of xs = multiset_of ys"
```
```   486   shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
```
```   487 proof -
```
```   488   from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long")
```
```   489     by (simp add: sublist'_append)
```
```   490   from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
```
```   491   with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long")
```
```   492     by (simp add: sublist'_append)
```
```   493   from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
```
```   494   moreover
```
```   495   from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
```
```   496     by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
```
```   497   moreover
```
```   498   from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
```
```   499     by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
```
```   500   moreover
```
```   501   ultimately show ?thesis by (simp add: multiset_of_append)
```
```   502 qed
```
```   503
```
```   504
```
```   505 end
```