--- 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