[isabelle] Automation for sub-term-like well-orderings
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