slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization

--- a/src/HOL/Code_Numeral.thy	Mon Jan 09 15:54:48 2017 +0000
+++ b/src/HOL/Code_Numeral.thy	Mon Jan 09 18:53:06 2017 +0100
@@ -225,7 +225,7 @@
   "of_nat (nat_of_integer k) = max 0 k"
   by transfer auto
 
-instantiation integer :: "{ring_div, normalization_semidom}"
+instantiation integer :: normalization_semidom
 begin
 
 lift_definition normalize_integer :: "integer \<Rightarrow> integer"
@@ -245,7 +245,16 @@
   .
 
 declare divide_integer.rep_eq [simp]
+  
+instance
+  by (standard; transfer)
+    (auto simp add: mult_sgn_abs sgn_mult abs_eq_iff')
 
+end
+
+instantiation integer :: ring_div
+begin
+  
 lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
   .
@@ -253,7 +262,7 @@
 declare modulo_integer.rep_eq [simp]
 
 instance
-  by standard (transfer, simp add: mult_sgn_abs sgn_mult)+
+  by (standard; transfer) simp_all
 
 end
 

--- a/src/HOL/Divides.thy	Mon Jan 09 15:54:48 2017 +0000
+++ b/src/HOL/Divides.thy	Mon Jan 09 18:53:06 2017 +0100
@@ -1812,7 +1812,7 @@
   assume "l \<noteq> 0"
   then show "k * l div l = k"
     by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
-qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
+qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
 
 end
 

--- a/src/HOL/Library/Polynomial.thy	Mon Jan 09 15:54:48 2017 +0000
+++ b/src/HOL/Library/Polynomial.thy	Mon Jan 09 18:53:06 2017 +0100
@@ -17,14 +17,13 @@
 lemma quotient_of_denom_pos': "snd (quotient_of x) > 0"
   using quotient_of_denom_pos [OF surjective_pairing] .
   
-lemma of_int_divide_in_Ints: 
-  "b dvd a \<Longrightarrow> of_int a div of_int b \<in> (\<int> :: 'a :: idom_divide set)"
-proof (cases "of_int b = (0 :: 'a)")
-  case False
-  assume "b dvd a"
-  then obtain c where "a = b * c" ..
-  with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
-qed auto
+lemma (in idom_divide) of_int_divide_in_Ints: 
+  "of_int a div of_int b \<in> \<int>" if "b dvd a"
+proof -
+  from that obtain c where "a = b * c" ..
+  then show ?thesis
+    by (cases "of_int b = 0") simp_all
+qed
 
   
 subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
@@ -3423,59 +3422,104 @@
       by force
 qed
 
-instantiation poly :: ("{normalization_semidom, idom_divide}") normalization_semidom
+instantiation poly :: ("{semidom_divide_unit_factor, idom_divide}") normalization_semidom
 begin
 
 definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
-  where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
+  where "unit_factor_poly p = [:unit_factor (lead_coeff p):]"
 
 definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
-  where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
+  where "normalize p = p div [:unit_factor (lead_coeff p):]"
 
 instance proof
   fix p :: "'a poly"
   show "unit_factor p * normalize p = p"
-    by (cases "p = 0")
-       (simp_all add: unit_factor_poly_def normalize_poly_def monom_0 
-          smult_conv_map_poly map_poly_map_poly o_def)
+  proof (cases "p = 0")
+    case True
+    then show ?thesis
+      by (simp add: unit_factor_poly_def normalize_poly_def)
+  next
+    case False
+    then have "lead_coeff p \<noteq> 0"
+      by simp
+    then have *: "unit_factor (lead_coeff p) \<noteq> 0"
+      using unit_factor_is_unit [of "lead_coeff p"] by auto
+    then have "unit_factor (lead_coeff p) dvd 1"
+      by (auto intro: unit_factor_is_unit)
+    then have **: "unit_factor (lead_coeff p) dvd c" for c
+      by (rule dvd_trans) simp
+    have ***: "unit_factor (lead_coeff p) * (c div unit_factor (lead_coeff p)) = c" for c
+    proof -
+      from ** obtain b where "c = unit_factor (lead_coeff p) * b" ..
+      then show ?thesis
+        using False * by simp
+    qed
+    have "p div [:unit_factor (lead_coeff p):] =
+      map_poly (\<lambda>c. c div unit_factor (lead_coeff p)) p"
+      by (simp add: const_poly_dvd_iff div_const_poly_conv_map_poly **)
+    then show ?thesis
+      by (simp add: normalize_poly_def unit_factor_poly_def
+        smult_conv_map_poly map_poly_map_poly o_def ***)
+  qed
 next
   fix p :: "'a poly"
   assume "is_unit p"
-  then obtain c where p: "p = [:c:]" "is_unit c"
+  then obtain c where p: "p = [:c:]" "c dvd 1"
     by (auto simp: is_unit_poly_iff)
-  thus "normalize p = 1"
-    by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
+  then show "unit_factor p = p"
+    by (simp add: unit_factor_poly_def monom_0 is_unit_unit_factor)
 next
   fix p :: "'a poly" assume "p \<noteq> 0"
-  thus "is_unit (unit_factor p)"
-    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
+  then show "is_unit (unit_factor p)"
+    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff unit_factor_is_unit)
 qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
 
 end
 
-lemma normalize_poly_eq_div:
-  "normalize p = p div [:unit_factor (lead_coeff p):]"
-proof (cases "p = 0")
-  case False
-  thus ?thesis
-    by (subst div_const_poly_conv_map_poly)
-       (auto simp: normalize_poly_def const_poly_dvd_iff)
-qed (auto simp: normalize_poly_def)
+lemma normalize_poly_eq_map_poly:
+  "normalize p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
+proof -
+  have "[:unit_factor (lead_coeff p):] dvd p"
+    by (metis unit_factor_poly_def unit_factor_self)
+  then show ?thesis
+    by (simp add: normalize_poly_def div_const_poly_conv_map_poly)
+qed
+
+lemma coeff_normalize [simp]:
+  "coeff (normalize p) n = coeff p n div unit_factor (lead_coeff p)"
+  by (simp add: normalize_poly_eq_map_poly coeff_map_poly)
+
+class field_unit_factor = field + unit_factor +
+  assumes unit_factor_field [simp]: "unit_factor = id"
+begin
+
+subclass semidom_divide_unit_factor
+proof
+  fix a
+  assume "a \<noteq> 0"
+  then have "1 = a * inverse a"
+    by simp
+  then have "a dvd 1" ..
+  then show "unit_factor a dvd 1"
+    by simp
+qed simp_all
+
+end
 
 lemma unit_factor_pCons:
-  "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
+  "unit_factor (pCons a p) = (if p = 0 then [:unit_factor a:] else unit_factor p)"
   by (simp add: unit_factor_poly_def)
 
 lemma normalize_monom [simp]:
   "normalize (monom a n) = monom (normalize a) n"
-  by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_def degree_monom_eq)
+  by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_eq_map_poly degree_monom_eq)
 
 lemma unit_factor_monom [simp]:
-  "unit_factor (monom a n) = monom (unit_factor a) 0"
+  "unit_factor (monom a n) = [:unit_factor a:]"
   by (cases "a = 0") (simp_all add: unit_factor_poly_def degree_monom_eq)
 
 lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
-  by (simp add: normalize_poly_def map_poly_pCons)
+  by (simp add: normalize_poly_eq_map_poly map_poly_pCons)
 
 lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
 proof -

--- a/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 15:54:48 2017 +0000
+++ b/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 18:53:06 2017 +0100
@@ -520,8 +520,8 @@
        (simp_all add: unit_factor_field_poly_def normalize_field_poly_def)
 next
   fix p :: "'a poly" assume "is_unit p"
-  thus "normalize_field_poly p = 1"
-    by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps)
+  then show "unit_factor_field_poly p = p"
+    by (elim is_unit_polyE) (auto simp: unit_factor_field_poly_def monom_0 one_poly_def field_simps)
 next
   fix p :: "'a poly" assume "p \<noteq> 0"
   thus "is_unit (unit_factor_field_poly p)"
@@ -566,7 +566,7 @@
 proof -
   have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
   have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 
-             normalize_field_poly unit_factor_field_poly" ..
+             unit_factor_field_poly normalize_field_poly" ..
   from field_poly.in_prime_factors_imp_prime [of p x] assms
     show ?thesis unfolding prime_elem_def dvd_field_poly
       comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast

--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Jan 09 15:54:48 2017 +0000
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Jan 09 18:53:06 2017 +0100
@@ -71,7 +71,7 @@
 
 lemma semiring_gcd:
   "class.semiring_gcd one zero times gcd lcm
-    divide plus minus normalize unit_factor"
+    divide plus minus unit_factor normalize"
 proof
   show "gcd a b dvd a"
     and "gcd a b dvd b" for a b
@@ -97,12 +97,12 @@
 qed
 
 interpretation semiring_gcd one zero times gcd lcm
-  divide plus minus normalize unit_factor
+  divide plus minus unit_factor normalize
   by (fact semiring_gcd)
   
 lemma semiring_Gcd:
   "class.semiring_Gcd one zero times gcd lcm Gcd Lcm
-    divide plus minus normalize unit_factor"
+    divide plus minus unit_factor normalize"
 proof -
   show ?thesis
   proof
@@ -180,13 +180,13 @@
 qed
 
 interpretation semiring_Gcd one zero times gcd lcm Gcd Lcm
-    divide plus minus normalize unit_factor
+    divide plus minus unit_factor normalize
   by (fact semiring_Gcd)
 
 subclass factorial_semiring
 proof -
   show "class.factorial_semiring divide plus minus zero times one
-     normalize unit_factor"
+     unit_factor normalize"
   proof (standard, rule factorial_semiring_altI_aux) -- \<open>FIXME rule\<close>
     fix x assume "x \<noteq> 0"
     thus "finite {p. p dvd x \<and> normalize p = p}"
@@ -406,7 +406,7 @@
   interpret semiring_Gcd 1 0 times
     Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
     Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
-    divide plus minus normalize unit_factor
+    divide plus minus unit_factor normalize
     rewrites "dvd.dvd op * = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
@@ -558,7 +558,7 @@
   interpret semiring_Gcd 1 0 times
     "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
     "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
-    divide plus minus normalize unit_factor
+    divide plus minus unit_factor normalize
     rewrites "dvd.dvd op * = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
@@ -590,7 +590,7 @@
   interpret semiring_Gcd 1 0 times
     "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
     "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
-    divide plus minus normalize unit_factor
+    divide plus minus unit_factor normalize
     rewrites "dvd.dvd op * = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"

--- a/src/HOL/Rings.thy	Mon Jan 09 15:54:48 2017 +0000
+++ b/src/HOL/Rings.thy	Mon Jan 09 18:53:06 2017 +0100
@@ -1156,15 +1156,20 @@
 
 end
 
-class normalization_semidom = algebraic_semidom +
+class unit_factor =
+  fixes unit_factor :: "'a \<Rightarrow> 'a"
+
+class semidom_divide_unit_factor = semidom_divide + unit_factor +
+  assumes unit_factor_0 [simp]: "unit_factor 0 = 0"
+    and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
+    and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
+    and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
+  -- \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
+  
+class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
   fixes normalize :: "'a \<Rightarrow> 'a"
-    and unit_factor :: "'a \<Rightarrow> 'a"
   assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
     and normalize_0 [simp]: "normalize 0 = 0"
-    and unit_factor_0 [simp]: "unit_factor 0 = 0"
-    and is_unit_normalize: "is_unit a  \<Longrightarrow> normalize a = 1"
-    and unit_factor_is_unit [iff]: "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
-    and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
 begin
 
 text \<open>
@@ -1176,6 +1181,8 @@
   think about equality of normalized values rather than associated elements.
 \<close>
 
+declare unit_factor_is_unit [iff]
+  
 lemma unit_factor_dvd [simp]: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
   by (rule unit_imp_dvd) simp
 
@@ -1207,13 +1214,45 @@
   then show ?lhs by simp
 qed
 
-lemma is_unit_unit_factor:
+lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
+proof (cases "a = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  then have "unit_factor a \<noteq> 0"
+    by simp
+  with nonzero_mult_div_cancel_left
+  have "unit_factor a * normalize a div unit_factor a = normalize a"
+    by blast
+  then show ?thesis by simp
+qed
+
+lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
+proof (cases "a = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
+    by simp
+  also have "\<dots> = 1 div unit_factor a"
+    using False by (subst is_unit_div_mult_cancel_right) simp_all
+  finally show ?thesis .
+qed
+
+lemma is_unit_normalize:
   assumes "is_unit a"
-  shows "unit_factor a = a"
+  shows "normalize a = 1"
 proof -
-  from assms have "normalize a = 1" by (rule is_unit_normalize)
-  moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
-  ultimately show ?thesis by simp
+  from assms have "unit_factor a = a"
+    by (rule is_unit_unit_factor)
+  moreover from assms have "a \<noteq> 0"
+    by auto
+  moreover have "normalize a = a div unit_factor a"
+    by simp
+  ultimately show ?thesis
+    by simp
 qed
 
 lemma unit_factor_1 [simp]: "unit_factor 1 = 1"
@@ -1251,32 +1290,6 @@
   then show ?thesis by simp
 qed
 
-lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
-proof (cases "a = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  then have "unit_factor a \<noteq> 0" by simp
-  with nonzero_mult_div_cancel_left
-  have "unit_factor a * normalize a div unit_factor a = normalize a"
-    by blast
-  then show ?thesis by simp
-qed
-
-lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
-proof (cases "a = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
-    by simp
-  also have "\<dots> = 1 div unit_factor a"
-    using False by (subst is_unit_div_mult_cancel_right) simp_all
-  finally show ?thesis .
-qed
-
 lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
   by (cases "b = 0") simp_all
 
@@ -1823,6 +1836,14 @@
 proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
   by (auto simp add: abs_if split: if_split_asm)
 
+lemma abs_eq_iff':
+  "\<bar>a\<bar> = b \<longleftrightarrow> b \<ge> 0 \<and> (a = b \<or> a = - b)"
+  by (cases "a \<ge> 0") auto
+
+lemma eq_abs_iff':
+  "a = \<bar>b\<bar> \<longleftrightarrow> a \<ge> 0 \<and> (b = a \<or> b = - a)"
+  using abs_eq_iff' [of b a] by auto
+
 lemma sum_squares_ge_zero: "0 \<le> x * x + y * y"
   by (intro add_nonneg_nonneg zero_le_square)