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

I am playing with defining some recursive functions and proving their properties, I don't understand some of what I am seeing. The following questions, I think, will help me move in the right direction.

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. 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.

value "hd []";
normal_form "hd []";
evaluate to themselves.  So does
value "if true then [2,3] else [4,5]"

How do I force evaluation of those? The first I have no idea what it should evaluate to; the last should be [2,3].

Thanks for any help,



@kasterma, http://twitter.com/kasterma
 Werner Herzog: the birds here ... they don't sing ... they scream in

blaginations, http://kasterma.wordpress.com
 A Better Tea Timer (version 0.1).

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