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



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





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