404 lemma prime_0[simp]: "~prime 0" by (simp add: prime_def) |
404 lemma prime_0[simp]: "~prime 0" by (simp add: prime_def) |
405 lemma prime_1[simp]: "~ prime 1" by (simp add: prime_def) |
405 lemma prime_1[simp]: "~ prime 1" by (simp add: prime_def) |
406 lemma prime_Suc0[simp]: "~ prime (Suc 0)" by (simp add: prime_def) |
406 lemma prime_Suc0[simp]: "~ prime (Suc 0)" by (simp add: prime_def) |
407 |
407 |
408 lemma prime_ge_2: "prime p ==> p \<ge> 2" by (simp add: prime_def) |
408 lemma prime_ge_2: "prime p ==> p \<ge> 2" by (simp add: prime_def) |
409 lemma prime_factor: assumes n: "n \<noteq> 1" shows "\<exists> p. prime p \<and> p dvd n" |
409 |
410 using n |
410 lemma prime_factor: "n \<noteq> 1 \<Longrightarrow> \<exists>p. prime p \<and> p dvd n" |
411 proof(induct n rule: nat_less_induct) |
411 proof (induct n rule: nat_less_induct) |
412 fix n |
412 fix n |
413 assume H: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)" "n \<noteq> 1" |
413 assume H: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)" "n \<noteq> 1" |
414 let ?ths = "\<exists>p. prime p \<and> p dvd n" |
414 show "\<exists>p. prime p \<and> p dvd n" |
415 {assume "n=0" hence ?ths using two_is_prime by auto} |
415 proof (cases "n = 0") |
416 moreover |
416 case True |
417 {assume nz: "n\<noteq>0" |
417 with two_is_prime show ?thesis by auto |
418 {assume "prime n" hence ?ths by - (rule exI[where x="n"], simp)} |
418 next |
419 moreover |
419 case nz: False |
420 {assume n: "\<not> prime n" |
420 show ?thesis |
421 with nz H(2) |
421 proof (cases "prime n") |
422 obtain k where k:"k dvd n" "k \<noteq> 1" "k \<noteq> n" by (auto simp add: prime_def) |
422 case True |
|
423 then have "prime n \<and> n dvd n" by simp |
|
424 then show ?thesis .. |
|
425 next |
|
426 case n: False |
|
427 with nz H(2) obtain k where k: "k dvd n" "k \<noteq> 1" "k \<noteq> n" |
|
428 by (auto simp: prime_def) |
423 from dvd_imp_le[OF k(1)] nz k(3) have kn: "k < n" by simp |
429 from dvd_imp_le[OF k(1)] nz k(3) have kn: "k < n" by simp |
424 from H(1)[rule_format, OF kn k(2)] obtain p where p: "prime p" "p dvd k" by blast |
430 from H(1)[rule_format, OF kn k(2)] obtain p where p: "prime p" "p dvd k" by blast |
425 from dvd_trans[OF p(2) k(1)] p(1) have ?ths by blast} |
431 from dvd_trans[OF p(2) k(1)] p(1) show ?thesis by blast |
426 ultimately have ?ths by blast} |
432 qed |
427 ultimately show ?ths by blast |
433 qed |
428 qed |
434 qed |
429 |
435 |
430 lemma prime_factor_lt: assumes p: "prime p" and n: "n \<noteq> 0" and npm:"n = p * m" |
436 lemma prime_factor_lt: |
|
437 assumes p: "prime p" and n: "n \<noteq> 0" and npm:"n = p * m" |
431 shows "m < n" |
438 shows "m < n" |
432 proof- |
439 proof (cases "m = 0") |
433 {assume "m=0" with n have ?thesis by simp} |
440 case True |
434 moreover |
441 with n show ?thesis by simp |
435 {assume m: "m \<noteq> 0" |
442 next |
436 from npm have mn: "m dvd n" unfolding dvd_def by auto |
443 case m: False |
437 from npm m have "n \<noteq> m" using p by auto |
444 from npm have mn: "m dvd n" unfolding dvd_def by auto |
438 with dvd_imp_le[OF mn] n have ?thesis by simp} |
445 from npm m have "n \<noteq> m" using p by auto |
439 ultimately show ?thesis by blast |
446 with dvd_imp_le[OF mn] n show ?thesis by simp |
440 qed |
447 qed |
441 |
448 |
442 lemma euclid_bound: "\<exists>p. prime p \<and> n < p \<and> p <= Suc (fact n)" |
449 lemma euclid_bound: "\<exists>p. prime p \<and> n < p \<and> p <= Suc (fact n)" |
443 proof- |
450 proof- |
444 have f1: "fact n + 1 \<noteq> 1" using fact_le[of n] by arith |
451 have f1: "fact n + 1 \<noteq> 1" using fact_le[of n] by arith |
489 |
496 |
490 lemma coprime_0'[simp]: "coprime 0 d \<longleftrightarrow> d = 1" by (simp add: coprime_commute[of 0 d]) |
497 lemma coprime_0'[simp]: "coprime 0 d \<longleftrightarrow> d = 1" by (simp add: coprime_commute[of 0 d]) |
491 lemma coprime_bezout_strong: assumes ab: "coprime a b" and b: "b \<noteq> 1" |
498 lemma coprime_bezout_strong: assumes ab: "coprime a b" and b: "b \<noteq> 1" |
492 shows "\<exists>x y. a * x = b * y + 1" |
499 shows "\<exists>x y. a * x = b * y + 1" |
493 proof- |
500 proof- |
494 from ab b have az: "a \<noteq> 0" by - (rule ccontr, auto) |
501 have az: "a \<noteq> 0" by (rule ccontr) (use ab b in auto) |
495 from bezout_gcd_strong[OF az, of b] ab[unfolded coprime_def] |
502 from bezout_gcd_strong[OF az, of b] ab[unfolded coprime_def] |
496 show ?thesis by auto |
503 show ?thesis by auto |
497 qed |
504 qed |
498 |
505 |
499 lemma bezout_prime: assumes p: "prime p" and pa: "\<not> p dvd a" |
506 lemma bezout_prime: assumes p: "prime p" and pa: "\<not> p dvd a" |
575 qed |
582 qed |
576 |
583 |
577 lemma distinct_prime_coprime: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q" |
584 lemma distinct_prime_coprime: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q" |
578 unfolding prime_def coprime_prime_eq by blast |
585 unfolding prime_def coprime_prime_eq by blast |
579 |
586 |
580 lemma prime_coprime_lt: assumes p: "prime p" and x: "0 < x" and xp: "x < p" |
587 lemma prime_coprime_lt: |
|
588 assumes p: "prime p" and x: "0 < x" and xp: "x < p" |
581 shows "coprime x p" |
589 shows "coprime x p" |
582 proof- |
590 proof (rule ccontr) |
583 {assume c: "\<not> coprime x p" |
591 assume c: "\<not> ?thesis" |
584 then obtain g where g: "g \<noteq> 1" "g dvd x" "g dvd p" unfolding coprime_def by blast |
592 then obtain g where g: "g \<noteq> 1" "g dvd x" "g dvd p" unfolding coprime_def by blast |
585 from dvd_imp_le[OF g(2)] x xp have gp: "g < p" by arith |
593 from dvd_imp_le[OF g(2)] x xp have gp: "g < p" by arith |
586 from g(2) x have "g \<noteq> 0" by - (rule ccontr, simp) |
594 have "g \<noteq> 0" by (rule ccontr) (use g(2) x in simp) |
587 with g gp p[unfolded prime_def] have False by blast} |
595 with g gp p[unfolded prime_def] show False by blast |
588 thus ?thesis by blast |
|
589 qed |
596 qed |
590 |
597 |
591 lemma prime_odd: "prime p \<Longrightarrow> p = 2 \<or> odd p" unfolding prime_def by auto |
598 lemma prime_odd: "prime p \<Longrightarrow> p = 2 \<or> odd p" unfolding prime_def by auto |
592 |
599 |
593 |
600 |
753 lemma prime_power_mult: |
760 lemma prime_power_mult: |
754 assumes p: "prime p" and xy: "x * y = p ^ k" |
761 assumes p: "prime p" and xy: "x * y = p ^ k" |
755 shows "\<exists>i j. x = p ^i \<and> y = p^ j" |
762 shows "\<exists>i j. x = p ^i \<and> y = p^ j" |
756 using xy |
763 using xy |
757 proof(induct k arbitrary: x y) |
764 proof(induct k arbitrary: x y) |
758 case 0 thus ?case apply simp by (rule exI[where x="0"], simp) |
765 case 0 |
|
766 thus ?case apply simp by (rule exI[where x="0"], simp) |
759 next |
767 next |
760 case (Suc k x y) |
768 case (Suc k x y) |
|
769 have p0: "p \<noteq> 0" by (rule ccontr) (use p in simp) |
761 from Suc.prems have pxy: "p dvd x*y" by auto |
770 from Suc.prems have pxy: "p dvd x*y" by auto |
762 from prime_divprod[OF p pxy] have pxyc: "p dvd x \<or> p dvd y" . |
771 from prime_divprod[OF p pxy] show ?case |
763 from p have p0: "p \<noteq> 0" by - (rule ccontr, simp) |
772 proof |
764 {assume px: "p dvd x" |
773 assume px: "p dvd x" |
765 then obtain d where d: "x = p*d" unfolding dvd_def by blast |
774 then obtain d where d: "x = p*d" unfolding dvd_def by blast |
766 from Suc.prems d have "p*d*y = p^Suc k" by simp |
775 from Suc.prems d have "p*d*y = p^Suc k" by simp |
767 hence th: "d*y = p^k" using p0 by simp |
776 hence th: "d*y = p^k" using p0 by simp |
768 from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast |
777 from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast |
769 with d have "x = p^Suc i" by simp |
778 with d have "x = p^Suc i" by simp |
770 with ij(2) have ?case by blast} |
779 with ij(2) show ?thesis by blast |
771 moreover |
780 next |
772 {assume px: "p dvd y" |
781 assume px: "p dvd y" |
773 then obtain d where d: "y = p*d" unfolding dvd_def by blast |
782 then obtain d where d: "y = p*d" unfolding dvd_def by blast |
774 from Suc.prems d have "p*d*x = p^Suc k" by (simp add: mult.commute) |
783 from Suc.prems d have "p*d*x = p^Suc k" by (simp add: mult.commute) |
775 hence th: "d*x = p^k" using p0 by simp |
784 hence th: "d*x = p^k" using p0 by simp |
776 from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast |
785 from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast |
777 with d have "y = p^Suc i" by simp |
786 with d have "y = p^Suc i" by simp |
778 with ij(2) have ?case by blast} |
787 with ij(2) show ?thesis by blast |
779 ultimately show ?case using pxyc by blast |
788 qed |
780 qed |
789 qed |
781 |
790 |
782 lemma prime_power_exp: assumes p: "prime p" and n:"n \<noteq> 0" |
791 lemma prime_power_exp: assumes p: "prime p" and n:"n \<noteq> 0" |
783 and xn: "x^n = p^k" shows "\<exists>i. x = p^i" |
792 and xn: "x^n = p^k" shows "\<exists>i. x = p^i" |
784 using n xn |
793 using n xn |