# [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.