Re: [isabelle] Large datatype definition: measuring elapsed time

On Wed, Mar 16, 2016 at 7:06 AM, C. Diekmann <diekmann at> wrote:

> Hi,
> I'm formalizing the syntax of IPv6 Addresses.
> I made a quite large datatype.

A suggestion on how to simplify the definition (I am not an Isabelle expert
so I will have to guess some notation). A "list with optional omission" can
be represented as a type List A | (List A, List A) (that is, a tuple of two
lists or one), and there is a function from this type and given a default
value a : A, to Option(FixedList n A) (lists of length n) which takes l :
List A to Some(l) if Len(l) = n and None otherwise, and takes (k,l) to
Some(k ++ [a; n - Len(k) - Len(l)] ++ l) (where ++ is list concat and [a;
n] is a list containing n a's) if n - Len(k) - Len(l) is nonnegative and
None otherwise.

Your IPv6 type is the above with n = 8 and A = "16 word", a = 0, and the
valid members of the type are those elements of List A | (List A, List A)
that don't map to None.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.