Re: [isabelle] Automation for sub-term-like well-orderings



Hi Lars,

AFAIK there is no automation support for this.

For finitely branching, tree-like data structures, the subterm relation is well-founded (as a proof, just take the size of the tree as a measure). So I'd expect that you can prove the induction statement using induction_schema and lexicographic_order (after some setup for tranclp and direct_sub_term).

If you have an infinitely branching tree (or recursion through other BNFs without a size function), then well-foundedness of the subterm relation cannot be proven with measures. In these cases, I normally manually write definitions similar to yours and prove well-foundedness, which I can then use in termination proofs for the function package.

So if you have the time to automate these steps, I'd be all in favour of it. I guess that this should not be too hard with the new datatype package, but it definitely requires some work, but Dmitriy and Jasmin are in a better position to estimate the effort needed.

Andreas

On 12/04/16 10:08, Lars Hupel wrote:
Dear list,

I have the following datatype:

datatype "term" =
   Const string |
   Free string |
   Abs "term" ("Î _" [71] 71) |
   Bound nat |
   App "term" "term" (infixl "$" 70)

I define a sub-term relation:

inductive direct_sub_term :: "term â term â bool" where
left: "direct_sub_term t (t $ u)" |
right: "direct_sub_term u (t $ u)" |
abs: "direct_sub_term t (Î t)"

abbreviation sub_term :: "term â term â bool" (infix "â" 50) where
"sub_term â direct_sub_termâ+â+"

I have no idea whether this is in fact a proper well-ordering, but I'd
like to at least prove the induction principle:

lemma sub_term_induct[case_names sub]:
   assumes "ât. (âu. u â t â P u) â P t"
   shows "P t"

The proof is rather mechanical, but it took me a while to figure out (by
looking at the corresponding proof for natural numbers).

I wonder if there's existing automation to derive the "â" predicate and
the corresponding proof.

Cheers
Lars





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