de-applying
authorpaulson <lp15@cam.ac.uk>
Wed Aug 01 22:59:42 2018 +0100 (11 months ago)
changeset 687096d9eca4805ff
parent 68708 77858f347020
child 68710 3db37e950118
child 68719 8aedca31957d
de-applying
src/HOL/List.thy
     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.134  by(simp add:inj_on_def)
   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.212 -apply(simp add:nth_Cons split:nat.split)apply blast
   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.451  by(simp add: hd_conv_nth)
   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.525 -apply(simp add:drop_Cons split:nat.split)
   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.553 -apply(simp add: upd_conv_take_nth_drop drop_take)
   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 [2] 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.684 -apply (simp add: ball_Un)
   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.709 -apply (simp add: ball_Un)
   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.781 -apply(clarsimp simp add: append_eq_Cons_conv)
   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.870  apply (simp add: le_max_iff_disj)
   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.896  by(simp add:rotate_def funpow_swap1)
   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.906  apply (simp add:rotate_def)
   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>