equal
deleted
inserted
replaced
28 b1 :: "'a -> tr" |
28 b1 :: "'a -> tr" |
29 b2 :: "'a -> tr" |
29 b2 :: "'a -> tr" |
30 g :: "'a -> 'a" |
30 g :: "'a -> 'a" |
31 |
31 |
32 definition |
32 definition |
33 p :: "'a -> 'a" |
33 p :: "'a -> 'a" where |
34 "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x fi)" |
34 "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x fi)" |
35 |
35 |
36 q :: "'a -> 'a" |
36 definition |
|
37 q :: "'a -> 'a" where |
37 "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x fi)" |
38 "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x fi)" |
38 |
39 |
39 |
40 |
40 (* --------- pure HOLCF logic, some little lemmas ------ *) |
41 (* --------- pure HOLCF logic, some little lemmas ------ *) |
41 |
42 |