--- a/src/HOL/Divides.thy Mon Sep 26 07:56:53 2016 +0200
+++ b/src/HOL/Divides.thy Mon Sep 26 07:56:54 2016 +0200
@@ -2310,6 +2310,16 @@
by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
qed
+lemma zmod_trival_iff:
+ fixes i k :: int
+ shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
+proof -
+ have "i mod k = i \<longleftrightarrow> i div k = 0"
+ by safe (insert mod_div_equality [of i k], auto)
+ with zdiv_eq_0_iff
+ show ?thesis
+ by simp
+qed
subsubsection \<open>Quotients of Signs\<close>
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Mon Sep 26 07:56:53 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Mon Sep 26 07:56:54 2016 +0200
@@ -26,6 +26,22 @@
"b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
begin
+lemma euclidean_size_normalize [simp]:
+ "euclidean_size (normalize a) = euclidean_size a"
+proof (cases "a = 0")
+ case True
+ then show ?thesis
+ by simp
+next
+ case [simp]: False
+ have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
+ by (rule size_mult_mono) simp
+ moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
+ by (rule size_mult_mono) simp
+ ultimately show ?thesis
+ by simp
+qed
+
lemma euclidean_division:
fixes a :: 'a and b :: 'a
assumes "b \<noteq> 0"
--- a/src/HOL/Rings.thy Mon Sep 26 07:56:53 2016 +0200
+++ b/src/HOL/Rings.thy Mon Sep 26 07:56:54 2016 +0200
@@ -1088,6 +1088,20 @@
lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
by (cases "b = 0") simp_all
+lemma inv_unit_factor_eq_0_iff [simp]:
+ "1 div unit_factor a = 0 \<longleftrightarrow> a = 0"
+ (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ assume ?lhs
+ then have "a * (1 div unit_factor a) = a * 0"
+ by simp
+ then show ?rhs
+ by simp
+next
+ assume ?rhs
+ then show ?lhs by simp
+qed
+
lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
proof (cases "a = 0 \<or> b = 0")
case True