# 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 \ f -` {a} \ A \ {THE x. x \ A \ 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: "\a \ A. f' (f a) = a" and right: "\a' \ A'. f (f' a') = a'" @@ -696,7 +693,7 @@ qed -subsubsection \Important examples\ +subsubsection \Inj/surj/bij of Algebraic Operations\ context cancel_semigroup_add begin @@ -718,6 +715,13 @@ context group_add begin +lemma diff_left_imp_eq: "a - b = a - c \ 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 \ range ((+) a)" by blast qed -lemma inj_diff_right [simp]: - \inj (\b. b - a)\ -by (auto intro: injI simp add: algebra_simps) +lemma surj_plus_right [simp]: + "surj (\b. b+a)" +proof (standard, simp, standard, simp) + fix b show "b \ range (\b. b+a)" + using diff_add_cancel[of b a, symmetric] by blast +qed + +lemma inj_on_diff_left [simp]: + \inj_on ((-) a) A\ +by (auto intro: inj_onI dest!: diff_left_imp_eq) + +lemma inj_on_diff_right [simp]: + \inj_on (\b. b - a) A\ +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 \ range ((-) a)" by blast +qed lemma surj_diff_right [simp]: "surj (\x. x - a)" @@ -738,6 +761,10 @@ thus "x \ range (\x. x - a)" by fast qed +lemma shows bij_plus: "bij ((+) a)" and bij_plus_right: "bij (\x. x + a)" + and bij_diff: "bij ((-) a)" and bij_diff_right: "bij (\x. x - a)" +by(simp_all add: bij_def) + lemma translation_subtract_Compl: "(\x. x - a) ` (- t) = - ((\x. x - a) ` t)" by(rule bij_image_Compl_eq)