author | paulson |
Mon, 21 May 2001 14:36:24 +0200 | |
changeset 11316 | b4e71bd751e4 |
parent 8127 | 68c6159440f1 |
child 13085 | bfdb0534c8ec |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/ex/Limit |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
1478 | 3 |
Author: Sten Agerholm |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
4 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
5 |
A formalization of the inverse limit construction of domain theory. |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
6 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
7 |
The following paper comments on the formalization: |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
8 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
9 |
"A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
10 |
In Proceedings of the First Isabelle Users Workshop, Technical |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
11 |
Report No. 379, University of Cambridge Computer Laboratory, 1995. |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
12 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
13 |
This is a condensed version of: |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
14 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
15 |
"A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
16 |
Technical Report No. 369, University of Cambridge Computer |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
17 |
Laboratory, 1995. |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
18 |
*) |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
19 |
|
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
2469
diff
changeset
|
20 |
Limit = Main + |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
21 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
22 |
consts |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
23 |
|
1401 | 24 |
"rel" :: [i,i,i]=>o (* rel(D,x,y) *) |
25 |
"set" :: i=>i (* set(D) *) |
|
26 |
"po" :: i=>o (* po(D) *) |
|
27 |
"chain" :: [i,i]=>o (* chain(D,X) *) |
|
28 |
"isub" :: [i,i,i]=>o (* isub(D,X,x) *) |
|
29 |
"islub" :: [i,i,i]=>o (* islub(D,X,x) *) |
|
30 |
"lub" :: [i,i]=>i (* lub(D,X) *) |
|
31 |
"cpo" :: i=>o (* cpo(D) *) |
|
32 |
"pcpo" :: i=>o (* pcpo(D) *) |
|
33 |
"bot" :: i=>i (* bot(D) *) |
|
34 |
"mono" :: [i,i]=>i (* mono(D,E) *) |
|
35 |
"cont" :: [i,i]=>i (* cont(D,E) *) |
|
36 |
"cf" :: [i,i]=>i (* cf(D,E) *) |
|
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
37 |
|
1401 | 38 |
"suffix" :: [i,i]=>i (* suffix(X,n) *) |
39 |
"subchain" :: [i,i]=>o (* subchain(X,Y) *) |
|
40 |
"dominate" :: [i,i,i]=>o (* dominate(D,X,Y) *) |
|
41 |
"matrix" :: [i,i]=>o (* matrix(D,M) *) |
|
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
42 |
|
1401 | 43 |
"projpair" :: [i,i,i,i]=>o (* projpair(D,E,e,p) *) |
44 |
"emb" :: [i,i,i]=>o (* emb(D,E,e) *) |
|
45 |
"Rp" :: [i,i,i]=>i (* Rp(D,E,e) *) |
|
46 |
"iprod" :: i=>i (* iprod(DD) *) |
|
47 |
"mkcpo" :: [i,i=>o]=>i (* mkcpo(D,P) *) |
|
48 |
"subcpo" :: [i,i]=>o (* subcpo(D,E) *) |
|
49 |
"subpcpo" :: [i,i]=>o (* subpcpo(D,E) *) |
|
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
50 |
|
1401 | 51 |
"emb_chain" :: [i,i]=>o (* emb_chain(DD,ee) *) |
52 |
"Dinf" :: [i,i]=>i (* Dinf(DD,ee) *) |
|
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
53 |
|
1401 | 54 |
"e_less" :: [i,i,i,i]=>i (* e_less(DD,ee,m,n) *) |
55 |
"e_gr" :: [i,i,i,i]=>i (* e_gr(DD,ee,m,n) *) |
|
56 |
"eps" :: [i,i,i,i]=>i (* eps(DD,ee,m,n) *) |
|
57 |
"rho_emb" :: [i,i,i]=>i (* rho_emb(DD,ee,n) *) |
|
58 |
"rho_proj" :: [i,i,i]=>i (* rho_proj(DD,ee,n) *) |
|
59 |
"commute" :: [i,i,i,i=>i]=>o (* commute(DD,ee,E,r) *) |
|
60 |
"mediating" :: [i,i,i=>i,i=>i,i]=>o (* mediating(E,G,r,f,t) *) |
|
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
61 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
62 |
rules |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
63 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
64 |
set_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
65 |
"set(D) == fst(D)" |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
66 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
67 |
rel_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
68 |
"rel(D,x,y) == <x,y>:snd(D)" |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
69 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
70 |
po_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
71 |
"po(D) == \ |
11316 | 72 |
\ (\\<forall>x \\<in> set(D). rel(D,x,x)) & \ |
73 |
\ (\\<forall>x \\<in> set(D). \\<forall>y \\<in> set(D). \\<forall>z \\<in> set(D). \ |
|
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
74 |
\ rel(D,x,y) --> rel(D,y,z) --> rel(D,x,z)) & \ |
11316 | 75 |
\ (\\<forall>x \\<in> set(D). \\<forall>y \\<in> set(D). rel(D,x,y) --> rel(D,y,x) --> x = y)" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
76 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
77 |
(* Chains are object level functions nat->set(D) *) |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
78 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
79 |
chain_def |
11316 | 80 |
"chain(D,X) == X \\<in> nat->set(D) & (\\<forall>n \\<in> nat. rel(D,X`n,X`(succ(n))))" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
81 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
82 |
isub_def |
11316 | 83 |
"isub(D,X,x) == x \\<in> set(D) & (\\<forall>n \\<in> nat. rel(D,X`n,x))" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
84 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
85 |
islub_def |
11316 | 86 |
"islub(D,X,x) == isub(D,X,x) & (\\<forall>y. isub(D,X,y) --> rel(D,x,y))" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
87 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
88 |
lub_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
89 |
"lub(D,X) == THE x. islub(D,X,x)" |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
90 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
91 |
cpo_def |
11316 | 92 |
"cpo(D) == po(D) & (\\<forall>X. chain(D,X) --> (\\<exists>x. islub(D,X,x)))" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
93 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
94 |
pcpo_def |
11316 | 95 |
"pcpo(D) == cpo(D) & (\\<exists>x \\<in> set(D). \\<forall>y \\<in> set(D). rel(D,x,y))" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
96 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
97 |
bot_def |
11316 | 98 |
"bot(D) == THE x. x \\<in> set(D) & (\\<forall>y \\<in> set(D). rel(D,x,y))" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
99 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
100 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
101 |
mono_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
102 |
"mono(D,E) == \ |
11316 | 103 |
\ {f \\<in> set(D)->set(E). \ |
104 |
\ \\<forall>x \\<in> set(D). \\<forall>y \\<in> set(D). rel(D,x,y) --> rel(E,f`x,f`y)}" |
|
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
105 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
106 |
cont_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
107 |
"cont(D,E) == \ |
11316 | 108 |
\ {f \\<in> mono(D,E). \ |
109 |
\ \\<forall>X. chain(D,X) --> f`(lub(D,X)) = lub(E,\\<lambda>n \\<in> nat. f`(X`n))}" |
|
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
110 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
111 |
cf_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
112 |
"cf(D,E) == \ |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
113 |
\ <cont(D,E), \ |
11316 | 114 |
\ {y \\<in> cont(D,E)*cont(D,E). \\<forall>x \\<in> set(D). rel(E,(fst(y))`x,(snd(y))`x)}>" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
115 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
116 |
suffix_def |
11316 | 117 |
"suffix(X,n) == \\<lambda>m \\<in> nat. X`(n #+ m)" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
118 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
119 |
subchain_def |
11316 | 120 |
"subchain(X,Y) == \\<forall>m \\<in> nat. \\<exists>n \\<in> nat. X`m = Y`(m #+ n)" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
121 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
122 |
dominate_def |
11316 | 123 |
"dominate(D,X,Y) == \\<forall>m \\<in> nat. \\<exists>n \\<in> nat. rel(D,X`m,Y`n)" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
124 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
125 |
matrix_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
126 |
"matrix(D,M) == \ |
11316 | 127 |
\ M \\<in> nat -> (nat -> set(D)) & \ |
128 |
\ (\\<forall>n \\<in> nat. \\<forall>m \\<in> nat. rel(D,M`n`m,M`succ(n)`m)) & \ |
|
129 |
\ (\\<forall>n \\<in> nat. \\<forall>m \\<in> nat. rel(D,M`n`m,M`n`succ(m))) & \ |
|
130 |
\ (\\<forall>n \\<in> nat. \\<forall>m \\<in> nat. rel(D,M`n`m,M`succ(n)`succ(m)))" |
|
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
131 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
132 |
projpair_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
133 |
"projpair(D,E,e,p) == \ |
11316 | 134 |
\ e \\<in> cont(D,E) & p \\<in> cont(E,D) & \ |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
135 |
\ p O e = id(set(D)) & rel(cf(E,E),e O p,id(set(E)))" |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
136 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
137 |
emb_def |
11316 | 138 |
"emb(D,E,e) == \\<exists>p. projpair(D,E,e,p)" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
139 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
140 |
Rp_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
141 |
"Rp(D,E,e) == THE p. projpair(D,E,e,p)" |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
142 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
143 |
(* Twice, constructions on cpos are more difficult. *) |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
144 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
145 |
iprod_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
146 |
"iprod(DD) == \ |
11316 | 147 |
\ <(\\<Pi>n \\<in> nat. set(DD`n)), \ |
148 |
\ {x:(\\<Pi>n \\<in> nat. set(DD`n))*(\\<Pi>n \\<in> nat. set(DD`n)). \ |
|
149 |
\ \\<forall>n \\<in> nat. rel(DD`n,fst(x)`n,snd(x)`n)}>" |
|
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
150 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
151 |
mkcpo_def (* Cannot use rel(D), is meta fun, need two more args *) |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
152 |
"mkcpo(D,P) == \ |
11316 | 153 |
\ <{x \\<in> set(D). P(x)},{x \\<in> set(D)*set(D). rel(D,fst(x),snd(x))}>" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
154 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
155 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
156 |
subcpo_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
157 |
"subcpo(D,E) == \ |
11316 | 158 |
\ set(D) \\<subseteq> set(E) & \ |
159 |
\ (\\<forall>x \\<in> set(D). \\<forall>y \\<in> set(D). rel(D,x,y) <-> rel(E,x,y)) & \ |
|
160 |
\ (\\<forall>X. chain(D,X) --> lub(E,X):set(D))" |
|
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
161 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
162 |
subpcpo_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
163 |
"subpcpo(D,E) == subcpo(D,E) & bot(E):set(D)" |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
164 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
165 |
emb_chain_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
166 |
"emb_chain(DD,ee) == \ |
11316 | 167 |
\ (\\<forall>n \\<in> nat. cpo(DD`n)) & (\\<forall>n \\<in> nat. emb(DD`n,DD`succ(n),ee`n))" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
168 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
169 |
Dinf_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
170 |
"Dinf(DD,ee) == \ |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
171 |
\ mkcpo(iprod(DD)) \ |
11316 | 172 |
\ (%x. \\<forall>n \\<in> nat. Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n)" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
173 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
174 |
e_less_def (* Valid for m le n only. *) |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
175 |
"e_less(DD,ee,m,n) == rec(n#-m,id(set(DD`m)),%x y. ee`(m#+x) O y)" |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
176 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
177 |
e_gr_def (* Valid for n le m only. *) |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
178 |
"e_gr(DD,ee,m,n) == \ |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
179 |
\ rec(m#-n,id(set(DD`n)), \ |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
180 |
\ %x y. y O Rp(DD`(n#+x),DD`(succ(n#+x)),ee`(n#+x)))" |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
181 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
182 |
eps_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
183 |
"eps(DD,ee,m,n) == if(m le n,e_less(DD,ee,m,n),e_gr(DD,ee,m,n))" |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
184 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
185 |
rho_emb_def |
11316 | 186 |
"rho_emb(DD,ee,n) == \\<lambda>x \\<in> set(DD`n). \\<lambda>m \\<in> nat. eps(DD,ee,n,m)`x" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
187 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
188 |
rho_proj_def |
11316 | 189 |
"rho_proj(DD,ee,n) == \\<lambda>x \\<in> set(Dinf(DD,ee)). x`n" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
190 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
191 |
commute_def |
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
192 |
"commute(DD,ee,E,r) == \ |
11316 | 193 |
\ (\\<forall>n \\<in> nat. emb(DD`n,E,r(n))) & \ |
194 |
\ (\\<forall>m \\<in> nat. \\<forall>n \\<in> nat. m le n --> r(n) O eps(DD,ee,m,n) = r(m))" |
|
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
195 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
196 |
mediating_def |
11316 | 197 |
"mediating(E,G,r,f,t) == emb(E,G,t) & (\\<forall>n \\<in> nat. f(n) = t O r(n))" |
1281
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
198 |
|
68f6be60ab1c
The inverse limit construction -- thanks to Sten Agerholm
paulson
parents:
diff
changeset
|
199 |
end |