# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1586103146 -3600
# Node ID 65489718f4dcc4c8ef8f1ffb1a013e3c87a716f0
# Parent  d682b4000a77318f114134f4be29ca9bcc22c091
Tidied up more ancient, horrible proofs. Liberalised frac_le

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