# Re: [isabelle] induction for mutually recursive functions

```Hi Viorel,

```
```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.
```
```
```
The two versions are actually equivalent, so one should be provable when the other is. Unfortunately, the equation "na = n" seems to be oriented in an unfortunate way, such that the simplifier does not help you here...
```
```
Note that here you are relying on a feature of the induct method to do induction over non-variable terms, which introduces equations on the fly (which you already see in the simplified form; if you add (no_simp) after "induct", you see where they come from).
```
```
You can avoid this situation altogether by using currying instead of tuple arguments in your function definition, which is generally recommended:
```
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

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)"
```
apply (induct n and n k s and n k s rule: init_fun_loop_fun_final_fun.induct)
```

Hope this helps...

Alex

```

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