doc-src/Tutorial/Ifexpr/Exercise.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/Exercise.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,25 @@
+Exercise = Main +
+datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
+consts valif :: ifex => (nat => bool) => bool
+primrec valif ifex
+"valif (CIF b)    env = b"
+"valif (VIF x)    env = env x"
+"valif (IF b t e) env = (if valif b env then valif t env
+                                        else valif e env)"
+consts normif :: ifex => ifex => ifex => ifex
+primrec normif ifex
+"normif (CIF b)    t e = (if b then t else e)"
+"normif (VIF x)    t e = IF (VIF x) t e"
+"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"
+consts norm :: ifex => ifex
+primrec norm ifex
+"norm (CIF b)    = CIF b"
+"norm (VIF x)    = VIF x"
+"norm (IF b t e) = normif b (norm t) (norm e)"
+consts normal :: ifex => bool
+primrec normal ifex
+"normal(CIF b) = True"
+"normal(VIF x) = True"
+"normal(IF b t e) = (normal t & normal e &
+      (case b of CIF b => False | VIF x => True | IF x y z => False))"
+end