39 The constant \ttindexbold{0} and the operations |
39 The constant \ttindexbold{0} and the operations |
40 \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun}, |
40 \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun}, |
41 \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min}, |
41 \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min}, |
42 \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and |
42 \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and |
43 \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available |
43 \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available |
44 not just for natural numbers but at other types as well (see |
44 not just for natural numbers but at other types as well. |
45 \S\ref{sec:overloading}). For example, given the goal @{prop"x+0 = x"}, |
45 For example, given the goal @{prop"x+0 = x"}, |
46 there is nothing to indicate that you are talking about natural numbers. |
46 there is nothing to indicate that you are talking about natural numbers. |
47 Hence Isabelle can only infer that @{term x} is of some arbitrary type where |
47 Hence Isabelle can only infer that @{term x} is of some arbitrary type where |
48 @{term 0} and @{text"+"} are declared. As a consequence, you will be unable |
48 @{term 0} and @{text"+"} are declared. As a consequence, you will be unable |
49 to prove the goal (although it may take you some time to realize what has |
49 to prove the goal (although it may take you some time to realize what has |
50 happened if @{text show_types} is not set). In this particular example, |
50 happened if @{text show_types} is not set). In this particular example, |
51 you need to include an explicit type constraint, for example |
51 you need to include an explicit type constraint, for example |
52 @{text"x+0 = (x::nat)"}. If there is enough contextual information this |
52 @{text"x+0 = (x::nat)"}. If there is enough contextual information this |
53 may not be necessary: @{prop"Suc x = x"} automatically implies |
53 may not be necessary: @{prop"Suc x = x"} automatically implies |
54 @{text"x::nat"} because @{term Suc} is not overloaded. |
54 @{text"x::nat"} because @{term Suc} is not overloaded. |
|
55 |
|
56 For details see \S\ref{sec:numbers} and \S\ref{sec:overloading}; |
|
57 Table~\ref{tab:overloading} in the appendix shows the most important overloaded |
|
58 operations. |
55 \end{warn} |
59 \end{warn} |
56 |
60 |
57 Simple arithmetic goals are proved automatically by both @{term auto} and the |
61 Simple arithmetic goals are proved automatically by both @{term auto} and the |
58 simplification methods introduced in \S\ref{sec:Simplification}. For |
62 simplification methods introduced in \S\ref{sec:Simplification}. For |
59 example, |
63 example, |