src/HOLCF/ex/Loop.thy
author slotosch
Mon Feb 17 11:04:00 1997 +0100 (1997-02-17)
changeset 2642 3c3a84cc85a9
parent 1479 21eb5e156d91
child 10835 f4745d77e620
permissions -rw-r--r--
Examples are adopted to the changes from HOLCF.
Classlib is reduced.
Classlib still uses arities, Classlib will change completely to new
classes of ADTs
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
slotosch@2642
     9
Loop = Tr +
nipkow@244
    10
nipkow@244
    11
consts
clasohm@1479
    12
        step  :: "('a -> tr)->('a -> 'a)->'a->'a"
clasohm@1479
    13
        while :: "('a -> tr)->('a -> 'a)->'a->'a"
nipkow@244
    14
regensbu@1168
    15
defs
nipkow@244
    16
clasohm@1479
    17
  step_def      "step == (LAM b g x. If b`x then g`x else x fi)"
clasohm@1479
    18
  while_def     "while == (LAM b g. fix`(LAM f x.
regensbu@1168
    19
                   If b`x then f`(g`x) else x fi))"
nipkow@244
    20
nipkow@244
    21
end
nipkow@244
    22