# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1533338355 -3600
# Node ID 8aedca31957d5409522186f49e2d7b178ceee520
# Parent  6d9eca4805ff91f6ee3f0e8dbdd1ce10eca83d02
de-applying

diff -r 6d9eca4805ff -r 8aedca31957d src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 01 22:59:42 2018 +0100
+++ b/src/HOL/List.thy	Sat Aug 04 00:19:15 2018 +0100
@@ -1242,7 +1242,7 @@
 
 lemma rev_induct [case_names Nil snoc]:
   "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
-apply(simplesubst rev_rev_ident[symmetric])
+apply(subst rev_rev_ident[symmetric])
 apply(rule_tac list = "rev xs" in list.induct, simp_all)
 done
 
@@ -1489,8 +1489,7 @@
   case Nil thus ?case by simp
 next
   case (Cons x xs) thus ?case
-    apply (auto split:if_split_asm)
-    using length_filter_le[of P xs] by arith
+    using Suc_le_eq by fastforce
 qed
 
 lemma length_filter_conv_card:
@@ -1558,17 +1557,17 @@
 lemma filter_eq_ConsD:
   "filter P ys = x#xs \<Longrightarrow>
   \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
-by(rule Cons_eq_filterD) simp
+  by(rule Cons_eq_filterD) simp
 
 lemma filter_eq_Cons_iff:
   "(filter P ys = x#xs) =
   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
-by(auto dest:filter_eq_ConsD)
+  by(auto dest:filter_eq_ConsD)
 
 lemma Cons_eq_filter_iff:
   "(x#xs = filter P ys) =
   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
-by(auto dest:Cons_eq_filterD)
+  by(auto dest:Cons_eq_filterD)
 
 lemma inj_on_filter_key_eq:
   assumes "inj_on f (insert y (set xs))"
@@ -1583,16 +1582,16 @@
 subsubsection \<open>List partitioning\<close>
 
 primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
-"partition P [] = ([], [])" |
-"partition P (x # xs) =
+  "partition P [] = ([], [])" |
+  "partition P (x # xs) =
   (let (yes, no) = partition P xs
    in if P x then (x # yes, no) else (yes, x # no))"
 
 lemma partition_filter1: "fst (partition P xs) = filter P xs"
-by (induct xs) (auto simp add: Let_def split_def)
+  by (induct xs) (auto simp add: Let_def split_def)
 
 lemma partition_filter2: "snd (partition P xs) = filter (Not \<circ> P) xs"
-by (induct xs) (auto simp add: Let_def split_def)
+  by (induct xs) (auto simp add: Let_def split_def)
 
 lemma partition_P:
   assumes "partition P xs = (yes, no)"
@@ -1614,8 +1613,8 @@
 
 lemma partition_filter_conv[simp]:
   "partition f xs = (filter f xs,filter (Not \<circ> f) xs)"
-unfolding partition_filter2[symmetric]
-unfolding partition_filter1[symmetric] by simp
+  unfolding partition_filter2[symmetric]
+  unfolding partition_filter1[symmetric] by simp
 
 declare partition.simps[simp del]
 
@@ -1623,28 +1622,28 @@
 subsubsection \<open>@{const concat}\<close>
 
 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
-by (induct xss) auto
+  by (induct xss) auto
 
 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
-by (induct xss) auto
+  by (induct xss) auto
 
 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
-by (induct xs) auto
+  by (induct xs) auto
 
 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)"
 proof (induct xs arbitrary: ys)
@@ -1653,21 +1652,21 @@
 qed (auto)
 
 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"
-by (simp add: concat_eq_concat_iff)
+  by (simp add: concat_eq_concat_iff)
 
 
 subsubsection \<open>@{const nth}\<close>
 
 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
-by auto
+  by auto
 
 lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"
-by auto
+  by auto
 
 declare nth.simps [simp del]
 
 lemma nth_Cons_pos[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
-by(auto simp: Nat.gr0_conv_Suc)
+  by(auto simp: Nat.gr0_conv_Suc)
 
 lemma nth_append:
   "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
@@ -1678,10 +1677,10 @@
 qed simp
 
 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
 proof (induct xs arbitrary: n)
@@ -1691,10 +1690,10 @@
 qed simp
 
 lemma nth_tl: "n < length (tl xs) \<Longrightarrow> tl xs ! n = xs ! Suc n"
-by (induction xs) auto
+  by (induction xs) auto
 
 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
-by(cases xs) simp_all
+  by(cases xs) simp_all
 
 
 lemma list_eq_iff_nth_eq:
@@ -1724,7 +1723,7 @@
 qed simp
 
 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
-by(auto simp:set_conv_nth)
+  by(auto simp:set_conv_nth)
 
 lemma nth_equal_first_eq:
   assumes "x \<notin> set xs"
@@ -1756,18 +1755,18 @@
 qed
 
 lemma list_ball_nth: "\<lbrakk>n < length xs; \<forall>x \<in> set xs. P x\<rbrakk> \<Longrightarrow> P(xs!n)"
-by (auto simp add: set_conv_nth)
+  by (auto simp add: set_conv_nth)
 
 lemma nth_mem [simp]: "n < length xs \<Longrightarrow> xs!n \<in> set xs"
-by (auto simp add: set_conv_nth)
+  by (auto simp add: set_conv_nth)
 
 lemma all_nth_imp_all_set:
   "\<lbrakk>\<forall>i < length xs. P(xs!i); x \<in> set xs\<rbrakk> \<Longrightarrow> P x"
-by (auto simp add: set_conv_nth)
+  by (auto simp add: set_conv_nth)
 
 lemma all_set_conv_all_nth:
   "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
-by (auto simp add: set_conv_nth)
+  by (auto simp add: set_conv_nth)
 
 lemma rev_nth:
   "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
@@ -1811,20 +1810,20 @@
 subsubsection \<open>@{const list_update}\<close>
 
 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
-by (induct xs arbitrary: i) (auto split: nat.split)
+  by (induct xs arbitrary: i) (auto split: nat.split)
 
 lemma nth_list_update:
-"i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
-by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
+  "i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
+  by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
 
 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"
-by (simp add: nth_list_update)
+  by (simp add: nth_list_update)
 
 lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
-by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
+  by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
 
 lemma list_update_id[simp]: "xs[i := xs!i] = xs"
-by (induct xs arbitrary: i) (simp_all split:nat.splits)
+  by (induct xs arbitrary: i) (simp_all split:nat.splits)
 
 lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
 proof (induct xs arbitrary: i)
@@ -1834,44 +1833,44 @@
 qed simp
 
 lemma list_update_nonempty[simp]: "xs[k:=x] = [] \<longleftrightarrow> xs=[]"
-by (simp only: length_0_conv[symmetric] length_list_update)
+  by (simp only: length_0_conv[symmetric] length_list_update)
 
 lemma list_update_same_conv:
   "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
-by (induct xs arbitrary: i) (auto split: nat.split)
+  by (induct xs arbitrary: i) (auto split: nat.split)
 
 lemma list_update_append1:
   "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
-by (induct xs arbitrary: i)(auto split:nat.split)
+  by (induct xs arbitrary: i)(auto split:nat.split)
 
 lemma list_update_append:
   "(xs @ ys) [n:= x] =
   (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
-by (induct xs arbitrary: n) (auto split:nat.splits)
+  by (induct xs arbitrary: n) (auto split:nat.splits)
 
 lemma list_update_length [simp]:
   "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
-by (induct xs, auto)
+  by (induct xs, auto)
 
 lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]"
-by(induct xs arbitrary: k)(auto split:nat.splits)
+  by(induct xs arbitrary: k)(auto split:nat.splits)
 
 lemma rev_update:
   "k < length xs \<Longrightarrow> rev (xs[k:= y]) = (rev xs)[length xs - k - 1 := y]"
-by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)
+  by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)
 
 lemma update_zip:
   "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
-by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
+  by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
 
 lemma set_update_subset_insert: "set(xs[i:=x]) \<le> insert x (set xs)"
-by (induct xs arbitrary: i) (auto split: nat.split)
+  by (induct xs arbitrary: i) (auto split: nat.split)
 
 lemma set_update_subsetI: "\<lbrakk>set xs \<subseteq> A; x \<in> A\<rbrakk> \<Longrightarrow> set(xs[i := x]) \<subseteq> A"
-by (blast dest!: set_update_subset_insert [THEN subsetD])
+  by (blast dest!: set_update_subset_insert [THEN subsetD])
 
 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
-by (induct xs arbitrary: n) (auto split:nat.splits)
+  by (induct xs arbitrary: n) (auto split:nat.splits)
 
 lemma list_update_overwrite[simp]:
   "xs [i := x, i := y] = xs [i := y]"
@@ -1885,67 +1884,67 @@
   "[][i := y] = []"
   "(x # xs)[0 := y] = y # xs"
   "(x # xs)[Suc i := y] = x # xs[i := y]"
-by simp_all
+  by simp_all
 
 
 subsubsection \<open>@{const last} and @{const butlast}\<close>
 
 lemma last_snoc [simp]: "last (xs @ [x]) = x"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
-by simp
+  by simp
 
 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
-by simp
+  by simp
 
 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
-by (induct xs) (auto)
+  by (induct xs) (auto)
 
 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
-by(simp add:last_append)
+  by(simp add:last_append)
 
 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
-by(simp add:last_append)
+  by(simp add:last_append)
 
 lemma last_tl: "xs = [] \<or> tl xs \<noteq> [] \<Longrightarrow>last (tl xs) = last xs"
-by (induct xs) simp_all
+  by (induct xs) simp_all
 
 lemma butlast_tl: "butlast (tl xs) = tl (butlast xs)"
-by (induct xs) simp_all
+  by (induct xs) simp_all
 
 lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
-by(rule rev_exhaust[of xs]) simp_all
+  by(rule rev_exhaust[of xs]) simp_all
 
 lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
-by(cases xs) simp_all
+  by(cases xs) simp_all
 
 lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
-by (induct as) auto
+  by (induct as) auto
 
 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
-by (induct xs rule: rev_induct) auto
+  by (induct xs rule: rev_induct) auto
 
 lemma butlast_append:
   "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
-by (induct xs arbitrary: ys) auto
+  by (induct xs arbitrary: ys) auto
 
 lemma append_butlast_last_id [simp]:
   "xs \<noteq> [] \<Longrightarrow> butlast xs @ [last xs] = xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma in_set_butlastD: "x \<in> set (butlast xs) \<Longrightarrow> x \<in> set xs"
-by (induct xs) (auto split: if_split_asm)
+  by (induct xs) (auto split: if_split_asm)
 
 lemma in_set_butlast_appendI:
   "x \<in> set (butlast xs) \<or> x \<in> set (butlast ys) \<Longrightarrow> x \<in> set (butlast (xs @ ys))"
-by (auto dest: in_set_butlastD simp add: butlast_append)
+  by (auto dest: in_set_butlastD simp add: butlast_append)
 
 lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"
-by (induct xs arbitrary: n)(auto split:nat.split)
+  by (induct xs arbitrary: n)(auto split:nat.split)
 
 lemma nth_butlast:
   assumes "n < length (butlast xs)" shows "butlast xs ! n = xs ! n"
@@ -1957,82 +1956,82 @@
 qed simp
 
 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
-by(induct xs)(auto simp:neq_Nil_conv)
+  by(induct xs)(auto simp:neq_Nil_conv)
 
 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
-by (induction xs rule: induct_list012) simp_all
+  by (induction xs rule: induct_list012) simp_all
 
 lemma last_list_update:
   "xs \<noteq> [] \<Longrightarrow> last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"
-by (auto simp: last_conv_nth)
+  by (auto simp: last_conv_nth)
 
 lemma butlast_list_update:
   "butlast(xs[k:=x]) =
   (if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])"
-by(cases xs rule:rev_cases)(auto simp: list_update_append split: nat.splits)
+  by(cases xs rule:rev_cases)(auto simp: list_update_append split: nat.splits)
 
 lemma last_map: "xs \<noteq> [] \<Longrightarrow> last (map f xs) = f (last xs)"
-by (cases xs rule: rev_cases) simp_all
+  by (cases xs rule: rev_cases) simp_all
 
 lemma map_butlast: "map f (butlast xs) = butlast (map f xs)"
-by (induct xs) simp_all
+  by (induct xs) simp_all
 
 lemma snoc_eq_iff_butlast:
   "xs @ [x] = ys \<longleftrightarrow> (ys \<noteq> [] \<and> butlast ys = xs \<and> last ys = x)"
-by fastforce
+  by fastforce
 
 corollary longest_common_suffix:
   "\<exists>ss xs' ys'. xs = xs' @ ss \<and> ys = ys' @ ss
        \<and> (xs' = [] \<or> ys' = [] \<or> last xs' \<noteq> last ys')"
-using longest_common_prefix[of "rev xs" "rev ys"]
-unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)
+  using longest_common_prefix[of "rev xs" "rev ys"]
+  unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)
 
 
 subsubsection \<open>@{const take} and @{const drop}\<close>
 
 lemma take_0: "take 0 xs = []"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma drop_0: "drop 0 xs = xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma take0[simp]: "take 0 = (\<lambda>xs. [])"
-by(rule ext) (rule take_0)
+  by(rule ext) (rule take_0)
 
 lemma drop0[simp]: "drop 0 = (\<lambda>x. x)"
-by(rule ext) (rule drop_0)
+  by(rule ext) (rule drop_0)
 
 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
-by simp
+  by simp
 
 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
-by simp
+  by simp
 
 declare take_Cons [simp del] and drop_Cons [simp del]
 
 lemma take_Suc: "xs \<noteq> [] \<Longrightarrow> take (Suc n) xs = hd xs # take n (tl xs)"
-by(clarsimp simp add:neq_Nil_conv)
+  by(clarsimp simp add:neq_Nil_conv)
 
 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
-by(cases xs, simp_all)
+  by(cases xs, simp_all)
 
 lemma hd_take[simp]: "j > 0 \<Longrightarrow> hd (take j xs) = hd xs"
-by (metis gr0_conv_Suc list.sel(1) take.simps(1) take_Suc)
+  by (metis gr0_conv_Suc list.sel(1) take.simps(1) take_Suc)
 
 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
-by (induct xs arbitrary: n) simp_all
+  by (induct xs arbitrary: n) simp_all
 
 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
-by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
+  by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
 
 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
-by (cases n, simp, cases xs, auto)
+  by (cases n, simp, cases xs, auto)
 
 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
-by (simp only: drop_tl)
+  by (simp only: drop_tl)
 
 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
-by (induct xs arbitrary: n, simp)(auto simp: drop_Cons nth_Cons split: nat.splits)
+  by (induct xs arbitrary: n, simp)(auto simp: drop_Cons nth_Cons split: nat.splits)
 
 lemma take_Suc_conv_app_nth:
   "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
@@ -2049,24 +2048,24 @@
 qed simp
 
 lemma length_take [simp]: "length (take n xs) = min (length xs) n"
-by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
 
 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
-by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
 
 lemma take_all [simp]: "length xs \<le> n ==> take n xs = xs"
-by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
 
 lemma drop_all [simp]: "length xs \<le> n ==> drop n xs = []"
-by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
 
 lemma take_append [simp]:
   "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
-by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
 
 lemma drop_append [simp]:
   "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
-by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+  by (induct n arbitrary: xs) (auto, case_tac xs, auto)
 
 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
 proof (induct m arbitrary: xs n)
@@ -2087,7 +2086,7 @@
 qed auto
 
 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
-by(induct xs arbitrary: m n)(auto simp: take_Cons drop_Cons split: nat.split)
+  by(induct xs arbitrary: m n)(auto simp: take_Cons drop_Cons split: nat.split)
 
 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
 proof (induct n arbitrary: xs)
@@ -2096,10 +2095,10 @@
 qed auto
 
 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
-by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split)
+  by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split)
 
 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs \<le> n)"
-by (induct xs arbitrary: n) (auto simp: drop_Cons split:nat.split)
+  by (induct xs arbitrary: n) (auto simp: drop_Cons split:nat.split)
 
 lemma take_map: "take n (map f xs) = map f (take n xs)"
 proof (induct n arbitrary: xs)
@@ -2146,19 +2145,19 @@
 
 lemma butlast_take:
   "n \<le> length xs ==> butlast (take n xs) = take (n - 1) xs"
-by (simp add: butlast_conv_take min.absorb1 min.absorb2)
+  by (simp add: butlast_conv_take min.absorb1 min.absorb2)
 
 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
-by (simp add: butlast_conv_take drop_take ac_simps)
+  by (simp add: butlast_conv_take drop_take ac_simps)
 
 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
-by (simp add: butlast_conv_take min.absorb1)
+  by (simp add: butlast_conv_take min.absorb1)
 
 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
-by (simp add: butlast_conv_take drop_take ac_simps)
+  by (simp add: butlast_conv_take drop_take ac_simps)
 
 lemma hd_drop_conv_nth: "n < length xs \<Longrightarrow> hd(drop n xs) = xs!n"
-by(simp add: hd_conv_nth)
+  by(simp add: hd_conv_nth)
 
 lemma set_take_subset_set_take:
   "m \<le> n \<Longrightarrow> set(take m xs) \<le> set(take n xs)"
@@ -2168,10 +2167,10 @@
 qed simp
 
 lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
-by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
+  by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
 
 lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
-by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
+  by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
 
 lemma set_drop_subset_set_drop:
   "m \<ge> n \<Longrightarrow> set(drop m xs) \<le> set(drop n xs)"
@@ -2182,10 +2181,10 @@
 qed simp
 
 lemma in_set_takeD: "x \<in> set(take n xs) \<Longrightarrow> x \<in> set xs"
-using set_take_subset by fast
+  using set_take_subset by fast
 
 lemma in_set_dropD: "x \<in> set(drop n xs) \<Longrightarrow> x \<in> set xs"
-using set_drop_subset by fast
+  using set_drop_subset by fast
 
 lemma append_eq_conv_conj:
   "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
@@ -2226,10 +2225,10 @@
 qed
 
 lemma take_update_cancel[simp]: "n \<le> m \<Longrightarrow> take n (xs[m := y]) = take n xs"
-by(simp add: list_eq_iff_nth_eq)
+  by(simp add: list_eq_iff_nth_eq)
 
 lemma drop_update_cancel[simp]: "n < m \<Longrightarrow> drop m (xs[n := x]) = drop m xs"
-by(simp add: list_eq_iff_nth_eq)
+  by(simp add: list_eq_iff_nth_eq)
 
 lemma upd_conv_take_nth_drop:
   "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
@@ -2258,27 +2257,27 @@
 qed auto
 
 lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
-by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
+  by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
 
 
 subsubsection \<open>@{const takeWhile} and @{const dropWhile}\<close>
 
 lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma takeWhile_append1 [simp]:
   "\<lbrakk>x \<in> set xs; \<not>P(x)\<rbrakk> \<Longrightarrow> takeWhile P (xs @ ys) = takeWhile P xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma takeWhile_append2 [simp]:
   "(\<And>x. x \<in> set xs \<Longrightarrow> P x) \<Longrightarrow> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma takeWhile_tail: "\<not> P x \<Longrightarrow> takeWhile P (xs @ (x#l)) = takeWhile P xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma takeWhile_nth: "j < length (takeWhile P xs) \<Longrightarrow> takeWhile P xs ! j = xs ! j"
   by (metis nth_append takeWhile_dropWhile_id)
@@ -2288,62 +2287,62 @@
   by (metis add.commute nth_append_length_plus takeWhile_dropWhile_id)
 
 lemma length_dropWhile_le: "length (dropWhile P xs) \<le> length xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma dropWhile_append1 [simp]:
   "\<lbrakk>x \<in> set xs; \<not>P(x)\<rbrakk> \<Longrightarrow> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma dropWhile_append2 [simp]:
   "(\<And>x. x \<in> set xs \<Longrightarrow> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma dropWhile_append3:
   "\<not> P y \<Longrightarrow>dropWhile P (xs @ y # ys) = dropWhile P xs @ y # ys"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma dropWhile_last:
   "x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> last (dropWhile P xs) = last xs"
-by (auto simp add: dropWhile_append3 in_set_conv_decomp)
+  by (auto simp add: dropWhile_append3 in_set_conv_decomp)
 
 lemma set_dropWhileD: "x \<in> set (dropWhile P xs) \<Longrightarrow> x \<in> set xs"
-by (induct xs) (auto split: if_split_asm)
+  by (induct xs) (auto split: if_split_asm)
 
 lemma set_takeWhileD: "x \<in> set (takeWhile P xs) \<Longrightarrow> x \<in> set xs \<and> P x"
-by (induct xs) (auto split: if_split_asm)
+  by (induct xs) (auto split: if_split_asm)
 
 lemma takeWhile_eq_all_conv[simp]:
   "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
-by(induct xs, auto)
+  by(induct xs, auto)
 
 lemma dropWhile_eq_Nil_conv[simp]:
   "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
-by(induct xs, auto)
+  by(induct xs, auto)
 
 lemma dropWhile_eq_Cons_conv:
   "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys \<and> \<not> P y)"
-by(induct xs, auto)
+  by(induct xs, auto)
 
 lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"
-by (induct xs) (auto dest: set_takeWhileD)
+  by (induct xs) (auto dest: set_takeWhileD)
 
 lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \<circ> f) xs)"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \<circ> f) xs)"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma takeWhile_eq_take: "takeWhile P xs = take (length (takeWhile P xs)) xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma hd_dropWhile: "dropWhile P xs \<noteq> [] \<Longrightarrow> \<not> P (hd (dropWhile P xs))"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma takeWhile_eq_filter:
   assumes "\<And> x. x \<in> set (dropWhile P xs) \<Longrightarrow> \<not> P x"
@@ -2384,12 +2383,12 @@
       thus "\<not> P (xs ! n')" using Cons by auto
     qed
     ultimately show ?thesis by simp
-   qed
+  qed
 qed
 
 lemma nth_length_takeWhile:
   "length (takeWhile P xs) < length xs \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma length_takeWhile_less_P_nth:
   assumes all: "\<And> i. i < j \<Longrightarrow> P (xs ! i)" and "j \<le> length xs"
@@ -2402,7 +2401,7 @@
 
 lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
   takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
-by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
+  by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
 
 lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
   dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
@@ -2414,34 +2413,34 @@
 
 lemma takeWhile_not_last:
   "distinct xs \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
-by(induction xs rule: induct_list012) auto
+  by(induction xs rule: induct_list012) auto
 
 lemma takeWhile_cong [fundef_cong]:
   "\<lbrakk>l = k; \<And>x. x \<in> set l \<Longrightarrow> P x = Q x\<rbrakk>
   \<Longrightarrow> takeWhile P l = takeWhile Q k"
-by (induct k arbitrary: l) (simp_all)
+  by (induct k arbitrary: l) (simp_all)
 
 lemma dropWhile_cong [fundef_cong]:
   "\<lbrakk>l = k; \<And>x. x \<in> set l \<Longrightarrow> P x = Q x\<rbrakk>
   \<Longrightarrow> dropWhile P l = dropWhile Q k"
-by (induct k arbitrary: l, simp_all)
+  by (induct k arbitrary: l, simp_all)
 
 lemma takeWhile_idem [simp]:
   "takeWhile P (takeWhile P xs) = takeWhile P xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma dropWhile_idem [simp]:
   "dropWhile P (dropWhile P xs) = dropWhile P xs"
-by (induct xs) auto
+  by (induct xs) auto
 
 
 subsubsection \<open>@{const zip}\<close>
 
 lemma zip_Nil [simp]: "zip [] ys = []"
-by (induct ys) auto
+  by (induct ys) auto
 
 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
-by simp
+  by simp
 
 declare zip_Cons [simp del]
 
@@ -2449,15 +2448,15 @@
   "zip [] ys = []"
   "zip xs [] = []"
   "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
-by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+
+  by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+
 
 lemma zip_Cons1:
   "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
-by(auto split:list.split)
+  by(auto split:list.split)
 
 lemma length_zip [simp]:
   "length (zip xs ys) = min (length xs) (length ys)"
-by (induct xs ys rule:list_induct2') auto
+  by (induct xs ys rule:list_induct2') auto
 
 lemma zip_obtain_same_length:
   assumes "\<And>zs ws n. length zs = length ws \<Longrightarrow> n = min (length xs) (length ys)
@@ -2479,21 +2478,21 @@
 lemma zip_append1:
   "zip (xs @ ys) zs =
   zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
-by (induct xs zs rule:list_induct2') auto
+  by (induct xs zs rule:list_induct2') auto
 
 lemma zip_append2:
   "zip xs (ys @ zs) =
   zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
-by (induct xs ys rule:list_induct2') auto
+  by (induct xs ys rule:list_induct2') auto
 
 lemma zip_append [simp]:
   "[| length xs = length us |] ==>
   zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
-by (simp add: zip_append1)
+  by (simp add: zip_append1)
 
 lemma zip_rev:
   "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
-by (induct rule:list_induct2, simp_all)
+  by (induct rule:list_induct2, simp_all)
 
 lemma zip_map_map:
   "zip (map f xs) (map g ys) = map (\<lambda> (x, y). (f x, g y)) (zip xs ys)"
@@ -2508,23 +2507,23 @@
 
 lemma zip_map1:
   "zip (map f xs) ys = map (\<lambda>(x, y). (f x, y)) (zip xs ys)"
-using zip_map_map[of f xs "\<lambda>x. x" ys] by simp
+  using zip_map_map[of f xs "\<lambda>x. x" ys] by simp
 
 lemma zip_map2:
   "zip xs (map f ys) = map (\<lambda>(x, y). (x, f y)) (zip xs ys)"
-using zip_map_map[of "\<lambda>x. x" xs f ys] by simp
+  using zip_map_map[of "\<lambda>x. x" xs f ys] by simp
 
 lemma map_zip_map:
   "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
-by (auto simp: zip_map1)
+  by (auto simp: zip_map1)
 
 lemma map_zip_map2:
   "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
-by (auto simp: zip_map2)
+  by (auto simp: zip_map2)
 
 text\<open>Courtesy of Andreas Lochbihler:\<close>
 lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
-by(induct xs) auto
+  by(induct xs) auto
 
 lemma nth_zip [simp]:
   "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
@@ -2536,10 +2535,10 @@
 
 lemma set_zip:
   "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
-by(simp add: set_conv_nth cong: rev_conj_cong)
+  by(simp add: set_conv_nth cong: rev_conj_cong)
 
 lemma zip_same: "((a,b) \<in> set (zip xs xs)) = (a \<in> set xs \<and> a = b)"
-by(induct xs) auto
+  by(induct xs) auto
 
 lemma zip_update: "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
   by (simp add: update_zip)
@@ -2553,7 +2552,7 @@
 qed auto
 
 lemma zip_replicate1: "zip (replicate n x) ys = map (Pair x) (take n ys)"
-by(induction ys arbitrary: n)(case_tac [2] n, simp_all)
+  by(induction ys arbitrary: n)(case_tac [2] n, simp_all)
 
 lemma take_zip: "take n (zip xs ys) = zip (take n xs) (take n ys)"
 proof (induct n arbitrary: xs ys)
@@ -2580,26 +2579,26 @@
 qed simp
 
 lemma set_zip_leftD: "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
-by (induct xs ys rule:list_induct2') auto
+  by (induct xs ys rule:list_induct2') auto
 
 lemma set_zip_rightD: "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
-by (induct xs ys rule:list_induct2') auto
+  by (induct xs ys rule:list_induct2') auto
 
 lemma in_set_zipE:
   "(x,y) \<in> set(zip xs ys) \<Longrightarrow> (\<lbrakk> x \<in> set xs; y \<in> set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
-by(blast dest: set_zip_leftD set_zip_rightD)
+  by(blast dest: set_zip_leftD set_zip_rightD)
 
 lemma zip_map_fst_snd: "zip (map fst zs) (map snd zs) = zs"
-by (induct zs) simp_all
+  by (induct zs) simp_all
 
 lemma zip_eq_conv:
   "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
-by (auto simp add: zip_map_fst_snd)
+  by (auto simp add: zip_map_fst_snd)
 
 lemma in_set_zip:
   "p \<in> set (zip xs ys) \<longleftrightarrow> (\<exists>n. xs ! n = fst p \<and> ys ! n = snd p
   \<and> n < length xs \<and> n < length ys)"
-by (cases p) (auto simp add: set_zip)
+  by (cases p) (auto simp add: set_zip)
 
 lemma in_set_impl_in_set_zip1:
   assumes "length xs = length ys"
@@ -2633,25 +2632,25 @@
 
 lemma list_all2_lengthD [intro?]:
   "list_all2 P xs ys ==> length xs = length ys"
-by (simp add: list_all2_iff)
+  by (simp add: list_all2_iff)
 
 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
-by (simp add: list_all2_iff)
+  by (simp add: list_all2_iff)
 
 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
-by (simp add: list_all2_iff)
+  by (simp add: list_all2_iff)
 
 lemma list_all2_Cons [iff, code]:
   "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
-by (auto simp add: list_all2_iff)
+  by (auto simp add: list_all2_iff)
 
 lemma list_all2_Cons1:
   "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
-by (cases ys) auto
+  by (cases ys) auto
 
 lemma list_all2_Cons2:
   "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
-by (cases xs) auto
+  by (cases xs) auto
 
 lemma list_all2_induct
   [consumes 1, case_names Nil Cons, induct set: list_all2]:
@@ -2660,16 +2659,16 @@
   assumes Cons: "\<And>x xs y ys.
     \<lbrakk>P x y; list_all2 P xs ys; R xs ys\<rbrakk> \<Longrightarrow> R (x # xs) (y # ys)"
   shows "R xs ys"
-using P
-by (induct xs arbitrary: ys) (auto simp add: list_all2_Cons1 Nil Cons)
+  using P
+  by (induct xs arbitrary: ys) (auto simp add: list_all2_Cons1 Nil Cons)
 
 lemma list_all2_rev [iff]:
   "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
-by (simp add: list_all2_iff zip_rev cong: conj_cong)
+  by (simp add: list_all2_iff zip_rev cong: conj_cong)
 
 lemma list_all2_rev1:
   "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
-by (subst list_all2_rev [symmetric]) simp
+  by (subst list_all2_rev [symmetric]) simp
 
 lemma list_all2_append1:
   "list_all2 P (xs @ ys) zs =
@@ -2708,21 +2707,21 @@
 lemma list_all2_append:
   "length xs = length ys \<Longrightarrow>
   list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
-by (induct rule:list_induct2, simp_all)
+  by (induct rule:list_induct2, simp_all)
 
 lemma list_all2_appendI [intro?, trans]:
   "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
-by (simp add: list_all2_append list_all2_lengthD)
+  by (simp add: list_all2_append list_all2_lengthD)
 
 lemma list_all2_conv_all_nth:
   "list_all2 P xs ys =
   (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
-by (force simp add: list_all2_iff set_zip)
+  by (force simp add: list_all2_iff set_zip)
 
 lemma list_all2_trans:
   assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
   shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
-        (is "!!bs cs. PROP ?Q as bs cs")
+    (is "!!bs cs. PROP ?Q as bs cs")
 proof (induct as)
   fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
   show "!!cs. PROP ?Q (x # xs) bs cs"
@@ -2735,35 +2734,35 @@
 
 lemma list_all2_all_nthI [intro?]:
   "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
-by (simp add: list_all2_conv_all_nth)
+  by (simp add: list_all2_conv_all_nth)
 
 lemma list_all2I:
   "\<forall>x \<in> set (zip a b). case_prod P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
-by (simp add: list_all2_iff)
+  by (simp add: list_all2_iff)
 
 lemma list_all2_nthD:
   "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
-by (simp add: list_all2_conv_all_nth)
+  by (simp add: list_all2_conv_all_nth)
 
 lemma list_all2_nthD2:
   "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
-by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
+  by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
 
 lemma list_all2_map1:
   "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
-by (simp add: list_all2_conv_all_nth)
+  by (simp add: list_all2_conv_all_nth)
 
 lemma list_all2_map2:
   "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
-by (auto simp add: list_all2_conv_all_nth)
+  by (auto simp add: list_all2_conv_all_nth)
 
 lemma list_all2_refl [intro?]:
   "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
-by (simp add: list_all2_conv_all_nth)
+  by (simp add: list_all2_conv_all_nth)
 
 lemma list_all2_update_cong:
   "\<lbrakk> list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
-by (cases "i < length ys") (auto simp add: list_all2_conv_all_nth nth_list_update)
+  by (cases "i < length ys") (auto simp add: list_all2_conv_all_nth nth_list_update)
 
 lemma list_all2_takeI [simp,intro?]:
   "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
@@ -2787,46 +2786,46 @@
 
 lemma list_all2_eq:
   "xs = ys \<longleftrightarrow> list_all2 (=) xs ys"
-by (induct xs ys rule: list_induct2') auto
+  by (induct xs ys rule: list_induct2') auto
 
 lemma list_eq_iff_zip_eq:
   "xs = ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x,y) \<in> set (zip xs ys). x = y)"
-by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
+  by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
 
 lemma list_all2_same: "list_all2 P xs xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x x)"
-by(auto simp add: list_all2_conv_all_nth set_conv_nth)
+  by(auto simp add: list_all2_conv_all_nth set_conv_nth)
 
 lemma zip_assoc:
   "zip xs (zip ys zs) = map (\<lambda>((x, y), z). (x, y, z)) (zip (zip xs ys) zs)"
-by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
+  by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
 
 lemma zip_commute: "zip xs ys = map (\<lambda>(x, y). (y, x)) (zip ys xs)"
-by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
+  by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
 
 lemma zip_left_commute:
   "zip xs (zip ys zs) = map (\<lambda>(y, (x, z)). (x, y, z)) (zip ys (zip xs zs))"
-by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
+  by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
 
 lemma zip_replicate2: "zip xs (replicate n y) = map (\<lambda>x. (x, y)) (take n xs)"
-by(subst zip_commute)(simp add: zip_replicate1)
+  by(subst zip_commute)(simp add: zip_replicate1)
 
 subsubsection \<open>@{const List.product} and @{const product_lists}\<close>
 
 lemma product_concat_map:
   "List.product xs ys = concat (map (\<lambda>x. map (\<lambda>y. (x,y)) ys) xs)"
-by(induction xs) (simp)+
+  by(induction xs) (simp)+
 
 lemma set_product[simp]: "set (List.product xs ys) = set xs \<times> set ys"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma length_product [simp]:
   "length (List.product xs ys) = length xs * length ys"
-by (induct xs) simp_all
+  by (induct xs) simp_all
 
 lemma product_nth:
   assumes "n < length xs * length ys"
   shows "List.product xs ys ! n = (xs ! (n div length ys), ys ! (n mod length ys))"
-using assms proof (induct xs arbitrary: n)
+  using assms proof (induct xs arbitrary: n)
   case Nil then show ?case by simp
 next
   case (Cons x xs n)
@@ -2837,7 +2836,7 @@
 
 lemma in_set_product_lists_length:
   "xs \<in> set (product_lists xss) \<Longrightarrow> length xs = length xss"
-by (induct xss arbitrary: xs) auto
+  by (induct xss arbitrary: xs) auto
 
 lemma product_lists_set:
   "set (product_lists xss) = {xs. list_all2 (\<lambda>x ys. x \<in> set ys) xs xss}" (is "?L = Collect ?R")
@@ -2856,25 +2855,25 @@
 lemma fold_simps [code]: \<comment> \<open>eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala\<close>
   "fold f [] s = s"
   "fold f (x # xs) s = fold f xs (f x s)"
-by simp_all
+  by simp_all
 
 lemma fold_remove1_split:
   "\<lbrakk> \<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x;
     x \<in> set xs \<rbrakk>
   \<Longrightarrow> fold f xs = fold f (remove1 x xs) \<circ> f x"
-by (induct xs) (auto simp add: comp_assoc)
+  by (induct xs) (auto simp add: comp_assoc)
 
 lemma fold_cong [fundef_cong]:
   "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
     \<Longrightarrow> fold f xs a = fold g ys b"
-by (induct ys arbitrary: a b xs) simp_all
+  by (induct ys arbitrary: a b xs) simp_all
 
 lemma fold_id: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = id) \<Longrightarrow> fold f xs = id"
-by (induct xs) simp_all
+  by (induct xs) simp_all
 
 lemma fold_commute:
   "(\<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"
-by (induct xs) (simp_all add: fun_eq_iff)
+  by (induct xs) (simp_all add: fun_eq_iff)
 
 lemma fold_commute_apply:
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
@@ -2887,41 +2886,41 @@
 lemma fold_invariant:
   "\<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>
   \<Longrightarrow> P (fold f xs s)"
-by (induct xs arbitrary: s) simp_all
+  by (induct xs arbitrary: s) simp_all
 
 lemma fold_append [simp]: "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
-by (induct xs) simp_all
+  by (induct xs) simp_all
 
 lemma fold_map [code_unfold]: "fold g (map f xs) = fold (g \<circ> f) xs"
-by (induct xs) simp_all
+  by (induct xs) simp_all
 
 lemma fold_filter:
   "fold f (filter P xs) = fold (\<lambda>x. if P x then f x else id) xs"
-by (induct xs) simp_all
+  by (induct xs) simp_all
 
 lemma fold_rev:
   "(\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y)
   \<Longrightarrow> fold f (rev xs) = fold f xs"
-by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff)
+  by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff)
 
 lemma fold_Cons_rev: "fold Cons xs = append (rev xs)"
-by (induct xs) simp_all
+  by (induct xs) simp_all
 
 lemma rev_conv_fold [code]: "rev xs = fold Cons xs []"
-by (simp add: fold_Cons_rev)
+  by (simp add: fold_Cons_rev)
 
 lemma fold_append_concat_rev: "fold append xss = append (concat (rev xss))"
-by (induct xss) simp_all
+  by (induct xss) simp_all
 
 text \<open>@{const Finite_Set.fold} and @{const fold}\<close>
 
 lemma (in comp_fun_commute) fold_set_fold_remdups:
   "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
-by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm insert_absorb)
+  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm insert_absorb)
 
 lemma (in comp_fun_idem) fold_set_fold:
   "Finite_Set.fold f y (set xs) = fold f xs y"
-by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm)
+  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm)
 
 lemma union_set_fold [code]: "set xs \<union> A = fold Set.insert xs A"
 proof -
@@ -2932,7 +2931,7 @@
 
 lemma union_coset_filter [code]:
   "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)"
-by auto
+  by auto
 
 lemma minus_set_fold [code]: "A - set xs = fold Set.remove xs A"
 proof -
@@ -2944,15 +2943,15 @@
 
 lemma minus_coset_filter [code]:
   "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
-by auto
+  by auto
 
 lemma inter_set_filter [code]:
   "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
-by auto
+  by auto
 
 lemma inter_coset_fold [code]:
   "A \<inter> List.coset xs = fold Set.remove xs A"
-by (simp add: Diff_eq [symmetric] minus_set_fold)
+  by (simp add: Diff_eq [symmetric] minus_set_fold)
 
 lemma (in semilattice_set) set_eq_fold [code]:
   "F (set (x # xs)) = fold f xs x"
@@ -3000,70 +2999,70 @@
 text \<open>Correspondence\<close>
 
 lemma foldr_conv_fold [code_abbrev]: "foldr f xs = fold f (rev xs)"
-by (induct xs) simp_all
+  by (induct xs) simp_all
 
 lemma foldl_conv_fold: "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
-by (induct xs arbitrary: s) simp_all
+  by (induct xs arbitrary: s) simp_all
 
 lemma foldr_conv_foldl: \<comment> \<open>The ``Third Duality Theorem'' in Bird \& Wadler:\<close>
   "foldr f xs a = foldl (\<lambda>x y. f y x) a (rev xs)"
-by (simp add: foldr_conv_fold foldl_conv_fold)
+  by (simp add: foldr_conv_fold foldl_conv_fold)
 
 lemma foldl_conv_foldr:
   "foldl f a xs = foldr (\<lambda>x y. f y x) (rev xs) a"
-by (simp add: foldr_conv_fold foldl_conv_fold)
+  by (simp add: foldr_conv_fold foldl_conv_fold)
 
 lemma foldr_fold:
   "(\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y)
   \<Longrightarrow> foldr f xs = fold f xs"
-unfolding foldr_conv_fold by (rule fold_rev)
+  unfolding foldr_conv_fold by (rule fold_rev)
 
 lemma foldr_cong [fundef_cong]:
   "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"
-by (auto simp add: foldr_conv_fold intro!: fold_cong)
+  by (auto simp add: foldr_conv_fold intro!: fold_cong)
 
 lemma foldl_cong [fundef_cong]:
   "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"
-by (auto simp add: foldl_conv_fold intro!: fold_cong)
+  by (auto simp add: foldl_conv_fold intro!: fold_cong)
 
 lemma foldr_append [simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
-by (simp add: foldr_conv_fold)
+  by (simp add: foldr_conv_fold)
 
 lemma foldl_append [simp]: "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
-by (simp add: foldl_conv_fold)
+  by (simp add: foldl_conv_fold)
 
 lemma foldr_map [code_unfold]: "foldr g (map f xs) a = foldr (g \<circ> f) xs a"
-by (simp add: foldr_conv_fold fold_map rev_map)
+  by (simp add: foldr_conv_fold fold_map rev_map)
 
 lemma foldr_filter:
   "foldr f (filter P xs) = foldr (\<lambda>x. if P x then f x else id) xs"
-by (simp add: foldr_conv_fold rev_filter fold_filter)
+  by (simp add: foldr_conv_fold rev_filter fold_filter)
 
 lemma foldl_map [code_unfold]:
   "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs"
-by (simp add: foldl_conv_fold fold_map comp_def)
+  by (simp add: foldl_conv_fold fold_map comp_def)
 
 lemma concat_conv_foldr [code]:
   "concat xss = foldr append xss []"
-by (simp add: fold_append_concat_rev foldr_conv_fold)
+  by (simp add: fold_append_concat_rev foldr_conv_fold)
 
 
 subsubsection \<open>@{const upt}\<close>
 
 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
-\<comment> \<open>simp does not terminate!\<close>
-by (induct j) auto
+  \<comment> \<open>simp does not terminate!\<close>
+  by (induct j) auto
 
 lemmas upt_rec_numeral[simp] = upt_rec[of "numeral m" "numeral n"] for m n
 
 lemma upt_conv_Nil [simp]: "j \<le> i ==> [i..<j] = []"
-by (subst upt_rec) simp
+  by (subst upt_rec) simp
 
 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j \<le> i)"
-by(induct j)simp_all
+  by(induct j)simp_all
 
 lemma upt_eq_Cons_conv:
- "([i..<j] = x#xs) = (i < j \<and> i = x \<and> [i+1..<j] = xs)"
+  "([i..<j] = x#xs) = (i < j \<and> i = x \<and> [i+1..<j] = xs)"
 proof (induct j arbitrary: x xs)
   case (Suc j)
   then show ?case
@@ -3071,11 +3070,11 @@
 qed simp
 
 lemma upt_Suc_append: "i \<le> j ==> [i..<(Suc j)] = [i..<j]@[j]"
-\<comment> \<open>Only needed if \<open>upt_Suc\<close> is deleted from the simpset.\<close>
-by simp
+  \<comment> \<open>Only needed if \<open>upt_Suc\<close> is deleted from the simpset.\<close>
+  by simp
 
 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
-by (simp add: upt_rec)
+  by (simp add: upt_rec)
 
 lemma upt_conv_Cons_Cons: \<comment> \<open>no precondition\<close>
   "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
@@ -3086,23 +3085,23 @@
 qed
 
 lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
-\<comment> \<open>LOOPS as a simprule, since \<open>j \<le> j\<close>.\<close>
-by (induct k) auto
+  \<comment> \<open>LOOPS as a simprule, since \<open>j \<le> j\<close>.\<close>
+  by (induct k) auto
 
 lemma length_upt [simp]: "length [i..<j] = j - i"
-by (induct j) (auto simp add: Suc_diff_le)
+  by (induct j) (auto simp add: Suc_diff_le)
 
 lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
-by (induct j) (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
+  by (induct j) (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
 
 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
-by(simp add:upt_conv_Cons)
+  by(simp add:upt_conv_Cons)
 
 lemma tl_upt: "tl [m..<n] = [Suc m..<n]"
-by (simp add: upt_rec)
+  by (simp add: upt_rec)
 
 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
-by(cases j)(auto simp: upt_Suc_append)
+  by(cases j)(auto simp: upt_Suc_append)
 
 lemma take_upt [simp]: "i+m \<le> n ==> take m [i..<n] = [i..<i+m]"
 proof (induct m arbitrary: i)
@@ -3112,26 +3111,26 @@
 qed simp
 
 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
-by(induct j) auto
+  by(induct j) auto
 
 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
-by (induct n) auto
+  by (induct n) auto
 
 lemma map_add_upt: "map (\<lambda>i. i + n) [0..<m] = [n..<m + n]"
-by (induct m) simp_all
+  by (induct m) simp_all
 
 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
 proof (induct n m  arbitrary: i rule: diff_induct)
-case (3 x y)
+  case (3 x y)
   then show ?case
     by (metis add.commute length_upt less_diff_conv nth_map nth_upt)
 qed auto
 
 lemma map_decr_upt: "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
-by (induct n) simp_all
+  by (induct n) simp_all
 
 lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda>i. f (Suc i)) [0 ..< n]"
-by (induct n arbitrary: f) auto
+  by (induct n arbitrary: f) auto
 
 lemma nth_take_lemma:
   "k \<le> length xs \<Longrightarrow> k \<le> length ys \<Longrightarrow>
@@ -3145,24 +3144,20 @@
 
 lemma nth_equalityI:
   "[| length xs = length ys; \<forall>i < length xs. xs!i = ys!i |] ==> xs = ys"
-by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
+  by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
 
 lemma map_nth:
   "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
-by (rule nth_equalityI, auto)
+  by (rule nth_equalityI, auto)
 
 lemma list_all2_antisym:
   "\<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>
   \<Longrightarrow> xs = ys"
-apply (simp add: list_all2_conv_all_nth)
-apply (rule nth_equalityI, blast, simp)
-done
+  by (simp add: list_all2_conv_all_nth nth_equalityI)
 
 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
 \<comment> \<open>The famous take-lemma.\<close>
-apply (drule_tac x = "max (length xs) (length ys)" in spec)
-apply (simp add: le_max_iff_disj)
-done
+  by (metis length_take min.commute order_refl take_all)
 
 lemma take_Cons':
   "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
@@ -3239,7 +3234,7 @@
 qed
 
 lemma nth_upto: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k"
-apply(induction i j arbitrary: k rule: upto.induct)
+  apply(induction i j arbitrary: k rule: upto.induct)
 apply(subst upto_rec1)
 apply(auto simp add: nth_Cons')
 done
@@ -3310,12 +3305,11 @@
 
 lemma length_remdups_eq[iff]:
   "(length (remdups xs) = length xs) = (remdups xs = xs)"
-apply(induct xs)
- apply auto
-apply(subgoal_tac "length (remdups xs) \<le> length xs")
- apply arith
-apply(rule length_remdups_leq)
-done
+proof (induct xs)
+  case (Cons a xs)
+  then show ?case
+    by simp (metis Suc_n_not_le_n impossible_Cons length_remdups_leq)
+qed auto
 
 lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)"
 by (induct xs) auto
@@ -3341,31 +3335,38 @@
 done
 
 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
-apply(induct xs arbitrary: i)
- apply simp
-apply (case_tac i)
- apply simp_all
-apply(blast dest:in_set_takeD)
-done
+proof (induct xs arbitrary: i)
+  case (Cons a xs)
+  then show ?case
+    by (metis Cons.prems append_take_drop_id distinct_append)
+qed auto
 
 lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
-apply(induct xs arbitrary: i)
- apply simp
-apply (case_tac i)
- apply simp_all
-done
+proof (induct xs arbitrary: i)
+  case (Cons a xs)
+  then show ?case
+    by (metis Cons.prems append_take_drop_id distinct_append)
+qed auto
 
 lemma distinct_list_update:
-assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
-shows "distinct (xs[i:=a])"
+  assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
+  shows "distinct (xs[i:=a])"
 proof (cases "i < length xs")
   case True
-  with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
-    apply (drule_tac id_take_nth_drop) by simp
-  with d True show ?thesis
-    apply (simp add: upd_conv_take_nth_drop)
-    apply (drule subst [OF id_take_nth_drop]) apply assumption
-    apply simp apply (cases "a = xs!i") apply simp by blast
+  with a have anot: "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
+    by simp (metis in_set_dropD in_set_takeD)
+  show ?thesis
+  proof (cases "a = xs!i")
+    case True
+    with d show ?thesis
+      by auto
+  next
+    case False
+    then show ?thesis
+      using d anot \<open>i < length xs\<close> 
+      apply (simp add: upd_conv_take_nth_drop)
+      by (metis disjoint_insert(1) distinct_append id_take_nth_drop set_simps(2))
+  qed
 next
   case False with d show ?thesis by auto
 qed
@@ -3380,22 +3381,14 @@
 text \<open>It is best to avoid this indexed version of distinct, but
 sometimes it is useful.\<close>
 
-lemma distinct_conv_nth:
-"distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j \<longrightarrow> xs!i \<noteq> xs!j)"
-apply (induct xs, simp, simp)
-apply (rule iffI, clarsimp)
- apply (case_tac i)
-apply (case_tac j, simp)
-apply (simp add: set_conv_nth)
- apply (case_tac j)
-apply (clarsimp simp add: set_conv_nth, simp)
-apply (rule conjI)
- apply (clarsimp simp add: set_conv_nth)
- apply (erule_tac x = 0 in allE, simp)
- apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
-apply (erule_tac x = "Suc i" in allE, simp)
-apply (erule_tac x = "Suc j" in allE, simp)
-done
+lemma distinct_conv_nth: "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j \<longrightarrow> xs!i \<noteq> xs!j)"
+proof (induct xs)
+  case (Cons x xs)
+  show ?case
+    apply (auto simp add: Cons nth_Cons split: nat.split_asm)
+    apply (metis Suc_less_eq2 in_set_conv_nth less_not_refl zero_less_Suc)+
+    done
+qed auto
 
 lemma nth_eq_iff_index_eq:
   "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
@@ -3420,7 +3413,7 @@
 
 lemma distinct_swap[simp]: "\<lbrakk> i < size xs; j < size xs \<rbrakk> \<Longrightarrow>
   distinct(xs[i := xs!j, j := xs!i]) = distinct xs"
-apply (simp add: distinct_conv_nth nth_list_update)
+  apply (simp add: distinct_conv_nth nth_list_update)
 apply safe
 apply metis+
 done
@@ -3434,8 +3427,6 @@
 
 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
 proof (induct xs)
-  case Nil thus ?case by simp
-next
   case (Cons x xs)
   show ?case
   proof (cases "x \<in> set xs")
@@ -3448,17 +3439,20 @@
     ultimately have False by simp
     thus ?thesis ..
   qed
-qed
+qed simp
 
 lemma distinct_length_filter: "distinct xs \<Longrightarrow> length (filter P xs) = card ({x. P x} Int set xs)"
 by (induct xs) (auto)
 
 lemma not_distinct_decomp: "\<not> distinct ws \<Longrightarrow> \<exists>xs ys zs y. ws = xs@[y]@ys@[y]@zs"
-apply (induct n == "length ws" arbitrary:ws) apply simp
-apply(case_tac ws) apply simp
-apply (simp split:if_split_asm)
-apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
-done
+proof (induct n == "length ws" arbitrary:ws)
+  case (Suc n ws)
+  then show ?case
+    using length_Suc_conv [of ws n]
+    apply (auto simp: eq_commute)
+     apply (metis append_Nil in_set_conv_decomp_first)
+    by (metis append_Cons)
+qed simp
 
 lemma not_distinct_conv_prefix:
   defines "dec as xs y ys \<equiv> y \<in> set xs \<and> distinct xs \<and> as = xs @ y # ys"
@@ -3690,7 +3684,6 @@
         then have "Suc 0 \<notin> f ` {0 ..< length (x1 # x2 # xs)}" by auto
         then show False using f_img \<open>2 \<le> length ys\<close> by auto
       qed
-
       obtain ys' where "ys = x1 # x2 # ys'"
         using \<open>2 \<le> length ys\<close> f_nth[of 0] f_nth[of 1]
         apply (cases ys)
@@ -3715,10 +3708,7 @@
           using Suc0_le_f_Suc f_mono by (auto simp: f'_def mono_iff_le_Suc le_diff_iff)
       next
         have "f' ` {0 ..< length (x2 # xs)} = (\<lambda>x. f x - 1) ` {0 ..< length (x1 # x2 #xs)}"
-          apply safe
-          apply (rename_tac [!] n,  case_tac [!] n)
-          apply (auto simp: f'_def \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close> intro: rev_image_eqI)
-          done
+          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)
         also have "\<dots> = (\<lambda>x. x - 1) ` f ` {0 ..< length (x1 # x2 #xs)}"
           by (auto simp: image_comp)
         also have "\<dots> = (\<lambda>x. x - 1) ` {0 ..< length ys}"
@@ -3885,10 +3875,12 @@
 
 lemma sum_count_set:
   "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> sum (count_list xs) X = length xs"
-apply(induction xs arbitrary: X)
- apply simp
-apply (simp add: sum.If_cases)
-by (metis Diff_eq sum.remove)
+proof (induction xs arbitrary: X)
+  case (Cons x xs)
+  then show ?case
+    apply (auto simp: sum.If_cases sum.remove)
+    by (metis (no_types) Cons.IH Cons.prems(2) diff_eq sum.remove)
+qed simp
 
 
 subsubsection \<open>@{const List.extract}\<close>
@@ -3931,23 +3923,13 @@
 
 lemma in_set_remove1[simp]:
   "a \<noteq> b \<Longrightarrow> a \<in> set(remove1 b xs) = (a \<in> set xs)"
-apply (induct xs)
- apply auto
-done
+  by (induct xs) auto
 
 lemma set_remove1_subset: "set(remove1 x xs) \<subseteq> set xs"
-apply(induct xs)
- apply simp
-apply simp
-apply blast
-done
+  by (induct xs) auto
 
 lemma set_remove1_eq [simp]: "distinct xs \<Longrightarrow> set(remove1 x xs) = set xs - {x}"
-apply(induct xs)
- apply simp
-apply simp
-apply blast
-done
+  by (induct xs) auto
 
 lemma length_remove1:
   "length(remove1 x xs) = (if x \<in> set xs then length xs - 1 else length xs)"
@@ -4067,9 +4049,7 @@
 text\<open>Courtesy of Matthias Daum:\<close>
 lemma append_replicate_commute:
   "replicate n x @ replicate k x = replicate k x @ replicate n x"
-apply (simp add: replicate_add [symmetric])
-apply (simp add: add.commute)
-done
+  by (metis add.commute replicate_add)
 
 text\<open>Courtesy of Andreas Lochbihler:\<close>
 lemma filter_replicate:
@@ -4090,23 +4070,24 @@
 
 text\<open>Courtesy of Matthias Daum (2 lemmas):\<close>
 lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
-apply (case_tac "k \<le> i")
- apply  (simp add: min_def)
-apply (drule not_le_imp_less)
-apply (simp add: min_def)
-apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
- apply  simp
-apply (simp add: replicate_add [symmetric])
-done
+proof (cases "k \<le> i")
+  case True
+  then show ?thesis
+    by (simp add: min_def)
+next
+  case False
+  then have "replicate k x = replicate i x @ replicate (k - i) x"
+    by (simp add: replicate_add [symmetric])
+  then show ?thesis
+    by (simp add: min_def)
+qed
 
 lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
-apply (induct k arbitrary: i)
- apply simp
-apply clarsimp
-apply (case_tac i)
- apply simp
-apply clarsimp
-done
+proof (induct k arbitrary: i)
+  case (Suc k)
+  then show ?case
+    by (simp add: drop_Cons')
+qed simp
 
 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
 by (induct n) auto
@@ -4148,11 +4129,11 @@
 
 lemma replicate_eq_replicate[simp]:
   "(replicate m x = replicate n y) \<longleftrightarrow> (m=n \<and> (m\<noteq>0 \<longrightarrow> x=y))"
-apply(induct m arbitrary: n)
- apply simp
-apply(induct_tac n)
-apply auto
-done
+proof (induct m arbitrary: n)
+  case (Suc m n)
+  then show ?case
+    by (induct n) auto
+qed simp
 
 lemma replicate_length_filter:
   "replicate (length (filter (\<lambda>y. x = y) xs)) x = filter (\<lambda>y. x = y) xs"
@@ -4239,10 +4220,7 @@
 lemma enumerate_simps [simp, code]:
   "enumerate n [] = []"
   "enumerate n (x # xs) = (n, x) # enumerate (Suc n) xs"
-apply (auto simp add: enumerate_eq_zip not_le)
-apply (cases "n < n + length xs")
- apply (auto simp add: upt_conv_Cons)
-done
+  by (simp_all add: enumerate_eq_zip upt_rec)
 
 lemma length_enumerate [simp]:
   "length (enumerate n xs) = length xs"
@@ -4288,12 +4266,7 @@
 
 lemma enumerate_append_eq:
   "enumerate n (xs @ ys) = enumerate n xs @ enumerate (n + length xs) ys"
-unfolding enumerate_eq_zip
-apply auto
- apply (subst zip_append [symmetric]) apply simp
- apply (subst upt_add_eq_append [symmetric])
- apply (simp_all add: ac_simps)
-done
+  by (simp add: enumerate_eq_zip add.assoc zip_append2)
 
 lemma enumerate_map_upt:
   "enumerate n (map f [n..<m]) = map (\<lambda>k. (k, f k)) [n..<m]"
@@ -4322,27 +4295,33 @@
 by(cases xs) simp_all
 
 lemma rotate_length01[simp]: "length xs \<le> 1 \<Longrightarrow> rotate n xs = xs"
-apply(induct n)
- apply simp
-apply (simp add:rotate_def)
-done
+  by (induct n) (simp_all add:rotate_def)
 
 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
 by (cases xs) simp_all
 
 lemma rotate_drop_take:
   "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
-apply(induct n)
- apply simp
-apply(simp add:rotate_def)
-apply(cases "xs = []")
- apply (simp)
-apply(case_tac "n mod length xs = 0")
- apply(simp add:mod_Suc)
- apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
-apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
-                take_hd_drop linorder_not_le)
-done
+proof (induct n)
+  case (Suc n)
+  show ?case
+  proof (cases "xs = []")
+    case False
+    then show ?thesis
+    proof (cases "n mod length xs = 0")
+      case True
+      then show ?thesis
+        apply (simp add: mod_Suc)
+        by (simp add: False Suc.hyps drop_Suc rotate1_hd_tl take_Suc)
+    next
+      case False
+      with \<open>xs \<noteq> []\<close> Suc
+      show ?thesis
+        by (simp add: rotate_def mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
+            take_hd_drop linorder_not_le)
+    qed
+  qed simp
+qed simp
 
 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
 by(simp add:rotate_drop_take)
@@ -4385,11 +4364,14 @@
     by(simp add:rotate_drop_take rev_drop rev_take)
 qed force
 
-lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
-apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
-apply(subgoal_tac "length xs \<noteq> 0")
- prefer 2 apply simp
-using mod_less_divisor[of "length xs" n] by arith
+lemma hd_rotate_conv_nth:
+  assumes "xs \<noteq> []" shows "hd(rotate n xs) = xs!(n mod length xs)"
+proof -
+  have "n mod length xs < length xs"
+    using assms by simp
+  then show ?thesis
+    by (metis drop_eq_Nil hd_append2 hd_drop_conv_nth leD rotate_drop_take)
+qed
 
 lemma rotate_append: "rotate (length l) (l @ q) = q @ l"
   by (induct l arbitrary: q) (auto simp add: rotate1_rotate_swap)
@@ -4408,14 +4390,13 @@
 by(simp add: nths_def length_filter_conv_card cong:conj_cong)
 
 lemma nths_shift_lemma_Suc:
-  "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
-   map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
-apply(induct xs arbitrary: "is")
- apply simp
-apply (case_tac "is")
- apply simp
-apply simp
-done
+  "map fst (filter (\<lambda>p. P(Suc(snd p))) (zip xs is)) =
+   map fst (filter (\<lambda>p. P(snd p)) (zip xs (map Suc is)))"
+proof (induct xs arbitrary: "is")
+  case (Cons x xs "is")
+  show ?case
+    by (cases "is") (auto simp add: Cons.hyps)
+qed simp
 
 lemma nths_shift_lemma:
   "map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [i..<i + length xs])) =
@@ -4424,26 +4405,26 @@
 
 lemma nths_append:
   "nths (l @ l') A = nths l A @ nths l' {j. j + length l \<in> A}"
-apply (unfold nths_def)
-apply (induct l' rule: rev_induct, simp)
-apply (simp add: upt_add_eq_append[of 0] nths_shift_lemma)
-apply (simp add: add.commute)
-done
+  unfolding nths_def
+proof (induct l' rule: rev_induct)
+  case (snoc x xs)
+  then show ?case
+    by (simp add: upt_add_eq_append[of 0] nths_shift_lemma add.commute)
+qed auto
 
 lemma nths_Cons:
   "nths (x # l) A = (if 0 \<in> A then [x] else []) @ nths l {j. Suc j \<in> A}"
-apply (induct l rule: rev_induct)
- apply (simp add: nths_def)
-apply (simp del: append_Cons add: append_Cons[symmetric] nths_append)
-done
+proof (induct l rule: rev_induct)
+  case (snoc x xs)
+  then show ?case
+    by (simp flip: append_Cons add: nths_append)
+qed (auto simp: nths_def)
 
 lemma nths_map: "nths (map f xs) I = map f (nths xs I)"
 by(induction xs arbitrary: I) (simp_all add: nths_Cons)
 
 lemma set_nths: "set(nths xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
-apply(induct xs arbitrary: I)
-apply(auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
-done
+  by (induct xs arbitrary: I) (auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
 
 lemma set_nths_subset: "set(nths xs I) \<subseteq> set xs"
 by(auto simp add:set_nths)
@@ -4792,8 +4773,7 @@
     show ?thesis
       unfolding transpose.simps \<open>i = Suc j\<close> nth_Cons_Suc "3.hyps"[OF j_less]
       apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric])
-      apply (rule list.exhaust)
-      by auto
+      by (simp add: nth_tl)
   qed
 qed simp_all
 
@@ -4917,11 +4897,7 @@
 qed
 
 lemma infinite_UNIV_listI: "\<not> finite(UNIV::'a list set)"
-apply (rule notI)
-apply (drule finite_maxlen)
-apply clarsimp
-apply (erule_tac x = "replicate n undefined" in allE)
-by simp
+  by (metis UNIV_I finite_maxlen length_replicate less_irrefl)
 
 
 subsection \<open>Sorting\<close>
@@ -4936,10 +4912,11 @@
 by(simp)
 
 lemma sorted_wrt2: "transp P \<Longrightarrow> sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))"
-apply(induction zs arbitrary: x y)
-apply(auto dest: transpD)
-apply (meson transpD)
-done
+proof (induction zs arbitrary: x y)
+  case (Cons z zs)
+  then show ?case
+    by simp (meson transpD)+
+qed auto
 
 lemmas sorted_wrt2_simps = sorted_wrt1 sorted_wrt2
 
@@ -4969,9 +4946,7 @@
 
 lemma sorted_wrt_iff_nth_less:
   "sorted_wrt P xs = (\<forall>i j. i < j \<longrightarrow> j < length xs \<longrightarrow> P (xs ! i) (xs ! j))"
-apply(induction xs)
-apply(auto simp add: in_set_conv_nth Ball_def nth_Cons split: nat.split)
-done
+  by (induction xs) (auto simp add: in_set_conv_nth Ball_def nth_Cons split: nat.split)
 
 lemma sorted_wrt_nth_less:
   "\<lbrakk> sorted_wrt P xs; i < j; j < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) (xs ! j)"
@@ -4981,10 +4956,11 @@
 by(induction n) (auto simp: sorted_wrt_append)
 
 lemma sorted_wrt_upto[simp]: "sorted_wrt (<) [i..j]"
-apply(induction i j rule: upto.induct)
-apply(subst upto.simps)
-apply(simp)
-done
+proof(induct i j rule:upto.induct)
+  case (1 i j)
+  from this show ?case
+    unfolding upto.simps[of i j] by auto
+qed
 
 text \<open>Each element is greater or equal to its index:\<close>
 
@@ -5313,12 +5289,13 @@
 qed
 
 lemma finite_sorted_distinct_unique:
-shows "finite A \<Longrightarrow> \<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
-apply(drule finite_distinct_list)
-apply clarify
-apply(rule_tac a="sort xs" in ex1I)
-apply (auto simp: sorted_distinct_set_unique)
-done
+  assumes "finite A" shows "\<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
+proof -
+  obtain xs where "distinct xs" "A = set xs"
+    using finite_distinct_list [OF assms] by metis
+  then show ?thesis
+    by (rule_tac a="sort xs" in ex1I) (auto simp: sorted_distinct_set_unique)
+qed
 
 lemma insort_insert_key_triv:
   "f x \<in> f ` set xs \<Longrightarrow> insort_insert_key f x xs = xs"
@@ -5741,12 +5718,12 @@
   | insert:  "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
 
 lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
-apply (rule iffI)
- apply (induct set: ListMem)
-  apply auto
-apply (induct xs)
- apply (auto intro: ListMem.intros)
-done
+proof
+  show "ListMem x xs \<Longrightarrow> x \<in> set xs"
+    by (induct set: ListMem) auto
+  show "x \<in> set xs \<Longrightarrow> ListMem x xs"
+    by (induct xs) (auto intro: ListMem.intros)
+qed
 
 
 subsubsection \<open>Lists as Cartesian products\<close>
@@ -5789,20 +5766,23 @@
 "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
         \<comment> \<open>Compares lists by their length and then lexicographically\<close>
 
-lemma wf_lexn: "wf r ==> wf (lexn r n)"
-apply (induct n, simp, simp)
-apply(rule wf_subset)
- prefer 2 apply (rule Int_lower1)
-apply(rule wf_map_prod_image)
- prefer 2 apply (rule inj_onI, auto)
-done
+lemma wf_lexn: assumes "wf r" shows "wf (lexn r n)"
+proof (induct n)
+  case (Suc n)
+  have inj: "inj (\<lambda>(x, xs). x # xs)"
+    using assms by (auto simp: inj_on_def)
+  have wf: "wf (map_prod (\<lambda>(x, xs). x # xs) (\<lambda>(x, xs). x # xs) ` (r <*lex*> lexn r n))"
+    by (simp add: Suc.hyps assms wf_lex_prod wf_map_prod_image [OF _ inj])
+  then show ?case
+    by (rule wf_subset) auto
+qed auto
 
 lemma lexn_length:
   "(xs, ys) \<in> lexn r n \<Longrightarrow> length xs = n \<and> length ys = n"
 by (induct n arbitrary: xs ys) auto
 
 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
-  apply (unfold lex_def)
+  unfolding lex_def
   apply (rule wf_UN)
    apply (simp add: wf_lexn)
   apply (metis DomainE Int_emptyI RangeE lexn_length)
@@ -5905,14 +5885,12 @@
 by (simp add:lex_conv)
 
 lemma Cons_in_lex [simp]:
-    "((x # xs, y # ys) \<in> lex r) =
+  "((x # xs, y # ys) \<in> lex r) =
       ((x, y) \<in> r \<and> length xs = length ys \<or> x = y \<and> (xs, ys) \<in> lex r)"
-apply (simp add: lex_conv)
-apply (rule iffI)
- prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
-apply (case_tac xys, simp, simp)
-apply blast
-  done
+  apply (simp add: lex_conv)
+  apply (rule iffI)
+   prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
+  by (metis hd_append append_Nil list.sel(1) list.sel(3) tl_append2)
 
 lemma lex_append_rightI:
   "(xs, ys) \<in> lex r \<Longrightarrow> length vs = length us \<Longrightarrow> (xs @ us, ys @ vs) \<in> lex r"
@@ -5960,12 +5938,13 @@
 by (unfold lexord_def, induct_tac x, auto)
 
 lemma lexord_cons_cons[simp]:
-     "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r \<or> (a = b \<and> (x,y)\<in> lexord r))"
-  apply (unfold lexord_def, safe, simp_all)
-  apply (case_tac u, simp, simp)
-  apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
-  apply (erule_tac x="b # u" in allE)
-  by force
+  "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r \<or> (a = b \<and> (x,y)\<in> lexord r))"
+  unfolding lexord_def
+  apply (safe, simp_all)
+     apply (metis hd_append list.sel(1))
+    apply (metis hd_append list.sel(1) list.sel(3) tl_append2)
+   apply blast
+  by (meson Cons_eq_appendI)
 
 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
 
@@ -5989,24 +5968,17 @@
      (\<exists>i. i < min(length x)(length y) \<and> take i x = take i y \<and> (x!i,y!i) \<in> r))"
   apply (unfold lexord_def Let_def, clarsimp)
   apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
+  apply (metis Cons_nth_drop_Suc append_eq_conv_conj drop_all list.simps(3) not_le)
   apply auto
-  apply (rule_tac x="hd (drop (length x) y)" in exI)
-  apply (rule_tac x="tl (drop (length x) y)" in exI)
-  apply (erule subst, simp add: min_def)
   apply (rule_tac x ="length u" in exI, simp)
-  apply (rule_tac x ="take i x" in exI)
-  apply (rule_tac x ="x ! i" in exI)
-  apply (rule_tac x ="y ! i" in exI, safe)
-  apply (rule_tac x="drop (Suc i) x" in exI)
-  apply (drule sym, simp add: Cons_nth_drop_Suc)
-  apply (rule_tac x="drop (Suc i) y" in exI)
-  by (simp add: Cons_nth_drop_Suc)
+  by (metis id_take_nth_drop)
 
 \<comment> \<open>lexord is extension of partial ordering List.lex\<close>
 lemma lexord_lex: "(x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
-  apply (rule_tac x = y in spec)
-  apply (induct_tac x, clarsimp)
-  by (clarify, case_tac x, simp, force)
+proof (induction x arbitrary: y)
+  case (Cons a x y) then show ?case
+    by (cases y) (force+)
+qed auto
 
 lemma lexord_irreflexive: "\<forall>x. (x,x) \<notin> r \<Longrightarrow> (xs,xs) \<notin> lexord r"
 by (induct xs) auto
@@ -6049,12 +6021,15 @@
 lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
 by (rule transI, drule lexord_trans, blast)
 
-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"
-  apply (rule_tac x = y in spec)
-  apply (induct_tac x, rule allI)
-  apply (case_tac x, simp, simp)
-  apply (rule allI, case_tac x, simp, simp)
-  by blast
+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"
+proof (induction x arbitrary: y)
+  case Nil
+  then show ?case
+    by (metis lexord_Nil_left list.exhaust)
+next
+  case (Cons a x y) then show ?case
+    by (cases y) (force+)
+qed 
 
 lemma lexord_irrefl:
   "irrefl R \<Longrightarrow> irrefl (lexord R)"
@@ -6220,27 +6195,17 @@
 lemma lexordp_eq_trans:
   assumes "lexordp_eq xs ys" and "lexordp_eq ys zs"
   shows "lexordp_eq xs zs"
-using assms
-apply(induct arbitrary: zs)
-apply(case_tac [2-3] zs)
-apply auto
-done
+  using assms
+  by (induct arbitrary: zs) (case_tac zs; auto)+
 
 lemma lexordp_trans:
   assumes "lexordp xs ys" "lexordp ys zs"
   shows "lexordp xs zs"
-using assms
-apply(induct arbitrary: zs)
-apply(case_tac [2-3] zs)
-apply auto
-done
+  using assms
+  by (induct arbitrary: zs) (case_tac zs; auto)+
 
 lemma lexordp_linear: "lexordp xs ys \<or> xs = ys \<or> lexordp ys xs"
-proof(induct xs arbitrary: ys)
-  case Nil thus ?case by(cases ys) simp_all
-next
-  case Cons thus ?case by(cases ys) auto
-qed
+  by(induct xs arbitrary: ys; case_tac ys; fastforce)
 
 lemma lexordp_conv_lexordp_eq: "lexordp xs ys \<longleftrightarrow> lexordp_eq xs ys \<and> \<not> lexordp_eq ys xs"
   (is "?lhs \<longleftrightarrow> ?rhs")
@@ -6258,13 +6223,11 @@
 by(auto simp add: lexordp_conv_lexordp_eq lexordp_eq_refl dest: lexordp_eq_antisym)
 
 lemma lexordp_eq_linear: "lexordp_eq xs ys \<or> lexordp_eq ys xs"
-apply(induct xs arbitrary: ys)
-apply(case_tac [!] ys)
-apply auto
-done
+  by (induct xs arbitrary: ys) (case_tac ys; auto)+
 
 lemma lexordp_linorder: "class.linorder lexordp_eq lexordp"
-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)
+  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)
 
 end
 
@@ -6402,17 +6365,20 @@
 apply (induct arbitrary: xs set: Wellfounded.acc)
 apply (erule thin_rl)
 apply (erule acc_induct)
-apply (rule accI)
+  apply (rule accI)
 apply (blast)
 done
 
 lemma lists_accD: "xs \<in> lists (Wellfounded.acc r) \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r)"
-apply (induct set: lists)
- apply (rule accI)
- apply simp
-apply (rule accI)
-apply (fast dest: acc_downward)
-done
+proof (induct set: lists)
+  case Nil
+  then show ?case
+    by (meson acc.intros not_listrel1_Nil)
+next
+  case (Cons a l)
+  then show ?case
+    by blast
+qed
 
 lemma lists_accI: "xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> xs \<in> lists (Wellfounded.acc r)"
 apply (induct set: Wellfounded.acc)
@@ -6459,10 +6425,7 @@
 
 
 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
-apply clarify
-apply (erule listrel.induct)
-apply (blast intro: listrel.intros)+
-done
+  by (meson listrel_iff_nth subrelI subset_eq)
 
 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
 apply clarify
@@ -6477,10 +6440,7 @@
 done
 
 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)"
-apply (auto simp add: sym_def)
-apply (erule listrel.induct)
-apply (blast intro: listrel.intros)+
-done
+  by (simp add: listrel_iff_nth sym_def)
 
 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)"
 apply (simp add: trans_def)
@@ -7365,10 +7325,7 @@
   "(rel_set A ===> rel_set (list_all2 A) ===> rel_set (list_all2 A))
     set_Cons set_Cons"
   unfolding rel_fun_def rel_set_def set_Cons_def
-  apply safe
-  apply (simp add: list_all2_Cons1, fast)
-  apply (simp add: list_all2_Cons2, fast)
-  done
+  by (fastforce simp add: list_all2_Cons1 list_all2_Cons2)
 
 lemma listset_transfer [transfer_rule]:
   "(list_all2 (rel_set A) ===> rel_set (list_all2 A)) listset listset"