summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 04 May 1999 16:49:24 +0200 | |

changeset 6577 | a2b5c84d590a |

parent 6576 | 7e0b35bed503 |

child 6578 | 918c41d2bfbe |

Arithmetic.

--- a/doc-src/Tutorial/Misc/ROOT.ML Tue May 04 16:18:16 1999 +0200 +++ b/doc-src/Tutorial/Misc/ROOT.ML Tue May 04 16:49:24 1999 +0200 @@ -1,3 +1,11 @@ +context Main.thy; +use "arith1.ML"; +by(Auto_tac); +use "arith2.ML"; +by(arith_tac 1); +use "arith3.ML"; +by(arith_tac 1); + use_thy "Tree"; context Main.thy;

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Tutorial/Misc/arith1.ML Tue May 04 16:49:24 1999 +0200 @@ -0,0 +1,1 @@ +Goal "[| ~ m < n; m < n+1 |] ==> m = n";

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Tutorial/Misc/arith2.ML Tue May 04 16:49:24 1999 +0200 @@ -0,0 +1,1 @@ +Goal "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Tutorial/Misc/arith3.ML Tue May 04 16:49:24 1999 +0200 @@ -0,0 +1,1 @@ +Goal "~ m < n & m < n+1 ==> m = n";

--- a/doc-src/Tutorial/fp.tex Tue May 04 16:18:16 1999 +0200 +++ b/doc-src/Tutorial/fp.tex Tue May 04 16:49:24 1999 +0200 @@ -338,8 +338,8 @@ loaded already. If you modify \texttt{T.thy} or \texttt{T.ML}, you can reload it by typing \texttt{use_thy~"T";} again. This time, however, only \texttt{T} is reloaded. If some of \texttt{T}'s parents have changed as well, -type \ttindexbold{update}\texttt{();} to reload all theories that have -changed. +type \ttindexbold{update_thy}~\texttt{"T";} to reload \texttt{T} and all of +its parents that have changed (or have changed parents). \end{description} Further commands are found in the Reference Manual. @@ -578,7 +578,9 @@ \section{Some basic types} + \subsection{Natural numbers} +\index{arithmetic|(} The type \ttindexbold{nat} of natural numbers is predefined and behaves like \begin{ttbox} @@ -599,17 +601,19 @@ \end{ttbox} The usual arithmetic operations \ttindexbold{+}, \ttindexbold{-}, -\ttindexbold{*}, \ttindexbold{div} and \ttindexbold{mod} are predefined, as -are the relations \ttindexbold{<=} and \ttindexbold{<}. There is even a least -number operation \ttindexbold{LEAST}. For example, \texttt{(LEAST n.$\,$1 < - n) = 2} (HOL does not prove this completely automatically). +\ttindexbold{*}, \ttindexbold{div}, \ttindexbold{mod}, \ttindexbold{min} and +\ttindexbold{max} are predefined, as are the relations \ttindexbold{<=} and +\ttindexbold{<}. There is even a least number operation \ttindexbold{LEAST}. +For example, \texttt{(LEAST n.$\,$1 < n) = 2} (HOL does not prove this +completely automatically). \begin{warn} - The operations \ttindexbold{+}, \ttindexbold{-}, \ttindexbold{*} 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 operations \ttindexbold{+}, \ttindexbold{-}, \ttindexbold{*}, + \ttindexbold{min}, \ttindexbold{max}, \ttindexbold{<=} and \ttindexbold{<} + 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 \texttt{x+y = y+x}, there is nothing to indicate that you are - talking about natural numbers. Hence Isabelle can only infer that + talking about natural numbers. Hence Isabelle can only infer that \texttt{x} and \texttt{y} are of some arbitrary type where \texttt{+} 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 @@ -619,6 +623,39 @@ \texttt{x+0 = x} automatically implies \texttt{x::nat}. \end{warn} +Simple arithmetic goals are proved automatically by both \texttt{Auto_tac} +and the simplification tactics introduced in \S\ref{sec:Simplification}. For +example, the goal +\begin{ttbox} +\input{Misc/arith1.ML}\end{ttbox} +is proved automatically. The main restriction is that only addition is taken +into account; other arithmetic operations and quantified formulae are ignored. + +For more complex goals, there is the special tactic \ttindexbold{arith_tac}. It +proves arithmetic goals involving the usual logical connectives (\verb$~$, +\verb$&$, \verb$|$, \verb$-->$), the relations \texttt{<=} and \texttt{<}, +and the operations \ttindexbold{+}, \ttindexbold{-}, \ttindexbold{min} and +\ttindexbold{max}. For example, it can prove +\begin{ttbox} +\input{Misc/arith2.ML}\end{ttbox} +because \texttt{k*k} can be treated as atomic. +In contrast, $n*n = n \Longrightarrow n=0 \lor n=1$ is not +even proved by \texttt{arith_tac} because the proof relies essentially on +properties of multiplication. + +\begin{warn} + The running time of \texttt{arith_tac} is exponential in the number of + occurrences of \ttindexbold{-}, \ttindexbold{min} and \ttindexbold{max} + because they are first eliminated by case distinctions. + + \texttt{arith_tac} is incomplete even for the restricted class of formulae + described above (known as ``linear arithmetic''). If divisibility plays a + role, it may fail to prove a valid formula, for example $m+m \neq n+n+1$. + Fortunately, such examples are rare in practice. +\end{warn} + +\index{arithmetic|)} + \subsection{Products} @@ -1010,6 +1047,20 @@ \end{ttbox} +\subsubsection{Arithmetic} +\index{arithmetic} + +The simplifier routinely solves a small class of linear arithmetic formulae +(over types \texttt{nat} and \texttt{int}): it only takes into account +assumptions and conclusions that are (possibly negated) (in)equalities +(\texttt{=}, \texttt{<=}, \texttt{<}) and it only knows about addition. Thus +\begin{ttbox} +\input{Misc/arith1.ML}\end{ttbox} +is proved by simplification, whereas the only slightly more complex +\begin{ttbox} +\input{Misc/arith3.ML}\end{ttbox} +is not proved by simplification and requires \texttt{arith_tac}. + \subsubsection{Permutative rewrite rules} A rewrite rule is {\bf permutative} if the left-hand side and right-hand side

--- a/doc-src/Tutorial/tutorial.bbl Tue May 04 16:18:16 1999 +0200 +++ b/doc-src/Tutorial/tutorial.bbl Tue May 04 16:49:24 1999 +0200 @@ -21,7 +21,8 @@ \bibitem{MuellerNvOS98} Olaf M\"uller, Tobias Nipkow, David~von Oheimb, and Oskar Slotosch. \newblock {HOLCF = HOL + LCF}. -\newblock Submitted for publication, 1998. +\newblock {\em J. Functional Programming}, 1999. +\newblock To appear. \bibitem{Isa-Ref-Man} Lawrence~C. Paulson.

--- a/doc-src/Tutorial/tutorial.ind Tue May 04 16:18:16 1999 +0200 +++ b/doc-src/Tutorial/tutorial.ind Tue May 04 16:49:24 1999 +0200 @@ -11,13 +11,13 @@ \item {\ttuniquex}, \bold{3} \item {\tt *}, \bold{17} \item {\tt +}, \bold{17} - \item {\tt -}, \bold{17} + \item {\tt -}, \bold{17, 18} \item {\tt <}, \bold{17} \item {\tt <=}, \bold{17} \item \ttlbr, \bold{9} \item \ttrbr, \bold{9} \item {\tt==>}, \bold{9} - \item {\tt==}, \bold{18} + \item {\tt==}, \bold{19} \item {\tt\%}, \bold{3} \item {\tt =>}, \bold{2} @@ -27,6 +27,8 @@ \item {\tt Addsplits}, \bold{24} \item {\tt addsplits}, \bold{24} \item {\tt and}, \bold{29} + \item {\tt arith_tac}, \bold{17} + \item arithmetic, 17--18, 24 \item {\tt Asm_full_simp_tac}, \bold{21} \item {\tt asm_full_simp_tac}, \bold{22} \item {\tt Asm_simp_tac}, \bold{21} @@ -39,7 +41,7 @@ \indexspace \item {\tt case}, \bold{3}, 4, \bold{13}, 24 - \item {\tt constdefs}, \bold{18} + \item {\tt constdefs}, \bold{19} \item {\tt consts}, \bold{7} \item {\tt context}, \bold{11} \item current theory, \bold{11} @@ -47,7 +49,7 @@ \indexspace \item {\tt datatype}, \bold{7}, 29--33 - \item {\tt defs}, \bold{18} + \item {\tt defs}, \bold{19} \item {\tt delsimps}, \bold{22} \item {\tt Delsplits}, \bold{24} \item {\tt delsplits}, \bold{24} @@ -84,7 +86,9 @@ \indexspace \item {\tt Main}, \bold{2} - \item measure function, \bold{35} + \item {\tt max}, \bold{17, 18} + \item measure function, \bold{36} + \item {\tt min}, \bold{17, 18} \item {\tt mod}, \bold{17} \item {\tt mutual_induct_tac}, \bold{30} @@ -138,7 +142,7 @@ \indexspace \item unknown, \bold{4} - \item {\tt update}, \bold{12} + \item {\tt update_thy}, \bold{12} \item {\tt use_thy}, \bold{2}, 12 \end{theindex}