src/HOLCF/ex/Loop.thy
author huffman
Sat Jun 04 02:24:47 2005 +0200 (2005-06-04)
changeset 16232 8a12e11d222b
parent 14981 e73f8140af78
child 17291 94f6113fe9ed
permissions -rw-r--r--
added explicit dependency on Fix theory
clasohm@1479
     1
(*  Title:      HOLCF/ex/Loop.thy
nipkow@244
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
nipkow@244
     4
nipkow@244
     5
Theory for a loop primitive like while
nipkow@244
     6
*)
nipkow@244
     7
huffman@16232
     8
Loop = Tr + Fix +
nipkow@244
     9
nipkow@244
    10
consts
clasohm@1479
    11
        step  :: "('a -> tr)->('a -> 'a)->'a->'a"
clasohm@1479
    12
        while :: "('a -> tr)->('a -> 'a)->'a->'a"
nipkow@244
    13
regensbu@1168
    14
defs
nipkow@244
    15
nipkow@10835
    16
  step_def      "step == (LAM b g x. If b$x then g$x else x fi)"
nipkow@10835
    17
  while_def     "while == (LAM b g. fix$(LAM f x.
nipkow@10835
    18
                   If b$x then f$(g$x) else x fi))"
nipkow@244
    19
nipkow@244
    20
end
nipkow@244
    21