Quelle natsum.thy

Sprache: Isabelle

(*<*)
theory natsum imports Main begin
(*>*)
text‹\noindent
particular, there are ‹case›-expressions, for example
{term[display]"case n of 0 => 0 | Suc m => m"}
recursion, for example
›

primrec sum :: "nat ==> nat" where
"sum 0 = 0" |
"sum (Suc n) = Suc n + sum n"

text‹\noindent
induction, for example
›

lemma "sum n + sum n = n*(Suc n)"
apply(induct_tac n)
apply(auto)
done

text‹\newcommand{\mystar}{*%

index{arithmetic operations!for \protect\isa{nat}}%
arithmetic operations \isadxboldpos{+}{$HOL2arithfun},
isadxboldpos{-}{$HOL2arithfun}, \isadxboldpos{\mystar}{$HOL2arithfun},
sdx{div}, \sdx{mod}, \cdx{min} and
cdx{max} are predefined, as are the relations
isadxboldpos{\isasymle}{$HOL2arithrel} and
isadxboldpos{<}{$HOL2arithrel}. As usual, prop‹m-n = (0::nat)› if
prop‹m<n\›. There is even a least number operation
sdx{LEAST}\@. For example, prop‹(LEAST n. 0 < n) = Suc 0›.
begin{warn}\index{overloading}
The constants \cdx{0} and \cdx{1} and the operations
\isadxboldpos{+}{$HOL2arithfun}, \isadxboldpos{-}{$HOL2arithfun},
\isadxboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
\cdx{max}, \isadxboldpos{\isasymle}{$HOL2arithrel} and
\isadxboldpos{<}{$HOL2arithrel} are overloaded: they are available
not just for natural numbers but for other types as well.
For example, given the goal ‹x + 0 = x›, there is nothing to indicate
that you are talking about natural numbers. Hence Isabelle can only infer
that term‹x› is of some arbitrary type where ‹0› and ‹+› are
declared. As a consequence, you will be unable to prove the
goal. To alert you to such pitfalls, Isabelle flags numerals without a
fixed type in its output: prop‹x+0 = x›. (In the absence of a numeral,
it may take you some time to realize what has happened if \pgmenu{Show
Types} is not set). In this particular example, you need to include
an explicit type constraint, for example ‹x+0 = (x::nat)›. If there
is enough contextual information this may not be necessary: prop‹Suc x =
x› automatically implies ‹x::nat› because term‹Suc› is not
overloaded.

For details on overloading see \S\ref{sec:overloading}.
Table~\ref{tab:overloading} in the appendix shows the most important
overloaded operations.
end{warn}
begin{warn}
The symbols \isadxboldpos{>}{$HOL2arithrel} and
\isadxboldpos{\isasymge}{$HOL2arithrel} are merely syntax: ‹x > y›
stands for prop‹y < x› and similary for ‹≥› and
‹≤›.
end{warn}
begin{warn}
Constant ‹1::nat› is defined to equal term‹Suc 0›. This definition
(see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
tactics (like ‹auto›, ‹simp› and ‹arith›) but not by
others (especially the single step tactics in Chapter~\ref{chap:rules}).
If you need the full set of numerals, see~\S\ref{sec:numerals}.
\emph{Novices are advised to stick to term‹0::nat› and term‹Suc›.}
end{warn}

‹auto› and ‹simp›
a method introduced below, \S\ref{sec:Simplification}) prove
arithmetic goals automatically:
›

lemma "[ ¬ m < n; m < n + (1::nat) ] ==> m = n"
(*<*)by(auto)(*>*)

text‹\noindent
efficiency's sake, this built-in prover ignores quantified formulae,
logical connectives, and all arithmetic operations apart from addition.
consequence, ‹auto› and ‹simp› cannot prove this slightly more complex goal:
›

lemma "m ≠ (n::nat) ==> m < n ∨ n < m"
(*<*)by(arith)(*>*)

text‹\noindent The method \methdx{arith} is more general. It attempts to
the first subgoal provided it is a \textbf{linear arithmetic} formula.
formulas may involve the usual logical connectives (‹¬›,
‹∧›, ‹∨›, ‹⟶›, ‹=›,
‹∀›, ‹∃›), the relations ‹=›,
‹≤› and ‹<\<close>, and the operations ‹+›, ‹-›,
term‹min› and term‹max›. For example,›

"min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))"
(arith)
(*<*)done(*>*)

text‹\noindent
because term‹k*k› can be treated as atomic. In contrast,
›

lemma "n*n = n+1 ==> n=0"
(*<*)oops(*>*)

text‹\noindent
not proved by ‹arith› because the proof relies
properties of multiplication. Only multiplication by numerals (which is
same as iterated addition) is taken into account.

begin{warn} The running time of ‹arith› is exponential in the number
of occurrences of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
\cdx{max} because they are first eliminated by case distinctions.

‹k› is a numeral, \sdx{div}~‹k›, \sdx{mod}~‹k› and
‹k›~\sdx{dvd} are also supported, where the former two are eliminated
case distinctions, again blowing up the running time.

the formula involves quantifiers, ‹arith› may take
-exponential time and space.
end{warn}
›

(*<*)
end
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.