# HG changeset patch
# User wenzelm
# Date 1586204980 -7200
# Node ID 23abd7f9f054a55e9690ce3ec298ed1774dc2b5f
# Parent  54ac957c53ec171362ec0eb2ccb17d9e93d547b3# Parent  8e5c20e4e11a35c4dbe0f256c659823e3d16e434
merged;

diff -r 54ac957c53ec -r 23abd7f9f054 src/HOL/Analysis/Lipschitz.thy
--- a/src/HOL/Analysis/Lipschitz.thy	Mon Apr 06 22:28:41 2020 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy	Mon Apr 06 22:29:40 2020 +0200
@@ -686,11 +686,14 @@
         using lx'(2) ly'(2) lt'(2) \<open>0 < rx _\<close>
         by (auto simp add: field_split_simps strict_mono_def)
       also have "\<dots> \<le> diameter ?S / n"
-        by (force intro!: \<open>0 < n\<close> strict_mono_def xy diameter_bounded_bound frac_le
-          compact_imp_bounded compact t
-          intro: le_trans[OF seq_suble[OF lt'(2)]]
-            le_trans[OF seq_suble[OF ly'(2)]]
-            le_trans[OF seq_suble[OF lx'(2)]])
+      proof (rule frac_le)
+        show "diameter ?S \<ge> 0"
+          using compact compact_imp_bounded diameter_ge_0 by blast
+        show "dist (f (?t n) (?y n)) (f (?t n) (?x n)) \<le> diameter ((\<lambda>(t,x). f t x) ` (T \<times> X))"
+          by (metis (no_types) compact compact_imp_bounded diameter_bounded_bound image_eqI mem_Sigma_iff o_apply split_conv t xy(1) xy(2))
+        show "real n \<le> real (rx (ry (rt n)))"
+          by (meson le_trans lt'(2) lx'(2) ly'(2) of_nat_mono strict_mono_imp_increasing)
+      qed (use \<open>n > 0\<close> in auto)
       also have "\<dots> \<le> abs (diameter ?S) / n"
         by (auto intro!: divide_right_mono)
       finally show ?case by simp
diff -r 54ac957c53ec -r 23abd7f9f054 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Mon Apr 06 22:28:41 2020 +0200
+++ b/src/HOL/Binomial.thy	Mon Apr 06 22:29:40 2020 +0200
@@ -121,21 +121,35 @@
   using binomial_Suc_Suc [of "n - 1" "k - 1"] by simp
 
 lemma Suc_times_binomial_eq: "Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
-  apply (induct n arbitrary: k)
-   apply simp
-   apply arith
-  apply (case_tac k)
-   apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
-  done
+proof (induction n arbitrary: k)
+  case 0
+  then show ?case
+    by auto
+next
+  case (Suc n)
+  show ?case 
+  proof (cases k)
+    case (Suc k')
+    then show ?thesis
+      using Suc.IH
+      by (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
+  qed auto
+qed
 
 lemma binomial_le_pow2: "n choose k \<le> 2^n"
-  apply (induct n arbitrary: k)
-   apply (case_tac k)
-    apply simp_all
-  apply (case_tac k)
-   apply auto
-  apply (simp add: add_le_mono mult_2)
-  done
+proof (induction n arbitrary: k)
+  case 0
+  then show ?case
+    using le_less less_le_trans by fastforce
+next
+  case (Suc n)
+  show ?case
+  proof (cases k)
+    case (Suc k')
+    then show ?thesis
+      using Suc.IH by (simp add: add_le_mono mult_2)
+  qed auto
+qed
 
 text \<open>The absorption property.\<close>
 lemma Suc_times_binomial: "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)"
@@ -246,9 +260,7 @@
   assumes kn: "k \<le> n"
   shows "(of_nat (n choose k) :: 'a::field_char_0) = fact n / (fact k * fact (n - k))"
   using binomial_fact_lemma[OF kn]
-  apply (simp add: field_simps)
-  apply (metis mult.commute of_nat_fact of_nat_mult)
-  done
+  by (metis (mono_tags, lifting) fact_nonzero mult_eq_0_iff nonzero_mult_div_cancel_left of_nat_fact of_nat_mult)
 
 lemma fact_binomial:
   assumes "k \<le> n"
@@ -361,11 +373,11 @@
   for a :: "'a::field_char_0"
 proof (cases k)
   case (Suc k')
+  then have "a gchoose k = pochhammer (a - of_nat k') (Suc k') / ((1 + of_nat k') * fact k')"
+    by (simp add: gbinomial_prod_rev pochhammer_prod_rev atLeastLessThanSuc_atLeastAtMost
+        prod.atLeast_Suc_atMost_Suc_shift of_nat_diff flip: power_mult_distrib prod.cl_ivl_Suc)
   then show ?thesis
-    apply (simp add: pochhammer_minus)
-    apply (simp add: gbinomial_prod_rev pochhammer_prod_rev power_mult_distrib [symmetric] atLeastLessThanSuc_atLeastAtMost
-        prod.atLeast_Suc_atMost_Suc_shift of_nat_diff del: prod.cl_ivl_Suc)
-    done
+    by (simp add: pochhammer_minus Suc)
 qed auto
 
 lemma gbinomial_pochhammer': "a gchoose k = pochhammer (a - of_nat k + 1) k / fact k"
@@ -437,10 +449,8 @@
   (is "?l = ?r")
 proof -
   have "?r = ((- 1) ^k * pochhammer (- a) k / fact k) * (of_nat k - (- a + of_nat k))"
-    apply (simp only: gbinomial_pochhammer pochhammer_Suc right_diff_distrib power_Suc)
-    apply (simp del: of_nat_Suc fact_Suc)
-    apply (auto simp add: field_simps simp del: of_nat_Suc)
-    done
+    unfolding gbinomial_pochhammer pochhammer_Suc right_diff_distrib power_Suc
+    by (auto simp add: field_simps simp del: of_nat_Suc)
   also have "\<dots> = ?l"
     by (simp add: field_simps gbinomial_pochhammer)
   finally show ?thesis ..
@@ -459,17 +469,17 @@
 next
   case (Suc h)
   have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
-    apply (rule prod.reindex_cong [where l = Suc])
-      using Suc
-      apply (auto simp add: image_Suc_atMost)
-    done
+  proof (rule prod.reindex_cong)
+    show "{1..k} = Suc ` {0..h}"
+      using Suc by (auto simp add: image_Suc_atMost)
+  qed auto
   have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) =
       (a gchoose Suc h) * (fact (Suc (Suc h))) +
       (a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))"
     by (simp add: Suc field_simps del: fact_Suc)
   also have "\<dots> =
     (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + (\<Prod>i=0..Suc h. a - of_nat i)"
-    apply (simp del: fact_Suc prod.op_ivl_Suc add: gbinomial_mult_fact field_simps mult.left_commute [of _ "2"])
+    apply (simp only: gbinomial_mult_fact field_simps mult.left_commute [of _ "2"])
     apply (simp del: fact_Suc add: fact_Suc [of "Suc h"] field_simps gbinomial_mult_fact
       mult.left_commute [of _ "2"] atLeastLessThanSuc_atLeastAtMost)
     done
@@ -608,10 +618,8 @@
   also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
         pochhammer b (Suc n) =
       (\<Sum>i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
-    apply (subst sum.atLeast_Suc_atMost)
-    apply simp
-    apply (subst sum.shift_bounds_cl_Suc_ivl)
-    apply (simp add: atLeast0AtMost)
+    apply (subst sum.atLeast_Suc_atMost, simp)
+    apply (simp add: sum.shift_bounds_cl_Suc_ivl atLeast0AtMost del: sum.cl_ivl_Suc)
     done
   also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
     using Suc by (intro sum.mono_neutral_right) (auto simp: not_le binomial_eq_0)
@@ -641,12 +649,11 @@
     using assms of_nat_0_le_iff order_trans by blast
   have "(a / of_nat k :: 'a) ^ k = (\<Prod>i = 0..<k. a / of_nat k :: 'a)"
     by simp
-  also have "\<dots> \<le> a gchoose k" (* FIXME *)
-    unfolding gbinomial_altdef_of_nat
-    apply (safe intro!: prod_mono)
-    apply simp_all
-    prefer 2
-    subgoal premises for i
+  also have "\<dots> \<le> a gchoose k"
+  proof -
+    have "\<And>i. i < k \<Longrightarrow> 0 \<le> a / of_nat k"
+      by (simp add: x zero_le_divide_iff)
+    moreover have "a / of_nat k \<le> (a - of_nat i) / of_nat (k - i)" if "i < k" for i
     proof -
       from assms have "a * of_nat i \<ge> of_nat (i * k)"
         by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult)
@@ -655,12 +662,14 @@
       then have "a * of_nat (k - i) \<le> (a - of_nat i) * of_nat k"
         using \<open>i < k\<close> by (simp add: algebra_simps zero_less_mult_iff of_nat_diff)
       then have "a * of_nat (k - i) \<le> (a - of_nat i) * (of_nat k :: 'a)"
-        by (simp only: of_nat_mult[symmetric] of_nat_le_iff)
+        by blast
       with assms show ?thesis
         using \<open>i < k\<close> by (simp add: field_simps)
     qed
-    apply (simp add: x zero_le_divide_iff)
-    done
+    ultimately show ?thesis
+      unfolding gbinomial_altdef_of_nat
+      by (intro prod_mono) auto
+  qed
   finally show ?thesis .
 qed
 
@@ -919,12 +928,16 @@
 
 lemma gbinomial_partial_sum_poly_xpos:
     "(\<Sum>k\<le>m. (of_nat m + a gchoose k) * x^k * y^(m-k)) =
-     (\<Sum>k\<le>m. (of_nat k + a - 1 gchoose k) * x^k * (x + y)^(m-k))"
-  apply (subst gbinomial_partial_sum_poly)
-  apply (subst gbinomial_negated_upper)
-  apply (intro sum.cong, rule refl)
-  apply (simp add: power_mult_distrib [symmetric])
-  done
+     (\<Sum>k\<le>m. (of_nat k + a - 1 gchoose k) * x^k * (x + y)^(m-k))" (is "?lhs = ?rhs")
+proof -
+  have "?lhs = (\<Sum>k\<le>m. (- a gchoose k) * (- x) ^ k * (x + y) ^ (m - k))"
+    by (simp add: gbinomial_partial_sum_poly)
+  also have "... = (\<Sum>k\<le>m. (-1) ^ k * (of_nat k - - a - 1 gchoose k) * (- x) ^ k * (x + y) ^ (m - k))"
+    by (metis (no_types, hide_lams) gbinomial_negated_upper)
+  also have "... = ?rhs"
+    by (intro sum.cong) (auto simp flip: power_mult_distrib)
+  finally show ?thesis .
+qed
 
 lemma binomial_r_part_sum: "(\<Sum>k\<le>m. (2 * m + 1 choose k)) = 2 ^ (2 * m)"
 proof -
@@ -1012,12 +1025,12 @@
   by (subst binomial_fact_lemma [symmetric]) auto
 
 lemma choose_dvd:
-  "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a::linordered_semidom)"
+  assumes "k \<le> n" shows "fact k * fact (n - k) dvd (fact n :: 'a::linordered_semidom)"
   unfolding dvd_def
-  apply (rule exI [where x="of_nat (n choose k)"])
-  using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]]
-  apply auto
-  done
+proof
+  show "fact n = fact k * fact (n - k) * of_nat (n choose k)"
+    by (metis assms binomial_fact_lemma of_nat_fact of_nat_mult) 
+qed
 
 lemma fact_fact_dvd_fact:
   "fact k * fact n dvd (fact (k + n) :: 'a::linordered_semidom)"
@@ -1030,11 +1043,14 @@
   have "?lhs =
       fact (m + r + k) div (fact (m + k) * fact (m + r - m)) * (fact (m + k) div (fact k * fact m))"
     by (simp add: binomial_altdef_nat)
-  also have "\<dots> = fact (m + r + k) div (fact r * (fact k * fact m))"
+  also have "... = fact (m + r + k) * fact (m + k) div
+                 (fact (m + k) * fact (m + r - m) * (fact k * fact m))"
     apply (subst div_mult_div_if_dvd)
-    apply (auto simp: algebra_simps fact_fact_dvd_fact)
+      apply (auto simp: algebra_simps fact_fact_dvd_fact)
     apply (metis add.assoc add.commute fact_fact_dvd_fact)
     done
+  also have "\<dots> = fact (m + r + k) div (fact r * (fact k * fact m))"
+    by (auto simp: algebra_simps fact_fact_dvd_fact)
   also have "\<dots> = (fact (m + r + k) * fact (m + r)) div (fact r * (fact k * fact m) * fact (m + r))"
     apply (subst div_mult_div_if_dvd [symmetric])
     apply (auto simp add: algebra_simps)
diff -r 54ac957c53ec -r 23abd7f9f054 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Mon Apr 06 22:28:41 2020 +0200
+++ b/src/HOL/Fields.thy	Mon Apr 06 22:29:40 2020 +0200
@@ -125,11 +125,14 @@
 qed
 
 lemma inverse_zero_imp_zero:
-  "inverse a = 0 \<Longrightarrow> a = 0"
-apply (rule classical)
-apply (drule nonzero_imp_inverse_nonzero)
-apply auto
-done
+  assumes "inverse a = 0" shows "a = 0"
+proof (rule ccontr)
+  assume "a \<noteq> 0"
+  then have "inverse a \<noteq> 0"
+    by (simp add: nonzero_imp_inverse_nonzero)
+  with assms show False
+    by auto
+qed
 
 lemma inverse_unique:
   assumes ab: "a * b = 1"
@@ -209,10 +212,10 @@
 lemma minus_divide_left: "- (a / b) = (-a) / b"
   by (simp add: divide_inverse)
 
-lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
+lemma nonzero_minus_divide_right: "b \<noteq> 0 \<Longrightarrow> - (a / b) = a / (- b)"
   by (simp add: divide_inverse nonzero_inverse_minus_eq)
 
-lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
+lemma nonzero_minus_divide_divide: "b \<noteq> 0 \<Longrightarrow> (-a) / (-b) = a / b"
   by (simp add: divide_inverse nonzero_inverse_minus_eq)
 
 lemma divide_minus_left [simp]: "(-a) / b = - (a / b)"
@@ -712,10 +715,16 @@
 qed
 
 lemma inverse_less_imp_less:
-  "inverse a < inverse b \<Longrightarrow> 0 < a \<Longrightarrow> b < a"
-apply (simp add: less_le [of "inverse a"] less_le [of "b"])
-apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)
-done
+  assumes "inverse a < inverse b" "0 < a"
+  shows "b < a"
+proof -
+  have "a \<noteq> b"
+    using assms by (simp add: less_le)
+  moreover have "b \<le> a"
+    using assms by (force simp: less_le dest: inverse_le_imp_le)
+  ultimately show ?thesis
+    by (simp add: less_le)
+qed
 
 text\<open>Both premises are essential. Consider -1 and 1.\<close>
 lemma inverse_less_iff_less [simp]:
@@ -734,41 +743,44 @@
 text\<open>These results refer to both operands being negative.  The opposite-sign
 case is trivial, since inverse preserves signs.\<close>
 lemma inverse_le_imp_le_neg:
-  "inverse a \<le> inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b \<le> a"
-apply (rule classical)
-apply (subgoal_tac "a < 0")
- prefer 2 apply force
-apply (insert inverse_le_imp_le [of "-b" "-a"])
-apply (simp add: nonzero_inverse_minus_eq)
-done
+  assumes "inverse a \<le> inverse b" "b < 0"
+  shows "b \<le> a"
+proof (rule classical)
+  assume "\<not> b \<le> a"
+  with \<open>b < 0\<close> have "a < 0"
+    by force
+  with assms show "b \<le> a"
+    using inverse_le_imp_le [of "-b" "-a"] by (simp add: nonzero_inverse_minus_eq)
+qed
 
 lemma less_imp_inverse_less_neg:
-   "a < b \<Longrightarrow> b < 0 \<Longrightarrow> inverse b < inverse a"
-apply (subgoal_tac "a < 0")
- prefer 2 apply (blast intro: less_trans)
-apply (insert less_imp_inverse_less [of "-b" "-a"])
-apply (simp add: nonzero_inverse_minus_eq)
-done
+  assumes "a < b" "b < 0"
+  shows "inverse b < inverse a"
+proof -
+  have "a < 0"
+    using assms by (blast intro: less_trans)
+  with less_imp_inverse_less [of "-b" "-a"] show ?thesis
+    by (simp add: nonzero_inverse_minus_eq assms)
+qed
 
 lemma inverse_less_imp_less_neg:
-   "inverse a < inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b < a"
-apply (rule classical)
-apply (subgoal_tac "a < 0")
- prefer 2
- apply force
-apply (insert inverse_less_imp_less [of "-b" "-a"])
-apply (simp add: nonzero_inverse_minus_eq)
-done
+  assumes "inverse a < inverse b" "b < 0"
+  shows "b < a"
+proof (rule classical)
+  assume "\<not> b < a"
+  with \<open>b < 0\<close> have "a < 0"
+    by force
+  with inverse_less_imp_less [of "-b" "-a"] show ?thesis
+    by (simp add: nonzero_inverse_minus_eq assms)
+qed
 
 lemma inverse_less_iff_less_neg [simp]:
   "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
-apply (insert inverse_less_iff_less [of "-b" "-a"])
-apply (simp del: inverse_less_iff_less
-            add: nonzero_inverse_minus_eq)
-done
+  using inverse_less_iff_less [of "-b" "-a"]
+  by (simp del: inverse_less_iff_less add: nonzero_inverse_minus_eq)
 
 lemma le_imp_inverse_le_neg:
-  "a \<le> b \<Longrightarrow> b < 0 ==> inverse b \<le> inverse a"
+  "a \<le> b \<Longrightarrow> b < 0 \<Longrightarrow> inverse b \<le> inverse a"
   by (force simp add: le_less less_imp_inverse_less_neg)
 
 lemma inverse_le_iff_le_neg [simp]:
@@ -907,113 +919,125 @@
   by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )
 
 lemma divide_pos_pos[simp]:
-  "0 < x ==> 0 < y ==> 0 < x / y"
+  "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> 0 < x / y"
 by(simp add:field_simps)
 
 lemma divide_nonneg_pos:
-  "0 <= x ==> 0 < y ==> 0 <= x / y"
+  "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> 0 \<le> x / y"
 by(simp add:field_simps)
 
 lemma divide_neg_pos:
-  "x < 0 ==> 0 < y ==> x / y < 0"
-by(simp add:field_simps)
+  "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> x / y < 0"
+  by(simp add:field_simps)
 
 lemma divide_nonpos_pos:
-  "x <= 0 ==> 0 < y ==> x / y <= 0"
-by(simp add:field_simps)
+  "x \<le> 0 \<Longrightarrow> 0 < y \<Longrightarrow> x / y \<le> 0"
+  by(simp add:field_simps)
 
 lemma divide_pos_neg:
-  "0 < x ==> y < 0 ==> x / y < 0"
-by(simp add:field_simps)
+  "0 < x \<Longrightarrow> y < 0 \<Longrightarrow> x / y < 0"
+  by(simp add:field_simps)
 
 lemma divide_nonneg_neg:
-  "0 <= x ==> y < 0 ==> x / y <= 0"
-by(simp add:field_simps)
+  "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> x / y \<le> 0"
+  by(simp add:field_simps)
 
 lemma divide_neg_neg:
-  "x < 0 ==> y < 0 ==> 0 < x / y"
-by(simp add:field_simps)
+  "x < 0 \<Longrightarrow> y < 0 \<Longrightarrow> 0 < x / y"
+  by(simp add:field_simps)
 
 lemma divide_nonpos_neg:
-  "x <= 0 ==> y < 0 ==> 0 <= x / y"
-by(simp add:field_simps)
+  "x \<le> 0 \<Longrightarrow> y < 0 \<Longrightarrow> 0 \<le> x / y"
+  by(simp add:field_simps)
 
 lemma divide_strict_right_mono:
-     "[|a < b; 0 < c|] ==> a / c < b / c"
-by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono
-              positive_imp_inverse_positive)
+  "\<lbrakk>a < b; 0 < c\<rbrakk> \<Longrightarrow> a / c < b / c"
+  by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono
+      positive_imp_inverse_positive)
 
 
 lemma divide_strict_right_mono_neg:
-     "[|b < a; c < 0|] ==> a / c < b / c"
-apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
-apply (simp add: less_imp_not_eq nonzero_minus_divide_right [symmetric])
-done
+  assumes "b < a" "c < 0" shows "a / c < b / c"
+proof -
+  have "b / - c < a / - c"
+    by (rule divide_strict_right_mono) (use assms in auto)
+  then show ?thesis
+    by (simp add: less_imp_not_eq)
+qed
 
 text\<open>The last premise ensures that \<^term>\<open>a\<close> and \<^term>\<open>b\<close>
       have the same sign\<close>
 lemma divide_strict_left_mono:
-  "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b"
+  "\<lbrakk>b < a; 0 < c; 0 < a*b\<rbrakk> \<Longrightarrow> c / a < c / b"
   by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono)
 
 lemma divide_left_mono:
-  "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / b"
+  "\<lbrakk>b \<le> a; 0 \<le> c; 0 < a*b\<rbrakk> \<Longrightarrow> c / a \<le> c / b"
   by (auto simp: field_simps zero_less_mult_iff mult_right_mono)
 
 lemma divide_strict_left_mono_neg:
-  "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b"
+  "\<lbrakk>a < b; c < 0; 0 < a*b\<rbrakk> \<Longrightarrow> c / a < c / b"
   by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg)
 
-lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==>
-    x / y <= z"
+lemma mult_imp_div_pos_le: "0 < y \<Longrightarrow> x \<le> z * y \<Longrightarrow> x / y \<le> z"
 by (subst pos_divide_le_eq, assumption+)
 
-lemma mult_imp_le_div_pos: "0 < y ==> z * y <= x ==>
-    z <= x / y"
+lemma mult_imp_le_div_pos: "0 < y \<Longrightarrow> z * y \<le> x \<Longrightarrow> z \<le> x / y"
 by(simp add:field_simps)
 
-lemma mult_imp_div_pos_less: "0 < y ==> x < z * y ==>
-    x / y < z"
+lemma mult_imp_div_pos_less: "0 < y \<Longrightarrow> x < z * y \<Longrightarrow> x / y < z"
 by(simp add:field_simps)
 
-lemma mult_imp_less_div_pos: "0 < y ==> z * y < x ==>
-    z < x / y"
+lemma mult_imp_less_div_pos: "0 < y \<Longrightarrow> z * y < x \<Longrightarrow> z < x / y"
 by(simp add:field_simps)
 
-lemma frac_le: "0 <= x ==>
-    x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
-  apply (rule mult_imp_div_pos_le)
-  apply simp
-  apply (subst times_divide_eq_left)
-  apply (rule mult_imp_le_div_pos, assumption)
-  apply (rule mult_mono)
-  apply simp_all
-done
+lemma frac_le:
+  assumes "0 \<le> y" "x \<le> y" "0 < w" "w \<le> z"
+  shows "x / z \<le> y / w"
+proof (rule mult_imp_div_pos_le)
+  show "z > 0"
+    using assms by simp
+  have "x \<le> y * z / w"
+  proof (rule mult_imp_le_div_pos [OF \<open>0 < w\<close>])
+    show "x * w \<le> y * z"
+      using assms by (auto intro: mult_mono)
+  qed
+  also have "... = y / w * z"
+    by simp
+  finally show "x \<le> y / w * z" .
+qed
 
-lemma frac_less: "0 <= x ==>
-    x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
-  apply (rule mult_imp_div_pos_less)
-  apply simp
-  apply (subst times_divide_eq_left)
-  apply (rule mult_imp_less_div_pos, assumption)
-  apply (erule mult_less_le_imp_less)
-  apply simp_all
-done
+lemma frac_less:
+  assumes "0 \<le> x" "x < y" "0 < w" "w \<le> z"
+  shows "x / z < y / w"
+proof (rule mult_imp_div_pos_less)
+  show "z > 0"
+    using assms by simp
+  have "x < y * z / w"
+  proof (rule mult_imp_less_div_pos [OF \<open>0 < w\<close>])
+    show "x * w < y * z"
+      using assms by (auto intro: mult_less_le_imp_less)
+  qed
+  also have "... = y / w * z"
+    by simp
+  finally show "x < y / w * z" .
+qed
 
-lemma frac_less2: "0 < x ==>
-    x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
-  apply (rule mult_imp_div_pos_less)
-  apply simp_all
-  apply (rule mult_imp_less_div_pos, assumption)
-  apply (erule mult_le_less_imp_less)
-  apply simp_all
-done
+lemma frac_less2:
+  assumes "0 < x" "x \<le> y" "0 < w" "w < z"
+  shows "x / z < y / w"
+proof (rule mult_imp_div_pos_less)
+  show "z > 0"
+    using assms by simp
+  show "x < y / w * z"
+    using assms by (force intro: mult_imp_less_div_pos mult_le_less_imp_less)
+qed
 
-lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)"
-by (simp add: field_simps zero_less_two)
+lemma less_half_sum: "a < b \<Longrightarrow> a < (a+b) / (1+1)"
+  by (simp add: field_simps zero_less_two)
 
-lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b"
-by (simp add: field_simps zero_less_two)
+lemma gt_half_sum: "a < b \<Longrightarrow> (a+b)/(1+1) < b"
+  by (simp add: field_simps zero_less_two)
 
 subclass unbounded_dense_linorder
 proof
@@ -1037,11 +1061,11 @@
   by (cases b 0 rule: linorder_cases) simp_all
 
 lemma nonzero_abs_inverse:
-  "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
+  "a \<noteq> 0 \<Longrightarrow> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
   by (rule abs_inverse)
 
 lemma nonzero_abs_divide:
-  "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
+  "b \<noteq> 0 \<Longrightarrow> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
   by (rule abs_divide)
 
 lemma field_le_epsilon:
@@ -1055,24 +1079,24 @@
   then show "t \<le> y" by (simp add: algebra_simps)
 qed
 
-lemma inverse_positive_iff_positive [simp]:
-  "(0 < inverse a) = (0 < a)"
-apply (cases "a = 0", simp)
-apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
-done
+lemma inverse_positive_iff_positive [simp]: "(0 < inverse a) = (0 < a)"
+proof (cases "a = 0")
+  case False
+  then show ?thesis
+    by (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
+qed auto
 
-lemma inverse_negative_iff_negative [simp]:
-  "(inverse a < 0) = (a < 0)"
-apply (cases "a = 0", simp)
-apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
-done
+lemma inverse_negative_iff_negative [simp]: "(inverse a < 0) = (a < 0)"
+proof (cases "a = 0")
+  case False
+  then show ?thesis
+    by (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
+qed auto
 
-lemma inverse_nonnegative_iff_nonnegative [simp]:
-  "0 \<le> inverse a \<longleftrightarrow> 0 \<le> a"
+lemma inverse_nonnegative_iff_nonnegative [simp]: "0 \<le> inverse a \<longleftrightarrow> 0 \<le> a"
   by (simp add: not_less [symmetric])
 
-lemma inverse_nonpositive_iff_nonpositive [simp]:
-  "inverse a \<le> 0 \<longleftrightarrow> a \<le> 0"
+lemma inverse_nonpositive_iff_nonpositive [simp]: "inverse a \<le> 0 \<longleftrightarrow> a \<le> 0"
   by (simp add: not_less [symmetric])
 
 lemma one_less_inverse_iff: "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1"
@@ -1144,20 +1168,14 @@
   by (simp add: divide_less_0_iff)
 
 lemma divide_right_mono:
-     "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/c"
-by (force simp add: divide_strict_right_mono le_less)
+  "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> a/c \<le> b/c"
+  by (force simp add: divide_strict_right_mono le_less)
 
-lemma divide_right_mono_neg: "a <= b
-    ==> c <= 0 ==> b / c <= a / c"
-apply (drule divide_right_mono [of _ _ "- c"])
-apply auto
-done
+lemma divide_right_mono_neg: "a \<le> b \<Longrightarrow> c \<le> 0 \<Longrightarrow> b / c \<le> a / c"
+  by (auto dest: divide_right_mono [of _ _ "- c"])
 
-lemma divide_left_mono_neg: "a <= b
-    ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
-  apply (drule divide_left_mono [of _ _ "- c"])
-  apply (auto simp add: mult.commute)
-done
+lemma divide_left_mono_neg: "a \<le> b \<Longrightarrow> c \<le> 0 \<Longrightarrow> 0 < a * b \<Longrightarrow> c / a \<le> c / b"
+  by (auto simp add: mult.commute dest: divide_left_mono [of _ _ "- c"])
 
 lemma inverse_le_iff: "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)"
   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
@@ -1176,19 +1194,19 @@
 
 lemma le_divide_eq_1:
   "(1 \<le> b / a) = ((0 < a \<and> a \<le> b) \<or> (a < 0 \<and> b \<le> a))"
-by (auto simp add: le_divide_eq)
+  by (auto simp add: le_divide_eq)
 
 lemma divide_le_eq_1:
   "(b / a \<le> 1) = ((0 < a \<and> b \<le> a) \<or> (a < 0 \<and> a \<le> b) \<or> a=0)"
-by (auto simp add: divide_le_eq)
+  by (auto simp add: divide_le_eq)
 
 lemma less_divide_eq_1:
   "(1 < b / a) = ((0 < a \<and> a < b) \<or> (a < 0 \<and> b < a))"
-by (auto simp add: less_divide_eq)
+  by (auto simp add: less_divide_eq)
 
 lemma divide_less_eq_1:
   "(b / a < 1) = ((0 < a \<and> b < a) \<or> (a < 0 \<and> a < b) \<or> a=0)"
-by (auto simp add: divide_less_eq)
+  by (auto simp add: divide_less_eq)
 
 lemma divide_nonneg_nonneg [simp]:
   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x / y"
@@ -1210,55 +1228,52 @@
 
 lemma le_divide_eq_1_pos [simp]:
   "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
-by (auto simp add: le_divide_eq)
+  by (auto simp add: le_divide_eq)
 
 lemma le_divide_eq_1_neg [simp]:
   "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
-by (auto simp add: le_divide_eq)
+  by (auto simp add: le_divide_eq)
 
 lemma divide_le_eq_1_pos [simp]:
   "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
-by (auto simp add: divide_le_eq)
+  by (auto simp add: divide_le_eq)
 
 lemma divide_le_eq_1_neg [simp]:
   "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
-by (auto simp add: divide_le_eq)
+  by (auto simp add: divide_le_eq)
 
 lemma less_divide_eq_1_pos [simp]:
   "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
-by (auto simp add: less_divide_eq)
+  by (auto simp add: less_divide_eq)
 
 lemma less_divide_eq_1_neg [simp]:
   "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
-by (auto simp add: less_divide_eq)
+  by (auto simp add: less_divide_eq)
 
 lemma divide_less_eq_1_pos [simp]:
   "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
-by (auto simp add: divide_less_eq)
+  by (auto simp add: divide_less_eq)
 
 lemma divide_less_eq_1_neg [simp]:
   "a < 0 \<Longrightarrow> b/a < 1 \<longleftrightarrow> a < b"
-by (auto simp add: divide_less_eq)
+  by (auto simp add: divide_less_eq)
 
 lemma eq_divide_eq_1 [simp]:
   "(1 = b/a) = ((a \<noteq> 0 \<and> a = b))"
-by (auto simp add: eq_divide_eq)
+  by (auto simp add: eq_divide_eq)
 
 lemma divide_eq_eq_1 [simp]:
   "(b/a = 1) = ((a \<noteq> 0 \<and> a = b))"
-by (auto simp add: divide_eq_eq)
+  by (auto simp add: divide_eq_eq)
 
-lemma abs_div_pos: "0 < y ==>
-    \<bar>x\<bar> / y = \<bar>x / y\<bar>"
-  apply (subst abs_divide)
-  apply (simp add: order_less_imp_le)
-done
+lemma abs_div_pos: "0 < y \<Longrightarrow> \<bar>x\<bar> / y = \<bar>x / y\<bar>"
+  by (simp add: order_less_imp_le)
 
 lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / \<bar>b\<bar>) = (0 \<le> a \<or> b = 0)"
-by (auto simp: zero_le_divide_iff)
+  by (auto simp: zero_le_divide_iff)
 
 lemma divide_le_0_abs_iff [simp]: "(a / \<bar>b\<bar> \<le> 0) = (a \<le> 0 \<or> b = 0)"
-by (auto simp: divide_le_0_iff)
+  by (auto simp: divide_le_0_iff)
 
 lemma field_le_mult_one_interval:
   assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
@@ -1279,13 +1294,14 @@
 text\<open>For creating values between \<^term>\<open>u\<close> and \<^term>\<open>v\<close>.\<close>
 lemma scaling_mono:
   assumes "u \<le> v" "0 \<le> r" "r \<le> s"
-    shows "u + r * (v - u) / s \<le> v"
+  shows "u + r * (v - u) / s \<le> v"
 proof -
   have "r/s \<le> 1" using assms
     using divide_le_eq_1 by fastforce
-  then have "(r/s) * (v - u) \<le> 1 * (v - u)"
-    apply (rule mult_right_mono)
+  moreover have "0 \<le> v - u"
     using assms by simp
+  ultimately have "(r/s) * (v - u) \<le> 1 * (v - u)"
+    by (rule mult_right_mono)
   then show ?thesis
     by (simp add: field_simps)
 qed
diff -r 54ac957c53ec -r 23abd7f9f054 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Mon Apr 06 22:28:41 2020 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Mon Apr 06 22:29:40 2020 +0200
@@ -49,27 +49,25 @@
   using ext[of P Q, OF assms] by simp
 
 text \<open>
-  Easier to apply than \<open>someI\<close> if the witness comes from an
+  Easier to use than \<open>someI\<close> if the witness comes from an
   existential formula.
 \<close>
 lemma someI_ex [elim?]: "\<exists>x. P x \<Longrightarrow> P (SOME x. P x)"
-  apply (erule exE)
-  apply (erule someI)
-  done
+  by (elim exE someI)
 
 lemma some_eq_imp:
   assumes "Eps P = a" "P b" shows "P a"
   using assms someI_ex by force
 
 text \<open>
-  Easier to apply than \<open>someI\<close> because the conclusion has only one
+  Easier to use than \<open>someI\<close> because the conclusion has only one
   occurrence of \<^term>\<open>P\<close>.
 \<close>
 lemma someI2: "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. P x)"
   by (blast intro: someI)
 
 text \<open>
-  Easier to apply than \<open>someI2\<close> if the witness comes from an
+  Easier to use than \<open>someI2\<close> if the witness comes from an
   existential formula.
 \<close>
 lemma someI2_ex: "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. P x)"
@@ -94,10 +92,7 @@
   by (rule some_equality) (rule refl)
 
 lemma some_sym_eq_trivial [simp]: "(SOME y. x = y) = x"
-  apply (rule some_equality)
-   apply (rule refl)
-  apply (erule sym)
-  done
+  by (iprover intro: some_equality)
 
 
 subsection \<open>Axiom of Choice, Proved Using the Description Operator\<close>
@@ -240,11 +235,16 @@
 lemma surj_iff_all: "surj f \<longleftrightarrow> (\<forall>x. f (inv f x) = x)"
   by (simp add: o_def surj_iff fun_eq_iff)
 
-lemma surj_imp_inv_eq: "surj f \<Longrightarrow> \<forall>x. g (f x) = x \<Longrightarrow> inv f = g"
-  apply (rule ext)
-  apply (drule_tac x = "inv f x" in spec)
-  apply (simp add: surj_f_inv_f)
-  done
+lemma surj_imp_inv_eq:
+  assumes "surj f" and gf: "\<And>x. g (f x) = x"
+  shows "inv f = g"
+proof (rule ext)
+  fix x
+  have "g (f (inv f x)) = inv f x"
+    by (rule gf)
+  then show "inv f x = g x"
+    by (simp add: surj_f_inv_f \<open>surj f\<close>)
+qed
 
 lemma bij_imp_bij_inv: "bij f \<Longrightarrow> bij (inv f)"
   by (simp add: bij_def inj_imp_surj_inv surj_imp_inj_inv)
@@ -266,11 +266,7 @@
 lemma inv_into_comp:
   "inj_on f (g ` A) \<Longrightarrow> inj_on g A \<Longrightarrow> x \<in> f ` g ` A \<Longrightarrow>
     inv_into A (f \<circ> g) x = (inv_into A g \<circ> inv_into (g ` A) f) x"
-  apply (rule inv_into_f_eq)
-    apply (fast intro: comp_inj_on)
-   apply (simp add: inv_into_into)
-  apply (simp add: f_inv_into_f inv_into_into)
-  done
+  by (auto simp: f_inv_into_f inv_into_into intro: inv_into_f_eq comp_inj_on)
 
 lemma o_inv_distrib: "bij f \<Longrightarrow> bij g \<Longrightarrow> inv (f \<circ> g) = inv g \<circ> inv f"
   by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)
@@ -281,16 +277,25 @@
 lemma image_inv_f_f: "inj f \<Longrightarrow> inv f ` (f ` A) = A"
   by simp
 
-lemma bij_image_Collect_eq: "bij f \<Longrightarrow> f ` Collect P = {y. P (inv f y)}"
-  apply auto
-   apply (force simp add: bij_is_inj)
-  apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
-  done
+lemma bij_image_Collect_eq:
+  assumes "bij f"
+  shows "f ` Collect P = {y. P (inv f y)}"
+proof
+  show "f ` Collect P \<subseteq> {y. P (inv f y)}"
+    using assms by (force simp add: bij_is_inj)
+  show "{y. P (inv f y)} \<subseteq> f ` Collect P"
+    using assms by (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
+qed
 
-lemma bij_vimage_eq_inv_image: "bij f \<Longrightarrow> f -` A = inv f ` A"
-  apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
-  apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
-  done
+lemma bij_vimage_eq_inv_image:
+  assumes "bij f"
+  shows "f -` A = inv f ` A"
+proof
+  show "f -` A \<subseteq> inv f ` A"
+    using assms by (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
+  show "inv f ` A \<subseteq> f -` A"
+    using assms by (auto simp add: bij_is_surj [THEN surj_f_inv_f])
+qed
 
 lemma inv_fn_o_fn_is_id:
   fixes f::"'a \<Rightarrow> 'a"
@@ -338,11 +343,16 @@
   shows "inv (f^^n) = ((inv f)^^n)"
 proof -
   have "inv (f^^n) x = ((inv f)^^n) x" for x
-  apply (rule inv_into_f_eq, auto simp add: inj_fn[OF bij_is_inj[OF assms]])
-  using fn_o_inv_fn_is_id[OF assms, of n, THEN fun_cong] by (simp)
+  proof (rule inv_into_f_eq)
+    show "inj (f ^^ n)"
+      by (simp add: inj_fn[OF bij_is_inj [OF assms]])
+    show "(f ^^ n) ((inv f ^^ n) x) = x"
+      using fn_o_inv_fn_is_id[OF assms, THEN fun_cong] by force
+  qed auto
   then show ?thesis by auto
 qed
 
+
 lemma mono_inv:
   fixes f::"'a::linorder \<Rightarrow> 'b::linorder"
   assumes "mono f" "bij f"
@@ -746,13 +756,16 @@
   qed
   then have "N \<le> card (f N)" by simp
   also have "\<dots> \<le> card S" using S by (intro card_mono)
-  finally have "f (card S) = f N" using eq by auto
-  then show ?thesis
-    using eq inj [of N]
-    apply auto
-    apply (case_tac "n < N")
-     apply (auto simp: not_less)
-    done
+  finally have \<section>: "f (card S) = f N" using eq by auto
+  moreover have "\<Union> (range f) \<subseteq> f N"
+  proof clarify
+    fix x n
+    assume "x \<in> f n"
+    with eq inj [of N] show "x \<in> f N"
+      by (cases "n < N") (auto simp: not_less)
+  qed
+  ultimately show ?thesis
+    by auto
 qed
 
 
@@ -822,28 +835,13 @@
   case True
   with infinite have "\<not> finite (A - {a})" by auto
   with infinite_iff_countable_subset[of "A - {a}"]
-  obtain f :: "nat \<Rightarrow> 'a" where 1: "inj f" and 2: "f ` UNIV \<subseteq> A - {a}" by blast
+  obtain f :: "nat \<Rightarrow> 'a" where "inj f" and f: "f ` UNIV \<subseteq> A - {a}" by blast
   define g where "g n = (if n = 0 then a else f (Suc n))" for n
   define A' where "A' = g ` UNIV"
-  have *: "\<forall>y. f y \<noteq> a" using 2 by blast
+  have *: "\<forall>y. f y \<noteq> a" using f by blast
   have 3: "inj_on g UNIV \<and> g ` UNIV \<subseteq> A \<and> a \<in> g ` UNIV"
-    apply (auto simp add: True g_def [abs_def])
-     apply (unfold inj_on_def)
-     apply (intro ballI impI)
-     apply (case_tac "x = 0")
-      apply (auto simp add: 2)
-  proof -
-    fix y
-    assume "a = (if y = 0 then a else f (Suc y))"
-    then show "y = 0" by (cases "y = 0") (use * in auto)
-  next
-    fix x y
-    assume "f (Suc x) = (if y = 0 then a else f (Suc y))"
-    with 1 * show "x = y" by (cases "y = 0") (auto simp: inj_on_def)
-  next
-    fix n
-    from 2 show "f (Suc n) \<in> A" by blast
-  qed
+    using \<open>inj f\<close> f * unfolding inj_on_def g_def
+    by (auto simp add: True image_subset_iff)
   then have 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<subseteq> A"
     using inj_on_imp_bij_betw[of g] by (auto simp: A'_def)
   then have 5: "bij_betw (inv g) A' UNIV"
@@ -852,38 +850,14 @@
   have 6: "bij_betw g (UNIV - {n}) (A' - {a})"
     by (rule bij_betw_subset) (use 3 4 n in \<open>auto simp: image_set_diff A'_def\<close>)
   define v where "v m = (if m < n then m else Suc m)" for m
-  have 7: "bij_betw v UNIV (UNIV - {n})"
-  proof (unfold bij_betw_def inj_on_def, intro conjI, clarify)
-    fix m1 m2
-    assume "v m1 = v m2"
-    then show "m1 = m2"
-      apply (cases "m1 < n")
-       apply (cases "m2 < n")
-        apply (auto simp: inj_on_def v_def [abs_def])
-      apply (cases "m2 < n")
-       apply auto
-      done
-  next
-    show "v ` UNIV = UNIV - {n}"
-    proof (auto simp: v_def [abs_def])
-      fix m
-      assume "m \<noteq> n"
-      assume *: "m \<notin> Suc ` {m'. \<not> m' < n}"
-      have False if "n \<le> m"
-      proof -
-        from \<open>m \<noteq> n\<close> that have **: "Suc n \<le> m" by auto
-        from Suc_le_D [OF this] obtain m' where m': "m = Suc m'" ..
-        with ** have "n \<le> m'" by auto
-        with m' * show ?thesis by auto
-      qed
-      then show "m < n" by force
-    qed
-  qed
+  have "m < n \<or> m = n" if "\<And>k. k < n \<or> m \<noteq> Suc k" for m
+    using that [of "m-1"] by auto
+  then have 7: "bij_betw v UNIV (UNIV - {n})"
+    unfolding bij_betw_def inj_on_def v_def by auto
   define h' where "h' = g \<circ> v \<circ> (inv g)"
   with 5 6 7 have 8: "bij_betw h' A' (A' - {a})"
     by (auto simp add: bij_betw_trans)
   define h where "h b = (if b \<in> A' then h' b else b)" for b
-  then have "\<forall>b \<in> A'. h b = h' b" by simp
   with 8 have "bij_betw h  A' (A' - {a})"
     using bij_betw_cong[of A' h] by auto
   moreover
@@ -943,14 +917,14 @@
 lemma Sup_Inf: "\<Squnion> (Inf ` A) = \<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B})"
 proof (rule antisym)
   show "\<Squnion> (Inf ` A) \<le> \<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B})"
-    apply (rule Sup_least, rule INF_greatest)
-    using Inf_lower2 Sup_upper by auto
+    using Inf_lower2 Sup_upper
+    by (fastforce simp add: intro: Sup_least INF_greatest)
 next
   show "\<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B}) \<le> \<Squnion> (Inf ` A)"
   proof (simp add:  Inf_Sup, rule SUP_least, simp, safe)
     fix f
     assume "\<forall>Y. (\<exists>f. Y = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<longrightarrow> f Y \<in> Y"
-    from this have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y) \<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z"
+    then have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y) \<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z"
       by auto
     show "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> \<Squnion>(Inf ` A)"
     proof (cases "\<exists> Z \<in> A . \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> Inf Z")
@@ -963,21 +937,20 @@
         by simp
     next
       case False
-      from this have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x \<in> Z \<and> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> x"
+      then have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x \<in> Z \<and> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> x"
         using Inf_greatest by blast
       define F where "F = (\<lambda> Z . SOME x . x \<in> Z \<and> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> x)"
-      have C: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
+      have C: "\<And>Y. Y \<in> A \<Longrightarrow> F Y \<in> Y"
         using X by (simp add: F_def, rule someI2_ex, auto)
-      have E: "\<And> Y . Y \<in> A \<Longrightarrow> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> F Y"
+      have E: "\<And>Y. Y \<in> A \<Longrightarrow> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> F Y"
         using X by (simp add: F_def, rule someI2_ex, auto)
       from C and B obtain  Z where D: "Z \<in> A " and Y: "f (F ` A) = F Z"
         by blast
       from E and D have W: "\<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> F Z"
         by simp
       have "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> f (F ` A)"
-        apply (rule INF_lower)
-        using C by blast
-      from this and W and Y show ?thesis
+        using C by (blast intro: INF_lower)
+      with W Y show ?thesis
         by simp
     qed
   qed
@@ -985,15 +958,13 @@
   
 lemma dual_complete_distrib_lattice:
   "class.complete_distrib_lattice Sup Inf sup (\<ge>) (>) inf \<top> \<bottom>"
-  apply (rule class.complete_distrib_lattice.intro)
-   apply (fact dual_complete_lattice)
-  by (simp add: class.complete_distrib_lattice_axioms_def Sup_Inf)
+  by (simp add: class.complete_distrib_lattice.intro [OF dual_complete_lattice] 
+                class.complete_distrib_lattice_axioms_def Sup_Inf)
 
 lemma sup_Inf: "a \<squnion> \<Sqinter>B = \<Sqinter>((\<squnion>) a ` B)"
 proof (rule antisym)
   show "a \<squnion> \<Sqinter>B \<le> \<Sqinter>((\<squnion>) a ` B)"
-    apply (rule INF_greatest)
-    using Inf_lower sup.mono by fastforce
+    using Inf_lower sup.mono by (fastforce intro: INF_greatest)
 next
   have "\<Sqinter>((\<squnion>) a ` B) \<le> \<Sqinter>(Sup ` {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B})"
     by (rule INF_greatest, auto simp add: INF_lower)
@@ -1034,8 +1005,7 @@
         have "(INF x\<in>{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> f {uu. \<exists>x. uu = P x y}"
           by (rule INF_lower, blast)
         also have "... \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y"
-          apply (rule someI2_ex)
-          using A by auto
+          by (rule someI2_ex) (use A in auto)
         finally show "\<Sqinter>(f ` {uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}) \<le>
           P (SOME x. f {uu. \<exists>x. uu = P x y} = P x y) y"
           by simp
@@ -1050,70 +1020,46 @@
 qed
 
 lemma INF_SUP_set: "(\<Sqinter>B\<in>A. \<Squnion>(g ` B)) = (\<Squnion>B\<in>{f ` A |f. \<forall>C\<in>A. f C \<in> C}. \<Sqinter>(g ` B))"
+                    (is "_ = (\<Squnion>B\<in>?F. _)")
 proof (rule antisym)
-  have "\<Sqinter> ((g \<circ> f) ` A) \<le> \<Squnion> (g ` B)" if "\<And>B. B \<in> A \<Longrightarrow> f B \<in> B" and "B \<in> A"
-    for f and B
+  have "\<Sqinter> ((g \<circ> f) ` A) \<le> \<Squnion> (g ` B)" if "\<And>B. B \<in> A \<Longrightarrow> f B \<in> B" "B \<in> A" for f B
     using that by (auto intro: SUP_upper2 INF_lower2)
-  then show "(\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)"
+  then show "(\<Squnion>x\<in>?F. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)"
     by (auto intro!: SUP_least INF_greatest simp add: image_comp)
 next
-  show "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)"
+  show "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Squnion>x\<in>?F. \<Sqinter>a\<in>x. g a)"
   proof (cases "{} \<in> A")
     case True
     then show ?thesis 
       by (rule INF_lower2) simp_all
   next
     case False
-    have *: "\<And>f B. B \<in> A \<Longrightarrow> f B \<in> B \<Longrightarrow>
-      (\<Sqinter>B. if B \<in> A then if f B \<in> B then g (f B) else \<bottom> else \<top>) \<le> g (f B)"
-      by (rule INF_lower2, auto)
-    have **: "\<And>f B. B \<in> A \<Longrightarrow> f B \<notin> B \<Longrightarrow>
-      (\<Sqinter>B. if B \<in> A then if f B \<in> B then g (f B) else \<bottom> else \<top>) \<le> g (SOME x. x \<in> B)"
-      by (rule INF_lower2, auto)
-    have ****: "\<And>f B. B \<in> A \<Longrightarrow>
-      (\<Sqinter>B. if B \<in> A then if f B \<in> B then g (f B) else \<bottom> else \<top>)
-        \<le> (if f B \<in> B then g (f B) else g (SOME x. x \<in> B))"
-      by (rule INF_lower2) auto
-    have ***: "\<And>x. (\<Sqinter>B. if B \<in> A then if x B \<in> B then g (x B) else \<bottom> else \<top>)
-        \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
-    proof -
-      fix x
-      define F where "F = (\<lambda> (y::'b set) . if x y \<in> y then x y else (SOME x . x \<in>y))"
-      have B: "(\<forall>Y\<in>A. F Y \<in> Y)"
-        using False some_in_eq F_def by auto
-      have A: "F ` A \<in> {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
-        using B by blast
-      show "(\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
-        using A apply (rule SUP_upper2)
-        apply (rule INF_greatest)
-        using * **
-        apply (auto simp add: F_def)
-        done
-    qed
-
     {fix x
-      have "(\<Sqinter>x\<in>A. \<Squnion>x\<in>x. g x) \<le> (\<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
+      have "(\<Sqinter>x\<in>A. \<Squnion>x\<in>x. g x) \<le> (\<Squnion>u. if x \<in> A then if u \<in> x then g u else \<bottom> else \<top>)"
       proof (cases "x \<in> A")
         case True
         then show ?thesis
-          apply (rule INF_lower2)
-          apply (rule SUP_least)
-          apply (rule SUP_upper2)
-           apply auto
-          done
-      next
-        case False
-        then show ?thesis by simp
+          by (intro INF_lower2 SUP_least SUP_upper2) auto
+      qed auto
+    }
+    then have "(\<Sqinter>Y\<in>A. \<Squnion>a\<in>Y. g a) \<le> (\<Sqinter>Y. \<Squnion>y. if Y \<in> A then if y \<in> Y then g y else \<bottom> else \<top>)"
+      by (rule INF_greatest)
+    also have "... = (\<Squnion>x. \<Sqinter>Y. if Y \<in> A then if x Y \<in> Y then g (x Y) else \<bottom> else \<top>)"
+      by (simp only: INF_SUP)
+    also have "... \<le> (\<Squnion>x\<in>?F. \<Sqinter>a\<in>x. g a)"
+    proof (rule SUP_least)
+      show "(\<Sqinter>B. if B \<in> A then if x B \<in> B then g (x B) else \<bottom> else \<top>)
+               \<le> (\<Squnion>x\<in>?F. \<Sqinter>x\<in>x. g x)" for x
+      proof -
+        define G where "G \<equiv> \<lambda>Y. if x Y \<in> Y then x Y else (SOME x. x \<in>Y)"
+        have "\<forall>Y\<in>A. G Y \<in> Y"
+          using False some_in_eq G_def by auto
+        then have A: "G ` A \<in> ?F"
+          by blast
+        show "(\<Sqinter>Y. if Y \<in> A then if x Y \<in> Y then g (x Y) else \<bottom> else \<top>) \<le> (\<Squnion>x\<in>?F. \<Sqinter>x\<in>x. g x)"
+          by (fastforce simp: G_def intro: SUP_upper2 [OF A] INF_greatest INF_lower2)
       qed
-    }
-    from this have "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Sqinter>x. \<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
-      by (rule INF_greatest)
-    also have "... = (\<Squnion>x. \<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>)"
-      by (simp only: INF_SUP)
-    also have "... \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)"
-      apply (rule SUP_least)
-      using *** apply simp
-      done
+    qed
     finally show ?thesis by simp
   qed
 qed
@@ -1181,22 +1127,15 @@
 instance proof (standard, clarsimp)
   fix A :: "(('a set) set) set"
   fix x::'a
-  define F where "F = (\<lambda> Y . (SOME X . (Y \<in> A \<and> X \<in> Y \<and> x \<in> X)))"
-  assume A: "\<forall>xa\<in>A. \<exists>X\<in>xa. x \<in> X"
-    
-  from this have B: " (\<forall>xa \<in> F ` A. x \<in> xa)"
-    apply (safe, simp add: F_def)
-    by (rule someI2_ex, auto)
-
-  have C: "(\<forall>Y\<in>A. F Y \<in> Y)"
-    apply (simp  add: F_def, safe)
-    apply (rule someI2_ex)
-    using A by auto
-
-  have "(\<exists>f. F ` A  = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y))"
-    using C by blast
-    
-  from B and this show "\<exists>X. (\<exists>f. X = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>xa\<in>X. x \<in> xa)"
+  assume A: "\<forall>\<S>\<in>A. \<exists>X\<in>\<S>. x \<in> X"
+  define F where "F \<equiv> \<lambda>Y. SOME X. Y \<in> A \<and> X \<in> Y \<and> x \<in> X"
+  have "(\<forall>S \<in> F ` A. x \<in> S)"
+    using A unfolding F_def by (fastforce intro: someI2_ex)
+  moreover have "\<forall>Y\<in>A. F Y \<in> Y"
+    using A unfolding F_def by (fastforce intro: someI2_ex)
+  then have "\<exists>f. F ` A  = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)"
+    by blast
+  ultimately show "\<exists>X. (\<exists>f. X = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>S\<in>X. x \<in> S)"
     by auto
 qed
 end
@@ -1212,85 +1151,56 @@
 
 context complete_linorder
 begin
-  
+
 subclass complete_distrib_lattice
 proof (standard, rule ccontr)
-  fix A
-  assume "\<not> \<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
-  then have C: "\<Sqinter>(Sup ` A) > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+  fix A :: "'a set set"
+  let ?F = "{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
+  assume "\<not> \<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` ?F)"
+  then have C: "\<Sqinter>(Sup ` A) > \<Squnion>(Inf ` ?F)"
     by (simp add: not_le)
   show False
-    proof (cases "\<exists> z . \<Sqinter>(Sup ` A) > z \<and> z > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})")
-      case True
-      from this obtain z where A: "z < \<Sqinter>(Sup ` A)" and X: "z > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
-        by blast
-          
-      from A have "\<And> Y . Y \<in> A \<Longrightarrow> z < Sup Y"
-        by (simp add: less_INF_D)
-    
-      from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . z < k"
-        using local.less_Sup_iff by blast
-          
-      define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> z < k)"
-        
-      have D: "\<And> Y . Y \<in> A \<Longrightarrow> z < F Y"
-        using B apply (simp add: F_def)
-        by (rule someI2_ex, auto)
+  proof (cases "\<exists> z . \<Sqinter>(Sup ` A) > z \<and> z > \<Squnion>(Inf ` ?F)")
+    case True
+    then obtain z where A: "z < \<Sqinter>(Sup ` A)" and X: "z > \<Squnion>(Inf ` ?F)"
+      by blast
+    then have B: "\<And>Y. Y \<in> A \<Longrightarrow> \<exists>k \<in>Y . z < k"
+      using local.less_Sup_iff by(force dest: less_INF_D)
+
+    define G where "G \<equiv> \<lambda>Y. SOME k . k \<in> Y \<and> z < k"
+    have E: "\<And>Y. Y \<in> A \<Longrightarrow> G Y \<in> Y"
+      using B unfolding G_def by (fastforce intro: someI2_ex)
+    have "z \<le> Inf (G ` A)"
+    proof (rule INF_greatest)
+      show  "\<And>Y. Y \<in> A \<Longrightarrow> z \<le> G Y"
+        using B unfolding G_def by (fastforce intro: someI2_ex)
+    qed
+    also have "... \<le> \<Squnion>(Inf ` ?F)"
+      by (rule SUP_upper) (use E in blast)
+    finally have "z \<le> \<Squnion>(Inf ` ?F)"
+      by simp
 
-    
-      have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
-        using B apply (simp add: F_def)
-        by (rule someI2_ex, auto)
-    
-      have "z \<le> Inf (F ` A)"
-        by (simp add: D local.INF_greatest local.order.strict_implies_order)
-    
-      also have "... \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
-        apply (rule SUP_upper, safe)
-        using E by blast
-      finally have "z \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
-        by simp
-          
-      from X and this show ?thesis
-        using local.not_less by blast
-    next
-      case False
-      from this have A: "\<And> z . \<Sqinter>(Sup ` A) \<le> z \<or> z \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
-        using local.le_less_linear by blast
-
-      from C have "\<And> Y . Y \<in> A \<Longrightarrow> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < Sup Y"
-        by (simp add: less_INF_D)
-
-      from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < k"
-        using local.less_Sup_iff by blast
-          
-      define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < k)"
-
-      have D: "\<And> Y . Y \<in> A \<Longrightarrow> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < F Y"
-        using B apply (simp add: F_def)
-        by (rule someI2_ex, auto)
-    
-      have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
-        using B apply (simp add: F_def)
-        by (rule someI2_ex, auto)
-          
-      have "\<And> Y . Y \<in> A \<Longrightarrow> \<Sqinter>(Sup ` A) \<le> F Y"
-        using D False local.leI by blast
-         
-      from this have "\<Sqinter>(Sup ` A) \<le> Inf (F ` A)"
-        by (simp add: local.INF_greatest)
-          
-      also have "Inf (F ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
-        apply (rule SUP_upper, safe)
-        using E by blast
-
-      finally have "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
-        by simp
-        
-      from C and this show ?thesis
-        using not_less by blast
-    qed
+    with X show ?thesis
+      using local.not_less by blast
+  next
+    case False
+    have B: "\<And>Y. Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . \<Squnion>(Inf ` ?F) < k"
+      using C local.less_Sup_iff by(force dest: less_INF_D)
+    define G where "G \<equiv> \<lambda> Y . SOME k . k \<in> Y \<and> \<Squnion>(Inf ` ?F) < k"
+    have E: "\<And>Y. Y \<in> A \<Longrightarrow> G Y \<in> Y"
+      using B unfolding G_def by (fastforce intro: someI2_ex)
+    have "\<And>Y. Y \<in> A \<Longrightarrow> \<Sqinter>(Sup ` A) \<le> G Y"
+      using B False local.leI unfolding G_def by (fastforce intro: someI2_ex)
+    then have "\<Sqinter>(Sup ` A) \<le> Inf (G ` A)"
+      by (simp add: local.INF_greatest)
+    also have "Inf (G ` A) \<le> \<Squnion>(Inf ` ?F)"
+      by (rule SUP_upper) (use E in blast)
+    finally have "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` ?F)"
+      by simp
+    with C show ?thesis
+      using not_less by blast
   qed
+qed
 end
 
 
diff -r 54ac957c53ec -r 23abd7f9f054 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon Apr 06 22:28:41 2020 +0200
+++ b/src/HOL/Rings.thy	Mon Apr 06 22:29:40 2020 +0200
@@ -1975,31 +1975,39 @@
 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
   by (drule mult_strict_right_mono [of b 0]) auto
 
-lemma zero_less_mult_pos: "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
-  apply (cases "b \<le> 0")
-   apply (auto simp add: le_less not_less)
-  apply (drule_tac mult_pos_neg [of a b])
-   apply (auto dest: less_not_sym)
-  done
-
-lemma zero_less_mult_pos2: "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
-  apply (cases "b \<le> 0")
-   apply (auto simp add: le_less not_less)
-  apply (drule_tac mult_pos_neg2 [of a b])
-   apply (auto dest: less_not_sym)
-  done
+lemma zero_less_mult_pos: 
+  assumes "0 < a * b" "0 < a" shows "0 < b"
+proof (cases "b \<le> 0")
+  case True
+  then show ?thesis
+    using assms by (auto simp: le_less dest: less_not_sym mult_pos_neg [of a b])
+qed (auto simp add: le_less not_less)
+
+
+lemma zero_less_mult_pos2: 
+  assumes "0 < b * a" "0 < a" shows "0 < b"
+proof (cases "b \<le> 0")
+  case True
+  then show ?thesis
+    using assms by (auto simp: le_less dest: less_not_sym mult_pos_neg2 [of a b])
+qed (auto simp add: le_less not_less)
 
 text \<open>Strict monotonicity in both arguments\<close>
 lemma mult_strict_mono:
-  assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
+  assumes "a < b" "c < d" "0 < b" "0 \<le> c"
   shows "a * c < b * d"
-  using assms
-  apply (cases "c = 0")
-   apply simp
-  apply (erule mult_strict_right_mono [THEN less_trans])
-   apply (auto simp add: le_less)
-  apply (erule (1) mult_strict_left_mono)
-  done
+proof (cases "c = 0")
+  case True
+  with assms show ?thesis
+    by simp
+next
+  case False
+  with assms have "a*c < b*c"
+    by (simp add: mult_strict_right_mono [OF \<open>a < b\<close>])
+  also have "\<dots> < b*d"
+    by (simp add: assms mult_strict_left_mono)
+  finally show ?thesis .
+qed
 
 text \<open>This weaker variant has more natural premises\<close>
 lemma mult_strict_mono':
@@ -2010,24 +2018,24 @@
 lemma mult_less_le_imp_less:
   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
   shows "a * c < b * d"
-  using assms
-  apply (subgoal_tac "a * c < b * c")
-   apply (erule less_le_trans)
-   apply (erule mult_left_mono)
-   apply simp
-  apply (erule (1) mult_strict_right_mono)
-  done
+proof -
+  have "a * c < b * c"
+    by (simp add: assms mult_strict_right_mono)
+  also have "... \<le> b * d"
+    by (intro mult_left_mono) (use assms in auto)
+  finally show ?thesis .
+qed
 
 lemma mult_le_less_imp_less:
   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
   shows "a * c < b * d"
-  using assms
-  apply (subgoal_tac "a * c \<le> b * c")
-   apply (erule le_less_trans)
-   apply (erule mult_strict_left_mono)
-   apply simp
-  apply (erule (1) mult_right_mono)
-  done
+proof -
+  have "a * c \<le> b * c"
+    by (simp add: assms mult_right_mono)
+  also have "... < b * d"
+    by (intro mult_strict_left_mono) (use assms in auto)
+  finally show ?thesis .
+qed
 
 end
 
@@ -2114,14 +2122,10 @@
   by (simp add: algebra_simps)
 
 lemma mult_left_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
-  apply (drule mult_left_mono [of _ _ "- c"])
-  apply simp_all
-  done
+  by (auto dest: mult_left_mono [of _ _ "- c"])
 
 lemma mult_right_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
-  apply (drule mult_right_mono [of _ _ "- c"])
-  apply simp_all
-  done
+  by (auto dest: mult_right_mono [of _ _ "- c"])
 
 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
   using mult_right_mono_neg [of a 0 b] by simp
@@ -2251,21 +2255,39 @@
   an assumption, but effectively four when the comparison is a goal.
 \<close>
 
-lemma mult_less_cancel_right_disj: "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
-  apply (cases "c = 0")
-   apply (auto simp add: neq_iff mult_strict_right_mono mult_strict_right_mono_neg)
-     apply (auto simp add: not_less not_le [symmetric, of "a*c"] not_le [symmetric, of a])
-     apply (erule_tac [!] notE)
-     apply (auto simp add: less_imp_le mult_right_mono mult_right_mono_neg)
-  done
-
-lemma mult_less_cancel_left_disj: "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
-  apply (cases "c = 0")
-   apply (auto simp add: neq_iff mult_strict_left_mono mult_strict_left_mono_neg)
-     apply (auto simp add: not_less not_le [symmetric, of "c * a"] not_le [symmetric, of a])
-     apply (erule_tac [!] notE)
-     apply (auto simp add: less_imp_le mult_left_mono mult_left_mono_neg)
-  done
+lemma mult_less_cancel_right_disj: "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a"
+proof (cases "c = 0")
+  case False
+  show ?thesis (is "?lhs \<longleftrightarrow> ?rhs")
+  proof
+    assume ?lhs
+    then have "c < 0 \<Longrightarrow> b < a" "c > 0 \<Longrightarrow> b > a"
+      by (auto simp flip: not_le intro: mult_right_mono mult_right_mono_neg)
+    with False show ?rhs 
+      by (auto simp add: neq_iff)
+  next
+    assume ?rhs
+    with False show ?lhs 
+      by (auto simp add: mult_strict_right_mono mult_strict_right_mono_neg)
+  qed
+qed auto
+
+lemma mult_less_cancel_left_disj: "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a"
+proof (cases "c = 0")
+  case False
+  show ?thesis (is "?lhs \<longleftrightarrow> ?rhs")
+  proof
+    assume ?lhs
+    then have "c < 0 \<Longrightarrow> b < a" "c > 0 \<Longrightarrow> b > a"
+      by (auto simp flip: not_le intro: mult_left_mono mult_left_mono_neg)
+    with False show ?rhs 
+      by (auto simp add: neq_iff)
+  next
+    assume ?rhs
+    with False show ?lhs 
+      by (auto simp add: mult_strict_left_mono mult_strict_left_mono_neg)
+  qed
+qed auto
 
 text \<open>
   The ``conjunction of implication'' lemmas produce two cases when the
@@ -2364,29 +2386,29 @@
 lemma add_diff_inverse: "\<not> a < b \<Longrightarrow> b + (a - b) = a"
   by simp
 
-lemma add_le_imp_le_diff: "i + k \<le> n \<Longrightarrow> i \<le> n - k"
-  apply (subst add_le_cancel_right [where c=k, symmetric])
-  apply (frule le_add_diff_inverse2)
-  apply (simp only: add.assoc [symmetric])
-  using add_implies_diff
-  apply fastforce
-  done
+lemma add_le_imp_le_diff: 
+  assumes "i + k \<le> n" shows "i \<le> n - k"
+proof -
+  have "n - (i + k) + i + k = n"
+    by (simp add: assms add.assoc)
+  with assms add_implies_diff have "i + k \<le> n - k + k"
+    by fastforce
+  then show ?thesis
+    by simp
+qed
 
 lemma add_le_add_imp_diff_le:
   assumes 1: "i + k \<le> n"
     and 2: "n \<le> j + k"
   shows "i + k \<le> n \<Longrightarrow> n \<le> j + k \<Longrightarrow> n - k \<le> j"
 proof -
-  have "n - (i + k) + (i + k) = n"
-    using 1 by simp
+  have "n - (i + k) + i + k = n"
+    using 1 by (simp add: add.assoc)
   moreover have "n - k = n - k - i + i"
     using 1 by (simp add: add_le_imp_le_diff)
   ultimately show ?thesis
-    using 2
-    apply (simp add: add.assoc [symmetric])
-    apply (rule add_le_imp_le_diff [of _ k "j + k", simplified add_diff_cancel_right'])
-    apply (simp add: add.commute diff_diff_add)
-    done
+    using 2 add_le_imp_le_diff [of "n-k" k "j + k"]
+    by (simp add: add.commute diff_diff_add)
 qed
 
 lemma less_1_mult: "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n"
diff -r 54ac957c53ec -r 23abd7f9f054 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Apr 06 22:28:41 2020 +0200
+++ b/src/HOL/Set_Interval.thy	Mon Apr 06 22:29:40 2020 +0200
@@ -812,10 +812,10 @@
     greaterThanLessThan_def)
 
 lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
-by (auto simp add: atLeastAtMost_def)
+  by auto
 
 lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}"
-by auto
+  by auto
 
 text \<open>The analogous result is useful on \<^typ>\<open>int\<close>:\<close>
 (* here, because we don't have an own int section *)
diff -r 54ac957c53ec -r 23abd7f9f054 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Mon Apr 06 22:28:41 2020 +0200
+++ b/src/HOL/Transfer.thy	Mon Apr 06 22:29:40 2020 +0200
@@ -162,31 +162,33 @@
 using assms by(auto simp add: right_total_def)
 
 lemma right_total_alt_def2:
-  "right_total R \<longleftrightarrow> ((R ===> (\<longrightarrow>)) ===> (\<longrightarrow>)) All All"
-  unfolding right_total_def rel_fun_def
-  apply (rule iffI, fast)
-  apply (rule allI)
-  apply (drule_tac x="\<lambda>x. True" in spec)
-  apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec)
-  apply fast
-  done
+  "right_total R \<longleftrightarrow> ((R ===> (\<longrightarrow>)) ===> (\<longrightarrow>)) All All" (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    unfolding right_total_def rel_fun_def by blast
+next
+  assume \<section>: ?rhs
+  show ?lhs
+    using \<section> [unfolded rel_fun_def, rule_format, of "\<lambda>x. True" "\<lambda>y. \<exists>x. R x y"]
+    unfolding right_total_def by blast
+qed
 
 lemma right_unique_alt_def2:
   "right_unique R \<longleftrightarrow> (R ===> R ===> (\<longrightarrow>)) (=) (=)"
   unfolding right_unique_def rel_fun_def by auto
 
 lemma bi_total_alt_def2:
-  "bi_total R \<longleftrightarrow> ((R ===> (=)) ===> (=)) All All"
-  unfolding bi_total_def rel_fun_def
-  apply (rule iffI, fast)
-  apply safe
-  apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec)
-  apply (drule_tac x="\<lambda>y. True" in spec)
-  apply fast
-  apply (drule_tac x="\<lambda>x. True" in spec)
-  apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec)
-  apply fast
-  done
+  "bi_total R \<longleftrightarrow> ((R ===> (=)) ===> (=)) All All" (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    unfolding bi_total_def rel_fun_def by blast
+next
+  assume \<section>: ?rhs
+  show ?lhs
+    using \<section> [unfolded rel_fun_def, rule_format, of "\<lambda>x. \<exists>y. R x y" "\<lambda>y. True"]
+    using \<section> [unfolded rel_fun_def, rule_format, of "\<lambda>x. True" "\<lambda>y. \<exists>x. R x y"]
+    by (auto simp: bi_total_def)
+qed
 
 lemma bi_unique_alt_def2:
   "bi_unique R \<longleftrightarrow> (R ===> R ===> (=)) (=) (=)"
@@ -194,19 +196,19 @@
 
 lemma [simp]:
   shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
-  and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
-by(auto simp add: left_unique_def right_unique_def)
+    and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
+  by(auto simp add: left_unique_def right_unique_def)
 
 lemma [simp]:
   shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
-  and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
-by(simp_all add: left_total_def right_total_def)
+    and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
+  by(simp_all add: left_total_def right_total_def)
 
 lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
-by(auto simp add: bi_unique_def)
+  by(auto simp add: bi_unique_def)
 
 lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
-by(auto simp add: bi_total_def)
+  by(auto simp add: bi_total_def)
 
 lemma right_unique_alt_def: "right_unique R = (conversep R OO R \<le> (=))" unfolding right_unique_def by blast
 lemma left_unique_alt_def: "left_unique R = (R OO (conversep R) \<le> (=))" unfolding left_unique_def by blast
@@ -230,21 +232,21 @@
 
 
 lemma is_equality_lemma: "(\<And>R. is_equality R \<Longrightarrow> PROP (P R)) \<equiv> PROP (P (=))"
-  apply (unfold is_equality_def)
-  apply (rule equal_intr_rule)
-   apply (drule meta_spec)
-   apply (erule meta_mp)
-   apply (rule refl)
-  apply simp
-  done
+  unfolding is_equality_def
+proof (rule equal_intr_rule)
+  show "(\<And>R. R = (=) \<Longrightarrow> PROP P R) \<Longrightarrow> PROP P (=)"
+    apply (drule meta_spec)
+    apply (erule meta_mp [OF _ refl])
+    done
+qed simp
 
 lemma Domainp_lemma: "(\<And>R. Domainp T = R \<Longrightarrow> PROP (P R)) \<equiv> PROP (P (Domainp T))"
-  apply (rule equal_intr_rule)
-   apply (drule meta_spec)
-   apply (erule meta_mp)
-   apply (rule refl)
-  apply simp
-  done
+proof (rule equal_intr_rule)
+  show "(\<And>R. Domainp T = R \<Longrightarrow> PROP P R) \<Longrightarrow> PROP P (Domainp T)"
+    apply (drule meta_spec)
+    apply (erule meta_mp [OF _ refl])
+    done
+qed simp
 
 ML_file \<open>Tools/Transfer/transfer.ML\<close>
 declare refl [transfer_rule]
@@ -266,14 +268,21 @@
 
 lemma Domainp_pred_fun_eq[relator_domain]:
   assumes "left_unique T"
-  shows "Domainp (T ===> S) = pred_fun (Domainp T) (Domainp S)"
-  using assms unfolding rel_fun_def Domainp_iff[abs_def] left_unique_def fun_eq_iff pred_fun_def
-  apply safe
-   apply blast
-  apply (subst all_comm)
-  apply (rule choice)
-  apply blast
-  done
+  shows "Domainp (T ===> S) = pred_fun (Domainp T) (Domainp S)"   (is "?lhs = ?rhs")
+proof (intro ext iffI)
+  fix x
+  assume "?lhs x"
+  then show "?rhs x"
+    using assms unfolding rel_fun_def pred_fun_def by blast
+next
+  fix x
+  assume "?rhs x"
+  then have "\<exists>g. \<forall>y xa. T xa y \<longrightarrow> S (x xa) (g y)"
+    using assms unfolding Domainp_iff left_unique_def  pred_fun_def
+    by (intro choice) blast
+  then show "?lhs x"
+    by blast
+qed
 
 text \<open>Properties are preserved by relation composition.\<close>
 
@@ -295,10 +304,10 @@
   unfolding right_unique_def OO_def by fast
 
 lemma left_total_OO: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
-unfolding left_total_def OO_def by fast
+  unfolding left_total_def OO_def by fast
 
 lemma left_unique_OO: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
-unfolding left_unique_def OO_def by blast
+  unfolding left_unique_def OO_def by blast
 
 
 subsection \<open>Properties of relators\<close>
@@ -322,18 +331,22 @@
   unfolding bi_unique_def by simp
 
 lemma left_total_fun[transfer_rule]:
-  "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
-  unfolding left_total_def rel_fun_def
-  apply (rule allI, rename_tac f)
-  apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
-  apply clarify
-  apply (subgoal_tac "(THE x. A x y) = x", simp)
-  apply (rule someI_ex)
-  apply (simp)
-  apply (rule the_equality)
-  apply assumption
-  apply (simp add: left_unique_def)
-  done
+  assumes "left_unique A" "left_total B"
+  shows "left_total (A ===> B)"
+  unfolding left_total_def 
+proof
+  fix f
+  show "Ex ((A ===> B) f)"
+    unfolding rel_fun_def
+  proof (intro exI strip)
+    fix x y
+    assume A: "A x y"
+    have "(THE x. A x y) = x"
+      using A assms by (simp add: left_unique_def the_equality)
+    then show "B (f x) (SOME z. B (f (THE x. A x y)) z)"
+      using assms by (force simp: left_total_def intro: someI_ex)
+  qed
+qed
 
 lemma left_unique_fun[transfer_rule]:
   "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
@@ -341,18 +354,22 @@
   by (clarify, rule ext, fast)
 
 lemma right_total_fun [transfer_rule]:
-  "\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)"
-  unfolding right_total_def rel_fun_def
-  apply (rule allI, rename_tac g)
-  apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
-  apply clarify
-  apply (subgoal_tac "(THE y. A x y) = y", simp)
-  apply (rule someI_ex)
-  apply (simp)
-  apply (rule the_equality)
-  apply assumption
-  apply (simp add: right_unique_def)
-  done
+  assumes "right_unique A" "right_total B"
+  shows "right_total (A ===> B)"
+  unfolding right_total_def 
+proof
+  fix g
+  show "\<exists>x. (A ===> B) x g"
+    unfolding rel_fun_def
+  proof (intro exI strip)
+    fix x y
+    assume A: "A x y"
+    have "(THE y. A x y) = y"
+      using A assms by (simp add: right_unique_def the_equality)
+    then show "B (SOME z. B z (g (THE y. A x y))) (g y)"
+      using assms by (force simp: right_total_def intro: someI_ex)
+  qed
+qed
 
 lemma right_unique_fun [transfer_rule]:
   "\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)"
@@ -435,8 +452,8 @@
   assumes "right_total B"
   assumes "bi_unique A"
   shows "((A ===> B ===> (=)) ===> implies) left_unique left_unique"
-using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
-by metis
+  using assms unfolding left_unique_def right_total_def bi_unique_def rel_fun_def
+  by metis
 
 lemma eq_transfer [transfer_rule]:
   assumes "bi_unique A"
@@ -446,14 +463,14 @@
 lemma right_total_Ex_transfer[transfer_rule]:
   assumes "right_total A"
   shows "((A ===> (=)) ===> (=)) (Bex (Collect (Domainp A))) Ex"
-using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def]
-by fast
+  using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff
+  by fast
 
 lemma right_total_All_transfer[transfer_rule]:
   assumes "right_total A"
   shows "((A ===> (=)) ===> (=)) (Ball (Collect (Domainp A))) All"
-using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def]
-by fast
+  using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff
+  by fast
 
 context
   includes lifting_syntax
@@ -480,7 +497,7 @@
 lemma Ex1_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A" "bi_total A"
   shows "((A ===> (=)) ===> (=)) Ex1 Ex1"
-unfolding Ex1_def[abs_def] by transfer_prover
+unfolding Ex1_def by transfer_prover
 
 declare If_transfer [transfer_rule]
 
@@ -498,7 +515,7 @@
 lemma fun_upd_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"
   shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
-  unfolding fun_upd_def [abs_def] by transfer_prover
+  unfolding fun_upd_def  by transfer_prover
 
 lemma case_nat_transfer [transfer_rule]:
   "(A ===> ((=) ===> A) ===> (=) ===> A) case_nat case_nat"
@@ -517,18 +534,18 @@
   assumes [transfer_rule]: "(A ===> A ===> (=)) (\<le>) (\<le>)"
   assumes [transfer_rule]: "(B ===> B ===> (=)) (\<le>) (\<le>)"
   shows "((A ===> B) ===> (=)) mono mono"
-unfolding mono_def[abs_def] by transfer_prover
+unfolding mono_def by transfer_prover
 
 lemma right_total_relcompp_transfer[transfer_rule]:
   assumes [transfer_rule]: "right_total B"
   shows "((A ===> B ===> (=)) ===> (B ===> C ===> (=)) ===> A ===> C ===> (=))
     (\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) (OO)"
-unfolding OO_def[abs_def] by transfer_prover
+unfolding OO_def by transfer_prover
 
 lemma relcompp_transfer[transfer_rule]:
   assumes [transfer_rule]: "bi_total B"
   shows "((A ===> B ===> (=)) ===> (B ===> C ===> (=)) ===> A ===> C ===> (=)) (OO) (OO)"
-unfolding OO_def[abs_def] by transfer_prover
+unfolding OO_def by transfer_prover
 
 lemma right_total_Domainp_transfer[transfer_rule]:
   assumes [transfer_rule]: "right_total B"
@@ -538,7 +555,7 @@
 lemma Domainp_transfer[transfer_rule]:
   assumes [transfer_rule]: "bi_total B"
   shows "((A ===> B ===> (=)) ===> A ===> (=)) Domainp Domainp"
-unfolding Domainp_iff[abs_def] by transfer_prover
+unfolding Domainp_iff by transfer_prover
 
 lemma reflp_transfer[transfer_rule]:
   "bi_total A \<Longrightarrow> ((A ===> A ===> (=)) ===> (=)) reflp reflp"
@@ -546,38 +563,38 @@
   "right_total A \<Longrightarrow> ((A ===> A ===> (=)) ===> implies) reflp reflp"
   "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
   "bi_total A \<Longrightarrow> ((A ===> A ===> (=)) ===> rev_implies) reflp reflp"
-unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
+unfolding reflp_def rev_implies_def bi_total_def right_total_def rel_fun_def
 by fast+
 
 lemma right_unique_transfer [transfer_rule]:
   "\<lbrakk> right_total A; right_total B; bi_unique B \<rbrakk>
   \<Longrightarrow> ((A ===> B ===> (=)) ===> implies) right_unique right_unique"
-unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
+unfolding right_unique_def right_total_def bi_unique_def rel_fun_def
 by metis
 
 lemma left_total_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_total A" "bi_total B"
   shows "((A ===> B ===> (=)) ===> (=)) left_total left_total"
-unfolding left_total_def[abs_def] by transfer_prover
+unfolding left_total_def by transfer_prover
 
 lemma right_total_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_total A" "bi_total B"
   shows "((A ===> B ===> (=)) ===> (=)) right_total right_total"
-unfolding right_total_def[abs_def] by transfer_prover
+unfolding right_total_def by transfer_prover
 
 lemma left_unique_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A" "bi_total A" "bi_total B"
   shows "((A ===> B ===> (=)) ===> (=)) left_unique left_unique"
-unfolding left_unique_def[abs_def] by transfer_prover
+unfolding left_unique_def by transfer_prover
 
 lemma prod_pred_parametric [transfer_rule]:
   "((A ===> (=)) ===> (B ===> (=)) ===> rel_prod A B ===> (=)) pred_prod pred_prod"
-unfolding prod.pred_set[abs_def] Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps 
+unfolding prod.pred_set Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps 
 by simp transfer_prover
 
 lemma apfst_parametric [transfer_rule]:
   "((A ===> B) ===> rel_prod A C ===> rel_prod B C) apfst apfst"
-unfolding apfst_def[abs_def] by transfer_prover
+unfolding apfst_def by transfer_prover
 
 lemma rel_fun_eq_eq_onp: "((=) ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
 unfolding eq_onp_def rel_fun_def by auto
@@ -589,7 +606,7 @@
 lemma eq_onp_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"
   shows "((A ===> (=)) ===> A ===> A ===> (=)) eq_onp eq_onp"
-unfolding eq_onp_def[abs_def] by transfer_prover
+unfolding eq_onp_def by transfer_prover
 
 lemma rtranclp_parametric [transfer_rule]:
   assumes "bi_unique A" "bi_total A"
@@ -633,11 +650,11 @@
 lemma right_unique_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_total A" "bi_unique B" "bi_total B"
   shows "((A ===> B ===> (=)) ===> (=)) right_unique right_unique"
-unfolding right_unique_def[abs_def] by transfer_prover
+  unfolding right_unique_def by transfer_prover
 
 lemma map_fun_parametric [transfer_rule]:
   "((A ===> B) ===> (C ===> D) ===> (B ===> C) ===> A ===> D) map_fun map_fun"
-unfolding map_fun_def[abs_def] by transfer_prover
+  unfolding map_fun_def by transfer_prover
 
 end
 
@@ -652,14 +669,14 @@
   \<open>((\<longleftrightarrow>) ===> (\<cong>)) of_bool of_bool\<close>
     if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
     for R :: \<open>'a::zero_neq_one \<Rightarrow> 'b::zero_neq_one \<Rightarrow> bool\<close>  (infix \<open>\<cong>\<close> 50)
-  by (unfold of_bool_def [abs_def]) transfer_prover
+  unfolding of_bool_def by transfer_prover
 
 lemma transfer_rule_of_nat:
   "((=) ===> (\<cong>)) of_nat of_nat"
     if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
     \<open>((\<cong>) ===> (\<cong>) ===> (\<cong>)) (+) (+)\<close>
   for R :: \<open>'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool\<close>  (infix \<open>\<cong>\<close> 50)
-  by (unfold of_nat_def [abs_def]) transfer_prover
+  unfolding of_nat_def by transfer_prover
 
 end