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