# HG changeset patch
# User haftmann
# Date 1545598283 0
# Node ID 0cf906072e209bc6aba6b13231092d8f30bb86a4
# Parent  4c1985eba1b780bb7deba232d2e17be41e85a305
more rules

diff -r 4c1985eba1b7 -r 0cf906072e20 src/HOL/Fields.thy
--- 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
diff -r 4c1985eba1b7 -r 0cf906072e20 src/HOL/Fun.thy
--- 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>
 
diff -r 4c1985eba1b7 -r 0cf906072e20 src/HOL/Parity.thy
--- 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>
 
diff -r 4c1985eba1b7 -r 0cf906072e20 src/HOL/Real.thy
--- 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
diff -r 4c1985eba1b7 -r 0cf906072e20 src/HOL/Set_Interval.thy
--- 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 {})"