# HG changeset patch # User haftmann # Date 1491392861 -7200 # Node ID 83586780598b0f2281c30e8bd701bd0cf55f1263 # Parent 6f9c6ae27984a787f4e64d7358272d625128d551 more concise criterion diff -r 6f9c6ae27984 -r 83586780598b src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Wed Apr 05 13:47:40 2017 +0200 +++ b/src/HOL/Library/Polynomial.thy Wed Apr 05 13:47:41 2017 +0200 @@ -103,7 +103,8 @@ begin lift_definition zero_poly :: "'a poly" - is "\_. 0" by (rule MOST_I) simp + is "\_. 0" + by (rule MOST_I) simp instance .. @@ -377,11 +378,13 @@ with Cons show ?case by auto qed -lemma last_coeffs_not_0: "p \ 0 \ last (coeffs p) \ 0" - by (induct p) (auto simp add: cCons_def) - -lemma strip_while_coeffs [simp]: "strip_while (HOL.eq 0) (coeffs p) = coeffs p" - by (cases "p = 0") (auto dest: last_coeffs_not_0 intro: strip_while_not_last) +lemma no_trailing_coeffs [simp]: + "no_trailing (HOL.eq 0) (coeffs p)" + by (induct p) auto + +lemma strip_while_coeffs [simp]: + "strip_while (HOL.eq 0) (coeffs p) = coeffs p" + by simp lemma coeffs_eq_iff: "p = q \ coeffs p = coeffs q" (is "?P \ ?Q") @@ -402,11 +405,12 @@ lemma coeffs_eqI: assumes coeff: "\n. coeff p n = nth_default 0 xs n" - assumes zero: "xs \ [] \ last xs \ 0" + assumes zero: "no_trailing (HOL.eq 0) xs" shows "coeffs p = xs" proof - - from coeff have "p = Poly xs" by (simp add: poly_eq_iff) - with zero show ?thesis by simp (cases xs; simp) + from coeff have "p = Poly xs" + by (simp add: poly_eq_iff) + with zero show ?thesis by simp qed lemma degree_eq_length_coeffs [code]: "degree p = length (coeffs p) - 1" @@ -737,28 +741,26 @@ have *: "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n" for xs ys :: "'a list" and n proof (induct xs ys arbitrary: n rule: plus_coeffs.induct) - case 3 - then show ?case by (cases n) (auto simp: cCons_def) - qed simp_all - have **: "last (plus_coeffs xs ys) \ 0" - if "xs \ [] \ last xs \ 0" and "ys \ [] \ last ys \ 0" and "plus_coeffs xs ys \ []" - for xs ys :: "'a list" - using that - proof (induct xs ys rule: plus_coeffs.induct) - case 3 - then show ?case by (auto simp add: cCons_def) metis + case (3 x xs y ys n) + then show ?case + by (cases n) (auto simp add: cCons_def) qed simp_all + have **: "no_trailing (HOL.eq 0) (plus_coeffs xs ys)" + if "no_trailing (HOL.eq 0) xs" and "no_trailing (HOL.eq 0) ys" + for xs ys :: "'a list" + using that by (induct xs ys rule: plus_coeffs.induct) (simp_all add: cCons_def) show ?thesis - apply (rule coeffs_eqI) - apply (simp add: * nth_default_coeffs_eq) - apply (rule **) - apply (auto dest: last_coeffs_not_0) - done + by (rule coeffs_eqI) (auto simp add: * nth_default_coeffs_eq intro: **) qed -lemma coeffs_uminus [code abstract]: "coeffs (- p) = map (\a. - a) (coeffs p)" - by (rule coeffs_eqI) - (simp_all add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq) +lemma coeffs_uminus [code abstract]: + "coeffs (- p) = map uminus (coeffs p)" +proof - + have eq_0: "HOL.eq 0 \ uminus = HOL.eq (0::'a)" + by (simp add: fun_eq_iff) + show ?thesis + by (rule coeffs_eqI) (simp_all add: nth_default_map_eq nth_default_coeffs_eq no_trailing_map eq_0) +qed lemma [code]: "p - q = p + - q" for p q :: "'a::ab_group_add poly" @@ -885,9 +887,12 @@ lemma coeffs_smult [code abstract]: "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))" for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" - by (rule coeffs_eqI) - (auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 - nth_default_map_eq nth_default_coeffs_eq) +proof - + have eq_0: "HOL.eq 0 \ times a = HOL.eq (0::'a)" if "a \ 0" + using that by (simp add: fun_eq_iff) + show ?thesis + by (rule coeffs_eqI) (auto simp add: no_trailing_map nth_default_map_eq nth_default_coeffs_eq eq_0) +qed lemma smult_eq_iff: fixes b :: "'a :: field" @@ -1120,16 +1125,15 @@ "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))" by (simp add: map_poly_def) -lemma set_coeffs_map_poly: - "(\x. f x = 0 \ x = 0) \ set (coeffs (map_poly f p)) = f ` set (coeffs p)" - by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0) - lemma coeffs_map_poly': assumes "\x. x \ 0 \ f x \ 0" shows "coeffs (map_poly f p) = map f (coeffs p)" - by (cases "p = 0") - (auto simp: assms coeffs_map_poly last_map last_coeffs_not_0 - intro!: strip_while_not_last split: if_splits) + using assms by (simp add: coeffs_map_poly no_trailing_map strip_while_idem_iff) + (metis comp_def no_leading_def no_trailing_coeffs) + +lemma set_coeffs_map_poly: + "(\x. f x = 0 \ x = 0) \ set (coeffs (map_poly f p)) = f ` set (coeffs p)" + by (simp add: coeffs_map_poly') lemma degree_map_poly: assumes "\x. x \ 0 \ f x \ 0" @@ -2146,7 +2150,8 @@ lemma poly_shift_monom: "poly_shift n (monom c m) = (if m \ n then monom c (m - n) else 0)" by (auto simp add: poly_eq_iff coeff_poly_shift) -lemma coeffs_shift_poly [code abstract]: "coeffs (poly_shift n p) = drop n (coeffs p)" +lemma coeffs_shift_poly [code abstract]: + "coeffs (poly_shift n p) = drop n (coeffs p)" proof (cases "p = 0") case True then show ?thesis by simp @@ -2154,7 +2159,7 @@ case False then show ?thesis by (intro coeffs_eqI) - (simp_all add: coeff_poly_shift nth_default_drop last_coeffs_not_0 nth_default_coeffs_eq) + (simp_all add: coeff_poly_shift nth_default_drop nth_default_coeffs_eq) qed @@ -2192,7 +2197,7 @@ unfolding no_trailing_unfold by auto then show ?thesis by (intro coeffs_eqI) - (simp_all add: coeff_poly_cutoff last_coeffs_not_0 nth_default_take nth_default_coeffs_eq) + (simp_all add: coeff_poly_cutoff nth_default_take nth_default_coeffs_eq) qed @@ -2308,7 +2313,8 @@ for xs :: "_::{comm_semiring_0,semiring_no_zero_divisors} poly list" by (induct xs) (simp_all add: reflect_poly_mult) -lemma reflect_poly_Poly_nz: "xs \ [] \ last xs \ 0 \ reflect_poly (Poly xs) = Poly (rev xs)" +lemma reflect_poly_Poly_nz: + "no_trailing (HOL.eq 0) xs \ reflect_poly (Poly xs) = Poly (rev xs)" by (simp add: reflect_poly_def) lemmas reflect_poly_simps = @@ -4137,39 +4143,36 @@ qed simp qed simp -lemma pseudo_divmod_impl[code]: "pseudo_divmod (f::'a::comm_ring_1 poly) g = - map_prod poly_of_list poly_of_list (pseudo_divmod_list (coeffs f) (coeffs g))" +lemma pseudo_divmod_impl [code]: + "pseudo_divmod f g = map_prod poly_of_list poly_of_list (pseudo_divmod_list (coeffs f) (coeffs g))" + for f g :: "'a::comm_ring_1 poly" proof (cases "g = 0") case False - then have coeffs_g_nonempty:"(coeffs g) \ []" - by simp - then have lastcoeffs: "last (coeffs g) = coeff g (degree g)" - by (simp add: hd_rev last_coeffs_eq_coeff_degree not_0_coeffs_not_Nil) - obtain q r where qr: - "pseudo_divmod_main_list - (last (coeffs g)) (rev []) - (rev (coeffs f)) (rev (coeffs g)) - (1 + length (coeffs f) - length (coeffs g)) = (q, rev (rev r))" + then have "last (coeffs g) \ 0" + and "last (coeffs g) = lead_coeff g" + and "coeffs g \ []" + by (simp_all add: last_coeffs_eq_coeff_degree) + moreover obtain q r where qr: "pseudo_divmod_main_list + (last (coeffs g)) (rev []) + (rev (coeffs f)) (rev (coeffs g)) + (1 + length (coeffs f) - + length (coeffs g)) = (q, rev (rev r))" by force - then have qr': - "pseudo_divmod_main_list - (hd (rev (coeffs g))) [] - (rev (coeffs f)) (rev (coeffs g)) - (1 + length (coeffs f) - length (coeffs g)) = (q, r)" - using hd_rev[OF coeffs_g_nonempty] by auto - from False have cg: "coeffs g = [] \ False" - by auto - from False have last_non0: "last (coeffs g) \ 0" - by (simp add: last_coeffs_not_0) - from False show ?thesis - unfolding pseudo_divmod_def pseudo_divmod_list_def Let_def qr' map_prod_def split cg if_False - pseudo_divmod_main_list_invar[OF last_non0 _ _ qr,unfolded lastcoeffs,simplified,symmetric,OF False] - poly_of_list_def - by (auto simp: degree_eq_length_coeffs) + ultimately have "(Poly q, Poly (rev r)) = pseudo_divmod_main (lead_coeff g) 0 f g + (length (coeffs f) - Suc 0) (Suc (length (coeffs f)) - length (coeffs g))" + by (subst pseudo_divmod_main_list_invar [symmetric]) auto + moreover have "pseudo_divmod_main_list + (hd (rev (coeffs g))) [] + (rev (coeffs f)) (rev (coeffs g)) + (1 + length (coeffs f) - + length (coeffs g)) = (q, r)" + using qr hd_rev [OF \coeffs g \ []\] by simp + ultimately show ?thesis + by (auto simp: degree_eq_length_coeffs pseudo_divmod_def pseudo_divmod_list_def Let_def) next case True then show ?thesis - by (auto simp: pseudo_divmod_def pseudo_divmod_list_def) + by (auto simp add: pseudo_divmod_def pseudo_divmod_list_def) qed lemma pseudo_mod_main_list: diff -r 6f9c6ae27984 -r 83586780598b src/HOL/Library/Polynomial_Factorial.thy --- a/src/HOL/Library/Polynomial_Factorial.thy Wed Apr 05 13:47:40 2017 +0200 +++ b/src/HOL/Library/Polynomial_Factorial.thy Wed Apr 05 13:47:41 2017 +0200 @@ -168,8 +168,8 @@ by (auto elim!: dvdE) lemma prod_mset_fract_poly: - "prod_mset (image_mset (\x. fract_poly (f x)) A) = fract_poly (prod_mset (image_mset f A))" - by (induct A) (simp_all add: one_poly_def ac_simps) + "(\x\#A. map_poly to_fract (f x)) = fract_poly (prod_mset (image_mset f A))" + by (induct A) (simp_all add: ac_simps) lemma is_unit_fract_poly_iff: "p dvd 1 \ fract_poly p dvd 1 \ content p = 1"