[isabelle] Pitfall with type-classes in Isar-Lemma format



Hi all,

(Referring to Isabelle2011-1)

I recently ran into the following pitfall:

lemma pitfall1:
  notes [[show_sorts]]
  notes test = refl[where 'a='a]
  fixes x::"'a::default"
  shows "x=x"
  thm test -- "'a has the wrong sort here!"
  using test apply -

Now it outputs:
type variables:
  'a :: type
  'a :: default

and, of course, apply (rule test) fails. When inspecting this failure,
the already confused user gets the following trace from the unifier
(even with show_sorts turned on!)

The following types do not unify:
'a \<Rightarrow> 'a \<Rightarrow> bool
'a \<Rightarrow> 'a \<Rightarrow> bool



I would expect that a type-variable with the same name should also have
the same sort -- at least when I introduce it within the
scope of the very same lemma.

And even more strange, this pitfall can be resolved by just swapping the
notes and the fixes declaration:

lemma pitfall1_resolved:
  fixes x::"'a::default"
  notes [[show_sorts]]
  notes test = refl[where 'a='a]
  shows "x=x"
  by (rule test)


Regards,
  Peter








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