--- a/src/HOL/Fun.thy Tue Oct 11 12:13:47 2022 +0200
+++ b/src/HOL/Fun.thy Tue Oct 11 14:22:11 2022 +0200
@@ -591,9 +591,6 @@
lemma inj_on_vimage_singleton: "inj_on f A \<Longrightarrow> f -` {a} \<inter> A \<subseteq> {THE x. x \<in> A \<and> f x = a}"
by (auto simp add: inj_on_def intro: the_equality [symmetric])
-lemma (in group_add) inj_uminus[simp, intro]: "inj_on uminus A"
- by (auto intro!: inj_onI)
-
lemma bij_betw_byWitness:
assumes left: "\<forall>a \<in> A. f' (f a) = a"
and right: "\<forall>a' \<in> A'. f (f' a') = a'"
@@ -696,7 +693,7 @@
qed
-subsubsection \<open>Important examples\<close>
+subsubsection \<open>Inj/surj/bij of Algebraic Operations\<close>
context cancel_semigroup_add
begin
@@ -718,6 +715,13 @@
context group_add
begin
+lemma diff_left_imp_eq: "a - b = a - c \<Longrightarrow> b = c"
+unfolding add_uminus_conv_diff[symmetric]
+by(drule local.add_left_imp_eq) simp
+
+lemma inj_uminus[simp, intro]: "inj_on uminus A"
+ by (auto intro!: inj_onI)
+
lemma surj_plus [simp]:
"surj ((+) a)"
proof (standard, simp, standard, simp)
@@ -726,9 +730,28 @@
thus "x \<in> range ((+) a)" by blast
qed
-lemma inj_diff_right [simp]:
- \<open>inj (\<lambda>b. b - a)\<close>
-by (auto intro: injI simp add: algebra_simps)
+lemma surj_plus_right [simp]:
+ "surj (\<lambda>b. b+a)"
+proof (standard, simp, standard, simp)
+ fix b show "b \<in> range (\<lambda>b. b+a)"
+ using diff_add_cancel[of b a, symmetric] by blast
+qed
+
+lemma inj_on_diff_left [simp]:
+ \<open>inj_on ((-) a) A\<close>
+by (auto intro: inj_onI dest!: diff_left_imp_eq)
+
+lemma inj_on_diff_right [simp]:
+ \<open>inj_on (\<lambda>b. b - a) A\<close>
+by (auto intro: inj_onI simp add: algebra_simps)
+
+lemma surj_diff [simp]:
+ "surj ((-) a)"
+proof (standard, simp, standard, simp)
+ fix x
+ have "x = a - (- x + a)" by (simp add: algebra_simps)
+ thus "x \<in> range ((-) a)" by blast
+qed
lemma surj_diff_right [simp]:
"surj (\<lambda>x. x - a)"
@@ -738,6 +761,10 @@
thus "x \<in> range (\<lambda>x. x - a)" by fast
qed
+lemma shows bij_plus: "bij ((+) a)" and bij_plus_right: "bij (\<lambda>x. x + a)"
+ and bij_diff: "bij ((-) a)" and bij_diff_right: "bij (\<lambda>x. x - a)"
+by(simp_all add: bij_def)
+
lemma translation_subtract_Compl:
"(\<lambda>x. x - a) ` (- t) = - ((\<lambda>x. x - a) ` t)"
by(rule bij_image_Compl_eq)