[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)
christian.urban at kcl.ac.uk
Mon Aug 5 18:14:27 CEST 2013
Thanks a lot! This fills a knowledge gap. ;o)
I am happy to keep the status quo. But I guess in an ideal world
one would then have two names for the associated theorems. Then
size would fit in with every other simp-theorems coming from
function or primrec definitions.
On Monday, August 5, 2013 at 08:43:06 (+0200), Andreas Lochbihler wrote:
> 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
> 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
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev