Hi,

"Closed" type definitions with

  typedef new_type = "some set"

are considered legacy. The warning message suggests
to use

  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

  new_type_def

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.

Any comments?

Best wishes,
Christian
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to