src/HOL/Computational_Algebra/Squarefree.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);
eberlm@66276
     1
(*
eberlm@66276
     2
  File:      HOL/Computational_Algebra/Squarefree.thy
eberlm@66276
     3
  Author:    Manuel Eberl <eberlm@in.tum.de>
eberlm@66276
     4
eberlm@66276
     5
  Squarefreeness and decomposition of ring elements into square part and squarefree part
eberlm@66276
     6
*)
eberlm@66276
     7
section \<open>Squarefreeness\<close>
eberlm@66276
     8
theory Squarefree
eberlm@66276
     9
imports Primes
eberlm@66276
    10
begin
eberlm@66276
    11
  
eberlm@66276
    12
(* TODO: Generalise to n-th powers *)
eberlm@66276
    13
eberlm@66276
    14
definition squarefree :: "'a :: comm_monoid_mult \<Rightarrow> bool" where
eberlm@66276
    15
  "squarefree n \<longleftrightarrow> (\<forall>x. x ^ 2 dvd n \<longrightarrow> x dvd 1)"
eberlm@66276
    16
  
eberlm@66276
    17
lemma squarefreeI: "(\<And>x. x ^ 2 dvd n \<Longrightarrow> x dvd 1) \<Longrightarrow> squarefree n"
eberlm@66276
    18
  by (auto simp: squarefree_def)
eberlm@66276
    19
eberlm@66276
    20
lemma squarefreeD: "squarefree n \<Longrightarrow> x ^ 2 dvd n \<Longrightarrow> x dvd 1"
eberlm@66276
    21
  by (auto simp: squarefree_def)
eberlm@66276
    22
eberlm@66276
    23
lemma not_squarefreeI: "x ^ 2 dvd n \<Longrightarrow> \<not>x dvd 1 \<Longrightarrow> \<not>squarefree n"
eberlm@66276
    24
  by (auto simp: squarefree_def)
eberlm@66276
    25
eberlm@66276
    26
lemma not_squarefreeE [case_names square_dvd]: 
eberlm@66276
    27
  "\<not>squarefree n \<Longrightarrow> (\<And>x. x ^ 2 dvd n \<Longrightarrow> \<not>x dvd 1 \<Longrightarrow> P) \<Longrightarrow> P"
eberlm@66276
    28
  by (auto simp: squarefree_def)
eberlm@66276
    29
eberlm@66276
    30
lemma not_squarefree_0 [simp]: "\<not>squarefree (0 :: 'a :: comm_semiring_1)"
eberlm@66276
    31
  by (rule not_squarefreeI[of 0]) auto
eberlm@66276
    32
eberlm@66276
    33
lemma squarefree_factorial_semiring:
eberlm@66276
    34
  assumes "n \<noteq> 0"
eberlm@66276
    35
  shows   "squarefree (n :: 'a :: factorial_semiring) \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> \<not>p ^ 2 dvd n)"
eberlm@66276
    36
  unfolding squarefree_def
eberlm@66276
    37
proof safe
eberlm@66276
    38
  assume *: "\<forall>p. prime p \<longrightarrow> \<not>p ^ 2 dvd n"
eberlm@66276
    39
  fix x :: 'a assume x: "x ^ 2 dvd n"
eberlm@66276
    40
  {
eberlm@66276
    41
    assume "\<not>is_unit x"
eberlm@66276
    42
    moreover from assms and x have "x \<noteq> 0" by auto
eberlm@66276
    43
    ultimately obtain p where "p dvd x" "prime p"
eberlm@66276
    44
      using prime_divisor_exists by blast
eberlm@66276
    45
    with * have "\<not>p ^ 2 dvd n" by blast
eberlm@66276
    46
    moreover from \<open>p dvd x\<close> have "p ^ 2 dvd x ^ 2" by (rule dvd_power_same)
eberlm@66276
    47
    ultimately have "\<not>x ^ 2 dvd n" by (blast dest: dvd_trans)
eberlm@66276
    48
    with x have False by contradiction
eberlm@66276
    49
  }
eberlm@66276
    50
  thus "is_unit x" by blast
eberlm@66276
    51
qed auto
eberlm@66276
    52
eberlm@66276
    53
lemma squarefree_factorial_semiring':
eberlm@66276
    54
  assumes "n \<noteq> 0"
eberlm@66276
    55
  shows   "squarefree (n :: 'a :: factorial_semiring) \<longleftrightarrow> 
eberlm@66276
    56
             (\<forall>p\<in>prime_factors n. multiplicity p n = 1)"
eberlm@66276
    57
proof (subst squarefree_factorial_semiring [OF assms], safe)
eberlm@66276
    58
  fix p assume "\<forall>p\<in>#prime_factorization n. multiplicity p n = 1" "prime p" "p^2 dvd n"
eberlm@66276
    59
  with assms show False
eberlm@66276
    60
    by (cases "p dvd n")
eberlm@66276
    61
       (auto simp: prime_factors_dvd power_dvd_iff_le_multiplicity not_dvd_imp_multiplicity_0)
eberlm@66276
    62
qed (auto intro!: multiplicity_eqI simp: power2_eq_square [symmetric])
eberlm@66276
    63
eberlm@66276
    64
lemma squarefree_factorial_semiring'':
eberlm@66276
    65
  assumes "n \<noteq> 0"
eberlm@66276
    66
  shows   "squarefree (n :: 'a :: factorial_semiring) \<longleftrightarrow> 
eberlm@66276
    67
             (\<forall>p. prime p \<longrightarrow> multiplicity p n \<le> 1)"
eberlm@66276
    68
  by (subst squarefree_factorial_semiring'[OF assms]) (auto simp: prime_factors_multiplicity)
eberlm@66276
    69
eberlm@66276
    70
lemma squarefree_unit [simp]: "is_unit n \<Longrightarrow> squarefree n"
eberlm@66276
    71
proof (rule squarefreeI) 
eberlm@66276
    72
  fix x assume "x^2 dvd n" "n dvd 1"
eberlm@66276
    73
  hence "is_unit (x^2)" by (rule dvd_unit_imp_unit)
eberlm@66276
    74
  thus "is_unit x" by (simp add: is_unit_power_iff)
eberlm@66276
    75
qed
eberlm@66276
    76
eberlm@66276
    77
lemma squarefree_1 [simp]: "squarefree (1 :: 'a :: algebraic_semidom)"
eberlm@66276
    78
  by simp
eberlm@66276
    79
eberlm@66276
    80
lemma squarefree_minus [simp]: "squarefree (-n :: 'a :: comm_ring_1) \<longleftrightarrow> squarefree n"
eberlm@66276
    81
  by (simp add: squarefree_def)
eberlm@66276
    82
eberlm@66276
    83
lemma squarefree_mono: "a dvd b \<Longrightarrow> squarefree b \<Longrightarrow> squarefree a"
eberlm@66276
    84
  by (auto simp: squarefree_def intro: dvd_trans)
eberlm@66276
    85
eberlm@66276
    86
lemma squarefree_multD:
eberlm@66276
    87
  assumes "squarefree (a * b)"
eberlm@66276
    88
  shows   "squarefree a" "squarefree b"
eberlm@66276
    89
  by (rule squarefree_mono[OF _ assms], simp)+
eberlm@66276
    90
    
eberlm@66276
    91
lemma squarefree_prime_elem: 
eberlm@66276
    92
  assumes "prime_elem (p :: 'a :: factorial_semiring)"
eberlm@66276
    93
  shows   "squarefree p"
eberlm@66276
    94
proof -
eberlm@66276
    95
  from assms have "p \<noteq> 0" by auto
eberlm@66276
    96
  show ?thesis
eberlm@66276
    97
  proof (subst squarefree_factorial_semiring [OF \<open>p \<noteq> 0\<close>]; safe)
eberlm@66276
    98
    fix q assume *: "prime q" "q^2 dvd p"
eberlm@66276
    99
    with assms have "multiplicity q p \<ge> 2" by (intro multiplicity_geI) auto
eberlm@66276
   100
    thus False using assms \<open>prime q\<close> prime_multiplicity_other[of q "normalize p"]
eberlm@66276
   101
      by (cases "q = normalize p") simp_all
eberlm@66276
   102
  qed
eberlm@66276
   103
qed
eberlm@66276
   104
eberlm@66276
   105
lemma squarefree_prime: 
eberlm@66276
   106
  assumes "prime (p :: 'a :: factorial_semiring)"
eberlm@66276
   107
  shows   "squarefree p"
eberlm@66276
   108
  using assms by (intro squarefree_prime_elem) auto
eberlm@66276
   109
eberlm@66276
   110
lemma squarefree_mult_coprime:
eberlm@66276
   111
  fixes a b :: "'a :: factorial_semiring_gcd"
eberlm@66276
   112
  assumes "coprime a b" "squarefree a" "squarefree b"
eberlm@66276
   113
  shows   "squarefree (a * b)"
eberlm@66276
   114
proof -
eberlm@66276
   115
  from assms have nz: "a * b \<noteq> 0" by auto
eberlm@66276
   116
  show ?thesis unfolding squarefree_factorial_semiring'[OF nz]
eberlm@66276
   117
  proof
eberlm@66276
   118
    fix p assume p: "p \<in> prime_factors (a * b)"
eberlm@66276
   119
    {
eberlm@66276
   120
      assume "p dvd a \<and> p dvd b"
eberlm@66276
   121
      hence "p dvd gcd a b" by simp
eberlm@66276
   122
      also have "gcd a b = 1" by fact
eberlm@66276
   123
      finally have False using nz using p by (auto simp: prime_factors_dvd)
eberlm@66276
   124
    }
eberlm@66276
   125
    hence "\<not>(p dvd a \<and> p dvd b)" by blast
eberlm@66276
   126
    moreover from p have "p dvd a \<or> p dvd b" using nz 
eberlm@66276
   127
      by (auto simp: prime_factors_dvd prime_dvd_mult_iff)
eberlm@66276
   128
    ultimately show "multiplicity p (a * b) = 1" using nz p assms(2,3)
eberlm@66276
   129
      by (auto simp: prime_elem_multiplicity_mult_distrib prime_factors_multiplicity
eberlm@66276
   130
            not_dvd_imp_multiplicity_0 squarefree_factorial_semiring')
eberlm@66276
   131
  qed
eberlm@66276
   132
qed
eberlm@66276
   133
eberlm@66276
   134
lemma squarefree_prod_coprime:
eberlm@66276
   135
  fixes f :: "'a \<Rightarrow> 'b :: factorial_semiring_gcd"
eberlm@66276
   136
  assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime (f a) (f b)"
eberlm@66276
   137
  assumes "\<And>a. a \<in> A \<Longrightarrow> squarefree (f a)"
eberlm@66276
   138
  shows   "squarefree (prod f A)"
eberlm@66276
   139
  using assms 
eberlm@66276
   140
  by (induction A rule: infinite_finite_induct) 
eberlm@66276
   141
     (auto intro!: squarefree_mult_coprime prod_coprime')
eberlm@66276
   142
eberlm@66276
   143
lemma squarefree_powerD: "m > 0 \<Longrightarrow> squarefree (n ^ m) \<Longrightarrow> squarefree n"
eberlm@66276
   144
  by (cases m) (auto dest: squarefree_multD)
eberlm@66276
   145
eberlm@66276
   146
lemma squarefree_power_iff: 
eberlm@66276
   147
  "squarefree (n ^ m) \<longleftrightarrow> m = 0 \<or> is_unit n \<or> (squarefree n \<and> m = 1)"
eberlm@66276
   148
proof safe
eberlm@66276
   149
  assume "squarefree (n ^ m)" "m > 0" "\<not>is_unit n"
eberlm@66276
   150
  show "m = 1"
eberlm@66276
   151
  proof (rule ccontr)
eberlm@66276
   152
    assume "m \<noteq> 1"
eberlm@66276
   153
    with \<open>m > 0\<close> have "n ^ 2 dvd n ^ m" by (intro le_imp_power_dvd) auto
eberlm@66276
   154
    from this and \<open>\<not>is_unit n\<close> have "\<not>squarefree (n ^ m)" by (rule not_squarefreeI)
eberlm@66276
   155
    with \<open>squarefree (n ^ m)\<close> show False by contradiction
eberlm@66276
   156
  qed
eberlm@66276
   157
qed (auto simp: is_unit_power_iff dest: squarefree_powerD)
eberlm@66276
   158
eberlm@66276
   159
definition squarefree_nat :: "nat \<Rightarrow> bool" where
eberlm@66276
   160
  [code_abbrev]: "squarefree_nat = squarefree"
eberlm@66276
   161
  
eberlm@66276
   162
lemma squarefree_nat_code_naive [code]: 
eberlm@66276
   163
  "squarefree_nat n \<longleftrightarrow> n \<noteq> 0 \<and> (\<forall>k\<in>{2..n}. \<not>k ^ 2 dvd n)"
eberlm@66276
   164
proof safe
eberlm@66276
   165
  assume *: "\<forall>k\<in>{2..n}. \<not> k\<^sup>2 dvd n" and n: "n > 0"
eberlm@66276
   166
  show "squarefree_nat n" unfolding squarefree_nat_def
eberlm@66276
   167
  proof (rule squarefreeI)
eberlm@66276
   168
    fix k assume k: "k ^ 2 dvd n"
eberlm@66276
   169
    have "k dvd n" by (rule dvd_trans[OF _ k]) auto
eberlm@66276
   170
    with n have "k \<le> n" by (intro dvd_imp_le)
eberlm@66276
   171
    with bspec[OF *, of k] k have "\<not>k > 1" by (intro notI) auto
eberlm@66276
   172
    moreover from k and n have "k \<noteq> 0" by (intro notI) auto
eberlm@66276
   173
    ultimately have "k = 1" by presburger
eberlm@66276
   174
    thus "is_unit k" by simp
eberlm@66276
   175
  qed
eberlm@66276
   176
qed (auto simp: squarefree_nat_def squarefree_def intro!: Nat.gr0I)
eberlm@66276
   177
eberlm@66276
   178
eberlm@66276
   179
eberlm@66276
   180
definition square_part :: "'a :: factorial_semiring \<Rightarrow> 'a" where
eberlm@66276
   181
  "square_part n = (if n = 0 then 0 else 
eberlm@66276
   182
     normalize (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n div 2)))"
eberlm@66276
   183
  
eberlm@66276
   184
lemma square_part_nonzero: 
eberlm@66276
   185
  "n \<noteq> 0 \<Longrightarrow> square_part n = normalize (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n div 2))"
eberlm@66276
   186
  by (simp add: square_part_def)
eberlm@66276
   187
  
eberlm@66276
   188
lemma square_part_0 [simp]: "square_part 0 = 0"
eberlm@66276
   189
  by (simp add: square_part_def)
eberlm@66276
   190
eberlm@66276
   191
lemma square_part_unit [simp]: "is_unit x \<Longrightarrow> square_part x = 1"
eberlm@66276
   192
  by (auto simp: square_part_def prime_factorization_unit)
eberlm@66276
   193
eberlm@66276
   194
lemma square_part_1 [simp]: "square_part 1 = 1"
eberlm@66276
   195
  by simp
eberlm@66276
   196
    
eberlm@66276
   197
lemma square_part_0_iff [simp]: "square_part n = 0 \<longleftrightarrow> n = 0"
eberlm@66276
   198
  by (simp add: square_part_def)
eberlm@66276
   199
eberlm@66276
   200
lemma normalize_uminus [simp]: 
eberlm@66276
   201
  "normalize (-x :: 'a :: {normalization_semidom, comm_ring_1}) = normalize x"
eberlm@66276
   202
  by (rule associatedI) auto
eberlm@66276
   203
eberlm@66276
   204
lemma multiplicity_uminus_right [simp]:
eberlm@66276
   205
  "multiplicity (x :: 'a :: {factorial_semiring, comm_ring_1}) (-y) = multiplicity x y"
eberlm@66276
   206
proof -
eberlm@66276
   207
  have "multiplicity x (-y) = multiplicity x (normalize (-y))"
eberlm@66276
   208
    by (rule multiplicity_normalize_right [symmetric])
eberlm@66276
   209
  also have "\<dots> = multiplicity x y" by simp
eberlm@66276
   210
  finally show ?thesis .
eberlm@66276
   211
qed
eberlm@66276
   212
eberlm@66276
   213
lemma multiplicity_uminus_left [simp]:
eberlm@66276
   214
  "multiplicity (-x :: 'a :: {factorial_semiring, comm_ring_1}) y = multiplicity x y"
eberlm@66276
   215
proof -
eberlm@66276
   216
  have "multiplicity (-x) y = multiplicity (normalize (-x)) y"
eberlm@66276
   217
    by (rule multiplicity_normalize_left [symmetric])
eberlm@66276
   218
  also have "\<dots> = multiplicity x y" by simp
eberlm@66276
   219
  finally show ?thesis .
eberlm@66276
   220
qed
eberlm@66276
   221
eberlm@66276
   222
lemma prime_factorization_uminus [simp]:
eberlm@66276
   223
  "prime_factorization (-x :: 'a :: {factorial_semiring, comm_ring_1}) = prime_factorization x"
eberlm@66276
   224
  by (rule prime_factorization_cong) simp_all
eberlm@66276
   225
eberlm@66276
   226
lemma square_part_uminus [simp]: 
eberlm@66276
   227
    "square_part (-x :: 'a :: {factorial_semiring, comm_ring_1}) = square_part x"
eberlm@66276
   228
  by (simp add: square_part_def)
eberlm@66276
   229
  
eberlm@66276
   230
lemma prime_multiplicity_square_part:
eberlm@66276
   231
  assumes "prime p"
eberlm@66276
   232
  shows   "multiplicity p (square_part n) = multiplicity p n div 2"
eberlm@66276
   233
proof (cases "n = 0")
eberlm@66276
   234
  case False
eberlm@66276
   235
  thus ?thesis unfolding square_part_nonzero[OF False] multiplicity_normalize_right
eberlm@66276
   236
    using finite_prime_divisors[of n] assms
eberlm@66276
   237
    by (subst multiplicity_prod_prime_powers)
eberlm@66276
   238
       (auto simp: not_dvd_imp_multiplicity_0 prime_factors_dvd multiplicity_prod_prime_powers)
eberlm@66276
   239
qed auto
eberlm@66276
   240
eberlm@66276
   241
lemma square_part_square_dvd [simp, intro]: "square_part n ^ 2 dvd n"
eberlm@66276
   242
proof (cases "n = 0")
eberlm@66276
   243
  case False
eberlm@66276
   244
  thus ?thesis
eberlm@66276
   245
    by (intro multiplicity_le_imp_dvd) 
eberlm@66276
   246
       (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_power_distrib)
eberlm@66276
   247
qed auto
eberlm@66276
   248
  
eberlm@66276
   249
lemma prime_multiplicity_le_imp_dvd:
eberlm@66276
   250
  assumes "x \<noteq> 0" "y \<noteq> 0"
eberlm@66276
   251
  shows   "x dvd y \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y)"
eberlm@66276
   252
  using assms by (auto intro: multiplicity_le_imp_dvd dvd_imp_multiplicity_le)
eberlm@66276
   253
eberlm@66276
   254
lemma dvd_square_part_iff: "x dvd square_part n \<longleftrightarrow> x ^ 2 dvd n"
eberlm@66276
   255
proof (cases "x = 0"; cases "n = 0")
eberlm@66276
   256
  assume nz: "x \<noteq> 0" "n \<noteq> 0"
eberlm@66276
   257
  thus ?thesis
eberlm@66276
   258
    by (subst (1 2) prime_multiplicity_le_imp_dvd)
eberlm@66276
   259
       (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_power_distrib)
eberlm@66276
   260
qed auto
eberlm@66276
   261
eberlm@66276
   262
eberlm@66276
   263
definition squarefree_part :: "'a :: factorial_semiring \<Rightarrow> 'a" where
eberlm@66276
   264
  "squarefree_part n = (if n = 0 then 1 else n div square_part n ^ 2)"
eberlm@66276
   265
eberlm@66276
   266
lemma squarefree_part_0 [simp]: "squarefree_part 0 = 1"
eberlm@66276
   267
  by (simp add: squarefree_part_def)
eberlm@66276
   268
eberlm@66276
   269
lemma squarefree_part_unit [simp]: "is_unit n \<Longrightarrow> squarefree_part n = n"
eberlm@66276
   270
  by (auto simp add: squarefree_part_def)
eberlm@66276
   271
  
eberlm@66276
   272
lemma squarefree_part_1 [simp]: "squarefree_part 1 = 1"
eberlm@66276
   273
  by simp
eberlm@66276
   274
    
eberlm@66276
   275
lemma squarefree_decompose: "n = squarefree_part n * square_part n ^ 2"
eberlm@66276
   276
  by (simp add: squarefree_part_def)
eberlm@66276
   277
eberlm@66276
   278
lemma squarefree_part_uminus [simp]: 
eberlm@66276
   279
  assumes "x \<noteq> 0"
eberlm@66276
   280
  shows   "squarefree_part (-x :: 'a :: {factorial_semiring, comm_ring_1}) = -squarefree_part x"
eberlm@66276
   281
proof -
eberlm@66276
   282
  have "-(squarefree_part x * square_part x ^ 2) = -x" 
eberlm@66276
   283
    by (subst squarefree_decompose [symmetric]) auto
eberlm@66276
   284
  also have "\<dots> = squarefree_part (-x) * square_part (-x) ^ 2" by (rule squarefree_decompose)
eberlm@66276
   285
  finally have "(- squarefree_part x) * square_part x ^ 2 = 
eberlm@66276
   286
                  squarefree_part (-x) * square_part x ^ 2" by simp
eberlm@66276
   287
  thus ?thesis using assms by (subst (asm) mult_right_cancel) auto
eberlm@66276
   288
qed
eberlm@66276
   289
eberlm@66276
   290
lemma squarefree_part_nonzero [simp]: "squarefree_part n \<noteq> 0"
eberlm@66276
   291
  using squarefree_decompose[of n] by (cases "n \<noteq> 0") auto    
eberlm@66276
   292
eberlm@66276
   293
lemma prime_multiplicity_squarefree_part:
eberlm@66276
   294
  assumes "prime p"
eberlm@66276
   295
  shows   "multiplicity p (squarefree_part n) = multiplicity p n mod 2"
eberlm@66276
   296
proof (cases "n = 0")
eberlm@66276
   297
  case False
eberlm@66276
   298
  hence n: "n \<noteq> 0" by auto
eberlm@66276
   299
  have "multiplicity p n mod 2 + 2 * (multiplicity p n div 2) = multiplicity p n" by simp
eberlm@66276
   300
  also have "\<dots> = multiplicity p (squarefree_part n * square_part n ^ 2)"
eberlm@66276
   301
    by (subst squarefree_decompose[of n]) simp
eberlm@66276
   302
  also from assms n have "\<dots> = multiplicity p (squarefree_part n) + 2 * (multiplicity p n div 2)"
eberlm@66276
   303
    by (subst prime_elem_multiplicity_mult_distrib) 
eberlm@66276
   304
       (auto simp: prime_elem_multiplicity_power_distrib prime_multiplicity_square_part)
eberlm@66276
   305
  finally show ?thesis by (subst (asm) add_right_cancel) simp
eberlm@66276
   306
qed auto
eberlm@66276
   307
  
eberlm@66276
   308
lemma prime_multiplicity_squarefree_part_le_Suc_0 [intro]:
eberlm@66276
   309
  assumes "prime p"
eberlm@66276
   310
  shows   "multiplicity p (squarefree_part n) \<le> Suc 0"
eberlm@66276
   311
  by (simp add: assms prime_multiplicity_squarefree_part)
eberlm@66276
   312
eberlm@66276
   313
lemma squarefree_squarefree_part [simp, intro]: "squarefree (squarefree_part n)"
eberlm@66276
   314
  by (subst squarefree_factorial_semiring'')
eberlm@66276
   315
     (auto simp: prime_multiplicity_squarefree_part_le_Suc_0)
eberlm@66276
   316
  
eberlm@66276
   317
lemma squarefree_decomposition_unique:
eberlm@66276
   318
  assumes "square_part m = square_part n"
eberlm@66276
   319
  assumes "squarefree_part m = squarefree_part n"
eberlm@66276
   320
  shows   "m = n"
eberlm@66276
   321
  by (subst (1 2) squarefree_decompose) (simp_all add: assms)
eberlm@66276
   322
    
eberlm@66276
   323
lemma normalize_square_part [simp]: "normalize (square_part x) = square_part x"
eberlm@66276
   324
  by (simp add: square_part_def)
eberlm@66276
   325
eberlm@66276
   326
lemma square_part_even_power': "square_part (x ^ (2 * n)) = normalize (x ^ n)"
eberlm@66276
   327
proof (cases "x = 0")
eberlm@66276
   328
  case False
eberlm@66276
   329
  have "normalize (square_part (x ^ (2 * n))) = normalize (x ^ n)" using False
eberlm@66276
   330
    by (intro multiplicity_eq_imp_eq)
eberlm@66276
   331
       (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_power_distrib)
eberlm@66276
   332
  thus ?thesis by simp
eberlm@66276
   333
qed (auto simp: power_0_left)
eberlm@66276
   334
eberlm@66276
   335
lemma square_part_even_power: "even n \<Longrightarrow> square_part (x ^ n) = normalize (x ^ (n div 2))"
eberlm@66276
   336
  by (subst square_part_even_power' [symmetric]) auto
eberlm@66276
   337
eberlm@66276
   338
lemma square_part_odd_power': "square_part (x ^ (Suc (2 * n))) = normalize (x ^ n * square_part x)"
eberlm@66276
   339
proof (cases "x = 0")
eberlm@66276
   340
  case False
eberlm@66276
   341
  have "normalize (square_part (x ^ (Suc (2 * n)))) = normalize (square_part x * x ^ n)" 
eberlm@66276
   342
  proof (rule multiplicity_eq_imp_eq, goal_cases)
eberlm@66276
   343
    case (3 p)
eberlm@66276
   344
    hence "multiplicity p (square_part (x ^ Suc (2 * n))) = 
eberlm@66276
   345
             (2 * (n * multiplicity p x) + multiplicity p x) div 2"
eberlm@66276
   346
      by (subst prime_multiplicity_square_part)
eberlm@66276
   347
         (auto simp: False prime_elem_multiplicity_power_distrib algebra_simps simp del: power_Suc)
eberlm@66276
   348
    also from 3 False have "\<dots> = multiplicity p (square_part x * x ^ n)"
eberlm@66276
   349
      by (subst div_mult_self4) (auto simp: prime_multiplicity_square_part 
eberlm@66276
   350
            prime_elem_multiplicity_mult_distrib prime_elem_multiplicity_power_distrib)
eberlm@66276
   351
    finally show ?case .
eberlm@66276
   352
  qed (insert False, auto)
eberlm@66276
   353
  thus ?thesis by (simp add: mult_ac)
eberlm@66276
   354
qed auto
eberlm@66276
   355
eberlm@66276
   356
lemma square_part_odd_power: 
eberlm@66276
   357
  "odd n \<Longrightarrow> square_part (x ^ n) = normalize (x ^ (n div 2) * square_part x)"
eberlm@66276
   358
  by (subst square_part_odd_power' [symmetric]) auto
eberlm@66276
   359
eberlm@66276
   360
end