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



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.