diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Nat.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -190,15 +190,38 @@
 
 end
 
+text \<open>Translation lemmas\<close>
+
 context ab_group_add
 begin
 
-lemma surj_plus [simp]:
-  "surj (plus a)"
+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
 
+lemma translation_Compl:
+  fixes a :: "'a::ab_group_add"
+  shows "(\<lambda>x. a + x) ` (- t) = - ((\<lambda>x. a + x) ` t)"
+  apply (auto simp: image_iff)
+  apply (rule_tac x="x - a" in bexI, auto)
+  done
+
+lemma translation_UNIV:
+  fixes a :: "'a::ab_group_add"
+  shows "range (\<lambda>x. a + x) = UNIV"
+  by (fact surj_plus)
+
+lemma translation_diff:
+  fixes a :: "'a::ab_group_add"
+  shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)"
+  by auto
+
+lemma translation_Int:
+  fixes a :: "'a::ab_group_add"
+  shows "(\<lambda>x. a + x) ` (s \<inter> t) = ((\<lambda>x. a + x) ` s) \<inter> ((\<lambda>x. a + x) ` t)"
+  by auto
+
 context semidom_divide
 begin