Re: [isabelle] Function definition
as Manuel indicated, you'll likely have to define your function in
One way would be to use mutual recursion:
interesting :: "nat â t â t" and
boring :: "nat â t â t"
"interesting k (N n) = N (n + k)"
| "interesting k (A t) = A (interesting (k + 1) t)"
| "interesting k t = boring k t"
| "boring k (N n) = N n"
| "boring k (A t) = A (interesting k (boring k t))"
| "boring k (B t1 t2) = B (interesting k (boring k t1)) (interesting k
(boring k t2))"
by (pat_completeness) auto
where your "boring" is replaced by a variant that only takes "k" as
parameter. Then we can prove that both functions are size-preserving, as
already suggested by Manuel.
shows "interesting_boring_dom (Inl (k, t)) â size (interesting k t) =
and "interesting_boring_dom (Inr (k, t)) â size (boring k t) = size t"
by (induct k t and k t rule: interesting_boring.pinduct)
(simp_all add: interesting.psimps boring.psimps)
Which incidentally suffices for termination:
termination by (lexicographic_order)
It remains to show that this actually corresponds to your original
function specification. Here, I use "boring'" for your "boring".
fun boring' :: "(t â t) â t â t" where
"boring' f (N n) = N n"
| "boring' f (A t) = A (f (boring' f t))"
| "boring' f (B t1 t2) = B (f (boring' f t1)) (f (boring' f t2))"
Your definition of "interesting" (modulo "case" on the right vs.
pattern-matching on the left) can be obtained by mutual induction:
shows "interesting k s =
(case s of
N n â N (n + k)
| A t â A (interesting (k + 1) t)
| t â boring' (interesting k) t)"
and "boring k s = boring' (interesting k) s"
by (induct k s and k s rule: interesting_boring.induct) auto
PS: For those who care and know what I'm talking about: termination of
the TRS corresponding to "interesting" and "boring" is trivial for
modern termination tools. Maybe a reason to revive IsaFoR/TermFun? ;)
On 09/27/2016 10:52 AM, Manuel Eberl wrote:
> Unfortunately, it's not that easy.
> You pass the "interesting" function to the "boring" function as a
> parameter, and the "boring" function applies that function that it is
> given to things. In order for this to work, you need to essentially show
> that the "interesting" function that you are defining is only called on
> values for which it terminates (i.e. that are smaller than the original
> argument that it got)
> Normally, this is done with a fundef_cong rule, but in this case, I
> don't see how that is possible, because the values that "interesting" is
> called on by "boring" are "boring f t1" and "boring f t2" â that means
> that you are relying on the fact that the "interesting" function does
> not increase the size of its argument.
> Showing that "interesting" is size-preserving is actually straightforward:
> lemma same_size_boring:
> assumes "ây. size (f y) = size y"
> shows "size (boring f x) = size x"
> using assms by (induction x) simp_all
> lemma size_interesting_aux:
> assumes "interesting_dom (k, t)"
> shows "size (interesting k t) = size t"
> using assms
> by (induction rule: interesting.pinduct) (simp_all add:
> interesting.psimps same_size_boring)
> However, I have no idea how you would then go on and prove termination.
> Termination proofs depend on the call graph that is computed for the
> recursive definition, and if you don't have a fundef_cong rule for
> boring, that call graph â as you discovered yourself â will be too
> coarse (i.e. you will not have the information that you need in your
> termination proof). However, as I see it, any cong rule for "boring"
> would have to be conditional, which is, as far as I am aware, not
> possible for fundef_cong rules.
> What you are trying to do may therefore very well be outside of what the
> function package can do. (although I'm not 100% sure about that â still,
> even if it is possible, I would bet it will be ugly)
> My advice would be: try to define your functions in a simpler way.
> Proofs involving nested recursion tend to get very ugly very quickly,
> because the termination of your function depends on the semantics of
> your function, and semantic properties are difficult to use without a
> full termination proof.
This archive was generated by a fusion of
Pipermail (Mailman edition) and