diff -r d682b4000a77 -r 65489718f4dc src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/HOL/Fields.thy	Sun Apr 05 17:12:26 2020 +0100
@@ -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