src/HOLCF/Fix.thy
changeset 1990 9e23119c0219
parent 1825 88d4c33d7947
child 2275 dbce3dce821a
equal deleted inserted replaced
1989:8e0ff1bfcfea 1990:9e23119c0219
    10 
    10 
    11 Fix = Cfun3 +
    11 Fix = Cfun3 +
    12 
    12 
    13 consts
    13 consts
    14 
    14 
    15 iterate :: "nat=>('a->'a)=>'a=>'a"
    15 iterate	:: "nat=>('a->'a)=>'a=>'a"
    16 Ifix    :: "('a->'a)=>'a"
    16 Ifix	:: "('a->'a)=>'a"
    17 fix     :: "('a->'a)->'a"
    17 fix	:: "('a->'a)->'a"
    18 adm          :: "('a=>bool)=>bool"
    18 adm		:: "('a=>bool)=>bool"
    19 admw         :: "('a=>bool)=>bool"
    19 admw		:: "('a=>bool)=>bool"
    20 chain_finite :: "'a=>bool"
    20 chain_finite	:: "'a=>bool"
    21 is_flat         :: "'a=>bool"
    21 is_flat		:: "'a=>bool" (* should be called flat, for consistency *)
    22 
    22 
    23 defs
    23 defs
    24 
    24 
    25 iterate_def   "iterate n F c == nat_rec c (%n x.F`x) n"
    25 iterate_def   "iterate n F c == nat_rec c (%n x.F`x) n"
    26 Ifix_def      "Ifix F == lub(range(%i.iterate i F UU))"
    26 Ifix_def      "Ifix F == lub(range(%i.iterate i F UU))"