|
8745
|
1 |
(*<*)
|
|
|
2 |
theory prime_def = Main:;
|
|
|
3 |
consts prime :: "nat \\<Rightarrow> bool"
|
|
|
4 |
(*>*)
|
|
|
5 |
(*<*)term(*>*)
|
|
|
6 |
|
|
|
7 |
"prime(p) \\<equiv> 1 < p \\<and> ((m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))";
|
|
|
8 |
text{*\noindent\small
|
|
|
9 |
where \isa{dvd} means ``divides''.
|
|
|
10 |
Isabelle rejects this ``definition'' because of the extra \isa{m} on the
|
|
|
11 |
right-hand side, which would introduce an inconsistency. (Why?) What you
|
|
|
12 |
should have written is
|
|
|
13 |
*}
|
|
|
14 |
(*<*)term(*>*)
|
|
|
15 |
"prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. (m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))"
|
|
|
16 |
(*<*)
|
|
|
17 |
end
|
|
|
18 |
(*>*)
|