Re: [isabelle] Termination Proof ``fun'' ;)
- To: Alexander Schimpf <info at hitstec.de>
- Subject: Re: [isabelle] Termination Proof ``fun'' ;)
- From: Scott West <scott.west at inf.ethz.ch>
- Date: Mon, 04 May 2009 11:09:41 +0200
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <49F6EC46.firstname.lastname@example.org>
- References: <49F5AA3F.email@example.com> <49F6C9C6.firstname.lastname@example.org> <49F6EC46.email@example.com>
- User-agent: Thunderbird 188.8.131.52 (X11/20090409)
Exactly! You will need to define a set "L" which contains all the nodes
that can be "seen". Instead of "measures" I would prefer the use of
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, chapter 9)
comes into play. "foldr" is eliminated using the congruence rule
'foldr_cong' (from List.thy) I think. But this rule 'abstracts' over the
second argument (of f), so that you are not able state anything about it
(and you will need it to proof termination). Therefore you have probably
first to find the right congruence rule for 'foldr' that somehow
preserves the information, that the second argument of f is 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. How
does it `abstract' over the second argument of `f' ?
If I do need to reformulate the foldr_cong rule to fit my needs, are
there any good examples of how these rules are applied during the proof,
so I can see what's going wrong?
Maybe it is a better idea to eliminate the use of foldr (if possible)
I do now have a version that I created without foldr that I can prove
termination. However eventually I will be doing things where foldr
becomes important (modeling imperative code, so the accumulated
parameter will be the state). So I guess I'm going down a more difficult
Thanks again for the help!
This archive was generated by a fusion of
Pipermail (Mailman edition) and