src/HOLCF/Fix.thy
author clasohm
Wed Jun 29 12:03:41 1994 +0200 (1994-06-29)
changeset 442 13ac1fd0a14d
parent 243 c22b85994e17
child 1150 66512c9e6bd6
permissions -rw-r--r--
added parentheses made necessary by change of constrain's precedence
nipkow@243
     1
(*  Title: 	HOLCF/fix.thy
nipkow@243
     2
    ID:         $Id$
nipkow@243
     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
nipkow@243
    15
iterate :: "nat=>('a->'a)=>'a=>'a"
nipkow@243
    16
Ifix    :: "('a->'a)=>'a"
nipkow@243
    17
fix     :: "('a->'a)->'a"
nipkow@243
    18
adm          :: "('a=>bool)=>bool"
nipkow@243
    19
admw         :: "('a=>bool)=>bool"
nipkow@243
    20
chain_finite :: "'a=>bool"
nipkow@243
    21
flat         :: "'a=>bool"
nipkow@243
    22
nipkow@243
    23
rules
nipkow@243
    24
nipkow@243
    25
iterate_def   "iterate(n,F,c) == nat_rec(n,c,%n x.F[x])"
nipkow@243
    26
Ifix_def      "Ifix(F) == lub(range(%i.iterate(i,F,UU)))"
nipkow@243
    27
fix_def       "fix == (LAM f. Ifix(f))"
nipkow@243
    28
nipkow@243
    29
adm_def       "adm(P) == !Y. is_chain(Y) --> \
nipkow@243
    30
\                        (!i.P(Y(i))) --> P(lub(range(Y)))"
nipkow@243
    31
nipkow@243
    32
admw_def      "admw(P)== (!F.((!n.P(iterate(n,F,UU)))-->\
nipkow@243
    33
\			 P(lub(range(%i.iterate(i,F,UU))))))" 
nipkow@243
    34
nipkow@243
    35
chain_finite_def  "chain_finite(x::'a)==\
nipkow@243
    36
\                        !Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y))"
nipkow@243
    37
nipkow@243
    38
flat_def          "flat(x::'a) ==\
clasohm@442
    39
\                        ! x y. (x::'a) << y --> (x = UU) | (x=y)"
nipkow@243
    40
nipkow@243
    41
end
nipkow@243
    42