*To*: Bart Kastermans <Bart.Kastermans at Colorado.EDU>*Subject*: Re: [isabelle] Two questions: one on "primrec hd" one on "value/normal_form"*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 02 Sep 2010 22:09:00 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4C7FFF9F.5090204@informatik.tu-muenchen.de>*References*: <alpine.DEB.2.00.1009021323460.27300@kasterma.Colorado.EDU> <4C7FFF9F.5090204@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.6; de; rv:1.9.2.8) Gecko/20100802 Thunderbird/3.1.2

Tobias Am 02/09/2010 21:48, schrieb Florian Haftmann:

Hi Bart,value "if true then [2,3] else [4,5]"try 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 doesvalue 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, Florian

**References**:**[isabelle] Two questions: one on "primrec hd" one on "value/normal_form"***From:*Bart Kastermans

**Re: [isabelle] Two questions: one on "primrec hd" one on "value/normal_form"***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] sets in HOL/CF
- Next by Date: Re: [isabelle] Two questions: one on "primrec hd" one on "value/normal_form"
- Previous by Thread: Re: [isabelle] Two questions: one on "primrec hd" one on "value/normal_form"
- Next by Thread: Re: [isabelle] Two questions: one on "primrec hd" one on "value/normal_form"
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list