author | wenzelm |
Fri, 07 Mar 1997 11:48:46 +0100 | |
changeset 2754 | 59bd96046ad6 |
parent 2640 | ee4dfce170a0 |
child 2841 | c2508f4ab739 |
permissions | -rw-r--r-- |
2640 | 1 |
(* Title: HOLCF/Fix.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1479 | 3 |
Author: Franz Regensburger |
243
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 |
|
1990 | 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" |
|
2275 | 21 |
flat :: "'a=>bool" (* should be called flat, for consistency *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
22 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
23 |
defs |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
24 |
|
1825 | 25 |
iterate_def "iterate n F c == nat_rec c (%n x.F`x) n" |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
26 |
Ifix_def "Ifix F == lub(range(%i.iterate i F UU))" |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
27 |
fix_def "fix == (LAM f. Ifix f)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
28 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
29 |
adm_def "adm P == !Y. is_chain(Y) --> |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
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 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
32 |
admw_def "admw P == !F. (!n.P (iterate n F UU)) --> |
1479 | 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 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
35 |
chain_finite_def "chain_finite (x::'a)== |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
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 |
|
2275 | 38 |
flat_def "flat (x::'a) == ! 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
|
39 |
|
2640 | 40 |
(* further useful class for HOLCF *) |
41 |
||
42 |
axclass chfin<pcpo |
|
43 |
||
44 |
ax_chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)" |
|
45 |
||
46 |
axclass flat<pcpo |
|
47 |
||
48 |
ax_flat "! x y.x << y --> (x = UU) | (x=y)" |
|
49 |
||
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
50 |
end |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
51 |