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