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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
