src/HOLCF/Fix.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12030 46d57d0290a2
child 15576 efb95d0d01f7
permissions -rw-r--r--
Merged in license change from Isabelle2004
     1 (*  Title:      HOLCF/Fix.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4 
     5 definitions for fixed point operator and admissibility
     6 *)
     7 
     8 Fix = Cfun3 +
     9 
    10 consts
    11 
    12 iterate	:: "nat=>('a->'a)=>'a=>'a"
    13 Ifix	:: "('a->'a)=>'a"
    14 fix	:: "('a->'a)->'a"
    15 adm		:: "('a::cpo=>bool)=>bool"
    16 admw		:: "('a=>bool)=>bool"
    17 
    18 primrec
    19   iterate_0   "iterate 0 F x = x"
    20   iterate_Suc "iterate (Suc n) F x  = F$(iterate n F x)"
    21 
    22 defs
    23 
    24 Ifix_def      "Ifix F == lub(range(%i. iterate i F UU))"
    25 fix_def       "fix == (LAM f. Ifix f)"
    26 
    27 adm_def       "adm P == !Y. chain(Y) --> 
    28                         (!i. P(Y i)) --> P(lub(range Y))"
    29 
    30 admw_def      "admw P == !F. (!n. P (iterate n F UU)) -->
    31                             P (lub(range (%i. iterate i F UU)))" 
    32 
    33 end
    34