[isabelle-dev] typedef (open) legacy
christian.urban at kcl.ac.uk
Thu Oct 4 13:37:22 CEST 2012
"Closed" type definitions with
typedef new_type = "some set"
are considered legacy. The warning message suggests
typedef (open) new_type = "some set"
but as far as I can see, this does not introduce
a definition for the set underlying the type. For
example the theorem
is not generated with open.
I have a number of lemmas that are of the form
f \<in> new_type ==> something
which require new_type_def. What is the received
wisdom to update those proofs?
I see that FinFun.thy goes around the problem
above by giving an explicit definition for the
set as in
definition new_type_set = something
typedef (open) new_type = new_type_set
Is this how it should be done nowadays? Looks
to me more verbose than an improvement.
More information about the isabelle-dev