# Theory Nth_Powers

theory Nth_Powers
imports Primes
```(*
File:      HOL/Computational_Algebra/Nth_Powers.thy
Author:    Manuel Eberl <eberlm@in.tum.de>

n-th powers in general and n-th roots of natural numbers
*)
section ‹\$n\$-th powers and roots of naturals›
theory Nth_Powers
imports Primes
begin

subsection ‹The set of \$n\$-th powers›

definition is_nth_power :: "nat ⇒ 'a :: monoid_mult ⇒ bool" where
"is_nth_power n x ⟷ (∃y. x = y ^ n)"

lemma is_nth_power_nth_power [simp, intro]: "is_nth_power n (x ^ n)"

lemma is_nth_powerI [intro?]: "x = y ^ n ⟹ is_nth_power n x"
by (auto simp: is_nth_power_def)

lemma is_nth_powerE: "is_nth_power n x ⟹ (⋀y. x = y ^ n ⟹ P) ⟹ P"
by (auto simp: is_nth_power_def)

abbreviation is_square where "is_square ≡ is_nth_power 2"

lemma is_zeroth_power [simp]: "is_nth_power 0 x ⟷ x = 1"

lemma is_first_power [simp]: "is_nth_power 1 x"

lemma is_first_power' [simp]: "is_nth_power (Suc 0) x"

lemma is_nth_power_0 [simp]: "n > 0 ⟹ is_nth_power n (0 :: 'a :: semiring_1)"
by (auto simp: is_nth_power_def power_0_left intro!: exI[of _ 0])

lemma is_nth_power_0_iff [simp]: "is_nth_power n (0 :: 'a :: semiring_1) ⟷ n > 0"
by (cases n) auto

lemma is_nth_power_1 [simp]: "is_nth_power n 1"
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)

lemma is_nth_power_conv_multiplicity:
fixes x :: "'a :: factorial_semiring"
assumes "n > 0"
shows   "is_nth_power n (normalize x) ⟷ (∀p. prime p ⟶ n dvd multiplicity p x)"
proof (cases "x = 0")
case False
show ?thesis
proof (safe intro!: is_nth_powerI elim!: is_nth_powerE)
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
with False and * and assms show "n dvd multiplicity p x"
by (auto simp: prime_elem_multiplicity_power_distrib)
next
assume *: "∀p. prime p ⟶ n dvd multiplicity p x"
have "multiplicity p ((∏p∈prime_factors x. p ^ (multiplicity p x div n)) ^ n) =
multiplicity p x" if "prime p" for p
proof -
from that and * have "n dvd multiplicity p x" by blast
have "multiplicity p x = 0" if "p ∉ prime_factors x"
using that and ‹prime p› by (simp add: prime_factors_multiplicity)
with that and * and assms show ?thesis unfolding prod_power_distrib power_mult [symmetric]
by (subst multiplicity_prod_prime_powers) (auto simp: in_prime_factors_imp_prime elim: dvdE)
qed
with assms False
have "normalize x = normalize ((∏p∈prime_factors x. p ^ (multiplicity p x div n)) ^ n)"
by (intro multiplicity_eq_imp_eq) (auto simp: multiplicity_prod_prime_powers)
thus "normalize x = normalize (∏p∈prime_factors x. p ^ (multiplicity p x div n)) ^ n"
qed
qed (insert assms, auto)

lemma is_nth_power_conv_multiplicity_nat:
assumes "n > 0"
shows   "is_nth_power n (x :: nat) ⟷ (∀p. prime p ⟶ n dvd multiplicity p x)"
using is_nth_power_conv_multiplicity[OF assms, of x] by simp

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

lemma is_nth_power_mult_coprime_natD:
fixes a b :: nat
assumes "coprime a b" "is_nth_power n (a * b)" "a > 0" "b > 0"
shows   "is_nth_power n a" "is_nth_power n b"
proof -
have A: "is_nth_power n a" if "coprime a b" "is_nth_power n (a * b)" "a ≠ 0" "b ≠ 0" "n > 0"
for a b :: nat unfolding is_nth_power_conv_multiplicity_nat[OF ‹n > 0›]
proof safe
fix p :: nat assume p: "prime p"
from ‹coprime a b› have "¬(p dvd a ∧ p dvd b)"
using coprime_common_divisor_nat[of a b p] p by auto
moreover from that and p
have "n dvd multiplicity p a + multiplicity p b"
by (auto simp: is_nth_power_conv_multiplicity_nat prime_elem_multiplicity_mult_distrib)
ultimately show "n dvd multiplicity p a"
by (auto simp: not_dvd_imp_multiplicity_0)
qed
from A[of a b] assms show "is_nth_power n a" by (cases "n = 0") simp_all
from A[of b a] assms show "is_nth_power n b"
by (cases "n = 0") (simp_all add: gcd.commute mult.commute)
qed

lemma is_nth_power_mult_coprime_nat_iff:
fixes a b :: nat
assumes "coprime a b"
shows   "is_nth_power n (a * b) ⟷ is_nth_power n a ∧is_nth_power n b"
using assms
by (cases "a = 0"; cases "b = 0")
(auto intro: is_nth_power_mult dest: is_nth_power_mult_coprime_natD[of a b n]
simp del: One_nat_def)

lemma is_nth_power_prime_power_nat_iff:
fixes p :: nat assumes "prime p"
shows "is_nth_power n (p ^ k) ⟷ n dvd k"
using assms
by (cases "n > 0")
(auto simp: is_nth_power_conv_multiplicity_nat prime_elem_multiplicity_power_distrib)

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

definition is_nth_power_nat :: "nat ⇒ nat ⇒ bool"
where [code_abbrev]: "is_nth_power_nat = is_nth_power"

lemma is_nth_power_nat_code [code]:
"is_nth_power_nat n m =
(if n = 0 then m = 1
else if m = 0 then n > 0
else if n = 1 then True
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)

(* TODO: Harmonise with Discrete.sqrt *)

subsection ‹The \$n\$-root of a natural number›

definition nth_root_nat :: "nat ⇒ nat ⇒ nat" where
"nth_root_nat k n = (if k = 0 then 0 else Max {m. m ^ k ≤ n})"

lemma zeroth_root_nat [simp]: "nth_root_nat 0 n = 0"

lemma nth_root_nat_aux1:
assumes "k > 0"
shows   "{m::nat. m ^ k ≤ n} ⊆ {..n}"
proof safe
fix m assume "m ^ k ≤ n"
show "m ≤ n"
proof (cases "m = 0")
case False
with assms have "m ^ 1 ≤ m ^ k" by (intro power_increasing) simp_all
also note ‹m ^ k ≤ n›
finally show ?thesis by simp
qed simp_all
qed

lemma nth_root_nat_aux2:
assumes "k > 0"
shows   "finite {m::nat. m ^ k ≤ n}" "{m::nat. m ^ k ≤ n} ≠ {}"
proof -
from assms have "{m. m ^ k ≤ n} ⊆ {..n}" by (rule nth_root_nat_aux1)
moreover have "finite {..n}" by simp
ultimately show "finite {m::nat. m ^ k ≤ n}" by (rule finite_subset)
next
from assms show "{m::nat. m ^ k ≤ n} ≠ {}" by (auto intro!: exI[of _ 0] simp: power_0_left)
qed

lemma
assumes "k > 0"
shows   nth_root_nat_power_le: "nth_root_nat k n ^ k ≤ n"
and   nth_root_nat_ge: "x ^ k ≤ n ⟹ x ≤ nth_root_nat k n"
using Max_in[OF nth_root_nat_aux2[OF assms], of n]
Max_ge[OF nth_root_nat_aux2(1)[OF assms], of x n] assms
by (auto simp: nth_root_nat_def)

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

lemma nth_root_nat_unique:
assumes "m ^ k ≤ n" "(m + 1) ^ k > n"
shows   "nth_root_nat k n = m"
proof (cases "k > 0")
case True
from nth_root_nat_less[OF ‹k > 0› assms(2)]
have "nth_root_nat k n ≤ m" by simp
moreover from ‹k > 0› and assms(1) have "nth_root_nat k n ≥ m"
by (intro nth_root_nat_ge)
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_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)

lemma first_root_nat [simp]: "nth_root_nat 1 n = n"
by (intro nth_root_nat_unique) auto

lemma first_root_nat' [simp]: "nth_root_nat (Suc 0) n = n"
by (intro nth_root_nat_unique) auto

lemma nth_root_nat_code_naive':
"nth_root_nat k n = (if k = 0 then 0 else Max (Set.filter (λm. m ^ k ≤ n) {..n}))"
proof (cases "k > 0")
case True
hence "{m. m ^ k ≤ n} ⊆ {..n}" by (rule nth_root_nat_aux1)
hence "Set.filter (λm. m ^ k ≤ n) {..n} = {m. m ^ k ≤ n}"
by (auto simp: Set.filter_def)
with True show ?thesis by (simp add: nth_root_nat_def Set.filter_def)
qed simp

function nth_root_nat_aux :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat" where
"nth_root_nat_aux m k acc n =
(let acc' = (k + 1) ^ m
in  if k ≥ n ∨ acc' > n then k else nth_root_nat_aux m (k+1) acc' n)"
by auto
termination by (relation "measure (λ(_,k,_,n). n - k)", goal_cases) auto

lemma nth_root_nat_aux_le:
assumes "k ^ m ≤ n" "m > 0"
shows   "nth_root_nat_aux m k (k ^ m) n ^ m ≤ n"
using assms
by (induction m k "k ^ m" n rule:  nth_root_nat_aux.induct) (auto simp: Let_def)

lemma nth_root_nat_aux_gt:
assumes "m > 0"
shows   "(nth_root_nat_aux m k (k ^ m) n + 1) ^ m > n"
using assms
proof (induction m k "k ^ m" n rule:  nth_root_nat_aux.induct)
case (1 m k n)
have "n < Suc k ^ m" if "n ≤ k"
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
finally show ?thesis .
qed
with 1 show ?case by (auto simp: Let_def)
qed

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)

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
nth_root_nat_aux m 1 1 n)"
using nth_root_nat_aux_correct[of 1 m n] by (auto simp: )

lemma nth_root_nat_nth_power [simp]: "k > 0 ⟹ nth_root_nat k (n ^ k) = n"
by (intro nth_root_nat_unique order.refl power_strict_mono) simp_all

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

lemma nth_root_nat_mono:
assumes "m ≤ n"
shows   "nth_root_nat k m ≤ nth_root_nat k n"
proof (cases "k = 0")
case False
with assms show ?thesis unfolding nth_root_nat_def
using nth_root_nat_aux2[of k m] nth_root_nat_aux2[of k n]
by (auto intro!: Max_mono)
qed auto

end```