doc-src/TutorialI/fp.tex
 changeset 9494 44fefb6e9994 parent 9493 494f8cd34df7 child 9541 d17c0b34d5c8
equal inserted replaced
9493:494f8cd34df7 9494:44fefb6e9994
   123   theory by hand is when you simply want to check if it loads successfully
   123   theory by hand is when you simply want to check if it loads successfully
   124   without wanting to make use of the theory itself. This you can do by typing
   124   without wanting to make use of the theory itself. This you can do by typing
   125   \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
   125   \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
   126
   126
   127   If you suddenly discover that you need to modify a parent theory of your
   127   If you suddenly discover that you need to modify a parent theory of your
   128   current theory you must first abandon your current theory (at the shell
   128   current theory you must first abandon your current theory\indexbold{abandon

   129   theory}\indexbold{theory!abandon} (at the shell
   129   level type \isacommand{kill}\indexbold{*kill}). After the parent theory has
   130   level type \isacommand{kill}\indexbold{*kill}). After the parent theory has
   130   been modified you go back to your original theory. When its first line
   131   been modified you go back to your original theory. When its first line
   131   \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the
   132   \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the
   132   modified parent is reloaded automatically.
   133   modified parent is reloaded automatically.
   133 \end{description}
   134 \end{description}
   314 \isa{2} are available as abbreviations for the corresponding
   315 \isa{2} are available as abbreviations for the corresponding
   315 \isa{Suc}-expressions. If you need the full set of numerals,
   316 \isa{Suc}-expressions. If you need the full set of numerals,
   316 see~\S\ref{nat-numerals}.
   317 see~\S\ref{nat-numerals}.
   317
   318
   318 \begin{warn}
   319 \begin{warn}
   319   The operations \ttindexboldpos{+}{$HOL2arithfun},  320 The constant \ttindexbold{0} and the operations  320 \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun},  321 \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},  321 \isaindexbold{min}, \isaindexbold{max},  322 \ttindexboldpos{*}{$HOL2arithfun}, \isaindexbold{min}, \isaindexbold{max},
   322   \indexboldpos{\isasymle}{$HOL2arithrel} and  323 \indexboldpos{\isasymle}{$HOL2arithrel} and
   323   \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available  324 \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
   324   not just for natural numbers but at other types as well (see
   325   not just for natural numbers but at other types as well (see
   325   \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+y = y+x},
   326   \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+0 = x}, there
   326   there is nothing to indicate that you are talking about natural numbers.
   327   is nothing to indicate that you are talking about natural numbers.  Hence
   327   Hence Isabelle can only infer that \isa{x} and \isa{y} are of some
   328   Isabelle can only infer that \isa{x} is of some arbitrary type where
   328   arbitrary type where \isa{+} is declared. As a consequence, you will be
   329   \isa{0} and \isa{+} are declared. As a consequence, you will be unable to
   329   unable to prove the goal (although it may take you some time to realize
   330   prove the goal (although it may take you some time to realize what has
   330   what has happened if \texttt{show_types} is not set).  In this particular
   331   happened if \texttt{show_types} is not set).  In this particular example,
   331   example, you need to include an explicit type constraint, for example
   332   you need to include an explicit type constraint, for example \isa{x+0 =
   332   \isa{x+y = y+(x::nat)}.  If there is enough contextual information this may
   333     (x::nat)}.  If there is enough contextual information this may not be
   333   not be necessary: \isa{x+0 = x} automatically implies \isa{x::nat}.
   334   necessary: \isa{Suc x = x} automatically implies \isa{x::nat} because

   335   \isa{Suc} is not overloaded.
   334 \end{warn}
   336 \end{warn}
   335
   337
   336 Simple arithmetic goals are proved automatically by both \isa{auto}
   338 Simple arithmetic goals are proved automatically by both \isa{auto}
   337 and the simplification methods introduced in \S\ref{sec:Simplification}.  For
   339 and the simplification methods introduced in \S\ref{sec:Simplification}.  For
   338 example,
   340 example,