# Re: [isabelle] Nested Recursion inside a tuple

```Dear Leonor and Ricardo,

```
```we are trying to define a function that uses nested primitive recursion
but we get the error below. We reproduce the error by using
the example in the tutorial where the recursion is inside a list and inside
a tuple (this seems to be the problem).
```
```
```
Primrec requires that you define a separate function for the pair. The following works:
```
consts
subst :: "('v => ('v,'f)term) => ('v,'f)term => ('v,'f)term"
```
substs:: "('v => ('v,'f)term) => (('v,'f)term × nat) list => (('v,'f)term × nat) list"
```  substp:: "('v => ('v,'f)term) => ('v,'f)term × nat => ('v,'f)term × nat"

primrec
"subst s (Var x) = s x"
subst_App:
"subst s (App f ts) = App f (substs s ts)"
"substs s [] = []"
"substp s (t,n) = (subst s t, n)"
"substs s (t # ts) = (substp s t # substs s ts)"

```
Instead of primrec, you could also use function/fun, which is more liberal. For example:
```
```
lemma term_size[simp]: "(a, b) : set ts ==> size a < Suc term_nat_x_list_size ts)"
```by (induct ts) auto

fun
subst :: "('v => ('v,'f)term) => ('v,'f)term => ('v,'f)term"
where
"subst s (Var x) = s x"
| "subst s (App f ts) = App f (map (%(t,n). (subst s t, n)) ts)"

```
The funny lemma about size is still required in Isabelle 2007, but will be unnecessary in the next version.
```
Alex

```

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