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



In higher-order logic, as in first-order logic, all functions are total. This is a fact of model theory. It doesn't imply that a partial function is “made total” in any explicit way, and it is obvious that no uniform definition of hd[] is possible. All that you can say for certain is that this value has the correct type and is equal to itself.
Larry Paulson


On 2 Sep 2010, at 20:31, Bart Kastermans wrote:

> 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.  thm hd_def gives information on where to look, but that theory file (SList.thy) is apparently only for "historical interest".  This makes me think there should be a better way to find out how this function is made total.






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