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