# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1584897676 0
# Node ID 4b1021677f151da54a21c2a0375004f40a948908
# Parent  24b68a932f26f71188dbc6b524f6118b923ad92a
tidying up some horrible proofs

diff -r 24b68a932f26 -r 4b1021677f15 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/HOL/List.thy	Sun Mar 22 17:21:16 2020 +0000
@@ -853,7 +853,7 @@
   "(Suc n \<le> length xs) = (\<exists>x ys. xs = x # ys \<and> n \<le> length ys)"
 by (metis Suc_le_D[of n] Suc_le_mono[of n] Suc_length_conv[of _ xs])
 
-lemma impossible_Cons: "length xs \<le> length ys ==> xs = x # ys = False"
+lemma impossible_Cons: "length xs \<le> length ys \<Longrightarrow> xs = x # ys = False"
 by (induct xs) auto
 
 lemma list_induct2 [consumes 1, case_names Nil Cons]:
@@ -972,7 +972,7 @@
 
 lemma append_eq_append_conv [simp]:
   "length xs = length ys \<or> length us = length vs
-  ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
+  \<Longrightarrow> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
   by (induct xs arbitrary: ys; case_tac ys; force)
 
 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
@@ -998,19 +998,19 @@
 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
 using append_same_eq [of "[]"] by auto
 
-lemma hd_Cons_tl: "xs \<noteq> [] ==> hd xs # tl xs = xs"
+lemma hd_Cons_tl: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs"
   by (fact list.collapse)
 
 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
 by (induct xs) auto
 
-lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs"
+lemma hd_append2 [simp]: "xs \<noteq> [] \<Longrightarrow> hd (xs @ ys) = hd xs"
 by (simp add: hd_append split: list.split)
 
 lemma tl_append: "tl (xs @ ys) = (case xs of [] \<Rightarrow> tl ys | z#zs \<Rightarrow> zs @ ys)"
 by (simp split: list.split)
 
-lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys"
+lemma tl_append2 [simp]: "xs \<noteq> [] \<Longrightarrow> tl (xs @ ys) = tl xs @ ys"
 by (simp add: tl_append split: list.split)
 
 
@@ -1031,16 +1031,14 @@
 
 text \<open>Trivial rules for solving \<open>@\<close>-equations automatically.\<close>
 
-lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
-by simp
-
-lemma Cons_eq_appendI:
-"[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"
-by (drule sym) simp
-
-lemma append_eq_appendI:
-"[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"
-by (drule sym) simp
+lemma eq_Nil_appendI: "xs = ys \<Longrightarrow> xs = [] @ ys"
+  by simp
+
+lemma Cons_eq_appendI: "\<lbrakk>x # xs1 = ys; xs = xs1 @ zs\<rbrakk> \<Longrightarrow> x # xs = ys @ zs"
+  by auto
+
+lemma append_eq_appendI: "\<lbrakk>xs @ xs1 = zs; ys = xs1 @ us\<rbrakk> \<Longrightarrow> xs @ ys = zs @ us"
+  by auto
 
 
 text \<open>
@@ -1100,7 +1098,7 @@
 lemma map_tl: "map f (tl xs) = tl (map f xs)"
 by (cases xs) simp_all
 
-lemma map_ext: "(\<And>x. x \<in> set xs \<longrightarrow> f x = g x) ==> map f xs = map g xs"
+lemma map_ext: "(\<And>x. x \<in> set xs \<longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g xs"
 by (induct xs) simp_all
 
 lemma map_ident [simp]: "map (\<lambda>x. x) = (\<lambda>xs. xs)"
@@ -1175,16 +1173,16 @@
 by(blast dest:map_inj_on)
 
 lemma map_injective:
-  "map f xs = map f ys ==> inj f ==> xs = ys"
+  "map f xs = map f ys \<Longrightarrow> inj f \<Longrightarrow> xs = ys"
 by (induct ys arbitrary: xs) (auto dest!:injD)
 
 lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
 by(blast dest:map_injective)
 
-lemma inj_mapI: "inj f ==> inj (map f)"
+lemma inj_mapI: "inj f \<Longrightarrow> inj (map f)"
 by (iprover dest: map_injective injD intro: inj_onI)
 
-lemma inj_mapD: "inj (map f) ==> inj f"
+lemma inj_mapD: "inj (map f) \<Longrightarrow> inj f"
   by (metis (no_types, hide_lams) injI list.inject list.simps(9) the_inv_f_f)
 
 lemma inj_map[iff]: "inj (map f) = inj f"
@@ -1260,13 +1258,16 @@
 by(simp add:inj_on_def)
 
 lemma rev_induct [case_names Nil snoc]:
-  "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
-apply(simplesubst rev_rev_ident[symmetric])
-apply(rule_tac list = "rev xs" in list.induct, simp_all)
-done
+  assumes "P []" and "\<And>x xs. P xs \<Longrightarrow> P (xs @ [x])"
+  shows "P xs"
+proof -
+  have "P (rev (rev xs))"
+    by (rule_tac list = "rev xs" in list.induct, simp_all add: assms)
+  then show ?thesis by simp
+qed
 
 lemma rev_exhaust [case_names Nil snoc]:
-  "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P"
+  "(xs = [] \<Longrightarrow> P) \<Longrightarrow>(\<And>ys y. xs = ys @ [y] \<Longrightarrow> P) \<Longrightarrow> P"
 by (induct xs rule: rev_induct) auto
 
 lemmas rev_cases = rev_exhaust
@@ -1475,10 +1476,10 @@
   "length(filter P xs) + length(filter (\<lambda>x. \<not>P x) xs) = length xs"
 by(induct xs) simp_all
 
-lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
+lemma filter_True [simp]: "\<forall>x \<in> set xs. P x \<Longrightarrow> filter P xs = xs"
 by (induct xs) auto
 
-lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
+lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x \<Longrightarrow> filter P xs = []"
 by (induct xs) auto
 
 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)"
@@ -1664,13 +1665,13 @@
 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
   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)"
+lemma concat_eq_concat_iff: "\<forall>(x, y) \<in> set (zip xs ys). length x = length y \<Longrightarrow> length xs = length ys \<Longrightarrow> (concat xs = concat ys) = (xs = ys)"
 proof (induct xs arbitrary: ys)
   case (Cons x xs ys)
   thus ?case by (cases ys) auto
 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"
+lemma concat_injective: "concat xs = concat ys \<Longrightarrow> length xs = length ys \<Longrightarrow> \<forall>(x, y) \<in> set (zip xs ys). length x = length y \<Longrightarrow> xs = ys"
   by (simp add: concat_eq_concat_iff)
 
 lemma concat_eq_appendD:
@@ -1725,7 +1726,7 @@
 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
   by (induct xs) auto
 
-lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
+lemma nth_map [simp]: "n < length xs \<Longrightarrow> (map f xs)!n = f(xs!n)"
 proof (induct xs arbitrary: n)
   case (Cons x xs)
   then show ?case
@@ -1856,13 +1857,13 @@
   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)"
+  "i < length xs\<Longrightarrow> (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"
+lemma nth_list_update_eq [simp]: "i < length xs \<Longrightarrow> (xs[i:=x])!i = x"
   by (simp add: nth_list_update)
 
-lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
+lemma nth_list_update_neq [simp]: "i \<noteq> j \<Longrightarrow> xs[i:=x]!j = xs!j"
   by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
 
 lemma list_update_id[simp]: "xs[i := xs!i] = xs"
@@ -1879,7 +1880,7 @@
   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)"
+  "i < length xs \<Longrightarrow> (xs[i := x] = xs) = (xs!i = x)"
   by (induct xs arbitrary: i) (auto split: nat.split)
 
 lemma list_update_append1:
@@ -2105,10 +2106,10 @@
 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
   by (induct n arbitrary: xs) (auto, case_tac xs, auto)
 
-lemma take_all [simp]: "length xs \<le> n ==> take n xs = xs"
+lemma take_all [simp]: "length xs \<le> n \<Longrightarrow> take n xs = xs"
   by (induct n arbitrary: xs) (auto, case_tac xs, auto)
 
-lemma drop_all [simp]: "length xs \<le> n ==> drop n xs = []"
+lemma drop_all [simp]: "length xs \<le> n \<Longrightarrow> drop n xs = []"
   by (induct n arbitrary: xs) (auto, case_tac xs, auto)
 
 lemma take_append [simp]:
@@ -2206,7 +2207,7 @@
 lemma take_rev: "take n (rev xs) = rev (drop (length xs - n) xs)"
   by (cases "length xs < n") (auto simp: rev_drop)
 
-lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
+lemma nth_take [simp]: "i < n \<Longrightarrow> (take n xs)!i = xs!i"
 proof (induct xs arbitrary: i n)
   case Nil
   then show ?case by simp
@@ -2216,7 +2217,7 @@
 qed
 
 lemma nth_drop [simp]:
-  "n \<le> length xs ==> (drop n xs)!i = xs!(n + i)"
+  "n \<le> length xs \<Longrightarrow> (drop n xs)!i = xs!(n + i)"
 proof (induct n arbitrary: xs)
   case 0
   then show ?case by simp
@@ -2226,13 +2227,13 @@
 qed
 
 lemma butlast_take:
-  "n \<le> length xs ==> butlast (take n xs) = take (n - 1) xs"
+  "n \<le> length xs \<Longrightarrow> butlast (take n xs) = take (n - 1) xs"
   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)
 
-lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
+lemma take_butlast: "n < length xs \<Longrightarrow> take n (butlast xs) = take n xs"
   by (simp add: butlast_conv_take min.absorb1)
 
 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
@@ -2390,7 +2391,7 @@
   by (induct xs) auto
 
 lemma dropWhile_append2 [simp]:
-  "(\<And>x. x \<in> set xs \<Longrightarrow> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
+  "(\<And>x. x \<in> set xs \<Longrightarrow> P(x)) \<Longrightarrow> dropWhile P (xs @ ys) = dropWhile P ys"
   by (induct xs) auto
 
 lemma dropWhile_append3:
@@ -2419,10 +2420,10 @@
   "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys \<and> \<not> P y)"
   by(induct xs, auto)
 
-lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"
+lemma distinct_takeWhile[simp]: "distinct xs \<Longrightarrow> distinct (takeWhile P xs)"
   by (induct xs) (auto dest: set_takeWhileD)
 
-lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
+lemma distinct_dropWhile[simp]: "distinct xs \<Longrightarrow> distinct (dropWhile P xs)"
   by (induct xs) auto
 
 lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \<circ> f) xs)"
@@ -2582,12 +2583,12 @@
   by (induct xs ys rule:list_induct2') auto
 
 lemma zip_append [simp]:
-  "[| length xs = length us |] ==>
+  "\<lbrakk>length xs = length us\<rbrakk> \<Longrightarrow>
   zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
   by (simp add: zip_append1)
 
 lemma zip_rev:
-  "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
+  "length xs = length ys \<Longrightarrow> zip (rev xs) (rev ys) = rev (zip xs ys)"
   by (induct rule:list_induct2, simp_all)
 
 lemma zip_map_map:
@@ -2622,7 +2623,7 @@
   by(induct xs) auto
 
 lemma nth_zip [simp]:
-  "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
+  "\<lbrakk>i < length xs; i < length ys\<rbrakk> \<Longrightarrow> (zip xs ys)!i = (xs!i, ys!i)"
 proof (induct ys arbitrary: i xs)
   case (Cons y ys)
   then show ?case
@@ -2804,7 +2805,7 @@
 subsubsection \<open>\<^const>\<open>list_all2\<close>\<close>
 
 lemma list_all2_lengthD [intro?]:
-  "list_all2 P xs ys ==> length xs = length ys"
+  "list_all2 P xs ys \<Longrightarrow> length xs = length ys"
   by (simp add: list_all2_iff)
 
 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
@@ -2892,8 +2893,8 @@
   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"
+  assumes tr: "!!a b c. P1 a b \<Longrightarrow> P2 b c \<Longrightarrow> P3 a c"
+  shows "!!bs cs. list_all2 P1 as bs \<Longrightarrow> list_all2 P2 bs cs \<Longrightarrow> list_all2 P3 as 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"
@@ -3224,7 +3225,7 @@
 
 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] = []"
+lemma upt_conv_Nil [simp]: "j \<le> i \<Longrightarrow> [i..<j] = []"
   by (subst upt_rec) simp
 
 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j \<le> i)"
@@ -3238,11 +3239,11 @@
     by (simp add: upt_rec)
 qed simp
 
-lemma upt_Suc_append: "i \<le> j ==> [i..<(Suc j)] = [i..<j]@[j]"
+lemma upt_Suc_append: "i \<le> j \<Longrightarrow> [i..<(Suc j)] = [i..<j]@[j]"
   \<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]"
+lemma upt_conv_Cons: "i < j \<Longrightarrow> [i..<j] = i # [Suc i..<j]"
   by (simp add: upt_rec)
 
 lemma upt_conv_Cons_Cons: \<comment> \<open>no precondition\<close>
@@ -3253,14 +3254,14 @@
   case True then show ?thesis by (simp add: upt_conv_Cons)
 qed
 
-lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
+lemma upt_add_eq_append: "i<=j \<Longrightarrow> [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
 
 lemma length_upt [simp]: "length [i..<j] = j - i"
   by (induct j) (auto simp add: Suc_diff_le)
 
-lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
+lemma nth_upt [simp]: "i + k < j \<Longrightarrow> [i..<j] ! k = i + k"
   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"
@@ -3272,7 +3273,7 @@
 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
   by(cases j)(auto simp: upt_Suc_append)
 
-lemma take_upt [simp]: "i+m \<le> n ==> take m [i..<n] = [i..<i+m]"
+lemma take_upt [simp]: "i+m \<le> n \<Longrightarrow> take m [i..<n] = [i..<i+m]"
 proof (induct m arbitrary: i)
   case (Suc m)
   then show ?case
@@ -3288,7 +3289,7 @@
 lemma map_add_upt: "map (\<lambda>i. i + n) [0..<m] = [n..<m + n]"
   by (induct m) simp_all
 
-lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
+lemma nth_map_upt: "i < n-m \<Longrightarrow> (map f [m..<n]) ! i = f(m+i)"
 proof (induct n m  arbitrary: i rule: diff_induct)
   case (3 x y)
   then show ?case
@@ -3324,7 +3325,7 @@
   \<Longrightarrow> xs = ys"
   by (simp add: list_all2_conv_all_nth nth_equalityI)
 
-lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
+lemma take_equalityI: "(\<forall>i. take i xs = take i ys) \<Longrightarrow> xs = ys"
 \<comment> \<open>The famous take-lemma.\<close>
   by (metis length_take min.commute order_refl take_all)
 
@@ -3403,10 +3404,11 @@
 qed
 
 lemma nth_upto[simp]: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k"
-  apply(induction i j arbitrary: k rule: upto.induct)
-apply(subst upto_rec1)
-apply(auto simp add: nth_Cons')
-done
+proof(induction i j arbitrary: k rule: upto.induct)
+  case (1 i j)
+  then show ?case
+    by (auto simp add: upto_rec1 [of i j] nth_Cons')
+qed
 
 lemma upto_split1:
   "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> [i..k] = [i..j-1] @ [j..k]"
@@ -3454,7 +3456,7 @@
 lemma distinct_remdups [iff]: "distinct (remdups xs)"
 by (induct xs) auto
 
-lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
+lemma distinct_remdups_id: "distinct xs \<Longrightarrow> remdups xs = xs"
 by (induct xs, auto)
 
 lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \<longleftrightarrow> distinct xs"
@@ -3491,17 +3493,18 @@
   "distinct (map f xs) \<Longrightarrow> distinct (map f (filter P xs))"
 by (induct xs) auto
 
-lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
+lemma distinct_filter [simp]: "distinct xs \<Longrightarrow> distinct (filter P xs)"
 by (induct xs) auto
 
 lemma distinct_upt[simp]: "distinct[i..<j]"
 by (induct j) auto
 
 lemma distinct_upto[simp]: "distinct[i..j]"
-apply(induct i j rule:upto.induct)
-apply(subst upto.simps)
-apply(simp)
-done
+proof (induction i j rule: upto.induct)
+  case (1 i j)
+  then show ?case
+    by (simp add: upto.simps [of i])
+qed
 
 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
 proof (induct xs arbitrary: i)
@@ -3531,10 +3534,10 @@
       by auto
   next
     case False
+    have "set (take i xs) \<inter> set (drop (Suc i) xs) = {}"
+      by (metis True d disjoint_insert(1) distinct_append id_take_nth_drop list.set(2))
     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))
+      using d False anot \<open>i < length xs\<close> by (simp add: upd_conv_take_nth_drop)
   qed
 next
   case False with d show ?thesis by auto
@@ -3580,21 +3583,20 @@
   set(xs[n := x]) = insert x (set xs - {xs!n})"
 by(auto simp: set_eq_iff in_set_conv_nth nth_list_update nth_eq_iff_index_eq)
 
-lemma distinct_swap[simp]: "\<lbrakk> i < size xs; j < size xs \<rbrakk> \<Longrightarrow>
+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 safe
-apply metis+
-done
+  apply (safe; metis)
+  done
 
 lemma set_swap[simp]:
   "\<lbrakk> i < size xs; j < size xs \<rbrakk> \<Longrightarrow> set(xs[i := xs!j, j := xs!i]) = set xs"
 by(simp add: set_conv_nth nth_list_update) metis
 
-lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
+lemma distinct_card: "distinct xs \<Longrightarrow> card (set xs) = size xs"
 by (induct xs) auto
 
-lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
+lemma card_distinct: "card (set xs) = size xs \<Longrightarrow> distinct xs"
 proof (induct xs)
   case (Cons x xs)
   show ?case
@@ -3822,18 +3824,12 @@
           using f_mono by (simp add: mono_iff_le_Suc)
       next
         have "?f' ` {0 ..< length (x1 # xs)} = f ` {Suc 0 ..< length (x1 # x2 # xs)}"
-          apply safe
-           apply fastforce
-          subgoal for \<dots> x by (cases x) auto
-          done
+          using less_Suc_eq_0_disj by auto
         also have "\<dots> = f ` {0 ..< length (x1 # x2 # xs)}"
         proof -
           have "f 0 = f (Suc 0)" using \<open>x1 = x2\<close> f_nth[of 0] by simp
           then show ?thesis
-            apply safe
-             apply fastforce
-            subgoal for \<dots> x by (cases x) auto
-            done
+            using less_Suc_eq_0_disj by auto
         qed
         also have "\<dots> = {0 ..< length ys}" by fact
         finally show  "?f' ` {0 ..< length (x1 # xs)} = {0 ..< length ys}" .
@@ -3842,7 +3838,7 @@
     next
       assume "x1 \<noteq> x2"
 
-      have "2 \<le> length ys"
+      have two: "Suc (Suc 0) \<le> length ys"
       proof -
         have "2 = card {f 0, f 1}" using \<open>x1 \<noteq> x2\<close> f_nth[of 0] by auto
         also have "\<dots> \<le> card (f ` {0..< length (x1 # x2 # xs)})"
@@ -3862,26 +3858,18 @@
         then have "Suc 0 \<noteq> f i" for i using \<open>f 0 = 0\<close>
           by (cases i) fastforce+
         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
+        then show False using f_img two 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)
-         apply (rename_tac [2] ys', case_tac [2] ys')
-          apply (auto simp: \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>)
-        done
+        using two f_nth[of 0] f_nth[of 1]
+        by (auto simp: Suc_le_length_iff  \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>)
+
+      have Suc0_le_f_Suc: "Suc 0 \<le> f (Suc i)" for i
+        by (metis Suc_le_mono \<open>f (Suc 0) = Suc 0\<close> f_mono le0 mono_def)
 
       define f' where "f' x = f (Suc x) - 1" for x
-
-      { fix i
-        have "Suc 0 \<le> f (Suc 0)" using f_nth[of 0] \<open>x1 \<noteq> x2\<close> \<open>f 0 = 0\<close>  by auto
-        also have "\<dots> \<le> f (Suc i)" using f_mono by (rule monoD) arith
-        finally have "Suc 0 \<le> f (Suc i)" .
-      } note Suc0_le_f_Suc = this
-
-      { fix i have "f (Suc i) = Suc (f' i)"
+      have f_Suc: "f (Suc i) = Suc (f' i)" for i
           using Suc0_le_f_Suc[of i] by (auto simp: f'_def)
-      } note f_Suc = this
 
       have "remdups_adj (x2 # xs) = (x2 # ys')"
       proof (intro "3.hyps" exI conjI impI allI)
@@ -3904,15 +3892,15 @@
 qed
 
 lemma hd_remdups_adj[simp]: "hd (remdups_adj xs) = hd xs"
-by (induction xs rule: remdups_adj.induct) simp_all
+  by (induction xs rule: remdups_adj.induct) simp_all
 
 lemma remdups_adj_Cons: "remdups_adj (x # xs) =
   (case remdups_adj xs of [] \<Rightarrow> [x] | y # xs \<Rightarrow> if x = y then y # xs else x # y # xs)"
-by (induct xs arbitrary: x) (auto split: list.splits)
+  by (induct xs arbitrary: x) (auto split: list.splits)
 
 lemma remdups_adj_append_two:
   "remdups_adj (xs @ [x,y]) = remdups_adj (xs @ [x]) @ (if x = y then [] else [y])"
-by (induct xs rule: remdups_adj.induct, simp_all)
+  by (induct xs rule: remdups_adj.induct, simp_all)
 
 lemma remdups_adj_adjacent:
   "Suc i < length (remdups_adj xs) \<Longrightarrow> remdups_adj xs ! i \<noteq> remdups_adj xs ! Suc i"
@@ -4059,8 +4047,8 @@
 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)
+    using sum.remove [of X x "count_list xs"]
+    by (auto simp: sum.If_cases simp flip: diff_eq)
 qed simp
 
 
@@ -4237,16 +4225,16 @@
   "filter P (replicate n x) = (if P x then replicate n x else [])"
 by(induct n) auto
 
-lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
+lemma hd_replicate [simp]: "n \<noteq> 0 \<Longrightarrow> hd (replicate n x) = x"
 by (induct n) auto
 
 lemma tl_replicate [simp]: "tl (replicate n x) = replicate (n - 1) x"
 by (induct n) auto
 
-lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
+lemma last_replicate [simp]: "n \<noteq> 0 \<Longrightarrow> last (replicate n x) = x"
 by (atomize (full), induct n) auto
 
-lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
+lemma nth_replicate[simp]: "i < n \<Longrightarrow> (replicate n x)!i = x"
 by (induct n arbitrary: i)(auto simp: nth_Cons split: nat.split)
 
 text\<open>Courtesy of Matthias Daum (2 lemmas):\<close>
@@ -4273,7 +4261,7 @@
 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
 by (induct n) auto
 
-lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"
+lemma set_replicate [simp]: "n \<noteq> 0 \<Longrightarrow> set (replicate n x) = {x}"
 by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
 
 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
@@ -4495,8 +4483,7 @@
     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)
+        by (auto simp add: mod_Suc False Suc.hyps drop_Suc rotate1_hd_tl take_Suc Suc_length_conv)
     next
       case False
       with \<open>xs \<noteq> []\<close> Suc
@@ -4508,37 +4495,37 @@
 qed simp
 
 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
-by(simp add:rotate_drop_take)
+  by(simp add:rotate_drop_take)
 
 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
-by(simp add:rotate_drop_take)
+  by(simp add:rotate_drop_take)
 
 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
-by (cases xs) simp_all
+  by (cases xs) simp_all
 
 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
-by (induct n arbitrary: xs) (simp_all add:rotate_def)
+  by (induct n arbitrary: xs) (simp_all add:rotate_def)
 
 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
-by (cases xs) auto
+  by (cases xs) auto
 
 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
-by (induct n) (simp_all add:rotate_def)
+  by (induct n) (simp_all add:rotate_def)
 
 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
-by(simp add:rotate_drop_take take_map drop_map)
+  by(simp add:rotate_drop_take take_map drop_map)
 
 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
-by (cases xs) auto
+  by (cases xs) auto
 
 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
-by (induct n) (simp_all add:rotate_def)
+  by (induct n) (simp_all add:rotate_def)
 
 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
-by (cases xs) auto
+  by (cases xs) auto
 
 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
-by (induct n) (simp_all add:rotate_def)
+  by (induct n) (simp_all add:rotate_def)
 
 lemma rotate_rev:
   "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
@@ -4564,21 +4551,20 @@
 subsubsection \<open>\<^const>\<open>nths\<close> --- a generalization of \<^const>\<open>nth\<close> to sets\<close>
 
 lemma nths_empty [simp]: "nths xs {} = []"
-by (auto simp add: nths_def)
+  by (auto simp add: nths_def)
 
 lemma nths_nil [simp]: "nths [] A = []"
-by (auto simp add: nths_def)
+  by (auto simp add: nths_def)
 
 lemma nths_all: "\<forall>i < length xs. i \<in> I \<Longrightarrow> nths xs I = xs"
 apply (simp add: nths_def)
 apply (subst filter_True)
- apply (clarsimp simp: in_set_zip subset_iff)
-apply simp
+ apply (auto simp: in_set_zip subset_iff)
 done
 
 lemma length_nths:
   "length (nths xs I) = card{i. i < length xs \<and> i \<in> I}"
-by(simp add: nths_def length_filter_conv_card cong:conj_cong)
+  by(simp add: nths_def length_filter_conv_card cong:conj_cong)
 
 lemma nths_shift_lemma_Suc:
   "map fst (filter (\<lambda>p. P(Suc(snd p))) (zip xs is)) =
@@ -4612,46 +4598,41 @@
 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)
+  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}"
-by (induct xs arbitrary: I) (auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
+  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)
+  by(auto simp add:set_nths)
 
 lemma notin_set_nthsI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(nths xs I)"
-by(auto simp add:set_nths)
+  by(auto simp add:set_nths)
 
 lemma in_set_nthsD: "x \<in> set(nths xs I) \<Longrightarrow> x \<in> set xs"
-by(auto simp add:set_nths)
+  by(auto simp add:set_nths)
 
 lemma nths_singleton [simp]: "nths [x] A = (if 0 \<in> A then [x] else [])"
-by (simp add: nths_Cons)
+  by (simp add: nths_Cons)
 
 lemma distinct_nthsI[simp]: "distinct xs \<Longrightarrow> distinct (nths xs I)"
-by (induct xs arbitrary: I) (auto simp: nths_Cons)
+  by (induct xs arbitrary: I) (auto simp: nths_Cons)
 
 lemma nths_upt_eq_take [simp]: "nths l {..<n} = take n l"
-by (induct l rule: rev_induct)
-   (simp_all split: nat_diff_split add: nths_append)
+  by (induct l rule: rev_induct) (simp_all split: nat_diff_split add: nths_append)
 
 lemma nths_nths: "nths (nths xs A) B = nths xs {i \<in> A. \<exists>j \<in> B. card {i' \<in> A. i' < i} = j}"
-apply(induction xs arbitrary: A B)
-apply(auto simp add: nths_Cons card_less_Suc card_less_Suc2)
-done
+  by (induction xs arbitrary: A B) (auto simp add: nths_Cons card_less_Suc card_less_Suc2)
 
 lemma drop_eq_nths: "drop n xs = nths xs {i. i \<ge> n}"
-apply(induction xs arbitrary: n)
-apply (auto simp add: nths_Cons nths_all drop_Cons' intro: arg_cong2[where f=nths, OF refl])
-done
+  by (induction xs arbitrary: n) (auto simp add: nths_Cons nths_all drop_Cons' intro: arg_cong2[where f=nths, OF refl])
 
 lemma nths_drop: "nths (drop n xs) I = nths xs ((+) n ` I)"
 by(force simp: drop_eq_nths nths_nths simp flip: atLeastLessThan_iff
          intro: arg_cong2[where f=nths, OF refl])
 
 lemma filter_eq_nths: "filter P xs = nths xs {i. i<length xs \<and> P(xs!i)}"
-by(induction xs) (auto simp: nths_Cons)
+  by(induction xs) (auto simp: nths_Cons)
 
 lemma filter_in_nths:
   "distinct xs \<Longrightarrow> filter (%x. x \<in> set (nths xs s)) xs = nths xs s"
@@ -4732,18 +4713,20 @@
 subsubsection \<open>\<^const>\<open>splice\<close>\<close>
 
 lemma splice_Nil2 [simp]: "splice xs [] = xs"
-by (cases xs) simp_all
+  by (cases xs) simp_all
 
 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
-by (induct xs ys rule: splice.induct) auto
+  by (induct xs ys rule: splice.induct) auto
 
 lemma split_Nil_iff[simp]: "splice xs ys = [] \<longleftrightarrow> xs = [] \<and> ys = []"
-by (induct xs ys rule: splice.induct) auto
+  by (induct xs ys rule: splice.induct) auto
 
 lemma splice_replicate[simp]: "splice (replicate m x) (replicate n x) = replicate (m+n) x"
-apply(induction "replicate m x" "replicate n x" arbitrary: m n rule: splice.induct)
-apply (auto simp add: Cons_replicate_eq dest: gr0_implies_Suc)
-done
+proof (induction "replicate m x" "replicate n x" arbitrary: m n rule: splice.induct)
+  case (2 x xs)
+  then show ?case 
+    by (auto simp add: Cons_replicate_eq dest: gr0_implies_Suc)
+qed auto
 
 subsubsection \<open>\<^const>\<open>shuffles\<close>\<close>
 
@@ -4768,7 +4751,7 @@
   by (induct xs ys rule: shuffles.induct) auto
 
 lemma splice_in_shuffles [simp, intro]: "splice xs ys \<in> shuffles xs ys"
-by (induction xs ys rule: splice.induct) (simp_all add: Cons_in_shuffles_iff shuffles_commutes)
+  by (induction xs ys rule: splice.induct) (simp_all add: Cons_in_shuffles_iff shuffles_commutes)
 
 lemma Nil_in_shufflesI: "xs = [] \<Longrightarrow> ys = [] \<Longrightarrow> [] \<in> shuffles xs ys"
   by simp
@@ -5001,13 +4984,13 @@
 subsubsection \<open>\<^const>\<open>min\<close> and \<^const>\<open>arg_min\<close>\<close>
 
 lemma min_list_Min: "xs \<noteq> [] \<Longrightarrow> min_list xs = Min (set xs)"
-by (induction xs rule: induct_list012)(auto)
+  by (induction xs rule: induct_list012)(auto)
 
 lemma f_arg_min_list_f: "xs \<noteq> [] \<Longrightarrow> f (arg_min_list f xs) = Min (f ` (set xs))"
-by(induction f xs rule: arg_min_list.induct) (auto simp: min_def intro!: antisym)
+  by(induction f xs rule: arg_min_list.induct) (auto simp: min_def intro!: antisym)
 
 lemma arg_min_list_in: "xs \<noteq> [] \<Longrightarrow> arg_min_list f xs \<in> set xs"
-by(induction xs rule: induct_list012) (auto simp: Let_def)
+  by(induction xs rule: induct_list012) (auto simp: Let_def)
 
 
 subsubsection \<open>(In)finiteness\<close>
@@ -5811,19 +5794,19 @@
 
 lemma sorted_list_of_set_empty:
   "sorted_list_of_set {} = []"
-by (fact sorted_list_of_set.empty)
+  by (fact sorted_list_of_set.empty)
 
 lemma sorted_list_of_set_insert [simp]:
   "finite A \<Longrightarrow> sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
-by (fact sorted_list_of_set.insert_remove)
+  by (fact sorted_list_of_set.insert_remove)
 
 lemma sorted_list_of_set_eq_Nil_iff [simp]:
   "finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
-by (auto simp: sorted_list_of_set.remove)
+  by (auto simp: sorted_list_of_set.remove)
 
 lemma set_sorted_list_of_set [simp]:
   "finite A \<Longrightarrow> set (sorted_list_of_set A) = A"
-by(induct A rule: finite_induct) (simp_all add: set_insort_key)
+  by(induct A rule: finite_induct) (simp_all add: set_insort_key)
 
 lemma sorted_sorted_list_of_set [simp]: "sorted (sorted_list_of_set A)"
 proof (cases "finite A")
@@ -5894,13 +5877,13 @@
   "listsp A []"
   "listsp A (x # xs)"
 
-lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
+lemma listsp_mono [mono]: "A \<le> B \<Longrightarrow> listsp A \<le> listsp B"
 by (rule predicate1I, erule listsp.induct, blast+)
 
 lemmas lists_mono = listsp_mono [to_set]
 
 lemma listsp_infI:
-  assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
+  assumes l: "listsp A l" shows "listsp B l \<Longrightarrow> listsp (inf A B) l" using l
 by induct blast+
 
 lemmas lists_IntI = listsp_infI [to_set]
@@ -5930,12 +5913,12 @@
 
 lemmas in_lists_conv_set [code_unfold] = in_listsp_conv_set [to_set]
 
-lemma in_listspD [dest!]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
+lemma in_listspD [dest!]: "listsp A xs \<Longrightarrow> \<forall>x\<in>set xs. A x"
 by (rule in_listsp_conv_set [THEN iffD1])
 
 lemmas in_listsD [dest!] = in_listspD [to_set]
 
-lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
+lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x \<Longrightarrow> listsp A xs"
 by (rule in_listsp_conv_set [THEN iffD2])
 
 lemmas in_listsI [intro!] = in_listspI [to_set]
@@ -6025,24 +6008,31 @@
 
 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)"
+  by (induct n arbitrary: xs ys) auto
+
+lemma wf_lex [intro!]: 
+  assumes "wf r" shows "wf (lex r)"
   unfolding lex_def
-  apply (rule wf_UN)
-   apply (simp add: wf_lexn)
-  apply (metis DomainE Int_emptyI RangeE lexn_length)
-  done
+proof (rule wf_UN)
+  show "wf (lexn r i)" for i
+    by (simp add: assms wf_lexn)
+  show "\<And>i j. lexn r i \<noteq> lexn r j \<Longrightarrow> Domain (lexn r i) \<inter> Range (lexn r j) = {}"
+    by (metis DomainE Int_emptyI RangeE lexn_length)
+qed
+
 
 lemma lexn_conv:
   "lexn r n =
     {(xs,ys). length xs = n \<and> length ys = n \<and>
     (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y) \<in> r)}"
-apply (induct n, simp)
-apply (simp add: image_Collect lex_prod_def, safe, blast)
- apply (rule_tac x = "ab # xys" in exI, simp)
-apply (case_tac xys, simp_all, blast)
-done
+proof (induction n)
+  case (Suc n)
+  then show ?case
+    apply (simp add: image_Collect lex_prod_def, safe, blast)
+     apply (rule_tac x = "ab # xys" in exI, simp)
+    apply (case_tac xys; force)
+    done
+qed auto
 
 text\<open>By Mathias Fleury:\<close>
 proposition lexn_transI:
@@ -6121,7 +6111,7 @@
     (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y) \<in> r)}"
 by (force simp add: lex_def lexn_conv)
 
-lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"
+lemma wf_lenlex [intro!]: "wf r \<Longrightarrow> wf (lenlex r)"
 by (unfold lenlex_def) blast
 
 lemma lenlex_conv:
@@ -6152,18 +6142,21 @@
   by (meson lex_transI trans_inv_image trans_less_than trans_lex_prod)
 
 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
-by (simp add: lex_conv)
+  by (simp add: lex_conv)
 
 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
-by (simp add:lex_conv)
+  by (simp add:lex_conv)
 
 lemma Cons_in_lex [simp]:
-  "((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)
-  by (metis hd_append append_Nil list.sel(1) list.sel(3) tl_append2)
+  "(x # xs, y # ys) \<in> lex r \<longleftrightarrow> (x, y) \<in> r \<and> length xs = length ys \<or> x = y \<and> (xs, ys) \<in> lex r"
+ (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (simp add: lex_conv) (metis hd_append list.sel(1) list.sel(3) tl_append2)
+next
+  assume ?rhs then show ?lhs
+    by (simp add: lex_conv) (blast intro: Cons_eq_appendI)
+qed
 
 lemma Nil_lenlex_iff1 [simp]: "([], ns) \<in> lenlex r \<longleftrightarrow> ns \<noteq> []" 
   and Nil_lenlex_iff2 [simp]: "(ns,[]) \<notin> lenlex r"
@@ -6181,24 +6174,23 @@
 
 lemma lex_append_rightI:
   "(xs, ys) \<in> lex r \<Longrightarrow> length vs = length us \<Longrightarrow> (xs @ us, ys @ vs) \<in> lex r"
-by (fastforce simp: lex_def lexn_conv)
+  by (fastforce simp: lex_def lexn_conv)
 
 lemma lex_append_leftI:
   "(ys, zs) \<in> lex r \<Longrightarrow> (xs @ ys, xs @ zs) \<in> lex r"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma lex_append_leftD:
   "\<forall>x. (x,x) \<notin> r \<Longrightarrow> (xs @ ys, xs @ zs) \<in> lex r \<Longrightarrow> (ys, zs) \<in> lex r"
-by (induct xs) auto
+  by (induct xs) auto
 
 lemma lex_append_left_iff:
   "\<forall>x. (x,x) \<notin> r \<Longrightarrow> (xs @ ys, xs @ zs) \<in> lex r \<longleftrightarrow> (ys, zs) \<in> lex r"
-by(metis lex_append_leftD lex_append_leftI)
+  by(metis lex_append_leftD lex_append_leftI)
 
 lemma lex_take_index:
   assumes "(xs, ys) \<in> lex r"
-  obtains i where "i < length xs" and "i < length ys" and "take i xs =
-take i ys"
+  obtains i where "i < length xs" and "i < length ys" and "take i xs = take i ys"
     and "(xs ! i, ys ! i) \<in> r"
 proof -
   obtain n us x xs' y ys' where "(xs, ys) \<in> lexn r n" and "length xs = n" and "length ys = n"
@@ -6225,40 +6217,47 @@
 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))"
-  unfolding lexord_def
-  apply (safe, simp_all)
-     apply (metis hd_append list.sel(1))
+  "(a # x, b # y) \<in> lexord r \<longleftrightarrow> (a,b)\<in> r \<or> (a = b \<and> (x,y)\<in> lexord r)"  (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    apply (simp add: lexord_def)
     apply (metis hd_append list.sel(1) list.sel(3) tl_append2)
-   apply blast
-  by (meson Cons_eq_appendI)
+    done
+qed (auto simp add: lexord_def; (blast | meson Cons_eq_appendI))
 
 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
 
 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
-by (induct_tac x, auto)
+  by (induct_tac x, auto)
 
 lemma lexord_append_left_rightI:
-     "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
-by (induct_tac u, auto)
+  "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
+  by (induct_tac u, auto)
 
 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
-by (induct x, auto)
+  by (induct x, auto)
 
 lemma lexord_append_leftD:
-     "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (\<forall>a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
-by (erule rev_mp, induct_tac x, auto)
+  "\<lbrakk>(x @ u, x @ v) \<in> lexord r; (\<forall>a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
+  by (erule rev_mp, induct_tac x, auto)
 
 lemma lexord_take_index_conv:
    "((x,y) \<in> lexord r) =
     ((length x < length y \<and> take (length x) y = x) \<or>
      (\<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 ="length u" in exI, simp)
-  by (metis id_take_nth_drop)
+proof -
+  have "(\<exists>a v. y = x @ a # v) = (length x < length y \<and> take (length x) y = x)"
+    by (metis Cons_nth_drop_Suc append_eq_conv_conj drop_all list.simps(3) not_le)
+  moreover
+  have "(\<exists>u a b. (a, b) \<in> r \<and> (\<exists>v. x = u @ a # v) \<and> (\<exists>w. y = u @ b # w)) =
+        (\<exists>i<length x. i < length y \<and> take i x = take i y \<and> (x ! i, y ! i) \<in> r)"
+    apply safe
+    using less_iff_Suc_add apply auto[1]
+    by (metis id_take_nth_drop)
+  ultimately show ?thesis
+    by (auto simp: lexord_def Let_def)
+qed
 
 \<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)"
@@ -6539,10 +6538,10 @@
 unfolding measures_def
 by auto
 
-lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
+lemma measures_less: "f x < f y \<Longrightarrow> (x, y) \<in> measures (f#fs)"
 by simp
 
-lemma measures_lesseq: "f x \<le> f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
+lemma measures_lesseq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> measures fs \<Longrightarrow> (x, y) \<in> measures (f#fs)"
 by auto
 
 
@@ -6685,7 +6684,7 @@
   for r :: "('a \<times> 'b) set"
 where
     Nil:  "([],[]) \<in> listrel r"
-  | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
+  | Cons: "\<lbrakk>(x,y) \<in> r; (xs,ys) \<in> listrel r\<rbrakk> \<Longrightarrow> (x#xs, y#ys) \<in> listrel r"
 
 inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
 inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
diff -r 24b68a932f26 -r 4b1021677f15 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/HOL/Nat.thy	Sun Mar 22 17:21:16 2020 +0000
@@ -65,15 +65,15 @@
   by (rule iffI, rule Suc_Rep_inject) simp_all
 
 lemma nat_induct0:
-  assumes "P 0"
-    and "\<And>n. P n \<Longrightarrow> P (Suc n)"
+  assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
   shows "P n"
-  using assms
-  apply (unfold Zero_nat_def Suc_def)
-  apply (rule Rep_Nat_inverse [THEN subst]) \<comment> \<open>types force good instantiation\<close>
-  apply (erule Nat_Rep_Nat [THEN Nat.induct])
-  apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
-  done
+proof -
+  have "P (Abs_Nat (Rep_Nat n))"
+    using assms unfolding Zero_nat_def Suc_def
+    by (iprover intro:  Nat_Rep_Nat [THEN Nat.induct] elim: Nat_Abs_Nat_inverse [THEN subst])
+  then show ?thesis
+    by (simp add: Rep_Nat_inverse)
+qed
 
 free_constructors case_nat for "0 :: nat" | Suc pred
   where "pred (0 :: nat) = (0 :: nat)"
@@ -87,11 +87,7 @@
 setup \<open>Sign.mandatory_path "old"\<close>
 
 old_rep_datatype "0 :: nat" Suc
-    apply (erule nat_induct0)
-    apply assumption
-   apply (rule nat.inject)
-  apply (rule nat.distinct(1))
-  done
+  by (erule nat_induct0) auto
 
 setup \<open>Sign.parent_path\<close>
 
@@ -356,18 +352,11 @@
 qed
 
 lemma one_eq_mult_iff [simp]: "Suc 0 = m * n \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
-  apply (rule trans)
-   apply (rule_tac [2] mult_eq_1_iff)
-  apply fastforce
-  done
-
-lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1"
-  for m n :: nat
-  unfolding One_nat_def by (rule mult_eq_1_iff)
-
-lemma nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1"
-  for m n :: nat
-  unfolding One_nat_def by (rule one_eq_mult_iff)
+  by (simp add: eq_commute flip: mult_eq_1_iff)
+
+lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1" 
+  and nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1" for m n :: nat
+  by auto
 
 lemma mult_cancel1 [simp]: "k * m = k * n \<longleftrightarrow> m = n \<or> k = 0"
   for k m n :: nat
@@ -584,22 +573,23 @@
     and less: "m < n \<Longrightarrow> P"
     and eq: "m = n \<Longrightarrow> P"
   shows P
-  apply (rule major [THEN lessE])
-   apply (rule eq)
-   apply blast
-  apply (rule less)
-  apply blast
-  done
+proof (rule major [THEN lessE])
+  show "Suc n = Suc m \<Longrightarrow> P"
+    using eq by blast
+  show "\<And>j. \<lbrakk>m < j; Suc n = Suc j\<rbrakk> \<Longrightarrow> P"
+    by (blast intro: less)
+qed
 
 lemma Suc_lessE:
   assumes major: "Suc i < k"
     and minor: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P"
   shows P
-  apply (rule major [THEN lessE])
-   apply (erule lessI [THEN minor])
-  apply (erule Suc_lessD [THEN minor])
-  apply assumption
-  done
+proof (rule major [THEN lessE])
+  show "k = Suc (Suc i) \<Longrightarrow> P"
+    using lessI minor by iprover
+  show "\<And>j. \<lbrakk>Suc i < j; k = Suc j\<rbrakk> \<Longrightarrow> P"
+    using Suc_lessD minor by iprover
+qed
 
 lemma Suc_less_SucD: "Suc m < Suc n \<Longrightarrow> m < n"
   by simp
@@ -786,12 +776,16 @@
   by (induct k) simp_all
 
 text \<open>strict, in both arguments\<close>
-lemma add_less_mono: "i < j \<Longrightarrow> k < l \<Longrightarrow> i + k < j + l"
-  for i j k l :: nat
-  apply (rule add_less_mono1 [THEN less_trans], assumption+)
-  apply (induct j)
-   apply simp_all
-  done
+lemma add_less_mono: 
+  fixes i j k l :: nat
+  assumes "i < j" "k < l" shows "i + k < j + l"
+proof -
+  have "i + k < j + k"
+    by (simp add: add_less_mono1 assms)
+  also have "...  < j + l"
+    using \<open>i < j\<close> by (induction j) (auto simp: assms)
+  finally show ?thesis .
+qed
 
 lemma less_imp_Suc_add: "m < n \<Longrightarrow> \<exists>k. n = Suc (m + k)"
 proof (induct n)
@@ -969,42 +963,55 @@
   for P :: "nat \<Rightarrow> bool"
   by (rule Least_equality[OF _ le0])
 
-lemma Least_Suc: "P n \<Longrightarrow> \<not> P 0 \<Longrightarrow> (LEAST n. P n) = Suc (LEAST m. P (Suc m))"
-  apply (cases n)
-   apply auto
-  apply (frule LeastI)
-  apply (drule_tac P = "\<lambda>x. P (Suc x)" in LeastI)
-  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
-   apply (erule_tac [2] Least_le)
-  apply (cases "LEAST x. P x")
-   apply auto
-  apply (drule_tac P = "\<lambda>x. P (Suc x)" in Least_le)
-  apply (blast intro: order_antisym)
-  done
+lemma Least_Suc:
+  assumes "P n" "\<not> P 0" 
+  shows "(LEAST n. P n) = Suc (LEAST m. P (Suc m))"
+proof (cases n)
+  case (Suc m)
+  show ?thesis
+  proof (rule antisym)
+    show "(LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))"
+      using assms Suc by (force intro: LeastI Least_le)
+    have \<section>: "P (LEAST x. P x)"
+      by (blast intro: LeastI assms)
+    show "Suc (LEAST m. P (Suc m)) \<le> (LEAST n. P n)"
+    proof (cases "(LEAST n. P n)")
+      case 0
+      then show ?thesis
+        using \<section> by (simp add: assms)
+    next
+      case Suc
+      with \<section> show ?thesis
+        by (auto simp: Least_le)
+    qed
+  qed
+qed (use assms in auto)
 
 lemma Least_Suc2: "P n \<Longrightarrow> Q m \<Longrightarrow> \<not> P 0 \<Longrightarrow> \<forall>k. P (Suc k) = Q k \<Longrightarrow> Least P = Suc (Least Q)"
   by (erule (1) Least_Suc [THEN ssubst]) simp
 
-lemma ex_least_nat_le: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not> P i) \<and> P k"
-  for P :: "nat \<Rightarrow> bool"
-  apply (cases n)
-   apply blast
-  apply (rule_tac x="LEAST k. P k" in exI)
-  apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
-  done
-
-lemma ex_least_nat_less: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not> P i) \<and> P (k + 1)"
-  for P :: "nat \<Rightarrow> bool"
-  apply (cases n)
-   apply blast
-  apply (frule (1) ex_least_nat_le)
-  apply (erule exE)
-  apply (case_tac k)
-   apply simp
-  apply (rename_tac k1)
-  apply (rule_tac x=k1 in exI)
-  apply (auto simp add: less_eq_Suc_le)
-  done
+lemma ex_least_nat_le:
+  fixes P :: "nat \<Rightarrow> bool"
+  assumes "P n" "\<not> P 0" 
+  shows "\<exists>k\<le>n. (\<forall>i<k. \<not> P i) \<and> P k"
+proof (cases n)
+  case (Suc m)
+  with assms show ?thesis
+    by (blast intro: Least_le LeastI_ex dest: not_less_Least)
+qed (use assms in auto)
+
+lemma ex_least_nat_less:
+  fixes P :: "nat \<Rightarrow> bool"
+  assumes "P n" "\<not> P 0" 
+  shows "\<exists>k<n. (\<forall>i\<le>k. \<not> P i) \<and> P (Suc k)"
+proof (cases n)
+  case (Suc m)
+  then obtain k where k: "k \<le> n" "\<forall>i<k. \<not> P i" "P k"
+    using ex_least_nat_le [OF assms] by blast
+  show ?thesis 
+    by (cases k) (use assms k less_eq_Suc_le in auto)
+qed (use assms in auto)
+
 
 lemma nat_less_induct:
   fixes P :: "nat \<Rightarrow> bool"
@@ -1070,11 +1077,10 @@
   assumes "P 0"
     and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> \<exists>m. m < n \<and> \<not> P m"
   shows "P n"
-  apply (rule infinite_descent)
-  using assms
-  apply (case_tac "n > 0")
-   apply auto
-  done
+proof (rule infinite_descent)
+  show "\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m"
+  using assms by (case_tac "n > 0") auto
+qed
 
 text \<open>
   Infinite descent using a mapping to \<open>nat\<close>:
@@ -1178,14 +1184,11 @@
 
 lemma not_add_less1 [iff]: "\<not> i + j < i"
   for i j :: nat
-  apply (rule notI)
-  apply (drule add_lessD1)
-  apply (erule less_irrefl [THEN notE])
-  done
+  by simp
 
 lemma not_add_less2 [iff]: "\<not> j + i < i"
   for i j :: nat
-  by (simp add: add.commute)
+  by simp
 
 lemma add_leD1: "m + k \<le> n \<Longrightarrow> m \<le> n"
   for k m n :: nat
@@ -1193,9 +1196,7 @@
 
 lemma add_leD2: "m + k \<le> n \<Longrightarrow> k \<le> n"
   for k m n :: nat
-  apply (simp add: add.commute)
-  apply (erule add_leD1)
-  done
+  by (force simp add: add.commute dest: add_leD1)
 
 lemma add_leE: "m + k \<le> n \<Longrightarrow> (m \<le> n \<Longrightarrow> k \<le> n \<Longrightarrow> R) \<Longrightarrow> R"
   for k m n :: nat
@@ -1213,10 +1214,7 @@
   by (induct m n rule: diff_induct) simp_all
 
 lemma diff_less_Suc: "m - n < Suc m"
-  apply (induct m n rule: diff_induct)
-    apply (erule_tac [3] less_SucE)
-     apply (simp_all add: less_Suc_eq)
-  done
+  by (induct m n rule: diff_induct) (auto simp: less_Suc_eq)
 
 lemma diff_le_self [simp]: "m - n \<le> m"
   for m n :: nat
@@ -1345,12 +1343,26 @@
 
 lemma mult_less_cancel2 [simp]: "m * k < n * k \<longleftrightarrow> 0 < k \<and> m < n"
   for k m n :: nat
-  apply (safe intro!: mult_less_mono1)
-   apply (cases k)
-    apply auto
-  apply (simp add: linorder_not_le [symmetric])
-  apply (blast intro: mult_le_mono1)
-  done
+proof (intro iffI conjI)
+  assume m: "m * k < n * k"
+  then show "0 < k"
+    by (cases k) auto
+  show "m < n"
+  proof (cases k)
+    case 0
+    then show ?thesis
+      using m by auto
+  next
+    case (Suc k')
+    then show ?thesis
+      using m
+      by (simp flip: linorder_not_le) (blast intro: add_mono mult_le_mono1)
+  qed
+next
+  assume "0 < k \<and> m < n"
+  then show "m * k < n * k"
+    by (blast intro: mult_less_mono1)
+qed
 
 lemma mult_less_cancel1 [simp]: "k * m < k * n \<longleftrightarrow> 0 < k \<and> m < n"
   for k m n :: nat
@@ -1379,16 +1391,18 @@
   by (cases m) (auto intro: le_add1)
 
 text \<open>Lemma for \<open>gcd\<close>\<close>
-lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0"
-  for m n :: nat
-  apply (drule sym)
-  apply (rule disjCI)
-  apply (rule linorder_cases)
-    defer
-    apply assumption
-   apply (drule mult_less_mono2)
-    apply auto
-  done
+lemma mult_eq_self_implies_10: 
+  fixes m n :: nat
+  assumes "m = m * n" shows "n = 1 \<or> m = 0"
+proof (rule disjCI)
+  assume "m \<noteq> 0"
+  show "n = 1"
+  proof (cases n "1::nat" rule: linorder_cases)
+    case greater
+    show ?thesis
+      using assms mult_less_mono2 [OF greater, of m] \<open>m \<noteq> 0\<close> by auto
+  qed (use assms \<open>m \<noteq> 0\<close> in auto)
+qed
 
 lemma mono_times_nat:
   fixes n :: nat
@@ -1849,28 +1863,20 @@
   by (simp add: Nats_def)
 
 lemma Nats_0 [simp]: "0 \<in> \<nat>"
-  apply (simp add: Nats_def)
-  apply (rule range_eqI)
-  apply (rule of_nat_0 [symmetric])
-  done
+  using of_nat_0 [symmetric] unfolding Nats_def
+  by (rule range_eqI)
 
 lemma Nats_1 [simp]: "1 \<in> \<nat>"
-  apply (simp add: Nats_def)
-  apply (rule range_eqI)
-  apply (rule of_nat_1 [symmetric])
-  done
+  using of_nat_1 [symmetric] unfolding Nats_def
+  by (rule range_eqI)
 
 lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>"
-  apply (auto simp add: Nats_def)
-  apply (rule range_eqI)
-  apply (rule of_nat_add [symmetric])
-  done
+  unfolding Nats_def using of_nat_add [symmetric]
+  by (blast intro: range_eqI)
 
 lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>"
-  apply (auto simp add: Nats_def)
-  apply (rule range_eqI)
-  apply (rule of_nat_mult [symmetric])
-  done
+  unfolding Nats_def using of_nat_mult [symmetric]
+  by (blast intro: range_eqI)
 
 lemma Nats_cases [cases set: Nats]:
   assumes "x \<in> \<nat>"
@@ -2303,21 +2309,21 @@
   qed
 qed
 
-lemma GreatestI_nat:
-  "\<lbrakk> P(k::nat); \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)"
-apply(drule (1) ex_has_greatest_nat)
-using GreatestI2_order by auto
-
-lemma Greatest_le_nat:
-  "\<lbrakk> P(k::nat);  \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> k \<le> (Greatest P)"
-apply(frule (1) ex_has_greatest_nat)
-using GreatestI2_order[where P=P and Q=\<open>\<lambda>x. k \<le> x\<close>] by auto
+lemma
+  fixes k::nat
+  assumes "P k" and minor: "\<And>y. P y \<Longrightarrow> y \<le> b"
+  shows GreatestI_nat: "P (Greatest P)" 
+    and Greatest_le_nat: "k \<le> Greatest P"
+proof -
+  obtain x where "P x" "\<And>y. P y \<Longrightarrow> y \<le> x"
+    using assms ex_has_greatest_nat by blast
+  with \<open>P k\<close> show "P (Greatest P)" "k \<le> Greatest P"
+    using GreatestI2_order by blast+
+qed
 
 lemma GreatestI_ex_nat:
-  "\<lbrakk> \<exists>k::nat. P k;  \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)"
-apply (erule exE)
-apply (erule (1) GreatestI_nat)
-done
+  "\<lbrakk> \<exists>k::nat. P k;  \<And>y. P y \<Longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)"
+  by (blast intro: GreatestI_nat)
 
 
 subsection \<open>Monotonicity of \<open>funpow\<close>\<close>
@@ -2363,11 +2369,16 @@
   for k m n :: nat
   unfolding dvd_def by (blast intro: right_diff_distrib' [symmetric])
 
-lemma dvd_diffD: "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd m"
-  for k m n :: nat
-  apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
-  apply (blast intro: dvd_add)
-  done
+lemma dvd_diffD: 
+  fixes k m n :: nat
+  assumes "k dvd m - n" "k dvd n" "n \<le> m"
+  shows "k dvd m"
+proof -
+  have "k dvd n + (m - n)"
+    using assms by (blast intro: dvd_add)
+  with assms show ?thesis
+    by simp
+qed
 
 lemma dvd_diffD1: "k dvd m - n \<Longrightarrow> k dvd m \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd n"
   for k m n :: nat
@@ -2384,13 +2395,19 @@
   then show ?thesis ..
 qed
 
-lemma dvd_mult_cancel1: "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = 1"
-  for m n :: nat
-  apply auto
-  apply (subgoal_tac "m * n dvd m * 1")
-   apply (drule dvd_mult_cancel)
-    apply auto
-  done
+lemma dvd_mult_cancel1:
+  fixes m n :: nat
+  assumes "0 < m"
+  shows "m * n dvd m \<longleftrightarrow> n = 1"
+proof 
+  assume "m * n dvd m"
+  then have "m * n dvd m * 1"
+    by simp
+  then have "n dvd 1"
+    by (iprover intro: assms dvd_mult_cancel)
+  then show "n = 1"
+    by auto
+qed auto
 
 lemma dvd_mult_cancel2: "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = 1"
   for m n :: nat
@@ -2441,15 +2458,6 @@
 lemma nat_mult_1_right: "n * 1 = n"
   for n :: nat
   by (fact mult_1_right)
-
-lemma nat_add_left_cancel: "k + m = k + n \<longleftrightarrow> m = n"
-  for k m n :: nat
-  by (fact add_left_cancel)
-
-lemma nat_add_right_cancel: "m + k = n + k \<longleftrightarrow> m = n"
-  for k m n :: nat
-  by (fact add_right_cancel)
-
 lemma diff_mult_distrib: "(m - n) * k = (m * k) - (n * k)"
   for k m n :: nat
   by (fact left_diff_distrib')
@@ -2458,14 +2466,6 @@
   for k m n :: nat
   by (fact right_diff_distrib')
 
-lemma le_add_diff: "k \<le> n \<Longrightarrow> m \<le> n + m - k"
-  for k m n :: nat
-  by (fact le_add_diff)  (* FIXME delete *)
-
-lemma le_diff_conv2: "k \<le> j \<Longrightarrow> (i \<le> j - k) = (i + k \<le> j)"
-  for i j k :: nat
-  by (fact le_diff_conv2) (* FIXME delete *)
-
 lemma diff_self_eq_0 [simp]: "m - m = 0"
   for m :: nat
   by (fact diff_cancel)
diff -r 24b68a932f26 -r 4b1021677f15 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/HOL/Transcendental.thy	Sun Mar 22 17:21:16 2020 +0000
@@ -618,10 +618,6 @@
   for r :: "'a::ring_1"
   by (simp add: sum_subtractf)
 
-lemma lemma_realpow_rev_sumr:
-  "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) = (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
-  by (subst sum.nat_diff_reindex[symmetric]) simp
-
 lemma lemma_termdiff2:
   fixes h :: "'a::field"
   assumes h: "h \<noteq> 0"
@@ -629,26 +625,26 @@
          h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))"
     (is "?lhs = ?rhs")
 proof (cases n)
-  case (Suc n)
+  case (Suc m)
   have 0: "\<And>x k. (\<Sum>n<Suc k. h * (z ^ x * (z ^ (k - n) * (h + z) ^ n))) =
                  (\<Sum>j<Suc k.  h * ((h + z) ^ j * z ^ (x + k - j)))"
-    apply (rule sum.cong [OF refl])
-    by (simp add: power_add [symmetric] mult.commute)
-  have *: "(\<Sum>i<n. z ^ i * ((z + h) ^ (n - i) - z ^ (n - i))) =
-           (\<Sum>i<n. \<Sum>j<n - i. h * ((z + h) ^ j * z ^ (n - Suc j)))"
-    apply (rule sum.cong [OF refl])
-    apply (clarsimp simp add: less_iff_Suc_add sum_distrib_left diff_power_eq_sum ac_simps 0
-        simp del: sum.lessThan_Suc power_Suc)
-    done
-  have "h * ?lhs = h * ?rhs"
-    apply (simp add: right_diff_distrib diff_divide_distrib h mult.assoc [symmetric])
-    using Suc
-    apply (simp add: diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
+    by (auto simp add: power_add [symmetric] mult.commute intro: sum.cong)
+  have *: "(\<Sum>i<m. z ^ i * ((z + h) ^ (m - i) - z ^ (m - i))) =
+           (\<Sum>i<m. \<Sum>j<m - i. h * ((z + h) ^ j * z ^ (m - Suc j)))"
+    by (force simp add: less_iff_Suc_add sum_distrib_left diff_power_eq_sum ac_simps 0
+        simp del: sum.lessThan_Suc power_Suc intro: sum.cong)
+  have "h * ?lhs = (z + h) ^ n - z ^ n - h * of_nat n * z ^ (n - Suc 0)"
+    by (simp add: right_diff_distrib diff_divide_distrib h mult.assoc [symmetric])
+  also have "... = h * ((\<Sum>p<Suc m. (z + h) ^ p * z ^ (m - p)) - of_nat (Suc m) * z ^ m)"
+    by (simp add: Suc diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
         del: power_Suc sum.lessThan_Suc of_nat_Suc)
-    apply (subst lemma_realpow_rev_sumr)
-    apply (subst sumr_diff_mult_const2)
-    apply (simp add: lemma_termdiff1 sum_distrib_left *)
-    done
+  also have "... = h * ((\<Sum>p<Suc m. (z + h) ^ (m - p) * z ^ p) - of_nat (Suc m) * z ^ m)"
+    by (subst sum.nat_diff_reindex[symmetric]) simp
+  also have "... = h * (\<Sum>i<Suc m. (z + h) ^ (m - i) * z ^ i - z ^ m)"
+    by (simp add: sum_subtractf)
+  also have "... = h * ?rhs"
+    by (simp add: lemma_termdiff1 sum_distrib_left Suc *)
+  finally have "h * ?lhs = h * ?rhs" .
   then show ?thesis
     by (simp add: h)
 qed auto
@@ -656,12 +652,15 @@
 
 lemma real_sum_nat_ivl_bounded2:
   fixes K :: "'a::linordered_semidom"
-  assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
-    and K: "0 \<le> K"
+  assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K" and K: "0 \<le> K"
   shows "sum f {..<n-k} \<le> of_nat n * K"
-  apply (rule order_trans [OF sum_mono [OF f]])
-  apply (auto simp: mult_right_mono K)
-  done
+proof -
+  have "sum f {..<n-k} \<le> (\<Sum>i<n - k. K)"
+    by (rule sum_mono [OF f]) auto
+  also have "... \<le> of_nat n * K"
+    by (auto simp: mult_right_mono K)
+  finally show ?thesis .
+qed
 
 lemma lemma_termdiff3:
   fixes h z :: "'a::real_normed_field"
@@ -678,21 +677,23 @@
   proof (rule mult_right_mono [OF _ norm_ge_zero])
     from norm_ge_zero 2 have K: "0 \<le> K"
       by (rule order_trans)
-    have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n"
-      apply (erule subst)
-      apply (simp only: norm_mult norm_power power_add)
-      apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
-      done
+    have le_Kn: "norm ((z + h) ^ i * z ^ j) \<le> K ^ n" if "i + j = n" for i j n
+    proof -
+      have "norm (z + h) ^ i * norm z ^ j \<le> K ^ i * K ^ j"
+        by (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
+      also have "... = K^n"
+        by (metis power_add that)
+      finally show ?thesis
+        by (simp add: norm_mult norm_power) 
+    qed
+    then have "\<And>p q.
+       \<lbrakk>p < n; q < n - Suc 0\<rbrakk> \<Longrightarrow> norm ((z + h) ^ q * z ^ (n - 2 - q)) \<le> K ^ (n - 2)"
+      by simp
+    then
     show "norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q)) \<le>
         of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
-      apply (intro
-          order_trans [OF norm_sum]
-          real_sum_nat_ivl_bounded2
-          mult_nonneg_nonneg
-          of_nat_0_le_iff
-          zero_le_power K)
-      apply (rule le_Kn, simp)
-      done
+      by (intro order_trans [OF norm_sum]
+          real_sum_nat_ivl_bounded2 mult_nonneg_nonneg of_nat_0_le_iff zero_le_power K)
   qed
   also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
     by (simp only: mult.assoc)
@@ -775,39 +776,30 @@
     then have "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))"
       by (rule diffs_equiv [THEN sums_summable])
     also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0)) =
-      (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
-      apply (rule ext)
-      apply (case_tac n)
-      apply (simp_all add: diffs_def r_neq_0)
-      done
+               (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
+      by (simp add: diffs_def r_neq_0 fun_eq_iff split: nat_diff_split)
     finally have "summable
       (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
       by (rule diffs_equiv [THEN sums_summable])
     also have
       "(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0)) =
        (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
-      apply (rule ext)
-      apply (case_tac n, simp)
-      apply (rename_tac nat)
-      apply (case_tac nat, simp)
-      apply (simp add: r_neq_0)
-      done
+      by (rule ext) (simp add: r_neq_0 split: nat_diff_split)
     finally show "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
   next
-    fix h :: 'a
-    fix n :: nat
+    fix h :: 'a and n
     assume h: "h \<noteq> 0"
     assume "norm h < r - norm x"
     then have "norm x + norm h < r" by simp
-    with norm_triangle_ineq have xh: "norm (x + h) < r"
+    with norm_triangle_ineq 
+    have xh: "norm (x + h) < r"
       by (rule order_le_less_trans)
-    show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) \<le>
+    have "norm (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))
+    \<le> real n * (real (n - Suc 0) * (r ^ (n - 2) * norm h))"
+      by (metis (mono_tags, lifting) h mult.assoc lemma_termdiff3 less_eq_real_def r1 xh)
+    then show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) \<le>
       norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
-      apply (simp only: norm_mult mult.assoc)
-      apply (rule mult_left_mono [OF _ norm_ge_zero])
-      apply (simp add: mult.assoc [symmetric])
-      apply (metis h lemma_termdiff3 less_eq_real_def r1 xh)
-      done
+      by (simp only: norm_mult mult.assoc mult_left_mono [OF _ norm_ge_zero])
   qed
 qed
 
@@ -900,12 +892,10 @@
     and K: "norm x < norm K"
   shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. diffs c n * x^n)"
 proof -
-  have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
-    using K
-    apply (auto simp: norm_divide field_simps)
-    apply (rule le_less_trans [of _ "of_real (norm K) + of_real (norm x)"])
-     apply (auto simp: mult_2_right norm_triangle_mono)
-    done
+  have "norm K + norm x < norm K + norm K"
+    using K by force
+  then have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
+    by (auto simp: norm_triangle_lt norm_divide field_simps)
   then have [simp]: "norm ((of_real (norm K) + of_real (norm x)) :: 'a) < norm K * 2"
     by simp
   have "summable (\<lambda>n. c n * (of_real (norm x + norm K) / 2) ^ n)"
@@ -915,11 +905,8 @@
   moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs(diffs c) n * x ^ n)"
     by (blast intro: sm termdiff_converges powser_inside)
   ultimately show ?thesis
-    apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
-    using K
-      apply (auto simp: field_simps)
-    apply (simp flip: of_real_add)
-    done
+    by (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
+       (use K in \<open>auto simp: field_simps simp flip: of_real_add\<close>)
 qed
 
 lemma termdiffs_strong_converges_everywhere:
@@ -999,11 +986,12 @@
     by (blast intro: DERIV_continuous)
   then have "((\<lambda>x. \<Sum>n. a n * x ^ n) \<longlongrightarrow> a 0) (at 0)"
     by (simp add: continuous_within)
-  then show ?thesis
-    apply (rule Lim_transform)
+  moreover have "(\<lambda>x. f x - (\<Sum>n. a n * x ^ n)) \<midarrow>0\<rightarrow> 0"
     apply (clarsimp simp: LIM_eq)
     apply (rule_tac x=s in exI)
     using s sm sums_unique by fastforce
+  ultimately show ?thesis
+    by (rule Lim_transform)
 qed
 
 lemma powser_limit_0_strong:
@@ -1015,9 +1003,7 @@
   have *: "((\<lambda>x. if x = 0 then a 0 else f x) \<longlongrightarrow> a 0) (at 0)"
     by (rule powser_limit_0 [OF s]) (auto simp: powser_sums_zero sm)
   show ?thesis
-    apply (subst LIM_equal [where g = "(\<lambda>x. if x = 0 then a 0 else f x)"])
-     apply (simp_all add: *)
-    done
+    by (simp add: * LIM_equal [where g = "(\<lambda>x. if x = 0 then a 0 else f x)"])
 qed
 
 
@@ -1591,10 +1577,10 @@
   have "1 + x \<le> (\<Sum>n<2. inverse (fact n) * x^n)"
     by (auto simp: numeral_2_eq_2)
   also have "\<dots> \<le> (\<Sum>n. inverse (fact n) * x^n)"
-    apply (rule sum_le_suminf [OF summable_exp])
-    using \<open>0 < x\<close>
-    apply (auto  simp add: zero_le_mult_iff)
-    done
+  proof (rule sum_le_suminf [OF summable_exp])
+    show "\<forall>m\<in>- {..<2}. 0 \<le> inverse (fact m) * x ^ m"
+      using \<open>0 < x\<close> by (auto  simp add: zero_le_mult_iff)
+  qed auto
   finally show "1 + x \<le> exp x"
     by (simp add: exp_def)
 qed auto
@@ -2049,9 +2035,7 @@
 proof (cases "0 \<le> x \<or> x \<le> -1")
   case True
   then show ?thesis
-    apply (rule disjE)
-     apply (simp add: exp_ge_add_one_self_aux)
-    using exp_ge_zero order_trans real_add_le_0_iff by blast
+    by (meson exp_ge_add_one_self_aux exp_ge_zero order.trans real_add_le_0_iff)
 next
   case False
   then have ln1: "ln (1 + x) \<le> x"
@@ -2463,11 +2447,12 @@
 lemma powr_non_neg[simp]: "\<not>a powr x < 0" for a x::real
   using powr_ge_pzero[of a x] by arith
 
+lemma inverse_powr: "\<And>y::real. 0 \<le> y \<Longrightarrow> inverse y powr a = inverse (y powr a)"
+    by (simp add: exp_minus ln_inverse powr_def)
+
 lemma powr_divide: "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
   for a b x :: real
-  apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
-  apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
-  done
+    by (simp add: divide_inverse powr_mult inverse_powr)
 
 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
   for a b x :: "'a::{ln,real_normed_field}"
@@ -3198,17 +3183,20 @@
 
 lemma summable_norm_sin: "summable (\<lambda>n. norm (sin_coeff n *\<^sub>R x^n))"
   for x :: "'a::{real_normed_algebra_1,banach}"
-  unfolding sin_coeff_def
-  apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
-  apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
-  done
+proof (rule summable_comparison_test [OF _ summable_norm_exp])
+  show "\<exists>N. \<forall>n\<ge>N. norm (norm (sin_coeff n *\<^sub>R x ^ n)) \<le> norm (x ^ n /\<^sub>R fact n)"
+    unfolding sin_coeff_def
+    by (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
+qed
 
 lemma summable_norm_cos: "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x^n))"
   for x :: "'a::{real_normed_algebra_1,banach}"
-  unfolding cos_coeff_def
-  apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
-  apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
-  done
+proof (rule summable_comparison_test [OF _ summable_norm_exp])
+  show "\<exists>N. \<forall>n\<ge>N. norm (norm (cos_coeff n *\<^sub>R x ^ n)) \<le> norm (x ^ n /\<^sub>R fact n)"
+    unfolding cos_coeff_def
+    by (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
+qed
+
 
 lemma sin_converges: "(\<lambda>n. sin_coeff n *\<^sub>R x^n) sums sin x"
   unfolding sin_def
@@ -3230,8 +3218,7 @@
     by (rule sin_converges)
   finally have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R x^n)) sums (sin (of_real x))" .
   then show ?thesis
-    using sums_unique2 sums_of_real [OF sin_converges]
-    by blast
+    using sums_unique2 sums_of_real [OF sin_converges] by blast
 qed
 
 corollary sin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> sin z \<in> \<real>"
@@ -3317,44 +3304,41 @@
 lemma continuous_on_cos_real: "continuous_on {a..b} cos" for a::real
   using continuous_at_imp_continuous_on isCont_cos by blast
 
+
+context
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::{real_normed_field,banach}"
+begin
+
 lemma isCont_sin' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   by (rule isCont_o2 [OF _ isCont_sin])
 
-(* FIXME a context for f would be better *)
-
 lemma isCont_cos' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   by (rule isCont_o2 [OF _ isCont_cos])
 
 lemma tendsto_sin [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) \<longlongrightarrow> sin a) F"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   by (rule isCont_tendsto_compose [OF isCont_sin])
 
 lemma tendsto_cos [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) \<longlongrightarrow> cos a) F"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   by (rule isCont_tendsto_compose [OF isCont_cos])
 
 lemma continuous_sin [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   unfolding continuous_def by (rule tendsto_sin)
 
 lemma continuous_on_sin [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   unfolding continuous_on_def by (auto intro: tendsto_sin)
 
+lemma continuous_cos [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
+  unfolding continuous_def by (rule tendsto_cos)
+
+lemma continuous_on_cos [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_cos)
+
+end
+
 lemma continuous_within_sin: "continuous (at z within s) sin"     
   for z :: "'a::{real_normed_field,banach}"
   by (simp add: continuous_within tendsto_sin)
 
-lemma continuous_cos [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
-  unfolding continuous_def by (rule tendsto_cos)
-
-lemma continuous_on_cos [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
-  unfolding continuous_on_def by (auto intro: tendsto_cos)
-
 lemma continuous_within_cos: "continuous (at z within s) cos"
   for z :: "'a::{real_normed_field,banach}"
   by (simp add: continuous_within tendsto_cos)
@@ -3369,10 +3353,10 @@
   by (simp add: cos_def cos_coeff_def scaleR_conv_of_real)
 
 lemma DERIV_fun_sin: "DERIV g x :> m \<Longrightarrow> DERIV (\<lambda>x. sin (g x)) x :> cos (g x) * m"
-  by (auto intro!: derivative_intros)
+  by (fact derivative_intros)
 
 lemma DERIV_fun_cos: "DERIV g x :> m \<Longrightarrow> DERIV (\<lambda>x. cos(g x)) x :> - sin (g x) * m"
-  by (auto intro!: derivative_eq_intros)
+  by (fact derivative_intros)
 
 
 subsection \<open>Deriving the Addition Formulas\<close>
@@ -3428,15 +3412,16 @@
     have "(-1) ^ ((n - Suc 0) div 2) * (-1) ^ ((p - Suc n) div 2) = - ((-1 :: real) ^ (p div 2))"
       if np: "odd n" "even p"
     proof -
+      have "p > 0"
+        using \<open>n \<le> p\<close> neq0_conv that(1) by blast
+      then have \<section>: "(- 1::real) ^ (p div 2 - Suc 0) = - ((- 1) ^ (p div 2))"
+        using \<open>even p\<close> by (auto simp add: dvd_def power_eq_if)
       from \<open>n \<le> p\<close> np have *: "n - Suc 0 + (p - Suc n) = p - Suc (Suc 0)" "Suc (Suc 0) \<le> p"
         by arith+
       have "(p - Suc (Suc 0)) div 2 = p div 2 - Suc 0"
         by simp
-      with \<open>n \<le> p\<close> np * show ?thesis
-        apply (simp add: power_add [symmetric] div_add [symmetric] del: div_add)
-        apply (metis (no_types) One_nat_def Suc_1 le_div_geq minus_minus
-            mult.left_neutral mult_minus_left power.simps(2) zero_less_Suc)
-        done
+      with \<open>n \<le> p\<close> np  \<section> * show ?thesis
+        by (simp add: flip: div_add power_add)
     qed
     then show ?thesis
       using \<open>n\<le>p\<close> by (auto simp: algebra_simps sin_coeff_def binomial_fact)
@@ -3884,22 +3869,31 @@
 lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
   by (simp add: sin_double)
 
+context
+  fixes w :: "'a::{real_normed_field,banach}"
+
+begin
+
 lemma sin_times_sin: "sin w * sin z = (cos (w - z) - cos (w + z)) / 2"
-  for w :: "'a::{real_normed_field,banach}"
   by (simp add: cos_diff cos_add)
 
 lemma sin_times_cos: "sin w * cos z = (sin (w + z) + sin (w - z)) / 2"
-  for w :: "'a::{real_normed_field,banach}"
   by (simp add: sin_diff sin_add)
 
 lemma cos_times_sin: "cos w * sin z = (sin (w + z) - sin (w - z)) / 2"
-  for w :: "'a::{real_normed_field,banach}"
   by (simp add: sin_diff sin_add)
 
 lemma cos_times_cos: "cos w * cos z = (cos (w - z) + cos (w + z)) / 2"
-  for w :: "'a::{real_normed_field,banach}"
   by (simp add: cos_diff cos_add)
 
+lemma cos_double_cos: "cos (2 * w) = 2 * cos w ^ 2 - 1"
+  by (simp add: cos_double sin_squared_eq)
+
+lemma cos_double_sin: "cos (2 * w) = 1 - 2 * sin w ^ 2"
+  by (simp add: cos_double sin_squared_eq)
+
+end
+
 lemma sin_plus_sin: "sin w + sin z = 2 * sin ((w + z) / 2) * cos ((w - z) / 2)"
   for w :: "'a::{real_normed_field,banach}" 
   apply (simp add: mult.assoc sin_times_cos)
@@ -3924,14 +3918,6 @@
   apply (simp add: field_simps)
   done
 
-lemma cos_double_cos: "cos (2 * z) = 2 * cos z ^ 2 - 1"
-  for z :: "'a::{real_normed_field,banach}"
-  by (simp add: cos_double sin_squared_eq)
-
-lemma cos_double_sin: "cos (2 * z) = 1 - 2 * sin z ^ 2"
-  for z :: "'a::{real_normed_field,banach}"
-  by (simp add: cos_double sin_squared_eq)
-
 lemma sin_pi_minus [simp]: "sin (pi - x) = sin x"
   by (metis sin_minus sin_periodic_pi minus_minus uminus_add_conv_diff)
 
@@ -4074,7 +4060,7 @@
 
 lemma cos_zero_lemma:
   assumes "0 \<le> x" "cos x = 0"
-  shows "\<exists>n. odd n \<and> x = of_nat n * (pi/2) \<and> n > 0"
+  shows "\<exists>n. odd n \<and> x = of_nat n * (pi/2)"
 proof -
   have xle: "x < (1 + real_of_int \<lfloor>x/pi\<rfloor>) * pi"
     using floor_correct [of "x/pi"]
@@ -4101,12 +4087,17 @@
     by (rule_tac x = "Suc (2 * n)" in exI) (simp add: algebra_simps)
 qed
 
-lemma sin_zero_lemma: "0 \<le> x \<Longrightarrow> sin x = 0 \<Longrightarrow> \<exists>n::nat. even n \<and> x = real n * (pi/2)"
-  using cos_zero_lemma [of "x + pi/2"]
-  apply (clarsimp simp add: cos_add)
-  apply (rule_tac x = "n - 1" in exI)
-  apply (simp add: algebra_simps of_nat_diff)
-  done
+lemma sin_zero_lemma:
+  assumes "0 \<le> x" "sin x = 0"
+  shows "\<exists>n::nat. even n \<and> x = real n * (pi/2)"
+proof -
+  obtain n where "odd n" and n: "x + pi/2 = of_nat n * (pi/2)" "n > 0"
+    using cos_zero_lemma [of "x + pi/2"] assms by (auto simp add: cos_add)
+  then have "x = real (n - 1) * (pi / 2)"
+    by (simp add: algebra_simps of_nat_diff)
+  then show ?thesis
+    by (simp add: \<open>odd n\<close>)
+qed
 
 lemma cos_zero_iff:
   "cos x = 0 \<longleftrightarrow> ((\<exists>n. odd n \<and> x = real n * (pi/2)) \<or> (\<exists>n. odd n \<and> x = - (real n * (pi/2))))"
@@ -4146,7 +4137,7 @@
     using that assms by (auto simp: sin_zero_iff)
 qed auto
 
-lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>n. odd n \<and> x = of_int n * (pi/2))"
+lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>i. odd i \<and> x = of_int i * (pi/2))"
 proof -
   have 1: "\<And>n. odd n \<Longrightarrow> \<exists>i. odd i \<and> real n = real_of_int i"
     by (metis even_of_nat of_int_of_nat_eq)
@@ -4159,15 +4150,21 @@
     by (force simp: cos_zero_iff intro!: 1 2 3)
 qed
 
-lemma sin_zero_iff_int: "sin x = 0 \<longleftrightarrow> (\<exists>n. even n \<and> x = of_int n * (pi/2))"
+lemma sin_zero_iff_int: "sin x = 0 \<longleftrightarrow> (\<exists>i. even i \<and> x = of_int i * (pi/2))" (is "?lhs = ?rhs")
 proof safe
-  assume "sin x = 0"
+  assume ?lhs
+  then consider (plus) n where "even n" "x = real n * (pi/2)" | (minus) n where "even n"  "x = - (real n * (pi/2))"
+    using sin_zero_iff by auto
   then show "\<exists>n. even n \<and> x = of_int n * (pi/2)"
-    apply (simp add: sin_zero_iff, safe)
-     apply (metis even_of_nat of_int_of_nat_eq)
-    apply (rule_tac x="- (int n)" in exI)
-    apply simp
-    done
+  proof cases
+    case plus
+    then show ?rhs
+      by (metis even_of_nat of_int_of_nat_eq)
+  next
+    case minus
+    then show ?thesis
+      by (rule_tac x="- (int n)" in exI) simp
+  qed
 next
   fix i :: int
   assume "even i"
@@ -4175,12 +4172,16 @@
     by (cases i rule: int_cases2, simp_all add: sin_zero_iff)
 qed
 
-lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = of_int n * pi)"
-  apply (simp only: sin_zero_iff_int)
-  apply (safe elim!: evenE)
-   apply (simp_all add: field_simps)
-  using dvd_triv_left apply fastforce
-  done
+lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>i::int. x = of_int i * pi)"
+proof -
+  have "sin x = 0 \<longleftrightarrow> (\<exists>i. even i \<and> x = real_of_int i * (pi / 2))"
+    by (auto simp: sin_zero_iff_int)
+  also have "... = (\<exists>j. x = real_of_int (2*j) * (pi / 2))"
+    using dvd_triv_left by blast
+  also have "... = (\<exists>i::int. x = of_int i * pi)"
+    by auto
+  finally show ?thesis .
+qed
 
 lemma sin_npi_int [simp]: "sin (pi * of_int n) = 0"
   by (simp add: sin_zero_iff_int2)
@@ -4252,15 +4253,14 @@
 
 lemma sin_x_le_x:
   fixes x :: real
-  assumes x: "x \<ge> 0"
+  assumes "x \<ge> 0"
   shows "sin x \<le> x"
 proof -
   let ?f = "\<lambda>x. x - sin x"
-  from x have "?f x \<ge> ?f 0"
-    apply (rule DERIV_nonneg_imp_nondecreasing)
-    apply (intro allI impI exI[of _ "1 - cos x" for x])
-    apply (auto intro!: derivative_eq_intros simp: field_simps)
-    done
+  have "\<And>u. \<lbrakk>0 \<le> u; u \<le> x\<rbrakk> \<Longrightarrow> \<exists>y. (?f has_real_derivative 1 - cos u) (at u)"
+    by (auto intro!: derivative_eq_intros simp: field_simps)
+  then have "?f x \<ge> ?f 0"
+    by (metis cos_le_one diff_ge_0_iff_ge DERIV_nonneg_imp_nondecreasing [OF assms])
   then show "sin x \<le> x" by simp
 qed
 
@@ -4270,11 +4270,10 @@
   shows "sin x \<ge> - x"
 proof -
   let ?f = "\<lambda>x. x + sin x"
-  from x have "?f x \<ge> ?f 0"
-    apply (rule DERIV_nonneg_imp_nondecreasing)
-    apply (intro allI impI exI[of _ "1 + cos x" for x])
-    apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
-    done
+  have \<section>: "\<And>u. \<lbrakk>0 \<le> u; u \<le> x\<rbrakk> \<Longrightarrow> \<exists>y. (?f has_real_derivative 1 + cos u) (at u)"
+    by (auto intro!: derivative_eq_intros simp: field_simps)
+  have "?f x \<ge> ?f 0"
+    by (rule DERIV_nonneg_imp_nondecreasing [OF assms]) (use \<section> real_0_le_add_iff in force)
   then show "sin x \<ge> -x" by simp
 qed
 
@@ -4409,9 +4408,8 @@
   have "cos(3 * x) = cos(2*x + x)"
     by simp
   also have "\<dots> = 4 * cos x ^ 3 - 3 * cos x"
-    apply (simp only: cos_add cos_double sin_double)
-    apply (simp add: * field_simps power2_eq_square power3_eq_cube)
-    done
+    unfolding cos_add cos_double sin_double
+    by (simp add: * field_simps power2_eq_square power3_eq_cube)
   finally show ?thesis .
 qed
 
@@ -4482,12 +4480,18 @@
   by (metis Ints_of_int sin_integer_2pi)
 
 lemma sincos_principal_value: "\<exists>y. (- pi < y \<and> y \<le> pi) \<and> (sin y = sin x \<and> cos y = cos x)"
-  apply (rule exI [where x="pi - (2 * pi) * frac ((pi - x) / (2 * pi))"])
-  apply (auto simp: field_simps frac_lt_1)
-   apply (simp_all add: frac_def field_simps)
-   apply (simp_all add: add_divide_distrib diff_divide_distrib)
-   apply (simp_all add: sin_add cos_add mult.assoc [symmetric])
-  done
+proof -
+  define y where "y \<equiv> pi - (2 * pi) * frac ((pi - x) / (2 * pi))"
+  have "-pi < y"" y \<le> pi"
+    by (auto simp: field_simps frac_lt_1 y_def)
+  moreover
+  have "sin y = sin x" "cos y = cos x"
+    unfolding y_def
+     apply (simp_all add: frac_def divide_simps sin_add cos_add)
+    by (metis sin_int_2pin cos_int_2pin diff_zero add.right_neutral mult.commute mult.left_neutral mult_zero_left)+
+  ultimately
+  show ?thesis by metis
+qed
 
 
 subsection \<open>Tangent\<close>
@@ -5238,10 +5242,11 @@
 qed (use assms isCont_arccos in auto)
 
 lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)"
-proof (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
-  show "(tan has_real_derivative 1 + x\<^sup>2) (at (arctan x))"
-    apply (rule derivative_eq_intros | simp)+
+proof (rule DERIV_inverse_function)
+  have "inverse ((cos (arctan x))\<^sup>2) = 1 + x\<^sup>2"
     by (metis arctan cos_arctan_not_zero power_inverse tan_sec)
+  then show "(tan has_real_derivative 1 + x\<^sup>2) (at (arctan x))"
+    by (auto intro!: derivative_eq_intros)
   show "\<And>y. \<lbrakk>x - 1 < y; y < x + 1\<rbrakk> \<Longrightarrow> tan (arctan y) = y"
     using tan_arctan by blast
   show "1 + x\<^sup>2 \<noteq> 0"
@@ -5999,19 +6004,15 @@
   assumes "x \<noteq> 0"
   shows "arctan (1 / x) = sgn x * pi/2 - arctan x"
 proof (rule arctan_unique)
+  have \<section>: "x > 0 \<Longrightarrow> arctan x < pi"
+    using arctan_bounded [of x] by linarith 
   show "- (pi/2) < sgn x * pi/2 - arctan x"
-    using arctan_bounded [of x] assms
-    unfolding sgn_real_def
-    apply (auto simp: arctan algebra_simps)
-    apply (drule zero_less_arctan_iff [THEN iffD2], arith)
-    done
+    using assms by (auto simp: sgn_real_def arctan algebra_simps \<section>)
   show "sgn x * pi/2 - arctan x < pi/2"
     using arctan_bounded [of "- x"] assms
-    unfolding sgn_real_def arctan_minus
-    by (auto simp: algebra_simps)
+    by (auto simp: algebra_simps sgn_real_def arctan_minus)
   show "tan (sgn x * pi/2 - arctan x) = 1 / x"
-    unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
-    unfolding sgn_real_def
+    unfolding tan_inverse [of "arctan x", unfolded tan_arctan] sgn_real_def
     by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
 qed
 
@@ -6032,18 +6033,18 @@
   by (rule power2_le_imp_le [OF _ zero_le_one])
     (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
 
-lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]
-
-lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
-
 lemma polar_Ex: "\<exists>r::real. \<exists>a. x = r * cos a \<and> y = r * sin a"
 proof -
-  have polar_ex1: "0 < y \<Longrightarrow> \<exists>r a. x = r * cos a \<and> y = r * sin a" for y
-    apply (rule exI [where x = "sqrt (x\<^sup>2 + y\<^sup>2)"])
-    apply (rule exI [where x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))"])
-    apply (simp add: cos_arccos_lemma1 sin_arccos_lemma1 power_divide
-        real_sqrt_mult [symmetric] right_diff_distrib)
-    done
+  have polar_ex1: "\<exists>r a. x = r * cos a \<and> y = r * sin a" if "0 < y" for y
+  proof -
+    have "x = sqrt (x\<^sup>2 + y\<^sup>2) * cos (arccos (x / sqrt (x\<^sup>2 + y\<^sup>2)))"
+      by (simp add: cos_arccos_abs [OF cos_x_y_le_one])
+    moreover have "y = sqrt (x\<^sup>2 + y\<^sup>2) * sin (arccos (x / sqrt (x\<^sup>2 + y\<^sup>2)))"
+      using that
+      by (simp add: sin_arccos_abs [OF cos_x_y_le_one] power_divide right_diff_distrib flip: real_sqrt_mult)
+    ultimately show ?thesis
+      by blast
+  qed
   show ?thesis
   proof (cases "0::real" y rule: linorder_cases)
     case less
@@ -6083,24 +6084,24 @@
   assumes m: "\<And>i. i > m \<Longrightarrow> a i = 0"
     and n: "\<And>j. j > n \<Longrightarrow> b j = 0"
   shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) =
-    (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
-proof -
+         (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
+proof -
+  have "\<And>i j. \<lbrakk>m + n - i < j; a i \<noteq> 0\<rbrakk> \<Longrightarrow> b j = 0"
+    by (meson le_add_diff leI le_less_trans m n)
+  then have \<section>: "(\<Sum>(i,j)\<in>(SIGMA i:{..m+n}. {m+n - i<..m+n}). a i * x ^ i * (b j * x ^ j)) = 0"
+    by (clarsimp simp add: sum_Un Sigma_interval_disjoint intro!: sum.neutral)
   have "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) = (\<Sum>i\<le>m. \<Sum>j\<le>n. (a i * x ^ i) * (b j * x ^ j))"
     by (rule sum_product)
   also have "\<dots> = (\<Sum>i\<le>m + n. \<Sum>j\<le>n + m. a i * x ^ i * (b j * x ^ j))"
     using assms by (auto simp: sum_up_index_split)
   also have "\<dots> = (\<Sum>r\<le>m + n. \<Sum>j\<le>m + n - r. a r * x ^ r * (b j * x ^ j))"
-    apply (simp add: add_ac sum.Sigma product_atMost_eq_Un)
-    apply (clarsimp simp add: sum_Un Sigma_interval_disjoint intro!: sum.neutral)
-    apply (metis add_diff_assoc2 add.commute add_lessD1 leD m n nat_le_linear neqE)
-    done
+    by (simp add: add_ac sum.Sigma product_atMost_eq_Un sum_Un Sigma_interval_disjoint \<section>)
   also have "\<dots> = (\<Sum>(i,j)\<in>{(i,j). i+j \<le> m+n}. (a i * x ^ i) * (b j * x ^ j))"
     by (auto simp: pairs_le_eq_Sigma sum.Sigma)
+  also have "... = (\<Sum>k\<le>m + n. \<Sum>i\<le>k. a i * x ^ i * (b (k - i) * x ^ (k - i)))"
+    by (rule sum.triangle_reindex_eq)
   also have "\<dots> = (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
-    apply (subst sum.triangle_reindex_eq)
-    apply (auto simp: algebra_simps sum_distrib_left intro!: sum.cong)
-    apply (metis le_add_diff_inverse power_add)
-    done
+    by (auto simp: algebra_simps sum_distrib_left simp flip: power_add intro!: sum.cong)
   finally show ?thesis .
 qed
 
@@ -6109,7 +6110,7 @@
   assumes m: "\<And>i. i > m \<Longrightarrow> a i = 0"
     and n: "\<And>j. j > n \<Longrightarrow> b j = 0"
   shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) =
-    (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
+         (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
   using polynomial_product [of m a n b x] assms
   by (simp only: of_nat_mult [symmetric] of_nat_power [symmetric]
       of_nat_eq_iff Int.int_sum [symmetric])
@@ -6148,10 +6149,10 @@
   have "(\<Sum>i=Suc j..n. a i * y^(i - j - 1)) = (\<Sum>k<n-j. a(j+k+1) * y^k)"
     if "j < n" for j :: nat
   proof -
-    have h: "bij_betw (\<lambda>i. i - (j + 1)) {Suc j..n} (lessThan (n-j))"
-      apply (auto simp: bij_betw_def inj_on_def)
-      apply (rule_tac x="x + Suc j" in image_eqI, auto)
-      done
+    have "\<And>k. k < n - j \<Longrightarrow> k \<in> (\<lambda>i. i - Suc j) ` {Suc j..n}"
+      by (rule_tac x="k + Suc j" in image_eqI, auto)
+    then have h: "bij_betw (\<lambda>i. i - (j + 1)) {Suc j..n} (lessThan (n-j))"
+      by (auto simp: bij_betw_def inj_on_def)
     then show ?thesis
       by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_simp)
   qed