# Re: [isabelle] Isabelle HOL Tutorial Exercise Answers

My solution looks very similar, but I have managed to fold your two norma and normb functions into 1 function each. Hence I cannot say for sure if your proposal is correct. But as I said, basically it looks good.
```
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)"
```
```

```

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