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