[isabelle] Nested Recursion inside a tuple



Dear Isabelle users,

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).

Is there anyway we can define this kind of nested recursion?
Thank you very much in advance for any tips,

Ricardo Peña and Leonor Prensa


-------------------------------------

theory Problem
imports Main
begin

datatype ('v,'f)"term" = Var 'v | App 'f "(('v,'f)term \<times> nat) list"

consts
subst :: "('v => ('v,'f)term) => ('v,'f)term => ('v,'f)term"

substs:: "('v => ('v,'f)term) => (('v,'f)term \<times> nat) list => (('v,'f)term \<times> nat) list"

primrec

"subst s (Var x) = s x"

subst_App:
"subst s (App f ts) = App f (substs s ts)"
"substs s [] = []"
"substs s (t # ts) = (case t of (t', n) => (subst s t', n) # substs s ts)"

end

---------------------------------------

*** Entity to be defined occurs on rhs
*** The error(s) above occurred in definition "subst_term_def":
*** "subst õ∫
*** õla b. term_rec_1 (õlx s. s x) (õlf ts tsa s. App f (tsa s)) (õls. [])
*** (õlt ts ta tsa s. case t of (t', n) õfi (subst s t', n) # tsa s) undefined b a"
*** At command "primrec".





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