src/HOL/Imperative_HOL/ex/Sublist.thy
changeset 30689 b14b2cc4e25e
parent 29920 b95f5b8b93dd
child 32580 5b88ae4307ff
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Mon Mar 23 19:01:17 2009 +0100
     1.3 @@ -0,0 +1,505 @@
     1.4 +(* $Id$ *)
     1.5 +
     1.6 +header {* Slices of lists *}
     1.7 +
     1.8 +theory Sublist
     1.9 +imports Multiset
    1.10 +begin
    1.11 +
    1.12 +
    1.13 +lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
    1.14 +apply (induct xs arbitrary: i j k)
    1.15 +apply simp
    1.16 +apply (simp only: sublist_Cons)
    1.17 +apply simp
    1.18 +apply safe
    1.19 +apply simp
    1.20 +apply (erule_tac x="0" in meta_allE)
    1.21 +apply (erule_tac x="j - 1" in meta_allE)
    1.22 +apply (erule_tac x="k - 1" in meta_allE)
    1.23 +apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
    1.24 +apply simp
    1.25 +apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
    1.26 +apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
    1.27 +apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
    1.28 +apply simp
    1.29 +apply fastsimp
    1.30 +apply fastsimp
    1.31 +apply fastsimp
    1.32 +apply fastsimp
    1.33 +apply (erule_tac x="i - 1" in meta_allE)
    1.34 +apply (erule_tac x="j - 1" in meta_allE)
    1.35 +apply (erule_tac x="k - 1" in meta_allE)
    1.36 +apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
    1.37 +apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
    1.38 +apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
    1.39 +apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
    1.40 +apply simp
    1.41 +apply fastsimp
    1.42 +apply fastsimp
    1.43 +apply fastsimp
    1.44 +apply fastsimp
    1.45 +done
    1.46 +
    1.47 +lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
    1.48 +apply (induct xs arbitrary: i inds)
    1.49 +apply simp
    1.50 +apply (case_tac i)
    1.51 +apply (simp add: sublist_Cons)
    1.52 +apply (simp add: sublist_Cons)
    1.53 +done
    1.54 +
    1.55 +lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
    1.56 +proof (induct xs arbitrary: i inds)
    1.57 +  case Nil thus ?case by simp
    1.58 +next
    1.59 +  case (Cons x xs)
    1.60 +  thus ?case
    1.61 +  proof (cases i)
    1.62 +    case 0 with Cons show ?thesis by (simp add: sublist_Cons)
    1.63 +  next
    1.64 +    case (Suc i')
    1.65 +    with Cons show ?thesis
    1.66 +      apply simp
    1.67 +      apply (simp add: sublist_Cons)
    1.68 +      apply auto
    1.69 +      apply (auto simp add: nat.split)
    1.70 +      apply (simp add: card_less_Suc[symmetric])
    1.71 +      apply (simp add: card_less_Suc2)
    1.72 +      done
    1.73 +  qed
    1.74 +qed
    1.75 +
    1.76 +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)"
    1.77 +by (simp add: sublist_update1 sublist_update2)
    1.78 +
    1.79 +lemma sublist_take: "sublist xs {j. j < m} = take m xs"
    1.80 +apply (induct xs arbitrary: m)
    1.81 +apply simp
    1.82 +apply (case_tac m)
    1.83 +apply simp
    1.84 +apply (simp add: sublist_Cons)
    1.85 +done
    1.86 +
    1.87 +lemma sublist_take': "sublist xs {0..<m} = take m xs"
    1.88 +apply (induct xs arbitrary: m)
    1.89 +apply simp
    1.90 +apply (case_tac m)
    1.91 +apply simp
    1.92 +apply (simp add: sublist_Cons sublist_take)
    1.93 +done
    1.94 +
    1.95 +lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
    1.96 +apply (induct xs)
    1.97 +apply simp
    1.98 +apply (simp add: sublist_Cons)
    1.99 +done
   1.100 +
   1.101 +lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
   1.102 +apply (induct xs)
   1.103 +apply simp
   1.104 +apply (simp add: sublist_Cons)
   1.105 +done
   1.106 +
   1.107 +lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
   1.108 +apply (induct xs arbitrary: a)
   1.109 +apply simp
   1.110 +apply(case_tac aa)
   1.111 +apply simp
   1.112 +apply (simp add: sublist_Cons)
   1.113 +apply simp
   1.114 +apply (simp add: sublist_Cons)
   1.115 +done
   1.116 +
   1.117 +lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []" 
   1.118 +apply (induct xs arbitrary: inds)
   1.119 +apply simp
   1.120 +apply (simp add: sublist_Cons)
   1.121 +apply auto
   1.122 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   1.123 +apply auto
   1.124 +done
   1.125 +
   1.126 +lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
   1.127 +apply (induct xs arbitrary: inds)
   1.128 +apply simp
   1.129 +apply (simp add: sublist_Cons)
   1.130 +apply (auto split: if_splits)
   1.131 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   1.132 +apply (case_tac x, auto)
   1.133 +done
   1.134 +
   1.135 +lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
   1.136 +apply (induct xs arbitrary: inds)
   1.137 +apply simp
   1.138 +apply (simp add: sublist_Cons)
   1.139 +apply auto
   1.140 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   1.141 +apply (case_tac x, auto)
   1.142 +done
   1.143 +
   1.144 +lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
   1.145 +apply (induct xs arbitrary: ys inds inds')
   1.146 +apply simp
   1.147 +apply (drule sym, rule sym)
   1.148 +apply (simp add: sublist_Nil, fastsimp)
   1.149 +apply (case_tac ys)
   1.150 +apply (simp add: sublist_Nil, fastsimp)
   1.151 +apply (auto simp add: sublist_Cons)
   1.152 +apply (erule_tac x="list" in meta_allE)
   1.153 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   1.154 +apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
   1.155 +apply fastsimp
   1.156 +apply (erule_tac x="list" in meta_allE)
   1.157 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   1.158 +apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
   1.159 +apply fastsimp
   1.160 +done
   1.161 +
   1.162 +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"
   1.163 +apply (induct xs arbitrary: ys inds)
   1.164 +apply simp
   1.165 +apply (rule sym, simp add: sublist_Nil)
   1.166 +apply (case_tac ys)
   1.167 +apply (simp add: sublist_Nil)
   1.168 +apply (auto simp add: sublist_Cons)
   1.169 +apply (erule_tac x="list" in meta_allE)
   1.170 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   1.171 +apply fastsimp
   1.172 +apply (erule_tac x="list" in meta_allE)
   1.173 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   1.174 +apply fastsimp
   1.175 +done
   1.176 +
   1.177 +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"
   1.178 +by (rule sublist_eq, auto)
   1.179 +
   1.180 +lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
   1.181 +apply (induct xs arbitrary: ys inds)
   1.182 +apply simp
   1.183 +apply (rule sym, simp add: sublist_Nil)
   1.184 +apply (case_tac ys)
   1.185 +apply (simp add: sublist_Nil)
   1.186 +apply (auto simp add: sublist_Cons)
   1.187 +apply (case_tac i)
   1.188 +apply auto
   1.189 +apply (case_tac i)
   1.190 +apply auto
   1.191 +done
   1.192 +
   1.193 +section {* Another sublist function *}
   1.194 +
   1.195 +function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
   1.196 +where
   1.197 +  "sublist' n m [] = []"
   1.198 +| "sublist' n 0 xs = []"
   1.199 +| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
   1.200 +| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
   1.201 +by pat_completeness auto
   1.202 +termination by lexicographic_order
   1.203 +
   1.204 +subsection {* Proving equivalence to the other sublist command *}
   1.205 +
   1.206 +lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
   1.207 +apply (induct xs arbitrary: n m)
   1.208 +apply simp
   1.209 +apply (case_tac n)
   1.210 +apply (case_tac m)
   1.211 +apply simp
   1.212 +apply (simp add: sublist_Cons)
   1.213 +apply (case_tac m)
   1.214 +apply simp
   1.215 +apply (simp add: sublist_Cons)
   1.216 +done
   1.217 +
   1.218 +
   1.219 +lemma "sublist' n m xs = sublist xs {n..<m}"
   1.220 +apply (induct xs arbitrary: n m)
   1.221 +apply simp
   1.222 +apply (case_tac n, case_tac m)
   1.223 +apply simp
   1.224 +apply simp
   1.225 +apply (simp add: sublist_take')
   1.226 +apply (case_tac m)
   1.227 +apply simp
   1.228 +apply (simp add: sublist_Cons sublist'_sublist)
   1.229 +done
   1.230 +
   1.231 +
   1.232 +subsection {* Showing equivalence to use of drop and take for definition *}
   1.233 +
   1.234 +lemma "sublist' n m xs = take (m - n) (drop n xs)"
   1.235 +apply (induct xs arbitrary: n m)
   1.236 +apply simp
   1.237 +apply (case_tac m)
   1.238 +apply simp
   1.239 +apply (case_tac n)
   1.240 +apply simp
   1.241 +apply simp
   1.242 +done
   1.243 +
   1.244 +subsection {* General lemma about sublist *}
   1.245 +
   1.246 +lemma sublist'_Nil[simp]: "sublist' i j [] = []"
   1.247 +by simp
   1.248 +
   1.249 +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)"
   1.250 +by (cases i) auto
   1.251 +
   1.252 +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))"
   1.253 +apply (cases j)
   1.254 +apply auto
   1.255 +apply (cases i)
   1.256 +apply auto
   1.257 +done
   1.258 +
   1.259 +lemma sublist_n_0: "sublist' n 0 xs = []"
   1.260 +by (induct xs, auto)
   1.261 +
   1.262 +lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
   1.263 +apply (induct xs arbitrary: n m)
   1.264 +apply simp
   1.265 +apply (case_tac m)
   1.266 +apply simp
   1.267 +apply (case_tac n)
   1.268 +apply simp
   1.269 +apply simp
   1.270 +done
   1.271 +
   1.272 +lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
   1.273 +apply (induct xs arbitrary: n m)
   1.274 +apply simp
   1.275 +apply (case_tac m)
   1.276 +apply simp
   1.277 +apply (case_tac n)
   1.278 +apply simp
   1.279 +apply simp
   1.280 +done
   1.281 +
   1.282 +lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
   1.283 +apply (induct xs arbitrary: n m)
   1.284 +apply simp
   1.285 +apply (case_tac m)
   1.286 +apply simp
   1.287 +apply (case_tac n)
   1.288 +apply simp
   1.289 +apply simp
   1.290 +done
   1.291 +
   1.292 +lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
   1.293 +apply (induct xs arbitrary: n m)
   1.294 +apply simp
   1.295 +apply (case_tac m)
   1.296 +apply simp
   1.297 +apply (case_tac n)
   1.298 +apply simp
   1.299 +apply simp
   1.300 +done
   1.301 +
   1.302 +lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
   1.303 +apply (induct xs arbitrary: n)
   1.304 +apply simp
   1.305 +apply simp
   1.306 +apply (case_tac n)
   1.307 +apply (simp add: sublist_n_0)
   1.308 +apply simp
   1.309 +done
   1.310 +
   1.311 +lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
   1.312 +apply (induct xs arbitrary: n m i)
   1.313 +apply simp
   1.314 +apply simp
   1.315 +apply (case_tac i)
   1.316 +apply simp
   1.317 +apply simp
   1.318 +done
   1.319 +
   1.320 +lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
   1.321 +apply (induct xs arbitrary: n m i)
   1.322 +apply simp
   1.323 +apply simp
   1.324 +apply (case_tac i)
   1.325 +apply simp
   1.326 +apply simp
   1.327 +done
   1.328 +
   1.329 +lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]"
   1.330 +proof (induct xs arbitrary: n m i)
   1.331 +  case Nil thus ?case by auto
   1.332 +next
   1.333 +  case (Cons x xs)
   1.334 +  thus ?case
   1.335 +    apply -
   1.336 +    apply auto
   1.337 +    apply (cases i)
   1.338 +    apply auto
   1.339 +    apply (cases i)
   1.340 +    apply auto
   1.341 +    done
   1.342 +qed
   1.343 +
   1.344 +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"
   1.345 +proof (induct xs arbitrary: i j ys n m)
   1.346 +  case Nil
   1.347 +  thus ?case
   1.348 +    apply -
   1.349 +    apply (rule sym, drule sym)
   1.350 +    apply (simp add: sublist'_Nil)
   1.351 +    apply (simp add: sublist'_Nil3)
   1.352 +    apply arith
   1.353 +    done
   1.354 +next
   1.355 +  case (Cons x xs i j ys n m)
   1.356 +  note c = this
   1.357 +  thus ?case
   1.358 +  proof (cases m)
   1.359 +    case 0 thus ?thesis by (simp add: sublist_n_0)
   1.360 +  next
   1.361 +    case (Suc m')
   1.362 +    note a = this
   1.363 +    thus ?thesis
   1.364 +    proof (cases n)
   1.365 +      case 0 note b = this
   1.366 +      show ?thesis
   1.367 +      proof (cases ys)
   1.368 +	case Nil  with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
   1.369 +      next
   1.370 +	case (Cons y ys)
   1.371 +	show ?thesis
   1.372 +	proof (cases j)
   1.373 +	  case 0 with a b Cons.prems show ?thesis by simp
   1.374 +	next
   1.375 +	  case (Suc j') with a b Cons.prems Cons show ?thesis 
   1.376 +	    apply -
   1.377 +	    apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
   1.378 +	    done
   1.379 +	qed
   1.380 +      qed
   1.381 +    next
   1.382 +      case (Suc n')
   1.383 +      show ?thesis
   1.384 +      proof (cases ys)
   1.385 +	case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
   1.386 +      next
   1.387 +	case (Cons y ys) with Suc a Cons.prems show ?thesis
   1.388 +	  apply -
   1.389 +	  apply simp
   1.390 +	  apply (cases j)
   1.391 +	  apply simp
   1.392 +	  apply (cases i)
   1.393 +	  apply simp
   1.394 +	  apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
   1.395 +	  apply simp
   1.396 +	  apply simp
   1.397 +	  apply simp
   1.398 +	  apply simp
   1.399 +	  apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
   1.400 +	  apply simp
   1.401 +	  apply simp
   1.402 +	  apply simp
   1.403 +	  done
   1.404 +      qed
   1.405 +    qed
   1.406 +  qed
   1.407 +qed
   1.408 +
   1.409 +lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
   1.410 +by (induct xs arbitrary: i j, auto)
   1.411 +
   1.412 +lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
   1.413 +apply (induct xs arbitrary: a i j)
   1.414 +apply simp
   1.415 +apply (case_tac j)
   1.416 +apply simp
   1.417 +apply (case_tac i)
   1.418 +apply simp
   1.419 +apply simp
   1.420 +done
   1.421 +
   1.422 +lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
   1.423 +apply (induct xs arbitrary: a i j)
   1.424 +apply simp
   1.425 +apply simp
   1.426 +apply (case_tac j)
   1.427 +apply simp
   1.428 +apply auto
   1.429 +apply (case_tac nat)
   1.430 +apply auto
   1.431 +done
   1.432 +
   1.433 +(* suffices that j \<le> length xs and length ys *) 
   1.434 +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')"
   1.435 +proof (induct xs arbitrary: ys i j)
   1.436 +  case Nil thus ?case by simp
   1.437 +next
   1.438 +  case (Cons x xs)
   1.439 +  thus ?case
   1.440 +    apply -
   1.441 +    apply (cases ys)
   1.442 +    apply simp
   1.443 +    apply simp
   1.444 +    apply auto
   1.445 +    apply (case_tac i', auto)
   1.446 +    apply (erule_tac x="Suc i'" in allE, auto)
   1.447 +    apply (erule_tac x="i' - 1" in allE, auto)
   1.448 +    apply (case_tac i', auto)
   1.449 +    apply (erule_tac x="Suc i'" in allE, auto)
   1.450 +    done
   1.451 +qed
   1.452 +
   1.453 +lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
   1.454 +by (induct xs, auto)
   1.455 +
   1.456 +lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" 
   1.457 +by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
   1.458 +
   1.459 +lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
   1.460 +by (induct xs arbitrary: i j k) auto
   1.461 +
   1.462 +lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
   1.463 +apply (induct xs arbitrary: i j k)
   1.464 +apply auto
   1.465 +apply (case_tac k)
   1.466 +apply auto
   1.467 +apply (case_tac i)
   1.468 +apply auto
   1.469 +done
   1.470 +
   1.471 +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}"
   1.472 +apply (simp add: sublist'_sublist)
   1.473 +apply (simp add: set_sublist)
   1.474 +apply auto
   1.475 +done
   1.476 +
   1.477 +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))"
   1.478 +unfolding set_sublist' by blast
   1.479 +
   1.480 +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))"
   1.481 +unfolding set_sublist' by blast
   1.482 +
   1.483 +
   1.484 +lemma multiset_of_sublist:
   1.485 +assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
   1.486 +assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
   1.487 +assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
   1.488 +assumes multiset: "multiset_of xs = multiset_of ys"
   1.489 +  shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
   1.490 +proof -
   1.491 +  from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") 
   1.492 +    by (simp add: sublist'_append)
   1.493 +  from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
   1.494 +  with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") 
   1.495 +    by (simp add: sublist'_append)
   1.496 +  from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
   1.497 +  moreover
   1.498 +  from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
   1.499 +    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   1.500 +  moreover
   1.501 +  from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
   1.502 +    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   1.503 +  moreover
   1.504 +  ultimately show ?thesis by (simp add: multiset_of_append)
   1.505 +qed
   1.506 +
   1.507 +
   1.508 +end