[isabelle-dev] BNF, -: flag, and sizes
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Thu May 15 17:54:56 CEST 2014
> 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)
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.
More information about the isabelle-dev