*To*: Lars Hupel <hupel at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Automation for sub-term-like well-orderings*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 12 Apr 2016 10:24:03 +0200*In-reply-to*: <570CACEF.9030506@in.tum.de>*References*: <570CACEF.9030506@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

Hi Lars, AFAIK there is no automation support for this.

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

**Follow-Ups**:**Re: [isabelle] Automation for sub-term-like well-orderings***From:*Andrei Popescu

**References**:**[isabelle] Automation for sub-term-like well-orderings***From:*Lars Hupel

- Previous by Date: [isabelle] Automation for sub-term-like well-orderings
- Next by Date: Re: [isabelle] Automation for sub-term-like well-orderings
- Previous by Thread: [isabelle] Automation for sub-term-like well-orderings
- Next by Thread: Re: [isabelle] Automation for sub-term-like well-orderings
- Cl-isabelle-users April 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list