*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] Automation for sub-term-like well-orderings*From*: Dmitriy Traytel <traytel at inf.ethz.ch>*Date*: Tue, 12 Apr 2016 11:00:02 +0200*Cc*: Andrei Popescu <a.popescu at mdx.ac.uk>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*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>

Hi Lars, this would be useful indeed. Here is my pattern for proving this for arbitrary datatypes (which constitute 100 percent of those in current use ;-) ). Note that my definitions and proofs are done on what we call the low-level (where there is only one constructor). Jasmin is usually the one lifting lemmas (in particular the intro rules and the induction principle of ââ1) to multiple constructors. But I presume this should not be harder than usual in this case. Dmitriy theory Scratch imports "~~/src/HOL/Library/BNF_Axiomatization" begin declare [[typedef_overloaded]] bnf_axiomatization 'a F [wits: "'a F"] datatype T = C "T F" inductive direct_sub_term :: "T â T â bool" (infix "ââ1" 50) where "y â set_F x â y ââ1 C x" abbreviation sub_term :: "T â T â bool" (infix "â" 50) where "sub_term â direct_sub_termâ+â+" inductive_cases direct_sub_termE[elim!]: "y ââ1 C x" inductive_cases sub_termE[elim!]: "y â C x" lemma sub_term_induct_aux[THEN spec, THEN mp, rotated]: assumes [intro]: "ât. (âu. u â t â P u) â P t" shows "âu. u â t â P u" apply (induct t) apply auto done lemma sub_term_induct[case_names sub]: assumes IH: "ât. (âu. u â t â P u) â P t" shows "P t" apply (cases t; hypsubst_thin) apply (rule IH) apply (erule sub_term_induct_aux) by (rule IH) end > On 12 Apr 2016, at 10:47, Andrei Popescu <a.popescu at mdx.ac.uk> 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: 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