*To*: Brian Huffman <brianh at cs.pdx.edu>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] On the use of the rule HOL.refl(exive)*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Tue, 27 Sep 2011 10:46:49 -0300*In-reply-to*: <CAAMXsiZevVsy4yHYP6uJ9zS5Ssuvgc5mgTR0=BWaLw3V6ywv+g@mail.gmail.com>*References*: <CAAPnxw1V0gtOFWO8mMTDWDxtVLVLHioR-E3UuYJQob7mgF4rpg@mail.gmail.com> <CAAMXsiZevVsy4yHYP6uJ9zS5Ssuvgc5mgTR0=BWaLw3V6ywv+g@mail.gmail.com>*Sender*: alfio.martini at gmail.com

Very well!! Thank you! On Tue, Sep 27, 2011 at 10:43 AM, Brian Huffman <brianh at cs.pdx.edu> wrote: > On Tue, Sep 27, 2011 at 6:29 AM, Alfio Martini <alfio.martini at acm.org> > wrote: > > Dear Isabelle Users, > > > > In the script bellow, I was expecting to solve lemmas 01 and 04 directly > by > > reflexivity of equality, like the > > other ones, since both terms are the same.. But the simplifier tells me > > that I have to use also the equation len01, to substitute len(Empty) for > Z. > > What (basic fact) am I missing here? > > > datatype Nat = Z | suc Nat > > datatype 'a List = Empty | cons 'a "'a List" > > > > primrec len :: "'a List => Nat" > > > (* lemma 01 *) > > lemma "len Empty = len Empty" by (simp only:len01) > > For lemma 01, Isabelle infers the following types: > > "len (Empty :: 'a List) = len (Empty :: 'b List)" > > i.e., the element types of the two lists are not necessarily the same. > Thus the goal is not an instance of the reflexivity rule. > > > (* lemma 04 *) > > lemma "add (len Empty) (len Empty) = add (len Empty) (len Empty)" > > A similar situation applies to lemma 04, but here the four lists may > have four different types. > > If you turn on "show types" or "show sorts", then the goal window > should list all the type variables in the current goal, which can give > you a hint about what is going on. Alternatively, you can turn on > "show consts" to have Isabelle list the full types of all constants > used in the goal. > > - Brian > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) Porto Alegre - RS - Brasil

**References**:**[isabelle] On the use of the rule HOL.refl(exive)***From:*Alfio Martini

- Previous by Date: Re: [isabelle] On the use of the rule HOL.refl(exive)
- Next by Date: Re: [isabelle] On the use of the rule HOL.refl(exive)
- Previous by Thread: Re: [isabelle] On the use of the rule HOL.refl(exive)
- Next by Thread: Re: [isabelle] On the use of the rule HOL.refl(exive)
- Cl-isabelle-users September 2011 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