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`