author paulson Wed Aug 01 22:59:42 2018 +0100 (11 months ago) changeset 68709 6d9eca4805ff parent 68708 77858f347020 child 68710 3db37e950118 child 68719 8aedca31957d
de-applying
 src/HOL/List.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/List.thy	Tue Jul 31 23:09:21 2018 +0100
1.2 +++ b/src/HOL/List.thy	Wed Aug 01 22:59:42 2018 +0100
1.3 @@ -1,5 +1,5 @@
1.4  (*  Title:      HOL/List.thy
1.5 -    Author:     Tobias Nipkow
1.6 +    Author:     Tobias Nipkow; proofs tidied by LCP
1.7  *)
1.8
1.9  section \<open>The datatype of finite lists\<close>
1.10 @@ -166,7 +166,7 @@
1.11
1.12  primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
1.13  upt_0: "[i..<0] = []" |
1.14 -upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
1.15 +upt_Suc: "[i..<(Suc j)] = (if i \<le> j then [i..<j] @ [j] else [])"
1.16
1.17  definition insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
1.18  "insert x xs = (if x \<in> set xs then xs else x # xs)"
1.19 @@ -834,11 +834,9 @@
1.20
1.21  lemma Suc_length_conv:
1.22    "(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
1.23 -apply (induct xs, simp, simp)
1.24 -apply blast
1.25 -done
1.26 -
1.27 -lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"
1.28 +  by (induct xs; simp; blast)
1.29 +
1.30 +lemma impossible_Cons: "length xs \<le> length ys ==> xs = x # ys = False"
1.31  by (induct xs) auto
1.32
1.33  lemma list_induct2 [consumes 1, case_names Nil Cons]:
1.34 @@ -846,10 +844,8 @@
1.35     (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (x#xs) (y#ys))
1.36     \<Longrightarrow> P xs ys"
1.37  proof (induct xs arbitrary: ys)
1.38 -  case Nil then show ?case by simp
1.39 -next
1.40    case (Cons x xs ys) then show ?case by (cases ys) simp_all
1.41 -qed
1.42 +qed simp
1.43
1.44  lemma list_induct3 [consumes 2, case_names Nil Cons]:
1.45    "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P [] [] [] \<Longrightarrow>
1.46 @@ -960,19 +956,15 @@
1.47  lemma append_eq_append_conv [simp]:
1.48    "length xs = length ys \<or> length us = length vs
1.49    ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
1.50 -apply (induct xs arbitrary: ys)
1.51 - apply (case_tac ys, simp, force)
1.52 -apply (case_tac ys, force, simp)
1.53 -done
1.54 +  by (induct xs arbitrary: ys; case_tac ys; force)
1.55
1.56  lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
1.57    (\<exists>us. xs = zs @ us \<and> us @ ys = ts \<or> xs @ us = zs \<and> ys = us @ ts)"
1.58 -apply (induct xs arbitrary: ys zs ts)
1.59 - apply fastforce
1.60 -apply(case_tac zs)
1.61 - apply simp
1.62 -apply fastforce
1.63 -done
1.64 +proof (induct xs arbitrary: ys zs ts)
1.65 +  case (Cons x xs)
1.66 +  then show ?case
1.67 +    by (case_tac zs) auto
1.68 +qed fastforce
1.69
1.70  lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"
1.71  by simp
1.72 @@ -1152,15 +1144,14 @@
1.73  qed
1.74
1.75  lemma map_inj_on:
1.76 - "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]
1.77 -  ==> xs = ys"
1.78 -apply(frule map_eq_imp_length_eq)
1.79 -apply(rotate_tac -1)
1.80 -apply(induct rule:list_induct2)
1.81 - apply simp
1.82 -apply(simp)
1.83 -apply (blast intro:sym)
1.84 -done
1.85 +  assumes map: "map f xs = map f ys" and inj: "inj_on f (set xs Un set ys)"
1.86 +  shows "xs = ys"
1.87 +  using map_eq_imp_length_eq [OF map] assms
1.88 +proof (induct rule: list_induct2)
1.89 +  case (Cons x xs y ys)
1.90 +  then show ?case
1.91 +    by (auto intro: sym)
1.92 +qed auto
1.93
1.94  lemma inj_on_map_eq_map:
1.95    "inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
1.96 @@ -1177,21 +1168,13 @@
1.97  by (iprover dest: map_injective injD intro: inj_onI)
1.98
1.99  lemma inj_mapD: "inj (map f) ==> inj f"
1.100 -  apply (unfold inj_def)
1.101 -  apply clarify
1.102 -  apply (erule_tac x = "[x]" in allE)
1.103 -  apply (erule_tac x = "[y]" in allE)
1.104 -  apply auto
1.105 -  done
1.106 +  by (metis (no_types, hide_lams) injI list.inject list.simps(9) the_inv_f_f)
1.107
1.108  lemma inj_map[iff]: "inj (map f) = inj f"
1.109  by (blast dest: inj_mapD intro: inj_mapI)
1.110
1.111  lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A"
1.112 -apply(rule inj_onI)
1.113 -apply(erule map_inj_on)
1.114 -apply(blast intro:inj_onI dest:inj_onD)
1.115 -done
1.116 +  by (blast intro:inj_onI dest:inj_onD map_inj_on)
1.117
1.118  lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
1.119  by (induct xs, auto)
1.120 @@ -1248,9 +1231,11 @@
1.121  by (cases xs) auto
1.122
1.123  lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
1.124 -apply (induct xs arbitrary: ys, force)
1.125 -apply (case_tac ys, simp, force)
1.126 -done
1.127 +proof  (induct xs arbitrary: ys)
1.128 +  case (Cons a xs)
1.129 +  then show ?case
1.130 +    by (case_tac ys) auto
1.131 +qed force
1.132
1.133  lemma inj_on_rev[iff]: "inj_on rev A"
1.135 @@ -1481,11 +1466,12 @@
1.136  by (induct xs) simp_all
1.137
1.138  lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
1.139 -apply (induct xs)
1.140 - apply auto
1.141 -apply(cut_tac P=P and xs=xs in length_filter_le)
1.142 -apply simp
1.143 -done
1.144 +proof (induct xs)
1.145 +  case (Cons x xs)
1.146 +  then show ?case
1.147 +    using length_filter_le
1.148 +    by (simp add: impossible_Cons)
1.149 +qed auto
1.150
1.151  lemma filter_map: "filter P (map f xs) = map f (filter (P \<circ> f) xs)"
1.152  by (induct xs) simp_all
1.153 @@ -1504,8 +1490,7 @@
1.154  next
1.155    case (Cons x xs) thus ?case
1.156      apply (auto split:if_split_asm)
1.157 -    using length_filter_le[of P xs] apply arith
1.158 -  done
1.159 +    using length_filter_le[of P xs] by arith
1.160  qed
1.161
1.162  lemma length_filter_conv_card:
1.163 @@ -1592,9 +1577,7 @@
1.164
1.165  lemma filter_cong[fundef_cong]:
1.166    "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
1.167 -apply simp
1.168 -apply(erule thin_rl)
1.169 -by (induct ys) simp_all
1.170 +  by (induct ys arbitrary: xs) auto
1.171
1.172
1.173  subsubsection \<open>List partitioning\<close>
1.174 @@ -1688,9 +1671,11 @@
1.175
1.176  lemma nth_append:
1.177    "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
1.178 -apply (induct xs arbitrary: n, simp)
1.179 -apply (case_tac n, auto)
1.180 -done
1.181 +proof (induct xs arbitrary: n)
1.182 +  case (Cons x xs)
1.183 +  then show ?case
1.184 +    using less_Suc_eq_0_disj by auto
1.185 +qed simp
1.186
1.187  lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
1.188  by (induct xs) auto
1.189 @@ -1699,9 +1684,11 @@
1.190  by (induct xs) auto
1.191
1.192  lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
1.193 -apply (induct xs arbitrary: n, simp)
1.194 -apply (case_tac n, auto)
1.195 -done
1.196 +proof (induct xs arbitrary: n)
1.197 +  case (Cons x xs)
1.198 +  then show ?case
1.199 +    using less_Suc_eq_0_disj by auto
1.200 +qed simp
1.201
1.202  lemma nth_tl: "n < length (tl xs) \<Longrightarrow> tl xs ! n = xs ! Suc n"
1.203  by (induction xs) auto
1.204 @@ -1712,21 +1699,29 @@
1.205
1.206  lemma list_eq_iff_nth_eq:
1.207    "(xs = ys) = (length xs = length ys \<and> (\<forall>i<length xs. xs!i = ys!i))"
1.208 -apply(induct xs arbitrary: ys)
1.209 - apply force
1.210 -apply(case_tac ys)
1.211 - apply simp
1.213 -done
1.214 +proof (induct xs arbitrary: ys)
1.215 +  case (Cons x xs ys)
1.216 +  show ?case
1.217 +  proof (cases ys)
1.218 +    case (Cons y ys)
1.219 +    then show ?thesis
1.220 +      using Cons.hyps by fastforce
1.221 +  qed simp
1.222 +qed force
1.223
1.224  lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
1.225 -apply (induct xs, simp, simp)
1.226 -apply safe
1.227 -apply (metis nat.case(1) nth.simps zero_less_Suc)
1.228 -apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
1.229 -apply (case_tac i, simp)
1.230 -apply (metis diff_Suc_Suc nat.case(2) nth.simps zero_less_diff)
1.231 -done
1.232 +proof (induct xs)
1.233 +  case (Cons x xs)
1.234 +  have "insert x {xs ! i |i. i < length xs} = {(x # xs) ! i |i. i < Suc (length xs)}" (is "?L=?R")
1.235 +  proof
1.236 +    show "?L \<subseteq> ?R"
1.237 +      by force
1.238 +    show "?R \<subseteq> ?L"
1.239 +      using less_Suc_eq_0_disj by auto
1.240 +  qed
1.241 +  with Cons show ?case
1.242 +    by simp
1.243 +qed simp
1.244
1.245  lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
1.246  by(auto simp:set_conv_nth)
1.247 @@ -1832,11 +1827,11 @@
1.248  by (induct xs arbitrary: i) (simp_all split:nat.splits)
1.249
1.250  lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
1.251 -apply (induct xs arbitrary: i)
1.252 - apply simp
1.253 -apply (case_tac i)
1.254 -apply simp_all
1.255 -done
1.256 +proof (induct xs arbitrary: i)
1.257 +  case (Cons x xs i)
1.258 +  then show ?case
1.259 +    by (metis leD length_list_update list_eq_iff_nth_eq nth_list_update_neq)
1.260 +qed simp
1.261
1.262  lemma list_update_nonempty[simp]: "xs[k:=x] = [] \<longleftrightarrow> xs=[]"
1.263  by (simp only: length_0_conv[symmetric] length_list_update)
1.264 @@ -1869,7 +1864,7 @@
1.265    "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
1.266  by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
1.267
1.268 -lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
1.269 +lemma set_update_subset_insert: "set(xs[i:=x]) \<le> insert x (set xs)"
1.270  by (induct xs arbitrary: i) (auto split: nat.split)
1.271
1.272  lemma set_update_subsetI: "\<lbrakk>set xs \<subseteq> A; x \<in> A\<rbrakk> \<Longrightarrow> set(xs[i := x]) \<subseteq> A"
1.273 @@ -1880,19 +1875,11 @@
1.274
1.275  lemma list_update_overwrite[simp]:
1.276    "xs [i := x, i := y] = xs [i := y]"
1.277 -apply (induct xs arbitrary: i) apply simp
1.278 -apply (case_tac i, simp_all)
1.279 -done
1.280 +  by (induct xs arbitrary: i) (simp_all split: nat.split)
1.281
1.282  lemma list_update_swap:
1.283    "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"
1.284 -apply (induct xs arbitrary: i i')
1.285 - apply simp
1.286 -apply (case_tac i, case_tac i')
1.287 -  apply auto
1.288 -apply (case_tac i')
1.289 -apply auto
1.290 -done
1.291 +  by (induct xs arbitrary: i i') (simp_all split: nat.split)
1.292
1.293  lemma list_update_code [code]:
1.294    "[][i := y] = []"
1.295 @@ -2049,15 +2036,17 @@
1.296
1.297  lemma take_Suc_conv_app_nth:
1.298    "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
1.299 -apply (induct xs arbitrary: i, simp)
1.300 -apply (case_tac i, auto)
1.301 -done
1.302 +proof (induct xs arbitrary: i)
1.303 +  case (Cons x xs) then show ?case
1.304 +    by (case_tac i, auto)
1.305 +qed simp
1.306
1.307  lemma Cons_nth_drop_Suc:
1.308    "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
1.309 -apply (induct xs arbitrary: i, simp)
1.310 -apply (case_tac i, auto)
1.311 -done
1.312 +proof (induct xs arbitrary: i)
1.313 +  case (Cons x xs) then show ?case
1.314 +    by (case_tac i, auto)
1.315 +qed simp
1.316
1.317  lemma length_take [simp]: "length (take n xs) = min (length xs) n"
1.318  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1.319 @@ -2065,10 +2054,10 @@
1.320  lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
1.321  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1.322
1.323 -lemma take_all [simp]: "length xs <= n ==> take n xs = xs"
1.324 +lemma take_all [simp]: "length xs \<le> n ==> take n xs = xs"
1.325  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1.326
1.327 -lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"
1.328 +lemma drop_all [simp]: "length xs \<le> n ==> drop n xs = []"
1.329  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1.330
1.331  lemma take_append [simp]:
1.332 @@ -2080,54 +2069,61 @@
1.333  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
1.334
1.335  lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
1.336 -apply (induct m arbitrary: xs n, auto)
1.337 - apply (case_tac xs, auto)
1.338 -apply (case_tac n, auto)
1.339 -done
1.340 +proof (induct m arbitrary: xs n)
1.341 +  case (Suc m) then show ?case
1.342 +    by (case_tac xs; case_tac n; simp)
1.343 +qed auto
1.344
1.345  lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
1.346 -apply (induct m arbitrary: xs, auto)
1.347 - apply (case_tac xs, auto)
1.348 -done
1.349 +proof (induct m arbitrary: xs)
1.350 +  case (Suc m) then show ?case
1.351 +    by (case_tac xs; simp)
1.352 +qed auto
1.353
1.354  lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
1.355 -apply (induct m arbitrary: xs n, auto)
1.356 - apply (case_tac xs, auto)
1.357 -done
1.358 +proof (induct m arbitrary: xs n)
1.359 +  case (Suc m) then show ?case
1.360 +    by (case_tac xs; case_tac n; simp)
1.361 +qed auto
1.362
1.363  lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
1.364  by(induct xs arbitrary: m n)(auto simp: take_Cons drop_Cons split: nat.split)
1.365
1.366  lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
1.367 -apply (induct n arbitrary: xs, auto)
1.368 -apply (case_tac xs, auto)
1.369 -done
1.370 +proof (induct n arbitrary: xs)
1.371 +  case (Suc n) then show ?case
1.372 +    by (case_tac xs; simp)
1.373 +qed auto
1.374
1.375  lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
1.376  by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split)
1.377
1.378 -lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"
1.379 +lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs \<le> n)"
1.380  by (induct xs arbitrary: n) (auto simp: drop_Cons split:nat.split)
1.381
1.382  lemma take_map: "take n (map f xs) = map f (take n xs)"
1.383 -apply (induct n arbitrary: xs, auto)
1.384 - apply (case_tac xs, auto)
1.385 -done
1.386 +proof (induct n arbitrary: xs)
1.387 +  case (Suc n) then show ?case
1.388 +    by (case_tac xs; simp)
1.389 +qed auto
1.390
1.391  lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
1.392 -apply (induct n arbitrary: xs, auto)
1.393 - apply (case_tac xs, auto)
1.394 -done
1.395 +proof (induct n arbitrary: xs)
1.396 +  case (Suc n) then show ?case
1.397 +    by (case_tac xs; simp)
1.398 +qed auto
1.399
1.400  lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
1.401 -apply (induct xs arbitrary: i, auto)
1.402 - apply (case_tac i, auto)
1.403 -done
1.404 +proof (induct xs arbitrary: i)
1.405 +  case (Cons x xs) then show ?case
1.406 +    by (case_tac i, auto)
1.407 +qed simp
1.408
1.409  lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
1.410 -apply (induct xs arbitrary: i, auto)
1.411 - apply (case_tac i, auto)
1.412 -done
1.413 +proof (induct xs arbitrary: i)
1.414 +  case (Cons x xs) then show ?case
1.415 +    by (case_tac i, auto)
1.416 +qed simp
1.417
1.418  lemma drop_rev: "drop n (rev xs) = rev (take (length xs - n) xs)"
1.419    by (cases "length xs < n") (auto simp: rev_take)
1.420 @@ -2136,19 +2132,20 @@
1.421    by (cases "length xs < n") (auto simp: rev_drop)
1.422
1.423  lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
1.424 -apply (induct xs arbitrary: i n, auto)
1.425 - apply (case_tac n, blast)
1.426 -apply (case_tac i, auto)
1.427 -done
1.428 +proof (induct xs arbitrary: i n)
1.429 +  case (Cons x xs) then show ?case
1.430 +    by (case_tac n; case_tac i; simp)
1.431 +qed auto
1.432
1.433  lemma nth_drop [simp]:
1.434 -  "n <= length xs ==> (drop n xs)!i = xs!(n + i)"
1.435 -apply (induct n arbitrary: xs i, auto)
1.436 - apply (case_tac xs, auto)
1.437 -done
1.438 +  "n \<le> length xs ==> (drop n xs)!i = xs!(n + i)"
1.439 +proof (induct n arbitrary: xs)
1.440 +  case (Suc n) then show ?case
1.441 +    by (case_tac xs; simp)
1.442 +qed auto
1.443
1.444  lemma butlast_take:
1.445 -  "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
1.446 +  "n \<le> length xs ==> butlast (take n xs) = take (n - 1) xs"
1.447  by (simp add: butlast_conv_take min.absorb1 min.absorb2)
1.448
1.449  lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
1.450 @@ -2164,12 +2161,11 @@
1.452
1.453  lemma set_take_subset_set_take:
1.454 -  "m <= n \<Longrightarrow> set(take m xs) <= set(take n xs)"
1.455 -apply (induct xs arbitrary: m n)
1.456 - apply simp
1.457 -apply (case_tac n)
1.458 -apply (auto simp: take_Cons)
1.459 -done
1.460 +  "m \<le> n \<Longrightarrow> set(take m xs) \<le> set(take n xs)"
1.461 +proof (induct xs arbitrary: m n)
1.462 +  case (Cons x xs m n) then show ?case
1.463 +    by (cases n) (auto simp: take_Cons)
1.464 +qed simp
1.465
1.466  lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
1.467  by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
1.468 @@ -2178,10 +2174,12 @@
1.469  by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
1.470
1.471  lemma set_drop_subset_set_drop:
1.472 -  "m >= n \<Longrightarrow> set(drop m xs) <= set(drop n xs)"
1.473 -apply(induct xs arbitrary: m n)
1.474 - apply(auto simp:drop_Cons split:nat.split)
1.475 -by (metis set_drop_subset subset_iff)
1.476 +  "m \<ge> n \<Longrightarrow> set(drop m xs) \<le> set(drop n xs)"
1.477 +proof (induct xs arbitrary: m n)
1.478 +  case (Cons x xs m n)
1.479 +  then show ?case
1.480 +    by (clarsimp simp: drop_Cons split: nat.split) (metis set_drop_subset subset_iff)
1.481 +qed simp
1.482
1.483  lemma in_set_takeD: "x \<in> set(take n xs) \<Longrightarrow> x \<in> set xs"
1.484  using set_take_subset by fast
1.485 @@ -2191,32 +2189,30 @@
1.486
1.487  lemma append_eq_conv_conj:
1.488    "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
1.489 -apply (induct xs arbitrary: zs, simp, clarsimp)
1.490 - apply (case_tac zs, auto)
1.491 -done
1.492 +proof (induct xs arbitrary: zs)
1.493 +  case (Cons x xs zs) then show ?case
1.494 +    by (cases zs, auto)
1.495 +qed auto
1.496
1.497  lemma take_add:  "take (i+j) xs = take i xs @ take j (drop i xs)"
1.498 -apply (induct xs arbitrary: i, auto)
1.499 - apply (case_tac i, simp_all)
1.500 -done
1.501 +proof (induct xs arbitrary: i)
1.502 +  case (Cons x xs i) then show ?case
1.503 +    by (cases i, auto)
1.504 +qed auto
1.505
1.506  lemma append_eq_append_conv_if:
1.507    "(xs\<^sub>1 @ xs\<^sub>2 = ys\<^sub>1 @ ys\<^sub>2) =
1.508    (if size xs\<^sub>1 \<le> size ys\<^sub>1
1.509     then xs\<^sub>1 = take (size xs\<^sub>1) ys\<^sub>1 \<and> xs\<^sub>2 = drop (size xs\<^sub>1) ys\<^sub>1 @ ys\<^sub>2
1.510     else take (size ys\<^sub>1) xs\<^sub>1 = ys\<^sub>1 \<and> drop (size ys\<^sub>1) xs\<^sub>1 @ xs\<^sub>2 = ys\<^sub>2)"
1.511 -apply(induct xs\<^sub>1 arbitrary: ys\<^sub>1)
1.512 - apply simp
1.513 -apply(case_tac ys\<^sub>1)
1.514 -apply simp_all
1.515 -done
1.516 +proof (induct xs\<^sub>1 arbitrary: ys\<^sub>1)
1.517 +  case (Cons a xs\<^sub>1 ys\<^sub>1) then show ?case
1.518 +    by (cases ys\<^sub>1, auto)
1.519 +qed auto
1.520
1.521  lemma take_hd_drop:
1.522    "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (Suc n) xs"
1.523 -apply(induct xs arbitrary: n)
1.524 - apply simp
1.526 -done
1.527 +  by (induct xs arbitrary: n) (simp_all add:drop_Cons split:nat.split)
1.528
1.529  lemma id_take_nth_drop:
1.530    "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs"
1.531 @@ -2225,7 +2221,7 @@
1.532    hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto
1.533    moreover
1.534    from si have "take (Suc i) xs = take i xs @ [xs!i]"
1.535 -    apply (rule_tac take_Suc_conv_app_nth) by arith
1.536 +    using take_Suc_conv_app_nth by blast
1.537    ultimately show ?thesis by auto
1.538  qed
1.539
1.540 @@ -2247,17 +2243,19 @@
1.541  qed
1.542
1.543  lemma take_update_swap: "take m (xs[n := x]) = (take m xs)[n := x]"
1.544 -apply(cases "n \<ge> length xs")
1.545 - apply simp
1.546 -apply(simp add: upd_conv_take_nth_drop take_Cons drop_take min_def diff_Suc
1.547 -  split: nat.split)
1.548 -done
1.549 -
1.550 -lemma drop_update_swap: "m \<le> n \<Longrightarrow> drop m (xs[n := x]) = (drop m xs)[n-m := x]"
1.551 -apply(cases "n \<ge> length xs")
1.552 - apply simp
1.554 -done
1.555 +proof (cases "n \<ge> length xs")
1.556 +  case False
1.557 +  then show ?thesis
1.558 +    by (simp add: upd_conv_take_nth_drop take_Cons drop_take min_def diff_Suc split: nat.split)
1.559 +qed auto
1.560 +
1.561 +lemma drop_update_swap:
1.562 +  assumes "m \<le> n" shows "drop m (xs[n := x]) = (drop m xs)[n-m := x]"
1.563 +proof (cases "n \<ge> length xs")
1.564 +  case False
1.565 +  with assms show ?thesis
1.566 +    by (simp add: upd_conv_take_nth_drop drop_take)
1.567 +qed auto
1.568
1.569  lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
1.570  by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
1.571 @@ -2283,11 +2281,11 @@
1.572  by (induct xs) auto
1.573
1.574  lemma takeWhile_nth: "j < length (takeWhile P xs) \<Longrightarrow> takeWhile P xs ! j = xs ! j"
1.575 -apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto
1.576 +  by (metis nth_append takeWhile_dropWhile_id)
1.577
1.578  lemma dropWhile_nth: "j < length (dropWhile P xs) \<Longrightarrow>
1.579    dropWhile P xs ! j = xs ! (j + length (takeWhile P xs))"
1.580 -apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto
1.581 +  by (metis add.commute nth_append_length_plus takeWhile_dropWhile_id)
1.582
1.583  lemma length_dropWhile_le: "length (dropWhile P xs) \<le> length xs"
1.584  by (induct xs) auto
1.585 @@ -2408,12 +2406,11 @@
1.586
1.587  lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
1.588    dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
1.589 -apply(induct xs)
1.590 - apply simp
1.591 -apply auto
1.592 -apply(subst dropWhile_append2)
1.593 -apply auto
1.594 -done
1.595 +proof (induct xs)
1.596 +  case (Cons a xs)
1.597 +  then show ?case
1.598 +    by(auto, subst dropWhile_append2, auto)
1.599 +qed simp
1.600
1.601  lemma takeWhile_not_last:
1.602    "distinct xs \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
1.603 @@ -2531,10 +2528,11 @@
1.604
1.605  lemma nth_zip [simp]:
1.606    "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
1.607 -apply (induct ys arbitrary: i xs, simp)
1.608 -apply (case_tac xs)
1.609 - apply (simp_all add: nth.simps split: nat.split)
1.610 -done
1.611 +proof (induct ys arbitrary: i xs)
1.612 +  case (Cons y ys)
1.613 +  then show ?case
1.614 +    by (cases xs) (simp_all add: nth.simps split: nat.split)
1.615 +qed auto
1.616
1.617  lemma set_zip:
1.618    "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
1.619 @@ -2543,34 +2541,33 @@
1.620  lemma zip_same: "((a,b) \<in> set (zip xs xs)) = (a \<in> set xs \<and> a = b)"
1.621  by(induct xs) auto
1.622
1.623 -lemma zip_update:
1.624 -  "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
1.625 -by(rule sym, simp add: update_zip)
1.626 +lemma zip_update: "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
1.627 +  by (simp add: update_zip)
1.628
1.629  lemma zip_replicate [simp]:
1.630    "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
1.631 -apply (induct i arbitrary: j, auto)
1.632 -apply (case_tac j, auto)
1.633 -done
1.634 +proof (induct i arbitrary: j)
1.635 +  case (Suc i)
1.636 +  then show ?case
1.637 +    by (cases j, auto)
1.638 +qed auto
1.639
1.640  lemma zip_replicate1: "zip (replicate n x) ys = map (Pair x) (take n ys)"
1.641  by(induction ys arbitrary: n)(case_tac  n, simp_all)
1.642
1.643 -lemma take_zip:
1.644 -  "take n (zip xs ys) = zip (take n xs) (take n ys)"
1.645 -apply (induct n arbitrary: xs ys)
1.646 - apply simp
1.647 -apply (case_tac xs, simp)
1.648 -apply (case_tac ys, simp_all)
1.649 -done
1.650 -
1.651 -lemma drop_zip:
1.652 -  "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
1.653 -apply (induct n arbitrary: xs ys)
1.654 - apply simp
1.655 -apply (case_tac xs, simp)
1.656 -apply (case_tac ys, simp_all)
1.657 -done
1.658 +lemma take_zip: "take n (zip xs ys) = zip (take n xs) (take n ys)"
1.659 +proof (induct n arbitrary: xs ys)
1.660 +  case (Suc n)
1.661 +  then show ?case
1.662 +    by (case_tac xs; case_tac ys; simp)
1.663 +qed simp
1.664 +
1.665 +lemma drop_zip: "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
1.666 +proof (induct n arbitrary: xs ys)
1.667 +  case (Suc n)
1.668 +  then show ?case
1.669 +    by (case_tac xs; case_tac ys; simp)
1.670 +qed simp
1.671
1.672  lemma zip_takeWhile_fst: "zip (takeWhile P xs) ys = takeWhile (P \<circ> fst) (zip xs ys)"
1.673  proof (induct xs arbitrary: ys)
1.674 @@ -2677,26 +2674,36 @@
1.675  lemma list_all2_append1:
1.676    "list_all2 P (xs @ ys) zs =
1.677    (\<exists>us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>
1.678 -    list_all2 P xs us \<and> list_all2 P ys vs)"
1.679 -apply (simp add: list_all2_iff zip_append1)
1.680 -apply (rule iffI)
1.681 - apply (rule_tac x = "take (length xs) zs" in exI)
1.682 - apply (rule_tac x = "drop (length xs) zs" in exI)
1.683 - apply (force split: nat_diff_split simp add: min_def, clarify)
1.685 -done
1.686 +    list_all2 P xs us \<and> list_all2 P ys vs)" (is "?lhs = ?rhs")
1.687 +proof
1.688 +  assume ?lhs
1.689 +  then show ?rhs
1.690 +    apply (rule_tac x = "take (length xs) zs" in exI)
1.691 +    apply (rule_tac x = "drop (length xs) zs" in exI)
1.692 +    apply (force split: nat_diff_split simp add: list_all2_iff zip_append1)
1.693 +    done
1.694 +next
1.695 +  assume ?rhs
1.696 +  then show ?lhs
1.697 +    by (auto simp add: list_all2_iff)
1.698 +qed
1.699
1.700  lemma list_all2_append2:
1.701    "list_all2 P xs (ys @ zs) =
1.702    (\<exists>us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>
1.703 -    list_all2 P us ys \<and> list_all2 P vs zs)"
1.704 -apply (simp add: list_all2_iff zip_append2)
1.705 -apply (rule iffI)
1.706 - apply (rule_tac x = "take (length ys) xs" in exI)
1.707 - apply (rule_tac x = "drop (length ys) xs" in exI)
1.708 - apply (force split: nat_diff_split simp add: min_def, clarify)
1.710 -done
1.711 +    list_all2 P us ys \<and> list_all2 P vs zs)" (is "?lhs = ?rhs")
1.712 +proof
1.713 +  assume ?lhs
1.714 +  then show ?rhs
1.715 +    apply (rule_tac x = "take (length ys) xs" in exI)
1.716 +    apply (rule_tac x = "drop (length ys) xs" in exI)
1.717 +    apply (force split: nat_diff_split simp add: list_all2_iff zip_append2)
1.718 +    done
1.719 +next
1.720 +  assume ?rhs
1.721 +  then show ?lhs
1.722 +    by (auto simp add: list_all2_iff)
1.723 +qed
1.724
1.725  lemma list_all2_append:
1.726    "length xs = length ys \<Longrightarrow>
1.727 @@ -2760,25 +2767,23 @@
1.728
1.729  lemma list_all2_takeI [simp,intro?]:
1.730    "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
1.731 -apply (induct xs arbitrary: n ys)
1.732 - apply simp
1.733 -apply (clarsimp simp add: list_all2_Cons1)
1.734 -apply (case_tac n)
1.735 -apply auto
1.736 -done
1.737 +proof (induct xs arbitrary: n ys)
1.738 +  case (Cons x xs)
1.739 +  then show ?case
1.740 +    by (cases n) (auto simp: list_all2_Cons1)
1.741 +qed auto
1.742
1.743  lemma list_all2_dropI [simp,intro?]:
1.744 -  "list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
1.745 -apply (induct as arbitrary: n bs, simp)
1.746 -apply (clarsimp simp add: list_all2_Cons1)
1.747 -apply (case_tac n, simp, simp)
1.748 -done
1.749 +  "list_all2 P xs ys \<Longrightarrow> list_all2 P (drop n xs) (drop n ys)"
1.750 +proof (induct xs arbitrary: n ys)
1.751 +  case (Cons x xs)
1.752 +  then show ?case
1.753 +    by (cases n) (auto simp: list_all2_Cons1)
1.754 +qed auto
1.755
1.756  lemma list_all2_mono [intro?]:
1.757    "list_all2 P xs ys \<Longrightarrow> (\<And>xs ys. P xs ys \<Longrightarrow> Q xs ys) \<Longrightarrow> list_all2 Q xs ys"
1.758 -apply (induct xs arbitrary: ys, simp)
1.759 -apply (case_tac ys, auto)
1.760 -done
1.761 +  by (rule list.rel_mono_strong)
1.762
1.763  lemma list_all2_eq:
1.764    "xs = ys \<longleftrightarrow> list_all2 (=) xs ys"
1.765 @@ -3051,21 +3056,21 @@
1.766
1.767  lemmas upt_rec_numeral[simp] = upt_rec[of "numeral m" "numeral n"] for m n
1.768
1.769 -lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
1.770 +lemma upt_conv_Nil [simp]: "j \<le> i ==> [i..<j] = []"
1.771  by (subst upt_rec) simp
1.772
1.773 -lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
1.774 +lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j \<le> i)"
1.775  by(induct j)simp_all
1.776
1.777  lemma upt_eq_Cons_conv:
1.778   "([i..<j] = x#xs) = (i < j \<and> i = x \<and> [i+1..<j] = xs)"
1.779 -apply(induct j arbitrary: x xs)
1.780 - apply simp
1.782 -apply arith
1.783 -done
1.784 -
1.785 -lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
1.786 +proof (induct j arbitrary: x xs)
1.787 +  case (Suc j)
1.788 +  then show ?case
1.789 +    by (simp add: upt_rec)
1.790 +qed simp
1.791 +
1.792 +lemma upt_Suc_append: "i \<le> j ==> [i..<(Suc j)] = [i..<j]@[j]"
1.793  \<comment> \<open>Only needed if \<open>upt_Suc\<close> is deleted from the simpset.\<close>
1.794  by simp
1.795
1.796 @@ -3081,7 +3086,7 @@
1.797  qed
1.798
1.799  lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
1.800 -\<comment> \<open>LOOPS as a simprule, since \<open>j <= j\<close>.\<close>
1.801 +\<comment> \<open>LOOPS as a simprule, since \<open>j \<le> j\<close>.\<close>
1.802  by (induct k) auto
1.803
1.804  lemma length_upt [simp]: "length [i..<j] = j - i"
1.805 @@ -3099,13 +3104,12 @@
1.806  lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
1.807  by(cases j)(auto simp: upt_Suc_append)
1.808
1.809 -lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
1.810 -apply (induct m arbitrary: i, simp)
1.811 -apply (subst upt_rec)
1.812 -apply (rule sym)
1.813 -apply (subst upt_rec)
1.814 -apply (simp del: upt.simps)
1.815 -done
1.816 +lemma take_upt [simp]: "i+m \<le> n ==> take m [i..<n] = [i..<i+m]"
1.817 +proof (induct m arbitrary: i)
1.818 +  case (Suc m)
1.819 +  then show ?case
1.820 +    by (subst take_Suc_conv_app_nth) auto
1.821 +qed simp
1.822
1.823  lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
1.824  by(induct j) auto
1.825 @@ -3117,10 +3121,11 @@
1.826  by (induct m) simp_all
1.827
1.828  lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
1.829 -apply (induct n m  arbitrary: i rule: diff_induct)
1.830 -  prefer 3 apply (subst map_Suc_upt[symmetric])
1.831 -  apply (auto simp add: less_diff_conv)
1.832 -done
1.833 +proof (induct n m  arbitrary: i rule: diff_induct)
1.834 +case (3 x y)
1.835 +  then show ?case
1.836 +    by (metis add.commute length_upt less_diff_conv nth_map nth_upt)
1.837 +qed auto
1.838
1.839  lemma map_decr_upt: "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
1.840  by (induct n) simp_all
1.841 @@ -3128,21 +3133,15 @@
1.842  lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda>i. f (Suc i)) [0 ..< n]"
1.843  by (induct n arbitrary: f) auto
1.844
1.845 -
1.846  lemma nth_take_lemma:
1.847    "k \<le> length xs \<Longrightarrow> k \<le> length ys \<Longrightarrow>
1.848       (\<And>i. i < k \<longrightarrow> xs!i = ys!i) \<Longrightarrow> take k xs = take k ys"
1.849 -apply (atomize, induct k arbitrary: xs ys)
1.850 -apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)
1.851 -txt \<open>Both lists must be non-empty\<close>
1.852 -apply (case_tac xs, simp)
1.853 -apply (case_tac ys, clarify)
1.854 - apply (simp (no_asm_use))
1.855 -apply clarify
1.856 -txt \<open>prenexing's needed, not miniscoping\<close>
1.857 -apply (simp (no_asm_use) add: all_simps [symmetric] del: all_simps)
1.858 -apply blast
1.859 -done
1.860 +proof (induct k arbitrary: xs ys)
1.861 +  case (Suc k)
1.862 +  then show ?case
1.863 +    apply (simp add: less_Suc_eq_0_disj)
1.864 +    by (simp add: Suc.prems(3) take_Suc_conv_app_nth)
1.865 +qed simp
1.866
1.867  lemma nth_equalityI:
1.868    "[| length xs = length ys; \<forall>i < length xs. xs!i = ys!i |] ==> xs = ys"
1.869 @@ -3165,7 +3164,6 @@
1.871  done
1.872
1.873 -
1.874  lemma take_Cons':
1.875    "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
1.876  by (cases n) simp_all
1.877 @@ -3307,14 +3305,14 @@
1.878  lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
1.879  by (induct x, auto)
1.880
1.881 -lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
1.882 +lemma length_remdups_leq[iff]: "length(remdups xs) \<le> length xs"
1.883  by (induct xs) auto
1.884
1.885  lemma length_remdups_eq[iff]:
1.886    "(length (remdups xs) = length xs) = (remdups xs = xs)"
1.887  apply(induct xs)
1.888   apply auto
1.889 -apply(subgoal_tac "length (remdups xs) <= length xs")
1.890 +apply(subgoal_tac "length (remdups xs) \<le> length xs")
1.891   apply arith
1.892  apply(rule length_remdups_leq)
1.893  done
1.894 @@ -4320,10 +4318,10 @@
1.895  lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
1.897
1.898 -lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
1.899 +lemma rotate1_length01[simp]: "length xs \<le> 1 \<Longrightarrow> rotate1 xs = xs"
1.900  by(cases xs) simp_all
1.901
1.902 -lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"
1.903 +lemma rotate_length01[simp]: "length xs \<le> 1 \<Longrightarrow> rotate n xs = xs"
1.904  apply(induct n)
1.905   apply simp
1.907 @@ -5719,7 +5717,7 @@
1.908
1.909  lemmas in_listsI [intro!] = in_listspI [to_set]
1.910
1.911 -lemma lists_eq_set: "lists A = {xs. set xs <= A}"
1.912 +lemma lists_eq_set: "lists A = {xs. set xs \<le> A}"
1.913  by auto
1.914
1.915  lemma lists_empty [simp]: "lists {} = {[]}"
1.916 @@ -6294,7 +6292,7 @@
1.917  lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
1.918  by simp
1.919
1.920 -lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
1.921 +lemma measures_lesseq: "f x \<le> f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
1.922  by auto
1.923
1.924
1.925 @@ -7138,7 +7136,7 @@
1.926  lemma subset_code [code]:
1.927    "set xs \<le> B \<longleftrightarrow> (\<forall>x\<in>set xs. x \<in> B)"
1.928    "A \<le> List.coset ys \<longleftrightarrow> (\<forall>y\<in>set ys. y \<notin> A)"
1.929 -  "List.coset [] \<le> set [] \<longleftrightarrow> False"
1.930 +  "List.coset [] \<subseteq> set [] \<longleftrightarrow> False"
1.931    by auto
1.932
1.933  text \<open>A frequent case -- avoid intermediate sets\<close>
```