# HG changeset patch
# User nipkow
# Date 1665490931 -7200
# Node ID 26524d0b43959e11c705f8aeeb7208443a8242f0
# Parent  5fd8ba24ca487bcf736847f62b66067a24906bd8
added and reorganized lemmas (some suggested by Jeremy Sylvestre)

diff -r 5fd8ba24ca48 -r 26524d0b4395 src/HOL/Fun.thy
--- 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)