Re: [isabelle] help with recdef definition and induction



Consider the following function:

  consts sum1 :: '[nat,nat] => nat"
  primrec
   "sum1 m 0 = m"
   "sum1 m (Suc n) = sum1 (Suc m) n"

Then I try to prove:

  lemma 1: "sum 0 n = n"

by
     apply (induct_tac n, auto)

resulting this:

   !!n. sum1  0 n = n ==> sum1 (Suc 0) n = Suc n

but this remaing stage seems trivial by definition of sum1.

It does *not* follow trivially - you have no defn or lemma which tells you what "sum1 (Suc 0) n" is. You need to prove such lemmas first.

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.