# [isabelle] induction for mutually recursive functions

*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] induction for mutually recursive functions
*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>
*Date*: Mon, 05 Sep 2011 15:08:19 +0300
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:6.0) Gecko/20110812 Thunderbird/6.0

Hello,
I have the following mutually recursive function definition
function
init_fun :: "nat => nat * nat * nat"
and loop_fun :: "nat * nat * nat => nat * nat * nat"
and final_fun :: "nat * nat * nat => nat * nat * nat"
where
"init_fun n = loop_fun (n, 0, 0)" |
"loop_fun (n, k, s) = (if k < n then loop_fun (n, k + 1, s + k + 1)
else if k = n then final_fun (n, k, s)
else (n, k, s))"|
"final_fun (n, k, s) = (n, k, s)"
by pat_completeness auto
termination

` apply (relation "measure (% x. case x of Inl n => n + 3 | Inr (Inl
``(n, k, s)) => n - k + 2 | Inr (Inr (n, k, s)) => n - k + 1)")
` by auto
Asumming that Testa, Testb, Testc, and Test are defined I want to prove by
(mutual) induction:
theorem TestInduction:
"Testa n ==> Test (init_fun n)"
"Testb n k s ==> Test (loop_fun (n, k, s))"
"Testc n k s ==> Test (final_fun (n, k, s))"
If I try

`apply (induct n and "(n, k, s)" and "(n, k, s)" rule:
``init_fun_loop_fun_final_fun.induct)
`
I get something that is unprovable:

`1. [| [| na = n; 0 = k; 0 = s; Testb n k s|] ==> Test (loop_fun (n, k,
``s)); Testa na |] ==> Test (init_fun na)
`2. ...
3. ...
I would expect something like:

`1. [| [| Testb na 0 0|] ==> Test (loop_fun (na, 0, 0)); Testa na |] ==>
``Test (init_fun na)
`2. ...
3. ...
that I can prove using the definition of the Test predicates.
Best regards,
Viorel Preoteasa

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