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



On 27.09.2011 15:29, Alfio Martini 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.

No, the two subtterms left and right of the equality sign are not exactly the same. Unfortunately, it is a bit misleading how this goal is presented by Isabelle. If you enable the display of types, you get at least a hint about what is going wrong:

  lemma "len Empty = len Empty"
  using [[show_types]]

outputs

  proof (prove): step 0

  goal (1 subgoal):
   1. len Empty = len Empty
  type variables:
    'a, 'b :: type

As you see, there are two type variables occuring in this term: Empty is polymorphic, but there are no constraints, which would enforce a particular instantiation of the polymorphic type variable -- not even that the types of the left and right Empty should be the same.

For this reason, refl is not applicable here.

  -- Lars





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