[isabelle] redundant equations and inconsistent function errors



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




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