src/HOLCF/fix.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
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=>bool)=>bool"
    19 admw         :: "('a=>bool)=>bool"
    20 chain_finite :: "'a=>bool"
    21 flat         :: "'a=>bool"
    22 
    23 rules
    24 
    25 iterate_def   "iterate(n,F,c) == nat_rec(n,c,%n x.F[x])"
    26 Ifix_def      "Ifix(F) == lub(range(%i.iterate(i,F,UU)))"
    27 fix_def       "fix == (LAM f. Ifix(f))"
    28 
    29 adm_def       "adm(P) == !Y. is_chain(Y) --> \
    30 \                        (!i.P(Y(i))) --> P(lub(range(Y)))"
    31 
    32 admw_def      "admw(P)== (!F.((!n.P(iterate(n,F,UU)))-->\
    33 \			 P(lub(range(%i.iterate(i,F,UU))))))" 
    34 
    35 chain_finite_def  "chain_finite(x::'a)==\
    36 \                        !Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y))"
    37 
    38 flat_def          "flat(x::'a) ==\
    39 \                        ! x y. x::'a << y --> (x = UU) | (x=y)"
    40 
    41 end
    42