--- a/src/HOL/Fun.thy Thu Oct 06 14:16:39 2022 +0000
+++ b/src/HOL/Fun.thy Sat Oct 08 18:35:53 2022 +0200
@@ -208,7 +208,7 @@
lemma bij_id[simp]: "bij id"
by (simp add: bij_betw_def)
-lemma bij_uminus: "bij (uminus :: 'a \<Rightarrow> 'a::ab_group_add)"
+lemma bij_uminus: "bij (uminus :: 'a \<Rightarrow> 'a::group_add)"
unfolding bij_betw_def inj_on_def
by (force intro: minus_minus [symmetric])
@@ -591,7 +591,7 @@
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 ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
+lemma (in group_add) inj_uminus[simp, intro]: "inj_on uminus A"
by (auto intro!: inj_onI)
lemma bij_betw_byWitness:
@@ -719,26 +719,55 @@
end
-context ab_group_add
+context group_add
begin
lemma surj_plus [simp]:
"surj ((+) a)"
- by (auto intro!: range_eqI [of b "(+) a" "b - a" for b]) (simp add: algebra_simps)
+proof (standard, simp, standard, simp)
+ fix x
+ have "x = a + (-a + x)" by (simp add: add.assoc)
+ thus "x \<in> range ((+) a)" by blast
+qed
lemma inj_diff_right [simp]:
\<open>inj (\<lambda>b. b - a)\<close>
-proof -
- have \<open>inj ((+) (- a))\<close>
- by (fact inj_add_left)
- also have \<open>(+) (- a) = (\<lambda>b. b - a)\<close>
- by (simp add: fun_eq_iff)
- finally show ?thesis .
-qed
+by (auto intro: injI simp add: algebra_simps)
lemma surj_diff_right [simp]:
"surj (\<lambda>x. x - a)"
- using surj_plus [of "- a"] by (simp cong: image_cong_simp)
+proof (standard, simp, standard, simp)
+ fix x
+ have "x = x + a - a" by simp
+ thus "x \<in> range (\<lambda>x. x - a)" by fast
+qed
+
+lemma translation_subtract_Compl:
+ "(\<lambda>x. x - a) ` (- t) = - ((\<lambda>x. x - a) ` t)"
+by(rule bij_image_Compl_eq)
+ (auto simp add: bij_def surj_def inj_def diff_eq_eq intro!: add_diff_cancel[symmetric])
+
+lemma translation_diff:
+ "(+) a ` (s - t) = ((+) a ` s) - ((+) a ` t)"
+ by auto
+
+lemma translation_subtract_diff:
+ "(\<lambda>x. x - a) ` (s - t) = ((\<lambda>x. x - a) ` s) - ((\<lambda>x. x - a) ` t)"
+by(rule image_set_diff)(simp add: inj_on_def diff_eq_eq)
+
+lemma translation_Int:
+ "(+) a ` (s \<inter> t) = ((+) a ` s) \<inter> ((+) a ` t)"
+ by auto
+
+lemma translation_subtract_Int:
+ "(\<lambda>x. x - a) ` (s \<inter> t) = ((\<lambda>x. x - a) ` s) \<inter> ((\<lambda>x. x - a) ` t)"
+by(rule image_Int)(simp add: inj_on_def diff_eq_eq)
+
+end
+
+(* TODO: prove in group_add *)
+context ab_group_add
+begin
lemma translation_Compl:
"(+) a ` (- t) = - ((+) a ` t)"
@@ -748,26 +777,6 @@
by (auto simp: image_iff algebra_simps intro!: bexI [of _ "b - a"])
qed
-lemma translation_subtract_Compl:
- "(\<lambda>x. x - a) ` (- t) = - ((\<lambda>x. x - a) ` t)"
- using translation_Compl [of "- a" t] by (simp cong: image_cong_simp)
-
-lemma translation_diff:
- "(+) a ` (s - t) = ((+) a ` s) - ((+) a ` t)"
- by auto
-
-lemma translation_subtract_diff:
- "(\<lambda>x. x - a) ` (s - t) = ((\<lambda>x. x - a) ` s) - ((\<lambda>x. x - a) ` t)"
- using translation_diff [of "- a"] by (simp cong: image_cong_simp)
-
-lemma translation_Int:
- "(+) a ` (s \<inter> t) = ((+) a ` s) \<inter> ((+) a ` t)"
- by auto
-
-lemma translation_subtract_Int:
- "(\<lambda>x. x - a) ` (s \<inter> t) = ((\<lambda>x. x - a) ` s) \<inter> ((\<lambda>x. x - a) ` t)"
- using translation_Int [of " -a"] by (simp cong: image_cong_simp)
-
end