author | haftmann |
Sun, 18 Jan 2009 21:12:06 +0100 | |
changeset 29554 | 7e5e5ebb7bf7 |
parent 29138 | 661a8db7e647 |
child 30607 | c3d1590debd8 |
permissions | -rw-r--r-- |
2640 | 1 |
(* Title: HOLCF/Lift.thy |
12026 | 2 |
Author: Olaf Mueller |
2640 | 3 |
*) |
4 |
||
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12026
diff
changeset
|
5 |
header {* Lifting types of class type to flat pcpo's *} |
12026 | 6 |
|
15577 | 7 |
theory Lift |
27311 | 8 |
imports Discrete Up Countable |
15577 | 9 |
begin |
12026 | 10 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12026
diff
changeset
|
11 |
defaultsort type |
12026 | 12 |
|
16748 | 13 |
pcpodef 'a lift = "UNIV :: 'a discr u set" |
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
27311
diff
changeset
|
14 |
by simp_all |
12026 | 15 |
|
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25723
diff
changeset
|
16 |
instance lift :: (finite) finite_po |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25723
diff
changeset
|
17 |
by (rule typedef_finite_po [OF type_definition_lift]) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25723
diff
changeset
|
18 |
|
16748 | 19 |
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric] |
12026 | 20 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
21 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
22 |
Def :: "'a \<Rightarrow> 'a lift" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
23 |
"Def x = Abs_lift (up\<cdot>(Discr x))" |
12026 | 24 |
|
25 |
subsection {* Lift as a datatype *} |
|
26 |
||
16748 | 27 |
lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y" |
28 |
apply (induct y) |
|
16755
fd02f9d06e43
renamed upE1 to upE; added simp rule cont2cont_flift1
huffman
parents:
16749
diff
changeset
|
29 |
apply (rule_tac p=y in upE) |
16748 | 30 |
apply (simp add: Abs_lift_strict) |
31 |
apply (case_tac x) |
|
32 |
apply (simp add: Def_def) |
|
33 |
done |
|
12026 | 34 |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26963
diff
changeset
|
35 |
rep_datatype "\<bottom>\<Colon>'a lift" Def |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26963
diff
changeset
|
36 |
by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject lift_def inst_lift_pcpo) |
12026 | 37 |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26963
diff
changeset
|
38 |
lemmas lift_distinct1 = lift.distinct(1) |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26963
diff
changeset
|
39 |
lemmas lift_distinct2 = lift.distinct(2) |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26963
diff
changeset
|
40 |
lemmas Def_not_UU = lift.distinct(2) |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26963
diff
changeset
|
41 |
lemmas Def_inject = lift.inject |
12026 | 42 |
|
43 |
||
16748 | 44 |
text {* @{term UU} and @{term Def} *} |
12026 | 45 |
|
16748 | 46 |
lemma Lift_exhaust: "x = \<bottom> \<or> (\<exists>y. x = Def y)" |
12026 | 47 |
by (induct x) simp_all |
48 |
||
16748 | 49 |
lemma Lift_cases: "\<lbrakk>x = \<bottom> \<Longrightarrow> P; \<exists>a. x = Def a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
12026 | 50 |
by (insert Lift_exhaust) blast |
51 |
||
16748 | 52 |
lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)" |
12026 | 53 |
by (cases x) simp_all |
54 |
||
16630
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset
|
55 |
lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset
|
56 |
by (cases x) simp_all |
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset
|
57 |
|
12026 | 58 |
text {* |
59 |
For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text |
|
60 |
x} by @{text "Def a"} in conclusion. *} |
|
61 |
||
16121 | 62 |
ML {* |
16630
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset
|
63 |
local val lift_definedE = thm "lift_definedE" |
12026 | 64 |
in val def_tac = SIMPSET' (fn ss => |
16630
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset
|
65 |
etac lift_definedE THEN' asm_simp_tac ss) |
12026 | 66 |
end; |
67 |
*} |
|
68 |
||
16748 | 69 |
lemma DefE: "Def x = \<bottom> \<Longrightarrow> R" |
70 |
by simp |
|
12026 | 71 |
|
16748 | 72 |
lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R" |
12026 | 73 |
by simp |
74 |
||
27292 | 75 |
lemma Def_inject_less_eq: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y" |
16748 | 76 |
by (simp add: less_lift_def Def_def Abs_lift_inverse lift_def) |
12026 | 77 |
|
27292 | 78 |
lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y" |
79 |
by (induct y, simp, simp add: Def_inject_less_eq) |
|
12026 | 80 |
|
81 |
||
82 |
subsection {* Lift is flat *} |
|
83 |
||
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12026
diff
changeset
|
84 |
instance lift :: (type) flat |
27292 | 85 |
proof |
86 |
fix x y :: "'a lift" |
|
87 |
assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y" |
|
88 |
by (induct x) auto |
|
89 |
qed |
|
12026 | 90 |
|
91 |
text {* |
|
92 |
\medskip Two specific lemmas for the combination of LCF and HOL |
|
93 |
terms. |
|
94 |
*} |
|
95 |
||
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
25920
diff
changeset
|
96 |
lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)" |
18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
17612
diff
changeset
|
97 |
by (rule cont2cont_Rep_CFun [THEN cont2cont_fun]) |
12026 | 98 |
|
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
25920
diff
changeset
|
99 |
lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)" |
18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
17612
diff
changeset
|
100 |
by (rule cont_Rep_CFun_app [THEN cont2cont_fun]) |
2640 | 101 |
|
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
102 |
subsection {* Further operations *} |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
103 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
104 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
105 |
flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10) where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
106 |
"flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))" |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
107 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
108 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
109 |
flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
110 |
"flift2 f = (FLIFT x. Def (f x))" |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
111 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
112 |
subsection {* Continuity Proofs for flift1, flift2 *} |
12026 | 113 |
|
114 |
text {* Need the instance of @{text flat}. *} |
|
115 |
||
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
116 |
lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
117 |
apply (induct x) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
118 |
apply simp |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
119 |
apply simp |
18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
17612
diff
changeset
|
120 |
apply (rule cont_id [THEN cont2cont_fun]) |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
121 |
done |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
122 |
|
25723 | 123 |
lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)" |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
124 |
apply (rule flatdom_strict2cont) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
125 |
apply simp |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
126 |
done |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
127 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
128 |
lemma cont_flift1: "cont flift1" |
27292 | 129 |
unfolding flift1_def |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
130 |
apply (rule cont2cont_LAM) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
131 |
apply (rule cont_lift_case2) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
132 |
apply (rule cont_lift_case1) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
133 |
done |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
134 |
|
27310 | 135 |
lemma FLIFT_mono: |
136 |
"(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)" |
|
137 |
apply (rule monofunE [where f=flift1]) |
|
138 |
apply (rule cont2mono [OF cont_flift1]) |
|
139 |
apply (simp add: less_fun_ext) |
|
140 |
done |
|
141 |
||
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
25920
diff
changeset
|
142 |
lemma cont2cont_flift1 [simp]: |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
143 |
"\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
144 |
apply (rule cont_flift1 [THEN cont2cont_app3]) |
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
25920
diff
changeset
|
145 |
apply simp |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
146 |
done |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
147 |
|
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
25920
diff
changeset
|
148 |
lemma cont2cont_lift_case [simp]: |
25723 | 149 |
"\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case UU (f x) (g x))" |
16757
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
150 |
apply (subgoal_tac "cont (\<lambda>x. (FLIFT y. f x y)\<cdot>(g x))") |
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
151 |
apply (simp add: flift1_def cont_lift_case2) |
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
25920
diff
changeset
|
152 |
apply simp |
16757
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
153 |
done |
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
154 |
|
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
155 |
text {* rewrites for @{term flift1}, @{term flift2} *} |
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
156 |
|
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
157 |
lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
158 |
by (simp add: flift1_def cont_lift_case2) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
159 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
160 |
lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
161 |
by (simp add: flift2_def) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
162 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
163 |
lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
164 |
by (simp add: flift1_def cont_lift_case2) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
165 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
166 |
lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
167 |
by (simp add: flift2_def) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
168 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
169 |
lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
170 |
by (erule lift_definedE, simp) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
171 |
|
19520 | 172 |
lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)" |
173 |
by (cases x, simp_all) |
|
174 |
||
12026 | 175 |
text {* |
14096 | 176 |
\medskip Extension of @{text cont_tac} and installation of simplifier. |
12026 | 177 |
*} |
178 |
||
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
25920
diff
changeset
|
179 |
lemmas cont_lemmas_ext = |
16757
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
180 |
cont2cont_flift1 cont2cont_lift_case cont2cont_lambda |
12026 | 181 |
cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if |
182 |
||
16121 | 183 |
ML {* |
19764 | 184 |
local |
185 |
val cont_lemmas2 = thms "cont_lemmas1" @ thms "cont_lemmas_ext"; |
|
186 |
val flift1_def = thm "flift1_def"; |
|
187 |
in |
|
12026 | 188 |
|
189 |
fun cont_tac i = resolve_tac cont_lemmas2 i; |
|
190 |
fun cont_tacR i = REPEAT (cont_tac i); |
|
191 |
||
19764 | 192 |
fun cont_tacRs ss i = |
17612 | 193 |
simp_tac ss i THEN |
12026 | 194 |
REPEAT (cont_tac i) |
195 |
end; |
|
15651
4b393520846e
Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
huffman
parents:
15577
diff
changeset
|
196 |
*} |
12026 | 197 |
|
26963 | 198 |
subsection {* Lifted countable types are bifinite *} |
199 |
||
200 |
instantiation lift :: (countable) bifinite |
|
201 |
begin |
|
202 |
||
203 |
definition |
|
204 |
approx_lift_def: |
|
205 |
"approx = (\<lambda>n. FLIFT x. if to_nat x < n then Def x else \<bottom>)" |
|
206 |
||
207 |
instance proof |
|
208 |
fix x :: "'a lift" |
|
27310 | 209 |
show "chain (approx :: nat \<Rightarrow> 'a lift \<rightarrow> 'a lift)" |
26963 | 210 |
unfolding approx_lift_def |
27310 | 211 |
by (rule chainI, simp add: FLIFT_mono) |
26963 | 212 |
next |
213 |
fix x :: "'a lift" |
|
214 |
show "(\<Squnion>i. approx i\<cdot>x) = x" |
|
215 |
unfolding approx_lift_def |
|
216 |
apply (cases x, simp) |
|
217 |
apply (rule thelubI) |
|
218 |
apply (rule is_lubI) |
|
219 |
apply (rule ub_rangeI, simp) |
|
220 |
apply (drule ub_rangeD) |
|
221 |
apply (erule rev_trans_less) |
|
222 |
apply simp |
|
223 |
apply (rule lessI) |
|
224 |
done |
|
225 |
next |
|
226 |
fix i :: nat and x :: "'a lift" |
|
227 |
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x" |
|
228 |
unfolding approx_lift_def |
|
229 |
by (cases x, simp, simp) |
|
230 |
next |
|
231 |
fix i :: nat |
|
232 |
show "finite {x::'a lift. approx i\<cdot>x = x}" |
|
233 |
proof (rule finite_subset) |
|
234 |
let ?S = "insert (\<bottom>::'a lift) (Def ` to_nat -` {..<i})" |
|
235 |
show "{x::'a lift. approx i\<cdot>x = x} \<subseteq> ?S" |
|
236 |
unfolding approx_lift_def |
|
237 |
by (rule subsetI, case_tac x, simp, simp split: split_if_asm) |
|
238 |
show "finite ?S" |
|
239 |
by (simp add: finite_vimageI) |
|
240 |
qed |
|
241 |
qed |
|
242 |
||
2640 | 243 |
end |
26963 | 244 |
|
245 |
end |