krauss at in.tum.de
Tue May 13 09:20:10 CEST 2008
* More flexible generation of measure functions for termination proofs:
Measure functions can be declared by proving a rule of the form
"is_measure f" and giving it the [measure_function] attribute. The
"is_measure" predicate is logically meaningless (always true), and
just guides the heuristic. To find suitable measure functions, the
termination prover sets up the goal "is_measure ?f" of the appropriate
type and generates all solutions by prolog-style backwards proof using
the declared rules.
This setup also deals with rules like
"is_measure f ==> is_measure (list_size f)"
which accomodates nested datatypes that recurse through lists. Similar
rules are predeclared for products and option types.
More information about the isabelle-dev