[isabelle] Isabelle HOL Tutorial Exercise Answers



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.