Tidied up more ancient, horrible proofs. Liberalised frac_le
--- 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
--- 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