*To*: TIMOTHY KREMANN <twksoa262 at verizon.net>*Subject*: Re: [isabelle] Isabelle HOL Tutorial Exercise Answers*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 17 Apr 2008 12:51:17 +0200*Cc*: Mailing List Isabelle <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <108035.73744.qm@web84006.mail.mud.yahoo.com>*References*: <108035.73744.qm@web84006.mail.mud.yahoo.com>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

Tobias TIMOTHY KREMANN wrote:

Cheers, Has someone compiled answers to the Tutorial's exercises? I am particularly having trouble with 3.4.1 Here is what I have so far? Am I getting close? primrec "norma (IF b a1 a2) = normifb (normb b) (norma a1) (norma a2)" "norma (Sum a1 a2) = Sum (norma a1) (norma a2)" "norma (Diff a1 a2) = Diff (norma a1) (norma a2)" "norma (Var v) = Var v" "norma (Num n) = Num n" "normb (Less a1 a2) = Less (norma a1) (norma a2)" "normb (And b1 b2) = And (normb b1) (normb b2)" "normb (Neg b) = Neg (normb b)" primrec "normifa (IF b a1 a2) = (normifb b (normifa a1) (normifa a2))" "normifa (Sum a1 a2) = Sum (normifa a1) (normifa a2)" "normifa (Diff a1 a2) = Diff (normifa a1) (normifa a2)" "normifa (Var v) = Var v" "normifa (Num n) = Num n" "normifb (Less a1 a2) t e = IF (Less (normifa a1) (normifa a2)) t e" "normifb (And b1 b2) t e = (normifb b1 (normifb b2 t e) e)" "normifb (Neg b) t e = (normifb b e t)"

**References**:**[isabelle] Isabelle HOL Tutorial Exercise Answers***From:*TIMOTHY KREMANN

- Previous by Date: Re: [isabelle] *** exception ValueMissing raised
- Next by Date: [isabelle] About simplificaton
- Previous by Thread: [isabelle] Isabelle HOL Tutorial Exercise Answers
- Next by Thread: [isabelle] [BUG?] value not working on an expression resulting in "True"
- Cl-isabelle-users April 2008 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