doc-src/TutorialI/Misc/natsum.thy
 author nipkow Wed Dec 13 09:39:53 2000 +0100 (2000-12-13) changeset 10654 458068404143 parent 10608 620647438780 child 10788 ea48dd8b0232 permissions -rw-r--r--
*** empty log message ***
     1 (*<*)

     2 theory natsum = Main:;

     3 (*>*)

     4 text{*\noindent

     5 In particular, there are @{text"case"}-expressions, for example

     6 @{term[display]"case n of 0 => 0 | Suc m => m"}

     7 primitive recursion, for example

     8 *}

     9

    10 consts sum :: "nat \<Rightarrow> nat";

    11 primrec "sum 0 = 0"

    12         "sum (Suc n) = Suc n + sum n";

    13

    14 text{*\noindent

    15 and induction, for example

    16 *}

    17

    18 lemma "sum n + sum n = n*(Suc n)";

    19 apply(induct_tac n);

    20 apply(auto);

    21 done

    22

    23 text{*\newcommand{\mystar}{*%

    24 }

    25 The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},   26 \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},   27 \isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and   28 \isaindexbold{max} are predefined, as are the relations   29 \indexboldpos{\isasymle}{$HOL2arithrel} and

    30 \ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = 0"} if   31 @{prop"m<n"}. There is even a least number operation   32 \isaindexbold{LEAST}. For example, @{prop"(LEAST n. 1 < n) = 2"}, although   33 Isabelle does not prove this completely automatically. Note that @{term 1}   34 and @{term 2} are available as abbreviations for the corresponding   35 @{term Suc}-expressions. If you need the full set of numerals,   36 see~\S\ref{sec:numerals}.   37   38 \begin{warn}   39 The constant \ttindexbold{0} and the operations   40 \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},   41 \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},

    42   \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and   43 \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available

    44   not just for natural numbers but at other types as well (see

    45   \S\ref{sec:overloading}). For example, given the goal @{prop"x+0 = x"},

    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

    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

    50   happened if @{text show_types} is not set).  In this particular example,

    51   you need to include an explicit type constraint, for example

    52   @{prop"x+0 = (x::nat)"}. If there is enough contextual information this

    53   may not be necessary: @{prop"Suc x = x"} automatically implies

    54   @{text"x::nat"} because @{term Suc} is not overloaded.

    55 \end{warn}

    56

    57 Simple arithmetic goals are proved automatically by both @{term auto} and the

    58 simplification methods introduced in \S\ref{sec:Simplification}.  For

    59 example,

    60 *}

    61

    62 lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"

    63 (*<*)by(auto)(*>*)

    64

    65 text{*\noindent

    66 is proved automatically. The main restriction is that only addition is taken

    67 into account; other arithmetic operations and quantified formulae are ignored.

    68

    69 For more complex goals, there is the special method \isaindexbold{arith}

    70 (which attacks the first subgoal). It proves arithmetic goals involving the

    71 usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},

    72 @{text"\<longrightarrow>"}), the relations @{text"\<le>"} and @{text"<"}, and the operations

    73 @{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is

    74 known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.

    75 For example,

    76 *}

    77

    78 lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";

    79 apply(arith)

    80 (*<*)done(*>*)

    81

    82 text{*\noindent

    83 succeeds because @{term"k*k"} can be treated as atomic. In contrast,

    84 *}

    85

    86 lemma "n*n = n \<Longrightarrow> n=0 \<or> n=1"

    87 (*<*)oops(*>*)

    88

    89 text{*\noindent

    90 is not even proved by @{text arith} because the proof relies essentially

    91 on properties of multiplication.

    92

    93 \begin{warn}

    94   The running time of @{text arith} is exponential in the number of occurrences

    95   of \ttindexboldpos{-}{\$HOL2arithfun}, \isaindexbold{min} and

    96   \isaindexbold{max} because they are first eliminated by case distinctions.

    97

    98   \isa{arith} is incomplete even for the restricted class of

    99   linear arithmetic formulae. If divisibility plays a

   100   role, it may fail to prove a valid formula, for example

   101   @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare in practice.

   102 \end{warn}

   103 *}

   104

   105 (*<*)

   106 end

   107 (*>*)