# HG changeset patch
# User paulson
# Date 1586555478 -3600
# Node ID 63eb6b3ebcfc78062f069f21322740b922b98ce6
# Parent  de37910974da85baa409206609690391f20d406c# Parent  0239bee6bffd67007ccce67b2ca43a36322e5023
merged

diff -r de37910974da -r 63eb6b3ebcfc src/HOL/Filter.thy
--- 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"
diff -r de37910974da -r 63eb6b3ebcfc src/HOL/Groups.thy
--- 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
 
diff -r de37910974da -r 63eb6b3ebcfc src/HOL/Rat.thy
--- 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