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



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

> Hi,
>
> I'm formalizing the syntax of IPv6 Addresses.
>
> I made a quite large datatype.
>
>
> https://github.com/diekmann/Iptables_Semantics/blob/ccc5d5f9f0e09834c676cb36380409c095e6580d/thy/Bitmagic/IPv6Addr.thy#L98
>

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.

Mario



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