Re: [isabelle] Automation for sub-term-like well-orderings
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.
On 12/04/16 10:08, Lars Hupel wrote:
I have the following datatype:
datatype "term" =
Const string |
Free string |
Abs "term" ("Î _"  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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and