author haftmann Mon, 09 Jan 2017 18:53:06 +0100 changeset 64848 c50db2128048 parent 64847 54f5afc9c413 child 64849 766db3539859
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
 src/HOL/Code_Numeral.thy file | annotate | diff | comparison | revisions src/HOL/Divides.thy file | annotate | diff | comparison | revisions src/HOL/Library/Polynomial.thy file | annotate | diff | comparison | revisions src/HOL/Library/Polynomial_Factorial.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Euclidean_Algorithm.thy file | annotate | diff | comparison | revisions src/HOL/Rings.thy file | annotate | diff | comparison | revisions
```--- 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)
```