[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)

[Andreas Lochbihler]

Hi Christian,

the two different size functions become relevant as soon as you have a polymorphic 
datatype such as

datatype 'a foo = Foo 'a | Bar "'a foo"

Then, foo_size takes size function for every type variable as additional parameters and 
takes them into account, whereas size ignores occurrences of the type variables.

thm foo.size

foo_size fa (Foo a) = fa a + Suc 0
foo_size fa (Bar foo) = foo_size fa foo + Suc 0
size (Foo a) = 0
size (Bar foo) = size foo + Suc 0

The generalised size function can be useful in termination proofs such as

function f :: "nat foo => unit" where
   "f (Foo 0) = ()"
| "f (Foo (Suc n)) = f (Foo n)"
| "f (Bar x) = f x"
by pat_completeness simp_all
termination by(relation "measure (foo_size size)") simp_all

Andreas


On 04/08/13 21:20, Christian Urban wrote:
>
>
> On Sunday, August 4, 2013 at 20:32:50 (+0200), Dmitriy Traytel wrote:
>   > ....I.e. everything that is defined by the new package and
>   > falls into the fragment of the old package can be registered as an old
>   > datatype benefiting from all the infrastructure built around it (e.g.
>   > size function, Quickcheck, and other "datatype interpretations").
>
> On the topic of size functions: I found it always odd that
> the existing datatype package (however I think this particular
> functionality is now provided by the function package) defines
> under <datatype_name>.simps "two" definitions of the corresponding
> size function. Consider for example
>
>
>    datatype test = A1 | A2 | A3 "test"
>
>    thm test.size
>
>    > test_size A1 = 0
>    > test_size A2 = 0
>    > test_size (A3 ?test) = test_size ?test + Suc 0
>    > size A1 = 0
>    > size A2 = 0
>    > size (A3 ?test) = size ?test + Suc 0
>
>
> Surely, it would be more uniform to have just the equations for
> size, no? Is there any usage for the test_size definitions?
> If not, then maybe in the course of updating the datatype
> package, this oddity can be eliminated (Nominal needed to work
> around it). But I am happy to admit that I might miss something
> important.
>
> Best wishes,
> Christian
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>