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

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.

Q2:
value "hd []";
and
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,

Best,
Bart

--
http://bartk.nl/

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

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.