|
1 ruleshell.ML lemmas.ML set.ML fun.ML subset.ML equalities.ML prod.ML sum.ML wf.ML mono.ML fixedpt.ML nat.ML list.ML |
|
2 ---------------------------------------------------------------- |
|
3 ruleshell.ML |
|
4 |
|
5 \idx{refl} t = t::'a |
|
6 \idx{subst} [| s = t; P(s) |] ==> P(t::'a) |
|
7 \idx{abs},!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x))) |
|
8 \idx{disch} (P ==> Q) ==> P-->Q |
|
9 \idx{mp} [| P-->Q; P |] ==> Q |
|
10 |
|
11 \idx{True_def} True = ((%x.x)=(%x.x)) |
|
12 \idx{All_def} All = (%P. P = (%x.True)) |
|
13 \idx{Ex_def} Ex = (%P. P(Eps(P))) |
|
14 \idx{False_def} False = (!P.P) |
|
15 \idx{not_def} not = (%P. P-->False) |
|
16 \idx{and_def} op & = (%P Q. !R. (P-->Q-->R) --> R) |
|
17 \idx{or_def} op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R) |
|
18 \idx{Ex1_def} Ex1 == (%P. ? x. P(x) & (! y. P(y) --> y=x)) |
|
19 |
|
20 \idx{iff} (P-->Q) --> (Q-->P) --> (P=Q) |
|
21 \idx{True_or_False} (P=True) | (P=False) |
|
22 \idx{select} P(x::'a) --> P(Eps(P)) |
|
23 |
|
24 \idx{Inv_def} Inv = (%(f::'a=>'b) y. @x. f(x)=y) |
|
25 \idx{o_def} op o = (%(f::'b=>'c) g (x::'a). f(g(x))) |
|
26 \idx{Cond_def} Cond = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y)) |
|
27 |
|
28 ---------------------------------------------------------------- |
|
29 lemmas.ML |
|
30 |
|
31 \idx{sym} s=t ==> t=s |
|
32 \idx{trans} [| r=s; s=t |] ==> r=t |
|
33 \idx{box_equals} |
|
34 [| a=b; a=c; b=d |] ==> c=d |
|
35 \idx{ap_term} s=t ==> f(s)=f(t) |
|
36 \idx{ap_thm} s::'a=>'b = t ==> s(x)=t(x) |
|
37 \idx{cong} |
|
38 [| f = g; x::'a = y |] ==> f(x) = g(y) |
|
39 \idx{iffI} |
|
40 [| P ==> Q; Q ==> P |] ==> P=Q |
|
41 \idx{iffD1} [| P=Q; Q |] ==> P |
|
42 \idx{iffE} |
|
43 [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R |
|
44 \idx{eqTrueI} P ==> P=True |
|
45 \idx{eqTrueE} P=True ==> P |
|
46 \idx{allI} (!!x::'a. P(x)) ==> !x. P(x) |
|
47 \idx{spec} !x::'a.P(x) ==> P(x) |
|
48 \idx{allE} [| !x.P(x); P(x) ==> R |] ==> R |
|
49 \idx{all_dupE} |
|
50 [| ! x.P(x); [| P(x); ! x.P(x) |] ==> R |
|
51 |] ==> R |
|
52 \idx{FalseE} False ==> P |
|
53 \idx{False_neq_True} False=True ==> P |
|
54 \idx{notI} (P ==> False) ==> ~P |
|
55 \idx{notE} [| ~P; P |] ==> R |
|
56 \idx{impE} [| P-->Q; P; Q ==> R |] ==> R |
|
57 \idx{rev_mp} [| P; P --> Q |] ==> Q |
|
58 \idx{contrapos} [| ~Q; P==>Q |] ==> ~P |
|
59 \idx{exI} P(x) ==> ? x::'a.P(x) |
|
60 \idx{exE} [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q |
|
61 |
|
62 \idx{conjI} [| P; Q |] ==> P&Q |
|
63 \idx{conjunct1} [| P & Q |] ==> P |
|
64 \idx{conjunct2} [| P & Q |] ==> Q |
|
65 \idx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R |
|
66 \idx{disjI1} P ==> P|Q |
|
67 \idx{disjI2} Q ==> P|Q |
|
68 \idx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R |
|
69 \idx{ccontr} (~P ==> False) ==> P |
|
70 \idx{classical} (~P ==> P) ==> P |
|
71 \idx{notnotD} ~~P ==> P |
|
72 \idx{ex1I} |
|
73 [| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x) |
|
74 \idx{ex1E} |
|
75 [| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R |] ==> R |
|
76 \idx{select_equality} |
|
77 [| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a |
|
78 \idx{disjCI} (~Q ==> P) ==> P|Q |
|
79 \idx{excluded_middle} ~P | P |
|
80 \idx{impCE} [| P-->Q; ~P ==> R; Q ==> R |] ==> R |
|
81 \idx{iffCE} |
|
82 [| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R |
|
83 \idx{exCI} (! x. ~P(x) ==> P(a)) ==> ? x.P(x) |
|
84 \idx{swap} ~P ==> (~Q ==> P) ==> Q |
|
85 |
|
86 ---------------------------------------------------------------- |
|
87 simpdata.ML |
|
88 |
|
89 \idx{if_True} Cond(True,x,y) = x |
|
90 \idx{if_False} Cond(False,x,y) = y |
|
91 \idx{if_P} P ==> Cond(P,x,y) = x |
|
92 \idx{if_not_P} ~P ==> Cond(P,x,y) = y |
|
93 \idx{expand_if} |
|
94 P(Cond(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y))) |
|
95 |
|
96 ---------------------------------------------------------------- |
|
97 \idx{set.ML} |
|
98 |
|
99 \idx{CollectI} [| P(a) |] ==> a : \{x.P(x)\} |
|
100 \idx{CollectD} [| a : \{x.P(x)\} |] ==> P(a) |
|
101 \idx{set_ext} [| !!x. (x:A) = (x:B) |] ==> A = B |
|
102 |
|
103 \idx{Ball_def} Ball(A,P) == ! x. x:A --> P(x) |
|
104 \idx{Bex_def} Bex(A,P) == ? x. x:A & P(x) |
|
105 \idx{subset_def} A <= B == ! x:A. x:B |
|
106 \idx{Un_def} A Un B == \{x.x:A | x:B\} |
|
107 \idx{Int_def} A Int B == \{x.x:A & x:B\} |
|
108 \idx{Compl_def} Compl(A) == \{x. ~x:A\} |
|
109 \idx{Inter_def} Inter(S) == \{x. ! A:S. x:A\} |
|
110 \idx{Union_def} Union(S) == \{x. ? A:S. x:A\} |
|
111 \idx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\} |
|
112 \idx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\} |
|
113 \idx{mono_def} mono(f) == (!A B. A <= B --> f(A) <= f(B)) |
|
114 \idx{image_def} f``A == \{y. ? x:A. y=f(x)\} |
|
115 \idx{singleton_def} \{a\} == \{x.x=a\} |
|
116 \idx{range_def} range(f) == \{y. ? x. y=f(x)\} |
|
117 \idx{One_One_def} One_One(f) == ! x y. f(x)=f(y) --> x=y |
|
118 \idx{One_One_on_def} One_One_on(f,A) == !x y. x:A --> y:A --> f(x)=f(y) --> x=y |
|
119 \idx{Onto_def} Onto(f) == ! y. ? x. y=f(x) |
|
120 |
|
121 |
|
122 \idx{Collect_cong} [| !!x. P(x)=Q(x) |] ==> \{x. P(x)\} = \{x. Q(x)\} |
|
123 |
|
124 \idx{ballI} [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x) |
|
125 \idx{bspec} [| ! x:A. P(x); x:A |] ==> P(x) |
|
126 \idx{ballE} [| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q |
|
127 |
|
128 \idx{bexI} [| P(x); x:A |] ==> ? x:A. P(x) |
|
129 \idx{bexCI} [| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A.P(x) |
|
130 \idx{bexE} [| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q |
|
131 |
|
132 \idx{ball_cong} |
|
133 [| A=A'; !!x. x:A' ==> P(x) = P'(x) |] ==> |
|
134 (! x:A. P(x)) = (! x:A'. P'(x)) |
|
135 |
|
136 \idx{bex_cong} |
|
137 [| A=A'; !!x. x:A' ==> P(x) = P'(x) |] ==> |
|
138 (? x:A. P(x)) = (? x:A'. P'(x)) |
|
139 |
|
140 \idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B |
|
141 \idx{subsetD} [| A <= B; c:A |] ==> c:B |
|
142 \idx{subsetCE} [| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P |
|
143 |
|
144 \idx{subset_refl} A <= A |
|
145 \idx{subset_antisym} [| A <= B; B <= A |] ==> A = B |
|
146 \idx{subset_trans} [| A<=B; B<=C |] ==> A<=C |
|
147 |
|
148 \idx{equalityD1} A = B ==> A<=B |
|
149 \idx{equalityD2} A = B ==> B<=A |
|
150 \idx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P |
|
151 |
|
152 \idx{singletonI} a : \{a\} |
|
153 \idx{singletonD} b : \{a\} ==> b=a |
|
154 |
|
155 \idx{imageI} [| x:A |] ==> f(x) : f``A |
|
156 \idx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P |
|
157 |
|
158 \idx{rangeI} f(x) : range(f) |
|
159 \idx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P |
|
160 |
|
161 \idx{UnionI} [| X:C; A:X |] ==> A : Union(C) |
|
162 \idx{UnionE} [| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R |
|
163 |
|
164 \idx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C) |
|
165 \idx{InterD} [| A : Inter(C); X:C |] ==> A:X |
|
166 \idx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R |
|
167 |
|
168 \idx{UN_I} [| a:A; b: B(a) |] ==> b: (UN x:A. B(x)) |
|
169 \idx{UN_E} [| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R |
|
170 |
|
171 \idx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x)) |
|
172 \idx{INT_D} [| b : (INT x:A. B(x)); a:A |] ==> b: B(a) |
|
173 \idx{INT_E} [| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R |
|
174 |
|
175 \idx{UnI1} c:A ==> c : A Un B |
|
176 \idx{UnI2} c:B ==> c : A Un B |
|
177 \idx{UnCI} (~c:B ==> c:A) ==> c : A Un B |
|
178 \idx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P |
|
179 |
|
180 \idx{IntI} [| c:A; c:B |] ==> c : A Int B |
|
181 \idx{IntD1} c : A Int B ==> c:A |
|
182 \idx{IntD2} c : A Int B ==> c:B |
|
183 \idx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P |
|
184 |
|
185 \idx{ComplI} [| c:A ==> False |] ==> c : Compl(A) |
|
186 \idx{ComplD} [| c : Compl(A) |] ==> ~c:A |
|
187 |
|
188 \idx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f) |
|
189 \idx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B) |
|
190 |
|
191 |
|
192 ---------------------------------------------------------------- |
|
193 \idx{fun.ML} |
|
194 |
|
195 \idx{One_OneI} [| !! x y. f(x) = f(y) ==> x=y |] ==> One_One(f) |
|
196 \idx{One_One_inverseI} (!!x. g(f(x)) = x) ==> One_One(f) |
|
197 \idx{One_OneD} [| One_One(f); f(x) = f(y) |] ==> x=y |
|
198 |
|
199 \idx{Inv_f_f} One_One(f) ==> Inv(f,f(x)) = x |
|
200 \idx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y |
|
201 |
|
202 \idx{Inv_injective} |
|
203 [| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y |
|
204 |
|
205 \idx{One_One_onI} |
|
206 (!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> One_One_on(f,A) |
|
207 |
|
208 \idx{One_One_on_inverseI} |
|
209 (!!x. x:A ==> g(f(x)) = x) ==> One_One_on(f,A) |
|
210 |
|
211 \idx{One_One_onD} |
|
212 [| One_One_on(f,A); f(x)=f(y); x:A; y:A |] ==> x=y |
|
213 |
|
214 \idx{One_One_on_contraD} |
|
215 [| One_One_on(f,A); ~x=y; x:A; y:A |] ==> ~ f(x)=f(y) |
|
216 |
|
217 |
|
218 ---------------------------------------------------------------- |
|
219 \idx{subset.ML} |
|
220 |
|
221 \idx{Union_upper} B:A ==> B <= Union(A) |
|
222 \idx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C |
|
223 |
|
224 \idx{Inter_lower} B:A ==> Inter(A) <= B |
|
225 \idx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A) |
|
226 |
|
227 \idx{Un_upper1} A <= A Un B |
|
228 \idx{Un_upper2} B <= A Un B |
|
229 \idx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C |
|
230 |
|
231 \idx{Int_lower1} A Int B <= A |
|
232 \idx{Int_lower2} A Int B <= B |
|
233 \idx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B |
|
234 |
|
235 |
|
236 ---------------------------------------------------------------- |
|
237 \idx{equalities.ML} |
|
238 |
|
239 \idx{Int_absorb} A Int A = A |
|
240 \idx{Int_commute} A Int B = B Int A |
|
241 \idx{Int_assoc} (A Int B) Int C = A Int (B Int C) |
|
242 \idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) |
|
243 |
|
244 \idx{Un_absorb} A Un A = A |
|
245 \idx{Un_commute} A Un B = B Un A |
|
246 \idx{Un_assoc} (A Un B) Un C = A Un (B Un C) |
|
247 \idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) |
|
248 |
|
249 \idx{Compl_disjoint} A Int Compl(A) = \{x.False\} |
|
250 \idx{Compl_partition A Un Compl(A) = \{x.True\} |
|
251 \idx{double_complement} Compl(Compl(A)) = A |
|
252 |
|
253 |
|
254 \idx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B) |
|
255 \idx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B) |
|
256 |
|
257 \idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B) |
|
258 \idx{Int_Union_image} A Int Union(B) = (UN C:B. A Int C) |
|
259 \idx{Un_Union_image} (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C) |
|
260 |
|
261 \idx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B) |
|
262 \idx{Un_Inter_image} A Un Inter(B) = (INT C:B. A Un C) |
|
263 \idx{Int_Inter_image} (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C) |
|
264 |
|
265 |
|
266 ---------------------------------------------------------------- |
|
267 prod.ML |
|
268 |
|
269 mixfix = [ Delimfix((1<_,/_>), ['a,'b] => ('a,'b)prod, Pair), |
|
270 TInfixl(*, prod, 20) ], |
|
271 thy = extend_theory Set.thy Prod |
|
272 [([prod],([[term],[term]],term))], |
|
273 ([fst], 'a * 'b => 'a), |
|
274 ([snd], 'a * 'b => 'b), |
|
275 ([split], ['a * 'b, ['a,'b]=>'c] => 'c)], |
|
276 \idx{fst_def} fst(p) == @a. ? b. p = <a,b>), |
|
277 \idx{snd_def} snd(p) == @b. ? a. p = <a,b>), |
|
278 \idx{split_def} split(p,c) == c(fst(p),snd(p))) |
|
279 |
|
280 \idx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R |
|
281 |
|
282 \idx{fst_conv} fst(<a,b>) = a |
|
283 \idx{snd_conv} snd(<a,b>) = b |
|
284 \idx{split_conv} split(<a,b>, c) = c(a,b) |
|
285 |
|
286 \idx{surjective_pairing} p = <fst(p),snd(p)> |
|
287 |
|
288 ---------------------------------------------------------------- |
|
289 sum.ML |
|
290 |
|
291 mixfix = [TInfixl(+, sum, 10)], |
|
292 thy = extend_theory Prod.thy sum |
|
293 [([sum], ([[term],[term]],term))], |
|
294 [Inl], 'a => 'a+'b), |
|
295 [Inr], 'b => 'a+'b), |
|
296 [when], ['a+'b, 'a=>'c, 'b=>'c] =>'c)], |
|
297 \idx{when_def} when == (%p f g. @z. (!x. p=Inl(x) --> z=f(x)) |
|
298 & (!y. p=Inr(y) --> z=g(y)))) |
|
299 |
|
300 \idx{Inl_not_Inr} ~ (Inl(a) = Inr(b)) |
|
301 |
|
302 \idx{One_One_Inl} One_One(Inl) |
|
303 |
|
304 \idx{One_One_Inr} One_One(Inr) |
|
305 |
|
306 \idx{when_Inl_conv} when(Inl(x), f, g) = f(x) |
|
307 |
|
308 \idx{when_Inr_conv} when(Inr(x), f, g) = g(x) |
|
309 |
|
310 \idx{sumE} |
|
311 [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) |
|
312 |] ==> P(s) |
|
313 |
|
314 \idx{surjective_sum} when(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s) |
|
315 |
|
316 |
|
317 ???????????????????????????????????????????????????????????????? |
|
318 trancl? |
|
319 |
|
320 ---------------------------------------------------------------- |
|
321 nat.ML |
|
322 |
|
323 Sext\{mixfix=[Delimfix(0, nat, 0), |
|
324 Infixl(<,[nat,nat] => bool,50)], |
|
325 thy = extend_theory Trancl.thy Nat |
|
326 [nat], ([],term)) |
|
327 [nat_case], [nat, 'a, nat=>'a] =>'a), |
|
328 [pred_nat],nat*nat) set), |
|
329 [nat_rec], [nat, 'a, [nat, 'a]=>'a] => 'a) |
|
330 |
|
331 \idx{nat_case_def} nat_case == (%n a f. @z. (n=0 --> z=a) |
|
332 & (!x. n=Suc(x) --> z=f(x)))), |
|
333 \idx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\} ), |
|
334 \idx{less_def} m<n == <m,n>:trancl(pred_nat)), |
|
335 \idx{nat_rec_def} |
|
336 nat_rec(n,c,d) == wfrec(trancl(pred_nat), |
|
337 %rec l. nat_case(l, c, %m. d(m,rec(m))), |
|
338 n) ) |
|
339 |
|
340 \idx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n) |
|
341 |
|
342 |
|
343 \idx{Suc_not_Zero} ~ (Suc(m) = 0) |
|
344 \idx{One_One_Suc} One_One(Suc) |
|
345 \idx{n_not_Suc_n} ~(n=Suc(n)) |
|
346 |
|
347 \idx{nat_case_0_conv} nat_case(0, a, f) = a |
|
348 |
|
349 \idx{nat_case_Suc_conv} nat_case(Suc(k), a, f) = f(k) |
|
350 |
|
351 \idx{pred_natI} <n, Suc(n)> : pred_nat |
|
352 \idx{pred_natE} |
|
353 [| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> R |
|
354 |] ==> R |
|
355 |
|
356 \idx{wf_pred_nat} wf(pred_nat) |
|
357 |
|
358 \idx{nat_rec_0_conv} nat_rec(0,c,h) = c |
|
359 |
|
360 \idx{nat_rec_Suc_conv} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h)) |
|
361 |
|
362 |
|
363 (*** Basic properties of less than ***) |
|
364 \idx{less_trans} [| i<j; j<k |] ==> i<k |
|
365 \idx{lessI} n < Suc(n) |
|
366 \idx{zero_less_Suc} 0 < Suc(n) |
|
367 |
|
368 \idx{less_not_sym} n<m --> ~m<n |
|
369 \idx{less_not_refl} ~ (n<n) |
|
370 \idx{not_less0} ~ (n<0) |
|
371 |
|
372 \idx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n) |
|
373 \idx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n) |
|
374 |
|
375 \idx{less_linear} m<n | m=n | n<m |
|
376 |
|
377 |
|
378 ---------------------------------------------------------------- |
|
379 list.ML |
|
380 |
|
381 [([list], ([[term]],term))], |
|
382 ([Nil], 'a list), |
|
383 ([Cons], ['a, 'a list] => 'a list), |
|
384 ([list_rec], ['a list, 'b, ['a ,'a list, 'b]=>'b] => 'b), |
|
385 ([list_all], ('a => bool) => ('a list => bool)), |
|
386 ([map], ('a=>'b) => ('a list => 'b list)) |
|
387 |
|
388 \idx{map_def} map(f,xs) == list_rec(xs, Nil, %x l r. Cons(f(x), r)) ) |
|
389 |
|
390 \idx{list_induct} |
|
391 [| P(Nil); |
|
392 !!x xs. [| P(xs) |] ==> P(Cons(x,xs)) |] ==> P(l) |
|
393 |
|
394 \idx{Cons_not_Nil} ~ Cons(x,xs) = Nil |
|
395 \idx{Cons_Cons_eq} (Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys) |
|
396 |
|
397 \idx{list_rec_Nil_conv} list_rec(Nil,c,h) = c |
|
398 \idx{list_rec_Cons_conv} list_rec(Cons(a,l), c, h) = |
|
399 h(a, l, list_rec(l,c,h)) |
|
400 |
|
401 \idx{map_Nil_conv} map(f,Nil) = Nil |
|
402 \idx{map_Cons_conv} map(f, Cons(x,xs)) = Cons(f(x), map(f,xs)) |
|
403 |