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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
