# HG changeset patch
# User haftmann
# Date 1509391746 0
# Node ID 826a5fd4d36c490f29536a5eea83139ac7c357bf
# Parent  80985b62029d9c1e69fba724863d3b30e2bee83a
added lemma

diff -r 80985b62029d -r 826a5fd4d36c src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Mon Oct 30 21:52:31 2017 +0100
+++ b/src/HOL/Analysis/Connected.thy	Mon Oct 30 19:29:06 2017 +0000
@@ -168,7 +168,7 @@
   apply (rule subsetD [OF closure_subset], simp)
   apply (simp add: closure_def, clarify)
   apply (rule closure_ball_lemma)
-  apply (simp add: zero_less_dist_iff)
+  apply simp
   done
 
 (* In a trivial vector space, this fails for e = 0. *)
@@ -1969,7 +1969,7 @@
   then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
     using \<open>a \<notin> U\<close> by (fast elim: eventually_mono)
   then show ?thesis
-    using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute zero_less_dist_iff eventually_at)
+    using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute eventually_at)
 qed
 
 lemma continuous_at_avoid:
@@ -3022,9 +3022,7 @@
 lemma translation_UNIV:
   fixes a :: "'a::ab_group_add"
   shows "range (\<lambda>x. a + x) = UNIV"
-  apply (auto simp: image_iff)
-  apply (rule_tac x="x - a" in exI, auto)
-  done
+  by (fact surj_plus)
 
 lemma translation_diff:
   fixes a :: "'a::ab_group_add"
diff -r 80985b62029d -r 826a5fd4d36c src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Oct 30 21:52:31 2017 +0100
+++ b/src/HOL/Nat.thy	Mon Oct 30 19:29:06 2017 +0000
@@ -190,6 +190,15 @@
 
 end
 
+context ab_group_add
+begin
+
+lemma surj_plus [simp]:
+  "surj (plus a)"
+  by (auto intro: range_eqI [of b "plus a" "b - a" for b] simp add: algebra_simps)
+
+end
+
 context semidom_divide
 begin