104

1 
%%%% RULES.ML


2 


3 
\idx{empty_set} ~(x:0)


4 
\idx{union_iff} A:Union(C) <> (EX B:C. A:B)


5 
\idx{power_set} A : Pow(B) <> A <= B


6 
\idx{infinity} 0:Inf & (ALL y:Inf. succ(y): Inf)


7 
\idx{foundation} A=0  (EX x:A. ALL y:x. ~ y:A)


8 


9 
\idx{replacement} (!!x y z.[ x:A; P(x,y); P(x,z) ] ==> y=z) ==>


10 
y : PrimReplace(A,P) <> (EX x:A. P(x,y))


11 


12 
\idx{Replace_def} Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))


13 
\idx{RepFun_def} RepFun(A,f) == Replace(A, %x u. u=f(x))


14 
\idx{Collect_def} Collect(A,P) == \{ y . x:A, x=y & P(x)\}


15 
\idx{the_def} The(P) == Union(\{y . x:\{0\}, P(y)\})


16 


17 
\idx{Upair_def} Upair(a,b) ==


18 
\{y. x:Pow(Pow(0)), (x=0 & y=a)  (x=Pow(0) & y=b)\}


19 


20 
\idx{Inter_def} Inter(A) == \{ x:Union(A) . ALL y:A. x:y\}


21 


22 
\idx{Un_def} A Un B == Union(Upair(A,B))


23 
\idx{Int_def} A Int B == Inter(Upair(A,B))


24 
\idx{Diff_def} A  B == \{ x:A . ~(x:B) \}


25 
\idx{cons_def} cons(a,A) == Upair(a,a) Un A


26 
\idx{succ_def} succ(i) == cons(i,i)


27 


28 
\idx{Pair_def} <a,b> == \{\{a,a\}, \{a,b\}\}


29 
\idx{fst_def} fst(A) == THE x. EX y. A=<x,y>


30 
\idx{snd_def} snd(A) == THE y. EX x. A=<x,y>


31 
\idx{split_def} split(p,c) == THE y. EX a b. p=<a,b> & y=c(a,b)


32 
\idx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}


33 


34 
\idx{domain_def} domain(r) == \{a:Union(Union(r)) . EX b. <a,b> : r\}


35 
\idx{range_def} range(r) == \{b:Union(Union(r)) . EX a. <a,b> : r\}


36 
\idx{field_def} field(r) == domain(r) Un range(r)


37 
\idx{image_def} r``A == \{y : range(r) . EX x:A. <x,y> : r\}


38 
\idx{vimage_def} r `` A == \{x : domain(r) . EX y:A. <x,y> : r\}


39 


40 
\idx{lam_def} Lambda(A,f) == RepFun(A, %x. <x,f(x)>)


41 
\idx{apply_def} f`a == THE y. <a,y> : f


42 
\idx{restrict_def} restrict(f,A) == lam x:A.f`x


43 
\idx{Pi_def} Pi(A,B) == \{f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f\}


44 


45 
\idx{subset_def} A <= B == ALL x:A. x:B


46 
\idx{strict_subset_def} A <! B == A <=B & ~(A=B)


47 
\idx{extension} A = B <> A <= B & B <= A


48 


49 
\idx{Ball_def} Ball(A,P) == ALL x. x:A > P(x)


50 
\idx{Bex_def} Bex(A,P) == EX x. x:A & P(x)


51 


52 


53 
%%%% LEMMAS.ML


54 


55 
\idx{ballI} [ !!x. x:A ==> P(x) ] ==> ALL x:A. P(x)


56 
\idx{bspec} [ ALL x:A. P(x); x: A ] ==> P(x)


57 
\idx{ballE} [ ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q ] ==> Q


58 


59 
\idx{ball_cong} [ A=A'; !!x. x:A' ==> P(x) <> P'(x) ] ==>


60 
(ALL x:A. P(x)) <> (ALL x:A'. P'(x))


61 


62 
\idx{bexI} [ P(x); x: A ] ==> EX x:A. P(x)


63 
\idx{bexCI} [ ALL x:A. ~P(x) ==> P(a); a: A ] ==> EX x:A.P(x)


64 
\idx{bexE} [ EX x:A. P(x); !!x. [ x:A; P(x) ] ==> Q ] ==> Q


65 


66 
\idx{bex_cong} [ A=A'; !!x. x:A' ==> P(x) <> P'(x) ] ==>


67 
(EX x:A. P(x)) <> (EX x:A'. P'(x))


68 


69 
\idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B


70 
\idx{subsetD} [ A <= B; c:A ] ==> c:B


71 
\idx{subsetCE} [ A <= B; ~(c:A) ==> P; c:B ==> P ] ==> P


72 
\idx{subset_refl} A <= A


73 
\idx{subset_trans} [ A<=B; B<=C ] ==> A<=C


74 


75 
\idx{equalityI} [ A <= B; B <= A ] ==> A = B


76 
\idx{equalityD1} A = B ==> A<=B


77 
\idx{equalityD2} A = B ==> B<=A


78 
\idx{equalityE} [ A = B; [ A<=B; B<=A ] ==> P ] ==> P


79 


80 
\idx{emptyE} a:0 ==> P


81 
\idx{empty_subsetI} 0 <= A


82 
\idx{equals0I} [ !!y. y:A ==> False ] ==> A=0


83 
\idx{equals0D} [ A=0; a:A ] ==> P


84 


85 
\idx{PowI} A <= B ==> A : Pow(B)


86 
\idx{PowD} A : Pow(B) ==> A<=B


87 


88 
\idx{ReplaceI} [ x: A; P(x,b); !!y. P(x,y) ==> y=b ] ==>


89 
b : \{y. x:A, P(x,y)\}


90 


91 
\idx{ReplaceE} [ b : \{y. x:A, P(x,y)\};


92 
!!x. [ x: A; P(x,b); ALL y. P(x,y)>y=b ] ==> R


93 
] ==> R


94 


95 
\idx{Replace_cong} [ A=B; !!x y. x:B ==> P(x,y) <> Q(x,y) ] ==>


96 
\{y. x:A, P(x,y)\} = \{y. x:B, Q(x,y)\}


97 


98 
\idx{RepFunI} [ a : A ] ==> f(a) : RepFun(A,f)


99 
\idx{RepFunE} [ b : RepFun(A, %x.f(x));


100 
!!x.[ x:A; b=f(x) ] ==> P ] ==> P


101 


102 
\idx{RepFun_cong} [ A=B; !!x. x:B ==> f(x)=g(x) ] ==>


103 
RepFun(A, %x.f(x)) = RepFun(B, %x.g(x))


104 


105 


106 
\idx{separation} x : Collect(A,P) <> x:A & P(x)


107 
\idx{CollectI} [ a:A; P(a) ] ==> a : \{x:A. P(x)\}


108 
\idx{CollectE} [ a : \{x:A. P(x)\}; [ a:A; P(a) ] ==> R ] ==> R


109 
\idx{CollectD1} a : \{x:A. P(x)\} ==> a:A


110 
\idx{CollectD2} a : \{x:A. P(x)\} ==> P(a)


111 


112 
\idx{Collect_cong} [ A=B; !!x. x:B ==> P(x) <> Q(x) ] ==>


113 
\{x:A. P(x)\} = \{x:B. Q(x)\}


114 


115 
\idx{UnionI} [ B: C; A: B ] ==> A: Union(C)


116 
\idx{UnionE} [ A : Union(C); !!B.[ A: B; B: C ] ==> R ] ==> R


117 


118 
\idx{InterI} [ !!x. x: C ==> A: x; c:C ] ==> A : Inter(C)


119 
\idx{InterD} [ A : Inter(C); B : C ] ==> A : B


120 
\idx{InterE} [ A : Inter(C); A:B ==> R; ~ B:C ==> R ] ==> R


121 


122 
\idx{UN_I} [ a: A; b: B(a) ] ==> b: (UN x:A. B(x))


123 
\idx{UN_E} [ b : (UN x:A. B(x)); !!x.[ x: A; b: B(x) ] ==> R ] ==> R


124 


125 
\idx{INT_I} [ !!x. x: A ==> b: B(x); a: A ] ==> b: (INT x:A. B(x))


126 
\idx{INT_E} [ b : (INT x:A. B(x)); a: A ] ==> b : B(a)


127 


128 


129 
%%%% UPAIR.ML


130 


131 
\idx{pairing} a:Upair(b,c) <> (a=b  a=c)


132 
\idx{UpairI1} a : Upair(a,b)


133 
\idx{UpairI2} b : Upair(a,b)


134 
\idx{UpairE} [ a : Upair(b,c); a = b ==> P; a = c ==> P ] ==> P


135 


136 
\idx{UnI1} c : A ==> c : A Un B


137 
\idx{UnI2} c : B ==> c : A Un B


138 
\idx{UnCI} (~c : B ==> c : A) ==> c : A Un B


139 
\idx{UnE} [ c : A Un B; c:A ==> P; c:B ==> P ] ==> P


140 


141 
\idx{IntI} [ c : A; c : B ] ==> c : A Int B


142 
\idx{IntD1} c : A Int B ==> c : A


143 
\idx{IntD2} c : A Int B ==> c : B


144 
\idx{IntE} [ c : A Int B; [ c:A; c:B ] ==> P ] ==> P


145 


146 
\idx{DiffI} [ c : A; ~ c : B ] ==> c : A  B


147 
\idx{DiffD1} c : A  B ==> c : A


148 
\idx{DiffD2} [ c : A  B; c : B ] ==> P


149 
\idx{DiffE} [ c : A  B; [ c:A; ~ c:B ] ==> P ] ==> P


150 


151 
\idx{consI1} a : cons(a,B)


152 
\idx{consI2} a : B ==> a : cons(b,B)


153 
\idx{consCI} (~ a:B ==> a=b) ==> a: cons(b,B)


154 
\idx{consE} [ a : cons(b,A); a=b ==> P; a:A ==> P ] ==> P


155 


156 
\idx{singletonI} a : \{a\}


157 
\idx{singletonE} [ a : \{b\}; a=b ==> P ] ==> P


158 


159 
\idx{succI1} i : succ(i)


160 
\idx{succI2} i : j ==> i : succ(j)


161 
\idx{succCI} (~ i:j ==> i=j) ==> i: succ(j)


162 
\idx{succE} [ i : succ(j); i=j ==> P; i:j ==> P ] ==> P


163 
\idx{succ_neq_0} [ succ(n)=0 ] ==> P


164 
\idx{succ_inject} succ(m) = succ(n) ==> m=n


165 


166 
\idx{the_equality} [ P(a); !!x. P(x) ==> x=a ] ==> (THE x. P(x)) = a


167 
\idx{theI} EX! x. P(x) ==> P(THE x. P(x))


168 


169 
\idx{mem_anti_sym} [ a:b; b:a ] ==> P


170 
\idx{mem_anti_refl} a:a ==> P


171 


172 


173 
%%% SUBSET.ML


174 


175 
\idx{Union_upper} B:A ==> B <= Union(A)


176 
\idx{Union_least} [ !!x. x:A ==> x<=C ] ==> Union(A) <= C


177 


178 
\idx{Inter_lower} B:A ==> Inter(A) <= B


179 
\idx{Inter_greatest} [ a:A; !!x. x:A ==> C<=x ] ==> C <= Inter(A)


180 


181 
\idx{Un_upper1} A <= A Un B


182 
\idx{Un_upper2} B <= A Un B


183 
\idx{Un_least} [ A<=C; B<=C ] ==> A Un B <= C


184 


185 
\idx{Int_lower1} A Int B <= A


186 
\idx{Int_lower2} A Int B <= B


187 
\idx{Int_greatest} [ C<=A; C<=B ] ==> C <= A Int B


188 


189 
\idx{Diff_subset} AB <= A


190 
\idx{Diff_contains} [ C<=A; C Int B = 0 ] ==> C <= AB


191 


192 
\idx{Collect_subset} Collect(A,P) <= A


193 


194 
%%% PAIR.ML


195 


196 
\idx{Pair_inject1} <a,b> = <c,d> ==> a=c


197 
\idx{Pair_inject2} <a,b> = <c,d> ==> b=d


198 
\idx{Pair_inject} [ <a,b> = <c,d>; [ a=c; b=d ] ==> P ] ==> P


199 
\idx{Pair_neq_0} <a,b>=0 ==> P


200 


201 
\idx{fst_conv} fst(<a,b>) = a


202 
\idx{snd_conv} snd(<a,b>) = b


203 
\idx{split_conv} split(<a,b>, %x y.c(x,y)) = c(a,b)


204 


205 
\idx{SigmaI} [ a:A; b:B(a) ] ==> <a,b> : (SUM x:A. B(x))


206 


207 
\idx{SigmaE} [ c: (SUM x:A. B(x));


208 
!!x y.[ x:A; y:B(x); c=<x,y> ] ==> P


209 
] ==> P


210 


211 
\idx{SigmaE2} [ <a,b> : (SUM x:A. B(x));


212 
[ a:A; b:B(a) ] ==> P


213 
] ==> P


214 


215 


216 
%%% DOMRANGE.ML


217 


218 
\idx{domainI} <a,b>: r ==> a : domain(r)


219 
\idx{domainE} [ a : domain(r); !!y. <a,y>: r ==> P ] ==> P


220 
\idx{domain_subset} domain(Sigma(A,B)) <= A


221 


222 
\idx{rangeI} <a,b>: r ==> b : range(r)


223 
\idx{rangeE} [ b : range(r); !!x. <x,b>: r ==> P ] ==> P


224 
\idx{range_subset} range(A*B) <= B


225 


226 
\idx{fieldI1} <a,b>: r ==> a : field(r)


227 
\idx{fieldI2} <a,b>: r ==> b : field(r)


228 
\idx{fieldCI} (~ <c,a>:r ==> <a,b>: r) ==> a : field(r)


229 


230 
\idx{fieldE} [ a : field(r);


231 
!!x. <a,x>: r ==> P;


232 
!!x. <x,a>: r ==> P


233 
] ==> P


234 


235 
\idx{field_subset} field(A*A) <= A


236 


237 
\idx{imageI} [ <a,b>: r; a:A ] ==> b : r``A


238 
\idx{imageE} [ b: r``A; !!x.[ <x,b>: r; x:A ] ==> P ] ==> P


239 


240 
\idx{vimageI} [ <a,b>: r; b:B ] ==> a : r``B


241 
\idx{vimageE} [ a: r``B; !!x.[ <a,x>: r; x:B ] ==> P ] ==> P


242 


243 


244 
%%% FUNC.ML


245 


246 
\idx{fun_is_rel} f: (PROD x:A.B(x)) ==> f <= Sigma(A,B)


247 


248 
\idx{apply_equality} [ <a,b>: f; f: (PROD x:A.B(x)) ] ==> f`a = b


249 
\idx{apply_equality2} [ <a,b>: f; <a,c>: f; f: (PROD x:A.B(x)) ] ==> b=c


250 


251 
\idx{apply_type} [ f: (PROD x:A.B(x)); a:A ] ==> f`a : B(a)


252 
\idx{apply_Pair} [ f: (PROD x:A.B(x)); a:A ] ==> <a,f`a>: f


253 
\idx{apply_iff} [ f: (PROD x:A.B(x)); a:A ] ==> <a,b>: f <> f`a = b


254 


255 
\idx{domain_type} [ <a,b> : f; f: (PROD x:A.B(x)) ] ==> a : A


256 
\idx{range_type} [ <a,b> : f; f: (PROD x:A.B(x)) ] ==> b : B(a)


257 


258 
\idx{Pi_type} [ f: A>C; !!x. x:A ==> f`x : B(x) ] ==> f: Pi(A,B)


259 
\idx{domain_of_fun} f : Pi(A,B) ==> domain(f)=A


260 
\idx{range_of_fun} f : Pi(A,B) ==> f: A>range(f)


261 


262 
\idx{fun_extension} [ f : (PROD x:A.B(x)); g: (PROD x:A.D(x));


263 
!!x. x:A ==> f`x = g`x


264 
] ==> f=g


265 


266 
\idx{lamI} a:A ==> <a,b(a)> : (lam x:A. b(x))


267 
\idx{lamE} [ p: (lam x:A. b(x)); !!x.[ x:A; p=<x,b(x)> ] ==> P


268 
] ==> P


269 


270 
\idx{lam_type} [ !!x. x:A ==> b(x): B(x) ] ==>


271 
(lam x:A.b(x)) : (PROD x:A.B(x))


272 


273 
\idx{beta_conv} a : A ==> (lam x:A.b(x)) ` a = b(a)


274 
\idx{eta_conv} f : (PROD x:A.B(x)) ==> (lam x:A. f`x) = f


275 


276 
\idx{lam_theI} (!!x. x:A ==> EX! y. Q(x,y)) ==> EX h. ALL x:A. Q(x, h`x)


277 


278 
\idx{restrict_conv} a : A ==> restrict(f,A) ` a = f`a


279 
\idx{restrict_type} [ !!x. x:A ==> f`x: B(x) ] ==>


280 
restrict(f,A) : (PROD x:A.B(x))


281 


282 
\idx{fun_empty} 0: 0>0


283 
\idx{fun_single} \{<a,b>\} : \{a\} > \{b\}


284 


285 
\idx{fun_disjoint_Un} [ f: A>B; g: C>D; A Int C = 0 ] ==>


286 
(f Un g) : (A Un C) > (B Un D)


287 


288 
\idx{fun_disjoint_apply1} [ a:A; f: A>B; g: C>D; A Int C = 0 ] ==>


289 
(f Un g)`a = f`a


290 


291 
\idx{fun_disjoint_apply2} [ c:C; f: A>B; g: C>D; A Int C = 0 ] ==>


292 
(f Un g)`c = g`c


293 


294 


295 
%%% SIMPDATA.ML


296 


297 
a\in a & \bimp & False\\


298 
a\in \emptyset & \bimp & False\\


299 
a \in A \union B & \bimp & a\in A \disj a\in B\\


300 
a \in A \inter B & \bimp & a\in A \conj a\in B\\


301 
a \in AB & \bimp & a\in A \conj \neg (a\in B)\\


302 
a \in {\tt cons}(b,B) & \bimp & a=b \disj a\in B\\


303 
i \in {\tt succ}(j) & \bimp & i=j \disj i\in j\\


304 
A\in \bigcup(C) & \bimp & (\exists B. B\in C \conj A\in B)\\


305 
A\in \bigcap(C) & \bimp & (\forall B. B\in C \imp A\in B)


306 
\qquad (\exists B. B\in C)\\


307 
a \in {\tt Collect}(A,P) & \bimp & a\in A \conj P(a)\\


308 
b \in {\tt RepFun}(A,f) & \bimp & (\exists x. x\in A \conj b=f(x))


309 


310 
equalities.ML perm.ML plus.ML nat.ML


311 



312 
equalities.ML


313 


314 
\idx{Int_absorb} A Int A = A


315 
\idx{Int_commute} A Int B = B Int A


316 
\idx{Int_assoc} (A Int B) Int C = A Int (B Int C)


317 
\idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)


318 


319 
\idx{Un_absorb} A Un A = A


320 
\idx{Un_commute} A Un B = B Un A


321 
\idx{Un_assoc} (A Un B) Un C = A Un (B Un C)


322 
\idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)


323 


324 
\idx{Diff_cancel} AA = 0


325 
\idx{Diff_disjoint} A Int (BA) = 0


326 
\idx{Diff_partition} A<=B ==> A Un (BA) = B


327 
\idx{double_complement} [ A<=B; B<= C ] ==> (B  (CA)) = A


328 
\idx{Diff_Un} A  (B Un C) = (AB) Int (AC)


329 
\idx{Diff_Int} A  (B Int C) = (AB) Un (AC)


330 


331 
\idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)


332 
\idx{Inter_Un_distrib} [ a:A; b:B ] ==>


333 
Inter(A Un B) = Inter(A) Int Inter(B)


334 


335 
\idx{Int_Union_RepFun} A Int Union(B) = (UN C:B. A Int C)


336 


337 
\idx{Un_Inter_RepFun} b:B ==>


338 
A Un Inter(B) = (INT C:B. A Un C)


339 


340 
\idx{SUM_Un_distrib1} (SUM x:A Un B. C(x)) =


341 
(SUM x:A. C(x)) Un (SUM x:B. C(x))


342 


343 
\idx{SUM_Un_distrib2} (SUM x:C. A(x) Un B(x)) =


344 
(SUM x:C. A(x)) Un (SUM x:C. B(x))


345 


346 
\idx{SUM_Int_distrib1} (SUM x:A Int B. C(x)) =


347 
(SUM x:A. C(x)) Int (SUM x:B. C(x))


348 


349 
\idx{SUM_Int_distrib2} (SUM x:C. A(x) Int B(x)) =


350 
(SUM x:C. A(x)) Int (SUM x:C. B(x))


351 


352 


353 



354 
perm.ML


355 


356 
\idx{comp_def}


357 
r O s == \{xz : domain(s)*range(r) .


358 
EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r\}),


359 
\idx{id_def} (*the identity function for A*)


360 
id(A) == (lam x:A. x)),


361 
\idx{inj_def}


362 
inj(A,B) ==


363 
\{ f: A>B. ALL w:A. ALL x:A. f`w=f`x > w=x\}),


364 
\idx{surj_def}


365 
surj(A,B) == \{ f: A>B . ALL y:B. EX x:A. f`x=y\}),


366 
\idx{bij_def}


367 
bij(A,B) == inj(A,B) Int surj(A,B))


368 


369 


370 
\idx{surj_is_fun} f: surj(A,B) ==> f: A>B


371 
\idx{fun_is_surj} f : Pi(A,B) ==> f: surj(A,range(f))


372 


373 
\idx{inj_is_fun} f: inj(A,B) ==> f: A>B


374 
\idx{inj_equality} [ <a,b>:f; <c,b>:f; f: inj(A,B) ] ==> a=c


375 


376 
\idx{bij_is_fun} f: bij(A,B) ==> f: A>B


377 


378 
\idx{inj_converse_surj} f: inj(A,B) ==> converse(f): surj(range(f), A)


379 


380 
\idx{left_inverse} [ f: inj(A,B); a: A ] ==> converse(f)`(f`a) = a


381 
\idx{right_inverse} [ f: inj(A,B); b: range(f) ] ==>


382 
f`(converse(f)`b) = b


383 


384 
\idx{inj_converse_inj} f: inj(A,B) ==> converse(f): inj(range(f), A)


385 
\idx{bij_converse_bij} f: bij(A,B) ==> converse(f): bij(B,A)


386 


387 
\idx{comp_type} [ s<=A*B; r<=B*C ] ==> (r O s) <= A*C


388 
\idx{comp_assoc} (r O s) O t = r O (s O t)


389 


390 
\idx{left_comp_id} r<=A*B ==> id(B) O r = r


391 
\idx{right_comp_id} r<=A*B ==> r O id(A) = r


392 


393 
\idx{comp_func} [ g: A>B; f: B>C ] ==> (f O g) : A>C


394 
\idx{comp_func_apply} [ g: A>B; f: B>C; a:A ] ==> (f O g)`a = f`(g`a)


395 


396 
\idx{comp_inj} [ g: inj(A,B); f: inj(B,C) ] ==> (f O g) : inj(A,C)


397 
\idx{comp_surj} [ g: surj(A,B); f: surj(B,C) ] ==> (f O g) : surj(A,C)


398 
\idx{comp_bij} [ g: bij(A,B); f: bij(B,C) ] ==> (f O g) : bij(A,C)


399 


400 
\idx{left_comp_inverse} f: inj(A,B) ==> converse(f) O f = id(A)


401 
\idx{right_comp_inverse} f: surj(A,B) ==> f O converse(f) = id(B)


402 


403 
\idx{bij_disjoint_Un}


404 
[ f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 ] ==>


405 
(f Un g) : bij(A Un C, B Un D)


406 


407 
\idx{restrict_bij} [ f: inj(A,B); C<=A ] ==> restrict(f,C): bij(C, f``C)


408 


409 


410 



411 
plus.ML


412 


413 
\idx{plus_def} A+B == \{0\}*A Un \{\{0\}\}*B


414 
\idx{Inl_def} Inl(a) == < 0 ,a>


415 
\idx{Inr_def} Inr(b) == <\{0\},b>


416 
\idx{when_def} when(u,c,d) ==


417 
THE y. EX z.(u=Inl(z) & y=c(z))  (u=Inr(z) & y=d(z))


418 


419 
\idx{plus_InlI} a : A ==> Inl(a) : A+B


420 
\idx{plus_InrI} b : B ==> Inr(b) : A+B


421 


422 
\idx{Inl_inject} Inl(a) = Inl(b) ==> a=b


423 
\idx{Inr_inject} Inr(a) = Inr(b) ==> a=b


424 
\idx{Inl_neq_Inr} Inl(a)=Inr(b) ==> P


425 


426 
\idx{plusE2} u: A+B ==> (EX x. x:A & u=Inl(x))  (EX y. y:B & u=Inr(y))


427 


428 
\idx{when_Inl_conv} when(Inl(a),c,d) = c(a)


429 
\idx{when_Inr_conv} when(Inr(b),c,d) = d(b)


430 


431 
\idx{when_type} [ u: A+B;


432 
!!x. x: A ==> c(x): C(Inl(x));


433 
!!y. y: B ==> d(y): C(Inr(y))


434 
] ==> when(u,c,d) : C(u)


435 


436 


437 



438 
nat.ML


439 


440 


441 
\idx{nat_def} nat == lfp(lam r: Pow(Inf). \{0\} Un RepFun(r,succ))


442 
\idx{nat_case_def} nat_case(n,a,b) ==


443 
THE y. n=0 & y=a  (EX x. n=succ(x) & y=b(x))


444 
\idx{nat_rec_def} nat_rec(k,a,b) ==


445 
transrec(nat, k, %n f. nat_case(n, a, %m. b(m, f`m)))


446 


447 
\idx{nat_0_I} 0 : nat


448 
\idx{nat_succ_I} n : nat ==> succ(n) : nat


449 


450 
\idx{nat_induct}


451 
[ n: nat; P(0); !!x. [ x: nat; P(x) ] ==> P(succ(x))


452 
] ==> P(n)


453 


454 
\idx{nat_case_0_conv} nat_case(0,a,b) = a


455 
\idx{nat_case_succ_conv} nat_case(succ(m),a,b) = b(m)


456 


457 
\idx{nat_case_type}


458 
[ n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m))


459 
] ==> nat_case(n,a,b) : C(n)


460 


461 
\idx{nat_rec_0_conv} nat_rec(0,a,b) = a


462 
\idx{nat_rec_succ_conv} m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))


463 


464 
\idx{nat_rec_type}


465 
[ n: nat;


466 
a: C(0);


467 
!!m z. [ m: nat; z: C(m) ] ==> b(m,z): C(succ(m))


468 
] ==> nat_rec(n,a,b) : C(n)
