Re: [isabelle] Nested Recursion inside a tuple

Thanks Alex. My own experience with such datatypes indicates that fun leads to simpler proofs because its induction principles avoid simultaneous inductions over lists.


Alexander Krauss schrieb:
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:

  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"

  "subst s (Var x) = s x"
  "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

subst :: "('v => ('v,'f)term) => ('v,'f)term => ('v,'f)term"
  "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.


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