# HG changeset patch # User nipkow # Date 1665507121 -7200 # Node ID 5ede2fce5b01b764cab52b57431cdba684e68317 # Parent 2f10e7a2ff01e9ba4037168be8f6e0608c08a7fb# Parent 7aa2eb860db4a44c8361ca37bc4d21451a9cbb83 merged diff -r 2f10e7a2ff01 -r 5ede2fce5b01 src/HOL/Fun.thy --- 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 \ 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 @@ -705,10 +702,6 @@ "inj_on ((+) a) A" by (rule inj_onI) simp -lemma inj_add_left: - \inj ((+) a)\ - by simp - lemma inj_on_add' [simp]: "inj_on (\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 \ 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 \ 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)" @@ -742,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) @@ -927,20 +950,6 @@ using that UNIV_I by (rule the_inv_into_f_f) -subsection \Cantor's Paradox\ - -theorem Cantors_paradox: "\f. f ` A = Pow A" -proof - assume "\f. f ` A = Pow A" - then obtain f where f: "f ` A = Pow A" .. - let ?X = "{a \ A. a \ f a}" - have "?X \ Pow A" by blast - then have "?X \ f ` A" by (simp only: f) - then obtain x where "x \ A" and "f x = ?X" by blast - then show False by blast -qed - - subsection \Monotonicity\ definition monotone_on :: "'a set \ ('a \ 'a \ bool) \ ('b \ 'b \ bool) \ ('a \ 'b) \ bool" diff -r 2f10e7a2ff01 -r 5ede2fce5b01 src/HOL/Number_Theory/Gauss.thy --- 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 (\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 \ x < int p \ [x \ 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 "\x \ E. [(p-x) mod p = - x](mod p)" by (metis cong_def minus_mod_self1 mod_mod_trivial) then have "[prod ((\x. x mod p) \ ((-) 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) diff -r 2f10e7a2ff01 -r 5ede2fce5b01 src/HOL/Set.thy --- 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: "\f. f ` A = Pow A" +proof + assume "\f. f ` A = Pow A" + then obtain f where f: "f ` A = Pow A" .. + let ?X = "{a \ A. a \ f a}" + have "?X \ Pow A" by blast + then have "?X \ f ` A" by (simp only: f) + then obtain x where "x \ A" and "f x = ?X" by blast + then show False by blast +qed text \\<^medskip> Range of a function -- just an abbreviation for image!\