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"
proof (prove): step 0
goal (1 subgoal):
1. len Empty = len Empty
'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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and