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.
Am 02/09/2010 21:48, schrieb Florian Haftmann:
value "if true then [2,3] else [4,5]"
value "if True then [2,3] else [4,5]"
instead (all clear? ;-))
In HOL/List.thy we see the definition:
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
From this you could even derive "hd  = undefined" manually.
value "hd ";
normal_form "hd ";
evaluate to themselves. So does
value and normal_form&co. use equational theorems as rewrite rules,
which you can inspect using
Since there is no rule for "hd ", it is not rewritten.
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and