[isabelle-dev] BNF, -: flag, and sizes

[Jasmin Christian Blanchette]

Hi René,

> I just wanted to report some unexpected behavior when adapting our theories to datatype_new.
> First of all, thanks for the development, the convenience of using this package is very welcome!
> (automatic generation of named selection, map, ..., speed, etc.).
> However, when playing around with "-:" I noticed that this changes the generated size-functions 
> (and hence automatic termination proofs), although this change is not immediately visible.

Thank you for your report. It was indeed an unintended behavior, and I have a patch on Testboard that addresses it. If things go well, I will push it tonight. With the patch,

    thm mix21.size(3-4) mix22.size(3-4) mix23.size(3-4)

outputs

    size (Mix21 ?x11.0 ?x12.0) = size_list (size_list1 (%_. 0)) ?x11.0 + size ?x12.0 + Suc 0
    size Nix21 = 0
    size (Mix22 ?x11.0 ?x12.0) = size_list size ?x11.0 + size ?x12.0 + Suc 0
    size Nix22 = 0
    size (Mix23 ?x11.0 ?x12.0) = size_list size ?x11.0 + size ?x12.0 + Suc 0
    size Nix23 = 0

which is as good as things can get.

Cheers,

Jasmin