|
8745
|
1 |
(*<*)
|
|
|
2 |
theory prime_def = Main:;
|
|
|
3 |
consts prime :: "nat \\<Rightarrow> bool"
|
|
|
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))"}
|
|
9792
|
11 |
Isabelle rejects this ``definition'' because of the extra @{term"m"} on the
|
|
11456
|
12 |
right-hand side, which would introduce an inconsistency (why?).
|
|
|
13 |
The correct version is
|
|
9844
|
14 |
@{term[display,quotes]"prime(p) == 1 < p & (!m. m dvd p --> (m=1 | m=p))"}
|
|
|
15 |
\end{warn}
|
|
8745
|
16 |
*}
|
|
|
17 |
(*<*)
|
|
|
18 |
end
|
|
|
19 |
(*>*)
|