src/HOLCF/ex/Loop.thy
 author nipkow Wed Jan 19 17:40:26 1994 +0100 (1994-01-19) changeset 244 929fc2c63bd0 child 1150 66512c9e6bd6 permissions -rw-r--r--
HOLCF examples
 nipkow@244 ` 1` ```(* Title: HOLCF/ex/loop.thy ``` nipkow@244 ` 2` ``` ID: \$Id\$ ``` nipkow@244 ` 3` ``` Author: Franz Regensburger ``` nipkow@244 ` 4` ``` Copyright 1993 Technische Universitaet Muenchen ``` nipkow@244 ` 5` nipkow@244 ` 6` ```Theory for a loop primitive like while ``` nipkow@244 ` 7` ```*) ``` nipkow@244 ` 8` nipkow@244 ` 9` ```Loop = Tr2 + ``` nipkow@244 ` 10` nipkow@244 ` 11` ```consts ``` nipkow@244 ` 12` nipkow@244 ` 13` ``` step :: "('a -> tr)->('a -> 'a)->'a->'a" ``` nipkow@244 ` 14` ``` while :: "('a -> tr)->('a -> 'a)->'a->'a" ``` nipkow@244 ` 15` nipkow@244 ` 16` ```rules ``` nipkow@244 ` 17` nipkow@244 ` 18` ``` step_def "step == (LAM b g x. If b[x] then g[x] else x fi)" ``` nipkow@244 ` 19` ``` while_def "while == (LAM b g. fix[LAM f x.\ ``` nipkow@244 ` 20` ```\ If b[x] then f[g[x]] else x fi])" ``` nipkow@244 ` 21` nipkow@244 ` 22` nipkow@244 ` 23` ```end ``` nipkow@244 ` 24` ``` ```