doc-src/Tutorial/Ifexpr/Exercise.thy
 changeset 5377 efb799c5ed3c
equal inserted replaced
5376:60b31a24f1a6 5377:efb799c5ed3c
`       `
`     1 Exercise = Main +`
`       `
`     2 datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex`
`       `
`     3 consts valif :: ifex => (nat => bool) => bool`
`       `
`     4 primrec valif ifex`
`       `
`     5 "valif (CIF b)    env = b"`
`       `
`     6 "valif (VIF x)    env = env x"`
`       `
`     7 "valif (IF b t e) env = (if valif b env then valif t env`
`       `
`     8                                         else valif e env)"`
`       `
`     9 consts normif :: ifex => ifex => ifex => ifex`
`       `
`    10 primrec normif ifex`
`       `
`    11 "normif (CIF b)    t e = (if b then t else e)"`
`       `
`    12 "normif (VIF x)    t e = IF (VIF x) t e"`
`       `
`    13 "normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"`
`       `
`    14 consts norm :: ifex => ifex`
`       `
`    15 primrec norm ifex`
`       `
`    16 "norm (CIF b)    = CIF b"`
`       `
`    17 "norm (VIF x)    = VIF x"`
`       `
`    18 "norm (IF b t e) = normif b (norm t) (norm e)"`
`       `
`    19 consts normal :: ifex => bool`
`       `
`    20 primrec normal ifex`
`       `
`    21 "normal(CIF b) = True"`
`       `
`    22 "normal(VIF x) = True"`
`       `
`    23 "normal(IF b t e) = (normal t & normal e &`
`       `
`    24       (case b of CIF b => False | VIF x => True | IF x y z => False))"`
`       `
`    25 end`