Re: [isabelle] Function definition



Dear Ed,

as Manuel indicated, you'll likely have to define your function in
another way.

One way would be to use mutual recursion:

function (sequential)
  interesting :: "nat â t â t" and
  boring :: "nat â t â t"
where
  "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.

lemma [termination_simp]:
  shows "interesting_boring_dom (Inl (k, t)) â size (interesting k t) =
size 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:

lemma
  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

cheers

chris

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.
> 
> Cheers,
> 
> Manuel
> 




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