# HG changeset patch # User paulson # Date 1617017173 -3600 # Node ID c526eb2c7ca0cb3488384c4c2cc7dcdba2ac1def # Parent 5d750df8e89402c47faa3a268bc7864e990f0446 removal of needless hypothesis in hd_rev and last_rev diff -r 5d750df8e894 -r c526eb2c7ca0 src/HOL/Computational_Algebra/Polynomial.thy --- a/src/HOL/Computational_Algebra/Polynomial.thy Sun Mar 28 12:21:37 2021 +0200 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Mon Mar 29 12:26:13 2021 +0100 @@ -597,7 +597,7 @@ lemma last_coeffs_eq_coeff_degree: "last (coeffs p) = lead_coeff p" if "p \ 0" using that by (simp add: coeffs_def) - + subsection \Addition and subtraction\ @@ -911,7 +911,7 @@ 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 +qed lemma smult_eq_iff: fixes b :: "'a :: field" @@ -1068,7 +1068,7 @@ lemma monom_altdef: "monom c n = smult c ([:0, 1:] ^ n)" - by (induct n) (simp_all add: monom_0 monom_Suc) + by (induct n) (simp_all add: monom_0 monom_Suc) instance poly :: ("{comm_semiring_1,semiring_1_no_zero_divisors}") semiring_1_no_zero_divisors .. instance poly :: (comm_ring) comm_ring .. @@ -1497,7 +1497,7 @@ lemma pos_poly_add: "pos_poly p \ pos_poly q \ pos_poly (p + q)" proof (induction p arbitrary: q) case (pCons a p) - then show ?case + then show ?case by (cases q; force simp add: pos_poly_pCons add_pos_pos) qed auto @@ -1734,7 +1734,7 @@ lemma order_1: "[:-a, 1:] ^ order a p dvd p" proof (cases "p = 0") case False - show ?thesis + show ?thesis proof (cases "order a p") case (Suc n) then show ?thesis @@ -1742,8 +1742,8 @@ qed auto qed auto -lemma order_2: - assumes "p \ 0" +lemma order_2: + assumes "p \ 0" shows "\ [:-a, 1:] ^ Suc (order a p) dvd p" proof - have False if "[:- a, 1:] ^ Suc (degree p) dvd p" @@ -1786,7 +1786,7 @@ unfolding Polynomial.order_def by (metis (mono_tags, lifting) Least_equality assms not_less_eq_eq power_le_dvd) -lemma order_mult: +lemma order_mult: assumes "p * q \ 0" shows "order a (p * q) = order a p + order a q" proof - define i where "i \ order a p" @@ -1828,7 +1828,7 @@ by (metis order_root poly_1 zero_neq_one) lemma order_uminus[simp]: "order x (-p) = order x p" - by (metis neg_equal_0_iff_equal order_smult smult_1_left smult_minus_left) + by (metis neg_equal_0_iff_equal order_smult smult_1_left smult_minus_left) lemma order_power_n_n: "order a ([:-a,1:]^n)=n" proof (induct n) (*might be proved more concisely using nat_less_induct*) @@ -2510,7 +2510,7 @@ for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" proof (cases "degree p") case 0 - then show ?thesis + then show ?thesis by (metis degree_eq_zeroE pderiv.simps) next case (Suc n) @@ -2526,7 +2526,7 @@ proof (cases "degree p") case (Suc n) then show ?thesis - by (metis coeff_pderiv degree_0 diff_Suc_1 le_degree leading_coeff_0_iff mult_eq_0_iff nat.distinct(1) of_nat_eq_0_iff) + by (metis coeff_pderiv degree_0 diff_Suc_1 le_degree leading_coeff_0_iff mult_eq_0_iff nat.distinct(1) of_nat_eq_0_iff) qed auto moreover have "\i>degree p - 1. coeff (pderiv p) i = 0" by (simp add: coeff_eq_0 coeff_pderiv) @@ -2575,7 +2575,7 @@ case (Suc n) then show ?case by (simp add: pderiv_mult smult_add_left algebra_simps) -qed auto +qed auto lemma pderiv_pcompose: "pderiv (pcompose p q) = pcompose (pderiv p) q * pderiv q" by (induction p rule: pCons_induct) @@ -2610,23 +2610,23 @@ lemma poly_DERIV [simp]: "DERIV (\x. poly p x) x :> poly (pderiv p) x" by (induct p) (auto intro!: derivative_eq_intros simp add: pderiv_pCons) -lemma poly_isCont[simp]: +lemma poly_isCont[simp]: fixes x::"'a::real_normed_field" shows "isCont (\x. poly p x) x" by (rule poly_DERIV [THEN DERIV_isCont]) lemma tendsto_poly [tendsto_intros]: "(f \ a) F \ ((\x. poly p (f x)) \ poly p a) F" - for f :: "_ \ 'a::real_normed_field" + for f :: "_ \ 'a::real_normed_field" by (rule isCont_tendsto_compose [OF poly_isCont]) lemma continuous_within_poly: "continuous (at z within s) (poly p)" for z :: "'a::{real_normed_field}" - by (simp add: continuous_within tendsto_poly) - + by (simp add: continuous_within tendsto_poly) + lemma continuous_poly [continuous_intros]: "continuous F f \ continuous F (\x. poly p (f x))" for f :: "_ \ 'a::real_normed_field" unfolding continuous_def by (rule tendsto_poly) - + lemma continuous_on_poly [continuous_intros]: fixes p :: "'a :: {real_normed_field} poly" assumes "continuous_on A f" @@ -3082,7 +3082,7 @@ qed (use assms in \auto simp: coeff_reflect_poly\) lemma algebraic_int_root: - assumes "algebraic_int y" + assumes "algebraic_int y" and "poly p x = y" and "\i. coeff p i \ \" and "lead_coeff p = 1" and "degree p > 0" shows "algebraic_int x" proof - @@ -3735,14 +3735,14 @@ then show "is_unit (unit_factor p)" by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff unit_factor_is_unit) next - fix a b :: "'a poly" assume "is_unit a" + fix a b :: "'a poly" assume "is_unit a" thus "unit_factor (a * b) = a * unit_factor b" by (auto simp: unit_factor_poly_def lead_coeff_mult unit_factor_mult elim!: is_unit_polyE) qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult) end -instance poly :: ("{semidom_divide_unit_factor,idom_divide,normalization_semidom_multiplicative}") +instance poly :: ("{semidom_divide_unit_factor,idom_divide,normalization_semidom_multiplicative}") normalization_semidom_multiplicative by intro_classes (auto simp: unit_factor_poly_def lead_coeff_mult unit_factor_mult) @@ -3849,7 +3849,7 @@ proof (induction x) case 0 then show ?case - using eucl_rel_poly_0 by blast + using eucl_rel_poly_0 by blast next case (pCons a x) then show ?case @@ -4337,9 +4337,9 @@ (rev (coeffs f)) (rev (coeffs g)) (1 + length (coeffs f) - length (coeffs g)) = (q, r)" - using qr hd_rev [OF \coeffs g \ []\] by simp + by (metis hd_rev qr rev.simps(1) rev_swap) ultimately show ?thesis - by (auto simp: degree_eq_length_coeffs pseudo_divmod_def pseudo_divmod_list_def Let_def) + by (simp add: degree_eq_length_coeffs pseudo_divmod_def pseudo_divmod_list_def) next case True then show ?thesis @@ -4872,7 +4872,7 @@ by simp_all then show ?thesis .. qed - + lemma content_dvd_contentI [intro]: "p dvd q \ content p dvd content q" using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast @@ -4984,7 +4984,7 @@ also have "primitive_part \ = smult (unit_factor a) (primitive_part p)" by (subst primitive_part_mult) simp_all finally show ?thesis . -qed +qed lemma primitive_part_dvd_primitive_partI [intro]: fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide, @@ -4992,13 +4992,13 @@ shows "p dvd q \ primitive_part p dvd primitive_part q" by (auto elim!: dvdE simp: primitive_part_mult) -lemma content_prod_mset: +lemma content_prod_mset: fixes A :: "'a :: {factorial_semiring, semiring_Gcd, normalization_semidom_multiplicative} poly multiset" shows "content (prod_mset A) = prod_mset (image_mset content A)" by (induction A) (simp_all add: content_mult mult_ac) -lemma content_prod_eq_1_iff: +lemma content_prod_eq_1_iff: fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, normalization_semidom_multiplicative} poly" shows "content (p * q) = 1 \ content p = 1 \ content q = 1" proof safe @@ -5009,7 +5009,7 @@ hence "content p dvd 1" by (rule dvdI) hence "content p = 1" by simp } note B = this - from A B[of p q] B [of q p] show "content p = 1" "content q = 1" + from A B[of p q] B [of q p] show "content p = 1" "content q = 1" by (simp_all add: content_mult mult_ac) qed (auto simp: content_mult) diff -r 5d750df8e894 -r c526eb2c7ca0 src/HOL/List.thy --- a/src/HOL/List.thy Sun Mar 28 12:21:37 2021 +0200 +++ b/src/HOL/List.thy Mon Mar 29 12:26:13 2021 +0100 @@ -1954,6 +1954,9 @@ subsubsection \\<^const>\last\ and \<^const>\butlast\\ +lemma hd_Nil_eq_last: "hd Nil = last Nil" + unfolding hd_def last_def by simp + lemma last_snoc [simp]: "last (xs @ [x]) = x" by (induct xs) auto @@ -1981,11 +1984,11 @@ lemma butlast_tl: "butlast (tl xs) = tl (butlast xs)" by (induct xs) simp_all -lemma hd_rev: "xs \ [] \ hd(rev xs) = last xs" - by(rule rev_exhaust[of xs]) simp_all - -lemma last_rev: "xs \ [] \ last(rev xs) = hd xs" - by(cases xs) simp_all +lemma hd_rev: "hd(rev xs) = last xs" + by (metis hd_Cons_tl hd_Nil_eq_last last_snoc rev_eq_Cons_iff rev_is_Nil_conv) + +lemma last_rev: "last(rev xs) = hd xs" + by (metis hd_rev rev_swap) lemma last_in_set[simp]: "as \ [] \ last as \ set as" by (induct as) auto