*To*: Scott West <scott.west at inf.ethz.ch>*Subject*: Re: [isabelle] Termination Proof ``fun'' ;)*From*: Alexander Schimpf <info at hitstec.de>*Date*: Mon, 04 May 2009 19:31:35 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <49FEB0D5.5050108@inf.ethz.ch>*References*: <49F5AA3F.5040004@inf.ethz.ch> <49F6C9C6.2020201@loria.fr> <49F6EC46.4030909@hitstec.de> <49FEB0D5.5050108@inf.ethz.ch>*User-agent*: Thunderbird 2.0.0.21 (Windows/20090302)

Dear Scott, Scott West schrieb:

Hello Alex,Exactly! You will need to define a set "L" which contains all thenodes that can be "seen". Instead of "measures" I would prefer theuse of "psubset" here.I'll look at psubset, thanks!But this is not the only problem you have here. Moreover the use of"foldr" complicates the proof. When you start your termination proof,you will notice, that there is no call of "foldr" anymore. Here the"Higher Order Recursion"(http://isabelle.in.tum.de/dist/Isabelle/doc/functions.pdf, chapter9) comes into play. "foldr" is eliminated using the congruence rule'foldr_cong' (from List.thy) I think. But this rule 'abstracts' overthe second argument (of f), so that you are not able state anythingabout it (and you will need it to proof termination). Therefore youhave probably first to find the right congruence rule for 'foldr'that somehow preserves the information, that the second argument of fis always a subset of "L".I read the functions.pdf that you pointed me to, however I still dont'feel as if I know how the congruence mechanism works in practice. Howdoes it `abstract' over the second argument of `f' ?If I do need to reformulate the foldr_cong rule to fit my needs, arethere any good examples of how these rules are applied during theproof, so I can see what's going wrong?

Maybe it is a better idea to eliminate the use of foldr (if possible)completely.I do now have a version that I created without foldr that I can provetermination. However eventually I will be doing things where foldrbecomes important (modeling imperative code, so the accumulatedparameter will be the state). So I guess I'm going down a moredifficult road ;).

Thanks again for the help!

No problem, so far! Regards, Alex

theory Test imports Main begin consts g :: "nat \<Rightarrow> nat list" function f :: "nat \<Rightarrow> nat list \<Rightarrow> nat list" and foldr_f :: "[nat list, nat list] \<Rightarrow> nat list" where "f k ks = (if k \<in> set ks then ks else foldr_f (g k) (k#ks))" | "foldr_f [] a = a" | "foldr_f (x#xs) a = f x (foldr_f xs a)" by pat_completeness auto consts lim :: "[nat, nat list] \<Rightarrow> nat set" --"lim takes the arguments of f and calculates all reachable nodes" lemma lim_finite: "finite (lim k ks)" sorry lemma lim_eq: "lim k (k#ks) = lim k ks" sorry lemma lim_subset: "set ks \<subseteq> lim k ks" sorry lemma lim_concat: "lim k (xs at ys) = lim k xs \<union> lim k ys" sorry lemma lim_append: "lim k (x#xs) = lim k [x] \<union> lim k xs" using lim_concat[of k "[x]" xs] by auto lemma lim_mem: "k\<in>set ks \<Longrightarrow> lim l (k#ks) = lim l ks" sorry lemma subset_prop': "f_foldr_f_dom (Inl (k, a)) \<Longrightarrow> set a \<subseteq> set (f k a) \<and> lim l (f k a) = lim l (k#a)" "f_foldr_f_dom (Inr (ks, a)) \<Longrightarrow> set a \<subseteq> set (foldr_f ks a) \<and> lim l (foldr_f ks a) = lim l (ks at a)" proof (induct a and a rule: f_foldr_f.pinduct) case goal1 thus ?case proof(cases "k\<in>set ks") case goal1 thus ?case using lim_mem by simp next case goal2 hence "lim l (g k @ k # ks) = lim l (k#ks)" sorry --"This should be true, since lim should contain all 'child nodes' that are calculated by g." --"Therefore the right hand side should contain 'g k' implicitly." thus ?case using goal2 by simp qed next case goal2 thus ?case by auto next case (goal3 k' ) have "lim l (k' # xs @ a) = lim l [k'] \<union> lim l (xs @ a)" using lim_append by blast moreover with goal3 have "\<dots> = lim l [k'] \<union> lim l (foldr_f xs a)" by auto moreover have "\<dots> = lim l (k' # foldr_f xs a)" using lim_append by blast moreover have "\<dots> = lim l (f k' (foldr_f xs a))" using goal3 by auto ultimately have "lim l (f k' (foldr_f xs a)) = lim l (k' # xs @ a)" by simp thus ?case using goal3 by auto qed lemma subset_prop: assumes "f_foldr_f_dom (Inr (ks, a))" shows "set a \<subseteq> set (foldr_f ks a)" and "lim k (foldr_f ks a) = lim k (ks at a)" using prems subset_prop' by auto abbreviation "my_term_ord \<equiv> inv_image (finite_psubset <*lex*> less_than) (\<lambda>v. (case v of (Inr (ys, ks)) \<Rightarrow> (lim (hd ks) (ks at ys) - set ks, size ys) | (Inl (k, ks)) \<Rightarrow> (lim k ks - set ks, 0) ))" lemma in_finite_psubset[simp]: "((A, B) \<in> finite_psubset) = (A \<subset> B \<and> finite B)" unfolding finite_psubset_def by simp termination proof (relation "my_term_ord") case goal1 thus ?case by (auto intro: wf_finite_psubset) next case (goal2 k ks) hence "lim k (k#ks) - insert k (set ks) \<subset> lim k ks - set ks" unfolding lim_eq sorry --"easy to proof" moreover have "finite (lim k ks - set ks)" using lim_finite by auto moreover have "lim k (k # ks) = lim k (k # ks @ g k)" sorry --"see above" ultimately show ?case by simp next case (goal3 k ks a) thus ?case apply simp sorry --"easy to proof" next case (goal4 k ks a) hence "set a \<subseteq> set (foldr_f ks a)" and "lim k (foldr_f ks a) = lim k (ks at a)" using subset_prop by auto moreover have "lim (hd a) (a @ k # ks) = lim k (ks at a)" sorry -- "easy to proof" ultimately show ?case apply simp sorry -- "again easy, use the premise" qed end

**References**:**Re: [isabelle] Termination Proof ``fun'' ;)***From:*Scott West

- Previous by Date: [isabelle] LFMTP 2009: Deadline extension
- Next by Date: [isabelle] A Quantification Binding Question
- Previous by Thread: Re: [isabelle] Termination Proof ``fun'' ;)
- Next by Thread: [isabelle] LFMTP 2009: Deadline extension
- Cl-isabelle-users May 2009 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