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