canonical multiplicative euclidean size

--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Mon Oct 09 19:10:51 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Mon Oct 09 19:10:52 2017 +0200
@@ -759,8 +759,8 @@
     with that show ?thesis
       by (cases "r = 0") (simp_all add: euclidean_size_poly_def div_poly_less ac_simps)
   qed
-qed (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq intro!: degree_mod_less' degree_mult_right_le
-    split: if_splits)
+qed (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq power_add
+    intro!: degree_mod_less' split: if_splits)
 
 end
 

--- a/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:51 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:52 2017 +0200
@@ -20,6 +20,27 @@
     "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)
 
@@ -108,7 +129,7 @@
 
 class euclidean_ring = idom_modulo + euclidean_semiring
 
-  
+
 subsection \<open>Euclidean (semi)rings with cancel rules\<close>
 
 class euclidean_semiring_cancel = euclidean_semiring +
@@ -506,10 +527,7 @@
 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:
@@ -625,7 +643,7 @@
     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)

--- a/src/HOL/Parity.thy	Mon Oct 09 19:10:51 2017 +0200
+++ b/src/HOL/Parity.thy	Mon Oct 09 19:10:52 2017 +0200
@@ -135,15 +135,7 @@
     show "euclidean_size (a mod 2) \<le> 1"
       using mod_size_less [of 2 a] by simp
     show "1 \<le> euclidean_size (a mod 2)"
-    proof (rule ccontr)
-      assume "\<not> 1 \<le> euclidean_size (a mod 2)"
-      then have "euclidean_size (a mod 2) = 0"
-        by simp
-      then have "division_segment (a mod 2) * of_nat (euclidean_size (a mod 2)) = division_segment (a mod 2) * of_nat 0"
-        by simp
-      with \<open>odd a\<close> show False
-        by (simp add: dvd_eq_mod_eq_0)
-    qed
+      using \<open>odd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0)
   qed 
   from \<open>odd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)"
     by simp