--- a/src/HOL/Nat.thy Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Nat.thy Mon Jan 14 18:35:03 2019 +0000
@@ -166,78 +166,6 @@
text \<open>Injectiveness and distinctness lemmas\<close>
-context cancel_ab_semigroup_add
-begin
-
-lemma inj_on_add [simp]:
- "inj_on (plus a) A"
-proof (rule inj_onI)
- fix b c
- assume "a + b = a + c"
- then have "a + b - a = a + c - a"
- by (simp only:)
- then show "b = c"
- by simp
-qed
-
-lemma inj_on_add' [simp]:
- "inj_on (\<lambda>b. b + a) A"
- using inj_on_add [of a A] by (simp add: add.commute [of _ a])
-
-lemma bij_betw_add [simp]:
- "bij_betw (plus a) A B \<longleftrightarrow> plus a ` A = B"
- by (simp add: bij_betw_def)
-
-end
-
-text \<open>Translation lemmas\<close>
-
-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
-
-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
-
-lemma inj_on_mult:
- "inj_on (times a) A" if "a \<noteq> 0"
-proof (rule inj_onI)
- fix b c
- assume "a * b = a * c"
- then have "a * b div a = a * c div a"
- by (simp only:)
- with that show "b = c"
- by simp
-qed
-
-end
-
lemma inj_Suc [simp]:
"inj_on Suc N"
by (simp add: inj_on_def)