equal
deleted
inserted
replaced
293 \<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m \<Longrightarrow> |
293 \<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m \<Longrightarrow> |
294 m dvd q \<Longrightarrow> m \<noteq> q \<Longrightarrow> m = 1" by auto |
294 m dvd q \<Longrightarrow> m \<noteq> q \<Longrightarrow> m = 1" by auto |
295 from 2 show ?thesis |
295 from 2 show ?thesis |
296 apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto |
296 apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto |
297 dest: prime_gt_Suc_0_nat) |
297 dest: prime_gt_Suc_0_nat) |
298 apply (metis One_nat_def Suc_le_eq less_not_refl prime_def) |
298 apply (metis One_nat_def Suc_le_eq less_not_refl is_prime_nat_iff) |
299 apply (metis One_nat_def Suc_le_eq aux prime_def) |
299 apply (metis One_nat_def Suc_le_eq aux is_prime_nat_iff) |
300 done |
300 done |
301 qed |
301 qed |
302 qed |
302 qed |
303 |
303 |
304 lemma primes_upto_sieve [code]: |
304 lemma primes_upto_sieve [code]: |