src/HOLCF/Fix.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5192 704dd3a6d47d
child 10834 a7897aebbffc
permissions -rw-r--r--
tidying
slotosch@2640
     1
(*  Title:      HOLCF/Fix.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993  Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
nipkow@243
     7
definitions for fixed point operator and admissibility
nipkow@243
     8
nipkow@243
     9
*)
nipkow@243
    10
nipkow@243
    11
Fix = Cfun3 +
nipkow@243
    12
nipkow@243
    13
consts
nipkow@243
    14
oheimb@1990
    15
iterate	:: "nat=>('a->'a)=>'a=>'a"
oheimb@1990
    16
Ifix	:: "('a->'a)=>'a"
oheimb@1990
    17
fix	:: "('a->'a)->'a"
nipkow@2841
    18
adm		:: "('a::cpo=>bool)=>bool"
oheimb@1990
    19
admw		:: "('a=>bool)=>bool"
nipkow@243
    20
berghofe@5192
    21
primrec
berghofe@5192
    22
  iterate_0   "iterate 0 F x = x"
berghofe@5192
    23
  iterate_Suc "iterate (Suc n) F x  = F`(iterate n F x)"
berghofe@5192
    24
regensbu@1168
    25
defs
nipkow@243
    26
wenzelm@3842
    27
Ifix_def      "Ifix F == lub(range(%i. iterate i F UU))"
regensbu@1168
    28
fix_def       "fix == (LAM f. Ifix f)"
nipkow@243
    29
oheimb@4721
    30
adm_def       "adm P == !Y. chain(Y) --> 
wenzelm@3842
    31
                        (!i. P(Y i)) --> P(lub(range Y))"
nipkow@243
    32
wenzelm@3842
    33
admw_def      "admw P == !F. (!n. P (iterate n F UU)) -->
clasohm@1479
    34
                            P (lub(range (%i. iterate i F UU)))" 
nipkow@243
    35
nipkow@243
    36
end
nipkow@243
    37