Re: [isabelle] Two questions: one on "primrec hd" one on "value/normal_form"



Just as an additional remark: the automatic tools like "value" and the simplifier are configures to operate only with the defining equations given by the user and not the implicitly added "lhs = undfined" ones. But by resorting to the internal definition it is always possible to drag "undefined" to the surface.

Tobias

Am 02/09/2010 21:48, schrieb Florian Haftmann:
Hi Bart,

value "if true then [2,3] else [4,5]"

try
   value "if True then [2,3] else [4,5]"
instead (all clear? ;-))

Q1:
In HOL/List.thy we see the definition:

primrec
   hd :: "'a list =>  'a" where
   "hd (x # xs) = x"

The tutorial states all functions defined this way must be total, so
somehow hd is made total.

Well, functions *are* total due to the very nature of the logic.  In the
case of missing patterns for primrec, the missing cases are just filled
with an (unspecified) constant "undefined".  This appears in the
primitive definition of hd, inspectible using

   thm hd_def

 From this you could even derive "hd [] = undefined" manually.

Q2:
value "hd []";
and
normal_form "hd []";
evaluate to themselves.  So does

value and normal_form&co. use equational theorems as rewrite rules,
which you can inspect using

   code_thms hd

Since there is no rule for "hd []", it is not rewritten.

Hope this helps,
	Florian






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