# HG changeset patch # User haftmann # Date 1483984386 -3600 # Node ID c50db21280482517eeb10a00d5e60051cfd3a7f9 # Parent 54f5afc9c41389d3339a5491790249c33ee165ac slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization diff -r 54f5afc9c413 -r c50db2128048 src/HOL/Code_Numeral.thy --- 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 \ 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 \ integer \ integer" is "modulo :: int \ int \ 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 diff -r 54f5afc9c413 -r c50db2128048 src/HOL/Divides.thy --- 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 \ 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 diff -r 54f5afc9c413 -r c50db2128048 src/HOL/Library/Polynomial.thy --- 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 \ of_int a div of_int b \ (\ :: '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 \of_int b \ (0::'a)\ show ?thesis by simp -qed auto +lemma (in idom_divide) of_int_divide_in_Ints: + "of_int a div of_int b \ \" 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 \Auxiliary: operations for lists (later) representing coefficients\ @@ -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 \ '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 \ 'a poly" - where "normalize_poly p = map_poly (\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 \ 0" + by simp + then have *: "unit_factor (lead_coeff p) \ 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 (\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 \ 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 (\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 \ 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 - diff -r 54f5afc9c413 -r c50db2128048 src/HOL/Library/Polynomial_Factorial.thy --- 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 \ 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 diff -r 54f5afc9c413 -r c50db2128048 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- 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) -- \FIXME rule\ fix x assume "x \ 0" thus "finite {p. p dvd x \ 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 \ _)" @@ -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 \ _) = 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 \ _) = gcd" diff -r 54f5afc9c413 -r c50db2128048 src/HOL/Rings.thy --- 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 \ '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 \ unit_factor a = a" + and unit_factor_is_unit: "a \ 0 \ unit_factor a dvd 1" + and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b" + -- \This fine-grained hierarchy will later on allow lean normalization of polynomials\ + +class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor + fixes normalize :: "'a \ 'a" - and unit_factor :: "'a \ '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 \ normalize a = 1" - and unit_factor_is_unit [iff]: "a \ 0 \ is_unit (unit_factor a)" - and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b" begin text \ @@ -1176,6 +1181,8 @@ think about equality of normalized values rather than associated elements. \ +declare unit_factor_is_unit [iff] + lemma unit_factor_dvd [simp]: "a \ 0 \ 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 \ 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 "\ = 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 \ 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 \ 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 "\ = 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: "\x\ = \y\ \ x = y \ x = -y" by (auto simp add: abs_if split: if_split_asm) +lemma abs_eq_iff': + "\a\ = b \ b \ 0 \ (a = b \ a = - b)" + by (cases "a \ 0") auto + +lemma eq_abs_iff': + "a = \b\ \ a \ 0 \ (b = a \ b = - a)" + using abs_eq_iff' [of b a] by auto + lemma sum_squares_ge_zero: "0 \ x * x + y * y" by (intro add_nonneg_nonneg zero_le_square)