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



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
> >
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.