--- a/src/HOL/Nat.thy Sun Oct 29 19:39:03 2017 +0100
+++ b/src/HOL/Nat.thy Mon Oct 30 13:18:41 2017 +0000
@@ -166,9 +166,36 @@
text \<open>Injectiveness and distinctness lemmas\<close>
-lemma (in semidom_divide) inj_times:
- "inj (times a)" if "a \<noteq> 0"
-proof (rule injI)
+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
+
+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"
@@ -177,20 +204,16 @@
by simp
qed
-lemma (in cancel_ab_semigroup_add) inj_plus:
- "inj (plus a)"
-proof (rule injI)
- 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_Suc[simp]: "inj_on Suc N"
+end
+
+lemma inj_Suc [simp]:
+ "inj_on Suc N"
by (simp add: inj_on_def)
+lemma bij_betw_Suc [simp]:
+ "bij_betw Suc M N \<longleftrightarrow> Suc ` M = N"
+ by (simp add: bij_betw_def)
+
lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R"
by (rule notE) (rule Suc_not_Zero)
@@ -338,16 +361,9 @@
for m n :: nat
by (induct m) simp_all
-lemma inj_on_add_nat [simp]: "inj_on (\<lambda>n. n + k) N"
- for k :: nat
-proof (induct k)
- case 0
- then show ?case by simp
-next
- case (Suc k)
- show ?case
- using comp_inj_on [OF Suc inj_Suc] by (simp add: o_def)
-qed
+lemma plus_1_eq_Suc:
+ "plus 1 = Suc"
+ by (simp add: fun_eq_iff)
lemma Suc_eq_plus1: "Suc n = n + 1"
by simp