Email Gateway (Aug 18 2022 at 12:02): Email Gateway (Aug 18 2022 at 12:02):From: Leonor Prensa <leonor.prensa@loria.fr>
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".
Email Gateway (Aug 18 2022 at 12:04):From: Alexander Krauss <krauss@in.tum.de>
Dear Leonor and Ricardo,
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
Email Gateway (Aug 18 2022 at 12:06):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks Alex. My own experience with such datatypes indicates that fun
leads to simpler proofs because its induction principles avoid
simultaneous inductions over lists.
Tobias
Alexander Krauss schrieb:
Last updated: May 03 2024 at 08:18 UTC