equal
deleted
inserted
replaced
42 apply simp |
42 apply simp |
43 apply simp |
43 apply simp |
44 done |
44 done |
45 |
45 |
46 lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))" |
46 lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))" |
47 by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps) |
47 by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps) |
48 |
48 |
49 lemma not_prime_ex_mk: |
49 lemma not_prime_ex_mk: |
50 assumes n: "Suc 0 < n" |
50 assumes n: "Suc 0 < n" |
51 shows "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n" |
51 shows "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n" |
52 proof - |
52 proof - |