Re: [isabelle] recursive functions and set comprehension



Dimitrios Vytiniotis wrote:
Hello all, consider the (admittedly strange) fragment:

datatype tm = Z | S "tm"

consts foo :: "tm => tm set"
recdef foo "measure size"
"foo x = { Z. (x = Z) } \<union>
         { (S x1) | x1. x = S x1 /\ x1 : (foo x1) }";

Isabelle cannot prove monotonicity, because the equation "x = S x1"
seems to not be available. [...]

Hello,

by declaring the congruence rule for conjunction via

  declare conj_cong [recdef_cong]

before invoking recdef, you can instruct Isabelle to use the
equation "x = S x1" when proving the termination condition for
"x1 : (foo x1)". With the above declaration, the termination
proof for "foo" is completely automatic.

Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.