Re: [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
>



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