Re: [isabelle] On the use of the rule HOL.refl(exive)
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>
> > Dear Isabelle Users,
> > In the script bellow, I was expecting to solve lemmas 01 and 04 directly
> > 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
> > 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