92 interchangeably for propositions that have been proved. |
92 interchangeably for propositions that have been proved. |
93 \end{warn} |
93 \end{warn} |
94 \begin{warn} |
94 \begin{warn} |
95 Numerals (@{text 0}, @{text 1}, @{text 2}, \dots) and most of the standard |
95 Numerals (@{text 0}, @{text 1}, @{text 2}, \dots) and most of the standard |
96 arithmetic operations (@{text "+"}, @{text "-"}, @{text "*"}, @{text"\<le>"}, |
96 arithmetic operations (@{text "+"}, @{text "-"}, @{text "*"}, @{text"\<le>"}, |
97 @{text"<"} etc) are overloaded: they are available |
97 @{text"<"}, etc.) are overloaded: they are available |
98 not just for natural numbers but for other types as well. |
98 not just for natural numbers but for other types as well. |
99 For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate |
99 For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate |
100 that you are talking about natural numbers. Hence Isabelle can only infer |
100 that you are talking about natural numbers. Hence Isabelle can only infer |
101 that @{term x} is of some arbitrary type where @{text 0} and @{text"+"} |
101 that @{term x} is of some arbitrary type where @{text 0} and @{text"+"} |
102 exist. As a consequence, you will be unable to prove the goal. |
102 exist. As a consequence, you will be unable to prove the goal. |
148 that is closer to traditional informal mathematical language and is often |
148 that is closer to traditional informal mathematical language and is often |
149 directly readable. |
149 directly readable. |
150 |
150 |
151 \subsection{Type \indexed{@{text list}}{list}} |
151 \subsection{Type \indexed{@{text list}}{list}} |
152 |
152 |
153 Although lists are already predefined, we define our own copy just for |
153 Although lists are already predefined, we define our own copy for |
154 demonstration purposes: |
154 demonstration purposes: |
155 *} |
155 *} |
156 (*<*) |
156 (*<*) |
157 apply(auto) |
157 apply(auto) |
158 done |
158 done |