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