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.