1.1 --- a/doc-src/Ref/simplifier.tex	Thu Nov 20 11:53:51 1997 +0100
     1.2 +++ b/doc-src/Ref/simplifier.tex	Thu Nov 20 11:54:31 1997 +0100
     1.3 @@ -713,15 +713,15 @@
     1.4  \begin{ttbox}
     1.5  NatSum = Arith +
     1.6  consts sum     :: [nat=>nat, nat] => nat
     1.7 -rules  sum_0      "sum f 0 = 0"
     1.8 -       sum_Suc    "sum f (Suc n) = f n + sum f n"
     1.9 +primrec "sum" nat 
    1.10 +  "sum f 0 = 0"
    1.11 +  "sum f (Suc n) = f(n) + sum f n"
    1.12  end
    1.13  \end{ttbox}
    1.14 -We make the required simpset by adding the AC-rules for~$+$ and the
    1.15 -axioms for~{\tt sum}:
    1.16 +The \texttt{primrec} declaration automatically adds rewrite rules for
    1.17 +\texttt{sum} to the default simpset.  We now insert the AC-rules for~$+$:
    1.18  \begin{ttbox}
    1.19 -val natsum_ss = simpset_of "Arith" addsimps ([sum_0,sum_Suc] \at add_ac);
    1.20 -{\out val natsum_ss = \ldots : simpset}
    1.21 +Addsimps add_ac;
    1.22  \end{ttbox}
    1.23  Our desired theorem now reads ${\tt sum} \, (\lambda i.i) \, (n+1) =
    1.24  n\times(n+1)/2$.  The Isabelle goal has both sides multiplied by~$2$:
    1.25 @@ -734,7 +734,7 @@
    1.26  Induction should not be applied until the goal is in the simplest
    1.27  form:
    1.28  \begin{ttbox}
    1.29 -by (simp_tac natsum_ss 1);
    1.30 +by (Simp_tac 1);
    1.31  {\out Level 1}
    1.32  {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
    1.33  {\out  1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
    1.34 @@ -742,29 +742,30 @@
    1.35  Ordered rewriting has sorted the terms in the left-hand side.  The
    1.36  subgoal is now ready for induction:
    1.37  \begin{ttbox}
    1.38 -by (nat_ind_tac "n" 1);
    1.39 +by (induct_tac "n" 1);
    1.40  {\out Level 2}
    1.41  {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
    1.42  {\out  1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0}
    1.43  \ttbreak
    1.44 -{\out  2. !!n1. n1 + (sum (\%i. i) n1 + sum (\%i. i) n1) = n1 * n1}
    1.45 -{\out           ==> Suc n1 + (sum (\%i. i) (Suc n1) + sum (\%i. i) (Suc n1)) =}
    1.46 -{\out               Suc n1 * Suc n1}
    1.47 +{\out  2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
    1.48 +{\out           ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i. i) (Suc n)) =}
    1.49 +{\out               Suc n * Suc n}
    1.50  \end{ttbox}
    1.51  Simplification proves both subgoals immediately:\index{*ALLGOALS}
    1.52  \begin{ttbox}
    1.53 -by (ALLGOALS (asm_simp_tac natsum_ss));
    1.54 +by (ALLGOALS Asm_simp_tac);
    1.55  {\out Level 3}
    1.56  {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
    1.57  {\out No subgoals!}
    1.58  \end{ttbox}
    1.59 -If we had omitted {\tt add_ac} from the simpset, simplification would have
    1.60 -failed to prove the induction step:
    1.61 +Simplification cannot prove the induction step if we omit {\tt add_ac} from
    1.62 +the simpset.  Observe that like terms have not been collected:
    1.63  \begin{ttbox}
    1.64 -2 * sum (\%i. i) (Suc n) = n * Suc n
    1.65 - 1. !!n1. n1 + sum (\%i. i) n1 + (n1 + sum (\%i. i) n1) = n1 + n1 * n1
    1.66 -          ==> n1 + (n1 + sum (\%i. i) n1) + (n1 + (n1 + sum (\%i.i) n1)) =
    1.67 -              n1 + (n1 + (n1 + n1 * n1))
    1.68 +{\out Level 3}
    1.69 +{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
    1.70 +{\out  1. !!n. n + sum (\%i. i) n + (n + sum (\%i. i) n) = n + n * n}
    1.71 +{\out           ==> n + (n + sum (\%i. i) n) + (n + (n + sum (\%i. i) n)) =}
    1.72 +{\out               n + (n + (n + n * n))}
    1.73  \end{ttbox}
    1.74  Ordered rewriting proves this by sorting the left-hand side.  Proving
    1.75  arithmetic theorems without ordered rewriting requires explicit use of