equal
deleted
inserted
replaced
151 |
151 |
152 lemma all_prime_nempty_g_one: |
152 lemma all_prime_nempty_g_one: |
153 assumes "all_prime ps" and "ps \<noteq> []" |
153 assumes "all_prime ps" and "ps \<noteq> []" |
154 shows "Suc 0 < (PROD m\<Colon>nat:#multiset_of ps. m)" |
154 shows "Suc 0 < (PROD m\<Colon>nat:#multiset_of ps. m)" |
155 using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct) |
155 using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct) |
156 (simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def) |
156 (simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def) |
157 |
157 |
158 lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = n)" |
158 lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = n)" |
159 proof (induct n rule: nat_wf_ind) |
159 proof (induct n rule: nat_wf_ind) |
160 case (1 n) |
160 case (1 n) |
161 from `Suc 0 < n` |
161 from `Suc 0 < n` |