merged

--- a/src/HOL/Fun.thy	Tue Oct 11 11:48:04 2022 +0200
+++ b/src/HOL/Fun.thy	Tue Oct 11 18:52:01 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
@@ -705,10 +702,6 @@
   "inj_on ((+) a) A"
   by (rule inj_onI) simp
 
-lemma inj_add_left:
-  \<open>inj ((+) a)\<close>
-  by simp
-
 lemma inj_on_add' [simp]:
   "inj_on (\<lambda>b. b + a) A"
   by (rule inj_onI) simp
@@ -722,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)
@@ -730,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)"
@@ -742,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)
@@ -927,20 +950,6 @@
   using that UNIV_I by (rule the_inv_into_f_f)
 
 
-subsection \<open>Cantor's Paradox\<close>
-
-theorem Cantors_paradox: "\<nexists>f. f ` A = Pow A"
-proof
-  assume "\<exists>f. f ` A = Pow A"
-  then obtain f where f: "f ` A = Pow A" ..
-  let ?X = "{a \<in> A. a \<notin> f a}"
-  have "?X \<in> Pow A" by blast
-  then have "?X \<in> f ` A" by (simp only: f)
-  then obtain x where "x \<in> A" and "f x = ?X" by blast
-  then show False by blast
-qed
-
-
 subsection \<open>Monotonicity\<close>
 
 definition monotone_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"

--- a/src/HOL/Number_Theory/Gauss.thy	Tue Oct 11 11:48:04 2022 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Tue Oct 11 18:52:01 2022 +0200
@@ -163,12 +163,6 @@
     by (auto simp add: B_def inj_on_def A_def) metis
 qed
 
-lemma inj_on_pminusx_E: "inj_on (\<lambda>x. p - x) E"
-  apply (auto simp add: E_def C_def B_def A_def)
-  apply (rule inj_on_inverseI [where g = "(-) (int p)"])
-  apply auto
-  done
-
 lemma nonzero_mod_p: "0 < x \<Longrightarrow> x < int p \<Longrightarrow> [x \<noteq> 0](mod p)"
   for x :: int
   by (simp add: cong_def)
@@ -241,7 +235,7 @@
   by (simp add: B_card_eq_A A_card_eq)
 
 lemma F_card_eq_E: "card F = card E"
-  using finite_E by (simp add: F_def inj_on_pminusx_E card_image)
+  using finite_E by (simp add: F_def card_image)
 
 lemma C_card_eq_B: "card C = card B"
 proof -
@@ -312,11 +306,7 @@
 lemma prod_F_zcong: "[prod id F = ((-1) ^ (card E)) * prod id E] (mod p)"
 proof -
   have FE: "prod id F = prod ((-) p) E"
-    apply (auto simp add: F_def)
-    apply (insert finite_E inj_on_pminusx_E)
-    apply (drule prod.reindex)
-    apply auto
-    done
+    using finite_E prod.reindex[OF inj_on_diff_left] by (auto simp add: F_def)
   then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
     by (metis cong_def minus_mod_self1 mod_mod_trivial)
   then have "[prod ((\<lambda>x. x mod p) \<circ> ((-) p)) E = prod (uminus) E](mod p)"
@@ -356,7 +346,7 @@
     by simp
   then have "[prod id A = ((-1)^(card E) * a^(card A) * prod id A)](mod p)"
     by (rule cong_trans)
-      (simp add: cong_scalar_left cong_scalar_right finite_A prod_constant ac_simps)
+      (simp add: cong_scalar_left cong_scalar_right finite_A ac_simps)
   then have a: "[prod id A * (-1)^(card E) =
       ((-1)^(card E) * a^(card A) * prod id A * (-1)^(card E))](mod p)"
     by (rule cong_scalar_right)

--- a/src/HOL/Set.thy	Tue Oct 11 11:48:04 2022 +0200
+++ b/src/HOL/Set.thy	Tue Oct 11 18:52:01 2022 +0200
@@ -952,6 +952,16 @@
 lemma image_add_0 [simp]: "(+) (0::'a::comm_monoid_add) ` S = S"
   by auto
 
+theorem Cantors_paradox: "\<nexists>f. f ` A = Pow A"
+proof
+  assume "\<exists>f. f ` A = Pow A"
+  then obtain f where f: "f ` A = Pow A" ..
+  let ?X = "{a \<in> A. a \<notin> f a}"
+  have "?X \<in> Pow A" by blast
+  then have "?X \<in> f ` A" by (simp only: f)
+  then obtain x where "x \<in> A" and "f x = ?X" by blast
+  then show False by blast
+qed
 
 text \<open>\<^medskip> Range of a function -- just an abbreviation for image!\<close>