Re: [isabelle] datatype_compat in Isabelle2018-RC0



Hi Gerwin,

> On 21 Jun 2018, at 19:07, Gerwin.Klein at data61.csiro.au wrote:
> 
> 
> 
>> On 21 Jun 2018, at 18:22, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
> [..]
>> The reason why the old-style definitions were supported for so long at all was for the benefit of the "old_datatype" command. The thread "Any users of 'Old_Datatype.thy' or 'Old_SMT.thy'?" (started in December 2017) didn't reveal any users, so when I removed the legacy "old_datatype", I also removed the old-style size infrastructure (which itself is an important step towards removing the last left-overs from the old datatype package from Isabelle, to keep the Isabelle code in a not too messy state).
> 
> Ha, I did see that query, but did not realise its implication :-)
> 
> 
>>> I’m using this a few times — not very often, but it’s annoying enough to recreate manually (see email thread on that around Isabelle2017..) that it’s worth checking at least.
>> 
>> I would like to know more about your use case. It seems like you found a corner case of the datatype package -- namely, you're presumably disabling "size" first, then invoking "datatype_compat" to produce an old-style "size". Is your main motivation for the use of old-style "size" definitions compatibility (i.e. no need to port old scripts), or do you find the old definitions intrinsically better?
>> 
>> The reason I'm asking is that there are advantages and disadvantages to both schemes, and it may be worthwhile to just support both, e.g. via an option.
> 
> This case is so far the only one I have encountered that showed a real difference between the two.
> 
> It is precisely as you guessed:
> 
> datatype (plugins del: size)
>         'a typ_desc   = TypDesc "'a typ_struct" typ_name
>    and  'a typ_struct = TypScalar nat nat "'a" |
>                         TypAggregate "('a typ_desc,field_name) dt_pair list"
> 
> datatype_compat dt_pair
> datatype_compat typ_desc typ_struct
> 
> then a bunch of rules recreating exactly the old induct rules, so I don’t have to dig into old and messy proofs, and then at some point:
> 
> fun
>  fold_td' :: "(typ_name => ('a * field_name) list => 'a) * 'a typ_desc => 'a"
> where
> fot0: "fold_td' (f,TypDesc st nm) = (case st of
>           TypScalar n algn d => d |
>           TypAggregate ts => f nm (map (\<lambda>x. case x of DTPair t n => (fold_td' (f,t),n)) ts))”

The following works for me out of the box. Note that I also have removed "(plugins del: size)" from dt_pair.

Cheers,
Dmitriy


type_synonym field_name = string
type_synonym typ_name = string

datatype ('a,'b) dt_pair = DTPair 'a 'b

datatype 'a typ_desc   = TypDesc "'a typ_struct" typ_name
   and   'a typ_struct = TypScalar nat nat "'a" |
                         TypAggregate "('a typ_desc,field_name) dt_pair list"

datatype_compat dt_pair
datatype_compat typ_desc typ_struct

fun
 fold_td' :: "(typ_name => ('a * field_name) list => 'a) * 'a typ_desc => 'a"
where
fot0: "fold_td' (f,TypDesc st nm) = (case st of
          TypScalar n algn d => d |
          TypAggregate ts => f nm (map (λx. case x of DTPair t n => (fold_td' (f,t),n)) ts))"




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