Re: [isabelle] Nested Recursion inside a tuple

[Alexander Krauss <krauss at in.tum.de>]

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