equal
deleted
inserted
replaced
1 (* Title: HOLCF/ex/Loop.thy |
1 (* Title: HOLCF/ex/Loop.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 |
|
5 Theory for a loop primitive like while |
|
6 *) |
4 *) |
7 |
5 |
8 Loop = Tr + Fix + |
6 header {* Theory for a loop primitive like while *} |
9 |
7 |
10 consts |
8 theory Loop |
11 step :: "('a -> tr)->('a -> 'a)->'a->'a" |
9 imports HOLCF |
12 while :: "('a -> tr)->('a -> 'a)->'a->'a" |
10 begin |
13 |
11 |
14 defs |
12 constdefs |
|
13 step :: "('a -> tr)->('a -> 'a)->'a->'a" |
|
14 "step == (LAM b g x. If b$x then g$x else x fi)" |
|
15 while :: "('a -> tr)->('a -> 'a)->'a->'a" |
|
16 "while == (LAM b g. fix$(LAM f x. |
|
17 If b$x then f$(g$x) else x fi))" |
15 |
18 |
16 step_def "step == (LAM b g x. If b$x then g$x else x fi)" |
19 ML {* use_legacy_bindings (the_context ()) *} |
17 while_def "while == (LAM b g. fix$(LAM f x. |
|
18 If b$x then f$(g$x) else x fi))" |
|
19 |
20 |
20 end |
21 end |
21 |
22 |