*To*: Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] Pitfall with type-classes in Isar-Lemma format*From*: Makarius <makarius at sketis.net>*Date*: Wed, 15 Feb 2012 14:27:59 +0100 (CET)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1327149342.11671.17.camel@lapbroy33>*References*: <1327149342.11671.17.camel@lapbroy33>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Sat, 21 Jan 2012, Peter Lammich wrote:

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)

The above forms are very uncommon, so uncommon effects are to be expected.

Makarius

**Follow-Ups**:**Re: [isabelle] Pitfall with type-classes in Isar-Lemma format***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Library of Proofs
- Next by Date: [isabelle] PostDoc available at LIX, Ecole Polytechnique, France
- Previous by Thread: Re: [isabelle] No such variable
- Next by Thread: Re: [isabelle] Pitfall with type-classes in Isar-Lemma format
- Cl-isabelle-users February 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list