[isabelle] typedef with sorts


I just noticed the following behaviour that I found a bit puzzling at first:

typedef 'a foo = "if finite (UNIV :: 'a :: finite set) then (UNIV :: 'a set) else {}"
  by auto

term "undefined :: nat foo"

Essentially, I define a type copy 'a foo for any finite type 'a; however, Isabelle does not prevent me from using the type copy with an infinite type like nat. I first thought that this must surely be inconsistent, because I defined 'a foo to be empty for infinite types, but to my relief, I found that all the lemmas generated by typedef are annotated with the proper sort constraints, so it seems that "nat foo" is logically /not/ an empty type, but more like a completely arbitrary (non-empty) type that I know nothing about.

My question now is this: is it possible to make writing "nat foo" a type error? Or, perhaps, is it possible to add the sort constraint 'a :: finite to the context if 'a foo appears anywhere?

My use case is that I use Fraction_Field from HOL-Library, which demands its type parameter to be an idom, but whenever I have lemmas using 'a fraction, I have to annotate 'a :: idom manually, which is annoying.



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