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