[isabelle-dev] typedef

[Andreas Schropp]

On 08/31/2011 04:21 PM, Andreas Schropp wrote:
> On 08/30/2011 08:12 PM, Brian Huffman wrote:
>> However, the nonemptiness proof does rely on type class assumptions:
>> Indeed, "{A. ~ finite A}" is actually empty for any finite type 'a. 

I think I get your point now: assumptions for type class constraints
on variables are indeed local to nonemptiness-proofs if we eliminate
typeclass-reasoning and don't regard it as primitive.

Generalizing the type well-formedness arguments to depend on arbitrary
local assumptions (instead of only type class assumptions) is the treatment
of local typedefs I talked about earlier.
But I think your suggestion via a different semantic interpretation of
typedefs would result in easier code.

Cheers,
   Andy