src/HOL/List.thy
changeset 68719 8aedca31957d
parent 68709 6d9eca4805ff
child 68723 60611540bcff
     1.1 --- a/src/HOL/List.thy	Wed Aug 01 22:59:42 2018 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Aug 04 00:19:15 2018 +0100
     1.3 @@ -1242,7 +1242,7 @@
     1.4  
     1.5  lemma rev_induct [case_names Nil snoc]:
     1.6    "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
     1.7 -apply(simplesubst rev_rev_ident[symmetric])
     1.8 +apply(subst rev_rev_ident[symmetric])
     1.9  apply(rule_tac list = "rev xs" in list.induct, simp_all)
    1.10  done
    1.11  
    1.12 @@ -1489,8 +1489,7 @@
    1.13    case Nil thus ?case by simp
    1.14  next
    1.15    case (Cons x xs) thus ?case
    1.16 -    apply (auto split:if_split_asm)
    1.17 -    using length_filter_le[of P xs] by arith
    1.18 +    using Suc_le_eq by fastforce
    1.19  qed
    1.20  
    1.21  lemma length_filter_conv_card:
    1.22 @@ -1558,17 +1557,17 @@
    1.23  lemma filter_eq_ConsD:
    1.24    "filter P ys = x#xs \<Longrightarrow>
    1.25    \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
    1.26 -by(rule Cons_eq_filterD) simp
    1.27 +  by(rule Cons_eq_filterD) simp
    1.28  
    1.29  lemma filter_eq_Cons_iff:
    1.30    "(filter P ys = x#xs) =
    1.31    (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
    1.32 -by(auto dest:filter_eq_ConsD)
    1.33 +  by(auto dest:filter_eq_ConsD)
    1.34  
    1.35  lemma Cons_eq_filter_iff:
    1.36    "(x#xs = filter P ys) =
    1.37    (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
    1.38 -by(auto dest:Cons_eq_filterD)
    1.39 +  by(auto dest:Cons_eq_filterD)
    1.40  
    1.41  lemma inj_on_filter_key_eq:
    1.42    assumes "inj_on f (insert y (set xs))"
    1.43 @@ -1583,16 +1582,16 @@
    1.44  subsubsection \<open>List partitioning\<close>
    1.45  
    1.46  primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
    1.47 -"partition P [] = ([], [])" |
    1.48 -"partition P (x # xs) =
    1.49 +  "partition P [] = ([], [])" |
    1.50 +  "partition P (x # xs) =
    1.51    (let (yes, no) = partition P xs
    1.52     in if P x then (x # yes, no) else (yes, x # no))"
    1.53  
    1.54  lemma partition_filter1: "fst (partition P xs) = filter P xs"
    1.55 -by (induct xs) (auto simp add: Let_def split_def)
    1.56 +  by (induct xs) (auto simp add: Let_def split_def)
    1.57  
    1.58  lemma partition_filter2: "snd (partition P xs) = filter (Not \<circ> P) xs"
    1.59 -by (induct xs) (auto simp add: Let_def split_def)
    1.60 +  by (induct xs) (auto simp add: Let_def split_def)
    1.61  
    1.62  lemma partition_P:
    1.63    assumes "partition P xs = (yes, no)"
    1.64 @@ -1614,8 +1613,8 @@
    1.65  
    1.66  lemma partition_filter_conv[simp]:
    1.67    "partition f xs = (filter f xs,filter (Not \<circ> f) xs)"
    1.68 -unfolding partition_filter2[symmetric]
    1.69 -unfolding partition_filter1[symmetric] by simp
    1.70 +  unfolding partition_filter2[symmetric]
    1.71 +  unfolding partition_filter1[symmetric] by simp
    1.72  
    1.73  declare partition.simps[simp del]
    1.74  
    1.75 @@ -1623,28 +1622,28 @@
    1.76  subsubsection \<open>@{const concat}\<close>
    1.77  
    1.78  lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
    1.79 -by (induct xs) auto
    1.80 +  by (induct xs) auto
    1.81  
    1.82  lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
    1.83 -by (induct xss) auto
    1.84 +  by (induct xss) auto
    1.85  
    1.86  lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
    1.87 -by (induct xss) auto
    1.88 +  by (induct xss) auto
    1.89  
    1.90  lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
    1.91 -by (induct xs) auto
    1.92 +  by (induct xs) auto
    1.93  
    1.94  lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
    1.95 -by (induct xs) auto
    1.96 +  by (induct xs) auto
    1.97  
    1.98  lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
    1.99 -by (induct xs) auto
   1.100 +  by (induct xs) auto
   1.101  
   1.102  lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
   1.103 -by (induct xs) auto
   1.104 +  by (induct xs) auto
   1.105  
   1.106  lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
   1.107 -by (induct xs) auto
   1.108 +  by (induct xs) auto
   1.109  
   1.110  lemma concat_eq_concat_iff: "\<forall>(x, y) \<in> set (zip xs ys). length x = length y ==> length xs = length ys ==> (concat xs = concat ys) = (xs = ys)"
   1.111  proof (induct xs arbitrary: ys)
   1.112 @@ -1653,21 +1652,21 @@
   1.113  qed (auto)
   1.114  
   1.115  lemma concat_injective: "concat xs = concat ys ==> length xs = length ys ==> \<forall>(x, y) \<in> set (zip xs ys). length x = length y ==> xs = ys"
   1.116 -by (simp add: concat_eq_concat_iff)
   1.117 +  by (simp add: concat_eq_concat_iff)
   1.118  
   1.119  
   1.120  subsubsection \<open>@{const nth}\<close>
   1.121  
   1.122  lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
   1.123 -by auto
   1.124 +  by auto
   1.125  
   1.126  lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"
   1.127 -by auto
   1.128 +  by auto
   1.129  
   1.130  declare nth.simps [simp del]
   1.131  
   1.132  lemma nth_Cons_pos[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
   1.133 -by(auto simp: Nat.gr0_conv_Suc)
   1.134 +  by(auto simp: Nat.gr0_conv_Suc)
   1.135  
   1.136  lemma nth_append:
   1.137    "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
   1.138 @@ -1678,10 +1677,10 @@
   1.139  qed simp
   1.140  
   1.141  lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
   1.142 -by (induct xs) auto
   1.143 +  by (induct xs) auto
   1.144  
   1.145  lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
   1.146 -by (induct xs) auto
   1.147 +  by (induct xs) auto
   1.148  
   1.149  lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
   1.150  proof (induct xs arbitrary: n)
   1.151 @@ -1691,10 +1690,10 @@
   1.152  qed simp
   1.153  
   1.154  lemma nth_tl: "n < length (tl xs) \<Longrightarrow> tl xs ! n = xs ! Suc n"
   1.155 -by (induction xs) auto
   1.156 +  by (induction xs) auto
   1.157  
   1.158  lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
   1.159 -by(cases xs) simp_all
   1.160 +  by(cases xs) simp_all
   1.161  
   1.162  
   1.163  lemma list_eq_iff_nth_eq:
   1.164 @@ -1724,7 +1723,7 @@
   1.165  qed simp
   1.166  
   1.167  lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
   1.168 -by(auto simp:set_conv_nth)
   1.169 +  by(auto simp:set_conv_nth)
   1.170  
   1.171  lemma nth_equal_first_eq:
   1.172    assumes "x \<notin> set xs"
   1.173 @@ -1756,18 +1755,18 @@
   1.174  qed
   1.175  
   1.176  lemma list_ball_nth: "\<lbrakk>n < length xs; \<forall>x \<in> set xs. P x\<rbrakk> \<Longrightarrow> P(xs!n)"
   1.177 -by (auto simp add: set_conv_nth)
   1.178 +  by (auto simp add: set_conv_nth)
   1.179  
   1.180  lemma nth_mem [simp]: "n < length xs \<Longrightarrow> xs!n \<in> set xs"
   1.181 -by (auto simp add: set_conv_nth)
   1.182 +  by (auto simp add: set_conv_nth)
   1.183  
   1.184  lemma all_nth_imp_all_set:
   1.185    "\<lbrakk>\<forall>i < length xs. P(xs!i); x \<in> set xs\<rbrakk> \<Longrightarrow> P x"
   1.186 -by (auto simp add: set_conv_nth)
   1.187 +  by (auto simp add: set_conv_nth)
   1.188  
   1.189  lemma all_set_conv_all_nth:
   1.190    "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
   1.191 -by (auto simp add: set_conv_nth)
   1.192 +  by (auto simp add: set_conv_nth)
   1.193  
   1.194  lemma rev_nth:
   1.195    "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
   1.196 @@ -1811,20 +1810,20 @@
   1.197  subsubsection \<open>@{const list_update}\<close>
   1.198  
   1.199  lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
   1.200 -by (induct xs arbitrary: i) (auto split: nat.split)
   1.201 +  by (induct xs arbitrary: i) (auto split: nat.split)
   1.202  
   1.203  lemma nth_list_update:
   1.204 -"i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
   1.205 -by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
   1.206 +  "i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
   1.207 +  by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
   1.208  
   1.209  lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"
   1.210 -by (simp add: nth_list_update)
   1.211 +  by (simp add: nth_list_update)
   1.212  
   1.213  lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
   1.214 -by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
   1.215 +  by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
   1.216  
   1.217  lemma list_update_id[simp]: "xs[i := xs!i] = xs"
   1.218 -by (induct xs arbitrary: i) (simp_all split:nat.splits)
   1.219 +  by (induct xs arbitrary: i) (simp_all split:nat.splits)
   1.220  
   1.221  lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
   1.222  proof (induct xs arbitrary: i)
   1.223 @@ -1834,44 +1833,44 @@
   1.224  qed simp
   1.225  
   1.226  lemma list_update_nonempty[simp]: "xs[k:=x] = [] \<longleftrightarrow> xs=[]"
   1.227 -by (simp only: length_0_conv[symmetric] length_list_update)
   1.228 +  by (simp only: length_0_conv[symmetric] length_list_update)
   1.229  
   1.230  lemma list_update_same_conv:
   1.231    "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
   1.232 -by (induct xs arbitrary: i) (auto split: nat.split)
   1.233 +  by (induct xs arbitrary: i) (auto split: nat.split)
   1.234  
   1.235  lemma list_update_append1:
   1.236    "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
   1.237 -by (induct xs arbitrary: i)(auto split:nat.split)
   1.238 +  by (induct xs arbitrary: i)(auto split:nat.split)
   1.239  
   1.240  lemma list_update_append:
   1.241    "(xs @ ys) [n:= x] =
   1.242    (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
   1.243 -by (induct xs arbitrary: n) (auto split:nat.splits)
   1.244 +  by (induct xs arbitrary: n) (auto split:nat.splits)
   1.245  
   1.246  lemma list_update_length [simp]:
   1.247    "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
   1.248 -by (induct xs, auto)
   1.249 +  by (induct xs, auto)
   1.250  
   1.251  lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]"
   1.252 -by(induct xs arbitrary: k)(auto split:nat.splits)
   1.253 +  by(induct xs arbitrary: k)(auto split:nat.splits)
   1.254  
   1.255  lemma rev_update:
   1.256    "k < length xs \<Longrightarrow> rev (xs[k:= y]) = (rev xs)[length xs - k - 1 := y]"
   1.257 -by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)
   1.258 +  by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)
   1.259  
   1.260  lemma update_zip:
   1.261    "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
   1.262 -by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
   1.263 +  by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
   1.264  
   1.265  lemma set_update_subset_insert: "set(xs[i:=x]) \<le> insert x (set xs)"
   1.266 -by (induct xs arbitrary: i) (auto split: nat.split)
   1.267 +  by (induct xs arbitrary: i) (auto split: nat.split)
   1.268  
   1.269  lemma set_update_subsetI: "\<lbrakk>set xs \<subseteq> A; x \<in> A\<rbrakk> \<Longrightarrow> set(xs[i := x]) \<subseteq> A"
   1.270 -by (blast dest!: set_update_subset_insert [THEN subsetD])
   1.271 +  by (blast dest!: set_update_subset_insert [THEN subsetD])
   1.272  
   1.273  lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
   1.274 -by (induct xs arbitrary: n) (auto split:nat.splits)
   1.275 +  by (induct xs arbitrary: n) (auto split:nat.splits)
   1.276  
   1.277  lemma list_update_overwrite[simp]:
   1.278    "xs [i := x, i := y] = xs [i := y]"
   1.279 @@ -1885,67 +1884,67 @@
   1.280    "[][i := y] = []"
   1.281    "(x # xs)[0 := y] = y # xs"
   1.282    "(x # xs)[Suc i := y] = x # xs[i := y]"
   1.283 -by simp_all
   1.284 +  by simp_all
   1.285  
   1.286  
   1.287  subsubsection \<open>@{const last} and @{const butlast}\<close>
   1.288  
   1.289  lemma last_snoc [simp]: "last (xs @ [x]) = x"
   1.290 -by (induct xs) auto
   1.291 +  by (induct xs) auto
   1.292  
   1.293  lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
   1.294 -by (induct xs) auto
   1.295 +  by (induct xs) auto
   1.296  
   1.297  lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
   1.298 -by simp
   1.299 +  by simp
   1.300  
   1.301  lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
   1.302 -by simp
   1.303 +  by simp
   1.304  
   1.305  lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
   1.306 -by (induct xs) (auto)
   1.307 +  by (induct xs) (auto)
   1.308  
   1.309  lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
   1.310 -by(simp add:last_append)
   1.311 +  by(simp add:last_append)
   1.312  
   1.313  lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
   1.314 -by(simp add:last_append)
   1.315 +  by(simp add:last_append)
   1.316  
   1.317  lemma last_tl: "xs = [] \<or> tl xs \<noteq> [] \<Longrightarrow>last (tl xs) = last xs"
   1.318 -by (induct xs) simp_all
   1.319 +  by (induct xs) simp_all
   1.320  
   1.321  lemma butlast_tl: "butlast (tl xs) = tl (butlast xs)"
   1.322 -by (induct xs) simp_all
   1.323 +  by (induct xs) simp_all
   1.324  
   1.325  lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
   1.326 -by(rule rev_exhaust[of xs]) simp_all
   1.327 +  by(rule rev_exhaust[of xs]) simp_all
   1.328  
   1.329  lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
   1.330 -by(cases xs) simp_all
   1.331 +  by(cases xs) simp_all
   1.332  
   1.333  lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
   1.334 -by (induct as) auto
   1.335 +  by (induct as) auto
   1.336  
   1.337  lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
   1.338 -by (induct xs rule: rev_induct) auto
   1.339 +  by (induct xs rule: rev_induct) auto
   1.340  
   1.341  lemma butlast_append:
   1.342    "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
   1.343 -by (induct xs arbitrary: ys) auto
   1.344 +  by (induct xs arbitrary: ys) auto
   1.345  
   1.346  lemma append_butlast_last_id [simp]:
   1.347    "xs \<noteq> [] \<Longrightarrow> butlast xs @ [last xs] = xs"
   1.348 -by (induct xs) auto
   1.349 +  by (induct xs) auto
   1.350  
   1.351  lemma in_set_butlastD: "x \<in> set (butlast xs) \<Longrightarrow> x \<in> set xs"
   1.352 -by (induct xs) (auto split: if_split_asm)
   1.353 +  by (induct xs) (auto split: if_split_asm)
   1.354  
   1.355  lemma in_set_butlast_appendI:
   1.356    "x \<in> set (butlast xs) \<or> x \<in> set (butlast ys) \<Longrightarrow> x \<in> set (butlast (xs @ ys))"
   1.357 -by (auto dest: in_set_butlastD simp add: butlast_append)
   1.358 +  by (auto dest: in_set_butlastD simp add: butlast_append)
   1.359  
   1.360  lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"
   1.361 -by (induct xs arbitrary: n)(auto split:nat.split)
   1.362 +  by (induct xs arbitrary: n)(auto split:nat.split)
   1.363  
   1.364  lemma nth_butlast:
   1.365    assumes "n < length (butlast xs)" shows "butlast xs ! n = xs ! n"
   1.366 @@ -1957,82 +1956,82 @@
   1.367  qed simp
   1.368  
   1.369  lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
   1.370 -by(induct xs)(auto simp:neq_Nil_conv)
   1.371 +  by(induct xs)(auto simp:neq_Nil_conv)
   1.372  
   1.373  lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
   1.374 -by (induction xs rule: induct_list012) simp_all
   1.375 +  by (induction xs rule: induct_list012) simp_all
   1.376  
   1.377  lemma last_list_update:
   1.378    "xs \<noteq> [] \<Longrightarrow> last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"
   1.379 -by (auto simp: last_conv_nth)
   1.380 +  by (auto simp: last_conv_nth)
   1.381  
   1.382  lemma butlast_list_update:
   1.383    "butlast(xs[k:=x]) =
   1.384    (if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])"
   1.385 -by(cases xs rule:rev_cases)(auto simp: list_update_append split: nat.splits)
   1.386 +  by(cases xs rule:rev_cases)(auto simp: list_update_append split: nat.splits)
   1.387  
   1.388  lemma last_map: "xs \<noteq> [] \<Longrightarrow> last (map f xs) = f (last xs)"
   1.389 -by (cases xs rule: rev_cases) simp_all
   1.390 +  by (cases xs rule: rev_cases) simp_all
   1.391  
   1.392  lemma map_butlast: "map f (butlast xs) = butlast (map f xs)"
   1.393 -by (induct xs) simp_all
   1.394 +  by (induct xs) simp_all
   1.395  
   1.396  lemma snoc_eq_iff_butlast:
   1.397    "xs @ [x] = ys \<longleftrightarrow> (ys \<noteq> [] \<and> butlast ys = xs \<and> last ys = x)"
   1.398 -by fastforce
   1.399 +  by fastforce
   1.400  
   1.401  corollary longest_common_suffix:
   1.402    "\<exists>ss xs' ys'. xs = xs' @ ss \<and> ys = ys' @ ss
   1.403         \<and> (xs' = [] \<or> ys' = [] \<or> last xs' \<noteq> last ys')"
   1.404 -using longest_common_prefix[of "rev xs" "rev ys"]
   1.405 -unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)
   1.406 +  using longest_common_prefix[of "rev xs" "rev ys"]
   1.407 +  unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)
   1.408  
   1.409  
   1.410  subsubsection \<open>@{const take} and @{const drop}\<close>
   1.411  
   1.412  lemma take_0: "take 0 xs = []"
   1.413 -by (induct xs) auto
   1.414 +  by (induct xs) auto
   1.415  
   1.416  lemma drop_0: "drop 0 xs = xs"
   1.417 -by (induct xs) auto
   1.418 +  by (induct xs) auto
   1.419  
   1.420  lemma take0[simp]: "take 0 = (\<lambda>xs. [])"
   1.421 -by(rule ext) (rule take_0)
   1.422 +  by(rule ext) (rule take_0)
   1.423  
   1.424  lemma drop0[simp]: "drop 0 = (\<lambda>x. x)"
   1.425 -by(rule ext) (rule drop_0)
   1.426 +  by(rule ext) (rule drop_0)
   1.427  
   1.428  lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
   1.429 -by simp
   1.430 +  by simp
   1.431  
   1.432  lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
   1.433 -by simp
   1.434 +  by simp
   1.435  
   1.436  declare take_Cons [simp del] and drop_Cons [simp del]
   1.437  
   1.438  lemma take_Suc: "xs \<noteq> [] \<Longrightarrow> take (Suc n) xs = hd xs # take n (tl xs)"
   1.439 -by(clarsimp simp add:neq_Nil_conv)
   1.440 +  by(clarsimp simp add:neq_Nil_conv)
   1.441  
   1.442  lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
   1.443 -by(cases xs, simp_all)
   1.444 +  by(cases xs, simp_all)
   1.445  
   1.446  lemma hd_take[simp]: "j > 0 \<Longrightarrow> hd (take j xs) = hd xs"
   1.447 -by (metis gr0_conv_Suc list.sel(1) take.simps(1) take_Suc)
   1.448 +  by (metis gr0_conv_Suc list.sel(1) take.simps(1) take_Suc)
   1.449  
   1.450  lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
   1.451 -by (induct xs arbitrary: n) simp_all
   1.452 +  by (induct xs arbitrary: n) simp_all
   1.453  
   1.454  lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
   1.455 -by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
   1.456 +  by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
   1.457  
   1.458  lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
   1.459 -by (cases n, simp, cases xs, auto)
   1.460 +  by (cases n, simp, cases xs, auto)
   1.461  
   1.462  lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
   1.463 -by (simp only: drop_tl)
   1.464 +  by (simp only: drop_tl)
   1.465  
   1.466  lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
   1.467 -by (induct xs arbitrary: n, simp)(auto simp: drop_Cons nth_Cons split: nat.splits)
   1.468 +  by (induct xs arbitrary: n, simp)(auto simp: drop_Cons nth_Cons split: nat.splits)
   1.469  
   1.470  lemma take_Suc_conv_app_nth:
   1.471    "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
   1.472 @@ -2049,24 +2048,24 @@
   1.473  qed simp
   1.474  
   1.475  lemma length_take [simp]: "length (take n xs) = min (length xs) n"
   1.476 -by (induct n arbitrary: xs) (auto, case_tac xs, auto)
   1.477 +  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
   1.478  
   1.479  lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
   1.480 -by (induct n arbitrary: xs) (auto, case_tac xs, auto)
   1.481 +  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
   1.482  
   1.483  lemma take_all [simp]: "length xs \<le> n ==> take n xs = xs"
   1.484 -by (induct n arbitrary: xs) (auto, case_tac xs, auto)
   1.485 +  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
   1.486  
   1.487  lemma drop_all [simp]: "length xs \<le> n ==> drop n xs = []"
   1.488 -by (induct n arbitrary: xs) (auto, case_tac xs, auto)
   1.489 +  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
   1.490  
   1.491  lemma take_append [simp]:
   1.492    "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
   1.493 -by (induct n arbitrary: xs) (auto, case_tac xs, auto)
   1.494 +  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
   1.495  
   1.496  lemma drop_append [simp]:
   1.497    "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
   1.498 -by (induct n arbitrary: xs) (auto, case_tac xs, auto)
   1.499 +  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
   1.500  
   1.501  lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
   1.502  proof (induct m arbitrary: xs n)
   1.503 @@ -2087,7 +2086,7 @@
   1.504  qed auto
   1.505  
   1.506  lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
   1.507 -by(induct xs arbitrary: m n)(auto simp: take_Cons drop_Cons split: nat.split)
   1.508 +  by(induct xs arbitrary: m n)(auto simp: take_Cons drop_Cons split: nat.split)
   1.509  
   1.510  lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
   1.511  proof (induct n arbitrary: xs)
   1.512 @@ -2096,10 +2095,10 @@
   1.513  qed auto
   1.514  
   1.515  lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
   1.516 -by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split)
   1.517 +  by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split)
   1.518  
   1.519  lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs \<le> n)"
   1.520 -by (induct xs arbitrary: n) (auto simp: drop_Cons split:nat.split)
   1.521 +  by (induct xs arbitrary: n) (auto simp: drop_Cons split:nat.split)
   1.522  
   1.523  lemma take_map: "take n (map f xs) = map f (take n xs)"
   1.524  proof (induct n arbitrary: xs)
   1.525 @@ -2146,19 +2145,19 @@
   1.526  
   1.527  lemma butlast_take:
   1.528    "n \<le> length xs ==> butlast (take n xs) = take (n - 1) xs"
   1.529 -by (simp add: butlast_conv_take min.absorb1 min.absorb2)
   1.530 +  by (simp add: butlast_conv_take min.absorb1 min.absorb2)
   1.531  
   1.532  lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
   1.533 -by (simp add: butlast_conv_take drop_take ac_simps)
   1.534 +  by (simp add: butlast_conv_take drop_take ac_simps)
   1.535  
   1.536  lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
   1.537 -by (simp add: butlast_conv_take min.absorb1)
   1.538 +  by (simp add: butlast_conv_take min.absorb1)
   1.539  
   1.540  lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
   1.541 -by (simp add: butlast_conv_take drop_take ac_simps)
   1.542 +  by (simp add: butlast_conv_take drop_take ac_simps)
   1.543  
   1.544  lemma hd_drop_conv_nth: "n < length xs \<Longrightarrow> hd(drop n xs) = xs!n"
   1.545 -by(simp add: hd_conv_nth)
   1.546 +  by(simp add: hd_conv_nth)
   1.547  
   1.548  lemma set_take_subset_set_take:
   1.549    "m \<le> n \<Longrightarrow> set(take m xs) \<le> set(take n xs)"
   1.550 @@ -2168,10 +2167,10 @@
   1.551  qed simp
   1.552  
   1.553  lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
   1.554 -by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
   1.555 +  by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
   1.556  
   1.557  lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
   1.558 -by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
   1.559 +  by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
   1.560  
   1.561  lemma set_drop_subset_set_drop:
   1.562    "m \<ge> n \<Longrightarrow> set(drop m xs) \<le> set(drop n xs)"
   1.563 @@ -2182,10 +2181,10 @@
   1.564  qed simp
   1.565  
   1.566  lemma in_set_takeD: "x \<in> set(take n xs) \<Longrightarrow> x \<in> set xs"
   1.567 -using set_take_subset by fast
   1.568 +  using set_take_subset by fast
   1.569  
   1.570  lemma in_set_dropD: "x \<in> set(drop n xs) \<Longrightarrow> x \<in> set xs"
   1.571 -using set_drop_subset by fast
   1.572 +  using set_drop_subset by fast
   1.573  
   1.574  lemma append_eq_conv_conj:
   1.575    "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
   1.576 @@ -2226,10 +2225,10 @@
   1.577  qed
   1.578  
   1.579  lemma take_update_cancel[simp]: "n \<le> m \<Longrightarrow> take n (xs[m := y]) = take n xs"
   1.580 -by(simp add: list_eq_iff_nth_eq)
   1.581 +  by(simp add: list_eq_iff_nth_eq)
   1.582  
   1.583  lemma drop_update_cancel[simp]: "n < m \<Longrightarrow> drop m (xs[n := x]) = drop m xs"
   1.584 -by(simp add: list_eq_iff_nth_eq)
   1.585 +  by(simp add: list_eq_iff_nth_eq)
   1.586  
   1.587  lemma upd_conv_take_nth_drop:
   1.588    "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
   1.589 @@ -2258,27 +2257,27 @@
   1.590  qed auto
   1.591  
   1.592  lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
   1.593 -by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
   1.594 +  by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
   1.595  
   1.596  
   1.597  subsubsection \<open>@{const takeWhile} and @{const dropWhile}\<close>
   1.598  
   1.599  lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
   1.600 -by (induct xs) auto
   1.601 +  by (induct xs) auto
   1.602  
   1.603  lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
   1.604 -by (induct xs) auto
   1.605 +  by (induct xs) auto
   1.606  
   1.607  lemma takeWhile_append1 [simp]:
   1.608    "\<lbrakk>x \<in> set xs; \<not>P(x)\<rbrakk> \<Longrightarrow> takeWhile P (xs @ ys) = takeWhile P xs"
   1.609 -by (induct xs) auto
   1.610 +  by (induct xs) auto
   1.611  
   1.612  lemma takeWhile_append2 [simp]:
   1.613    "(\<And>x. x \<in> set xs \<Longrightarrow> P x) \<Longrightarrow> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
   1.614 -by (induct xs) auto
   1.615 +  by (induct xs) auto
   1.616  
   1.617  lemma takeWhile_tail: "\<not> P x \<Longrightarrow> takeWhile P (xs @ (x#l)) = takeWhile P xs"
   1.618 -by (induct xs) auto
   1.619 +  by (induct xs) auto
   1.620  
   1.621  lemma takeWhile_nth: "j < length (takeWhile P xs) \<Longrightarrow> takeWhile P xs ! j = xs ! j"
   1.622    by (metis nth_append takeWhile_dropWhile_id)
   1.623 @@ -2288,62 +2287,62 @@
   1.624    by (metis add.commute nth_append_length_plus takeWhile_dropWhile_id)
   1.625  
   1.626  lemma length_dropWhile_le: "length (dropWhile P xs) \<le> length xs"
   1.627 -by (induct xs) auto
   1.628 +  by (induct xs) auto
   1.629  
   1.630  lemma dropWhile_append1 [simp]:
   1.631    "\<lbrakk>x \<in> set xs; \<not>P(x)\<rbrakk> \<Longrightarrow> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
   1.632 -by (induct xs) auto
   1.633 +  by (induct xs) auto
   1.634  
   1.635  lemma dropWhile_append2 [simp]:
   1.636    "(\<And>x. x \<in> set xs \<Longrightarrow> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
   1.637 -by (induct xs) auto
   1.638 +  by (induct xs) auto
   1.639  
   1.640  lemma dropWhile_append3:
   1.641    "\<not> P y \<Longrightarrow>dropWhile P (xs @ y # ys) = dropWhile P xs @ y # ys"
   1.642 -by (induct xs) auto
   1.643 +  by (induct xs) auto
   1.644  
   1.645  lemma dropWhile_last:
   1.646    "x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> last (dropWhile P xs) = last xs"
   1.647 -by (auto simp add: dropWhile_append3 in_set_conv_decomp)
   1.648 +  by (auto simp add: dropWhile_append3 in_set_conv_decomp)
   1.649  
   1.650  lemma set_dropWhileD: "x \<in> set (dropWhile P xs) \<Longrightarrow> x \<in> set xs"
   1.651 -by (induct xs) (auto split: if_split_asm)
   1.652 +  by (induct xs) (auto split: if_split_asm)
   1.653  
   1.654  lemma set_takeWhileD: "x \<in> set (takeWhile P xs) \<Longrightarrow> x \<in> set xs \<and> P x"
   1.655 -by (induct xs) (auto split: if_split_asm)
   1.656 +  by (induct xs) (auto split: if_split_asm)
   1.657  
   1.658  lemma takeWhile_eq_all_conv[simp]:
   1.659    "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
   1.660 -by(induct xs, auto)
   1.661 +  by(induct xs, auto)
   1.662  
   1.663  lemma dropWhile_eq_Nil_conv[simp]:
   1.664    "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
   1.665 -by(induct xs, auto)
   1.666 +  by(induct xs, auto)
   1.667  
   1.668  lemma dropWhile_eq_Cons_conv:
   1.669    "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys \<and> \<not> P y)"
   1.670 -by(induct xs, auto)
   1.671 +  by(induct xs, auto)
   1.672  
   1.673  lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"
   1.674 -by (induct xs) (auto dest: set_takeWhileD)
   1.675 +  by (induct xs) (auto dest: set_takeWhileD)
   1.676  
   1.677  lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
   1.678 -by (induct xs) auto
   1.679 +  by (induct xs) auto
   1.680  
   1.681  lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \<circ> f) xs)"
   1.682 -by (induct xs) auto
   1.683 +  by (induct xs) auto
   1.684  
   1.685  lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \<circ> f) xs)"
   1.686 -by (induct xs) auto
   1.687 +  by (induct xs) auto
   1.688  
   1.689  lemma takeWhile_eq_take: "takeWhile P xs = take (length (takeWhile P xs)) xs"
   1.690 -by (induct xs) auto
   1.691 +  by (induct xs) auto
   1.692  
   1.693  lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs"
   1.694 -by (induct xs) auto
   1.695 +  by (induct xs) auto
   1.696  
   1.697  lemma hd_dropWhile: "dropWhile P xs \<noteq> [] \<Longrightarrow> \<not> P (hd (dropWhile P xs))"
   1.698 -by (induct xs) auto
   1.699 +  by (induct xs) auto
   1.700  
   1.701  lemma takeWhile_eq_filter:
   1.702    assumes "\<And> x. x \<in> set (dropWhile P xs) \<Longrightarrow> \<not> P x"
   1.703 @@ -2384,12 +2383,12 @@
   1.704        thus "\<not> P (xs ! n')" using Cons by auto
   1.705      qed
   1.706      ultimately show ?thesis by simp
   1.707 -   qed
   1.708 +  qed
   1.709  qed
   1.710  
   1.711  lemma nth_length_takeWhile:
   1.712    "length (takeWhile P xs) < length xs \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"
   1.713 -by (induct xs) auto
   1.714 +  by (induct xs) auto
   1.715  
   1.716  lemma length_takeWhile_less_P_nth:
   1.717    assumes all: "\<And> i. i < j \<Longrightarrow> P (xs ! i)" and "j \<le> length xs"
   1.718 @@ -2402,7 +2401,7 @@
   1.719  
   1.720  lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
   1.721    takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
   1.722 -by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
   1.723 +  by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
   1.724  
   1.725  lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
   1.726    dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
   1.727 @@ -2414,34 +2413,34 @@
   1.728  
   1.729  lemma takeWhile_not_last:
   1.730    "distinct xs \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
   1.731 -by(induction xs rule: induct_list012) auto
   1.732 +  by(induction xs rule: induct_list012) auto
   1.733  
   1.734  lemma takeWhile_cong [fundef_cong]:
   1.735    "\<lbrakk>l = k; \<And>x. x \<in> set l \<Longrightarrow> P x = Q x\<rbrakk>
   1.736    \<Longrightarrow> takeWhile P l = takeWhile Q k"
   1.737 -by (induct k arbitrary: l) (simp_all)
   1.738 +  by (induct k arbitrary: l) (simp_all)
   1.739  
   1.740  lemma dropWhile_cong [fundef_cong]:
   1.741    "\<lbrakk>l = k; \<And>x. x \<in> set l \<Longrightarrow> P x = Q x\<rbrakk>
   1.742    \<Longrightarrow> dropWhile P l = dropWhile Q k"
   1.743 -by (induct k arbitrary: l, simp_all)
   1.744 +  by (induct k arbitrary: l, simp_all)
   1.745  
   1.746  lemma takeWhile_idem [simp]:
   1.747    "takeWhile P (takeWhile P xs) = takeWhile P xs"
   1.748 -by (induct xs) auto
   1.749 +  by (induct xs) auto
   1.750  
   1.751  lemma dropWhile_idem [simp]:
   1.752    "dropWhile P (dropWhile P xs) = dropWhile P xs"
   1.753 -by (induct xs) auto
   1.754 +  by (induct xs) auto
   1.755  
   1.756  
   1.757  subsubsection \<open>@{const zip}\<close>
   1.758  
   1.759  lemma zip_Nil [simp]: "zip [] ys = []"
   1.760 -by (induct ys) auto
   1.761 +  by (induct ys) auto
   1.762  
   1.763  lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
   1.764 -by simp
   1.765 +  by simp
   1.766  
   1.767  declare zip_Cons [simp del]
   1.768  
   1.769 @@ -2449,15 +2448,15 @@
   1.770    "zip [] ys = []"
   1.771    "zip xs [] = []"
   1.772    "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
   1.773 -by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+
   1.774 +  by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+
   1.775  
   1.776  lemma zip_Cons1:
   1.777    "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
   1.778 -by(auto split:list.split)
   1.779 +  by(auto split:list.split)
   1.780  
   1.781  lemma length_zip [simp]:
   1.782    "length (zip xs ys) = min (length xs) (length ys)"
   1.783 -by (induct xs ys rule:list_induct2') auto
   1.784 +  by (induct xs ys rule:list_induct2') auto
   1.785  
   1.786  lemma zip_obtain_same_length:
   1.787    assumes "\<And>zs ws n. length zs = length ws \<Longrightarrow> n = min (length xs) (length ys)
   1.788 @@ -2479,21 +2478,21 @@
   1.789  lemma zip_append1:
   1.790    "zip (xs @ ys) zs =
   1.791    zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
   1.792 -by (induct xs zs rule:list_induct2') auto
   1.793 +  by (induct xs zs rule:list_induct2') auto
   1.794  
   1.795  lemma zip_append2:
   1.796    "zip xs (ys @ zs) =
   1.797    zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
   1.798 -by (induct xs ys rule:list_induct2') auto
   1.799 +  by (induct xs ys rule:list_induct2') auto
   1.800  
   1.801  lemma zip_append [simp]:
   1.802    "[| length xs = length us |] ==>
   1.803    zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
   1.804 -by (simp add: zip_append1)
   1.805 +  by (simp add: zip_append1)
   1.806  
   1.807  lemma zip_rev:
   1.808    "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
   1.809 -by (induct rule:list_induct2, simp_all)
   1.810 +  by (induct rule:list_induct2, simp_all)
   1.811  
   1.812  lemma zip_map_map:
   1.813    "zip (map f xs) (map g ys) = map (\<lambda> (x, y). (f x, g y)) (zip xs ys)"
   1.814 @@ -2508,23 +2507,23 @@
   1.815  
   1.816  lemma zip_map1:
   1.817    "zip (map f xs) ys = map (\<lambda>(x, y). (f x, y)) (zip xs ys)"
   1.818 -using zip_map_map[of f xs "\<lambda>x. x" ys] by simp
   1.819 +  using zip_map_map[of f xs "\<lambda>x. x" ys] by simp
   1.820  
   1.821  lemma zip_map2:
   1.822    "zip xs (map f ys) = map (\<lambda>(x, y). (x, f y)) (zip xs ys)"
   1.823 -using zip_map_map[of "\<lambda>x. x" xs f ys] by simp
   1.824 +  using zip_map_map[of "\<lambda>x. x" xs f ys] by simp
   1.825  
   1.826  lemma map_zip_map:
   1.827    "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
   1.828 -by (auto simp: zip_map1)
   1.829 +  by (auto simp: zip_map1)
   1.830  
   1.831  lemma map_zip_map2:
   1.832    "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
   1.833 -by (auto simp: zip_map2)
   1.834 +  by (auto simp: zip_map2)
   1.835  
   1.836  text\<open>Courtesy of Andreas Lochbihler:\<close>
   1.837  lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
   1.838 -by(induct xs) auto
   1.839 +  by(induct xs) auto
   1.840  
   1.841  lemma nth_zip [simp]:
   1.842    "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
   1.843 @@ -2536,10 +2535,10 @@
   1.844  
   1.845  lemma set_zip:
   1.846    "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
   1.847 -by(simp add: set_conv_nth cong: rev_conj_cong)
   1.848 +  by(simp add: set_conv_nth cong: rev_conj_cong)
   1.849  
   1.850  lemma zip_same: "((a,b) \<in> set (zip xs xs)) = (a \<in> set xs \<and> a = b)"
   1.851 -by(induct xs) auto
   1.852 +  by(induct xs) auto
   1.853  
   1.854  lemma zip_update: "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
   1.855    by (simp add: update_zip)
   1.856 @@ -2553,7 +2552,7 @@
   1.857  qed auto
   1.858  
   1.859  lemma zip_replicate1: "zip (replicate n x) ys = map (Pair x) (take n ys)"
   1.860 -by(induction ys arbitrary: n)(case_tac [2] n, simp_all)
   1.861 +  by(induction ys arbitrary: n)(case_tac [2] n, simp_all)
   1.862  
   1.863  lemma take_zip: "take n (zip xs ys) = zip (take n xs) (take n ys)"
   1.864  proof (induct n arbitrary: xs ys)
   1.865 @@ -2580,26 +2579,26 @@
   1.866  qed simp
   1.867  
   1.868  lemma set_zip_leftD: "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
   1.869 -by (induct xs ys rule:list_induct2') auto
   1.870 +  by (induct xs ys rule:list_induct2') auto
   1.871  
   1.872  lemma set_zip_rightD: "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
   1.873 -by (induct xs ys rule:list_induct2') auto
   1.874 +  by (induct xs ys rule:list_induct2') auto
   1.875  
   1.876  lemma in_set_zipE:
   1.877    "(x,y) \<in> set(zip xs ys) \<Longrightarrow> (\<lbrakk> x \<in> set xs; y \<in> set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
   1.878 -by(blast dest: set_zip_leftD set_zip_rightD)
   1.879 +  by(blast dest: set_zip_leftD set_zip_rightD)
   1.880  
   1.881  lemma zip_map_fst_snd: "zip (map fst zs) (map snd zs) = zs"
   1.882 -by (induct zs) simp_all
   1.883 +  by (induct zs) simp_all
   1.884  
   1.885  lemma zip_eq_conv:
   1.886    "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
   1.887 -by (auto simp add: zip_map_fst_snd)
   1.888 +  by (auto simp add: zip_map_fst_snd)
   1.889  
   1.890  lemma in_set_zip:
   1.891    "p \<in> set (zip xs ys) \<longleftrightarrow> (\<exists>n. xs ! n = fst p \<and> ys ! n = snd p
   1.892    \<and> n < length xs \<and> n < length ys)"
   1.893 -by (cases p) (auto simp add: set_zip)
   1.894 +  by (cases p) (auto simp add: set_zip)
   1.895  
   1.896  lemma in_set_impl_in_set_zip1:
   1.897    assumes "length xs = length ys"
   1.898 @@ -2633,25 +2632,25 @@
   1.899  
   1.900  lemma list_all2_lengthD [intro?]:
   1.901    "list_all2 P xs ys ==> length xs = length ys"
   1.902 -by (simp add: list_all2_iff)
   1.903 +  by (simp add: list_all2_iff)
   1.904  
   1.905  lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
   1.906 -by (simp add: list_all2_iff)
   1.907 +  by (simp add: list_all2_iff)
   1.908  
   1.909  lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
   1.910 -by (simp add: list_all2_iff)
   1.911 +  by (simp add: list_all2_iff)
   1.912  
   1.913  lemma list_all2_Cons [iff, code]:
   1.914    "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
   1.915 -by (auto simp add: list_all2_iff)
   1.916 +  by (auto simp add: list_all2_iff)
   1.917  
   1.918  lemma list_all2_Cons1:
   1.919    "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
   1.920 -by (cases ys) auto
   1.921 +  by (cases ys) auto
   1.922  
   1.923  lemma list_all2_Cons2:
   1.924    "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
   1.925 -by (cases xs) auto
   1.926 +  by (cases xs) auto
   1.927  
   1.928  lemma list_all2_induct
   1.929    [consumes 1, case_names Nil Cons, induct set: list_all2]:
   1.930 @@ -2660,16 +2659,16 @@
   1.931    assumes Cons: "\<And>x xs y ys.
   1.932      \<lbrakk>P x y; list_all2 P xs ys; R xs ys\<rbrakk> \<Longrightarrow> R (x # xs) (y # ys)"
   1.933    shows "R xs ys"
   1.934 -using P
   1.935 -by (induct xs arbitrary: ys) (auto simp add: list_all2_Cons1 Nil Cons)
   1.936 +  using P
   1.937 +  by (induct xs arbitrary: ys) (auto simp add: list_all2_Cons1 Nil Cons)
   1.938  
   1.939  lemma list_all2_rev [iff]:
   1.940    "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
   1.941 -by (simp add: list_all2_iff zip_rev cong: conj_cong)
   1.942 +  by (simp add: list_all2_iff zip_rev cong: conj_cong)
   1.943  
   1.944  lemma list_all2_rev1:
   1.945    "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
   1.946 -by (subst list_all2_rev [symmetric]) simp
   1.947 +  by (subst list_all2_rev [symmetric]) simp
   1.948  
   1.949  lemma list_all2_append1:
   1.950    "list_all2 P (xs @ ys) zs =
   1.951 @@ -2708,21 +2707,21 @@
   1.952  lemma list_all2_append:
   1.953    "length xs = length ys \<Longrightarrow>
   1.954    list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
   1.955 -by (induct rule:list_induct2, simp_all)
   1.956 +  by (induct rule:list_induct2, simp_all)
   1.957  
   1.958  lemma list_all2_appendI [intro?, trans]:
   1.959    "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
   1.960 -by (simp add: list_all2_append list_all2_lengthD)
   1.961 +  by (simp add: list_all2_append list_all2_lengthD)
   1.962  
   1.963  lemma list_all2_conv_all_nth:
   1.964    "list_all2 P xs ys =
   1.965    (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
   1.966 -by (force simp add: list_all2_iff set_zip)
   1.967 +  by (force simp add: list_all2_iff set_zip)
   1.968  
   1.969  lemma list_all2_trans:
   1.970    assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
   1.971    shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
   1.972 -        (is "!!bs cs. PROP ?Q as bs cs")
   1.973 +    (is "!!bs cs. PROP ?Q as bs cs")
   1.974  proof (induct as)
   1.975    fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
   1.976    show "!!cs. PROP ?Q (x # xs) bs cs"
   1.977 @@ -2735,35 +2734,35 @@
   1.978  
   1.979  lemma list_all2_all_nthI [intro?]:
   1.980    "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
   1.981 -by (simp add: list_all2_conv_all_nth)
   1.982 +  by (simp add: list_all2_conv_all_nth)
   1.983  
   1.984  lemma list_all2I:
   1.985    "\<forall>x \<in> set (zip a b). case_prod P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
   1.986 -by (simp add: list_all2_iff)
   1.987 +  by (simp add: list_all2_iff)
   1.988  
   1.989  lemma list_all2_nthD:
   1.990    "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
   1.991 -by (simp add: list_all2_conv_all_nth)
   1.992 +  by (simp add: list_all2_conv_all_nth)
   1.993  
   1.994  lemma list_all2_nthD2:
   1.995    "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
   1.996 -by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
   1.997 +  by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
   1.998  
   1.999  lemma list_all2_map1:
  1.1000    "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
  1.1001 -by (simp add: list_all2_conv_all_nth)
  1.1002 +  by (simp add: list_all2_conv_all_nth)
  1.1003  
  1.1004  lemma list_all2_map2:
  1.1005    "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
  1.1006 -by (auto simp add: list_all2_conv_all_nth)
  1.1007 +  by (auto simp add: list_all2_conv_all_nth)
  1.1008  
  1.1009  lemma list_all2_refl [intro?]:
  1.1010    "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
  1.1011 -by (simp add: list_all2_conv_all_nth)
  1.1012 +  by (simp add: list_all2_conv_all_nth)
  1.1013  
  1.1014  lemma list_all2_update_cong:
  1.1015    "\<lbrakk> list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
  1.1016 -by (cases "i < length ys") (auto simp add: list_all2_conv_all_nth nth_list_update)
  1.1017 +  by (cases "i < length ys") (auto simp add: list_all2_conv_all_nth nth_list_update)
  1.1018  
  1.1019  lemma list_all2_takeI [simp,intro?]:
  1.1020    "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
  1.1021 @@ -2787,46 +2786,46 @@
  1.1022  
  1.1023  lemma list_all2_eq:
  1.1024    "xs = ys \<longleftrightarrow> list_all2 (=) xs ys"
  1.1025 -by (induct xs ys rule: list_induct2') auto
  1.1026 +  by (induct xs ys rule: list_induct2') auto
  1.1027  
  1.1028  lemma list_eq_iff_zip_eq:
  1.1029    "xs = ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x,y) \<in> set (zip xs ys). x = y)"
  1.1030 -by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
  1.1031 +  by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
  1.1032  
  1.1033  lemma list_all2_same: "list_all2 P xs xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x x)"
  1.1034 -by(auto simp add: list_all2_conv_all_nth set_conv_nth)
  1.1035 +  by(auto simp add: list_all2_conv_all_nth set_conv_nth)
  1.1036  
  1.1037  lemma zip_assoc:
  1.1038    "zip xs (zip ys zs) = map (\<lambda>((x, y), z). (x, y, z)) (zip (zip xs ys) zs)"
  1.1039 -by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
  1.1040 +  by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
  1.1041  
  1.1042  lemma zip_commute: "zip xs ys = map (\<lambda>(x, y). (y, x)) (zip ys xs)"
  1.1043 -by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
  1.1044 +  by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
  1.1045  
  1.1046  lemma zip_left_commute:
  1.1047    "zip xs (zip ys zs) = map (\<lambda>(y, (x, z)). (x, y, z)) (zip ys (zip xs zs))"
  1.1048 -by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
  1.1049 +  by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
  1.1050  
  1.1051  lemma zip_replicate2: "zip xs (replicate n y) = map (\<lambda>x. (x, y)) (take n xs)"
  1.1052 -by(subst zip_commute)(simp add: zip_replicate1)
  1.1053 +  by(subst zip_commute)(simp add: zip_replicate1)
  1.1054  
  1.1055  subsubsection \<open>@{const List.product} and @{const product_lists}\<close>
  1.1056  
  1.1057  lemma product_concat_map:
  1.1058    "List.product xs ys = concat (map (\<lambda>x. map (\<lambda>y. (x,y)) ys) xs)"
  1.1059 -by(induction xs) (simp)+
  1.1060 +  by(induction xs) (simp)+
  1.1061  
  1.1062  lemma set_product[simp]: "set (List.product xs ys) = set xs \<times> set ys"
  1.1063 -by (induct xs) auto
  1.1064 +  by (induct xs) auto
  1.1065  
  1.1066  lemma length_product [simp]:
  1.1067    "length (List.product xs ys) = length xs * length ys"
  1.1068 -by (induct xs) simp_all
  1.1069 +  by (induct xs) simp_all
  1.1070  
  1.1071  lemma product_nth:
  1.1072    assumes "n < length xs * length ys"
  1.1073    shows "List.product xs ys ! n = (xs ! (n div length ys), ys ! (n mod length ys))"
  1.1074 -using assms proof (induct xs arbitrary: n)
  1.1075 +  using assms proof (induct xs arbitrary: n)
  1.1076    case Nil then show ?case by simp
  1.1077  next
  1.1078    case (Cons x xs n)
  1.1079 @@ -2837,7 +2836,7 @@
  1.1080  
  1.1081  lemma in_set_product_lists_length:
  1.1082    "xs \<in> set (product_lists xss) \<Longrightarrow> length xs = length xss"
  1.1083 -by (induct xss arbitrary: xs) auto
  1.1084 +  by (induct xss arbitrary: xs) auto
  1.1085  
  1.1086  lemma product_lists_set:
  1.1087    "set (product_lists xss) = {xs. list_all2 (\<lambda>x ys. x \<in> set ys) xs xss}" (is "?L = Collect ?R")
  1.1088 @@ -2856,25 +2855,25 @@
  1.1089  lemma fold_simps [code]: \<comment> \<open>eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala\<close>
  1.1090    "fold f [] s = s"
  1.1091    "fold f (x # xs) s = fold f xs (f x s)"
  1.1092 -by simp_all
  1.1093 +  by simp_all
  1.1094  
  1.1095  lemma fold_remove1_split:
  1.1096    "\<lbrakk> \<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x;
  1.1097      x \<in> set xs \<rbrakk>
  1.1098    \<Longrightarrow> fold f xs = fold f (remove1 x xs) \<circ> f x"
  1.1099 -by (induct xs) (auto simp add: comp_assoc)
  1.1100 +  by (induct xs) (auto simp add: comp_assoc)
  1.1101  
  1.1102  lemma fold_cong [fundef_cong]:
  1.1103    "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
  1.1104      \<Longrightarrow> fold f xs a = fold g ys b"
  1.1105 -by (induct ys arbitrary: a b xs) simp_all
  1.1106 +  by (induct ys arbitrary: a b xs) simp_all
  1.1107  
  1.1108  lemma fold_id: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = id) \<Longrightarrow> fold f xs = id"
  1.1109 -by (induct xs) simp_all
  1.1110 +  by (induct xs) simp_all
  1.1111  
  1.1112  lemma fold_commute:
  1.1113    "(\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h) \<Longrightarrow> h \<circ> fold g xs = fold f xs \<circ> h"
  1.1114 -by (induct xs) (simp_all add: fun_eq_iff)
  1.1115 +  by (induct xs) (simp_all add: fun_eq_iff)
  1.1116  
  1.1117  lemma fold_commute_apply:
  1.1118    assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
  1.1119 @@ -2887,41 +2886,41 @@
  1.1120  lemma fold_invariant:
  1.1121    "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> Q x;  P s;  \<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s) \<rbrakk>
  1.1122    \<Longrightarrow> P (fold f xs s)"
  1.1123 -by (induct xs arbitrary: s) simp_all
  1.1124 +  by (induct xs arbitrary: s) simp_all
  1.1125  
  1.1126  lemma fold_append [simp]: "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
  1.1127 -by (induct xs) simp_all
  1.1128 +  by (induct xs) simp_all
  1.1129  
  1.1130  lemma fold_map [code_unfold]: "fold g (map f xs) = fold (g \<circ> f) xs"
  1.1131 -by (induct xs) simp_all
  1.1132 +  by (induct xs) simp_all
  1.1133  
  1.1134  lemma fold_filter:
  1.1135    "fold f (filter P xs) = fold (\<lambda>x. if P x then f x else id) xs"
  1.1136 -by (induct xs) simp_all
  1.1137 +  by (induct xs) simp_all
  1.1138  
  1.1139  lemma fold_rev:
  1.1140    "(\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y)
  1.1141    \<Longrightarrow> fold f (rev xs) = fold f xs"
  1.1142 -by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff)
  1.1143 +  by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff)
  1.1144  
  1.1145  lemma fold_Cons_rev: "fold Cons xs = append (rev xs)"
  1.1146 -by (induct xs) simp_all
  1.1147 +  by (induct xs) simp_all
  1.1148  
  1.1149  lemma rev_conv_fold [code]: "rev xs = fold Cons xs []"
  1.1150 -by (simp add: fold_Cons_rev)
  1.1151 +  by (simp add: fold_Cons_rev)
  1.1152  
  1.1153  lemma fold_append_concat_rev: "fold append xss = append (concat (rev xss))"
  1.1154 -by (induct xss) simp_all
  1.1155 +  by (induct xss) simp_all
  1.1156  
  1.1157  text \<open>@{const Finite_Set.fold} and @{const fold}\<close>
  1.1158  
  1.1159  lemma (in comp_fun_commute) fold_set_fold_remdups:
  1.1160    "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
  1.1161 -by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm insert_absorb)
  1.1162 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm insert_absorb)
  1.1163  
  1.1164  lemma (in comp_fun_idem) fold_set_fold:
  1.1165    "Finite_Set.fold f y (set xs) = fold f xs y"
  1.1166 -by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm)
  1.1167 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm)
  1.1168  
  1.1169  lemma union_set_fold [code]: "set xs \<union> A = fold Set.insert xs A"
  1.1170  proof -
  1.1171 @@ -2932,7 +2931,7 @@
  1.1172  
  1.1173  lemma union_coset_filter [code]:
  1.1174    "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)"
  1.1175 -by auto
  1.1176 +  by auto
  1.1177  
  1.1178  lemma minus_set_fold [code]: "A - set xs = fold Set.remove xs A"
  1.1179  proof -
  1.1180 @@ -2944,15 +2943,15 @@
  1.1181  
  1.1182  lemma minus_coset_filter [code]:
  1.1183    "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
  1.1184 -by auto
  1.1185 +  by auto
  1.1186  
  1.1187  lemma inter_set_filter [code]:
  1.1188    "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
  1.1189 -by auto
  1.1190 +  by auto
  1.1191  
  1.1192  lemma inter_coset_fold [code]:
  1.1193    "A \<inter> List.coset xs = fold Set.remove xs A"
  1.1194 -by (simp add: Diff_eq [symmetric] minus_set_fold)
  1.1195 +  by (simp add: Diff_eq [symmetric] minus_set_fold)
  1.1196  
  1.1197  lemma (in semilattice_set) set_eq_fold [code]:
  1.1198    "F (set (x # xs)) = fold f xs x"
  1.1199 @@ -3000,70 +2999,70 @@
  1.1200  text \<open>Correspondence\<close>
  1.1201  
  1.1202  lemma foldr_conv_fold [code_abbrev]: "foldr f xs = fold f (rev xs)"
  1.1203 -by (induct xs) simp_all
  1.1204 +  by (induct xs) simp_all
  1.1205  
  1.1206  lemma foldl_conv_fold: "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
  1.1207 -by (induct xs arbitrary: s) simp_all
  1.1208 +  by (induct xs arbitrary: s) simp_all
  1.1209  
  1.1210  lemma foldr_conv_foldl: \<comment> \<open>The ``Third Duality Theorem'' in Bird \& Wadler:\<close>
  1.1211    "foldr f xs a = foldl (\<lambda>x y. f y x) a (rev xs)"
  1.1212 -by (simp add: foldr_conv_fold foldl_conv_fold)
  1.1213 +  by (simp add: foldr_conv_fold foldl_conv_fold)
  1.1214  
  1.1215  lemma foldl_conv_foldr:
  1.1216    "foldl f a xs = foldr (\<lambda>x y. f y x) (rev xs) a"
  1.1217 -by (simp add: foldr_conv_fold foldl_conv_fold)
  1.1218 +  by (simp add: foldr_conv_fold foldl_conv_fold)
  1.1219  
  1.1220  lemma foldr_fold:
  1.1221    "(\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y)
  1.1222    \<Longrightarrow> foldr f xs = fold f xs"
  1.1223 -unfolding foldr_conv_fold by (rule fold_rev)
  1.1224 +  unfolding foldr_conv_fold by (rule fold_rev)
  1.1225  
  1.1226  lemma foldr_cong [fundef_cong]:
  1.1227    "a = b \<Longrightarrow> l = k \<Longrightarrow> (\<And>a x. x \<in> set l \<Longrightarrow> f x a = g x a) \<Longrightarrow> foldr f l a = foldr g k b"
  1.1228 -by (auto simp add: foldr_conv_fold intro!: fold_cong)
  1.1229 +  by (auto simp add: foldr_conv_fold intro!: fold_cong)
  1.1230  
  1.1231  lemma foldl_cong [fundef_cong]:
  1.1232    "a = b \<Longrightarrow> l = k \<Longrightarrow> (\<And>a x. x \<in> set l \<Longrightarrow> f a x = g a x) \<Longrightarrow> foldl f a l = foldl g b k"
  1.1233 -by (auto simp add: foldl_conv_fold intro!: fold_cong)
  1.1234 +  by (auto simp add: foldl_conv_fold intro!: fold_cong)
  1.1235  
  1.1236  lemma foldr_append [simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
  1.1237 -by (simp add: foldr_conv_fold)
  1.1238 +  by (simp add: foldr_conv_fold)
  1.1239  
  1.1240  lemma foldl_append [simp]: "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
  1.1241 -by (simp add: foldl_conv_fold)
  1.1242 +  by (simp add: foldl_conv_fold)
  1.1243  
  1.1244  lemma foldr_map [code_unfold]: "foldr g (map f xs) a = foldr (g \<circ> f) xs a"
  1.1245 -by (simp add: foldr_conv_fold fold_map rev_map)
  1.1246 +  by (simp add: foldr_conv_fold fold_map rev_map)
  1.1247  
  1.1248  lemma foldr_filter:
  1.1249    "foldr f (filter P xs) = foldr (\<lambda>x. if P x then f x else id) xs"
  1.1250 -by (simp add: foldr_conv_fold rev_filter fold_filter)
  1.1251 +  by (simp add: foldr_conv_fold rev_filter fold_filter)
  1.1252  
  1.1253  lemma foldl_map [code_unfold]:
  1.1254    "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs"
  1.1255 -by (simp add: foldl_conv_fold fold_map comp_def)
  1.1256 +  by (simp add: foldl_conv_fold fold_map comp_def)
  1.1257  
  1.1258  lemma concat_conv_foldr [code]:
  1.1259    "concat xss = foldr append xss []"
  1.1260 -by (simp add: fold_append_concat_rev foldr_conv_fold)
  1.1261 +  by (simp add: fold_append_concat_rev foldr_conv_fold)
  1.1262  
  1.1263  
  1.1264  subsubsection \<open>@{const upt}\<close>
  1.1265  
  1.1266  lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
  1.1267 -\<comment> \<open>simp does not terminate!\<close>
  1.1268 -by (induct j) auto
  1.1269 +  \<comment> \<open>simp does not terminate!\<close>
  1.1270 +  by (induct j) auto
  1.1271  
  1.1272  lemmas upt_rec_numeral[simp] = upt_rec[of "numeral m" "numeral n"] for m n
  1.1273  
  1.1274  lemma upt_conv_Nil [simp]: "j \<le> i ==> [i..<j] = []"
  1.1275 -by (subst upt_rec) simp
  1.1276 +  by (subst upt_rec) simp
  1.1277  
  1.1278  lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j \<le> i)"
  1.1279 -by(induct j)simp_all
  1.1280 +  by(induct j)simp_all
  1.1281  
  1.1282  lemma upt_eq_Cons_conv:
  1.1283 - "([i..<j] = x#xs) = (i < j \<and> i = x \<and> [i+1..<j] = xs)"
  1.1284 +  "([i..<j] = x#xs) = (i < j \<and> i = x \<and> [i+1..<j] = xs)"
  1.1285  proof (induct j arbitrary: x xs)
  1.1286    case (Suc j)
  1.1287    then show ?case
  1.1288 @@ -3071,11 +3070,11 @@
  1.1289  qed simp
  1.1290  
  1.1291  lemma upt_Suc_append: "i \<le> j ==> [i..<(Suc j)] = [i..<j]@[j]"
  1.1292 -\<comment> \<open>Only needed if \<open>upt_Suc\<close> is deleted from the simpset.\<close>
  1.1293 -by simp
  1.1294 +  \<comment> \<open>Only needed if \<open>upt_Suc\<close> is deleted from the simpset.\<close>
  1.1295 +  by simp
  1.1296  
  1.1297  lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
  1.1298 -by (simp add: upt_rec)
  1.1299 +  by (simp add: upt_rec)
  1.1300  
  1.1301  lemma upt_conv_Cons_Cons: \<comment> \<open>no precondition\<close>
  1.1302    "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
  1.1303 @@ -3086,23 +3085,23 @@
  1.1304  qed
  1.1305  
  1.1306  lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
  1.1307 -\<comment> \<open>LOOPS as a simprule, since \<open>j \<le> j\<close>.\<close>
  1.1308 -by (induct k) auto
  1.1309 +  \<comment> \<open>LOOPS as a simprule, since \<open>j \<le> j\<close>.\<close>
  1.1310 +  by (induct k) auto
  1.1311  
  1.1312  lemma length_upt [simp]: "length [i..<j] = j - i"
  1.1313 -by (induct j) (auto simp add: Suc_diff_le)
  1.1314 +  by (induct j) (auto simp add: Suc_diff_le)
  1.1315  
  1.1316  lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
  1.1317 -by (induct j) (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
  1.1318 +  by (induct j) (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
  1.1319  
  1.1320  lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
  1.1321 -by(simp add:upt_conv_Cons)
  1.1322 +  by(simp add:upt_conv_Cons)
  1.1323  
  1.1324  lemma tl_upt: "tl [m..<n] = [Suc m..<n]"
  1.1325 -by (simp add: upt_rec)
  1.1326 +  by (simp add: upt_rec)
  1.1327  
  1.1328  lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
  1.1329 -by(cases j)(auto simp: upt_Suc_append)
  1.1330 +  by(cases j)(auto simp: upt_Suc_append)
  1.1331  
  1.1332  lemma take_upt [simp]: "i+m \<le> n ==> take m [i..<n] = [i..<i+m]"
  1.1333  proof (induct m arbitrary: i)
  1.1334 @@ -3112,26 +3111,26 @@
  1.1335  qed simp
  1.1336  
  1.1337  lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
  1.1338 -by(induct j) auto
  1.1339 +  by(induct j) auto
  1.1340  
  1.1341  lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
  1.1342 -by (induct n) auto
  1.1343 +  by (induct n) auto
  1.1344  
  1.1345  lemma map_add_upt: "map (\<lambda>i. i + n) [0..<m] = [n..<m + n]"
  1.1346 -by (induct m) simp_all
  1.1347 +  by (induct m) simp_all
  1.1348  
  1.1349  lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
  1.1350  proof (induct n m  arbitrary: i rule: diff_induct)
  1.1351 -case (3 x y)
  1.1352 +  case (3 x y)
  1.1353    then show ?case
  1.1354      by (metis add.commute length_upt less_diff_conv nth_map nth_upt)
  1.1355  qed auto
  1.1356  
  1.1357  lemma map_decr_upt: "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
  1.1358 -by (induct n) simp_all
  1.1359 +  by (induct n) simp_all
  1.1360  
  1.1361  lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda>i. f (Suc i)) [0 ..< n]"
  1.1362 -by (induct n arbitrary: f) auto
  1.1363 +  by (induct n arbitrary: f) auto
  1.1364  
  1.1365  lemma nth_take_lemma:
  1.1366    "k \<le> length xs \<Longrightarrow> k \<le> length ys \<Longrightarrow>
  1.1367 @@ -3145,24 +3144,20 @@
  1.1368  
  1.1369  lemma nth_equalityI:
  1.1370    "[| length xs = length ys; \<forall>i < length xs. xs!i = ys!i |] ==> xs = ys"
  1.1371 -by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
  1.1372 +  by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
  1.1373  
  1.1374  lemma map_nth:
  1.1375    "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
  1.1376 -by (rule nth_equalityI, auto)
  1.1377 +  by (rule nth_equalityI, auto)
  1.1378  
  1.1379  lemma list_all2_antisym:
  1.1380    "\<lbrakk> (\<And>x y. \<lbrakk>P x y; Q y x\<rbrakk> \<Longrightarrow> x = y); list_all2 P xs ys; list_all2 Q ys xs \<rbrakk>
  1.1381    \<Longrightarrow> xs = ys"
  1.1382 -apply (simp add: list_all2_conv_all_nth)
  1.1383 -apply (rule nth_equalityI, blast, simp)
  1.1384 -done
  1.1385 +  by (simp add: list_all2_conv_all_nth nth_equalityI)
  1.1386  
  1.1387  lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
  1.1388  \<comment> \<open>The famous take-lemma.\<close>
  1.1389 -apply (drule_tac x = "max (length xs) (length ys)" in spec)
  1.1390 -apply (simp add: le_max_iff_disj)
  1.1391 -done
  1.1392 +  by (metis length_take min.commute order_refl take_all)
  1.1393  
  1.1394  lemma take_Cons':
  1.1395    "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
  1.1396 @@ -3239,7 +3234,7 @@
  1.1397  qed
  1.1398  
  1.1399  lemma nth_upto: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k"
  1.1400 -apply(induction i j arbitrary: k rule: upto.induct)
  1.1401 +  apply(induction i j arbitrary: k rule: upto.induct)
  1.1402  apply(subst upto_rec1)
  1.1403  apply(auto simp add: nth_Cons')
  1.1404  done
  1.1405 @@ -3310,12 +3305,11 @@
  1.1406  
  1.1407  lemma length_remdups_eq[iff]:
  1.1408    "(length (remdups xs) = length xs) = (remdups xs = xs)"
  1.1409 -apply(induct xs)
  1.1410 - apply auto
  1.1411 -apply(subgoal_tac "length (remdups xs) \<le> length xs")
  1.1412 - apply arith
  1.1413 -apply(rule length_remdups_leq)
  1.1414 -done
  1.1415 +proof (induct xs)
  1.1416 +  case (Cons a xs)
  1.1417 +  then show ?case
  1.1418 +    by simp (metis Suc_n_not_le_n impossible_Cons length_remdups_leq)
  1.1419 +qed auto
  1.1420  
  1.1421  lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)"
  1.1422  by (induct xs) auto
  1.1423 @@ -3341,31 +3335,38 @@
  1.1424  done
  1.1425  
  1.1426  lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
  1.1427 -apply(induct xs arbitrary: i)
  1.1428 - apply simp
  1.1429 -apply (case_tac i)
  1.1430 - apply simp_all
  1.1431 -apply(blast dest:in_set_takeD)
  1.1432 -done
  1.1433 +proof (induct xs arbitrary: i)
  1.1434 +  case (Cons a xs)
  1.1435 +  then show ?case
  1.1436 +    by (metis Cons.prems append_take_drop_id distinct_append)
  1.1437 +qed auto
  1.1438  
  1.1439  lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
  1.1440 -apply(induct xs arbitrary: i)
  1.1441 - apply simp
  1.1442 -apply (case_tac i)
  1.1443 - apply simp_all
  1.1444 -done
  1.1445 +proof (induct xs arbitrary: i)
  1.1446 +  case (Cons a xs)
  1.1447 +  then show ?case
  1.1448 +    by (metis Cons.prems append_take_drop_id distinct_append)
  1.1449 +qed auto
  1.1450  
  1.1451  lemma distinct_list_update:
  1.1452 -assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
  1.1453 -shows "distinct (xs[i:=a])"
  1.1454 +  assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
  1.1455 +  shows "distinct (xs[i:=a])"
  1.1456  proof (cases "i < length xs")
  1.1457    case True
  1.1458 -  with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
  1.1459 -    apply (drule_tac id_take_nth_drop) by simp
  1.1460 -  with d True show ?thesis
  1.1461 -    apply (simp add: upd_conv_take_nth_drop)
  1.1462 -    apply (drule subst [OF id_take_nth_drop]) apply assumption
  1.1463 -    apply simp apply (cases "a = xs!i") apply simp by blast
  1.1464 +  with a have anot: "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
  1.1465 +    by simp (metis in_set_dropD in_set_takeD)
  1.1466 +  show ?thesis
  1.1467 +  proof (cases "a = xs!i")
  1.1468 +    case True
  1.1469 +    with d show ?thesis
  1.1470 +      by auto
  1.1471 +  next
  1.1472 +    case False
  1.1473 +    then show ?thesis
  1.1474 +      using d anot \<open>i < length xs\<close> 
  1.1475 +      apply (simp add: upd_conv_take_nth_drop)
  1.1476 +      by (metis disjoint_insert(1) distinct_append id_take_nth_drop set_simps(2))
  1.1477 +  qed
  1.1478  next
  1.1479    case False with d show ?thesis by auto
  1.1480  qed
  1.1481 @@ -3380,22 +3381,14 @@
  1.1482  text \<open>It is best to avoid this indexed version of distinct, but
  1.1483  sometimes it is useful.\<close>
  1.1484  
  1.1485 -lemma distinct_conv_nth:
  1.1486 -"distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j \<longrightarrow> xs!i \<noteq> xs!j)"
  1.1487 -apply (induct xs, simp, simp)
  1.1488 -apply (rule iffI, clarsimp)
  1.1489 - apply (case_tac i)
  1.1490 -apply (case_tac j, simp)
  1.1491 -apply (simp add: set_conv_nth)
  1.1492 - apply (case_tac j)
  1.1493 -apply (clarsimp simp add: set_conv_nth, simp)
  1.1494 -apply (rule conjI)
  1.1495 - apply (clarsimp simp add: set_conv_nth)
  1.1496 - apply (erule_tac x = 0 in allE, simp)
  1.1497 - apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
  1.1498 -apply (erule_tac x = "Suc i" in allE, simp)
  1.1499 -apply (erule_tac x = "Suc j" in allE, simp)
  1.1500 -done
  1.1501 +lemma distinct_conv_nth: "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j \<longrightarrow> xs!i \<noteq> xs!j)"
  1.1502 +proof (induct xs)
  1.1503 +  case (Cons x xs)
  1.1504 +  show ?case
  1.1505 +    apply (auto simp add: Cons nth_Cons split: nat.split_asm)
  1.1506 +    apply (metis Suc_less_eq2 in_set_conv_nth less_not_refl zero_less_Suc)+
  1.1507 +    done
  1.1508 +qed auto
  1.1509  
  1.1510  lemma nth_eq_iff_index_eq:
  1.1511    "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
  1.1512 @@ -3420,7 +3413,7 @@
  1.1513  
  1.1514  lemma distinct_swap[simp]: "\<lbrakk> i < size xs; j < size xs \<rbrakk> \<Longrightarrow>
  1.1515    distinct(xs[i := xs!j, j := xs!i]) = distinct xs"
  1.1516 -apply (simp add: distinct_conv_nth nth_list_update)
  1.1517 +  apply (simp add: distinct_conv_nth nth_list_update)
  1.1518  apply safe
  1.1519  apply metis+
  1.1520  done
  1.1521 @@ -3434,8 +3427,6 @@
  1.1522  
  1.1523  lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
  1.1524  proof (induct xs)
  1.1525 -  case Nil thus ?case by simp
  1.1526 -next
  1.1527    case (Cons x xs)
  1.1528    show ?case
  1.1529    proof (cases "x \<in> set xs")
  1.1530 @@ -3448,17 +3439,20 @@
  1.1531      ultimately have False by simp
  1.1532      thus ?thesis ..
  1.1533    qed
  1.1534 -qed
  1.1535 +qed simp
  1.1536  
  1.1537  lemma distinct_length_filter: "distinct xs \<Longrightarrow> length (filter P xs) = card ({x. P x} Int set xs)"
  1.1538  by (induct xs) (auto)
  1.1539  
  1.1540  lemma not_distinct_decomp: "\<not> distinct ws \<Longrightarrow> \<exists>xs ys zs y. ws = xs@[y]@ys@[y]@zs"
  1.1541 -apply (induct n == "length ws" arbitrary:ws) apply simp
  1.1542 -apply(case_tac ws) apply simp
  1.1543 -apply (simp split:if_split_asm)
  1.1544 -apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
  1.1545 -done
  1.1546 +proof (induct n == "length ws" arbitrary:ws)
  1.1547 +  case (Suc n ws)
  1.1548 +  then show ?case
  1.1549 +    using length_Suc_conv [of ws n]
  1.1550 +    apply (auto simp: eq_commute)
  1.1551 +     apply (metis append_Nil in_set_conv_decomp_first)
  1.1552 +    by (metis append_Cons)
  1.1553 +qed simp
  1.1554  
  1.1555  lemma not_distinct_conv_prefix:
  1.1556    defines "dec as xs y ys \<equiv> y \<in> set xs \<and> distinct xs \<and> as = xs @ y # ys"
  1.1557 @@ -3690,7 +3684,6 @@
  1.1558          then have "Suc 0 \<notin> f ` {0 ..< length (x1 # x2 # xs)}" by auto
  1.1559          then show False using f_img \<open>2 \<le> length ys\<close> by auto
  1.1560        qed
  1.1561 -
  1.1562        obtain ys' where "ys = x1 # x2 # ys'"
  1.1563          using \<open>2 \<le> length ys\<close> f_nth[of 0] f_nth[of 1]
  1.1564          apply (cases ys)
  1.1565 @@ -3715,10 +3708,7 @@
  1.1566            using Suc0_le_f_Suc f_mono by (auto simp: f'_def mono_iff_le_Suc le_diff_iff)
  1.1567        next
  1.1568          have "f' ` {0 ..< length (x2 # xs)} = (\<lambda>x. f x - 1) ` {0 ..< length (x1 # x2 #xs)}"
  1.1569 -          apply safe
  1.1570 -          apply (rename_tac [!] n,  case_tac [!] n)
  1.1571 -          apply (auto simp: f'_def \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close> intro: rev_image_eqI)
  1.1572 -          done
  1.1573 +          by (auto simp: f'_def \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close> image_def Bex_def less_Suc_eq_0_disj)
  1.1574          also have "\<dots> = (\<lambda>x. x - 1) ` f ` {0 ..< length (x1 # x2 #xs)}"
  1.1575            by (auto simp: image_comp)
  1.1576          also have "\<dots> = (\<lambda>x. x - 1) ` {0 ..< length ys}"
  1.1577 @@ -3885,10 +3875,12 @@
  1.1578  
  1.1579  lemma sum_count_set:
  1.1580    "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> sum (count_list xs) X = length xs"
  1.1581 -apply(induction xs arbitrary: X)
  1.1582 - apply simp
  1.1583 -apply (simp add: sum.If_cases)
  1.1584 -by (metis Diff_eq sum.remove)
  1.1585 +proof (induction xs arbitrary: X)
  1.1586 +  case (Cons x xs)
  1.1587 +  then show ?case
  1.1588 +    apply (auto simp: sum.If_cases sum.remove)
  1.1589 +    by (metis (no_types) Cons.IH Cons.prems(2) diff_eq sum.remove)
  1.1590 +qed simp
  1.1591  
  1.1592  
  1.1593  subsubsection \<open>@{const List.extract}\<close>
  1.1594 @@ -3931,23 +3923,13 @@
  1.1595  
  1.1596  lemma in_set_remove1[simp]:
  1.1597    "a \<noteq> b \<Longrightarrow> a \<in> set(remove1 b xs) = (a \<in> set xs)"
  1.1598 -apply (induct xs)
  1.1599 - apply auto
  1.1600 -done
  1.1601 +  by (induct xs) auto
  1.1602  
  1.1603  lemma set_remove1_subset: "set(remove1 x xs) \<subseteq> set xs"
  1.1604 -apply(induct xs)
  1.1605 - apply simp
  1.1606 -apply simp
  1.1607 -apply blast
  1.1608 -done
  1.1609 +  by (induct xs) auto
  1.1610  
  1.1611  lemma set_remove1_eq [simp]: "distinct xs \<Longrightarrow> set(remove1 x xs) = set xs - {x}"
  1.1612 -apply(induct xs)
  1.1613 - apply simp
  1.1614 -apply simp
  1.1615 -apply blast
  1.1616 -done
  1.1617 +  by (induct xs) auto
  1.1618  
  1.1619  lemma length_remove1:
  1.1620    "length(remove1 x xs) = (if x \<in> set xs then length xs - 1 else length xs)"
  1.1621 @@ -4067,9 +4049,7 @@
  1.1622  text\<open>Courtesy of Matthias Daum:\<close>
  1.1623  lemma append_replicate_commute:
  1.1624    "replicate n x @ replicate k x = replicate k x @ replicate n x"
  1.1625 -apply (simp add: replicate_add [symmetric])
  1.1626 -apply (simp add: add.commute)
  1.1627 -done
  1.1628 +  by (metis add.commute replicate_add)
  1.1629  
  1.1630  text\<open>Courtesy of Andreas Lochbihler:\<close>
  1.1631  lemma filter_replicate:
  1.1632 @@ -4090,23 +4070,24 @@
  1.1633  
  1.1634  text\<open>Courtesy of Matthias Daum (2 lemmas):\<close>
  1.1635  lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
  1.1636 -apply (case_tac "k \<le> i")
  1.1637 - apply  (simp add: min_def)
  1.1638 -apply (drule not_le_imp_less)
  1.1639 -apply (simp add: min_def)
  1.1640 -apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
  1.1641 - apply  simp
  1.1642 -apply (simp add: replicate_add [symmetric])
  1.1643 -done
  1.1644 +proof (cases "k \<le> i")
  1.1645 +  case True
  1.1646 +  then show ?thesis
  1.1647 +    by (simp add: min_def)
  1.1648 +next
  1.1649 +  case False
  1.1650 +  then have "replicate k x = replicate i x @ replicate (k - i) x"
  1.1651 +    by (simp add: replicate_add [symmetric])
  1.1652 +  then show ?thesis
  1.1653 +    by (simp add: min_def)
  1.1654 +qed
  1.1655  
  1.1656  lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
  1.1657 -apply (induct k arbitrary: i)
  1.1658 - apply simp
  1.1659 -apply clarsimp
  1.1660 -apply (case_tac i)
  1.1661 - apply simp
  1.1662 -apply clarsimp
  1.1663 -done
  1.1664 +proof (induct k arbitrary: i)
  1.1665 +  case (Suc k)
  1.1666 +  then show ?case
  1.1667 +    by (simp add: drop_Cons')
  1.1668 +qed simp
  1.1669  
  1.1670  lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
  1.1671  by (induct n) auto
  1.1672 @@ -4148,11 +4129,11 @@
  1.1673  
  1.1674  lemma replicate_eq_replicate[simp]:
  1.1675    "(replicate m x = replicate n y) \<longleftrightarrow> (m=n \<and> (m\<noteq>0 \<longrightarrow> x=y))"
  1.1676 -apply(induct m arbitrary: n)
  1.1677 - apply simp
  1.1678 -apply(induct_tac n)
  1.1679 -apply auto
  1.1680 -done
  1.1681 +proof (induct m arbitrary: n)
  1.1682 +  case (Suc m n)
  1.1683 +  then show ?case
  1.1684 +    by (induct n) auto
  1.1685 +qed simp
  1.1686  
  1.1687  lemma replicate_length_filter:
  1.1688    "replicate (length (filter (\<lambda>y. x = y) xs)) x = filter (\<lambda>y. x = y) xs"
  1.1689 @@ -4239,10 +4220,7 @@
  1.1690  lemma enumerate_simps [simp, code]:
  1.1691    "enumerate n [] = []"
  1.1692    "enumerate n (x # xs) = (n, x) # enumerate (Suc n) xs"
  1.1693 -apply (auto simp add: enumerate_eq_zip not_le)
  1.1694 -apply (cases "n < n + length xs")
  1.1695 - apply (auto simp add: upt_conv_Cons)
  1.1696 -done
  1.1697 +  by (simp_all add: enumerate_eq_zip upt_rec)
  1.1698  
  1.1699  lemma length_enumerate [simp]:
  1.1700    "length (enumerate n xs) = length xs"
  1.1701 @@ -4288,12 +4266,7 @@
  1.1702  
  1.1703  lemma enumerate_append_eq:
  1.1704    "enumerate n (xs @ ys) = enumerate n xs @ enumerate (n + length xs) ys"
  1.1705 -unfolding enumerate_eq_zip
  1.1706 -apply auto
  1.1707 - apply (subst zip_append [symmetric]) apply simp
  1.1708 - apply (subst upt_add_eq_append [symmetric])
  1.1709 - apply (simp_all add: ac_simps)
  1.1710 -done
  1.1711 +  by (simp add: enumerate_eq_zip add.assoc zip_append2)
  1.1712  
  1.1713  lemma enumerate_map_upt:
  1.1714    "enumerate n (map f [n..<m]) = map (\<lambda>k. (k, f k)) [n..<m]"
  1.1715 @@ -4322,27 +4295,33 @@
  1.1716  by(cases xs) simp_all
  1.1717  
  1.1718  lemma rotate_length01[simp]: "length xs \<le> 1 \<Longrightarrow> rotate n xs = xs"
  1.1719 -apply(induct n)
  1.1720 - apply simp
  1.1721 -apply (simp add:rotate_def)
  1.1722 -done
  1.1723 +  by (induct n) (simp_all add:rotate_def)
  1.1724  
  1.1725  lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
  1.1726  by (cases xs) simp_all
  1.1727  
  1.1728  lemma rotate_drop_take:
  1.1729    "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
  1.1730 -apply(induct n)
  1.1731 - apply simp
  1.1732 -apply(simp add:rotate_def)
  1.1733 -apply(cases "xs = []")
  1.1734 - apply (simp)
  1.1735 -apply(case_tac "n mod length xs = 0")
  1.1736 - apply(simp add:mod_Suc)
  1.1737 - apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
  1.1738 -apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
  1.1739 -                take_hd_drop linorder_not_le)
  1.1740 -done
  1.1741 +proof (induct n)
  1.1742 +  case (Suc n)
  1.1743 +  show ?case
  1.1744 +  proof (cases "xs = []")
  1.1745 +    case False
  1.1746 +    then show ?thesis
  1.1747 +    proof (cases "n mod length xs = 0")
  1.1748 +      case True
  1.1749 +      then show ?thesis
  1.1750 +        apply (simp add: mod_Suc)
  1.1751 +        by (simp add: False Suc.hyps drop_Suc rotate1_hd_tl take_Suc)
  1.1752 +    next
  1.1753 +      case False
  1.1754 +      with \<open>xs \<noteq> []\<close> Suc
  1.1755 +      show ?thesis
  1.1756 +        by (simp add: rotate_def mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
  1.1757 +            take_hd_drop linorder_not_le)
  1.1758 +    qed
  1.1759 +  qed simp
  1.1760 +qed simp
  1.1761  
  1.1762  lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
  1.1763  by(simp add:rotate_drop_take)
  1.1764 @@ -4385,11 +4364,14 @@
  1.1765      by(simp add:rotate_drop_take rev_drop rev_take)
  1.1766  qed force
  1.1767  
  1.1768 -lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
  1.1769 -apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
  1.1770 -apply(subgoal_tac "length xs \<noteq> 0")
  1.1771 - prefer 2 apply simp
  1.1772 -using mod_less_divisor[of "length xs" n] by arith
  1.1773 +lemma hd_rotate_conv_nth:
  1.1774 +  assumes "xs \<noteq> []" shows "hd(rotate n xs) = xs!(n mod length xs)"
  1.1775 +proof -
  1.1776 +  have "n mod length xs < length xs"
  1.1777 +    using assms by simp
  1.1778 +  then show ?thesis
  1.1779 +    by (metis drop_eq_Nil hd_append2 hd_drop_conv_nth leD rotate_drop_take)
  1.1780 +qed
  1.1781  
  1.1782  lemma rotate_append: "rotate (length l) (l @ q) = q @ l"
  1.1783    by (induct l arbitrary: q) (auto simp add: rotate1_rotate_swap)
  1.1784 @@ -4408,14 +4390,13 @@
  1.1785  by(simp add: nths_def length_filter_conv_card cong:conj_cong)
  1.1786  
  1.1787  lemma nths_shift_lemma_Suc:
  1.1788 -  "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
  1.1789 -   map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
  1.1790 -apply(induct xs arbitrary: "is")
  1.1791 - apply simp
  1.1792 -apply (case_tac "is")
  1.1793 - apply simp
  1.1794 -apply simp
  1.1795 -done
  1.1796 +  "map fst (filter (\<lambda>p. P(Suc(snd p))) (zip xs is)) =
  1.1797 +   map fst (filter (\<lambda>p. P(snd p)) (zip xs (map Suc is)))"
  1.1798 +proof (induct xs arbitrary: "is")
  1.1799 +  case (Cons x xs "is")
  1.1800 +  show ?case
  1.1801 +    by (cases "is") (auto simp add: Cons.hyps)
  1.1802 +qed simp
  1.1803  
  1.1804  lemma nths_shift_lemma:
  1.1805    "map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [i..<i + length xs])) =
  1.1806 @@ -4424,26 +4405,26 @@
  1.1807  
  1.1808  lemma nths_append:
  1.1809    "nths (l @ l') A = nths l A @ nths l' {j. j + length l \<in> A}"
  1.1810 -apply (unfold nths_def)
  1.1811 -apply (induct l' rule: rev_induct, simp)
  1.1812 -apply (simp add: upt_add_eq_append[of 0] nths_shift_lemma)
  1.1813 -apply (simp add: add.commute)
  1.1814 -done
  1.1815 +  unfolding nths_def
  1.1816 +proof (induct l' rule: rev_induct)
  1.1817 +  case (snoc x xs)
  1.1818 +  then show ?case
  1.1819 +    by (simp add: upt_add_eq_append[of 0] nths_shift_lemma add.commute)
  1.1820 +qed auto
  1.1821  
  1.1822  lemma nths_Cons:
  1.1823    "nths (x # l) A = (if 0 \<in> A then [x] else []) @ nths l {j. Suc j \<in> A}"
  1.1824 -apply (induct l rule: rev_induct)
  1.1825 - apply (simp add: nths_def)
  1.1826 -apply (simp del: append_Cons add: append_Cons[symmetric] nths_append)
  1.1827 -done
  1.1828 +proof (induct l rule: rev_induct)
  1.1829 +  case (snoc x xs)
  1.1830 +  then show ?case
  1.1831 +    by (simp flip: append_Cons add: nths_append)
  1.1832 +qed (auto simp: nths_def)
  1.1833  
  1.1834  lemma nths_map: "nths (map f xs) I = map f (nths xs I)"
  1.1835  by(induction xs arbitrary: I) (simp_all add: nths_Cons)
  1.1836  
  1.1837  lemma set_nths: "set(nths xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
  1.1838 -apply(induct xs arbitrary: I)
  1.1839 -apply(auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
  1.1840 -done
  1.1841 +  by (induct xs arbitrary: I) (auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
  1.1842  
  1.1843  lemma set_nths_subset: "set(nths xs I) \<subseteq> set xs"
  1.1844  by(auto simp add:set_nths)
  1.1845 @@ -4792,8 +4773,7 @@
  1.1846      show ?thesis
  1.1847        unfolding transpose.simps \<open>i = Suc j\<close> nth_Cons_Suc "3.hyps"[OF j_less]
  1.1848        apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric])
  1.1849 -      apply (rule list.exhaust)
  1.1850 -      by auto
  1.1851 +      by (simp add: nth_tl)
  1.1852    qed
  1.1853  qed simp_all
  1.1854  
  1.1855 @@ -4917,11 +4897,7 @@
  1.1856  qed
  1.1857  
  1.1858  lemma infinite_UNIV_listI: "\<not> finite(UNIV::'a list set)"
  1.1859 -apply (rule notI)
  1.1860 -apply (drule finite_maxlen)
  1.1861 -apply clarsimp
  1.1862 -apply (erule_tac x = "replicate n undefined" in allE)
  1.1863 -by simp
  1.1864 +  by (metis UNIV_I finite_maxlen length_replicate less_irrefl)
  1.1865  
  1.1866  
  1.1867  subsection \<open>Sorting\<close>
  1.1868 @@ -4936,10 +4912,11 @@
  1.1869  by(simp)
  1.1870  
  1.1871  lemma sorted_wrt2: "transp P \<Longrightarrow> sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))"
  1.1872 -apply(induction zs arbitrary: x y)
  1.1873 -apply(auto dest: transpD)
  1.1874 -apply (meson transpD)
  1.1875 -done
  1.1876 +proof (induction zs arbitrary: x y)
  1.1877 +  case (Cons z zs)
  1.1878 +  then show ?case
  1.1879 +    by simp (meson transpD)+
  1.1880 +qed auto
  1.1881  
  1.1882  lemmas sorted_wrt2_simps = sorted_wrt1 sorted_wrt2
  1.1883  
  1.1884 @@ -4969,9 +4946,7 @@
  1.1885  
  1.1886  lemma sorted_wrt_iff_nth_less:
  1.1887    "sorted_wrt P xs = (\<forall>i j. i < j \<longrightarrow> j < length xs \<longrightarrow> P (xs ! i) (xs ! j))"
  1.1888 -apply(induction xs)
  1.1889 -apply(auto simp add: in_set_conv_nth Ball_def nth_Cons split: nat.split)
  1.1890 -done
  1.1891 +  by (induction xs) (auto simp add: in_set_conv_nth Ball_def nth_Cons split: nat.split)
  1.1892  
  1.1893  lemma sorted_wrt_nth_less:
  1.1894    "\<lbrakk> sorted_wrt P xs; i < j; j < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) (xs ! j)"
  1.1895 @@ -4981,10 +4956,11 @@
  1.1896  by(induction n) (auto simp: sorted_wrt_append)
  1.1897  
  1.1898  lemma sorted_wrt_upto[simp]: "sorted_wrt (<) [i..j]"
  1.1899 -apply(induction i j rule: upto.induct)
  1.1900 -apply(subst upto.simps)
  1.1901 -apply(simp)
  1.1902 -done
  1.1903 +proof(induct i j rule:upto.induct)
  1.1904 +  case (1 i j)
  1.1905 +  from this show ?case
  1.1906 +    unfolding upto.simps[of i j] by auto
  1.1907 +qed
  1.1908  
  1.1909  text \<open>Each element is greater or equal to its index:\<close>
  1.1910  
  1.1911 @@ -5313,12 +5289,13 @@
  1.1912  qed
  1.1913  
  1.1914  lemma finite_sorted_distinct_unique:
  1.1915 -shows "finite A \<Longrightarrow> \<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
  1.1916 -apply(drule finite_distinct_list)
  1.1917 -apply clarify
  1.1918 -apply(rule_tac a="sort xs" in ex1I)
  1.1919 -apply (auto simp: sorted_distinct_set_unique)
  1.1920 -done
  1.1921 +  assumes "finite A" shows "\<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
  1.1922 +proof -
  1.1923 +  obtain xs where "distinct xs" "A = set xs"
  1.1924 +    using finite_distinct_list [OF assms] by metis
  1.1925 +  then show ?thesis
  1.1926 +    by (rule_tac a="sort xs" in ex1I) (auto simp: sorted_distinct_set_unique)
  1.1927 +qed
  1.1928  
  1.1929  lemma insort_insert_key_triv:
  1.1930    "f x \<in> f ` set xs \<Longrightarrow> insort_insert_key f x xs = xs"
  1.1931 @@ -5741,12 +5718,12 @@
  1.1932    | insert:  "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
  1.1933  
  1.1934  lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
  1.1935 -apply (rule iffI)
  1.1936 - apply (induct set: ListMem)
  1.1937 -  apply auto
  1.1938 -apply (induct xs)
  1.1939 - apply (auto intro: ListMem.intros)
  1.1940 -done
  1.1941 +proof
  1.1942 +  show "ListMem x xs \<Longrightarrow> x \<in> set xs"
  1.1943 +    by (induct set: ListMem) auto
  1.1944 +  show "x \<in> set xs \<Longrightarrow> ListMem x xs"
  1.1945 +    by (induct xs) (auto intro: ListMem.intros)
  1.1946 +qed
  1.1947  
  1.1948  
  1.1949  subsubsection \<open>Lists as Cartesian products\<close>
  1.1950 @@ -5789,20 +5766,23 @@
  1.1951  "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
  1.1952          \<comment> \<open>Compares lists by their length and then lexicographically\<close>
  1.1953  
  1.1954 -lemma wf_lexn: "wf r ==> wf (lexn r n)"
  1.1955 -apply (induct n, simp, simp)
  1.1956 -apply(rule wf_subset)
  1.1957 - prefer 2 apply (rule Int_lower1)
  1.1958 -apply(rule wf_map_prod_image)
  1.1959 - prefer 2 apply (rule inj_onI, auto)
  1.1960 -done
  1.1961 +lemma wf_lexn: assumes "wf r" shows "wf (lexn r n)"
  1.1962 +proof (induct n)
  1.1963 +  case (Suc n)
  1.1964 +  have inj: "inj (\<lambda>(x, xs). x # xs)"
  1.1965 +    using assms by (auto simp: inj_on_def)
  1.1966 +  have wf: "wf (map_prod (\<lambda>(x, xs). x # xs) (\<lambda>(x, xs). x # xs) ` (r <*lex*> lexn r n))"
  1.1967 +    by (simp add: Suc.hyps assms wf_lex_prod wf_map_prod_image [OF _ inj])
  1.1968 +  then show ?case
  1.1969 +    by (rule wf_subset) auto
  1.1970 +qed auto
  1.1971  
  1.1972  lemma lexn_length:
  1.1973    "(xs, ys) \<in> lexn r n \<Longrightarrow> length xs = n \<and> length ys = n"
  1.1974  by (induct n arbitrary: xs ys) auto
  1.1975  
  1.1976  lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
  1.1977 -  apply (unfold lex_def)
  1.1978 +  unfolding lex_def
  1.1979    apply (rule wf_UN)
  1.1980     apply (simp add: wf_lexn)
  1.1981    apply (metis DomainE Int_emptyI RangeE lexn_length)
  1.1982 @@ -5905,14 +5885,12 @@
  1.1983  by (simp add:lex_conv)
  1.1984  
  1.1985  lemma Cons_in_lex [simp]:
  1.1986 -    "((x # xs, y # ys) \<in> lex r) =
  1.1987 +  "((x # xs, y # ys) \<in> lex r) =
  1.1988        ((x, y) \<in> r \<and> length xs = length ys \<or> x = y \<and> (xs, ys) \<in> lex r)"
  1.1989 -apply (simp add: lex_conv)
  1.1990 -apply (rule iffI)
  1.1991 - prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
  1.1992 -apply (case_tac xys, simp, simp)
  1.1993 -apply blast
  1.1994 -  done
  1.1995 +  apply (simp add: lex_conv)
  1.1996 +  apply (rule iffI)
  1.1997 +   prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
  1.1998 +  by (metis hd_append append_Nil list.sel(1) list.sel(3) tl_append2)
  1.1999  
  1.2000  lemma lex_append_rightI:
  1.2001    "(xs, ys) \<in> lex r \<Longrightarrow> length vs = length us \<Longrightarrow> (xs @ us, ys @ vs) \<in> lex r"
  1.2002 @@ -5960,12 +5938,13 @@
  1.2003  by (unfold lexord_def, induct_tac x, auto)
  1.2004  
  1.2005  lemma lexord_cons_cons[simp]:
  1.2006 -     "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r \<or> (a = b \<and> (x,y)\<in> lexord r))"
  1.2007 -  apply (unfold lexord_def, safe, simp_all)
  1.2008 -  apply (case_tac u, simp, simp)
  1.2009 -  apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
  1.2010 -  apply (erule_tac x="b # u" in allE)
  1.2011 -  by force
  1.2012 +  "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r \<or> (a = b \<and> (x,y)\<in> lexord r))"
  1.2013 +  unfolding lexord_def
  1.2014 +  apply (safe, simp_all)
  1.2015 +     apply (metis hd_append list.sel(1))
  1.2016 +    apply (metis hd_append list.sel(1) list.sel(3) tl_append2)
  1.2017 +   apply blast
  1.2018 +  by (meson Cons_eq_appendI)
  1.2019  
  1.2020  lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
  1.2021  
  1.2022 @@ -5989,24 +5968,17 @@
  1.2023       (\<exists>i. i < min(length x)(length y) \<and> take i x = take i y \<and> (x!i,y!i) \<in> r))"
  1.2024    apply (unfold lexord_def Let_def, clarsimp)
  1.2025    apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
  1.2026 +  apply (metis Cons_nth_drop_Suc append_eq_conv_conj drop_all list.simps(3) not_le)
  1.2027    apply auto
  1.2028 -  apply (rule_tac x="hd (drop (length x) y)" in exI)
  1.2029 -  apply (rule_tac x="tl (drop (length x) y)" in exI)
  1.2030 -  apply (erule subst, simp add: min_def)
  1.2031    apply (rule_tac x ="length u" in exI, simp)
  1.2032 -  apply (rule_tac x ="take i x" in exI)
  1.2033 -  apply (rule_tac x ="x ! i" in exI)
  1.2034 -  apply (rule_tac x ="y ! i" in exI, safe)
  1.2035 -  apply (rule_tac x="drop (Suc i) x" in exI)
  1.2036 -  apply (drule sym, simp add: Cons_nth_drop_Suc)
  1.2037 -  apply (rule_tac x="drop (Suc i) y" in exI)
  1.2038 -  by (simp add: Cons_nth_drop_Suc)
  1.2039 +  by (metis id_take_nth_drop)
  1.2040  
  1.2041  \<comment> \<open>lexord is extension of partial ordering List.lex\<close>
  1.2042  lemma lexord_lex: "(x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
  1.2043 -  apply (rule_tac x = y in spec)
  1.2044 -  apply (induct_tac x, clarsimp)
  1.2045 -  by (clarify, case_tac x, simp, force)
  1.2046 +proof (induction x arbitrary: y)
  1.2047 +  case (Cons a x y) then show ?case
  1.2048 +    by (cases y) (force+)
  1.2049 +qed auto
  1.2050  
  1.2051  lemma lexord_irreflexive: "\<forall>x. (x,x) \<notin> r \<Longrightarrow> (xs,xs) \<notin> lexord r"
  1.2052  by (induct xs) auto
  1.2053 @@ -6049,12 +6021,15 @@
  1.2054  lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
  1.2055  by (rule transI, drule lexord_trans, blast)
  1.2056  
  1.2057 -lemma lexord_linear: "(\<forall>a b. (a,b)\<in> r \<or> a = b \<or> (b,a) \<in> r) \<Longrightarrow> (x,y) \<in> lexord r \<or> x = y \<or> (y,x) \<in> lexord r"
  1.2058 -  apply (rule_tac x = y in spec)
  1.2059 -  apply (induct_tac x, rule allI)
  1.2060 -  apply (case_tac x, simp, simp)
  1.2061 -  apply (rule allI, case_tac x, simp, simp)
  1.2062 -  by blast
  1.2063 +lemma lexord_linear: "(\<forall>a b. (a,b) \<in> r \<or> a = b \<or> (b,a) \<in> r) \<Longrightarrow> (x,y) \<in> lexord r \<or> x = y \<or> (y,x) \<in> lexord r"
  1.2064 +proof (induction x arbitrary: y)
  1.2065 +  case Nil
  1.2066 +  then show ?case
  1.2067 +    by (metis lexord_Nil_left list.exhaust)
  1.2068 +next
  1.2069 +  case (Cons a x y) then show ?case
  1.2070 +    by (cases y) (force+)
  1.2071 +qed 
  1.2072  
  1.2073  lemma lexord_irrefl:
  1.2074    "irrefl R \<Longrightarrow> irrefl (lexord R)"
  1.2075 @@ -6220,27 +6195,17 @@
  1.2076  lemma lexordp_eq_trans:
  1.2077    assumes "lexordp_eq xs ys" and "lexordp_eq ys zs"
  1.2078    shows "lexordp_eq xs zs"
  1.2079 -using assms
  1.2080 -apply(induct arbitrary: zs)
  1.2081 -apply(case_tac [2-3] zs)
  1.2082 -apply auto
  1.2083 -done
  1.2084 +  using assms
  1.2085 +  by (induct arbitrary: zs) (case_tac zs; auto)+
  1.2086  
  1.2087  lemma lexordp_trans:
  1.2088    assumes "lexordp xs ys" "lexordp ys zs"
  1.2089    shows "lexordp xs zs"
  1.2090 -using assms
  1.2091 -apply(induct arbitrary: zs)
  1.2092 -apply(case_tac [2-3] zs)
  1.2093 -apply auto
  1.2094 -done
  1.2095 +  using assms
  1.2096 +  by (induct arbitrary: zs) (case_tac zs; auto)+
  1.2097  
  1.2098  lemma lexordp_linear: "lexordp xs ys \<or> xs = ys \<or> lexordp ys xs"
  1.2099 -proof(induct xs arbitrary: ys)
  1.2100 -  case Nil thus ?case by(cases ys) simp_all
  1.2101 -next
  1.2102 -  case Cons thus ?case by(cases ys) auto
  1.2103 -qed
  1.2104 +  by(induct xs arbitrary: ys; case_tac ys; fastforce)
  1.2105  
  1.2106  lemma lexordp_conv_lexordp_eq: "lexordp xs ys \<longleftrightarrow> lexordp_eq xs ys \<and> \<not> lexordp_eq ys xs"
  1.2107    (is "?lhs \<longleftrightarrow> ?rhs")
  1.2108 @@ -6258,13 +6223,11 @@
  1.2109  by(auto simp add: lexordp_conv_lexordp_eq lexordp_eq_refl dest: lexordp_eq_antisym)
  1.2110  
  1.2111  lemma lexordp_eq_linear: "lexordp_eq xs ys \<or> lexordp_eq ys xs"
  1.2112 -apply(induct xs arbitrary: ys)
  1.2113 -apply(case_tac [!] ys)
  1.2114 -apply auto
  1.2115 -done
  1.2116 +  by (induct xs arbitrary: ys) (case_tac ys; auto)+
  1.2117  
  1.2118  lemma lexordp_linorder: "class.linorder lexordp_eq lexordp"
  1.2119 -by unfold_locales(auto simp add: lexordp_conv_lexordp_eq lexordp_eq_refl lexordp_eq_antisym intro: lexordp_eq_trans del: disjCI intro: lexordp_eq_linear)
  1.2120 +  by unfold_locales
  1.2121 +     (auto simp add: lexordp_conv_lexordp_eq lexordp_eq_refl lexordp_eq_antisym intro: lexordp_eq_trans del: disjCI intro: lexordp_eq_linear)
  1.2122  
  1.2123  end
  1.2124  
  1.2125 @@ -6402,17 +6365,20 @@
  1.2126  apply (induct arbitrary: xs set: Wellfounded.acc)
  1.2127  apply (erule thin_rl)
  1.2128  apply (erule acc_induct)
  1.2129 -apply (rule accI)
  1.2130 +  apply (rule accI)
  1.2131  apply (blast)
  1.2132  done
  1.2133  
  1.2134  lemma lists_accD: "xs \<in> lists (Wellfounded.acc r) \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r)"
  1.2135 -apply (induct set: lists)
  1.2136 - apply (rule accI)
  1.2137 - apply simp
  1.2138 -apply (rule accI)
  1.2139 -apply (fast dest: acc_downward)
  1.2140 -done
  1.2141 +proof (induct set: lists)
  1.2142 +  case Nil
  1.2143 +  then show ?case
  1.2144 +    by (meson acc.intros not_listrel1_Nil)
  1.2145 +next
  1.2146 +  case (Cons a l)
  1.2147 +  then show ?case
  1.2148 +    by blast
  1.2149 +qed
  1.2150  
  1.2151  lemma lists_accI: "xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> xs \<in> lists (Wellfounded.acc r)"
  1.2152  apply (induct set: Wellfounded.acc)
  1.2153 @@ -6459,10 +6425,7 @@
  1.2154  
  1.2155  
  1.2156  lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
  1.2157 -apply clarify
  1.2158 -apply (erule listrel.induct)
  1.2159 -apply (blast intro: listrel.intros)+
  1.2160 -done
  1.2161 +  by (meson listrel_iff_nth subrelI subset_eq)
  1.2162  
  1.2163  lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
  1.2164  apply clarify
  1.2165 @@ -6477,10 +6440,7 @@
  1.2166  done
  1.2167  
  1.2168  lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)"
  1.2169 -apply (auto simp add: sym_def)
  1.2170 -apply (erule listrel.induct)
  1.2171 -apply (blast intro: listrel.intros)+
  1.2172 -done
  1.2173 +  by (simp add: listrel_iff_nth sym_def)
  1.2174  
  1.2175  lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)"
  1.2176  apply (simp add: trans_def)
  1.2177 @@ -7365,10 +7325,7 @@
  1.2178    "(rel_set A ===> rel_set (list_all2 A) ===> rel_set (list_all2 A))
  1.2179      set_Cons set_Cons"
  1.2180    unfolding rel_fun_def rel_set_def set_Cons_def
  1.2181 -  apply safe
  1.2182 -  apply (simp add: list_all2_Cons1, fast)
  1.2183 -  apply (simp add: list_all2_Cons2, fast)
  1.2184 -  done
  1.2185 +  by (fastforce simp add: list_all2_Cons1 list_all2_Cons2)
  1.2186  
  1.2187  lemma listset_transfer [transfer_rule]:
  1.2188    "(list_all2 (rel_set A) ===> rel_set (list_all2 A)) listset listset"