summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/fp.tex

changeset 9494 | 44fefb6e9994 |

parent 9493 | 494f8cd34df7 |

child 9541 | d17c0b34d5c8 |

--- a/doc-src/TutorialI/fp.tex Wed Aug 02 11:30:38 2000 +0200 +++ b/doc-src/TutorialI/fp.tex Wed Aug 02 13:17:11 2000 +0200 @@ -125,7 +125,8 @@ \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}. If you suddenly discover that you need to modify a parent theory of your - current theory you must first abandon your current theory (at the shell + current theory you must first abandon your current theory\indexbold{abandon + theory}\indexbold{theory!abandon} (at the shell level type \isacommand{kill}\indexbold{*kill}). After the parent theory has been modified you go back to your original theory. When its first line \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the @@ -316,21 +317,22 @@ see~\S\ref{nat-numerals}. \begin{warn} - The operations \ttindexboldpos{+}{$HOL2arithfun}, - \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun}, - \isaindexbold{min}, \isaindexbold{max}, + The constant \ttindexbold{0} and the operations + \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun}, + \ttindexboldpos{*}{$HOL2arithfun}, \isaindexbold{min}, \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available not just for natural numbers but at other types as well (see - \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+y = y+x}, - there is nothing to indicate that you are talking about natural numbers. - Hence Isabelle can only infer that \isa{x} and \isa{y} are of some - arbitrary type where \isa{+} is declared. As a consequence, you will be - unable to prove the goal (although it may take you some time to realize - what has happened if \texttt{show_types} is not set). In this particular - example, you need to include an explicit type constraint, for example - \isa{x+y = y+(x::nat)}. If there is enough contextual information this may - not be necessary: \isa{x+0 = x} automatically implies \isa{x::nat}. + \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+0 = x}, there + is nothing to indicate that you are talking about natural numbers. Hence + Isabelle can only infer that \isa{x} is of some arbitrary type where + \isa{0} and \isa{+} are declared. As a consequence, you will be unable to + prove the goal (although it may take you some time to realize what has + happened if \texttt{show_types} is not set). In this particular example, + you need to include an explicit type constraint, for example \isa{x+0 = + (x::nat)}. If there is enough contextual information this may not be + necessary: \isa{Suc x = x} automatically implies \isa{x::nat} because + \isa{Suc} is not overloaded. \end{warn} Simple arithmetic goals are proved automatically by both \isa{auto}