*To*: Lucas Cavalcante <thesupervisar at gmail.com>*Subject*: Re: [isabelle] help with recdef definition and induction*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 17 Aug 2007 10:28:32 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <b4d8f2180708161045p4195014ay11a9a2b99159ba6e@mail.gmail.com>*References*: <b4d8f2180708161045p4195014ay11a9a2b99159ba6e@mail.gmail.com>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

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.

Tobias

**References**:**[isabelle] help with recdef definition and induction***From:*Lucas Cavalcante

- Previous by Date: Re: [isabelle] Simplication Confusion?
- Next by Date: Re: [isabelle] help with recdef definition and induction
- Previous by Thread: [isabelle] help with recdef definition and induction
- Next by Thread: Re: [isabelle] help with recdef definition and induction
- Cl-isabelle-users August 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list