src/HOL/Euclidean_Division.thy

   assumes mod_size_less: 
     "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
   assumes size_mult_mono:
     "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
 begin
+
+lemma euclidean_size_eq_0_iff [simp]:
+  "euclidean_size b = 0 \<longleftrightarrow> b = 0"
+proof
+  assume "b = 0"
+  then show "euclidean_size b = 0"
+    by simp
+next
+  assume "euclidean_size b = 0"
+  show "b = 0"
+  proof (rule ccontr)
+    assume "b \<noteq> 0"
+    with mod_size_less have "euclidean_size (b mod b) < euclidean_size b" .
+    with \<open>euclidean_size b = 0\<close> show False
+      by simp
+  qed
+qed
+
+lemma euclidean_size_greater_0_iff [simp]:
+  "euclidean_size b > 0 \<longleftrightarrow> b \<noteq> 0"
+  using euclidean_size_eq_0_iff [symmetric, of b] by safe simp
 
 lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
   by (subst mult.commute) (rule size_mult_mono)
 
 lemma dvd_euclidean_size_eq_imp_dvd:

 
 end
 
 class euclidean_ring = idom_modulo + euclidean_semiring
 
-  
+
 subsection \<open>Euclidean (semi)rings with cancel rules\<close>
 
 class euclidean_semiring_cancel = euclidean_semiring +
   assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
   and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"

 
   
 subsection \<open>Uniquely determined division\<close>
   
 class unique_euclidean_semiring = euclidean_semiring + 
-  assumes size_mono_mult:
-    "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
-      \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
-    -- \<open>FIXME justify\<close>
+  assumes euclidean_size_mult: "euclidean_size (a * b) = euclidean_size a * euclidean_size b"
   fixes division_segment :: "'a \<Rightarrow> 'a"
   assumes is_unit_division_segment [simp]: "is_unit (division_segment a)"
     and division_segment_mult:
     "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> division_segment (a * b) = division_segment a * division_segment b"
     and division_segment_mod:

     from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
       by simp
     from remainder \<open>c \<noteq> 0\<close>
     have "division_segment (r * c) = division_segment (b * c)"
       and "euclidean_size (r * c) < euclidean_size (b * c)"
-      by (simp_all add: division_segment_mult division_segment_mod size_mono_mult)
+      by (simp_all add: division_segment_mult division_segment_mod euclidean_size_mult)
     with remainder show ?thesis
       by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
         (use \<open>b * c \<noteq> 0\<close> in simp)
   qed
 qed