1.1 --- a/doc-src/ZF/ZF.tex Wed Aug 20 11:12:48 2003 +0200
1.2 +++ b/doc-src/ZF/ZF.tex Wed Aug 20 13:05:22 2003 +0200
1.3 @@ -231,7 +231,7 @@
1.4 & | & term " -`` " term \\
1.5 & | & term " ` " term \\
1.6 & | & term " * " term \\
1.7 - & | & term " Int " term \\
1.8 + & | & term " \isasyminter " term \\
1.9 & | & term " \isasymunion " term \\
1.10 & | & term " - " term \\
1.11 & | & term " -> " term \\
1.12 @@ -373,7 +373,7 @@
1.13
1.14 \tdx{Inter_def}: Inter(A) == {\ttlbrace}x \isasymin Union(A) . {\isasymforall}y \isasymin A. x \isasymin y{\ttrbrace}
1.15 \tdx{Un_def}: A \isasymunion B == Union(Upair(A,B))
1.16 -\tdx{Int_def}: A Int B == Inter(Upair(A,B))
1.17 +\tdx{Int_def}: A \isasyminter B == Inter(Upair(A,B))
1.18 \tdx{Diff_def}: A - B == {\ttlbrace}x \isasymin A . x \isasymnotin B{\ttrbrace}
1.19 \subcaption{Union, intersection, difference}
1.20 \end{alltt*}
1.21 @@ -434,7 +434,8 @@
1.22 same set, if $P(x,y)$ is single-valued. The nice syntax for replacement
1.23 expands to \isa{Replace}.
1.24
1.25 -Other consequences of replacement include functional replacement
1.26 +Other consequences of replacement include replacement for
1.27 +meta-level functions
1.28 (\cdx{RepFun}) and definite descriptions (\cdx{The}).
1.29 Axioms for separation (\cdx{Collect}) and unordered pairs
1.30 (\cdx{Upair}) are traditionally assumed, but they actually follow
1.31 @@ -617,10 +618,10 @@
1.32 \tdx{UnCI}: (c \isasymnotin B ==> c\isasymin{}A) ==> c\isasymin{}A \isasymunion B
1.33 \tdx{UnE}: [| c\isasymin{}A \isasymunion B; c\isasymin{}A ==> P; c\isasymin{}B ==> P |] ==> P
1.34
1.35 -\tdx{IntI}: [| c\isasymin{}A; c\isasymin{}B |] ==> c\isasymin{}A Int B
1.36 -\tdx{IntD1}: c\isasymin{}A Int B ==> c\isasymin{}A
1.37 -\tdx{IntD2}: c\isasymin{}A Int B ==> c\isasymin{}B
1.38 -\tdx{IntE}: [| c\isasymin{}A Int B; [| c\isasymin{}A; c\isasymin{}B |] ==> P |] ==> P
1.39 +\tdx{IntI}: [| c\isasymin{}A; c\isasymin{}B |] ==> c\isasymin{}A \isasyminter B
1.40 +\tdx{IntD1}: c\isasymin{}A \isasyminter B ==> c\isasymin{}A
1.41 +\tdx{IntD2}: c\isasymin{}A \isasyminter B ==> c\isasymin{}B
1.42 +\tdx{IntE}: [| c\isasymin{}A \isasyminter B; [| c\isasymin{}A; c\isasymin{}B |] ==> P |] ==> P
1.43
1.44 \tdx{DiffI}: [| c\isasymin{}A; c \isasymnotin B |] ==> c\isasymin{}A - B
1.45 \tdx{DiffD1}: c\isasymin{}A - B ==> c\isasymin{}A
1.46 @@ -715,12 +716,12 @@
1.47 \tdx{Un_upper2}: B \isasymsubseteq A \isasymunion B
1.48 \tdx{Un_least}: [| A \isasymsubseteq C; B \isasymsubseteq C |] ==> A \isasymunion B \isasymsubseteq C
1.49
1.50 -\tdx{Int_lower1}: A Int B \isasymsubseteq A
1.51 -\tdx{Int_lower2}: A Int B \isasymsubseteq B
1.52 -\tdx{Int_greatest}: [| C \isasymsubseteq A; C \isasymsubseteq B |] ==> C \isasymsubseteq A Int B
1.53 +\tdx{Int_lower1}: A \isasyminter B \isasymsubseteq A
1.54 +\tdx{Int_lower2}: A \isasyminter B \isasymsubseteq B
1.55 +\tdx{Int_greatest}: [| C \isasymsubseteq A; C \isasymsubseteq B |] ==> C \isasymsubseteq A \isasyminter B
1.56
1.57 \tdx{Diff_subset}: A-B \isasymsubseteq A
1.58 -\tdx{Diff_contains}: [| C \isasymsubseteq A; C Int B = 0 |] ==> C \isasymsubseteq A-B
1.59 +\tdx{Diff_contains}: [| C \isasymsubseteq A; C \isasyminter B = 0 |] ==> C \isasymsubseteq A-B
1.60
1.61 \tdx{Collect_subset}: Collect(A,P) \isasymsubseteq A
1.62 \end{alltt*}
1.63 @@ -825,9 +826,9 @@
1.64 \tdx{fieldCI}: (<c,a> \isasymnotin r ==> <a,b>\isasymin{}r) ==> a\isasymin{}field(r)
1.65
1.66 \tdx{fieldE}: [| a\isasymin{}field(r);
1.67 - !!x. <a,x>\isasymin{}r ==> P;
1.68 - !!x. <x,a>\isasymin{}r ==> P
1.69 - |] ==> P
1.70 + !!x. <a,x>\isasymin{}r ==> P;
1.71 + !!x. <x,a>\isasymin{}r ==> P
1.72 + |] ==> P
1.73
1.74 \tdx{field_subset}: field(A*A) \isasymsubseteq A
1.75 \end{alltt*}
1.76 @@ -867,7 +868,7 @@
1.77 \begin{alltt*}\isastyleminor
1.78 \tdx{fun_is_rel}: f\isasymin{}Pi(A,B) ==> f \isasymsubseteq Sigma(A,B)
1.79
1.80 -\tdx{apply_equality}: [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> f`a = b
1.81 +\tdx{apply_equality}: [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> f`a = b
1.82 \tdx{apply_equality2}: [| <a,b>\isasymin{}f; <a,c>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> b=c
1.83
1.84 \tdx{apply_type}: [| f\isasymin{}Pi(A,B); a\isasymin{}A |] ==> f`a\isasymin{}B(a)
1.85 @@ -912,7 +913,7 @@
1.86 \tdx{fun_empty}: 0\isasymin{}0->0
1.87 \tdx{fun_single}: {\ttlbrace}<a,b>{\ttrbrace}\isasymin{}{\ttlbrace}a{\ttrbrace} -> {\ttlbrace}b{\ttrbrace}
1.88
1.89 -\tdx{fun_disjoint_Un}: [| f\isasymin{}A->B; g\isasymin{}C->D; A Int C = 0 |] ==>
1.90 +\tdx{fun_disjoint_Un}: [| f\isasymin{}A->B; g\isasymin{}C->D; A \isasyminter C = 0 |] ==>
1.91 (f \isasymunion g)\isasymin{}(A \isasymunion C) -> (B \isasymunion D)
1.92
1.93 \tdx{fun_disjoint_apply1}: [| a\isasymin{}A; f\isasymin{}A->B; g\isasymin{}C->D; A\isasyminter{}C = 0 |] ==>
1.94 @@ -955,28 +956,28 @@
1.95
1.96 \begin{figure}
1.97 \begin{alltt*}\isastyleminor
1.98 -\tdx{Int_absorb}: A Int A = A
1.99 -\tdx{Int_commute}: A Int B = B Int A
1.100 -\tdx{Int_assoc}: (A Int B) Int C = A Int (B Int C)
1.101 -\tdx{Int_Un_distrib}: (A \isasymunion B) Int C = (A Int C) \isasymunion (B Int C)
1.102 +\tdx{Int_absorb}: A \isasyminter A = A
1.103 +\tdx{Int_commute}: A \isasyminter B = B \isasyminter A
1.104 +\tdx{Int_assoc}: (A \isasyminter B) \isasyminter C = A \isasyminter (B \isasyminter C)
1.105 +\tdx{Int_Un_distrib}: (A \isasymunion B) \isasyminter C = (A \isasyminter C) \isasymunion (B \isasyminter C)
1.106
1.107 \tdx{Un_absorb}: A \isasymunion A = A
1.108 \tdx{Un_commute}: A \isasymunion B = B \isasymunion A
1.109 \tdx{Un_assoc}: (A \isasymunion B) \isasymunion C = A \isasymunion (B \isasymunion C)
1.110 -\tdx{Un_Int_distrib}: (A Int B) \isasymunion C = (A \isasymunion C) Int (B \isasymunion C)
1.111 +\tdx{Un_Int_distrib}: (A \isasyminter B) \isasymunion C = (A \isasymunion C) \isasyminter (B \isasymunion C)
1.112
1.113 \tdx{Diff_cancel}: A-A = 0
1.114 -\tdx{Diff_disjoint}: A Int (B-A) = 0
1.115 +\tdx{Diff_disjoint}: A \isasyminter (B-A) = 0
1.116 \tdx{Diff_partition}: A \isasymsubseteq B ==> A \isasymunion (B-A) = B
1.117 \tdx{double_complement}: [| A \isasymsubseteq B; B \isasymsubseteq C |] ==> (B - (C-A)) = A
1.118 -\tdx{Diff_Un}: A - (B \isasymunion C) = (A-B) Int (A-C)
1.119 -\tdx{Diff_Int}: A - (B Int C) = (A-B) \isasymunion (A-C)
1.120 +\tdx{Diff_Un}: A - (B \isasymunion C) = (A-B) \isasyminter (A-C)
1.121 +\tdx{Diff_Int}: A - (B \isasyminter C) = (A-B) \isasymunion (A-C)
1.122
1.123 \tdx{Union_Un_distrib}: Union(A \isasymunion B) = Union(A) \isasymunion Union(B)
1.124 \tdx{Inter_Un_distrib}: [| a \isasymin A; b \isasymin B |] ==>
1.125 - Inter(A \isasymunion B) = Inter(A) Int Inter(B)
1.126 -
1.127 -\tdx{Int_Union_RepFun}: A Int Union(B) = ({\isasymUnion}C \isasymin B. A Int C)
1.128 + Inter(A \isasymunion B) = Inter(A) \isasyminter Inter(B)
1.129 +
1.130 +\tdx{Int_Union_RepFun}: A \isasyminter Union(B) = ({\isasymUnion}C \isasymin B. A \isasyminter C)
1.131
1.132 \tdx{Un_Inter_RepFun}: b \isasymin B ==>
1.133 A \isasymunion Inter(B) = ({\isasymInter}C \isasymin B. A \isasymunion C)
1.134 @@ -987,11 +988,11 @@
1.135 \tdx{SUM_Un_distrib2}: (SUM x \isasymin C. A(x) \isasymunion B(x)) =
1.136 (SUM x \isasymin C. A(x)) \isasymunion (SUM x \isasymin C. B(x))
1.137
1.138 -\tdx{SUM_Int_distrib1}: (SUM x \isasymin A Int B. C(x)) =
1.139 - (SUM x \isasymin A. C(x)) Int (SUM x \isasymin B. C(x))
1.140 -
1.141 -\tdx{SUM_Int_distrib2}: (SUM x \isasymin C. A(x) Int B(x)) =
1.142 - (SUM x \isasymin C. A(x)) Int (SUM x \isasymin C. B(x))
1.143 +\tdx{SUM_Int_distrib1}: (SUM x \isasymin A \isasyminter B. C(x)) =
1.144 + (SUM x \isasymin A. C(x)) \isasyminter (SUM x \isasymin B. C(x))
1.145 +
1.146 +\tdx{SUM_Int_distrib2}: (SUM x \isasymin C. A(x) \isasyminter B(x)) =
1.147 + (SUM x \isasymin C. A(x)) \isasyminter (SUM x \isasymin C. B(x))
1.148 \end{alltt*}
1.149 \caption{Equalities} \label{zf-equalities}
1.150 \end{figure}
1.151 @@ -1109,13 +1110,13 @@
1.152 \begin{figure}
1.153 \begin{alltt*}\isastyleminor
1.154 \tdx{bnd_mono_def}: bnd_mono(D,h) ==
1.155 - h(D) \isasymsubseteq D & ({\isasymforall}W X. W \isasymsubseteq X --> X \isasymsubseteq D --> h(W) \isasymsubseteq h(X))
1.156 + h(D)\isasymsubseteq{}D & ({\isasymforall}W X. W\isasymsubseteq{}X --> X\isasymsubseteq{}D --> h(W)\isasymsubseteq{}h(X))
1.157
1.158 \tdx{lfp_def}: lfp(D,h) == Inter({\ttlbrace}X \isasymin Pow(D). h(X) \isasymsubseteq X{\ttrbrace})
1.159 \tdx{gfp_def}: gfp(D,h) == Union({\ttlbrace}X \isasymin Pow(D). X \isasymsubseteq h(X){\ttrbrace})
1.160
1.161
1.162 -\tdx{lfp_lowerbound} [| h(A) \isasymsubseteq A; A \isasymsubseteq D |] ==> lfp(D,h) \isasymsubseteq A
1.163 +\tdx{lfp_lowerbound}: [| h(A) \isasymsubseteq A; A \isasymsubseteq D |] ==> lfp(D,h) \isasymsubseteq A
1.164
1.165 \tdx{lfp_subset}: lfp(D,h) \isasymsubseteq D
1.166
1.167 @@ -1133,7 +1134,7 @@
1.168 !!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X)
1.169 |] ==> lfp(D,h) \isasymsubseteq lfp(E,i)
1.170
1.171 -\tdx{gfp_upperbound} [| A \isasymsubseteq h(A); A \isasymsubseteq D |] ==> A \isasymsubseteq gfp(D,h)
1.172 +\tdx{gfp_upperbound}: [| A \isasymsubseteq h(A); A \isasymsubseteq D |] ==> A \isasymsubseteq gfp(D,h)
1.173
1.174 \tdx{gfp_subset}: gfp(D,h) \isasymsubseteq D
1.175
1.176 @@ -1191,7 +1192,7 @@
1.177 \tdx{Fin_induct}
1.178 [| b \isasymin Fin(A);
1.179 P(0);
1.180 - !!x y. [| x \isasymin A; y \isasymin Fin(A); x \isasymnotin y; P(y) |] ==> P(cons(x,y))
1.181 + !!x y. [| x\isasymin{}A; y\isasymin{}Fin(A); x\isasymnotin{}y; P(y) |] ==> P(cons(x,y))
1.182 |] ==> P(b)
1.183
1.184 \tdx{Fin_mono}: A \isasymsubseteq B ==> Fin(A) \isasymsubseteq Fin(B)
1.185 @@ -1216,8 +1217,8 @@
1.186
1.187 \underscoreon %%because @ is used here
1.188 \begin{alltt*}\isastyleminor
1.189 -\tdx{NilI}: Nil \isasymin list(A)
1.190 -\tdx{ConsI}: [| a \isasymin A; l \isasymin list(A) |] ==> Cons(a,l) \isasymin list(A)
1.191 +\tdx{NilI}: Nil \isasymin list(A)
1.192 +\tdx{ConsI}: [| a \isasymin A; l \isasymin list(A) |] ==> Cons(a,l) \isasymin list(A)
1.193
1.194 \tdx{List.induct}
1.195 [| l \isasymin list(A);
1.196 @@ -1230,11 +1231,11 @@
1.197
1.198 \tdx{list_mono}: A \isasymsubseteq B ==> list(A) \isasymsubseteq list(B)
1.199
1.200 -\tdx{map_ident}: l \isasymin list(A) ==> map(\%u. u, l) = l
1.201 -\tdx{map_compose}: l \isasymin list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l)
1.202 -\tdx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)
1.203 +\tdx{map_ident}: l\isasymin{}list(A) ==> map(\%u. u, l) = l
1.204 +\tdx{map_compose}: l\isasymin{}list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l)
1.205 +\tdx{map_app_distrib}: xs\isasymin{}list(A) ==> map(h, xs@ys) = map(h,xs)@map(h,ys)
1.206 \tdx{map_type}
1.207 - [| l \isasymin list(A); !!x. x \isasymin A ==> h(x) \isasymin B |] ==> map(h,l) \isasymin list(B)
1.208 + [| l\isasymin{}list(A); !!x. x\isasymin{}A ==> h(x)\isasymin{}B |] ==> map(h,l)\isasymin{}list(B)
1.209 \tdx{map_flat}
1.210 ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))
1.211 \end{alltt*}
1.212 @@ -1265,40 +1266,39 @@
1.213 \tdx{comp_def}: r O s == {\ttlbrace}xz \isasymin domain(s)*range(r) .
1.214 {\isasymexists}x y z. xz=<x,z> & <x,y> \isasymin s & <y,z> \isasymin r{\ttrbrace}
1.215 \tdx{id_def}: id(A) == (lam x \isasymin A. x)
1.216 -\tdx{inj_def}: inj(A,B) == {\ttlbrace} f \isasymin A->B. {\isasymforall}w \isasymin A. {\isasymforall}x \isasymin A. f`w=f`x --> w=x {\ttrbrace}
1.217 -\tdx{surj_def}: surj(A,B) == {\ttlbrace} f \isasymin A->B . {\isasymforall}y \isasymin B. {\isasymexists}x \isasymin A. f`x=y {\ttrbrace}
1.218 -\tdx{bij_def}: bij(A,B) == inj(A,B) Int surj(A,B)
1.219 -
1.220 -
1.221 -\tdx{left_inverse}: [| f \isasymin inj(A,B); a \isasymin A |] ==> converse(f)`(f`a) = a
1.222 -\tdx{right_inverse}: [| f \isasymin inj(A,B); b \isasymin range(f) |] ==>
1.223 +\tdx{inj_def}: inj(A,B) == {\ttlbrace} f\isasymin{}A->B. {\isasymforall}w\isasymin{}A. {\isasymforall}x\isasymin{}A. f`w=f`x --> w=x {\ttrbrace}
1.224 +\tdx{surj_def}: surj(A,B) == {\ttlbrace} f\isasymin{}A->B . {\isasymforall}y\isasymin{}B. {\isasymexists}x\isasymin{}A. f`x=y {\ttrbrace}
1.225 +\tdx{bij_def}: bij(A,B) == inj(A,B) \isasyminter surj(A,B)
1.226 +
1.227 +
1.228 +\tdx{left_inverse}: [| f\isasymin{}inj(A,B); a\isasymin{}A |] ==> converse(f)`(f`a) = a
1.229 +\tdx{right_inverse}: [| f\isasymin{}inj(A,B); b\isasymin{}range(f) |] ==>
1.230 f`(converse(f)`b) = b
1.231
1.232 -\tdx{inj_converse_inj} f \isasymin inj(A,B) ==> converse(f) \isasymin inj(range(f), A)
1.233 -\tdx{bij_converse_bij} f \isasymin bij(A,B) ==> converse(f) \isasymin bij(B,A)
1.234 -
1.235 -\tdx{comp_type}: [| s \isasymsubseteq A*B; r \isasymsubseteq B*C |] ==> (r O s) \isasymsubseteq A*C
1.236 -\tdx{comp_assoc}: (r O s) O t = r O (s O t)
1.237 -
1.238 -\tdx{left_comp_id}: r \isasymsubseteq A*B ==> id(B) O r = r
1.239 -\tdx{right_comp_id}: r \isasymsubseteq A*B ==> r O id(A) = r
1.240 -
1.241 -\tdx{comp_func}: [| g \isasymin A->B; f \isasymin B->C |] ==> (f O g)
1.242 -\isasymin A ->C
1.243 -\tdx{comp_func_apply}: [| g \isasymin A->B; f \isasymin B->C; a \isasymin A |] ==> (f O g)`a = f`(g`a)
1.244 -
1.245 -\tdx{comp_inj}: [| g \isasymin inj(A,B); f \isasymin inj(B,C) |] ==> (f O g):inj(A,C)
1.246 -\tdx{comp_surj}: [| g \isasymin surj(A,B); f \isasymin surj(B,C) |] ==> (f O g):surj(A,C)
1.247 -\tdx{comp_bij}: [| g \isasymin bij(A,B); f \isasymin bij(B,C) |] ==> (f O g):bij(A,C)
1.248 -
1.249 -\tdx{left_comp_inverse}: f \isasymin inj(A,B) ==> converse(f) O f = id(A)
1.250 -\tdx{right_comp_inverse}: f \isasymin surj(A,B) ==> f O converse(f) = id(B)
1.251 +\tdx{inj_converse_inj}: f\isasymin{}inj(A,B) ==> converse(f) \isasymin inj(range(f),A)
1.252 +\tdx{bij_converse_bij}: f\isasymin{}bij(A,B) ==> converse(f) \isasymin bij(B,A)
1.253 +
1.254 +\tdx{comp_type}: [| s \isasymsubseteq A*B; r \isasymsubseteq B*C |] ==> (r O s) \isasymsubseteq A*C
1.255 +\tdx{comp_assoc}: (r O s) O t = r O (s O t)
1.256 +
1.257 +\tdx{left_comp_id}: r \isasymsubseteq A*B ==> id(B) O r = r
1.258 +\tdx{right_comp_id}: r \isasymsubseteq A*B ==> r O id(A) = r
1.259 +
1.260 +\tdx{comp_func}: [| g\isasymin{}A->B; f\isasymin{}B->C |] ==> (f O g) \isasymin A->C
1.261 +\tdx{comp_func_apply}: [| g\isasymin{}A->B; f\isasymin{}B->C; a\isasymin{}A |] ==> (f O g)`a = f`(g`a)
1.262 +
1.263 +\tdx{comp_inj}: [| g\isasymin{}inj(A,B); f\isasymin{}inj(B,C) |] ==> (f O g)\isasymin{}inj(A,C)
1.264 +\tdx{comp_surj}: [| g\isasymin{}surj(A,B); f\isasymin{}surj(B,C) |] ==> (f O g)\isasymin{}surj(A,C)
1.265 +\tdx{comp_bij}: [| g\isasymin{}bij(A,B); f\isasymin{}bij(B,C) |] ==> (f O g)\isasymin{}bij(A,C)
1.266 +
1.267 +\tdx{left_comp_inverse}: f\isasymin{}inj(A,B) ==> converse(f) O f = id(A)
1.268 +\tdx{right_comp_inverse}: f\isasymin{}surj(A,B) ==> f O converse(f) = id(B)
1.269
1.270 \tdx{bij_disjoint_Un}:
1.271 - [| f \isasymin bij(A,B); g \isasymin bij(C,D); A Int C = 0; B Int D = 0 |] ==>
1.272 - (f \isasymunion g) \isasymin bij(A \isasymunion C, B \isasymunion D)
1.273 -
1.274 -\tdx{restrict_bij}: [| f \isasymin inj(A,B); C \isasymsubseteq A |] ==> restrict(f,C) \isasymin bij(C, f``C)
1.275 + [| f\isasymin{}bij(A,B); g\isasymin{}bij(C,D); A \isasyminter C = 0; B \isasyminter D = 0 |] ==>
1.276 + (f \isasymunion g)\isasymin{}bij(A \isasymunion C, B \isasymunion D)
1.277 +
1.278 +\tdx{restrict_bij}: [| f\isasymin{}inj(A,B); C\isasymsubseteq{}A |] ==> restrict(f,C)\isasymin{}bij(C, f``C)
1.279 \end{alltt*}
1.280 \caption{Permutations} \label{zf-perm}
1.281 \end{figure}
1.282 @@ -1371,7 +1371,8 @@
1.283 essentially type-checking. Such proofs are built by applying rules such as
1.284 these:
1.285 \begin{ttbox}\isastyleminor
1.286 -[| ?P ==> ?a \isasymin ?A; ~?P ==> ?b \isasymin ?A |] ==> (if ?P then ?a else ?b) \isasymin ?A
1.287 +[| ?P ==> ?a \isasymin ?A; ~?P ==> ?b \isasymin ?A |]
1.288 +==> (if ?P then ?a else ?b) \isasymin ?A
1.289
1.290 [| ?m \isasymin nat; ?n \isasymin nat |] ==> ?m #+ ?n \isasymin nat
1.291
1.292 @@ -1394,7 +1395,7 @@
1.293 break down all subgoals using type-checking rules. You can add new
1.294 type-checking rules temporarily like this:
1.295 \begin{isabelle}
1.296 -\isacommand{apply}\ (typecheck add: inj_is_fun)
1.297 +\isacommand{apply}\ (typecheck add:\ inj_is_fun)
1.298 \end{isabelle}
1.299
1.300
1.301 @@ -1460,33 +1461,33 @@
1.302 \tt \#- & $[i,i]\To i$ & Left 65 & subtraction
1.303 \end{constants}
1.304
1.305 -\begin{ttbox}\isastyleminor
1.306 +\begin{alltt*}\isastyleminor
1.307 \tdx{nat_def}: nat == lfp(lam r \isasymin Pow(Inf). {\ttlbrace}0{\ttrbrace} \isasymunion {\ttlbrace}succ(x). x \isasymin r{\ttrbrace}
1.308
1.309 -\tdx{nat_case_def}: nat_case(a,b,k) ==
1.310 +\tdx{nat_case_def}: nat_case(a,b,k) ==
1.311 THE y. k=0 & y=a | ({\isasymexists}x. k=succ(x) & y=b(x))
1.312
1.313 -\tdx{nat_0I}: 0 \isasymin nat
1.314 -\tdx{nat_succI}: n \isasymin nat ==> succ(n) \isasymin nat
1.315 -
1.316 -\tdx{nat_induct}:
1.317 +\tdx{nat_0I}: 0 \isasymin nat
1.318 +\tdx{nat_succI}: n \isasymin nat ==> succ(n) \isasymin nat
1.319 +
1.320 +\tdx{nat_induct}:
1.321 [| n \isasymin nat; P(0); !!x. [| x \isasymin nat; P(x) |] ==> P(succ(x))
1.322 |] ==> P(n)
1.323
1.324 -\tdx{nat_case_0}: nat_case(a,b,0) = a
1.325 -\tdx{nat_case_succ}: nat_case(a,b,succ(m)) = b(m)
1.326 -
1.327 -\tdx{add_0_natify}: 0 #+ n = natify(n)
1.328 -\tdx{add_succ}: succ(m) #+ n = succ(m #+ n)
1.329 -
1.330 -\tdx{mult_type}: m #* n \isasymin nat
1.331 -\tdx{mult_0}: 0 #* n = 0
1.332 -\tdx{mult_succ}: succ(m) #* n = n #+ (m #* n)
1.333 -\tdx{mult_commute}: m #* n = n #* m
1.334 -\tdx{add_mult_dist}: (m #+ n) #* k = (m #* k) #+ (n #* k)
1.335 -\tdx{mult_assoc}: (m #* n) #* k = m #* (n #* k)
1.336 -\tdx{mod_div_equality} m \isasymin nat ==> (m div n)#*n #+ m mod n = m
1.337 -\end{ttbox}
1.338 +\tdx{nat_case_0}: nat_case(a,b,0) = a
1.339 +\tdx{nat_case_succ}: nat_case(a,b,succ(m)) = b(m)
1.340 +
1.341 +\tdx{add_0_natify}: 0 #+ n = natify(n)
1.342 +\tdx{add_succ}: succ(m) #+ n = succ(m #+ n)
1.343 +
1.344 +\tdx{mult_type}: m #* n \isasymin nat
1.345 +\tdx{mult_0}: 0 #* n = 0
1.346 +\tdx{mult_succ}: succ(m) #* n = n #+ (m #* n)
1.347 +\tdx{mult_commute}: m #* n = n #* m
1.348 +\tdx{add_mult_dist}: (m #+ n) #* k = (m #* k) #+ (n #* k)
1.349 +\tdx{mult_assoc}: (m #* n) #* k = m #* (n #* k)
1.350 +\tdx{mod_div_equality}: m \isasymin nat ==> (m div n)#*n #+ m mod n = m
1.351 +\end{alltt*}
1.352 \caption{The natural numbers} \label{zf-nat}
1.353 \end{figure}
1.354
1.355 @@ -1543,7 +1544,7 @@
1.356 \tt \$<= & $[i,i]\To o$ & Left 50 & $\le$ on integers
1.357 \end{constants}
1.358
1.359 -\begin{ttbox}\isastyleminor
1.360 +\begin{alltt*}\isastyleminor
1.361 \tdx{zadd_0_intify}: 0 $+ n = intify(n)
1.362
1.363 \tdx{zmult_type}: m $* n \isasymin int
1.364 @@ -1551,7 +1552,7 @@
1.365 \tdx{zmult_commute}: m $* n = n $* m
1.366 \tdx{zadd_zmult_dist}: (m $+ n) $* k = (m $* k) $+ (n $* k)
1.367 \tdx{zmult_assoc}: (m $* n) $* k = m $* (n $* k)
1.368 -\end{ttbox}
1.369 +\end{alltt*}
1.370 \caption{The integers} \label{zf-int}
1.371 \end{figure}
1.372
1.373 @@ -1637,34 +1638,34 @@
1.374
1.375 A simple example of a datatype is \isa{list}, which is built-in, and is
1.376 defined by
1.377 -\begin{ttbox}\isastyleminor
1.378 +\begin{alltt*}\isastyleminor
1.379 consts list :: "i=>i"
1.380 datatype "list(A)" = Nil | Cons ("a \isasymin A", "l \isasymin list(A)")
1.381 -\end{ttbox}
1.382 +\end{alltt*}
1.383 Note that the datatype operator must be declared as a constant first.
1.384 However, the package declares the constructors. Here, \isa{Nil} gets type
1.385 $i$ and \isa{Cons} gets type $[i,i]\To i$.
1.386
1.387 Trees and forests can be modelled by the mutually recursive datatype
1.388 definition
1.389 -\begin{ttbox}\isastyleminor
1.390 +\begin{alltt*}\isastyleminor
1.391 consts
1.392 tree :: "i=>i"
1.393 forest :: "i=>i"
1.394 tree_forest :: "i=>i"
1.395 datatype "tree(A)" = Tcons ("a{\isasymin}A", "f{\isasymin}forest(A)")
1.396 and "forest(A)" = Fnil | Fcons ("t{\isasymin}tree(A)", "f{\isasymin}forest(A)")
1.397 -\end{ttbox}
1.398 +\end{alltt*}
1.399 Here $\isa{tree}(A)$ is the set of trees over $A$, $\isa{forest}(A)$ is
1.400 the set of forests over $A$, and $\isa{tree_forest}(A)$ is the union of
1.401 the previous two sets. All three operators must be declared first.
1.402
1.403 The datatype \isa{term}, which is defined by
1.404 -\begin{ttbox}\isastyleminor
1.405 +\begin{alltt*}\isastyleminor
1.406 consts term :: "i=>i"
1.407 datatype "term(A)" = Apply ("a \isasymin A", "l \isasymin list(term(A))")
1.408 monos list_mono
1.409 -\end{ttbox}
1.410 +\end{alltt*}
1.411 is an example of nested recursion. (The theorem \isa{list_mono} is proved
1.412 in theory \isa{List}, and the \isa{term} example is developed in
1.413 theory
1.414 @@ -1698,17 +1699,17 @@
1.415 \isa{TF}. The rule \isa{tree_forest.induct} performs induction over a
1.416 single predicate~\isa{P}, which is presumed to be defined for both trees
1.417 and forests:
1.418 -\begin{ttbox}\isastyleminor
1.419 +\begin{alltt*}\isastyleminor
1.420 [| x \isasymin tree_forest(A);
1.421 !!a f. [| a \isasymin A; f \isasymin forest(A); P(f) |] ==> P(Tcons(a, f));
1.422 P(Fnil);
1.423 !!f t. [| t \isasymin tree(A); P(t); f \isasymin forest(A); P(f) |]
1.424 ==> P(Fcons(t, f))
1.425 |] ==> P(x)
1.426 -\end{ttbox}
1.427 +\end{alltt*}
1.428 The rule \isa{tree_forest.mutual_induct} performs induction over two
1.429 distinct predicates, \isa{P_tree} and \isa{P_forest}.
1.430 -\begin{ttbox}\isastyleminor
1.431 +\begin{alltt*}\isastyleminor
1.432 [| !!a f.
1.433 [| a{\isasymin}A; f{\isasymin}forest(A); P_forest(f) |] ==> P_tree(Tcons(a,f));
1.434 P_forest(Fnil);
1.435 @@ -1716,24 +1717,24 @@
1.436 ==> P_forest(Fcons(t, f))
1.437 |] ==> ({\isasymforall}za. za \isasymin tree(A) --> P_tree(za)) &
1.438 ({\isasymforall}za. za \isasymin forest(A) --> P_forest(za))
1.439 -\end{ttbox}
1.440 +\end{alltt*}
1.441
1.442 For datatypes with nested recursion, such as the \isa{term} example from
1.443 above, things are a bit more complicated. The rule \isa{term.induct}
1.444 refers to the monotonic operator, \isa{list}:
1.445 -\begin{ttbox}\isastyleminor
1.446 +\begin{alltt*}\isastyleminor
1.447 [| x \isasymin term(A);
1.448 - !!a l. [| a \isasymin A; l \isasymin list(Collect(term(A), P)) |] ==> P(Apply(a, l))
1.449 + !!a l. [| a\isasymin{}A; l\isasymin{}list(Collect(term(A), P)) |] ==> P(Apply(a,l))
1.450 |] ==> P(x)
1.451 -\end{ttbox}
1.452 +\end{alltt*}
1.453 The theory \isa{Induct/Term.thy} derives two higher-level induction rules,
1.454 one of which is particularly useful for proving equations:
1.455 -\begin{ttbox}\isastyleminor
1.456 +\begin{alltt*}\isastyleminor
1.457 [| t \isasymin term(A);
1.458 !!x zs. [| x \isasymin A; zs \isasymin list(term(A)); map(f, zs) = map(g, zs) |]
1.459 ==> f(Apply(x, zs)) = g(Apply(x, zs))
1.460 |] ==> f(t) = g(t)
1.461 -\end{ttbox}
1.462 +\end{alltt*}
1.463 How this can be generalized to other nested datatypes is a matter for future
1.464 research.
1.465
1.466 @@ -1863,10 +1864,10 @@
1.467
1.468 Let us define the set $\isa{bt}(A)$ of binary trees over~$A$. The theory
1.469 must contain these lines:
1.470 -\begin{ttbox}\isastyleminor
1.471 +\begin{alltt*}\isastyleminor
1.472 consts bt :: "i=>i"
1.473 datatype "bt(A)" = Lf | Br ("a\isasymin{}A", "t1\isasymin{}bt(A)", "t2\isasymin{}bt(A)")
1.474 -\end{ttbox}
1.475 +\end{alltt*}
1.476 After loading the theory, we can prove some theorem.
1.477 We begin by declaring the constructor's typechecking rules
1.478 as simplification rules:
1.479 @@ -1880,8 +1881,7 @@
1.480 the \isa{rule\_format} attribute will remove the quantifiers
1.481 before the theorem is stored.
1.482 \begin{isabelle}
1.483 -\isacommand{lemma}\ Br\_neq\_left\ [rule\_format]:\ "l\ \isasymin \
1.484 -bt(A)\ ==>\ \isasymforall x\ r.\ Br(x,l,r)\isasymnoteq{}l"\isanewline
1.485 +\isacommand{lemma}\ Br\_neq\_left\ [rule\_format]:\ "l\isasymin bt(A)\ ==>\ \isasymforall x\ r.\ Br(x,l,r)\isasymnoteq{}l"\isanewline
1.486 \ 1.\ l\ \isasymin \ bt(A)\ \isasymLongrightarrow \ \isasymforall x\ r.\ Br(x,\ l,\ r)\ \isasymnoteq \ l%
1.487 \end{isabelle}
1.488 This can be proved by the structural induction tactic:
1.489 @@ -1944,12 +1944,12 @@
1.490
1.491 Mixfix syntax is sometimes convenient. The theory \isa{Induct/PropLog} makes a
1.492 deep embedding of propositional logic:
1.493 -\begin{ttbox}\isastyleminor
1.494 +\begin{alltt*}\isastyleminor
1.495 consts prop :: i
1.496 datatype "prop" = Fls
1.497 | Var ("n \isasymin nat") ("#_" [100] 100)
1.498 | "=>" ("p \isasymin prop", "q \isasymin prop") (infixr 90)
1.499 -\end{ttbox}
1.500 +\end{alltt*}
1.501 The second constructor has a special $\#n$ syntax, while the third constructor
1.502 is an infixed arrow.
1.503
1.504 @@ -1957,7 +1957,7 @@
1.505 \subsubsection{A giant enumeration type}
1.506
1.507 This example shows a datatype that consists of 60 constructors:
1.508 -\begin{ttbox}\isastyleminor
1.509 +\begin{alltt*}\isastyleminor
1.510 consts enum :: i
1.511 datatype
1.512 "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
1.513 @@ -1967,7 +1967,7 @@
1.514 | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49
1.515 | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59
1.516 end
1.517 -\end{ttbox}
1.518 +\end{alltt*}
1.519 The datatype package scales well. Even though all properties are proved
1.520 rather than assumed, full processing of this definition takes around two seconds
1.521 (on a 1.8GHz machine). The constructors have a balanced representation,
1.522 @@ -2220,11 +2220,11 @@
1.523 Here is the output that results (with the flag set) when the
1.524 \isa{type_intros} and \isa{type_elims} are omitted from the inductive
1.525 definition above:
1.526 -\begin{ttbox}\isastyleminor
1.527 +\begin{alltt*}\isastyleminor
1.528 Inductive definition Finite.Fin
1.529 Fin(A) ==
1.530 lfp(Pow(A),
1.531 - \%X. {z \isasymin Pow(A) . z = 0 | ({\isasymexists}a b. z = cons(a, b) & a \isasymin A & b \isasymin X)})
1.532 + \%X. {z\isasymin{}Pow(A) . z = 0 | ({\isasymexists}a b. z = cons(a,b) & a\isasymin{}A & b\isasymin{}X)})
1.533 Proving monotonicity...
1.534 \ttbreak
1.535 Proving the introduction rules...
1.536 @@ -2236,11 +2236,11 @@
1.537 0 \isasymin Fin(A)
1.538 1. 0 \isasymin Pow(A)
1.539 *** prove_goal: tactic failed
1.540 -\end{ttbox}
1.541 +\end{alltt*}
1.542 We see the need to supply theorems to let the package prove
1.543 $\emptyset\in\isa{Pow}(A)$. Restoring the \isa{type_intros} but not the
1.544 \isa{type_elims}, we again get an error message:
1.545 -\begin{ttbox}\isastyleminor
1.546 +\begin{alltt*}\isastyleminor
1.547 The type-checking subgoal:
1.548 0 \isasymin Fin(A)
1.549 1. 0 \isasymin Pow(A)
1.550 @@ -2257,7 +2257,7 @@
1.551 cons(a, b) \isasymin Fin(A)
1.552 1. [| a \isasymin A; b \isasymin Pow(A) |] ==> cons(a, b) \isasymin Pow(A)
1.553 *** prove_goal: tactic failed
1.554 -\end{ttbox}
1.555 +\end{alltt*}
1.556 The first rule has been type-checked, but the second one has failed. The
1.557 simplest solution to such problems is to prove the failed subgoal separately
1.558 and to supply it under \isa{type_intros}. The solution actually used is
1.559 @@ -2341,12 +2341,12 @@
1.560 elsewhere~\cite{paulson-generic}. The theory first defines the
1.561 datatype
1.562 \isa{comb} of combinators:
1.563 -\begin{ttbox}\isastyleminor
1.564 +\begin{alltt*}\isastyleminor
1.565 consts comb :: i
1.566 datatype "comb" = K
1.567 | S
1.568 | "#" ("p \isasymin comb", "q \isasymin comb") (infixl 90)
1.569 -\end{ttbox}
1.570 +\end{alltt*}
1.571 The theory goes on to define contraction and parallel contraction
1.572 inductively. Then the theory \isa{Induct/Comb.thy} defines special
1.573 cases of contraction, such as this one:
1.574 @@ -2396,7 +2396,7 @@
1.575 not yet been written up anywhere. Here is a summary:
1.576 \begin{itemize}
1.577 \item Theory \isa{Rel} defines the basic properties of relations, such as
1.578 - (ir)reflexivity, (a)symmetry, and transitivity.
1.579 + reflexivity, symmetry and transitivity.
1.580
1.581 \item Theory \isa{EquivClass} develops a theory of equivalence
1.582 classes, not using the Axiom of Choice.