--- a/src/HOL/Filter.thy Thu Apr 09 21:58:34 2020 +0200
+++ b/src/HOL/Filter.thy Fri Apr 10 22:51:18 2020 +0100
@@ -300,20 +300,15 @@
"eventually P (inf F F') \<longleftrightarrow>
(\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
unfolding inf_filter_def
- apply (rule eventually_Abs_filter, rule is_filter.intro)
- apply (fast intro: eventually_True)
- apply clarify
- apply (intro exI conjI)
- apply (erule (1) eventually_conj)
- apply (erule (1) eventually_conj)
- apply simp
- apply auto
+ apply (rule eventually_Abs_filter [OF is_filter.intro])
+ apply (blast intro: eventually_True)
+ apply (force elim!: eventually_conj)+
done
lemma eventually_Sup:
"eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"
unfolding Sup_filter_def
- apply (rule eventually_Abs_filter, rule is_filter.intro)
+ apply (rule eventually_Abs_filter [OF is_filter.intro])
apply (auto intro: eventually_conj elim!: eventually_rev_mp)
done
@@ -557,8 +552,7 @@
lemma eventually_filtermap:
"eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"
unfolding filtermap_def
- apply (rule eventually_Abs_filter)
- apply (rule is_filter.intro)
+ apply (rule eventually_Abs_filter [OF is_filter.intro])
apply (auto elim!: eventually_rev_mp)
done
@@ -746,10 +740,7 @@
lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"
unfolding le_filter_def eventually_principal
- apply safe
- apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
- apply (auto elim: eventually_mono)
- done
+ by (force elim: eventually_mono)
lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
unfolding eq_iff by simp
@@ -1172,11 +1163,7 @@
lemma eventually_prod_same: "eventually P (F \<times>\<^sub>F F) \<longleftrightarrow>
(\<exists>Q. eventually Q F \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))"
- unfolding eventually_prod_filter
- apply safe
- apply (rule_tac x="inf Pf Pg" in exI)
- apply (auto simp: inf_fun_def intro!: eventually_conj)
- done
+ unfolding eventually_prod_filter by (blast intro!: eventually_conj)
lemma eventually_prod_sequentially:
"eventually P (sequentially \<times>\<^sub>F sequentially) \<longleftrightarrow> (\<exists>N. \<forall>m \<ge> N. \<forall>n \<ge> N. P (n, m))"
@@ -1227,13 +1214,15 @@
using prod_filter_INF[of "{A}" J "\<lambda>x. x" B] by simp
lemma prod_filtermap1: "prod_filter (filtermap f F) G = filtermap (apfst f) (prod_filter F G)"
- apply(clarsimp simp add: filter_eq_iff eventually_filtermap eventually_prod_filter; safe)
+ unfolding filter_eq_iff eventually_filtermap eventually_prod_filter
+ apply safe
subgoal by auto
subgoal for P Q R by(rule exI[where x="\<lambda>y. \<exists>x. y = f x \<and> Q x"])(auto intro: eventually_mono)
done
lemma prod_filtermap2: "prod_filter F (filtermap g G) = filtermap (apsnd g) (prod_filter F G)"
- apply(clarsimp simp add: filter_eq_iff eventually_filtermap eventually_prod_filter; safe)
+ unfolding filter_eq_iff eventually_filtermap eventually_prod_filter
+ apply safe
subgoal by auto
subgoal for P Q R by(auto intro: exI[where x="\<lambda>y. \<exists>x. y = g x \<and> R x"] eventually_mono)
done
@@ -1291,10 +1280,12 @@
assumes "filterlim f F G" and ord: "F \<le> F'" "G' \<le> G"
assumes eq: "eventually (\<lambda>x. f x = f' x) G'"
shows "filterlim f' F' G'"
- apply (rule filterlim_cong[OF refl refl eq, THEN iffD1])
- apply (rule filterlim_mono[OF _ ord])
- apply fact
- done
+proof -
+ have "filterlim f F' G'"
+ by (simp add: filterlim_mono[OF _ ord] assms)
+ then show ?thesis
+ by (rule filterlim_cong[OF refl refl eq, THEN iffD1])
+qed
lemma filtermap_mono_strong: "inj f \<Longrightarrow> filtermap f F \<le> filtermap f G \<longleftrightarrow> F \<le> G"
apply (safe intro!: filtermap_mono)
@@ -1458,8 +1449,7 @@
assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
thus "eventually (\<lambda>x. f x < Z) F"
- apply (rule eventually_mono)
- using 1 by auto
+ by (rule eventually_mono) (use 1 in auto)
next
fix Z :: 'b
show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
--- a/src/HOL/Groups.thy Thu Apr 09 21:58:34 2020 +0200
+++ b/src/HOL/Groups.thy Fri Apr 10 22:51:18 2020 +0100
@@ -635,9 +635,7 @@
text \<open>non-strict, in both arguments\<close>
lemma add_mono: "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
- apply (erule add_right_mono [THEN order_trans])
- apply (simp add: add.commute add_left_mono)
- done
+ by (simp add: add.commute add_left_mono add_right_mono [THEN order_trans])
end
@@ -656,20 +654,16 @@
by (simp add: add.commute [of _ c] add_strict_left_mono)
subclass strict_ordered_ab_semigroup_add
- apply standard
- apply (erule add_strict_right_mono [THEN less_trans])
- apply (erule add_strict_left_mono)
- done
+proof
+ show "\<And>a b c d. \<lbrakk>a < b; c < d\<rbrakk> \<Longrightarrow> a + c < b + d"
+ by (iprover intro: add_strict_left_mono add_strict_right_mono less_trans)
+qed
lemma add_less_le_mono: "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
- apply (erule add_strict_right_mono [THEN less_le_trans])
- apply (erule add_left_mono)
- done
+ by (iprover intro: add_left_mono add_strict_right_mono less_le_trans)
lemma add_le_less_mono: "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
- apply (erule add_right_mono [THEN le_less_trans])
- apply (erule add_strict_left_mono)
- done
+ by (iprover intro: add_strict_left_mono add_right_mono less_le_trans)
end
@@ -684,12 +678,7 @@
from less have le: "c + a \<le> c + b"
by (simp add: order_le_less)
have "a \<le> b"
- apply (insert le)
- apply (drule add_le_imp_le_left)
- apply (insert le)
- apply (drule add_le_imp_le_left)
- apply assumption
- done
+ using add_le_imp_le_left [OF le] .
moreover have "a \<noteq> b"
proof (rule ccontr)
assume "\<not> ?thesis"
@@ -711,10 +700,7 @@
by (blast intro: add_less_imp_less_right add_strict_right_mono)
lemma add_le_cancel_left [simp]: "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
- apply auto
- apply (drule add_le_imp_le_left)
- apply (simp_all add: add_left_mono)
- done
+ by (auto simp: dest: add_le_imp_le_left add_left_mono)
lemma add_le_cancel_right [simp]: "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
by (simp add: add.commute [of a c] add.commute [of b c])
@@ -927,17 +913,7 @@
qed
lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
-proof -
- have mm: "- (- a) < - b \<Longrightarrow> - (- b) < -a" for a b :: 'a
- by (simp only: minus_less_iff)
- have "- (- a) \<le> - b \<longleftrightarrow> b \<le> - a"
- apply (auto simp only: le_less)
- apply (drule mm)
- apply (simp_all)
- apply (drule mm[simplified], assumption)
- done
- then show ?thesis by simp
-qed
+ by (auto simp: order.order_iff_strict less_minus_iff)
lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
by (auto simp add: le_less minus_less_iff)
@@ -955,17 +931,17 @@
lemma diff_less_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a - b < c \<longleftrightarrow> a < c + b"
- apply (subst less_iff_diff_less_0 [of a])
- apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
- apply (simp add: algebra_simps)
- done
+proof (subst less_iff_diff_less_0 [of a])
+ show "(a - b < c) = (a - (c + b) < 0)"
+ by (simp add: algebra_simps less_iff_diff_less_0 [of _ c])
+qed
lemma less_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a < c - b \<longleftrightarrow> a + b < c"
- apply (subst less_iff_diff_less_0 [of "a + b"])
- apply (subst less_iff_diff_less_0 [of a])
- apply (simp add: algebra_simps)
- done
+proof (subst less_iff_diff_less_0 [of "a + b"])
+ show "(a < c - b) = (a + b - c < 0)"
+ by (simp add: algebra_simps less_iff_diff_less_0 [of a])
+qed
lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \<longleftrightarrow> a > b"
by (simp add: less_diff_eq)
@@ -1070,11 +1046,10 @@
assume *: "\<not> ?thesis"
then have "b \<le> a" by (simp add: linorder_not_le)
then have "c + b \<le> c + a" by (rule add_left_mono)
- with le1 have "a = b"
- apply -
- apply (drule antisym)
- apply simp_all
- done
+ then have "c + a = c + b"
+ using le1 by (iprover intro: antisym)
+ then have "a = b"
+ by simp
with * show False
by (simp add: linorder_not_le [symmetric])
qed
@@ -1146,10 +1121,7 @@
qed
lemma double_zero_sym [simp]: "0 = a + a \<longleftrightarrow> a = 0"
- apply (rule iffI)
- apply (drule sym)
- apply simp_all
- done
+ using double_zero [of a] by (simp only: eq_commute)
lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
proof
@@ -1358,13 +1330,17 @@
lemma dense_eq0_I:
fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
- shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) \<Longrightarrow> x = 0"
- apply (cases "\<bar>x\<bar> = 0")
- apply simp
- apply (simp only: zero_less_abs_iff [symmetric])
- apply (drule dense)
- apply (auto simp add: not_less [symmetric])
- done
+ assumes "\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e"
+ shows "x = 0"
+proof (cases "\<bar>x\<bar> = 0")
+ case False
+ then have "\<bar>x\<bar> > 0"
+ by simp
+ then obtain z where "0 < z" "z < \<bar>x\<bar>"
+ using dense by force
+ then show ?thesis
+ using assms by (simp flip: not_less)
+qed auto
hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
--- a/src/HOL/Rat.thy Thu Apr 09 21:58:34 2020 +0200
+++ b/src/HOL/Rat.thy Fri Apr 10 22:51:18 2020 +0100
@@ -463,16 +463,12 @@
lemma positive_add: "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)"
apply transfer
- apply (simp add: zero_less_mult_iff)
- apply (elim disjE)
- apply (simp_all add: add_pos_pos add_neg_neg mult_pos_neg mult_neg_pos mult_neg_neg)
+ apply (auto simp add: zero_less_mult_iff add_pos_pos add_neg_neg mult_pos_neg mult_neg_pos mult_neg_neg)
done
lemma positive_mult: "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
apply transfer
- apply (drule (1) mult_pos_pos)
- apply (simp add: ac_simps)
- done
+ by (metis fst_conv mult.commute mult_pos_neg2 snd_conv zero_less_mult_iff)
lemma positive_minus: "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
by transfer (auto simp: neq_iff zero_less_mult_iff mult_less_0_iff)
@@ -495,24 +491,15 @@
by (rule abs_rat_def)
show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
unfolding less_eq_rat_def less_rat_def
- apply auto
- apply (drule (1) positive_add)
- apply (simp_all add: positive_zero)
- done
+ using positive_add positive_zero by force
show "a \<le> a"
unfolding less_eq_rat_def by simp
show "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"
unfolding less_eq_rat_def less_rat_def
- apply auto
- apply (drule (1) positive_add)
- apply (simp add: algebra_simps)
- done
+ using positive_add by fastforce
show "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b"
unfolding less_eq_rat_def less_rat_def
- apply auto
- apply (drule (1) positive_add)
- apply (simp add: positive_zero)
- done
+ using positive_add positive_zero by fastforce
show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
unfolding less_eq_rat_def less_rat_def by auto
show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
@@ -522,9 +509,7 @@
by (auto dest!: positive_minus)
show "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
unfolding less_rat_def
- apply (drule (1) positive_mult)
- apply (simp add: algebra_simps)
- done
+ by (metis diff_zero positive_mult right_diff_distrib')
qed
end
@@ -712,8 +697,7 @@
lemma of_rat_eq_iff [simp]: "of_rat a = of_rat b \<longleftrightarrow> a = b"
apply transfer
- apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
- apply (simp only: of_int_mult [symmetric] of_int_eq_iff)
+ apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq flip: of_int_mult)
done
lemma of_rat_eq_0_iff [simp]: "of_rat a = 0 \<longleftrightarrow> a = 0"
@@ -856,46 +840,28 @@
unfolding Rats_def by (rule range_eqI) (rule of_rat_1 [symmetric])
lemma Rats_add [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a + b \<in> \<rat>"
- apply (auto simp add: Rats_def)
- apply (rule range_eqI)
- apply (rule of_rat_add [symmetric])
- done
+ by (metis Rats_cases Rats_of_rat of_rat_add)
lemma Rats_minus_iff [simp]: "- a \<in> \<rat> \<longleftrightarrow> a \<in> \<rat>"
-by (metis Rats_cases Rats_of_rat add.inverse_inverse of_rat_minus)
+ by (metis Rats_cases Rats_of_rat add.inverse_inverse of_rat_minus)
lemma Rats_diff [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a - b \<in> \<rat>"
- apply (auto simp add: Rats_def)
- apply (rule range_eqI)
- apply (rule of_rat_diff [symmetric])
- done
+ by (metis Rats_add Rats_minus_iff diff_conv_add_uminus)
lemma Rats_mult [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a * b \<in> \<rat>"
- apply (auto simp add: Rats_def)
- apply (rule range_eqI)
- apply (rule of_rat_mult [symmetric])
- done
+ by (metis Rats_cases Rats_of_rat of_rat_mult)
lemma Rats_inverse [simp]: "a \<in> \<rat> \<Longrightarrow> inverse a \<in> \<rat>"
for a :: "'a::field_char_0"
- apply (auto simp add: Rats_def)
- apply (rule range_eqI)
- apply (rule of_rat_inverse [symmetric])
- done
+ by (metis Rats_cases Rats_of_rat of_rat_inverse)
lemma Rats_divide [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a / b \<in> \<rat>"
for a b :: "'a::field_char_0"
- apply (auto simp add: Rats_def)
- apply (rule range_eqI)
- apply (rule of_rat_divide [symmetric])
- done
+ by (simp add: divide_inverse)
lemma Rats_power [simp]: "a \<in> \<rat> \<Longrightarrow> a ^ n \<in> \<rat>"
for a :: "'a::field_char_0"
- apply (auto simp add: Rats_def)
- apply (rule range_eqI)
- apply (rule of_rat_power [symmetric])
- done
+ by (metis Rats_cases Rats_of_rat of_rat_power)
lemma Rats_induct [case_names of_rat, induct set: Rats]: "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
by (rule Rats_cases) auto