# HG changeset patch
# User immler
# Date 1572193610 -3600
# Node ID f140135ff375be4866ebb91b5fd43986dd977128
# Parent  678b2abe9f7d372876d8eae6be2091a565a53d00
example applications of the 'metric' decision procedure, by Maximilian Schäffeler

diff -r 678b2abe9f7d -r f140135ff375 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Oct 27 16:32:01 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Oct 27 17:26:50 2019 +0100
@@ -13,15 +13,7 @@
 
 lemma ball_trans:
   assumes "y \<in> ball z q" "r + q \<le> s" shows "ball y r \<subseteq> ball z s"
-proof safe
-  fix x assume x: "x \<in> ball y r"
-  have "dist z x \<le> dist z y + dist y x"
-    by (rule dist_triangle)
-  also have "\<dots> < s"
-    using assms x by auto
-  finally show "x \<in> ball z s"
-    by simp
-qed
+  using assms by metric
 
 lemma has_integral_implies_lebesgue_measurable_cbox:
   fixes f :: "'a :: euclidean_space \<Rightarrow> real"
diff -r 678b2abe9f7d -r f140135ff375 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 27 16:32:01 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 27 17:26:50 2019 +0100
@@ -142,12 +142,7 @@
     then show ?rhs
       by (simp add: dist_norm)
   qed
-next
-  assume ?rhs
-  then show ?lhs
-    by (auto simp: ball_def dist_norm)
-      (metis add.commute add_le_cancel_right dist_norm dist_triangle3 order_trans)
-qed
+qed metric
 
 lemma cball_subset_ball_iff: "cball a r \<subseteq> ball a' r' \<longleftrightarrow> dist a a' + r < r' \<or> r < 0"
   (is "?lhs \<longleftrightarrow> ?rhs")
@@ -188,8 +183,7 @@
 next
   assume ?rhs
   then show ?lhs
-    by (auto simp: ball_def dist_norm)
-      (metis add.commute add_le_cancel_right dist_norm dist_triangle3 le_less_trans)
+    by metric
 qed
 
 lemma ball_subset_cball_iff: "ball a r \<subseteq> cball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r \<le> 0"
@@ -198,7 +192,7 @@
 proof (cases "r \<le> 0")
   case True
   then show ?thesis
-    using dist_not_less_zero less_le_trans by force
+    by metric
 next
   case False
   show ?thesis
@@ -211,7 +205,7 @@
   next
     assume ?rhs
     with False show ?lhs
-      using ball_subset_cball cball_subset_cball_iff by blast
+      by metric
   qed
 qed
 
@@ -221,24 +215,18 @@
         (is "?lhs = ?rhs")
 proof (cases "r \<le> 0")
   case True then show ?thesis
-    using dist_not_less_zero less_le_trans by force
+    by metric
 next
   case False show ?thesis
   proof
     assume ?lhs
     then have "0 < r'"
-      by (metis (no_types) False \<open>?lhs\<close> centre_in_ball dist_norm le_less_trans mem_ball norm_ge_zero not_less subsetD)
+      using False by metric
     then have "(cball a r \<subseteq> cball a' r')"
       by (metis False\<open>?lhs\<close> closure_ball closure_mono not_less)
     then show ?rhs
       using False cball_subset_cball_iff by fastforce
-  next
-  assume ?rhs then show ?lhs
-    apply (auto simp: ball_def)
-    apply (metis add.commute add_le_cancel_right dist_commute dist_triangle_lt not_le order_trans)
-    using dist_not_less_zero order.strict_trans2 apply blast
-    done
-  qed
+  qed metric
 qed