(* File: HOL/Computational_Algebra/Squarefree.thy Author: Manuel Eberl <manuel@pruvisto.org> Squarefreeness and decomposition of ring elements into square part and squarefree part *) section ‹Squarefreeness› theory Squarefree imports Primes begin (* TODO: Generalise to n-th powers *) definition squarefree :: "'a :: comm_monoid_mult ⇒ bool" where "squarefree n ⟷ (∀x. x ^ 2 dvd n ⟶ x dvd 1)" lemma squarefreeI: "(⋀x. x ^ 2 dvd n ⟹ x dvd 1) ⟹ squarefree n" by (auto simp: squarefree_def) lemma squarefreeD: "squarefree n ⟹ x ^ 2 dvd n ⟹ x dvd 1" by (auto simp: squarefree_def) lemma not_squarefreeI: "x ^ 2 dvd n ⟹ ¬x dvd 1 ⟹ ¬squarefree n" by (auto simp: squarefree_def) lemma not_squarefreeE [case_names square_dvd]: "¬squarefree n ⟹ (⋀x. x ^ 2 dvd n ⟹ ¬x dvd 1 ⟹ P) ⟹ P" by (auto simp: squarefree_def) lemma not_squarefree_0 [simp]: "¬squarefree (0 :: 'a :: comm_semiring_1)" by (rule not_squarefreeI[of 0]) auto lemma squarefree_factorial_semiring: assumes "n ≠ 0" shows "squarefree (n :: 'a :: factorial_semiring) ⟷ (∀p. prime p ⟶ ¬p ^ 2 dvd n)" unfolding squarefree_def proof safe assume *: "∀p. prime p ⟶ ¬p ^ 2 dvd n" fix x :: 'a assume x: "x ^ 2 dvd n" { assume "¬is_unit x" moreover from assms and x have "x ≠ 0" by auto ultimately obtain p where "p dvd x" "prime p" using prime_divisor_exists by blast with * have "¬p ^ 2 dvd n" by blast moreover from ‹p dvd x› have "p ^ 2 dvd x ^ 2" by (rule dvd_power_same) ultimately have "¬x ^ 2 dvd n" by (blast dest: dvd_trans) with x have False by contradiction } thus "is_unit x" by blast qed auto lemma squarefree_factorial_semiring': assumes "n ≠ 0" shows "squarefree (n :: 'a :: factorial_semiring) ⟷ (∀p∈prime_factors n. multiplicity p n = 1)" proof (subst squarefree_factorial_semiring [OF assms], safe) fix p assume "∀p∈#prime_factorization n. multiplicity p n = 1" "prime p" "p^2 dvd n" with assms show False by (cases "p dvd n") (auto simp: prime_factors_dvd power_dvd_iff_le_multiplicity not_dvd_imp_multiplicity_0) qed (auto intro!: multiplicity_eqI simp: power2_eq_square [symmetric]) lemma squarefree_factorial_semiring'': assumes "n ≠ 0" shows "squarefree (n :: 'a :: factorial_semiring) ⟷ (∀p. prime p ⟶ multiplicity p n ≤ 1)" by (subst squarefree_factorial_semiring'[OF assms]) (auto simp: prime_factors_multiplicity) lemma squarefree_unit [simp]: "is_unit n ⟹ squarefree n" proof (rule squarefreeI) fix x assume "x^2 dvd n" "n dvd 1" hence "is_unit (x^2)" by (rule dvd_unit_imp_unit) thus "is_unit x" by (simp add: is_unit_power_iff) qed lemma squarefree_1 [simp]: "squarefree (1 :: 'a :: algebraic_semidom)" by simp lemma squarefree_minus [simp]: "squarefree (-n :: 'a :: comm_ring_1) ⟷ squarefree n" by (simp add: squarefree_def) lemma squarefree_mono: "a dvd b ⟹ squarefree b ⟹ squarefree a" by (auto simp: squarefree_def intro: dvd_trans) lemma squarefree_multD: assumes "squarefree (a * b)" shows "squarefree a" "squarefree b" by (rule squarefree_mono[OF _ assms], simp)+ lemma squarefree_prime_elem: assumes "prime_elem (p :: 'a :: factorial_semiring)" shows "squarefree p" proof - from assms have "p ≠ 0" by auto show ?thesis proof (subst squarefree_factorial_semiring [OF ‹p ≠ 0›]; safe) fix q assume *: "prime q" "q^2 dvd p" with assms have "multiplicity q p ≥ 2" by (intro multiplicity_geI) auto thus False using assms ‹prime q› prime_multiplicity_other[of q "normalize p"] by (cases "q = normalize p") simp_all qed qed lemma squarefree_prime: assumes "prime (p :: 'a :: factorial_semiring)" shows "squarefree p" using assms by (intro squarefree_prime_elem) auto lemma squarefree_mult_coprime: fixes a b :: "'a :: factorial_semiring_gcd" assumes "coprime a b" "squarefree a" "squarefree b" shows "squarefree (a * b)" proof - from assms have nz: "a * b ≠ 0" by auto show ?thesis unfolding squarefree_factorial_semiring'[OF nz] proof fix p assume p: "p ∈ prime_factors (a * b)" with nz have "prime p" by (simp add: prime_factors_dvd) have "¬ (p dvd a ∧ p dvd b)" proof assume "p dvd a ∧ p dvd b" with ‹coprime a b› have "is_unit p" by (auto intro: coprime_common_divisor) with ‹prime p› show False by simp qed moreover from p have "p dvd a ∨ p dvd b" using nz by (auto simp: prime_factors_dvd prime_dvd_mult_iff) ultimately show "multiplicity p (a * b) = 1" using nz p assms(2,3) by (auto simp: prime_elem_multiplicity_mult_distrib prime_factors_multiplicity not_dvd_imp_multiplicity_0 squarefree_factorial_semiring') qed qed lemma squarefree_prod_coprime: fixes f :: "'a ⇒ 'b :: factorial_semiring_gcd" assumes "⋀a b. a ∈ A ⟹ b ∈ A ⟹ a ≠ b ⟹ coprime (f a) (f b)" assumes "⋀a. a ∈ A ⟹ squarefree (f a)" shows "squarefree (prod f A)" using assms by (induction A rule: infinite_finite_induct) (auto intro!: squarefree_mult_coprime prod_coprime_right) lemma squarefree_powerD: "m > 0 ⟹ squarefree (n ^ m) ⟹ squarefree n" by (cases m) (auto dest: squarefree_multD) lemma squarefree_power_iff: "squarefree (n ^ m) ⟷ m = 0 ∨ is_unit n ∨ (squarefree n ∧ m = 1)" proof safe assume "squarefree (n ^ m)" "m > 0" "¬is_unit n" show "m = 1" proof (rule ccontr) assume "m ≠ 1" with ‹m > 0› have "n ^ 2 dvd n ^ m" by (intro le_imp_power_dvd) auto from this and ‹¬is_unit n› have "¬squarefree (n ^ m)" by (rule not_squarefreeI) with ‹squarefree (n ^ m)› show False by contradiction qed qed (auto simp: is_unit_power_iff dest: squarefree_powerD) definition squarefree_nat :: "nat ⇒ bool" where [code_abbrev]: "squarefree_nat = squarefree" lemma squarefree_nat_code_naive [code]: "squarefree_nat n ⟷ n ≠ 0 ∧ (∀k∈{2..n}. ¬k ^ 2 dvd n)" proof safe assume *: "∀k∈{2..n}. ¬ k⇧^{2}dvd n" and n: "n > 0" show "squarefree_nat n" unfolding squarefree_nat_def proof (rule squarefreeI) fix k assume k: "k ^ 2 dvd n" have "k dvd n" by (rule dvd_trans[OF _ k]) auto with n have "k ≤ n" by (intro dvd_imp_le) with bspec[OF *, of k] k have "¬k > 1" by (intro notI) auto moreover from k and n have "k ≠ 0" by (intro notI) auto ultimately have "k = 1" by presburger thus "is_unit k" by simp qed qed (auto simp: squarefree_nat_def squarefree_def intro!: Nat.gr0I) definition square_part :: "'a :: factorial_semiring ⇒ 'a" where "square_part n = (if n = 0 then 0 else normalize (∏p∈prime_factors n. p ^ (multiplicity p n div 2)))" lemma square_part_nonzero: "n ≠ 0 ⟹ square_part n = normalize (∏p∈prime_factors n. p ^ (multiplicity p n div 2))" by (simp add: square_part_def) lemma square_part_0 [simp]: "square_part 0 = 0" by (simp add: square_part_def) lemma square_part_unit [simp]: "is_unit x ⟹ square_part x = 1" by (auto simp: square_part_def prime_factorization_unit) lemma square_part_1 [simp]: "square_part 1 = 1" by simp lemma square_part_0_iff [simp]: "square_part n = 0 ⟷ n = 0" by (simp add: square_part_def) lemma normalize_uminus [simp]: "normalize (-x :: 'a :: {normalization_semidom, comm_ring_1}) = normalize x" by (rule associatedI) auto lemma multiplicity_uminus_right [simp]: "multiplicity (x :: 'a :: {factorial_semiring, comm_ring_1}) (-y) = multiplicity x y" proof - have "multiplicity x (-y) = multiplicity x (normalize (-y))" by (rule multiplicity_normalize_right [symmetric]) also have "… = multiplicity x y" by simp finally show ?thesis . qed lemma multiplicity_uminus_left [simp]: "multiplicity (-x :: 'a :: {factorial_semiring, comm_ring_1}) y = multiplicity x y" proof - have "multiplicity (-x) y = multiplicity (normalize (-x)) y" by (rule multiplicity_normalize_left [symmetric]) also have "… = multiplicity x y" by simp finally show ?thesis . qed lemma prime_factorization_uminus [simp]: "prime_factorization (-x :: 'a :: {factorial_semiring, comm_ring_1}) = prime_factorization x" by (rule prime_factorization_cong) simp_all lemma square_part_uminus [simp]: "square_part (-x :: 'a :: {factorial_semiring, comm_ring_1}) = square_part x" by (simp add: square_part_def) lemma prime_multiplicity_square_part: assumes "prime p" shows "multiplicity p (square_part n) = multiplicity p n div 2" proof (cases "n = 0") case False thus ?thesis unfolding square_part_nonzero[OF False] multiplicity_normalize_right using finite_prime_divisors[of n] assms by (subst multiplicity_prod_prime_powers) (auto simp: not_dvd_imp_multiplicity_0 prime_factors_dvd multiplicity_prod_prime_powers) qed auto lemma square_part_square_dvd [simp, intro]: "square_part n ^ 2 dvd n" proof (cases "n = 0") case False thus ?thesis by (intro multiplicity_le_imp_dvd) (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_power_distrib) qed auto lemma prime_multiplicity_le_imp_dvd: assumes "x ≠ 0" "y ≠ 0" shows "x dvd y ⟷ (∀p. prime p ⟶ multiplicity p x ≤ multiplicity p y)" using assms by (auto intro: multiplicity_le_imp_dvd dvd_imp_multiplicity_le) lemma dvd_square_part_iff: "x dvd square_part n ⟷ x ^ 2 dvd n" proof (cases "x = 0"; cases "n = 0") assume nz: "x ≠ 0" "n ≠ 0" thus ?thesis by (subst (1 2) prime_multiplicity_le_imp_dvd) (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_power_distrib) qed auto definition squarefree_part :: "'a :: factorial_semiring ⇒ 'a" where "squarefree_part n = (if n = 0 then 1 else n div square_part n ^ 2)" lemma squarefree_part_0 [simp]: "squarefree_part 0 = 1" by (simp add: squarefree_part_def) lemma squarefree_part_unit [simp]: "is_unit n ⟹ squarefree_part n = n" by (auto simp add: squarefree_part_def) lemma squarefree_part_1 [simp]: "squarefree_part 1 = 1" by simp lemma squarefree_decompose: "n = squarefree_part n * square_part n ^ 2" by (simp add: squarefree_part_def) lemma squarefree_part_uminus [simp]: assumes "x ≠ 0" shows "squarefree_part (-x :: 'a :: {factorial_semiring, comm_ring_1}) = -squarefree_part x" proof - have "-(squarefree_part x * square_part x ^ 2) = -x" by (subst squarefree_decompose [symmetric]) auto also have "… = squarefree_part (-x) * square_part (-x) ^ 2" by (rule squarefree_decompose) finally have "(- squarefree_part x) * square_part x ^ 2 = squarefree_part (-x) * square_part x ^ 2" by simp thus ?thesis using assms by (subst (asm) mult_right_cancel) auto qed lemma squarefree_part_nonzero [simp]: "squarefree_part n ≠ 0" using squarefree_decompose[of n] by (cases "n ≠ 0") auto lemma prime_multiplicity_squarefree_part: assumes "prime p" shows "multiplicity p (squarefree_part n) = multiplicity p n mod 2" proof (cases "n = 0") case False hence n: "n ≠ 0" by auto have "multiplicity p n mod 2 + 2 * (multiplicity p n div 2) = multiplicity p n" by simp also have "… = multiplicity p (squarefree_part n * square_part n ^ 2)" by (subst squarefree_decompose[of n]) simp also from assms n have "… = multiplicity p (squarefree_part n) + 2 * (multiplicity p n div 2)" by (subst prime_elem_multiplicity_mult_distrib) (auto simp: prime_elem_multiplicity_power_distrib prime_multiplicity_square_part) finally show ?thesis by (subst (asm) add_right_cancel) simp qed auto lemma prime_multiplicity_squarefree_part_le_Suc_0 [intro]: assumes "prime p" shows "multiplicity p (squarefree_part n) ≤ Suc 0" by (simp add: assms prime_multiplicity_squarefree_part) lemma squarefree_squarefree_part [simp, intro]: "squarefree (squarefree_part n)" by (subst squarefree_factorial_semiring'') (auto simp: prime_multiplicity_squarefree_part_le_Suc_0) lemma squarefree_decomposition_unique: assumes "square_part m = square_part n" assumes "squarefree_part m = squarefree_part n" shows "m = n" by (subst (1 2) squarefree_decompose) (simp_all add: assms) lemma normalize_square_part [simp]: "normalize (square_part x) = square_part x" by (simp add: square_part_def) lemma square_part_even_power': "square_part (x ^ (2 * n)) = normalize (x ^ n)" proof (cases "x = 0") case False have "normalize (square_part (x ^ (2 * n))) = normalize (x ^ n)" using False by (intro multiplicity_eq_imp_eq) (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_power_distrib) thus ?thesis by simp qed (auto simp: power_0_left) lemma square_part_even_power: "even n ⟹ square_part (x ^ n) = normalize (x ^ (n div 2))" by (subst square_part_even_power' [symmetric]) auto lemma square_part_odd_power': "square_part (x ^ (Suc (2 * n))) = normalize (x ^ n * square_part x)" proof (cases "x = 0") case False have "normalize (square_part (x ^ (Suc (2 * n)))) = normalize (square_part x * x ^ n)" proof (rule multiplicity_eq_imp_eq, goal_cases) case (3 p) hence "multiplicity p (square_part (x ^ Suc (2 * n))) = (2 * (n * multiplicity p x) + multiplicity p x) div 2" by (subst prime_multiplicity_square_part) (auto simp: False prime_elem_multiplicity_power_distrib algebra_simps simp del: power_Suc) also from 3 False have "… = multiplicity p (square_part x * x ^ n)" by (subst div_mult_self4) (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_mult_distrib prime_elem_multiplicity_power_distrib) finally show ?case . qed (insert False, auto) thus ?thesis by (simp add: mult_ac) qed auto lemma square_part_odd_power: "odd n ⟹ square_part (x ^ n) = normalize (x ^ (n div 2) * square_part x)" by (subst square_part_odd_power' [symmetric]) auto end