# HG changeset patch # User paulson # Date 1744144364 -3600 # Node ID 7bd2e917f4253f0adea84372401923a119ca7aee # Parent eea85bbd2feb080c784ef96ef3e616227f8c8df8 Another Eberl lemma plus tidying diff -r eea85bbd2feb -r 7bd2e917f425 src/HOL/Computational_Algebra/Nth_Powers.thy --- a/src/HOL/Computational_Algebra/Nth_Powers.thy Tue Apr 08 20:05:54 2025 +0100 +++ b/src/HOL/Computational_Algebra/Nth_Powers.thy Tue Apr 08 21:32:44 2025 +0100 @@ -45,7 +45,7 @@ by (auto simp: is_nth_power_def intro!: exI[of _ 1]) lemma is_nth_power_Suc_0 [simp]: "is_nth_power n (Suc 0)" - by (simp add: One_nat_def [symmetric] del: One_nat_def) + by (metis One_nat_def is_nth_power_1) lemma is_nth_power_conv_multiplicity: fixes x :: "'a :: {factorial_semiring, normalization_semidom_multiplicative}" @@ -58,7 +58,7 @@ fix y p :: 'a assume *: "normalize x = y ^ n" "prime p" with assms and False have [simp]: "y \ 0" by (auto simp: power_0_left) have "multiplicity p x = multiplicity p (y ^ n)" - by (subst *(1) [symmetric]) simp + by (metis "*"(1) multiplicity_normalize_right) with False and * and assms show "n dvd multiplicity p x" by (auto simp: prime_elem_multiplicity_power_distrib) next @@ -88,11 +88,7 @@ lemma is_nth_power_mult: assumes "is_nth_power n a" "is_nth_power n b" shows "is_nth_power n (a * b :: 'a :: comm_monoid_mult)" -proof - - from assms obtain a' b' where "a = a' ^ n" "b = b' ^ n" by (auto elim!: is_nth_powerE) - hence "a * b = (a' * b') ^ n" by (simp add: power_mult_distrib) - thus ?thesis by (rule is_nth_powerI) -qed + by (metis assms is_nth_power_def power_mult_distrib) lemma is_nth_power_mult_coprime_natD: fixes a b :: nat @@ -136,12 +132,7 @@ lemma is_nth_power_nth_power': assumes "n dvd n'" shows "is_nth_power n (m ^ n')" -proof - - from assms have "n' = n' div n * n" by simp - also have "m ^ \ = (m ^ (n' div n)) ^ n" by (simp add: power_mult) - also have "is_nth_power n \" by simp - finally show ?thesis . -qed + by (metis assms dvd_div_mult_self is_nth_power_def power_mult) definition is_nth_power_nat :: "nat \ nat \ bool" where [code_abbrev]: "is_nth_power_nat = is_nth_power" @@ -154,6 +145,36 @@ else (\k\{1..m}. k ^ n = m))" by (auto simp: is_nth_power_nat_def is_nth_power_def power_eq_iff_eq_base self_le_power) +lemma is_nth_power_mult_cancel_left: + fixes a b :: "'a :: semiring_gcd" + assumes "is_nth_power n a" "a \ 0" + shows "is_nth_power n (a * b) \ is_nth_power n b" +proof (cases "n > 0") + case True + show ?thesis + proof + assume "is_nth_power n (a * b)" + then obtain x where x: "a * b = x ^ n" + by (elim is_nth_powerE) + obtain y where y: "a = y ^ n" + using assms by (elim is_nth_powerE) + have "y ^ n dvd x ^ n" + by (simp flip: x y) + hence "y dvd x" + using \n > 0\ by simp + then obtain z where z: "x = y * z" + by (elim dvdE) + with \a \ 0\ show "is_nth_power n b" + by (metis is_nth_powerI mult_left_cancel power_mult_distrib x y) + qed (use assms in \auto intro: is_nth_power_mult\) +qed (use assms in auto) + +lemma is_nth_power_mult_cancel_right: + fixes a b :: "'a :: semiring_gcd" + assumes "is_nth_power n b" "b \ 0" + shows "is_nth_power n (a * b) \ is_nth_power n a" + by (metis assms is_nth_power_mult_cancel_left mult.commute) + (* TODO: Harmonise with Discrete_Functions.floor_sqrt *) @@ -201,11 +222,8 @@ lemma nth_root_nat_less: assumes "k > 0" "x ^ k > n" shows "nth_root_nat k n < x" -proof - - from \k > 0\ have "nth_root_nat k n ^ k \ n" by (rule nth_root_nat_power_le) - also have "n < x ^ k" by fact - finally show ?thesis by (rule power_less_imp_less_base) simp_all -qed + by (meson assms nth_root_nat_power_le order.strict_trans1 power_less_imp_less_base + zero_le) lemma nth_root_nat_unique: assumes "m ^ k \ n" "(m + 1) ^ k > n" @@ -219,11 +237,15 @@ ultimately show ?thesis by (rule antisym) qed (insert assms, auto) -lemma nth_root_nat_0 [simp]: "nth_root_nat k 0 = 0" by (simp add: nth_root_nat_def) +lemma nth_root_nat_0 [simp]: "nth_root_nat k 0 = 0" + by (simp add: nth_root_nat_def) + lemma nth_root_nat_1 [simp]: "k > 0 \ nth_root_nat k 1 = 1" by (rule nth_root_nat_unique) (auto simp del: One_nat_def) + lemma nth_root_nat_Suc_0 [simp]: "k > 0 \ nth_root_nat k (Suc 0) = Suc 0" - using nth_root_nat_1 by (simp del: nth_root_nat_1) + using One_nat_def is_nth_power_nat_def nth_root_nat_1 + by presburger lemma first_root_nat [simp]: "nth_root_nat 1 n = n" by (intro nth_root_nat_unique) auto @@ -265,7 +287,8 @@ proof - note that also have "k < Suc k ^ 1" by simp - also from \m > 0\ have "\ \ Suc k ^ m" by (intro power_increasing) simp_all + also from \m > 0\ have "\ \ Suc k ^ m" + by (intro power_increasing) simp_all finally show ?thesis . qed with 1 show ?case by (auto simp: Let_def) @@ -274,7 +297,7 @@ lemma nth_root_nat_aux_correct: assumes "k ^ m \ n" "m > 0" shows "nth_root_nat_aux m k (k ^ m) n = nth_root_nat m n" - by (rule sym, intro nth_root_nat_unique nth_root_nat_aux_le nth_root_nat_aux_gt assms) + by (metis assms nth_root_nat_aux_gt nth_root_nat_aux_le nth_root_nat_unique) lemma nth_root_nat_naive_code [code]: "nth_root_nat m n = (if m = 0 \ n = 0 then 0 else if m = 1 \ n = 1 then n else @@ -288,12 +311,7 @@ lemma nth_root_nat_nth_power': assumes "k > 0" "k dvd m" shows "nth_root_nat k (n ^ m) = n ^ (m div k)" -proof - - from assms have "m = (m div k) * k" by simp - also have "n ^ \ = (n ^ (m div k)) ^ k" by (simp add: power_mult) - also from assms have "nth_root_nat k \ = n ^ (m div k)" by simp - finally show ?thesis . -qed + by (metis assms dvd_div_mult_self nth_root_nat_nth_power power_mult) lemma nth_root_nat_mono: assumes "m \ n"