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

[Christian Urban]

Hi Andreas,

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. 

Thanks again,
Christian

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
 > 
 > 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
 > >
 > _______________________________________________
 > isabelle-dev mailing list
 > isabelle-dev at in.tum.de
 > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

--