Re: [isabelle] [ExternalEmail] Re: datatype_compat in Isabelle2018-RC0



Well, that turned out to something mildly embarrassing. Since the definition of dt_pair is in a different theory, I had forgotten to remove the (plugins del: size) part there as well. If I do that, the fun definitions do go through.

Thanks, Dmitriy for pointing that out.

There are later proofs that then break, but I’ve bitten the bullet and updated those to what comes out of the new datatype package. The image builds fine and the direct tests on top seem to be fine as well, so it’s looking good so far. 

Cheers,
Gerwin


> On 21 Jun 2018, at 19:39, Gerwin.Klein at data61.csiro.au wrote:
> 
> Hm, I had tried that before and it failed. Let me get back to you.
> 
> Cheers,
> Gerwin
> 
> On 21 Jun 2018, at 19:33, Traytel Dmitriy <traytel at inf.ethz.ch<mailto:traytel at inf.ethz.ch>> wrote:
> 
> Hi Gerwin,
> 
> On 21 Jun 2018, at 19:07, Gerwin.Klein at data61.csiro.au<mailto:Gerwin.Klein at data61.csiro.au> wrote:
> 
> 
> 
> On 21 Jun 2018, at 18:22, Jasmin Blanchette <jasmin.blanchette at inria.fr<mailto: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.