# HG changeset patch
# User haftmann
# Date 1474869414 -7200
# Node ID 559f0882d6a6cb4c0abd82d082045397edfe1176
# Parent  d05da6b707dd16ef22ae7568b57802f817db3b2c
more lemmas

diff -r d05da6b707dd -r 559f0882d6a6 src/HOL/Divides.thy
--- 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>
 
diff -r d05da6b707dd -r 559f0882d6a6 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- 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"
diff -r d05da6b707dd -r 559f0882d6a6 src/HOL/Rings.thy
--- 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