# Re: [isabelle] On the use of the rule HOL.refl(exive)

```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

```

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