equal
deleted
inserted
replaced
580 shows "\<exists>b. b dvd a \<and> is_prime b" |
580 shows "\<exists>b. b dvd a \<and> is_prime b" |
581 proof - |
581 proof - |
582 from prime_factorization_exists'[OF assms(1)] guess A . note A = this |
582 from prime_factorization_exists'[OF assms(1)] guess A . note A = this |
583 moreover from A and assms have "A \<noteq> {#}" by auto |
583 moreover from A and assms have "A \<noteq> {#}" by auto |
584 then obtain x where "x \<in># A" by blast |
584 then obtain x where "x \<in># A" by blast |
585 with A(1) have "x dvd msetprod A" "is_prime x" by (auto simp: dvd_msetprod) |
585 with A(1) have *: "x dvd msetprod A" "is_prime x" by (auto simp: dvd_msetprod) |
586 moreover from this A have "x dvd a" by simp |
586 with A have "x dvd a" by simp |
587 ultimately show ?thesis by blast |
587 with * show ?thesis by blast |
588 qed |
588 qed |
589 |
589 |
590 lemma prime_divisors_induct [case_names zero unit factor]: |
590 lemma prime_divisors_induct [case_names zero unit factor]: |
591 assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. is_prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)" |
591 assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. is_prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)" |
592 shows "P x" |
592 shows "P x" |