src/HOLCF/Fix.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5192 704dd3a6d47d
child 10834 a7897aebbffc
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/Fix.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 
     7 definitions for fixed point operator and admissibility
     8 
     9 *)
    10 
    11 Fix = Cfun3 +
    12 
    13 consts
    14 
    15 iterate	:: "nat=>('a->'a)=>'a=>'a"
    16 Ifix	:: "('a->'a)=>'a"
    17 fix	:: "('a->'a)->'a"
    18 adm		:: "('a::cpo=>bool)=>bool"
    19 admw		:: "('a=>bool)=>bool"
    20 
    21 primrec
    22   iterate_0   "iterate 0 F x = x"
    23   iterate_Suc "iterate (Suc n) F x  = F`(iterate n F x)"
    24 
    25 defs
    26 
    27 Ifix_def      "Ifix F == lub(range(%i. iterate i F UU))"
    28 fix_def       "fix == (LAM f. Ifix f)"
    29 
    30 adm_def       "adm P == !Y. chain(Y) --> 
    31                         (!i. P(Y i)) --> P(lub(range Y))"
    32 
    33 admw_def      "admw P == !F. (!n. P (iterate n F UU)) -->
    34                             P (lub(range (%i. iterate i F UU)))" 
    35 
    36 end
    37