author immler Sun, 27 Oct 2019 17:26:50 +0100 changeset 71148 f140135ff375 parent 71147 678b2abe9f7d child 71149 420359ba6acd
example applications of the 'metric' decision procedure, by Maximilian SchÃ¤ffeler
```--- 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"```
```--- 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
qed
-next
-  assume ?rhs
-  then show ?lhs
-    by (auto simp: ball_def dist_norm)
-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)
+    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)