[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)
andreas.lochbihler at inf.ethz.ch
Mon Aug 5 08:43:06 CEST 2013
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.
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
> Best wishes,
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev