*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Automation for sub-term-like well-orderings*From*: Peter Lammich <lammich at in.tum.de>*Date*: Tue, 12 Apr 2016 11:32:16 +0200*In-reply-to*: <5F22105EAD3CAD4689EC4570AA1802B0BF06BE1C0F@WGFP-EXMAV1.uni.mdx.ac.uk>*References*: <570CACEF.9030506@in.tum.de> <570CB0A3.5060504@inf.ethz.ch> <5F22105EAD3CAD4689EC4570AA1802B0BF06BE1C0F@WGFP-EXMAV1.uni.mdx.ac.uk>

On set-based relations, there is a constant "measure", such that the proof could be done by showing inductive_set direct_sub_term :: "(term Ã term) set" where left: "(t, t $ u) â direct_sub_term " | right: "(u, t $ u) â direct_sub_term" | abs: "(t, (Î t)) â direct_sub_term" abbreviation sub_term :: "(term Ã term) set" where "sub_term â direct_sub_termâ+" lemma wf: "wf direct_sub_term" apply (rule wf_subset) apply (rule wf_measure[where f=size]) by (auto elim: direct_sub_term.cases) lemmas induct_rl = wf_induct[OF wf_trancl[OF wf]] (* Produces (âx. ây. (y, x) â sub_term â ?P y â ?P x) â ?P ?a *) On predicates, the concept of "measure" seems to be missing in the library, but there is also a wfP_trancl-lemma in the library, which could simplify Andrei's proof a bit. -- Peter On Di, 2016-04-12 at 09:47 +0100, Andrei Popescu wrote: > 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 > > >

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

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

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

- Previous by Date: Re: [isabelle] Automation for sub-term-like well-orderings
- Next by Date: [isabelle] New in the AFP: Kleene Algebras with Domain
- Previous by Thread: Re: [isabelle] Automation for sub-term-like well-orderings
- Next by Thread: [isabelle] New in the AFP: Kleene Algebras with Domain
- 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