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

[René Thiemann]

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.thiemann at 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