Re: [isabelle] undefined & None



> > "undefined" is frequently used by packages (primrec, function,
> > partial_function) in cases where the user has not given a full
> > specification of a constant.
> 
> I am not sure how widespread this usage still is in Isabelle. But where
> it happens, I consider it a (minor) shortcoming, because it leads to
> spurious equations: the user arguably never intended to specify that,
> e.g., "hd [] = last []".
> 

However, this comes in handy in some cases. Consider, e.g., the
following lemma:

lemma map_eq_nth_eq:
  assumes A: "map f l = map f l'" 
  shows "f (l!i) = f (l'!i)"


without knowing that nth is undefined if the index is out of bounds,
this lemma would have a precondition (i<length l) which makes it harder
to be used by the simplifier.

--
  Peter






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