Re: [isabelle] Isabelle2016-RC1: typedef-overloaded and records



Dear RenÃ,

unfortunately, I have no answer to your question.

Thank you for sharing the 'context notes [[typedef_overloaded]]'
pattern to enable overloading for only one datatype definition. This
solves one of my problems
(http://article.gmane.org/gmane.science.mathematics.logic.isabelle.user/12503).

The following question remains:
  Is using typedef_overloaded somehow dangerous?

Best Regards,
  Cornelius

2016-01-18 12:51 GMT+01:00 Thiemann, Rene <Rene.Thiemann at uibk.ac.at>:
> Dear all,
>
> when adapting our theories to Isabelle2016-RC1, I encountered a problem with the new upgrade of typedef and the overloaded constants.
>
> Note that ('a,'b)rbt in "~~/src/HOL/Library/RBT" is such an overloaded type. As a user of RBTâs I now have to put a context around
> other types that use RBTâs with a parametric 'a as in the example type âuse_rbt_Aâ.
>
> However, the problem is that, I now cannot put these types into records or use records with generic RBTâs as arguments, since
> records are not localized. So, the creation of both types use_rbt_B and use_rbt_C fails.
>
> Is there any known work-around to this problem?
> (Except for converting the records into datatypes and then recursively wrap a context with [[typedef_overloaded]] around every further
>  type declaration that transitively depends on these types)
>
> With best regards,
> RenÃ
>
>
> theory Test
> imports
>   "~~/src/HOL/Library/RBT"
> begin
>
> context
>   notes [[typedef_overloaded]]
> begin
> datatype 'a use_rbt_A = Foo "('a,bool) rbt"
> end
>
> record 'a use_rbt_B =
>   bar :: "'a use_rbt_A"
>
> record 'a use_rbt_C =
>   com :: "('a,bool)rbt"
>
> end




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