*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, Lars Hupel <hupel at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Automation for sub-term-like well-orderings*From*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Tue, 12 Apr 2016 09:47:38 +0100*Accept-language*: en-US, en-GB*Acceptlanguage*: en-US, en-GB*In-reply-to*: <570CB0A3.5060504@inf.ethz.ch>*References*: <570CACEF.9030506@in.tum.de> <570CB0A3.5060504@inf.ethz.ch>*Thread-index*: AdGUlONPCnoWa3MSTAWbUkYo31bntgAAdkoT*Thread-topic*: [isabelle] Automation for sub-term-like well-orderings

Hi Lars and Andreas, Yes, it would be nice to have this automated. Back in the days when designing the new datatype package, we thought of adding this as well, but eventually renounced in order to keep the effort size manageable. Here is my pattern for proving this for finitely branching datatypes (which constitute 99 percent of those in current use). The following lemma transports well-foundedness back from the order on naturals: lemma wfP_lt: assumes "â x y. r x y â (f x::nat) < f y" shows "wfP r" proof- have "{(x, y). r x y} â inv_image {(x,y) . x < y} f" using assms unfolding inv_image_def by auto thus ?thesis unfolding wfP_def using wf_inv_image wf_less wf_subset by blast qed Then the following are absolute routine (and are presumably not hard to automate, but have the usual complications coming from "mutual" and "nested"): lemma size_direct_sub_term[simp]: assumes "direct_sub_term t u" shows "size t < size u" using assms by induction auto lemma sub_term[simp]: assumes "sub_term t u" shows "size t < size u" using assms apply(induction, simp_all) using dual_order.strict_trans size_direct_sub_term by blast lemma wfP_sub_term: "wfP sub_term" using sub_term wfP_lt by blast lemma sub_term_induct[case_names sub]: assumes "ât. (âu. u â t â P u) â P t" shows "P t" using assms wfP_sub_term by (metis wfP_induct_rule) All the best, Andrei ________________________________________ From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Andreas Lochbihler [andreas.lochbihler at inf.ethz.ch] Sent: Tuesday, April 12, 2016 9:24 AM To: Lars Hupel; cl-isabelle-users at lists.cam.ac.uk Subject: 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 >

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

**Re: [isabelle] Automation for sub-term-like well-orderings***From:*Dmitriy Traytel

**Re: [isabelle] Automation for sub-term-like well-orderings***From:*Peter Lammich

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

**Re: [isabelle] Automation for sub-term-like well-orderings***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Automation for sub-term-like well-orderings
- Next by Date: Re: [isabelle] Automation for sub-term-like well-orderings
- Previous by Thread: Re: [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