src/HOLCF/ex/Loop.thy
 author clasohm Tue Feb 06 12:42:31 1996 +0100 (1996-02-06) changeset 1479 21eb5e156d91 parent 1274 ea0668a1c0ba child 2642 3c3a84cc85a9 permissions -rw-r--r--
expanded tabs
 clasohm@1479 ` 1` ```(* Title: HOLCF/ex/Loop.thy ``` nipkow@244 ` 2` ``` ID: \$Id\$ ``` clasohm@1479 ` 3` ``` Author: Franz Regensburger ``` clasohm@1479 ` 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` clasohm@1479 ` 13` ``` step :: "('a -> tr)->('a -> 'a)->'a->'a" ``` clasohm@1479 ` 14` ``` while :: "('a -> tr)->('a -> 'a)->'a->'a" ``` nipkow@244 ` 15` regensbu@1168 ` 16` ```defs ``` nipkow@244 ` 17` clasohm@1479 ` 18` ``` step_def "step == (LAM b g x. If b`x then g`x else x fi)" ``` clasohm@1479 ` 19` ``` while_def "while == (LAM b g. fix`(LAM f x. ``` regensbu@1168 ` 20` ``` If b`x then f`(g`x) else x fi))" ``` nipkow@244 ` 21` nipkow@244 ` 22` ```end ``` nipkow@244 ` 23` ``` ```