--- a/src/HOL/Fields.thy Sun Dec 23 15:40:28 2018 +0100
+++ b/src/HOL/Fields.thy Sun Dec 23 20:51:23 2018 +0000
@@ -13,6 +13,32 @@
imports Nat
begin
+context idom
+begin
+
+lemma inj_mult_left [simp]: \<open>inj ((*) a) \<longleftrightarrow> a \<noteq> 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+ assume ?P
+ show ?Q
+ proof
+ assume \<open>a = 0\<close>
+ with \<open>?P\<close> have "inj ((*) 0)"
+ by simp
+ moreover have "0 * 0 = 0 * 1"
+ by simp
+ ultimately have "0 = 1"
+ by (rule injD)
+ then show False
+ by simp
+ qed
+next
+ assume ?Q then show ?P
+ by (auto intro: injI)
+qed
+
+end
+
+
subsection \<open>Division rings\<close>
text \<open>
@@ -513,6 +539,21 @@
by simp
qed simp
+lemma inj_divide_right [simp]:
+ "inj (\<lambda>b. b / a) \<longleftrightarrow> a \<noteq> 0"
+proof -
+ have "(\<lambda>b. b / a) = (*) (inverse a)"
+ by (simp add: field_simps fun_eq_iff)
+ then have "inj (\<lambda>y. y / a) \<longleftrightarrow> inj ((*) (inverse a))"
+ by simp
+ also have "\<dots> \<longleftrightarrow> inverse a \<noteq> 0"
+ by simp
+ also have "\<dots> \<longleftrightarrow> a \<noteq> 0"
+ by simp
+ finally show ?thesis
+ by simp
+qed
+
end
class field_char_0 = field + ring_char_0
--- a/src/HOL/Fun.thy Sun Dec 23 15:40:28 2018 +0100
+++ b/src/HOL/Fun.thy Sun Dec 23 20:51:23 2018 +0000
@@ -594,6 +594,30 @@
using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast
qed
+text \<open>Important examples\<close>
+
+context cancel_semigroup_add
+begin
+
+lemma inj_add_left [simp]: \<open>inj ((+) a)\<close>
+ by (rule injI) simp
+
+end
+
+context ab_group_add
+begin
+
+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
+
+end
+
subsection \<open>Function Updating\<close>
--- a/src/HOL/Parity.thy Sun Dec 23 15:40:28 2018 +0100
+++ b/src/HOL/Parity.thy Sun Dec 23 20:51:23 2018 +0000
@@ -549,6 +549,10 @@
"n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
using not_mod_2_eq_1_eq_0 [of n] by simp
+lemma odd_card_imp_not_empty:
+ \<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close>
+ using that by auto
+
subsection \<open>Parity and powers\<close>
--- a/src/HOL/Real.thy Sun Dec 23 15:40:28 2018 +0100
+++ b/src/HOL/Real.thy Sun Dec 23 20:51:23 2018 +0000
@@ -28,14 +28,6 @@
fixes n::nat shows "\<lbrakk>n \<le> m; n\<noteq>0\<rbrakk> \<Longrightarrow> 1 / of_nat m \<le> (1::'a::linordered_field) / of_nat n"
by (simp add: frac_le)
-lemma inj_add_left [simp]: "inj ((+) x)"
- for x :: "'a::cancel_semigroup_add"
- by (meson add_left_imp_eq injI)
-
-lemma inj_mult_left [simp]: "inj ((*) x) \<longleftrightarrow> x \<noteq> 0"
- for x :: "'a::idom"
- by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
-
lemma add_diff_add: "(a + c) - (b + d) = (a - b) + (c - d)"
for a b c d :: "'a::ab_group_add"
by simp
--- a/src/HOL/Set_Interval.thy Sun Dec 23 15:40:28 2018 +0100
+++ b/src/HOL/Set_Interval.thy Sun Dec 23 20:51:23 2018 +0000
@@ -1015,13 +1015,28 @@
"(\<lambda>t. t-d)`{a..b} = {a-d..b-d}" for d::"'a::linordered_idom"
by (metis (no_types, lifting) diff_conv_add_uminus image_add_atLeastAtMost' image_cong)
-context linordered_field begin
+context linordered_field
+begin
lemma image_mult_atLeastAtMost [simp]:
"((*) d ` {a..b}) = {d*a..d*b}" if "d>0"
using that
by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
+lemma image_divide_atLeastAtMost [simp]:
+ "((\<lambda>c. c / d) ` {a..b}) = {a/d..b/d}" if "d>0"
+proof -
+ from that have "inverse d > 0"
+ by simp
+ with image_mult_atLeastAtMost [of "inverse d" a b]
+ have "(*) (inverse d) ` {a..b} = {inverse d * a..inverse d * b}"
+ by blast
+ moreover have "(*) (inverse d) = (\<lambda>c. c / d)"
+ by (simp add: fun_eq_iff field_simps)
+ ultimately show ?thesis
+ by simp
+qed
+
lemma image_mult_atLeastAtMost_if:
"(*) c ` {x .. y} =
(if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"