|
8745
|
1 |
(*<*)
|
|
58860
|
2 |
theory prime_def imports Main begin
|
|
11457
|
3 |
consts prime :: "nat \<Rightarrow> bool"
|
|
8745
|
4 |
(*>*)
|
|
9844
|
5 |
text{*
|
|
|
6 |
\begin{warn}
|
|
|
7 |
A common mistake when writing definitions is to introduce extra free
|
|
11456
|
8 |
variables on the right-hand side. Consider the following, flawed definition
|
|
|
9 |
(where @{text"dvd"} means ``divides''):
|
|
9844
|
10 |
@{term[display,quotes]"prime(p) == 1 < p & (m dvd p --> (m=1 | m=p))"}
|
|
11457
|
11 |
\par\noindent\hangindent=0pt
|
|
9792
|
12 |
Isabelle rejects this ``definition'' because of the extra @{term"m"} on the
|
|
11456
|
13 |
right-hand side, which would introduce an inconsistency (why?).
|
|
|
14 |
The correct version is
|
|
9844
|
15 |
@{term[display,quotes]"prime(p) == 1 < p & (!m. m dvd p --> (m=1 | m=p))"}
|
|
|
16 |
\end{warn}
|
|
8745
|
17 |
*}
|
|
|
18 |
(*<*)
|
|
|
19 |
end
|
|
|
20 |
(*>*)
|