Re: [isabelle] redundant equations and inconsistent function errors



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

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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