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