Email Gateway (Aug 18 2022 at 17:40): Email Gateway (Aug 18 2022 at 17:40):From: Anh Le <anhlevn@cims.nyu.edu>
Hi everyone,
I am reading some Isabelle code (proving type safety of Featherweight Java).
A primitive recursion is defined below, where the function subst_list is
defined twice, exactly the same, with two different names: subst_list1 and
subst_list2.
I though it was redundant and removes one of them, and renamed the other to
subst_list. But then Isabelle showed an error, which is inconsistent
function error.
So my question is why isabelle requires those duplicated equations? is there
any way that we can just define only one function subst_list?
Thank you very much
Anh
primrec
substs :: "(varName \<rightharpoonup> exp) \<Rightarrow> exp \<Rightarrow>
exp"
and subst_list1 :: "(varName \<rightharpoonup> exp) \<Rightarrow> exp list
\<Rightarrow> exp list"
and subst_list2 :: "(varName \<rightharpoonup> exp) \<Rightarrow> exp list
\<Rightarrow> exp list"
where
"substs sub (Var x) = (case (sub(x)) of None \<Rightarrow> (Var x) | Some
p \<Rightarrow> p)" |
"substs sub (FieldProj e f) = FieldProj(substs sub e) f" |
"substs sub (MethodInvk e m es) = MethodInvk (substs sub e) m
(subst_list1 sub es)" |
"substs sub (New C es) = New C (subst_list2 sub es)" |
"substs sub (Cast C e) = Cast C (substs sub e)" |
"subst_list1 sub [] = []" |
"subst_list2 sub (h # t) = (substs sub h) # (subst_list sub t)" |
"subst_list2 sub [] = []" |
"subst_list2 sub (h # t) = (substs sub h) # (subst_list2 sub t)"
Email Gateway (Aug 18 2022 at 17:40):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Anh,
restrictions of the primrec and datatype package is the reason for two versions
of subst_list. As I gather from the function definition of substs, the exp
datatype looks something like this:
datatype exp
= Var vname
| FieldProj exp fname
| MethodInvk exp mname "exp list"
| New cname "exp list"
| Cast cname exp
The problem here is that the two constructors MethodInvk and New both take a
list of expressions. The datatype package unfolds nested recursion in datatype
declarations into primitive recursion by mutual recursion, see Section 3.4.2 of
the Isabelle/HOL tutorial. Since nested recursion occurs twice, the datatype
package inlines the list datatype twice. This can also be seen in the induction
rule foo.induct and the recursion combinators foo_rec_1, foo_rec_2 and foo_rec3.
primrec expects the function definition to strictly follow the induction rule
and the recursion combinators. Hence, there must be two definitions of subst_list.
The fun command allows more general recursion. By replacing primrec with fun,
you may get rid of the duplicated subst_list functions. fun also proves an
induction rule for proofs about substs.
Andreas
Anh Le schrieb:
Last updated: Nov 21 2024 at 12:39 UTC