src/HOL/Computational_Algebra/Nth_Powers.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (22 months ago)
changeset 66983 df83b66f1d94
parent 66276 acc3b7dd0b21
child 67051 e7e54a0b9197
permissions -rw-r--r--
proper merge (amending fb46c031c841);
     1 (*
     2   File:      HOL/Computational_Algebra/Nth_Powers.thy
     3   Author:    Manuel Eberl <eberlm@in.tum.de>
     4 
     5   n-th powers in general and n-th roots of natural numbers
     6 *)
     7 section \<open>$n$-th powers and roots of naturals\<close>
     8 theory Nth_Powers
     9   imports Primes
    10 begin
    11   
    12 subsection \<open>The set of $n$-th powers\<close>
    13 
    14 definition is_nth_power :: "nat \<Rightarrow> 'a :: monoid_mult \<Rightarrow> bool" where
    15   "is_nth_power n x \<longleftrightarrow> (\<exists>y. x = y ^ n)"
    16   
    17 lemma is_nth_power_nth_power [simp, intro]: "is_nth_power n (x ^ n)"
    18   by (auto simp add: is_nth_power_def)
    19 
    20 lemma is_nth_powerI [intro?]: "x = y ^ n \<Longrightarrow> is_nth_power n x"
    21   by (auto simp: is_nth_power_def)
    22 
    23 lemma is_nth_powerE: "is_nth_power n x \<Longrightarrow> (\<And>y. x = y ^ n \<Longrightarrow> P) \<Longrightarrow> P"
    24   by (auto simp: is_nth_power_def)
    25 
    26   
    27 abbreviation is_square where "is_square \<equiv> is_nth_power 2"
    28   
    29 lemma is_zeroth_power [simp]: "is_nth_power 0 x \<longleftrightarrow> x = 1"
    30   by (simp add: is_nth_power_def)
    31 
    32 lemma is_first_power [simp]: "is_nth_power 1 x"
    33   by (simp add: is_nth_power_def)
    34 
    35 lemma is_first_power' [simp]: "is_nth_power (Suc 0) x"
    36   by (simp add: is_nth_power_def)
    37 
    38 lemma is_nth_power_0 [simp]: "n > 0 \<Longrightarrow> is_nth_power n (0 :: 'a :: semiring_1)" 
    39   by (auto simp: is_nth_power_def power_0_left intro!: exI[of _ 0])
    40     
    41 lemma is_nth_power_0_iff [simp]: "is_nth_power n (0 :: 'a :: semiring_1) \<longleftrightarrow> n > 0"
    42   by (cases n) auto
    43 
    44 lemma is_nth_power_1 [simp]: "is_nth_power n 1"
    45   by (auto simp: is_nth_power_def intro!: exI[of _ 1])
    46 
    47 lemma is_nth_power_Suc_0 [simp]: "is_nth_power n (Suc 0)"
    48   by (simp add: One_nat_def [symmetric] del: One_nat_def)
    49 
    50 lemma is_nth_power_conv_multiplicity: 
    51   fixes x :: "'a :: factorial_semiring"
    52   assumes "n > 0"
    53   shows   "is_nth_power n (normalize x) \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)"
    54 proof (cases "x = 0")
    55   case False
    56   show ?thesis
    57   proof (safe intro!: is_nth_powerI elim!: is_nth_powerE)
    58     fix y p :: 'a assume *: "normalize x = y ^ n" "prime p"
    59     with assms and False have [simp]: "y \<noteq> 0" by (auto simp: power_0_left)
    60     have "multiplicity p x = multiplicity p (y ^ n)"
    61       by (subst *(1) [symmetric]) simp
    62     with False and * and assms show "n dvd multiplicity p x"
    63       by (auto simp: prime_elem_multiplicity_power_distrib)
    64   next
    65     assume *: "\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x"
    66     have "multiplicity p ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) = 
    67             multiplicity p x" if "prime p" for p
    68     proof -
    69       from that and * have "n dvd multiplicity p x" by blast
    70       have "multiplicity p x = 0" if "p \<notin> prime_factors x"
    71         using that and \<open>prime p\<close> by (simp add: prime_factors_multiplicity)
    72       with that and * and assms show ?thesis unfolding prod_power_distrib power_mult [symmetric]
    73         by (subst multiplicity_prod_prime_powers) (auto simp: in_prime_factors_imp_prime elim: dvdE)
    74     qed
    75     with assms False 
    76       have "normalize x = normalize ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n)"
    77       by (intro multiplicity_eq_imp_eq) (auto simp: multiplicity_prod_prime_powers)
    78     thus "normalize x = normalize (\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n"
    79       by (simp add: normalize_power)
    80   qed
    81 qed (insert assms, auto)
    82 
    83 lemma is_nth_power_conv_multiplicity_nat:
    84   assumes "n > 0"
    85   shows   "is_nth_power n (x :: nat) \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)"
    86   using is_nth_power_conv_multiplicity[OF assms, of x] by simp
    87 
    88 lemma is_nth_power_mult:
    89   assumes "is_nth_power n a" "is_nth_power n b"
    90   shows   "is_nth_power n (a * b :: 'a :: comm_monoid_mult)"
    91 proof -
    92   from assms obtain a' b' where "a = a' ^ n" "b = b' ^ n" by (auto elim!: is_nth_powerE)
    93   hence "a * b = (a' * b') ^ n" by (simp add: power_mult_distrib)
    94   thus ?thesis by (rule is_nth_powerI)
    95 qed
    96     
    97 lemma is_nth_power_mult_coprime_natD:
    98   fixes a b :: nat
    99   assumes "coprime a b" "is_nth_power n (a * b)" "a > 0" "b > 0"
   100   shows   "is_nth_power n a" "is_nth_power n b"
   101 proof -
   102   have A: "is_nth_power n a" if "coprime a b" "is_nth_power n (a * b)" "a \<noteq> 0" "b \<noteq> 0" "n > 0" 
   103     for a b :: nat unfolding is_nth_power_conv_multiplicity_nat[OF \<open>n > 0\<close>]
   104   proof safe
   105     fix p :: nat assume p: "prime p"
   106     from \<open>coprime a b\<close> have "\<not>(p dvd a \<and> p dvd b)"
   107       using coprime_common_divisor_nat[of a b p] p by auto
   108     moreover from that and p
   109       have "n dvd multiplicity p a + multiplicity p b"
   110       by (auto simp: is_nth_power_conv_multiplicity_nat prime_elem_multiplicity_mult_distrib)
   111     ultimately show "n dvd multiplicity p a"
   112       by (auto simp: not_dvd_imp_multiplicity_0)
   113   qed
   114   from A[of a b] assms show "is_nth_power n a" by (cases "n = 0") simp_all
   115   from A[of b a] assms show "is_nth_power n b" 
   116     by (cases "n = 0") (simp_all add: gcd.commute mult.commute)
   117 qed
   118     
   119 lemma is_nth_power_mult_coprime_nat_iff:
   120   fixes a b :: nat
   121   assumes "coprime a b"
   122   shows   "is_nth_power n (a * b) \<longleftrightarrow> is_nth_power n a \<and>is_nth_power n b" 
   123   using assms
   124   by (cases "a = 0"; cases "b = 0")
   125      (auto intro: is_nth_power_mult dest: is_nth_power_mult_coprime_natD[of a b n]
   126            simp del: One_nat_def)
   127 
   128 lemma is_nth_power_prime_power_nat_iff:
   129   fixes p :: nat assumes "prime p"
   130   shows "is_nth_power n (p ^ k) \<longleftrightarrow> n dvd k"
   131   using assms
   132   by (cases "n > 0")
   133      (auto simp: is_nth_power_conv_multiplicity_nat prime_elem_multiplicity_power_distrib)
   134 
   135 lemma is_nth_power_nth_power': 
   136   assumes "n dvd n'"
   137   shows   "is_nth_power n (m ^ n')"
   138 proof -
   139   from assms have "n' = n' div n * n" by simp
   140   also have "m ^ \<dots> = (m ^ (n' div n)) ^ n" by (simp add: power_mult)
   141   also have "is_nth_power n \<dots>" by simp
   142   finally show ?thesis .
   143 qed
   144 
   145 definition is_nth_power_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
   146   where [code_abbrev]: "is_nth_power_nat = is_nth_power"
   147 
   148 lemma is_nth_power_nat_code [code]:
   149   "is_nth_power_nat n m = 
   150      (if n = 0 then m = 1 
   151       else if m = 0 then n > 0
   152       else if n = 1 then True
   153       else (\<exists>k\<in>{1..m}. k ^ n = m))"
   154   by (auto simp: is_nth_power_nat_def is_nth_power_def power_eq_iff_eq_base self_le_power)
   155 
   156 
   157 (* TODO: Harmonise with Discrete.sqrt *)
   158 
   159 subsection \<open>The $n$-root of a natural number\<close>
   160 
   161 definition nth_root_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
   162   "nth_root_nat k n = (if k = 0 then 0 else Max {m. m ^ k \<le> n})"
   163 
   164 lemma zeroth_root_nat [simp]: "nth_root_nat 0 n = 0"
   165   by (simp add: nth_root_nat_def)
   166 
   167 lemma nth_root_nat_aux1: 
   168   assumes "k > 0"
   169   shows   "{m::nat. m ^ k \<le> n} \<subseteq> {..n}"
   170 proof safe
   171   fix m assume "m ^ k \<le> n"
   172   show "m \<le> n"
   173   proof (cases "m = 0")
   174     case False
   175     with assms have "m ^ 1 \<le> m ^ k" by (intro power_increasing) simp_all
   176     also note \<open>m ^ k \<le> n\<close>
   177     finally show ?thesis by simp
   178   qed simp_all
   179 qed
   180 
   181 lemma nth_root_nat_aux2:
   182   assumes "k > 0"
   183   shows   "finite {m::nat. m ^ k \<le> n}" "{m::nat. m ^ k \<le> n} \<noteq> {}"
   184 proof -
   185   from assms have "{m. m ^ k \<le> n} \<subseteq> {..n}" by (rule nth_root_nat_aux1)
   186   moreover have "finite {..n}" by simp
   187   ultimately show "finite {m::nat. m ^ k \<le> n}" by (rule finite_subset)
   188 next
   189   from assms show "{m::nat. m ^ k \<le> n} \<noteq> {}" by (auto intro!: exI[of _ 0] simp: power_0_left)
   190 qed
   191 
   192 lemma 
   193   assumes "k > 0"
   194   shows   nth_root_nat_power_le: "nth_root_nat k n ^ k \<le> n"
   195     and   nth_root_nat_ge: "x ^ k \<le> n \<Longrightarrow> x \<le> nth_root_nat k n"
   196   using Max_in[OF nth_root_nat_aux2[OF assms], of n]
   197         Max_ge[OF nth_root_nat_aux2(1)[OF assms], of x n] assms
   198   by (auto simp: nth_root_nat_def)
   199 
   200 lemma nth_root_nat_less: 
   201   assumes "k > 0" "x ^ k > n"
   202   shows   "nth_root_nat k n < x"
   203 proof -
   204   from \<open>k > 0\<close> have "nth_root_nat k n ^ k \<le> n" by (rule nth_root_nat_power_le)
   205   also have "n < x ^ k" by fact
   206   finally show ?thesis by (rule power_less_imp_less_base) simp_all
   207 qed
   208 
   209 lemma nth_root_nat_unique:
   210   assumes "m ^ k \<le> n" "(m + 1) ^ k > n"
   211   shows   "nth_root_nat k n = m"
   212 proof (cases "k > 0")
   213   case True
   214   from nth_root_nat_less[OF \<open>k > 0\<close> assms(2)] 
   215     have "nth_root_nat k n \<le> m" by simp
   216   moreover from \<open>k > 0\<close> and assms(1) have "nth_root_nat k n \<ge> m"
   217     by (intro nth_root_nat_ge)
   218   ultimately show ?thesis by (rule antisym)
   219 qed (insert assms, auto)
   220 
   221 lemma nth_root_nat_0 [simp]: "nth_root_nat k 0 = 0" by (simp add: nth_root_nat_def)
   222 lemma nth_root_nat_1 [simp]: "k > 0 \<Longrightarrow> nth_root_nat k 1 = 1"
   223   by (rule nth_root_nat_unique) (auto simp del: One_nat_def)
   224 lemma nth_root_nat_Suc_0 [simp]: "k > 0 \<Longrightarrow> nth_root_nat k (Suc 0) = Suc 0"
   225   using nth_root_nat_1 by (simp del: nth_root_nat_1)
   226 
   227 lemma first_root_nat [simp]: "nth_root_nat 1 n = n"
   228   by (intro nth_root_nat_unique) auto
   229     
   230 lemma first_root_nat' [simp]: "nth_root_nat (Suc 0) n = n"
   231   by (intro nth_root_nat_unique) auto
   232 
   233 
   234 lemma nth_root_nat_code_naive':
   235   "nth_root_nat k n = (if k = 0 then 0 else Max (Set.filter (\<lambda>m. m ^ k \<le> n) {..n}))"
   236 proof (cases "k > 0")
   237   case True
   238   hence "{m. m ^ k \<le> n} \<subseteq> {..n}" by (rule nth_root_nat_aux1)
   239   hence "Set.filter (\<lambda>m. m ^ k \<le> n) {..n} = {m. m ^ k \<le> n}"
   240     by (auto simp: Set.filter_def)
   241   with True show ?thesis by (simp add: nth_root_nat_def Set.filter_def)
   242 qed simp
   243 
   244 function nth_root_nat_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   245   "nth_root_nat_aux m k acc n =
   246      (let acc' = (k + 1) ^ m
   247       in  if k \<ge> n \<or> acc' > n then k else nth_root_nat_aux m (k+1) acc' n)"
   248   by auto
   249 termination by (relation "measure (\<lambda>(_,k,_,n). n - k)", goal_cases) auto
   250 
   251 lemma nth_root_nat_aux_le:
   252   assumes "k ^ m \<le> n" "m > 0"
   253   shows   "nth_root_nat_aux m k (k ^ m) n ^ m \<le> n"
   254   using assms
   255   by (induction m k "k ^ m" n rule:  nth_root_nat_aux.induct) (auto simp: Let_def)
   256 
   257 lemma nth_root_nat_aux_gt:
   258   assumes "m > 0"
   259   shows   "(nth_root_nat_aux m k (k ^ m) n + 1) ^ m > n"
   260   using assms
   261 proof (induction m k "k ^ m" n rule:  nth_root_nat_aux.induct)
   262   case (1 m k n)
   263   have "n < Suc k ^ m" if "n \<le> k"
   264   proof -
   265     note that
   266     also have "k < Suc k ^ 1" by simp
   267     also from \<open>m > 0\<close> have "\<dots> \<le> Suc k ^ m" by (intro power_increasing) simp_all
   268     finally show ?thesis .
   269   qed
   270   with 1 show ?case by (auto simp: Let_def)
   271 qed
   272 
   273 lemma nth_root_nat_aux_correct:
   274   assumes "k ^ m \<le> n" "m > 0"
   275   shows   "nth_root_nat_aux m k (k ^ m) n = nth_root_nat m n"
   276   by (rule sym, intro nth_root_nat_unique nth_root_nat_aux_le nth_root_nat_aux_gt assms)
   277 
   278 lemma nth_root_nat_naive_code [code]:
   279   "nth_root_nat m n = (if m = 0 \<or> n = 0 then 0 else if m = 1 \<or> n = 1 then n else
   280                         nth_root_nat_aux m 1 1 n)"
   281   using nth_root_nat_aux_correct[of 1 m n] by (auto simp: )
   282 
   283 
   284 lemma nth_root_nat_nth_power [simp]: "k > 0 \<Longrightarrow> nth_root_nat k (n ^ k) = n"
   285   by (intro nth_root_nat_unique order.refl power_strict_mono) simp_all
   286 
   287 lemma nth_root_nat_nth_power':
   288   assumes "k > 0" "k dvd m" 
   289   shows   "nth_root_nat k (n ^ m) = n ^ (m div k)"
   290 proof -
   291   from assms have "m = (m div k) * k" by simp
   292   also have "n ^ \<dots> = (n ^ (m div k)) ^ k" by (simp add: power_mult)
   293   also from assms have "nth_root_nat k \<dots> = n ^ (m div k)" by simp
   294   finally show ?thesis .
   295 qed
   296 
   297 lemma nth_root_nat_mono:
   298   assumes "m \<le> n"
   299   shows   "nth_root_nat k m \<le> nth_root_nat k n"
   300 proof (cases "k = 0")
   301   case False
   302   with assms show ?thesis unfolding nth_root_nat_def
   303     using nth_root_nat_aux2[of k m] nth_root_nat_aux2[of k n]
   304     by (auto intro!: Max_mono)
   305 qed auto
   306 
   307 end