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

Hi Bart,

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

  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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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