# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1585493094 -3600
# Node ID a9de39608b1a887866f379b8dd05f893be10e3da
# Parent  74c874b5aed0165c9be0a23162fda889363b014b
more tidying up of old apply-proofs

diff -r 74c874b5aed0 -r a9de39608b1a src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sat Mar 28 21:54:31 2020 +0100
+++ b/src/HOL/Fun.thy	Sun Mar 29 15:44:54 2020 +0100
@@ -738,7 +738,7 @@
   by (simp add: fun_eq_iff)
 
 lemma fun_upd_twist: "a \<noteq> c \<Longrightarrow> (m(a := b))(c := d) = (m(c := d))(a := b)"
-  by (rule ext) auto
+  by auto
 
 lemma inj_on_fun_updI: "inj_on f A \<Longrightarrow> y \<notin> f ` A \<Longrightarrow> inj_on (f(x := y)) A"
   by (auto simp: inj_on_def)
diff -r 74c874b5aed0 -r a9de39608b1a src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sat Mar 28 21:54:31 2020 +0100
+++ b/src/HOL/Int.thy	Sun Mar 29 15:44:54 2020 +0100
@@ -136,21 +136,23 @@
     by (cases "k = 0") (simp_all add: distrib_right add_strict_mono)
 qed
 
-lemma zero_le_imp_eq_int: "0 \<le> k \<Longrightarrow> \<exists>n. k = int n"
-  for k :: int
-  apply transfer
-  apply clarsimp
-  apply (rule_tac x="a - b" in exI)
-  apply simp
-  done
+lemma zero_le_imp_eq_int:
+  assumes "k \<ge> (0::int)" shows "\<exists>n. k = int n"
+proof -
+  have "b \<le> a \<Longrightarrow> \<exists>n::nat. a = n + b" for a b
+    by (rule_tac x="a - b" in exI) simp
+  with assms show ?thesis
+    by transfer auto
+qed
 
-lemma zero_less_imp_eq_int: "0 < k \<Longrightarrow> \<exists>n>0. k = int n"
-  for k :: int
-  apply transfer
-  apply clarsimp
-  apply (rule_tac x="a - b" in exI)
-  apply simp
-  done
+lemma zero_less_imp_eq_int:
+  assumes "k > (0::int)" shows "\<exists>n>0. k = int n"
+proof -
+  have "b < a \<Longrightarrow> \<exists>n::nat. n>0 \<and> a = n + b" for a b
+    by (rule_tac x="a - b" in exI) simp
+  with assms show ?thesis
+    by transfer auto
+qed
 
 lemma zmult_zless_mono2: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
   for i j k :: int
@@ -185,12 +187,12 @@
 
 lemma zless_iff_Suc_zadd: "w < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
   for w z :: int
-  apply transfer
-  apply auto
-  apply (rename_tac a b c d)
-  apply (rule_tac x="c+b - Suc(a+d)" in exI)
-  apply arith
-  done
+proof -
+  have "\<And>a b c d. a + d < c + b \<Longrightarrow> \<exists>n. c + b = Suc (a + n + d)"
+    by (rule_tac x="c+b - Suc(a+d)" in exI) arith
+  then show ?thesis
+    by transfer auto
+qed
 
 lemma zabs_less_one_iff [simp]: "\<bar>z\<bar> < 1 \<longleftrightarrow> z = 0" (is "?lhs \<longleftrightarrow> ?rhs")
   for z :: int
@@ -471,16 +473,16 @@
 qed
 
 instance int :: no_top
-  apply standard
-  apply (rule_tac x="x + 1" in exI)
-  apply simp
-  done
+proof
+  show "\<And>x::int. \<exists>y. x < y"
+    by (rule_tac x="x + 1" in exI) simp
+qed
 
 instance int :: no_bot
-  apply standard
-  apply (rule_tac x="x - 1" in exI)
-  apply simp
-  done
+proof
+  show "\<And>x::int. \<exists>y. y < x"
+    by (rule_tac x="x - 1" in exI) simp
+qed
 
 
 subsection \<open>Magnitude of an Integer, as a Natural Number: \<open>nat\<close>\<close>
@@ -732,12 +734,14 @@
   for a :: "'a::linordered_idom"
   by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
 
-lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
-  apply transfer
-  apply clarsimp
-  apply (rule_tac x="b - Suc a" in exI)
-  apply arith
-  done
+lemma negD:
+  assumes "x < 0" shows "\<exists>n. x = - (int (Suc n))"
+proof -
+  have "\<And>a b. a < b \<Longrightarrow> \<exists>n. Suc (a + n) = b"
+    by (rule_tac x="b - Suc a" in exI) arith
+  with assms show ?thesis
+    by transfer auto
+qed
 
 
 subsection \<open>Cases and induction\<close>
@@ -754,13 +758,17 @@
 
 text \<open>This is the default, with a negative case.\<close>
 lemma int_cases [case_names nonneg neg, cases type: int]:
-  "(\<And>n. z = int n \<Longrightarrow> P) \<Longrightarrow> (\<And>n. z = - (int (Suc n)) \<Longrightarrow> P) \<Longrightarrow> P"
-  apply (cases "z < 0")
-   apply (blast dest!: negD)
-  apply (simp add: linorder_not_less del: of_nat_Suc)
-  apply auto
-  apply (blast dest: nat_0_le [THEN sym])
-  done
+  assumes pos: "\<And>n. z = int n \<Longrightarrow> P" and neg: "\<And>n. z = - (int (Suc n)) \<Longrightarrow> P"
+  shows P
+proof (cases "z < 0")
+  case True
+  with neg show ?thesis
+    by (blast dest!: negD)
+next
+  case False
+  with pos show ?thesis
+    by (force simp add: linorder_not_less dest: nat_0_le [THEN sym])
+qed
 
 lemma int_cases3 [case_names zero pos neg]:
   fixes k :: int
@@ -891,31 +899,19 @@
   by (subst of_nat_numeral [symmetric], rule Ints_of_nat)
 
 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
-  apply (auto simp add: Ints_def)
-  apply (rule range_eqI)
-  apply (rule of_int_add [symmetric])
-  done
+  by (force simp add: Ints_def simp flip: of_int_add intro: range_eqI)
 
 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
-  apply (auto simp add: Ints_def)
-  apply (rule range_eqI)
-  apply (rule of_int_minus [symmetric])
-  done
+  by (force simp add: Ints_def simp flip: of_int_minus intro: range_eqI)
 
 lemma minus_in_Ints_iff: "-x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
   using Ints_minus[of x] Ints_minus[of "-x"] by auto
 
 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
-  apply (auto simp add: Ints_def)
-  apply (rule range_eqI)
-  apply (rule of_int_diff [symmetric])
-  done
+  by (force simp add: Ints_def simp flip: of_int_diff intro: range_eqI)
 
 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
-  apply (auto simp add: Ints_def)
-  apply (rule range_eqI)
-  apply (rule of_int_mult [symmetric])
-  done
+  by (force simp add: Ints_def simp flip: of_int_mult intro: range_eqI)
 
 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
   by (induct n) simp_all
@@ -1234,12 +1230,15 @@
          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
 qed
 
-lemma nat_mult_distrib_neg: "z \<le> 0 \<Longrightarrow> nat (z * z') = nat (- z) * nat (- z')"
-  for z z' :: int
-  apply (rule trans)
-   apply (rule_tac [2] nat_mult_distrib)
-   apply auto
-  done
+lemma nat_mult_distrib_neg:
+  assumes "z \<le> (0::int)" shows "nat (z * z') = nat (- z) * nat (- z')" (is "?L = ?R")
+proof -
+  have "?L = nat (- z * - z')"
+    using assms by auto
+  also have "... = ?R"
+    by (rule nat_mult_distrib) (use assms in auto)
+  finally show ?thesis .
+qed
 
 lemma nat_abs_mult_distrib: "nat \<bar>w * z\<bar> = nat \<bar>w\<bar> * nat \<bar>z\<bar>"
   by (cases "z = 0 \<or> w = 0")
@@ -1332,16 +1331,14 @@
 (* `set:int': dummy construction *)
 theorem int_gr_induct [case_names base step, induct set: int]:
   fixes i k :: int
-  assumes gr: "k < i"
-    and base: "P (k + 1)"
-    and step: "\<And>i. k < i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
+  assumes "k < i" "P (k + 1)" "\<And>i. k < i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
   shows "P i"
-  apply (rule int_ge_induct[of "k + 1"])
-  using gr apply arith
-   apply (rule base)
-  apply (rule step)
-   apply simp_all
-  done
+proof -
+  have "k+1 \<le> i"
+    using assms by auto
+  then show ?thesis
+    by (induction i rule: int_ge_induct) (auto simp: assms)
+qed
 
 theorem int_le_induct [consumes 1, case_names base step]:
   fixes i k :: int
@@ -1367,16 +1364,14 @@
 
 theorem int_less_induct [consumes 1, case_names base step]:
   fixes i k :: int
-  assumes less: "i < k"
-    and base: "P (k - 1)"
-    and step: "\<And>i. i < k \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
+  assumes "i < k" "P (k - 1)" "\<And>i. i < k \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
   shows "P i"
-  apply (rule int_le_induct[of _ "k - 1"])
-  using less apply arith
-   apply (rule base)
-  apply (rule step)
-   apply simp_all
-  done
+proof -
+  have "i \<le> k-1"
+    using assms by auto
+  then show ?thesis
+    by (induction i rule: int_le_induct) (auto simp: assms)
+qed
 
 theorem int_induct [case_names base step1 step2]:
   fixes k :: int
@@ -1401,26 +1396,30 @@
 
 subsection \<open>Intermediate value theorems\<close>
 
+lemma nat_ivt_aux: 
+  "\<lbrakk>\<forall>i<n. \<bar>f (Suc i) - f i\<bar> \<le> 1; f 0 \<le> k; k \<le> f n\<rbrakk> \<Longrightarrow> \<exists>i \<le> n. f i = k"
+  for m n :: nat and k :: int
+proof (induct n)
+  case (Suc n)
+  show ?case
+  proof (cases "k = f (Suc n)")
+    case False
+    with Suc have "k \<le> f n"
+      by auto
+    with Suc show ?thesis
+      by (auto simp add: abs_if split: if_split_asm intro: le_SucI)
+  qed (use Suc in auto)
+qed auto
+
 lemma nat_intermed_int_val:
-  "\<exists>i. m \<le> i \<and> i \<le> n \<and> f i = k"
-  if "\<forall>i. m \<le> i \<and> i < n \<longrightarrow> \<bar>f (Suc i) - f i\<bar> \<le> 1"
-    "m \<le> n" "f m \<le> k" "k \<le> f n"
-  for m n :: nat and k :: int
+  fixes m n :: nat and k :: int
+  assumes "\<forall>i. m \<le> i \<and> i < n \<longrightarrow> \<bar>f (Suc i) - f i\<bar> \<le> 1" "m \<le> n" "f m \<le> k" "k \<le> f n"
+  shows "\<exists>i. m \<le> i \<and> i \<le> n \<and> f i = k"
 proof -
-  have "(\<forall>i<n. \<bar>f (Suc i) - f i\<bar> \<le> 1) \<Longrightarrow> f 0 \<le> k \<Longrightarrow> k \<le> f n
-    \<Longrightarrow> (\<exists>i \<le> n. f i = k)"
-  for n :: nat and f
-    apply (induct n)
-     apply auto
-    apply (erule_tac x = n in allE)
-    apply (case_tac "k = f (Suc n)")
-     apply (auto simp add: abs_if split: if_split_asm intro: le_SucI)
-    done
-  from this [of "n - m" "f \<circ> plus m"] that show ?thesis
-    apply auto
-    apply (rule_tac x = "m + i" in exI)
-    apply auto
-    done
+  obtain i where "i \<le> n - m" "k = f (m + i)"
+    using nat_ivt_aux [of "n - m" "f \<circ> plus m" k] assms by auto
+  with assms show ?thesis
+    by (rule_tac x = "m + i" in exI) auto
 qed
 
 lemma nat0_intermed_int_val:
@@ -1465,14 +1464,12 @@
     by (auto dest: pos_zmult_eq_1_iff_lemma)
 qed
 
-lemma zmult_eq_1_iff: "m * n = 1 \<longleftrightarrow> (m = 1 \<and> n = 1) \<or> (m = - 1 \<and> n = - 1)"
+lemma zmult_eq_1_iff: "m * n = 1 \<longleftrightarrow> (m = 1 \<and> n = 1) \<or> (m = - 1 \<and> n = - 1)" (is "?L = ?R")
   for m n :: int
-  apply (rule iffI)
-   apply (frule pos_zmult_eq_1_iff_lemma)
-   apply (simp add: mult.commute [of m])
-   apply (frule pos_zmult_eq_1_iff_lemma)
-   apply auto
-  done
+proof
+  assume L: ?L show ?R
+    using pos_zmult_eq_1_iff_lemma [OF L] L by force
+qed auto
 
 lemma infinite_UNIV_int [simp]: "\<not> finite (UNIV::int set)"
 proof
@@ -1677,13 +1674,12 @@
   using nat_less_eq_zless[of a "numeral x ^ n"]
   by (cases "a < 0") (auto simp: nat_power_eq less_le_trans[where y=0])
 
-lemma zdvd_imp_le: "z dvd n \<Longrightarrow> 0 < n \<Longrightarrow> z \<le> n"
-  for n z :: int
-  apply (cases n)
-  apply auto
-  apply (cases z)
-   apply (auto simp add: dvd_imp_le)
-  done
+lemma zdvd_imp_le: "z \<le> n" if "z dvd n" "0 < n" for n z :: int
+proof (cases n)
+  case (nonneg n)
+  show ?thesis
+    by (cases z) (use nonneg dvd_imp_le that in auto)
+qed (use that in auto)
 
 lemma zdvd_period:
   fixes a d :: int
diff -r 74c874b5aed0 -r a9de39608b1a src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sat Mar 28 21:54:31 2020 +0100
+++ b/src/HOL/Map.thy	Sun Mar 29 15:44:54 2020 +0100
@@ -110,18 +110,19 @@
 
 lemma map_upd_Some_unfold:
   "((m(a\<mapsto>b)) x = Some y) = (x = a \<and> b = y \<or> x \<noteq> a \<and> m x = Some y)"
-by auto
+  by auto
 
 lemma image_map_upd [simp]: "x \<notin> A \<Longrightarrow> m(x \<mapsto> y) ` A = m ` A"
-by auto
+  by auto
 
-lemma finite_range_updI: "finite (range f) \<Longrightarrow> finite (range (f(a\<mapsto>b)))"
-unfolding image_def
-apply (simp (no_asm_use) add:full_SetCompr_eq)
-apply (rule finite_subset)
- prefer 2 apply assumption
-apply (auto)
-done
+lemma finite_range_updI:
+  assumes "finite (range f)" shows "finite (range (f(a\<mapsto>b)))"
+proof -
+  have "range (f(a\<mapsto>b)) \<subseteq> insert (Some b) (range f)"
+    by auto
+  then show ?thesis
+    by (rule finite_subset) (use assms in auto)
+qed
 
 
 subsection \<open>@{term [source] map_of}\<close>
@@ -143,21 +144,19 @@
 
 lemma map_of_eq_Some_iff [simp]:
   "distinct(map fst xys) \<Longrightarrow> (map_of xys x = Some y) = ((x,y) \<in> set xys)"
-apply (induct xys)
- apply simp
-apply (auto simp: map_of_eq_None_iff [symmetric])
-done
+proof (induct xys)
+  case (Cons xy xys)
+  then show ?case
+    by (cases xy) (auto simp flip: map_of_eq_None_iff)
+qed auto
 
 lemma Some_eq_map_of_iff [simp]:
   "distinct(map fst xys) \<Longrightarrow> (Some y = map_of xys x) = ((x,y) \<in> set xys)"
 by (auto simp del: map_of_eq_Some_iff simp: map_of_eq_Some_iff [symmetric])
 
-lemma map_of_is_SomeI [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
-    \<Longrightarrow> map_of xys x = Some y"
-apply (induct xys)
- apply simp
-apply force
-done
+lemma map_of_is_SomeI [simp]: 
+  "\<lbrakk>distinct(map fst xys); (x,y) \<in> set xys\<rbrakk> \<Longrightarrow> map_of xys x = Some y"
+  by simp
 
 lemma map_of_zip_is_None [simp]:
   "length xs = length ys \<Longrightarrow> (map_of (zip xs ys) x = None) = (x \<notin> set xs)"
@@ -233,12 +232,11 @@
   by (induct xs) (simp_all add: fun_eq_iff)
 
 lemma finite_range_map_of: "finite (range (map_of xys))"
-apply (induct xys)
- apply (simp_all add: image_constant)
-apply (rule finite_subset)
- prefer 2 apply assumption
-apply auto
-done
+proof (induct xys)
+  case (Cons a xys)
+  then show ?case
+    using finite_range_updI by fastforce
+qed auto
 
 lemma map_of_SomeD: "map_of xs k = Some y \<Longrightarrow> (k, y) \<in> set xs"
   by (induct xs) (auto split: if_splits)
@@ -334,23 +332,24 @@
 by (rule ext) (auto simp: map_add_def dom_def split: option.split)
 
 lemma map_of_append[simp]: "map_of (xs @ ys) = map_of ys ++ map_of xs"
-unfolding map_add_def
-apply (induct xs)
- apply simp
-apply (rule ext)
-apply (simp split: option.split)
-done
+  unfolding map_add_def
+proof (induct xs)
+  case (Cons a xs)
+  then show ?case
+    by (force split: option.split)
+qed auto
 
 lemma finite_range_map_of_map_add:
   "finite (range f) \<Longrightarrow> finite (range (f ++ map_of l))"
-apply (induct l)
- apply (auto simp del: fun_upd_apply)
-apply (erule finite_range_updI)
-done
+proof (induct l)
+case (Cons a l)
+  then show ?case
+    by (metis finite_range_updI map_add_upd map_of.simps(2))
+qed auto
 
 lemma inj_on_map_add_dom [iff]:
   "inj_on (m ++ m') (dom m') = inj_on m' (dom m')"
-by (fastforce simp: map_add_def dom_def inj_on_def split: option.splits)
+  by (fastforce simp: map_add_def dom_def inj_on_def split: option.splits)
 
 lemma map_upds_fold_map_upd:
   "m(ks[\<mapsto>]vs) = foldl (\<lambda>m (k, v). m(k \<mapsto> v)) m (zip ks vs)"
@@ -369,46 +368,46 @@
 subsection \<open>@{term [source] restrict_map}\<close>
 
 lemma restrict_map_to_empty [simp]: "m|`{} = empty"
-by (simp add: restrict_map_def)
+  by (simp add: restrict_map_def)
 
 lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
-by (auto simp: restrict_map_def)
+  by (auto simp: restrict_map_def)
 
 lemma restrict_map_empty [simp]: "empty|`D = empty"
-by (simp add: restrict_map_def)
+  by (simp add: restrict_map_def)
 
 lemma restrict_in [simp]: "x \<in> A \<Longrightarrow> (m|`A) x = m x"
-by (simp add: restrict_map_def)
+  by (simp add: restrict_map_def)
 
 lemma restrict_out [simp]: "x \<notin> A \<Longrightarrow> (m|`A) x = None"
-by (simp add: restrict_map_def)
+  by (simp add: restrict_map_def)
 
 lemma ran_restrictD: "y \<in> ran (m|`A) \<Longrightarrow> \<exists>x\<in>A. m x = Some y"
-by (auto simp: restrict_map_def ran_def split: if_split_asm)
+  by (auto simp: restrict_map_def ran_def split: if_split_asm)
 
 lemma dom_restrict [simp]: "dom (m|`A) = dom m \<inter> A"
-by (auto simp: restrict_map_def dom_def split: if_split_asm)
+  by (auto simp: restrict_map_def dom_def split: if_split_asm)
 
 lemma restrict_upd_same [simp]: "m(x\<mapsto>y)|`(-{x}) = m|`(-{x})"
-by (rule ext) (auto simp: restrict_map_def)
+  by (rule ext) (auto simp: restrict_map_def)
 
 lemma restrict_restrict [simp]: "m|`A|`B = m|`(A\<inter>B)"
-by (rule ext) (auto simp: restrict_map_def)
+  by (rule ext) (auto simp: restrict_map_def)
 
 lemma restrict_fun_upd [simp]:
   "m(x := y)|`D = (if x \<in> D then (m|`(D-{x}))(x := y) else m|`D)"
-by (simp add: restrict_map_def fun_eq_iff)
+  by (simp add: restrict_map_def fun_eq_iff)
 
 lemma fun_upd_None_restrict [simp]:
   "(m|`D)(x := None) = (if x \<in> D then m|`(D - {x}) else m|`D)"
-by (simp add: restrict_map_def fun_eq_iff)
+  by (simp add: restrict_map_def fun_eq_iff)
 
 lemma fun_upd_restrict: "(m|`D)(x := y) = (m|`(D-{x}))(x := y)"
-by (simp add: restrict_map_def fun_eq_iff)
+  by (simp add: restrict_map_def fun_eq_iff)
 
 lemma fun_upd_restrict_conv [simp]:
   "x \<in> D \<Longrightarrow> (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
-by (simp add: restrict_map_def fun_eq_iff)
+  by (rule fun_upd_restrict)
 
 lemma map_of_map_restrict:
   "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
@@ -416,47 +415,62 @@
 
 lemma restrict_complement_singleton_eq:
   "f |` (- {x}) = f(x := None)"
-  by (simp add: restrict_map_def fun_eq_iff)
+  by auto
 
 
 subsection \<open>@{term [source] map_upds}\<close>
 
 lemma map_upds_Nil1 [simp]: "m([] [\<mapsto>] bs) = m"
-by (simp add: map_upds_def)
+  by (simp add: map_upds_def)
 
 lemma map_upds_Nil2 [simp]: "m(as [\<mapsto>] []) = m"
-by (simp add:map_upds_def)
+  by (simp add:map_upds_def)
 
 lemma map_upds_Cons [simp]: "m(a#as [\<mapsto>] b#bs) = (m(a\<mapsto>b))(as[\<mapsto>]bs)"
-by (simp add:map_upds_def)
+  by (simp add:map_upds_def)
 
-lemma map_upds_append1 [simp]: "size xs < size ys \<Longrightarrow>
-  m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
-apply(induct xs arbitrary: ys m)
- apply (clarsimp simp add: neq_Nil_conv)
-apply (case_tac ys)
- apply simp
-apply simp
-done
+lemma map_upds_append1 [simp]:
+  "size xs < size ys \<Longrightarrow> m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
+proof (induct xs arbitrary: ys m)
+  case Nil
+  then show ?case
+    by (auto simp: neq_Nil_conv)
+next
+  case (Cons a xs)
+  then show ?case
+    by (cases ys) auto
+qed
 
 lemma map_upds_list_update2_drop [simp]:
   "size xs \<le> i \<Longrightarrow> m(xs[\<mapsto>]ys[i:=y]) = m(xs[\<mapsto>]ys)"
-apply (induct xs arbitrary: m ys i)
- apply simp
-apply (case_tac ys)
- apply simp
-apply (simp split: nat.split)
-done
+proof (induct xs arbitrary: m ys i)
+  case Nil
+  then show ?case
+    by auto
+next
+  case (Cons a xs)
+  then show ?case
+    by (cases ys) (use Cons in \<open>auto split: nat.split\<close>)
+qed
 
+text \<open>Something weirdly sensitive about this proof, which needs only four lines in apply style\<close>
 lemma map_upd_upds_conv_if:
   "(f(x\<mapsto>y))(xs [\<mapsto>] ys) =
    (if x \<in> set(take (length ys) xs) then f(xs [\<mapsto>] ys)
                                     else (f(xs [\<mapsto>] ys))(x\<mapsto>y))"
-apply (induct xs arbitrary: x y ys f)
- apply simp
-apply (case_tac ys)
- apply (auto split: if_split simp: fun_upd_twist)
-done
+proof (induct xs arbitrary: x y ys f)
+  case (Cons a xs)
+  show ?case
+  proof (cases ys)
+    case (Cons z zs)
+    then show ?thesis
+      using Cons.hyps
+      apply (auto split: if_split simp: fun_upd_twist)
+      using Cons.hyps apply fastforce+
+      done
+  qed auto
+qed auto
+
 
 lemma map_upds_twist [simp]:
   "a \<notin> set as \<Longrightarrow> m(a\<mapsto>b)(as[\<mapsto>]bs) = m(as[\<mapsto>]bs)(a\<mapsto>b)"
@@ -464,39 +478,42 @@
 
 lemma map_upds_apply_nontin [simp]:
   "x \<notin> set xs \<Longrightarrow> (f(xs[\<mapsto>]ys)) x = f x"
-apply (induct xs arbitrary: ys)
- apply simp
-apply (case_tac ys)
- apply (auto simp: map_upd_upds_conv_if)
-done
+proof (induct xs arbitrary: ys)
+  case (Cons a xs)
+  then show ?case
+    by (cases ys) (auto simp: map_upd_upds_conv_if)
+qed auto
 
 lemma fun_upds_append_drop [simp]:
   "size xs = size ys \<Longrightarrow> m(xs@zs[\<mapsto>]ys) = m(xs[\<mapsto>]ys)"
-apply (induct xs arbitrary: m ys)
- apply simp
-apply (case_tac ys)
- apply simp_all
-done
+proof (induct xs arbitrary: ys)
+  case (Cons a xs)
+  then show ?case
+    by (cases ys) (auto simp: map_upd_upds_conv_if)
+qed auto
 
 lemma fun_upds_append2_drop [simp]:
   "size xs = size ys \<Longrightarrow> m(xs[\<mapsto>]ys@zs) = m(xs[\<mapsto>]ys)"
-apply (induct xs arbitrary: m ys)
- apply simp
-apply (case_tac ys)
- apply simp_all
-done
-
+proof (induct xs arbitrary: ys)
+  case (Cons a xs)
+  then show ?case
+    by (cases ys) (auto simp: map_upd_upds_conv_if)
+qed auto
 
 lemma restrict_map_upds[simp]:
   "\<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
     \<Longrightarrow> m(xs [\<mapsto>] ys)|`D = (m|`(D - set xs))(xs [\<mapsto>] ys)"
-apply (induct xs arbitrary: m ys)
- apply simp
-apply (case_tac ys)
- apply simp
-apply (simp add: Diff_insert [symmetric] insert_absorb)
-apply (simp add: map_upd_upds_conv_if)
-done
+proof (induct xs arbitrary: m ys)
+  case (Cons a xs)
+  then show ?case
+  proof (cases ys)
+    case (Cons z zs)
+    with Cons.hyps Cons.prems show ?thesis
+      apply (simp add: insert_absorb flip: Diff_insert)
+      apply (auto simp add: map_upd_upds_conv_if)
+      done
+  qed auto
+qed auto
 
 
 subsection \<open>@{term [source] dom}\<close>
@@ -537,11 +554,12 @@
 
 lemma dom_map_upds [simp]:
   "dom(m(xs[\<mapsto>]ys)) = set(take (length ys) xs) \<union> dom m"
-apply (induct xs arbitrary: m ys)
- apply simp
-apply (case_tac ys)
- apply auto
-done
+proof (induct xs arbitrary: ys)
+  case (Cons a xs)
+  then show ?case
+    by (cases ys) (auto simp: map_upd_upds_conv_if)
+qed auto
+
 
 lemma dom_map_add [simp]: "dom (m ++ n) = dom n \<union> dom m"
   by (auto simp: dom_def)
@@ -638,12 +656,9 @@
 lemma ran_empty [simp]: "ran empty = {}"
   by (auto simp: ran_def)
 
-lemma ran_map_upd [simp]: "m a = None \<Longrightarrow> ran(m(a\<mapsto>b)) = insert b (ran m)"
+lemma ran_map_upd [simp]:  "m a = None \<Longrightarrow> ran(m(a\<mapsto>b)) = insert b (ran m)"
   unfolding ran_def
-apply auto
-apply (subgoal_tac "aa \<noteq> a")
- apply auto
-done
+  by force
 
 lemma ran_map_add:
   assumes "dom m1 \<inter> dom m2 = {}"
@@ -712,11 +727,11 @@
 
 lemma map_le_upds [simp]:
   "f \<subseteq>\<^sub>m g \<Longrightarrow> f(as [\<mapsto>] bs) \<subseteq>\<^sub>m g(as [\<mapsto>] bs)"
-apply (induct as arbitrary: f g bs)
- apply simp
-apply (case_tac bs)
- apply auto
-done
+proof (induct as arbitrary: f g bs)
+  case (Cons a as)
+  then show ?case
+    by (cases bs) (use Cons in auto)
+qed auto
 
 lemma map_le_implies_dom_le: "(f \<subseteq>\<^sub>m g) \<Longrightarrow> (dom f \<subseteq> dom g)"
   by (fastforce simp add: map_le_def dom_def)
@@ -728,11 +743,8 @@
   by (auto simp add: map_le_def dom_def)
 
 lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
-unfolding map_le_def
-apply (rule ext)
-apply (case_tac "x \<in> dom f", simp)
-apply (case_tac "x \<in> dom g", simp, fastforce)
-done
+  unfolding map_le_def
+  by (metis ext domIff)
 
 lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m g ++ f"
   by (fastforce simp: map_le_def)