1.1 --- a/doc-src/Logics/HOL-rules.txt Tue May 04 18:04:45 1999 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,403 +0,0 @@
1.4 -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
1.5 -----------------------------------------------------------------
1.6 -ruleshell.ML
1.7 -
1.8 -\idx{refl} t = t::'a
1.9 -\idx{subst} [| s = t; P(s) |] ==> P(t::'a)
1.10 -\idx{abs},!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x)))
1.11 -\idx{disch} (P ==> Q) ==> P-->Q
1.12 -\idx{mp} [| P-->Q; P |] ==> Q
1.13 -
1.14 -\idx{True_def} True = ((%x.x)=(%x.x))
1.15 -\idx{All_def} All = (%P. P = (%x.True))
1.16 -\idx{Ex_def} Ex = (%P. P(Eps(P)))
1.17 -\idx{False_def} False = (!P.P)
1.18 -\idx{not_def} not = (%P. P-->False)
1.19 -\idx{and_def} op & = (%P Q. !R. (P-->Q-->R) --> R)
1.20 -\idx{or_def} op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)
1.21 -\idx{Ex1_def} Ex1 == (%P. ? x. P(x) & (! y. P(y) --> y=x))
1.22 -
1.23 -\idx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
1.24 -\idx{True_or_False} (P=True) | (P=False)
1.25 -\idx{select} P(x::'a) --> P(Eps(P))
1.26 -
1.27 -\idx{Inv_def} Inv = (%(f::'a=>'b) y. @x. f(x)=y)
1.28 -\idx{o_def} op o = (%(f::'b=>'c) g (x::'a). f(g(x)))
1.29 -\idx{Cond_def} Cond = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))
1.30 -
1.31 -----------------------------------------------------------------
1.32 -lemmas.ML
1.33 -
1.34 -\idx{sym} s=t ==> t=s
1.35 -\idx{trans} [| r=s; s=t |] ==> r=t
1.36 -\idx{box_equals}
1.37 - [| a=b; a=c; b=d |] ==> c=d
1.38 -\idx{ap_term} s=t ==> f(s)=f(t)
1.39 -\idx{ap_thm} s::'a=>'b = t ==> s(x)=t(x)
1.40 -\idx{cong}
1.41 - [| f = g; x::'a = y |] ==> f(x) = g(y)
1.42 -\idx{iffI}
1.43 - [| P ==> Q; Q ==> P |] ==> P=Q
1.44 -\idx{iffD1} [| P=Q; Q |] ==> P
1.45 -\idx{iffE}
1.46 - [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
1.47 -\idx{eqTrueI} P ==> P=True
1.48 -\idx{eqTrueE} P=True ==> P
1.49 -\idx{allI} (!!x::'a. P(x)) ==> !x. P(x)
1.50 -\idx{spec} !x::'a.P(x) ==> P(x)
1.51 -\idx{allE} [| !x.P(x); P(x) ==> R |] ==> R
1.52 -\idx{all_dupE}
1.53 - [| ! x.P(x); [| P(x); ! x.P(x) |] ==> R
1.54 - |] ==> R
1.55 -\idx{FalseE} False ==> P
1.56 -\idx{False_neq_True} False=True ==> P
1.57 -\idx{notI} (P ==> False) ==> ~P
1.58 -\idx{notE} [| ~P; P |] ==> R
1.59 -\idx{impE} [| P-->Q; P; Q ==> R |] ==> R
1.60 -\idx{rev_mp} [| P; P --> Q |] ==> Q
1.61 -\idx{contrapos} [| ~Q; P==>Q |] ==> ~P
1.62 -\idx{exI} P(x) ==> ? x::'a.P(x)
1.63 -\idx{exE} [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
1.64 -
1.65 -\idx{conjI} [| P; Q |] ==> P&Q
1.66 -\idx{conjunct1} [| P & Q |] ==> P
1.67 -\idx{conjunct2} [| P & Q |] ==> Q
1.68 -\idx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
1.69 -\idx{disjI1} P ==> P|Q
1.70 -\idx{disjI2} Q ==> P|Q
1.71 -\idx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
1.72 -\idx{ccontr} (~P ==> False) ==> P
1.73 -\idx{classical} (~P ==> P) ==> P
1.74 -\idx{notnotD} ~~P ==> P
1.75 -\idx{ex1I}
1.76 - [| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)
1.77 -\idx{ex1E}
1.78 - [| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R |] ==> R
1.79 -\idx{select_equality}
1.80 - [| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
1.81 -\idx{disjCI} (~Q ==> P) ==> P|Q
1.82 -\idx{excluded_middle} ~P | P
1.83 -\idx{impCE} [| P-->Q; ~P ==> R; Q ==> R |] ==> R
1.84 -\idx{iffCE}
1.85 - [| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
1.86 -\idx{exCI} (! x. ~P(x) ==> P(a)) ==> ? x.P(x)
1.87 -\idx{swap} ~P ==> (~Q ==> P) ==> Q
1.88 -
1.89 -----------------------------------------------------------------
1.90 -simpdata.ML
1.91 -
1.92 -\idx{if_True} Cond(True,x,y) = x
1.93 -\idx{if_False} Cond(False,x,y) = y
1.94 -\idx{if_P} P ==> Cond(P,x,y) = x
1.95 -\idx{if_not_P} ~P ==> Cond(P,x,y) = y
1.96 -\idx{expand_if}
1.97 - P(Cond(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
1.98 -
1.99 -----------------------------------------------------------------
1.100 -\idx{set.ML}
1.101 -
1.102 -\idx{CollectI} [| P(a) |] ==> a : \{x.P(x)\}
1.103 -\idx{CollectD} [| a : \{x.P(x)\} |] ==> P(a)
1.104 -\idx{set_ext} [| !!x. (x:A) = (x:B) |] ==> A = B
1.105 -
1.106 -\idx{Ball_def} Ball(A,P) == ! x. x:A --> P(x)
1.107 -\idx{Bex_def} Bex(A,P) == ? x. x:A & P(x)
1.108 -\idx{subset_def} A <= B == ! x:A. x:B
1.109 -\idx{Un_def} A Un B == \{x.x:A | x:B\}
1.110 -\idx{Int_def} A Int B == \{x.x:A & x:B\}
1.111 -\idx{Compl_def} Compl(A) == \{x. ~x:A\}
1.112 -\idx{Inter_def} Inter(S) == \{x. ! A:S. x:A\}
1.113 -\idx{Union_def} Union(S) == \{x. ? A:S. x:A\}
1.114 -\idx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\}
1.115 -\idx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\}
1.116 -\idx{mono_def} mono(f) == (!A B. A <= B --> f(A) <= f(B))
1.117 -\idx{image_def} f``A == \{y. ? x:A. y=f(x)\}
1.118 -\idx{singleton_def} \{a\} == \{x.x=a\}
1.119 -\idx{range_def} range(f) == \{y. ? x. y=f(x)\}
1.120 -\idx{One_One_def} One_One(f) == ! x y. f(x)=f(y) --> x=y
1.121 -\idx{One_One_on_def} One_One_on(f,A) == !x y. x:A --> y:A --> f(x)=f(y) --> x=y
1.122 -\idx{Onto_def} Onto(f) == ! y. ? x. y=f(x)
1.123 -
1.124 -
1.125 -\idx{Collect_cong} [| !!x. P(x)=Q(x) |] ==> \{x. P(x)\} = \{x. Q(x)\}
1.126 -
1.127 -\idx{ballI} [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
1.128 -\idx{bspec} [| ! x:A. P(x); x:A |] ==> P(x)
1.129 -\idx{ballE} [| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q
1.130 -
1.131 -\idx{bexI} [| P(x); x:A |] ==> ? x:A. P(x)
1.132 -\idx{bexCI} [| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A.P(x)
1.133 -\idx{bexE} [| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q
1.134 -
1.135 -\idx{ball_cong}
1.136 - [| A=A'; !!x. x:A' ==> P(x) = P'(x) |] ==>
1.137 - (! x:A. P(x)) = (! x:A'. P'(x))
1.138 -
1.139 -\idx{bex_cong}
1.140 - [| A=A'; !!x. x:A' ==> P(x) = P'(x) |] ==>
1.141 - (? x:A. P(x)) = (? x:A'. P'(x))
1.142 -
1.143 -\idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B
1.144 -\idx{subsetD} [| A <= B; c:A |] ==> c:B
1.145 -\idx{subsetCE} [| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P
1.146 -
1.147 -\idx{subset_refl} A <= A
1.148 -\idx{subset_antisym} [| A <= B; B <= A |] ==> A = B
1.149 -\idx{subset_trans} [| A<=B; B<=C |] ==> A<=C
1.150 -
1.151 -\idx{equalityD1} A = B ==> A<=B
1.152 -\idx{equalityD2} A = B ==> B<=A
1.153 -\idx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
1.154 -
1.155 -\idx{singletonI} a : \{a\}
1.156 -\idx{singletonD} b : \{a\} ==> b=a
1.157 -
1.158 -\idx{imageI} [| x:A |] ==> f(x) : f``A
1.159 -\idx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P
1.160 -
1.161 -\idx{rangeI} f(x) : range(f)
1.162 -\idx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P
1.163 -
1.164 -\idx{UnionI} [| X:C; A:X |] ==> A : Union(C)
1.165 -\idx{UnionE} [| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R
1.166 -
1.167 -\idx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C)
1.168 -\idx{InterD} [| A : Inter(C); X:C |] ==> A:X
1.169 -\idx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R
1.170 -
1.171 -\idx{UN_I} [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))
1.172 -\idx{UN_E} [| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R
1.173 -
1.174 -\idx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
1.175 -\idx{INT_D} [| b : (INT x:A. B(x)); a:A |] ==> b: B(a)
1.176 -\idx{INT_E} [| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R
1.177 -
1.178 -\idx{UnI1} c:A ==> c : A Un B
1.179 -\idx{UnI2} c:B ==> c : A Un B
1.180 -\idx{UnCI} (~c:B ==> c:A) ==> c : A Un B
1.181 -\idx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
1.182 -
1.183 -\idx{IntI} [| c:A; c:B |] ==> c : A Int B
1.184 -\idx{IntD1} c : A Int B ==> c:A
1.185 -\idx{IntD2} c : A Int B ==> c:B
1.186 -\idx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
1.187 -
1.188 -\idx{ComplI} [| c:A ==> False |] ==> c : Compl(A)
1.189 -\idx{ComplD} [| c : Compl(A) |] ==> ~c:A
1.190 -
1.191 -\idx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
1.192 -\idx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B)
1.193 -
1.194 -
1.195 -----------------------------------------------------------------
1.196 -\idx{fun.ML}
1.197 -
1.198 -\idx{One_OneI} [| !! x y. f(x) = f(y) ==> x=y |] ==> One_One(f)
1.199 -\idx{One_One_inverseI} (!!x. g(f(x)) = x) ==> One_One(f)
1.200 -\idx{One_OneD} [| One_One(f); f(x) = f(y) |] ==> x=y
1.201 -
1.202 -\idx{Inv_f_f} One_One(f) ==> Inv(f,f(x)) = x
1.203 -\idx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y
1.204 -
1.205 -\idx{Inv_injective}
1.206 - [| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y
1.207 -
1.208 -\idx{One_One_onI}
1.209 - (!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> One_One_on(f,A)
1.210 -
1.211 -\idx{One_One_on_inverseI}
1.212 - (!!x. x:A ==> g(f(x)) = x) ==> One_One_on(f,A)
1.213 -
1.214 -\idx{One_One_onD}
1.215 - [| One_One_on(f,A); f(x)=f(y); x:A; y:A |] ==> x=y
1.216 -
1.217 -\idx{One_One_on_contraD}
1.218 - [| One_One_on(f,A); ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)
1.219 -
1.220 -
1.221 -----------------------------------------------------------------
1.222 -\idx{subset.ML}
1.223 -
1.224 -\idx{Union_upper} B:A ==> B <= Union(A)
1.225 -\idx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
1.226 -
1.227 -\idx{Inter_lower} B:A ==> Inter(A) <= B
1.228 -\idx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
1.229 -
1.230 -\idx{Un_upper1} A <= A Un B
1.231 -\idx{Un_upper2} B <= A Un B
1.232 -\idx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
1.233 -
1.234 -\idx{Int_lower1} A Int B <= A
1.235 -\idx{Int_lower2} A Int B <= B
1.236 -\idx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
1.237 -
1.238 -
1.239 -----------------------------------------------------------------
1.240 -\idx{equalities.ML}
1.241 -
1.242 -\idx{Int_absorb} A Int A = A
1.243 -\idx{Int_commute} A Int B = B Int A
1.244 -\idx{Int_assoc} (A Int B) Int C = A Int (B Int C)
1.245 -\idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
1.246 -
1.247 -\idx{Un_absorb} A Un A = A
1.248 -\idx{Un_commute} A Un B = B Un A
1.249 -\idx{Un_assoc} (A Un B) Un C = A Un (B Un C)
1.250 -\idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
1.251 -
1.252 -\idx{Compl_disjoint} A Int Compl(A) = \{x.False\}
1.253 -\idx{Compl_partition A Un Compl(A) = \{x.True\}
1.254 -\idx{double_complement} Compl(Compl(A)) = A
1.255 -
1.256 -
1.257 -\idx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)
1.258 -\idx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)
1.259 -
1.260 -\idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)
1.261 -\idx{Int_Union_image} A Int Union(B) = (UN C:B. A Int C)
1.262 -\idx{Un_Union_image} (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
1.263 -
1.264 -\idx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)
1.265 -\idx{Un_Inter_image} A Un Inter(B) = (INT C:B. A Un C)
1.266 -\idx{Int_Inter_image} (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
1.267 -
1.268 -
1.269 -----------------------------------------------------------------
1.270 -prod.ML
1.271 -
1.272 - mixfix = [ Delimfix((1<_,/_>), ['a,'b] => ('a,'b)prod, Pair),
1.273 - TInfixl(*, prod, 20) ],
1.274 -thy = extend_theory Set.thy Prod
1.275 - [([prod],([[term],[term]],term))],
1.276 - ([fst], 'a * 'b => 'a),
1.277 - ([snd], 'a * 'b => 'b),
1.278 - ([split], ['a * 'b, ['a,'b]=>'c] => 'c)],
1.279 -\idx{fst_def} fst(p) == @a. ? b. p = <a,b>),
1.280 -\idx{snd_def} snd(p) == @b. ? a. p = <a,b>),
1.281 -\idx{split_def} split(p,c) == c(fst(p),snd(p)))
1.282 -
1.283 -\idx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
1.284 -
1.285 -\idx{fst_conv} fst(<a,b>) = a
1.286 -\idx{snd_conv} snd(<a,b>) = b
1.287 -\idx{split_conv} split(<a,b>, c) = c(a,b)
1.288 -
1.289 -\idx{surjective_pairing} p = <fst(p),snd(p)>
1.290 -
1.291 -----------------------------------------------------------------
1.292 -sum.ML
1.293 -
1.294 - mixfix = [TInfixl(+, sum, 10)],
1.295 -thy = extend_theory Prod.thy sum
1.296 - [([sum], ([[term],[term]],term))],
1.297 - [Inl], 'a => 'a+'b),
1.298 - [Inr], 'b => 'a+'b),
1.299 - [when], ['a+'b, 'a=>'c, 'b=>'c] =>'c)],
1.300 -\idx{when_def} when == (%p f g. @z. (!x. p=Inl(x) --> z=f(x))
1.301 - & (!y. p=Inr(y) --> z=g(y))))
1.302 -
1.303 -\idx{Inl_not_Inr} ~ (Inl(a) = Inr(b))
1.304 -
1.305 -\idx{One_One_Inl} One_One(Inl)
1.306 -
1.307 -\idx{One_One_Inr} One_One(Inr)
1.308 -
1.309 -\idx{when_Inl_conv} when(Inl(x), f, g) = f(x)
1.310 -
1.311 -\idx{when_Inr_conv} when(Inr(x), f, g) = g(x)
1.312 -
1.313 -\idx{sumE}
1.314 - [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y))
1.315 - |] ==> P(s)
1.316 -
1.317 -\idx{surjective_sum} when(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)
1.318 -
1.319 -
1.320 -????????????????????????????????????????????????????????????????
1.321 -trancl?
1.322 -
1.323 -----------------------------------------------------------------
1.324 -nat.ML
1.325 -
1.326 - Sext\{mixfix=[Delimfix(0, nat, 0),
1.327 - Infixl(<,[nat,nat] => bool,50)],
1.328 -thy = extend_theory Trancl.thy Nat
1.329 -[nat], ([],term))
1.330 -[nat_case], [nat, 'a, nat=>'a] =>'a),
1.331 -[pred_nat],nat*nat) set),
1.332 -[nat_rec], [nat, 'a, [nat, 'a]=>'a] => 'a)
1.333 -
1.334 -\idx{nat_case_def} nat_case == (%n a f. @z. (n=0 --> z=a)
1.335 - & (!x. n=Suc(x) --> z=f(x)))),
1.336 -\idx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\} ),
1.337 -\idx{less_def} m<n == <m,n>:trancl(pred_nat)),
1.338 -\idx{nat_rec_def}
1.339 - nat_rec(n,c,d) == wfrec(trancl(pred_nat),
1.340 - %rec l. nat_case(l, c, %m. d(m,rec(m))),
1.341 - n) )
1.342 -
1.343 -\idx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n)
1.344 -
1.345 -
1.346 -\idx{Suc_not_Zero} ~ (Suc(m) = 0)
1.347 -\idx{One_One_Suc} One_One(Suc)
1.348 -\idx{n_not_Suc_n} ~(n=Suc(n))
1.349 -
1.350 -\idx{nat_case_0_conv} nat_case(0, a, f) = a
1.351 -
1.352 -\idx{nat_case_Suc_conv} nat_case(Suc(k), a, f) = f(k)
1.353 -
1.354 -\idx{pred_natI} <n, Suc(n)> : pred_nat
1.355 -\idx{pred_natE}
1.356 - [| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> R
1.357 - |] ==> R
1.358 -
1.359 -\idx{wf_pred_nat} wf(pred_nat)
1.360 -
1.361 -\idx{nat_rec_0_conv} nat_rec(0,c,h) = c
1.362 -
1.363 -\idx{nat_rec_Suc_conv} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
1.364 -
1.365 -
1.366 -(*** Basic properties of less than ***)
1.367 -\idx{less_trans} [| i<j; j<k |] ==> i<k
1.368 -\idx{lessI} n < Suc(n)
1.369 -\idx{zero_less_Suc} 0 < Suc(n)
1.370 -
1.371 -\idx{less_not_sym} n<m --> ~m<n
1.372 -\idx{less_not_refl} ~ (n<n)
1.373 -\idx{not_less0} ~ (n<0)
1.374 -
1.375 -\idx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)
1.376 -\idx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n)
1.377 -
1.378 -\idx{less_linear} m<n | m=n | n<m
1.379 -
1.380 -
1.381 -----------------------------------------------------------------
1.382 -list.ML
1.383 -
1.384 - [([list], ([[term]],term))],
1.385 - ([Nil], 'a list),
1.386 - ([Cons], ['a, 'a list] => 'a list),
1.387 - ([list_rec], ['a list, 'b, ['a ,'a list, 'b]=>'b] => 'b),
1.388 - ([list_all], ('a => bool) => ('a list => bool)),
1.389 - ([map], ('a=>'b) => ('a list => 'b list))
1.390 -
1.391 -\idx{map_def} map(f,xs) == list_rec(xs, Nil, %x l r. Cons(f(x), r)) )
1.392 -
1.393 -\idx{list_induct}
1.394 - [| P(Nil);
1.395 - !!x xs. [| P(xs) |] ==> P(Cons(x,xs)) |] ==> P(l)
1.396 -
1.397 -\idx{Cons_not_Nil} ~ Cons(x,xs) = Nil
1.398 -\idx{Cons_Cons_eq} (Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys)
1.399 -
1.400 -\idx{list_rec_Nil_conv} list_rec(Nil,c,h) = c
1.401 -\idx{list_rec_Cons_conv} list_rec(Cons(a,l), c, h) =
1.402 - h(a, l, list_rec(l,c,h))
1.403 -
1.404 -\idx{map_Nil_conv} map(f,Nil) = Nil
1.405 -\idx{map_Cons_conv} map(f, Cons(x,xs)) = Cons(f(x), map(f,xs))
1.406 -