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