src/HOLCF/Fix.thy
author clasohm
Wed, 21 Jun 1995 15:14:58 +0200
changeset 1150 66512c9e6bd6
parent 442 13ac1fd0a14d
child 1168 74be52691d62
permissions -rw-r--r--
removed \...\ inside strings
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     1
(*  Title: 	HOLCF/fix.thy
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     3
    Author: 	Franz Regensburger
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
    Copyright   1993  Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     6
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     7
definitions for fixed point operator and admissibility
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     8
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     9
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    11
Fix = Cfun3 +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    12
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    13
consts
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    14
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    15
iterate :: "nat=>('a->'a)=>'a=>'a"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    16
Ifix    :: "('a->'a)=>'a"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    17
fix     :: "('a->'a)->'a"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    18
adm          :: "('a=>bool)=>bool"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    19
admw         :: "('a=>bool)=>bool"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    20
chain_finite :: "'a=>bool"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    21
flat         :: "'a=>bool"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    22
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    23
rules
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    24
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    25
iterate_def   "iterate(n,F,c) == nat_rec(n,c,%n x.F[x])"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    26
Ifix_def      "Ifix(F) == lub(range(%i.iterate(i,F,UU)))"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    27
fix_def       "fix == (LAM f. Ifix(f))"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    28
1150
66512c9e6bd6 removed \...\ inside strings
clasohm
parents: 442
diff changeset
    29
adm_def       "adm(P) == !Y. is_chain(Y) --> 
66512c9e6bd6 removed \...\ inside strings
clasohm
parents: 442
diff changeset
    30
                        (!i.P(Y(i))) --> P(lub(range(Y)))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    31
1150
66512c9e6bd6 removed \...\ inside strings
clasohm
parents: 442
diff changeset
    32
admw_def      "admw(P)== (!F.((!n.P(iterate(n,F,UU)))-->
66512c9e6bd6 removed \...\ inside strings
clasohm
parents: 442
diff changeset
    33
			 P(lub(range(%i.iterate(i,F,UU))))))" 
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    34
1150
66512c9e6bd6 removed \...\ inside strings
clasohm
parents: 442
diff changeset
    35
chain_finite_def  "chain_finite(x::'a)==
66512c9e6bd6 removed \...\ inside strings
clasohm
parents: 442
diff changeset
    36
                        !Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    37
1150
66512c9e6bd6 removed \...\ inside strings
clasohm
parents: 442
diff changeset
    38
flat_def          "flat(x::'a) ==
66512c9e6bd6 removed \...\ inside strings
clasohm
parents: 442
diff changeset
    39
                        ! x y. (x::'a) << y --> (x = UU) | (x=y)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    40
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    41
end
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    42