# HG changeset patch # User eberlm # Date 1470671271 -7200 # Node ID 2accfb71e33bc1d5cc7442b6deba217479d49768 # Parent 6ddb43c6b711e362ae3bdabee396d9fe272c3365 is_prime -> prime diff -r 6ddb43c6b711 -r 2accfb71e33b src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Mon Aug 08 14:13:14 2016 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Mon Aug 08 17:47:51 2016 +0200 @@ -2250,7 +2250,7 @@ subsection \Irreducible Elements are Prime\ -lemma (in factorial_monoid) irreducible_is_prime: +lemma (in factorial_monoid) irreducible_prime: assumes pirr: "irreducible G p" and pcarr: "p \ carrier G" shows "prime G p" @@ -2340,7 +2340,7 @@ \"A version using @{const factors}, more complicated" -lemma (in factorial_monoid) factors_irreducible_is_prime: +lemma (in factorial_monoid) factors_irreducible_prime: assumes pirr: "irreducible G p" and pcarr: "p \ carrier G" shows "prime G p" @@ -3638,7 +3638,7 @@ done sublocale factorial_monoid \ primeness_condition_monoid - by standard (rule irreducible_is_prime) + by standard (rule irreducible_prime) lemma (in factorial_monoid) primeness_condition: diff -r 6ddb43c6b711 -r 2accfb71e33b src/HOL/Algebra/Exponent.thy --- a/src/HOL/Algebra/Exponent.thy Mon Aug 08 14:13:14 2016 +0200 +++ b/src/HOL/Algebra/Exponent.thy Mon Aug 08 17:47:51 2016 +0200 @@ -15,8 +15,8 @@ text\needed in this form to prove Sylow's theorem\ corollary (in algebraic_semidom) div_combine: - "\is_prime_elem p; \ p ^ Suc r dvd n; p ^ (a + r) dvd n * k\ \ p ^ a dvd k" - by (metis add_Suc_right mult.commute prime_power_dvd_cases) + "\prime_elem p; \ p ^ Suc r dvd n; p ^ (a + r) dvd n * k\ \ p ^ a dvd k" + by (metis add_Suc_right mult.commute prime_elem_power_dvd_cases) lemma exponent_p_a_m_k_equation: fixes p :: nat @@ -61,16 +61,16 @@ case (Suc k) then have *: "(Suc (j+k) choose Suc k) > 0" by simp then have "multiplicity p ((Suc (j+k) choose Suc k) * Suc k) = multiplicity p (Suc k)" - by (subst Suc_times_binomial_eq [symmetric], subst prime_multiplicity_mult_distrib) + by (subst Suc_times_binomial_eq [symmetric], subst prime_elem_multiplicity_mult_distrib) (insert p Suc.prems, simp_all add: eeq [symmetric] Suc.IH) with p * show ?case - by (subst (asm) prime_multiplicity_mult_distrib) simp_all + by (subst (asm) prime_elem_multiplicity_mult_distrib) simp_all qed text\The lemma above, with two changes of variables\ lemma p_not_div_choose: assumes "k < K" and "k \ n" - and eeq: "\j. \0 \ multiplicity p (n - k + (K - j)) = multiplicity p (K - j)" "is_prime p" + and eeq: "\j. \0 \ multiplicity p (n - k + (K - j)) = multiplicity p (K - j)" "prime p" shows "multiplicity p (n choose k) = 0" apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1]) apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff) @@ -78,7 +78,7 @@ done proposition const_p_fac: - assumes "m>0" and prime: "is_prime p" + assumes "m>0" and prime: "prime p" shows "multiplicity p (p^a * m choose p^a) = multiplicity p m" proof- from assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \ p^a * m" @@ -93,13 +93,13 @@ by (subst times_binomial_minus1_eq [symmetric]) (auto simp: prime_gt_0_nat) also from p have "p ^ a - Suc 0 \ p ^ a * m - Suc 0" by linarith with prime * p have "multiplicity p ?rhs = multiplicity p (p ^ a * m)" - by (subst prime_multiplicity_mult_distrib) auto + by (subst prime_elem_multiplicity_mult_distrib) auto also have "\ = a + multiplicity p m" - using prime p by (subst prime_multiplicity_mult_distrib) simp_all + using prime p by (subst prime_elem_multiplicity_mult_distrib) simp_all finally show ?thesis . qed then show ?thesis - using prime p by (subst (asm) prime_multiplicity_mult_distrib) simp_all + using prime p by (subst (asm) prime_elem_multiplicity_mult_distrib) simp_all qed end diff -r 6ddb43c6b711 -r 2accfb71e33b src/HOL/Algebra/Ideal.thy --- a/src/HOL/Algebra/Ideal.thy Mon Aug 08 14:13:14 2016 +0200 +++ b/src/HOL/Algebra/Ideal.thy Mon Aug 08 17:47:51 2016 +0200 @@ -99,7 +99,7 @@ assumes I_notcarr: "carrier R \ I" and I_prime: "\a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ I" -lemma (in primeideal) is_primeideal: "primeideal I R" +lemma (in primeideal) primeideal: "primeideal I R" by (rule primeideal_axioms) lemma primeidealI: @@ -769,7 +769,7 @@ qed text \In a cring every maximal ideal is prime\ -lemma (in cring) maximalideal_is_prime: +lemma (in cring) maximalideal_prime: assumes "maximalideal I R" shows "primeideal I R" proof - diff -r 6ddb43c6b711 -r 2accfb71e33b src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Mon Aug 08 14:13:14 2016 +0200 +++ b/src/HOL/Algebra/IntRing.thy Mon Aug 08 17:47:51 2016 +0200 @@ -251,7 +251,7 @@ then obtain x where "1 = x * p" by best then have "\p * x\ = 1" by (simp add: mult.commute) then show False using prime - by (auto dest!: abs_zmult_eq_1 simp: is_prime_def) + by (auto dest!: abs_zmult_eq_1 simp: prime_def) qed diff -r 6ddb43c6b711 -r 2accfb71e33b src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy --- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Mon Aug 08 14:13:14 2016 +0200 +++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Mon Aug 08 17:47:51 2016 +0200 @@ -67,7 +67,7 @@ (* Goldblatt: Exercise 5.11(3a) - p 57 *) lemma starprime: "starprime = {p. 1 < p & (\m. m dvd p --> m = 1 | m = p)}" -by (transfer, auto simp add: is_prime_nat_iff) +by (transfer, auto simp add: prime_nat_iff) (* Goldblatt Exercise 5.11(3b) - p 57 *) lemma hyperprime_factor_exists [rule_format]: @@ -277,7 +277,7 @@ apply (subgoal_tac "k \ hypnat_of_nat ` {p. prime p}") apply (force simp add: starprime_def) apply (metis Compl_iff add.commute dvd_add_left_iff empty_iff hdvd_one_eq_one hypnat_one_not_prime - imageE insert_iff mem_Collect_eq not_is_prime_0) + imageE insert_iff mem_Collect_eq not_prime_0) done end diff -r 6ddb43c6b711 -r 2accfb71e33b src/HOL/Number_Theory/Eratosthenes.thy --- a/src/HOL/Number_Theory/Eratosthenes.thy Mon Aug 08 14:13:14 2016 +0200 +++ b/src/HOL/Number_Theory/Eratosthenes.thy Mon Aug 08 17:47:51 2016 +0200 @@ -295,8 +295,8 @@ from 2 show ?thesis apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto dest: prime_gt_Suc_0_nat) - apply (metis One_nat_def Suc_le_eq less_not_refl is_prime_nat_iff) - apply (metis One_nat_def Suc_le_eq aux is_prime_nat_iff) + apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_iff) + apply (metis One_nat_def Suc_le_eq aux prime_nat_iff) done qed qed diff -r 6ddb43c6b711 -r 2accfb71e33b src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Mon Aug 08 14:13:14 2016 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Mon Aug 08 17:47:51 2016 +0200 @@ -411,7 +411,7 @@ interpret semiring_gcd 1 0 "op *" gcd_eucl lcm_eucl "op div" "op +" "op -" normalize unit_factor by standard (rule lcm_gcd_eucl_facts; assumption)+ fix p assume p: "irreducible p" - thus "is_prime_elem p" by (rule irreducible_imp_prime_gcd) + thus "prime_elem p" by (rule irreducible_imp_prime_elem_gcd) qed lemma gcd_eucl_eq_gcd_factorial: "gcd_eucl = gcd_factorial" diff -r 6ddb43c6b711 -r 2accfb71e33b src/HOL/Number_Theory/Factorial_Ring.thy --- a/src/HOL/Number_Theory/Factorial_Ring.thy Mon Aug 08 14:13:14 2016 +0200 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy Mon Aug 08 17:47:51 2016 +0200 @@ -54,51 +54,51 @@ lemma irreducibleD: "irreducible p \ p = a * b \ a dvd 1 \ b dvd 1" by (simp add: irreducible_def) -definition is_prime_elem :: "'a \ bool" where - "is_prime_elem p \ p \ 0 \ \p dvd 1 \ (\a b. p dvd (a * b) \ p dvd a \ p dvd b)" +definition prime_elem :: "'a \ bool" where + "prime_elem p \ p \ 0 \ \p dvd 1 \ (\a b. p dvd (a * b) \ p dvd a \ p dvd b)" -lemma not_is_prime_elem_zero [simp]: "\is_prime_elem 0" - by (simp add: is_prime_elem_def) +lemma not_prime_elem_zero [simp]: "\prime_elem 0" + by (simp add: prime_elem_def) -lemma is_prime_elem_not_unit: "is_prime_elem p \ \p dvd 1" - by (simp add: is_prime_elem_def) +lemma prime_elem_not_unit: "prime_elem p \ \p dvd 1" + by (simp add: prime_elem_def) -lemma is_prime_elemI: - "p \ 0 \ \p dvd 1 \ (\a b. p dvd (a * b) \ p dvd a \ p dvd b) \ is_prime_elem p" - by (simp add: is_prime_elem_def) +lemma prime_elemI: + "p \ 0 \ \p dvd 1 \ (\a b. p dvd (a * b) \ p dvd a \ p dvd b) \ prime_elem p" + by (simp add: prime_elem_def) -lemma prime_divides_productD: - "is_prime_elem p \ p dvd (a * b) \ p dvd a \ p dvd b" - by (simp add: is_prime_elem_def) +lemma prime_elem_dvd_multD: + "prime_elem p \ p dvd (a * b) \ p dvd a \ p dvd b" + by (simp add: prime_elem_def) -lemma prime_dvd_mult_iff: - "is_prime_elem p \ p dvd (a * b) \ p dvd a \ p dvd b" - by (auto simp: is_prime_elem_def) +lemma prime_elem_dvd_mult_iff: + "prime_elem p \ p dvd (a * b) \ p dvd a \ p dvd b" + by (auto simp: prime_elem_def) -lemma not_is_prime_elem_one [simp]: - "\ is_prime_elem 1" - by (auto dest: is_prime_elem_not_unit) +lemma not_prime_elem_one [simp]: + "\ prime_elem 1" + by (auto dest: prime_elem_not_unit) -lemma is_prime_elem_not_zeroI: - assumes "is_prime_elem p" +lemma prime_elem_not_zeroI: + assumes "prime_elem p" shows "p \ 0" using assms by (auto intro: ccontr) -lemma is_prime_elem_dvd_power: - "is_prime_elem p \ p dvd x ^ n \ p dvd x" - by (induction n) (auto dest: prime_divides_productD intro: dvd_trans[of _ 1]) +lemma prime_elem_dvd_power: + "prime_elem p \ p dvd x ^ n \ p dvd x" + by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1]) -lemma is_prime_elem_dvd_power_iff: - "is_prime_elem p \ n > 0 \ p dvd x ^ n \ p dvd x" - by (auto dest: is_prime_elem_dvd_power intro: dvd_trans) +lemma prime_elem_dvd_power_iff: + "prime_elem p \ n > 0 \ p dvd x ^ n \ p dvd x" + by (auto dest: prime_elem_dvd_power intro: dvd_trans) -lemma is_prime_elem_imp_nonzero [simp]: - "ASSUMPTION (is_prime_elem x) \ x \ 0" - unfolding ASSUMPTION_def by (rule is_prime_elem_not_zeroI) +lemma prime_elem_imp_nonzero [simp]: + "ASSUMPTION (prime_elem x) \ x \ 0" + unfolding ASSUMPTION_def by (rule prime_elem_not_zeroI) -lemma is_prime_elem_imp_not_one [simp]: - "ASSUMPTION (is_prime_elem x) \ x \ 1" +lemma prime_elem_imp_not_one [simp]: + "ASSUMPTION (prime_elem x) \ x \ 1" unfolding ASSUMPTION_def by auto end @@ -110,42 +110,42 @@ lemma mult_unit_dvd_iff': "is_unit a \ (a * b) dvd c \ b dvd c" by (subst mult.commute) (rule mult_unit_dvd_iff) -lemma prime_imp_irreducible: - assumes "is_prime_elem p" +lemma prime_elem_imp_irreducible: + assumes "prime_elem p" shows "irreducible p" proof (rule irreducibleI) fix a b assume p_eq: "p = a * b" with assms have nz: "a \ 0" "b \ 0" by auto from p_eq have "p dvd a * b" by simp - with \is_prime_elem p\ have "p dvd a \ p dvd b" by (rule prime_divides_productD) + with \prime_elem p\ have "p dvd a \ p dvd b" by (rule prime_elem_dvd_multD) with \p = a * b\ have "a * b dvd 1 * b \ a * b dvd a * 1" by auto thus "a dvd 1 \ b dvd 1" by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)]) -qed (insert assms, simp_all add: is_prime_elem_def) +qed (insert assms, simp_all add: prime_elem_def) -lemma is_prime_elem_mono: - assumes "is_prime_elem p" "\q dvd 1" "q dvd p" - shows "is_prime_elem q" +lemma prime_elem_mono: + assumes "prime_elem p" "\q dvd 1" "q dvd p" + shows "prime_elem q" proof - from \q dvd p\ obtain r where r: "p = q * r" by (elim dvdE) hence "p dvd q * r" by simp - with \is_prime_elem p\ have "p dvd q \ p dvd r" by (rule prime_divides_productD) + with \prime_elem p\ have "p dvd q \ p dvd r" by (rule prime_elem_dvd_multD) hence "p dvd q" proof assume "p dvd r" then obtain s where s: "r = p * s" by (elim dvdE) from r have "p * 1 = p * (q * s)" by (subst (asm) s) (simp add: mult_ac) - with \is_prime_elem p\ have "q dvd 1" + with \prime_elem p\ have "q dvd 1" by (subst (asm) mult_cancel_left) auto with \\q dvd 1\ show ?thesis by contradiction qed show ?thesis - proof (rule is_prime_elemI) + proof (rule prime_elemI) fix a b assume "q dvd (a * b)" with \p dvd q\ have "p dvd (a * b)" by (rule dvd_trans) - with \is_prime_elem p\ have "p dvd a \ p dvd b" by (rule prime_divides_productD) + with \prime_elem p\ have "p dvd a \ p dvd b" by (rule prime_elem_dvd_multD) with \q dvd p\ show "q dvd a \ q dvd b" by (blast intro: dvd_trans) qed (insert assms, auto) qed @@ -178,12 +178,12 @@ "irreducible x \ x \ 0 \ \is_unit x \ (\b. b dvd x \ x dvd b \ is_unit b)" using irreducibleI'[of x] irreducibleD'[of x] irreducible_not_unit[of x] by auto -lemma is_prime_elem_multD: - assumes "is_prime_elem (a * b)" +lemma prime_elem_multD: + assumes "prime_elem (a * b)" shows "is_unit a \ is_unit b" proof - - from assms have "a \ 0" "b \ 0" by (auto dest!: is_prime_elem_not_zeroI) - moreover from assms prime_divides_productD [of "a * b"] have "a * b dvd a \ a * b dvd b" + from assms have "a \ 0" "b \ 0" by (auto dest!: prime_elem_not_zeroI) + moreover from assms prime_elem_dvd_multD [of "a * b"] have "a * b dvd a \ a * b dvd b" by auto ultimately show ?thesis using dvd_times_left_cancel_iff [of a b 1] @@ -191,36 +191,62 @@ by auto qed -lemma is_prime_elemD2: - assumes "is_prime_elem p" and "a dvd p" and "\ is_unit a" +lemma prime_elemD2: + assumes "prime_elem p" and "a dvd p" and "\ is_unit a" shows "p dvd a" proof - from \a dvd p\ obtain b where "p = a * b" .. - with \is_prime_elem p\ is_prime_elem_multD \\ is_unit a\ have "is_unit b" by auto + with \prime_elem p\ prime_elem_multD \\ is_unit a\ have "is_unit b" by auto with \p = a * b\ show ?thesis by (auto simp add: mult_unit_dvd_iff) qed +lemma prime_elem_dvd_msetprodE: + assumes "prime_elem p" + assumes dvd: "p dvd msetprod A" + obtains a where "a \# A" and "p dvd a" +proof - + from dvd have "\a. a \# A \ p dvd a" + proof (induct A) + case empty then show ?case + using \prime_elem p\ by (simp add: prime_elem_not_unit) + next + case (add A a) + then have "p dvd msetprod A * a" by simp + with \prime_elem p\ consider (A) "p dvd msetprod A" | (B) "p dvd a" + by (blast dest: prime_elem_dvd_multD) + then show ?case proof cases + case B then show ?thesis by auto + next + case A + with add.hyps obtain b where "b \# A" "p dvd b" + by auto + then show ?thesis by auto + qed + qed + with that show thesis by blast +qed + context begin -private lemma is_prime_elem_powerD: - assumes "is_prime_elem (p ^ n)" - shows "is_prime_elem p \ n = 1" +private lemma prime_elem_powerD: + assumes "prime_elem (p ^ n)" + shows "prime_elem p \ n = 1" proof (cases n) case (Suc m) note assms also from Suc have "p ^ n = p * p^m" by simp - finally have "is_unit p \ is_unit (p^m)" by (rule is_prime_elem_multD) - moreover from assms have "\is_unit p" by (simp add: is_prime_elem_def is_unit_power_iff) + finally have "is_unit p \ is_unit (p^m)" by (rule prime_elem_multD) + moreover from assms have "\is_unit p" by (simp add: prime_elem_def is_unit_power_iff) ultimately have "is_unit (p ^ m)" by simp with \\is_unit p\ have "m = 0" by (simp add: is_unit_power_iff) with Suc assms show ?thesis by simp qed (insert assms, simp_all) -lemma is_prime_elem_power_iff: - "is_prime_elem (p ^ n) \ is_prime_elem p \ n = 1" - by (auto dest: is_prime_elem_powerD) +lemma prime_elem_power_iff: + "prime_elem (p ^ n) \ prime_elem p \ n = 1" + by (auto dest: prime_elem_powerD) end @@ -229,17 +255,17 @@ by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff dvd_mult_unit_iff) -lemma is_prime_elem_mult_unit_left: - "is_unit a \ is_prime_elem (a * p) \ is_prime_elem p" - by (auto simp: is_prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff) +lemma prime_elem_mult_unit_left: + "is_unit a \ prime_elem (a * p) \ prime_elem p" + by (auto simp: prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff) -lemma prime_dvd_cases: - assumes pk: "p*k dvd m*n" and p: "is_prime_elem p" +lemma prime_elem_dvd_cases: + assumes pk: "p*k dvd m*n" and p: "prime_elem p" shows "(\x. k dvd x*n \ m = p*x) \ (\y. k dvd m*y \ n = p*y)" proof - have "p dvd m*n" using dvd_mult_left pk by blast then consider "p dvd m" | "p dvd n" - using p prime_dvd_mult_iff by blast + using p prime_elem_dvd_mult_iff by blast then show ?thesis proof cases case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) @@ -254,8 +280,8 @@ qed qed -lemma prime_power_dvd_prod: - assumes pc: "p^c dvd m*n" and p: "is_prime_elem p" +lemma prime_elem_power_dvd_prod: + assumes pc: "p^c dvd m*n" and p: "prime_elem p" shows "\a b. a+b = c \ p^a dvd m \ p^b dvd n" using pc proof (induct c arbitrary: m n) @@ -263,7 +289,7 @@ next case (Suc c) consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y" - using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force + using prime_elem_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force then show ?case proof cases case (1 x) @@ -284,217 +310,40 @@ lemma add_eq_Suc_lem: "a+b = Suc (x+y) \ a \ x \ b \ y" by arith -lemma prime_power_dvd_cases: - "\p^c dvd m * n; a + b = Suc c; is_prime_elem p\ \ p ^ a dvd m \ p ^ b dvd n" - using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem) - -end - -context normalization_semidom -begin - -lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x" - using irreducible_mult_unit_left[of "1 div unit_factor x" x] - by (cases "x = 0") (simp_all add: unit_div_commute) - -lemma is_prime_elem_normalize_iff [simp]: "is_prime_elem (normalize x) = is_prime_elem x" - using is_prime_elem_mult_unit_left[of "1 div unit_factor x" x] - by (cases "x = 0") (simp_all add: unit_div_commute) - -definition is_prime :: "'a \ bool" where - "is_prime p \ is_prime_elem p \ normalize p = p" - -lemma not_is_prime_0 [simp]: "\is_prime 0" by (simp add: is_prime_def) - -lemma not_is_prime_unit: "is_unit x \ \is_prime x" - using is_prime_elem_not_unit[of x] by (auto simp add: is_prime_def) - -lemma not_is_prime_1 [simp]: "\is_prime 1" by (simp add: not_is_prime_unit) - -lemma is_primeI: "is_prime_elem x \ normalize x = x \ is_prime x" - by (simp add: is_prime_def) - -lemma prime_imp_prime_elem [dest]: "is_prime p \ is_prime_elem p" - by (simp add: is_prime_def) - -lemma normalize_is_prime: "is_prime p \ normalize p = p" - by (simp add: is_prime_def) - -lemma is_prime_normalize_iff [simp]: "is_prime (normalize p) \ is_prime_elem p" - by (auto simp add: is_prime_def) - -lemma is_prime_power_iff: - "is_prime (p ^ n) \ is_prime p \ n = 1" - by (auto simp: is_prime_def is_prime_elem_power_iff) - -lemma is_prime_elem_not_unit' [simp]: - "ASSUMPTION (is_prime_elem x) \ \is_unit x" - unfolding ASSUMPTION_def by (rule is_prime_elem_not_unit) - -lemma is_prime_imp_nonzero [simp]: - "ASSUMPTION (is_prime x) \ x \ 0" - unfolding ASSUMPTION_def is_prime_def by auto - -lemma is_prime_imp_not_one [simp]: - "ASSUMPTION (is_prime x) \ x \ 1" - unfolding ASSUMPTION_def by auto - -lemma is_prime_not_unit' [simp]: - "ASSUMPTION (is_prime x) \ \is_unit x" - unfolding ASSUMPTION_def is_prime_def by auto - -lemma is_prime_normalize' [simp]: "ASSUMPTION (is_prime x) \ normalize x = x" - unfolding ASSUMPTION_def is_prime_def by simp - -lemma unit_factor_is_prime: "is_prime x \ unit_factor x = 1" - using unit_factor_normalize[of x] unfolding is_prime_def by auto - -lemma unit_factor_is_prime' [simp]: "ASSUMPTION (is_prime x) \ unit_factor x = 1" - unfolding ASSUMPTION_def by (rule unit_factor_is_prime) - -lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (is_prime x) \ is_prime_elem x" - by (simp add: is_prime_def ASSUMPTION_def) - - lemma is_prime_elem_associated: - assumes "is_prime_elem p" and "is_prime_elem q" and "q dvd p" - shows "normalize q = normalize p" -using \q dvd p\ proof (rule associatedI) - from \is_prime_elem q\ have "\ is_unit q" - by (simp add: is_prime_elem_not_unit) - with \is_prime_elem p\ \q dvd p\ show "p dvd q" - by (blast intro: is_prime_elemD2) -qed - -lemma is_prime_dvd_multD: "is_prime p \ p dvd a * b \ p dvd a \ p dvd b" - by (intro prime_divides_productD) simp_all - -lemma is_prime_dvd_mult_iff [simp]: "is_prime p \ p dvd a * b \ p dvd a \ p dvd b" - by (auto dest: is_prime_dvd_multD) - -lemma is_prime_dvd_power: - "is_prime p \ p dvd x ^ n \ p dvd x" - by (auto dest!: is_prime_elem_dvd_power simp: is_prime_def) - -lemma is_prime_dvd_power_iff: - "is_prime p \ n > 0 \ p dvd x ^ n \ p dvd x" - by (intro is_prime_elem_dvd_power_iff) simp_all +lemma prime_elem_power_dvd_cases: + "\p^c dvd m * n; a + b = Suc c; prime_elem p\ \ p ^ a dvd m \ p ^ b dvd n" + using power_le_dvd by (blast dest: prime_elem_power_dvd_prod add_eq_Suc_lem) -lemma prime_dvd_msetprodE: - assumes "is_prime_elem p" - assumes dvd: "p dvd msetprod A" - obtains a where "a \# A" and "p dvd a" -proof - - from dvd have "\a. a \# A \ p dvd a" - proof (induct A) - case empty then show ?case - using \is_prime_elem p\ by (simp add: is_prime_elem_not_unit) - next - case (add A a) - then have "p dvd msetprod A * a" by simp - with \is_prime_elem p\ consider (A) "p dvd msetprod A" | (B) "p dvd a" - by (blast dest: prime_divides_productD) - then show ?case proof cases - case B then show ?thesis by auto - next - case A - with add.hyps obtain b where "b \# A" "p dvd b" - by auto - then show ?thesis by auto - qed - qed - with that show thesis by blast -qed - -lemma msetprod_subset_imp_dvd: - assumes "A \# B" - shows "msetprod A dvd msetprod B" -proof - - from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add) - also have "msetprod \ = msetprod (B - A) * msetprod A" by simp - also have "msetprod A dvd \" by simp - finally show ?thesis . -qed - -lemma prime_dvd_msetprod_iff: "is_prime p \ p dvd msetprod A \ (\x. x \# A \ p dvd x)" - by (induction A) (simp_all add: prime_dvd_mult_iff prime_imp_prime_elem, blast+) +lemma prime_elem_not_unit' [simp]: + "ASSUMPTION (prime_elem x) \ \is_unit x" + unfolding ASSUMPTION_def by (rule prime_elem_not_unit) -lemma primes_dvd_imp_eq: - assumes "is_prime p" "is_prime q" "p dvd q" - shows "p = q" -proof - - from assms have "irreducible q" by (simp add: prime_imp_irreducible is_prime_def) - from irreducibleD'[OF this \p dvd q\] assms have "q dvd p" by simp - with \p dvd q\ have "normalize p = normalize q" by (rule associatedI) - with assms show "p = q" by simp -qed - -lemma prime_dvd_msetprod_primes_iff: - assumes "is_prime p" "\q. q \# A \ is_prime q" - shows "p dvd msetprod A \ p \# A" -proof - - from assms(1) have "p dvd msetprod A \ (\x. x \# A \ p dvd x)" by (rule prime_dvd_msetprod_iff) - also from assms have "\ \ p \# A" by (auto dest: primes_dvd_imp_eq) - finally show ?thesis . -qed - -lemma msetprod_primes_dvd_imp_subset: - assumes "msetprod A dvd msetprod B" "\p. p \# A \ is_prime p" "\p. p \# B \ is_prime p" - shows "A \# B" -using assms -proof (induction A arbitrary: B) - case empty - thus ?case by simp -next - case (add A p B) - hence p: "is_prime p" by simp - define B' where "B' = B - {#p#}" - from add.prems have "p dvd msetprod B" by (simp add: dvd_mult_right) - with add.prems have "p \# B" - by (subst (asm) (2) prime_dvd_msetprod_primes_iff) simp_all - hence B: "B = B' + {#p#}" by (simp add: B'_def) - from add.prems p have "A \# B'" by (intro add.IH) (simp_all add: B) - thus ?case by (simp add: B) -qed - -lemma normalize_msetprod_primes: - "(\p. p \# A \ is_prime p) \ normalize (msetprod A) = msetprod A" -proof (induction A) - case (add A p) - hence "is_prime p" by simp - hence "normalize p = p" by simp - with add show ?case by (simp add: normalize_mult) -qed simp_all - -lemma msetprod_dvd_msetprod_primes_iff: - assumes "\x. x \# A \ is_prime x" "\x. x \# B \ is_prime x" - shows "msetprod A dvd msetprod B \ A \# B" - using assms by (auto intro: msetprod_subset_imp_dvd msetprod_primes_dvd_imp_subset) - -lemma prime_dvd_power_iff: - assumes "is_prime_elem p" +lemma prime_elem_dvd_power_iff: + assumes "prime_elem p" shows "p dvd a ^ n \ p dvd a \ n > 0" - using assms by (induct n) (auto dest: is_prime_elem_not_unit prime_divides_productD) + using assms by (induct n) (auto dest: prime_elem_not_unit prime_elem_dvd_multD) lemma prime_power_dvd_multD: - assumes "is_prime_elem p" + assumes "prime_elem p" assumes "p ^ n dvd a * b" and "n > 0" and "\ p dvd a" shows "p ^ n dvd b" -using \p ^ n dvd a * b\ and \n > 0\ proof (induct n arbitrary: b) + using \p ^ n dvd a * b\ and \n > 0\ +proof (induct n arbitrary: b) case 0 then show ?case by simp next case (Suc n) show ?case proof (cases "n = 0") - case True with Suc \is_prime_elem p\ \\ p dvd a\ show ?thesis - by (simp add: prime_dvd_mult_iff) + case True with Suc \prime_elem p\ \\ p dvd a\ show ?thesis + by (simp add: prime_elem_dvd_mult_iff) next case False then have "n > 0" by simp - from \is_prime_elem p\ have "p \ 0" by auto + from \prime_elem p\ have "p \ 0" by auto from Suc.prems have *: "p * p ^ n dvd a * b" by simp then have "p dvd a * b" by (rule dvd_mult_left) - with Suc \is_prime_elem p\ \\ p dvd a\ have "p dvd b" - by (simp add: prime_dvd_mult_iff) + with Suc \prime_elem p\ \\ p dvd a\ have "p dvd b" + by (simp add: prime_elem_dvd_mult_iff) moreover define c where "c = b div p" ultimately have b: "b = p * c" by simp with * have "p * p ^ n dvd p * (a * c)" @@ -508,6 +357,158 @@ qed qed +end + +context normalization_semidom +begin + +lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x" + using irreducible_mult_unit_left[of "1 div unit_factor x" x] + by (cases "x = 0") (simp_all add: unit_div_commute) + +lemma prime_elem_normalize_iff [simp]: "prime_elem (normalize x) = prime_elem x" + using prime_elem_mult_unit_left[of "1 div unit_factor x" x] + by (cases "x = 0") (simp_all add: unit_div_commute) + +lemma prime_elem_associated: + assumes "prime_elem p" and "prime_elem q" and "q dvd p" + shows "normalize q = normalize p" +using \q dvd p\ proof (rule associatedI) + from \prime_elem q\ have "\ is_unit q" + by (auto simp add: prime_elem_not_unit) + with \prime_elem p\ \q dvd p\ show "p dvd q" + by (blast intro: prime_elemD2) +qed + +definition prime :: "'a \ bool" where + "prime p \ prime_elem p \ normalize p = p" + +lemma not_prime_0 [simp]: "\prime 0" by (simp add: prime_def) + +lemma not_prime_unit: "is_unit x \ \prime x" + using prime_elem_not_unit[of x] by (auto simp add: prime_def) + +lemma not_prime_1 [simp]: "\prime 1" by (simp add: not_prime_unit) + +lemma primeI: "prime_elem x \ normalize x = x \ prime x" + by (simp add: prime_def) + +lemma prime_imp_prime_elem [dest]: "prime p \