Dear all, 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.
Consider the following theory. theory Test imports Main begin datatype 'a list1 = Nil1 | Cons1 'a "'a list1" datatype_new 'a list2 = Nil2 | Cons2 'a "'a list2" datatype_new (-:'a) list3 = Nil3 | Cons3 'a "'a list3" (* the sizes of all three list variants are identical *) thm list1.size(3-4) list2.size(3-4) list3.size(3-4) datatype 'a mix11 = Mix11 "'a list1 list" "'a mix11" | Nix11 datatype 'a mix12 = Mix12 "'a list2 list" "'a mix12" | Nix12 datatype 'a mix13 = Mix13 "'a list3 list" "'a mix13" | Nix13 (* the size of all three mix variants are identical *) thm mix11.size(3-4) mix12.size(3-4) mix13.size(3-4) datatype_new 'a mix21 = Mix21 "'a list1 list" "'a mix21" | Nix21 datatype_new 'a mix22 = Mix22 "'a list2 list" "'a mix22" | Nix22 datatype_new 'a mix23 = Mix23 "'a list3 list" "'a mix23" | Nix23 (* the size of mix22 is different from both mix21 and mix23. whereas size_mix21 != size_mix22 might be okay I would not have expected size_mix22 != size_mix23 i.e., toggling -: in list2/3 on and off has an impact on other size functions although there is no difference in the size functions for list2/3 *) thm mix21.size(3-4) mix22.size(3-4) mix23.size(3-4) (* we get the same behavior if we also use "-:" in mix *) datatype_new (-:'a) mix31 = Mix31 "'a list1 list" "'a mix31" | Nix31 datatype_new (-:'a) mix32 = Mix32 "'a list2 list" "'a mix32" | Nix32 datatype_new (-:'a) mix33 = Mix33 "'a list3 list" "'a mix33" | Nix33 thm mix31.size(3-4) mix32.size(3-4) mix33.size(3-4) end I'm referring to Isabelle d0e04fdf4276 Kinds regards, René -- René Thiemann mailto:rene.thiem...@uibk.ac.at Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/ Institute of Computer Science phone: +43 512 507-6434 University of Innsbruck _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
