Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Computational_Algebra/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 12 kB

Quelle Nth_Powers.thy Sprache: Isabelle

(*
  File:      HOL/Computational_Algebra/Nth_Powers.thy
  Author:    Manuel Eberl <manuel@pruvisto.org>

  n-th powers in general and n-th roots of natural numbers
*)
section \<open>$n$-th powers and roots of naturals\<close>
theory Nth_Powers
  imports Primes
begin

subsection \<open>The set of $n$-th powers\<close>

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)"
  by (auto simp add: is_nth_power_def)

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"
  by (simp add: is_nth_power_def)

lemma is_first_power [simp]: "is_nth_power 1 x"
  by (simp add: is_nth_power_def)

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

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 (metis One_nat_def is_nth_power_1)

lemma is_nth_power_conv_multiplicity:
  fixes x :: "'a :: {factorial_semiring, normalization_semidom_multiplicative}"
  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 (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
    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 \<open>prime p\<close> 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)
    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"
      by (simp add: normalize_power)
  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)"
  by (metis assms is_nth_power_def power_mult_distrib)

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 \<open>n > 0\<close>]
  proof safe
    fix p :: nat assume p: "prime p"
    from \<open>coprime a b\<close> have "\<not>(p dvd a \<and> 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: ac_simps)
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')"
  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"

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 (\<exists>k\<in>{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 \<open>n > 0\<close> by simp
    then obtain z where z: "x = y * z"
      by (elim dvdE)
    with \<open>a \<noteq> 0\<close> show "is_nth_power n b"
      by (metis  is_nth_powerI mult_left_cancel power_mult_distrib x y)
  qed (use assms in \<open>auto intro: is_nth_power_mult\<close>)
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 *)

subsection \<open>The $n$-root of a natural number\<close>

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"
  by (simp add: nth_root_nat_def)

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 \<open>m ^ k \<le> n\<close>
    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"
  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"
  shows   "nth_root_nat k n = m"
proof (cases "k > 0")
  case True
  from nth_root_nat_less[OF \<open>k > 0\<close> assms(2)]
    have "nth_root_nat k n \ m" by simp
  moreover from \<open>k > 0\<close> and assms(1) have "nth_root_nat k n \<ge> 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 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

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
  then have "{m. m ^ k \ n} \ {..n}" by (rule nth_root_nat_aux1)
  then have "Set.filter (\m. m ^ k \ n) {..n} = {m. m ^ k \ n}"
    by (auto simp:)
  with True show ?thesis
    by (simp add: nth_root_nat_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 \<ge> n \<or> 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 \<open>m > 0\<close> have "\<dots> \<le> 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 (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
                        nth_root_nat_aux m 1 1 n)"
  using nth_root_nat_aux_correct[of 1 m n] by auto

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)"
  by (metis assms dvd_div_mult_self nth_root_nat_nth_power power_mult)

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

quality96%

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.