1.1 --- a/doc-src/ZF/FOL.tex Wed Aug 20 11:12:48 2003 +0200
1.2 +++ b/doc-src/ZF/FOL.tex Wed Aug 20 13:05:22 2003 +0200
1.3 @@ -259,8 +259,9 @@
1.4 IntPr.fast_tac : int -> tactic
1.5 IntPr.best_tac : int -> tactic
1.6 \end{ttbox}
1.7 -Most of these belong to the structure \ML{} \texttt{IntPr} and resemble the
1.8 -tactics of Isabelle's classical reasoner. Note that you can use the
1.9 +Most of these belong to the structure \ML{} structure \texttt{IntPr} and resemble the
1.10 +tactics of Isabelle's classical reasoner. There are no corresponding
1.11 +Isar methods, but you can use the
1.12 \isa{tactic} method to call \ML{} tactics in an Isar script:
1.13 \begin{isabelle}
1.14 \isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*})
1.15 @@ -350,12 +351,14 @@
1.16
1.17
1.18 \section{An intuitionistic example}
1.19 -Here is a session similar to one in {\em Logic and Computation}
1.20 -\cite[pages~222--3]{paulson87}. Isabelle treats quantifiers differently
1.21 -from {\sc lcf}-based theorem provers such as {\sc hol}.
1.22 +Here is a session similar to one in the book {\em Logic and Computation}
1.23 +\cite[pages~222--3]{paulson87}. It illustrates the treatment of
1.24 +quantifier reasoning, which is different in Isabelle than it is in
1.25 +{\sc lcf}-based theorem provers such as {\sc hol}.
1.26
1.27 -The theory header must specify that we are working in intuitionistic
1.28 -logic:
1.29 +The theory header specifies that we are working in intuitionistic
1.30 +logic by designating \isa{IFOL} rather than \isa{FOL} as the parent
1.31 +theory:
1.32 \begin{isabelle}
1.33 \isacommand{theory}\ IFOL\_examples\ =\ IFOL:
1.34 \end{isabelle}
1.35 @@ -524,7 +527,7 @@
1.36 $\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as
1.37 follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
1.38 $\all{x}P(x)$ is true. Either way the theorem holds. First, we must
1.39 -work in a theory based on classical logic:
1.40 +work in a theory based on classical logic, the theory \isa{FOL}:
1.41 \begin{isabelle}
1.42 \isacommand{theory}\ FOL\_examples\ =\ FOL:
1.43 \end{isabelle}
2.1 --- a/doc-src/ZF/ZF.tex Wed Aug 20 11:12:48 2003 +0200
2.2 +++ b/doc-src/ZF/ZF.tex Wed Aug 20 13:05:22 2003 +0200
2.3 @@ -231,7 +231,7 @@
2.4 & | & term " -`` " term \\
2.5 & | & term " ` " term \\
2.6 & | & term " * " term \\
2.7 - & | & term " Int " term \\
2.8 + & | & term " \isasyminter " term \\
2.9 & | & term " \isasymunion " term \\
2.10 & | & term " - " term \\
2.11 & | & term " -> " term \\
2.12 @@ -373,7 +373,7 @@
2.13
2.14 \tdx{Inter_def}: Inter(A) == {\ttlbrace}x \isasymin Union(A) . {\isasymforall}y \isasymin A. x \isasymin y{\ttrbrace}
2.15 \tdx{Un_def}: A \isasymunion B == Union(Upair(A,B))
2.16 -\tdx{Int_def}: A Int B == Inter(Upair(A,B))
2.17 +\tdx{Int_def}: A \isasyminter B == Inter(Upair(A,B))
2.18 \tdx{Diff_def}: A - B == {\ttlbrace}x \isasymin A . x \isasymnotin B{\ttrbrace}
2.19 \subcaption{Union, intersection, difference}
2.20 \end{alltt*}
2.21 @@ -434,7 +434,8 @@
2.22 same set, if $P(x,y)$ is single-valued. The nice syntax for replacement
2.23 expands to \isa{Replace}.
2.24
2.25 -Other consequences of replacement include functional replacement
2.26 +Other consequences of replacement include replacement for
2.27 +meta-level functions
2.28 (\cdx{RepFun}) and definite descriptions (\cdx{The}).
2.29 Axioms for separation (\cdx{Collect}) and unordered pairs
2.30 (\cdx{Upair}) are traditionally assumed, but they actually follow
2.31 @@ -617,10 +618,10 @@
2.32 \tdx{UnCI}: (c \isasymnotin B ==> c\isasymin{}A) ==> c\isasymin{}A \isasymunion B
2.33 \tdx{UnE}: [| c\isasymin{}A \isasymunion B; c\isasymin{}A ==> P; c\isasymin{}B ==> P |] ==> P
2.34
2.35 -\tdx{IntI}: [| c\isasymin{}A; c\isasymin{}B |] ==> c\isasymin{}A Int B
2.36 -\tdx{IntD1}: c\isasymin{}A Int B ==> c\isasymin{}A
2.37 -\tdx{IntD2}: c\isasymin{}A Int B ==> c\isasymin{}B
2.38 -\tdx{IntE}: [| c\isasymin{}A Int B; [| c\isasymin{}A; c\isasymin{}B |] ==> P |] ==> P
2.39 +\tdx{IntI}: [| c\isasymin{}A; c\isasymin{}B |] ==> c\isasymin{}A \isasyminter B
2.40 +\tdx{IntD1}: c\isasymin{}A \isasyminter B ==> c\isasymin{}A
2.41 +\tdx{IntD2}: c\isasymin{}A \isasyminter B ==> c\isasymin{}B
2.42 +\tdx{IntE}: [| c\isasymin{}A \isasyminter B; [| c\isasymin{}A; c\isasymin{}B |] ==> P |] ==> P
2.43
2.44 \tdx{DiffI}: [| c\isasymin{}A; c \isasymnotin B |] ==> c\isasymin{}A - B
2.45 \tdx{DiffD1}: c\isasymin{}A - B ==> c\isasymin{}A
2.46 @@ -715,12 +716,12 @@
2.47 \tdx{Un_upper2}: B \isasymsubseteq A \isasymunion B
2.48 \tdx{Un_least}: [| A \isasymsubseteq C; B \isasymsubseteq C |] ==> A \isasymunion B \isasymsubseteq C
2.49
2.50 -\tdx{Int_lower1}: A Int B \isasymsubseteq A
2.51 -\tdx{Int_lower2}: A Int B \isasymsubseteq B
2.52 -\tdx{Int_greatest}: [| C \isasymsubseteq A; C \isasymsubseteq B |] ==> C \isasymsubseteq A Int B
2.53 +\tdx{Int_lower1}: A \isasyminter B \isasymsubseteq A
2.54 +\tdx{Int_lower2}: A \isasyminter B \isasymsubseteq B
2.55 +\tdx{Int_greatest}: [| C \isasymsubseteq A; C \isasymsubseteq B |] ==> C \isasymsubseteq A \isasyminter B
2.56
2.57 \tdx{Diff_subset}: A-B \isasymsubseteq A
2.58 -\tdx{Diff_contains}: [| C \isasymsubseteq A; C Int B = 0 |] ==> C \isasymsubseteq A-B
2.59 +\tdx{Diff_contains}: [| C \isasymsubseteq A; C \isasyminter B = 0 |] ==> C \isasymsubseteq A-B
2.60
2.61 \tdx{Collect_subset}: Collect(A,P) \isasymsubseteq A
2.62 \end{alltt*}
2.63 @@ -825,9 +826,9 @@
2.64 \tdx{fieldCI}: (<c,a> \isasymnotin r ==> <a,b>\isasymin{}r) ==> a\isasymin{}field(r)
2.65
2.66 \tdx{fieldE}: [| a\isasymin{}field(r);
2.67 - !!x. <a,x>\isasymin{}r ==> P;
2.68 - !!x. <x,a>\isasymin{}r ==> P
2.69 - |] ==> P
2.70 + !!x. <a,x>\isasymin{}r ==> P;
2.71 + !!x. <x,a>\isasymin{}r ==> P
2.72 + |] ==> P
2.73
2.74 \tdx{field_subset}: field(A*A) \isasymsubseteq A
2.75 \end{alltt*}
2.76 @@ -867,7 +868,7 @@
2.77 \begin{alltt*}\isastyleminor
2.78 \tdx{fun_is_rel}: f\isasymin{}Pi(A,B) ==> f \isasymsubseteq Sigma(A,B)
2.79
2.80 -\tdx{apply_equality}: [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> f`a = b
2.81 +\tdx{apply_equality}: [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> f`a = b
2.82 \tdx{apply_equality2}: [| <a,b>\isasymin{}f; <a,c>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> b=c
2.83
2.84 \tdx{apply_type}: [| f\isasymin{}Pi(A,B); a\isasymin{}A |] ==> f`a\isasymin{}B(a)
2.85 @@ -912,7 +913,7 @@
2.86 \tdx{fun_empty}: 0\isasymin{}0->0
2.87 \tdx{fun_single}: {\ttlbrace}<a,b>{\ttrbrace}\isasymin{}{\ttlbrace}a{\ttrbrace} -> {\ttlbrace}b{\ttrbrace}
2.88
2.89 -\tdx{fun_disjoint_Un}: [| f\isasymin{}A->B; g\isasymin{}C->D; A Int C = 0 |] ==>
2.90 +\tdx{fun_disjoint_Un}: [| f\isasymin{}A->B; g\isasymin{}C->D; A \isasyminter C = 0 |] ==>
2.91 (f \isasymunion g)\isasymin{}(A \isasymunion C) -> (B \isasymunion D)
2.92
2.93 \tdx{fun_disjoint_apply1}: [| a\isasymin{}A; f\isasymin{}A->B; g\isasymin{}C->D; A\isasyminter{}C = 0 |] ==>
2.94 @@ -955,28 +956,28 @@
2.95
2.96 \begin{figure}
2.97 \begin{alltt*}\isastyleminor
2.98 -\tdx{Int_absorb}: A Int A = A
2.99 -\tdx{Int_commute}: A Int B = B Int A
2.100 -\tdx{Int_assoc}: (A Int B) Int C = A Int (B Int C)
2.101 -\tdx{Int_Un_distrib}: (A \isasymunion B) Int C = (A Int C) \isasymunion (B Int C)
2.102 +\tdx{Int_absorb}: A \isasyminter A = A
2.103 +\tdx{Int_commute}: A \isasyminter B = B \isasyminter A
2.104 +\tdx{Int_assoc}: (A \isasyminter B) \isasyminter C = A \isasyminter (B \isasyminter C)
2.105 +\tdx{Int_Un_distrib}: (A \isasymunion B) \isasyminter C = (A \isasyminter C) \isasymunion (B \isasyminter C)
2.106
2.107 \tdx{Un_absorb}: A \isasymunion A = A
2.108 \tdx{Un_commute}: A \isasymunion B = B \isasymunion A
2.109 \tdx{Un_assoc}: (A \isasymunion B) \isasymunion C = A \isasymunion (B \isasymunion C)
2.110 -\tdx{Un_Int_distrib}: (A Int B) \isasymunion C = (A \isasymunion C) Int (B \isasymunion C)
2.111 +\tdx{Un_Int_distrib}: (A \isasyminter B) \isasymunion C = (A \isasymunion C) \isasyminter (B \isasymunion C)
2.112
2.113 \tdx{Diff_cancel}: A-A = 0
2.114 -\tdx{Diff_disjoint}: A Int (B-A) = 0
2.115 +\tdx{Diff_disjoint}: A \isasyminter (B-A) = 0
2.116 \tdx{Diff_partition}: A \isasymsubseteq B ==> A \isasymunion (B-A) = B
2.117 \tdx{double_complement}: [| A \isasymsubseteq B; B \isasymsubseteq C |] ==> (B - (C-A)) = A
2.118 -\tdx{Diff_Un}: A - (B \isasymunion C) = (A-B) Int (A-C)
2.119 -\tdx{Diff_Int}: A - (B Int C) = (A-B) \isasymunion (A-C)
2.120 +\tdx{Diff_Un}: A - (B \isasymunion C) = (A-B) \isasyminter (A-C)
2.121 +\tdx{Diff_Int}: A - (B \isasyminter C) = (A-B) \isasymunion (A-C)
2.122
2.123 \tdx{Union_Un_distrib}: Union(A \isasymunion B) = Union(A) \isasymunion Union(B)
2.124 \tdx{Inter_Un_distrib}: [| a \isasymin A; b \isasymin B |] ==>
2.125 - Inter(A \isasymunion B) = Inter(A) Int Inter(B)
2.126 -
2.127 -\tdx{Int_Union_RepFun}: A Int Union(B) = ({\isasymUnion}C \isasymin B. A Int C)
2.128 + Inter(A \isasymunion B) = Inter(A) \isasyminter Inter(B)
2.129 +
2.130 +\tdx{Int_Union_RepFun}: A \isasyminter Union(B) = ({\isasymUnion}C \isasymin B. A \isasyminter C)
2.131
2.132 \tdx{Un_Inter_RepFun}: b \isasymin B ==>
2.133 A \isasymunion Inter(B) = ({\isasymInter}C \isasymin B. A \isasymunion C)
2.134 @@ -987,11 +988,11 @@
2.135 \tdx{SUM_Un_distrib2}: (SUM x \isasymin C. A(x) \isasymunion B(x)) =
2.136 (SUM x \isasymin C. A(x)) \isasymunion (SUM x \isasymin C. B(x))
2.137
2.138 -\tdx{SUM_Int_distrib1}: (SUM x \isasymin A Int B. C(x)) =
2.139 - (SUM x \isasymin A. C(x)) Int (SUM x \isasymin B. C(x))
2.140 -
2.141 -\tdx{SUM_Int_distrib2}: (SUM x \isasymin C. A(x) Int B(x)) =
2.142 - (SUM x \isasymin C. A(x)) Int (SUM x \isasymin C. B(x))
2.143 +\tdx{SUM_Int_distrib1}: (SUM x \isasymin A \isasyminter B. C(x)) =
2.144 + (SUM x \isasymin A. C(x)) \isasyminter (SUM x \isasymin B. C(x))
2.145 +
2.146 +\tdx{SUM_Int_distrib2}: (SUM x \isasymin C. A(x) \isasyminter B(x)) =
2.147 + (SUM x \isasymin C. A(x)) \isasyminter (SUM x \isasymin C. B(x))
2.148 \end{alltt*}
2.149 \caption{Equalities} \label{zf-equalities}
2.150 \end{figure}
2.151 @@ -1109,13 +1110,13 @@
2.152 \begin{figure}
2.153 \begin{alltt*}\isastyleminor
2.154 \tdx{bnd_mono_def}: bnd_mono(D,h) ==
2.155 - h(D) \isasymsubseteq D & ({\isasymforall}W X. W \isasymsubseteq X --> X \isasymsubseteq D --> h(W) \isasymsubseteq h(X))
2.156 + h(D)\isasymsubseteq{}D & ({\isasymforall}W X. W\isasymsubseteq{}X --> X\isasymsubseteq{}D --> h(W)\isasymsubseteq{}h(X))
2.157
2.158 \tdx{lfp_def}: lfp(D,h) == Inter({\ttlbrace}X \isasymin Pow(D). h(X) \isasymsubseteq X{\ttrbrace})
2.159 \tdx{gfp_def}: gfp(D,h) == Union({\ttlbrace}X \isasymin Pow(D). X \isasymsubseteq h(X){\ttrbrace})
2.160
2.161
2.162 -\tdx{lfp_lowerbound} [| h(A) \isasymsubseteq A; A \isasymsubseteq D |] ==> lfp(D,h) \isasymsubseteq A
2.163 +\tdx{lfp_lowerbound}: [| h(A) \isasymsubseteq A; A \isasymsubseteq D |] ==> lfp(D,h) \isasymsubseteq A
2.164
2.165 \tdx{lfp_subset}: lfp(D,h) \isasymsubseteq D
2.166
2.167 @@ -1133,7 +1134,7 @@
2.168 !!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X)
2.169 |] ==> lfp(D,h) \isasymsubseteq lfp(E,i)
2.170
2.171 -\tdx{gfp_upperbound} [| A \isasymsubseteq h(A); A \isasymsubseteq D |] ==> A \isasymsubseteq gfp(D,h)
2.172 +\tdx{gfp_upperbound}: [| A \isasymsubseteq h(A); A \isasymsubseteq D |] ==> A \isasymsubseteq gfp(D,h)
2.173
2.174 \tdx{gfp_subset}: gfp(D,h) \isasymsubseteq D
2.175
2.176 @@ -1191,7 +1192,7 @@
2.177 \tdx{Fin_induct}
2.178 [| b \isasymin Fin(A);
2.179 P(0);
2.180 - !!x y. [| x \isasymin A; y \isasymin Fin(A); x \isasymnotin y; P(y) |] ==> P(cons(x,y))
2.181 + !!x y. [| x\isasymin{}A; y\isasymin{}Fin(A); x\isasymnotin{}y; P(y) |] ==> P(cons(x,y))
2.182 |] ==> P(b)
2.183
2.184 \tdx{Fin_mono}: A \isasymsubseteq B ==> Fin(A) \isasymsubseteq Fin(B)
2.185 @@ -1216,8 +1217,8 @@
2.186
2.187 \underscoreon %%because @ is used here
2.188 \begin{alltt*}\isastyleminor
2.189 -\tdx{NilI}: Nil \isasymin list(A)
2.190 -\tdx{ConsI}: [| a \isasymin A; l \isasymin list(A) |] ==> Cons(a,l) \isasymin list(A)
2.191 +\tdx{NilI}: Nil \isasymin list(A)
2.192 +\tdx{ConsI}: [| a \isasymin A; l \isasymin list(A) |] ==> Cons(a,l) \isasymin list(A)
2.193
2.194 \tdx{List.induct}
2.195 [| l \isasymin list(A);
2.196 @@ -1230,11 +1231,11 @@
2.197
2.198 \tdx{list_mono}: A \isasymsubseteq B ==> list(A) \isasymsubseteq list(B)
2.199
2.200 -\tdx{map_ident}: l \isasymin list(A) ==> map(\%u. u, l) = l
2.201 -\tdx{map_compose}: l \isasymin list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l)
2.202 -\tdx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)
2.203 +\tdx{map_ident}: l\isasymin{}list(A) ==> map(\%u. u, l) = l
2.204 +\tdx{map_compose}: l\isasymin{}list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l)
2.205 +\tdx{map_app_distrib}: xs\isasymin{}list(A) ==> map(h, xs@ys) = map(h,xs)@map(h,ys)
2.206 \tdx{map_type}
2.207 - [| l \isasymin list(A); !!x. x \isasymin A ==> h(x) \isasymin B |] ==> map(h,l) \isasymin list(B)
2.208 + [| l\isasymin{}list(A); !!x. x\isasymin{}A ==> h(x)\isasymin{}B |] ==> map(h,l)\isasymin{}list(B)
2.209 \tdx{map_flat}
2.210 ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))
2.211 \end{alltt*}
2.212 @@ -1265,40 +1266,39 @@
2.213 \tdx{comp_def}: r O s == {\ttlbrace}xz \isasymin domain(s)*range(r) .
2.214 {\isasymexists}x y z. xz=<x,z> & <x,y> \isasymin s & <y,z> \isasymin r{\ttrbrace}
2.215 \tdx{id_def}: id(A) == (lam x \isasymin A. x)
2.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}
2.217 -\tdx{surj_def}: surj(A,B) == {\ttlbrace} f \isasymin A->B . {\isasymforall}y \isasymin B. {\isasymexists}x \isasymin A. f`x=y {\ttrbrace}
2.218 -\tdx{bij_def}: bij(A,B) == inj(A,B) Int surj(A,B)
2.219 -
2.220 -
2.221 -\tdx{left_inverse}: [| f \isasymin inj(A,B); a \isasymin A |] ==> converse(f)`(f`a) = a
2.222 -\tdx{right_inverse}: [| f \isasymin inj(A,B); b \isasymin range(f) |] ==>
2.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}
2.224 +\tdx{surj_def}: surj(A,B) == {\ttlbrace} f\isasymin{}A->B . {\isasymforall}y\isasymin{}B. {\isasymexists}x\isasymin{}A. f`x=y {\ttrbrace}
2.225 +\tdx{bij_def}: bij(A,B) == inj(A,B) \isasyminter surj(A,B)
2.226 +
2.227 +
2.228 +\tdx{left_inverse}: [| f\isasymin{}inj(A,B); a\isasymin{}A |] ==> converse(f)`(f`a) = a
2.229 +\tdx{right_inverse}: [| f\isasymin{}inj(A,B); b\isasymin{}range(f) |] ==>
2.230 f`(converse(f)`b) = b
2.231
2.232 -\tdx{inj_converse_inj} f \isasymin inj(A,B) ==> converse(f) \isasymin inj(range(f), A)
2.233 -\tdx{bij_converse_bij} f \isasymin bij(A,B) ==> converse(f) \isasymin bij(B,A)
2.234 -
2.235 -\tdx{comp_type}: [| s \isasymsubseteq A*B; r \isasymsubseteq B*C |] ==> (r O s) \isasymsubseteq A*C
2.236 -\tdx{comp_assoc}: (r O s) O t = r O (s O t)
2.237 -
2.238 -\tdx{left_comp_id}: r \isasymsubseteq A*B ==> id(B) O r = r
2.239 -\tdx{right_comp_id}: r \isasymsubseteq A*B ==> r O id(A) = r
2.240 -
2.241 -\tdx{comp_func}: [| g \isasymin A->B; f \isasymin B->C |] ==> (f O g)
2.242 -\isasymin A ->C
2.243 -\tdx{comp_func_apply}: [| g \isasymin A->B; f \isasymin B->C; a \isasymin A |] ==> (f O g)`a = f`(g`a)
2.244 -
2.245 -\tdx{comp_inj}: [| g \isasymin inj(A,B); f \isasymin inj(B,C) |] ==> (f O g):inj(A,C)
2.246 -\tdx{comp_surj}: [| g \isasymin surj(A,B); f \isasymin surj(B,C) |] ==> (f O g):surj(A,C)
2.247 -\tdx{comp_bij}: [| g \isasymin bij(A,B); f \isasymin bij(B,C) |] ==> (f O g):bij(A,C)
2.248 -
2.249 -\tdx{left_comp_inverse}: f \isasymin inj(A,B) ==> converse(f) O f = id(A)
2.250 -\tdx{right_comp_inverse}: f \isasymin surj(A,B) ==> f O converse(f) = id(B)
2.251 +\tdx{inj_converse_inj}: f\isasymin{}inj(A,B) ==> converse(f) \isasymin inj(range(f),A)
2.252 +\tdx{bij_converse_bij}: f\isasymin{}bij(A,B) ==> converse(f) \isasymin bij(B,A)
2.253 +
2.254 +\tdx{comp_type}: [| s \isasymsubseteq A*B; r \isasymsubseteq B*C |] ==> (r O s) \isasymsubseteq A*C
2.255 +\tdx{comp_assoc}: (r O s) O t = r O (s O t)
2.256 +
2.257 +\tdx{left_comp_id}: r \isasymsubseteq A*B ==> id(B) O r = r
2.258 +\tdx{right_comp_id}: r \isasymsubseteq A*B ==> r O id(A) = r
2.259 +
2.260 +\tdx{comp_func}: [| g\isasymin{}A->B; f\isasymin{}B->C |] ==> (f O g) \isasymin A->C
2.261 +\tdx{comp_func_apply}: [| g\isasymin{}A->B; f\isasymin{}B->C; a\isasymin{}A |] ==> (f O g)`a = f`(g`a)
2.262 +
2.263 +\tdx{comp_inj}: [| g\isasymin{}inj(A,B); f\isasymin{}inj(B,C) |] ==> (f O g)\isasymin{}inj(A,C)
2.264 +\tdx{comp_surj}: [| g\isasymin{}surj(A,B); f\isasymin{}surj(B,C) |] ==> (f O g)\isasymin{}surj(A,C)
2.265 +\tdx{comp_bij}: [| g\isasymin{}bij(A,B); f\isasymin{}bij(B,C) |] ==> (f O g)\isasymin{}bij(A,C)
2.266 +
2.267 +\tdx{left_comp_inverse}: f\isasymin{}inj(A,B) ==> converse(f) O f = id(A)
2.268 +\tdx{right_comp_inverse}: f\isasymin{}surj(A,B) ==> f O converse(f) = id(B)
2.269
2.270 \tdx{bij_disjoint_Un}:
2.271 - [| f \isasymin bij(A,B); g \isasymin bij(C,D); A Int C = 0; B Int D = 0 |] ==>
2.272 - (f \isasymunion g) \isasymin bij(A \isasymunion C, B \isasymunion D)
2.273 -
2.274 -\tdx{restrict_bij}: [| f \isasymin inj(A,B); C \isasymsubseteq A |] ==> restrict(f,C) \isasymin bij(C, f``C)
2.275 + [| f\isasymin{}bij(A,B); g\isasymin{}bij(C,D); A \isasyminter C = 0; B \isasyminter D = 0 |] ==>
2.276 + (f \isasymunion g)\isasymin{}bij(A \isasymunion C, B \isasymunion D)
2.277 +
2.278 +\tdx{restrict_bij}: [| f\isasymin{}inj(A,B); C\isasymsubseteq{}A |] ==> restrict(f,C)\isasymin{}bij(C, f``C)
2.279 \end{alltt*}
2.280 \caption{Permutations} \label{zf-perm}
2.281 \end{figure}
2.282 @@ -1371,7 +1371,8 @@
2.283 essentially type-checking. Such proofs are built by applying rules such as
2.284 these:
2.285 \begin{ttbox}\isastyleminor
2.286 -[| ?P ==> ?a \isasymin ?A; ~?P ==> ?b \isasymin ?A |] ==> (if ?P then ?a else ?b) \isasymin ?A
2.287 +[| ?P ==> ?a \isasymin ?A; ~?P ==> ?b \isasymin ?A |]
2.288 +==> (if ?P then ?a else ?b) \isasymin ?A
2.289
2.290 [| ?m \isasymin nat; ?n \isasymin nat |] ==> ?m #+ ?n \isasymin nat
2.291
2.292 @@ -1394,7 +1395,7 @@
2.293 break down all subgoals using type-checking rules. You can add new
2.294 type-checking rules temporarily like this:
2.295 \begin{isabelle}
2.296 -\isacommand{apply}\ (typecheck add: inj_is_fun)
2.297 +\isacommand{apply}\ (typecheck add:\ inj_is_fun)
2.298 \end{isabelle}
2.299
2.300
2.301 @@ -1460,33 +1461,33 @@
2.302 \tt \#- & $[i,i]\To i$ & Left 65 & subtraction
2.303 \end{constants}
2.304
2.305 -\begin{ttbox}\isastyleminor
2.306 +\begin{alltt*}\isastyleminor
2.307 \tdx{nat_def}: nat == lfp(lam r \isasymin Pow(Inf). {\ttlbrace}0{\ttrbrace} \isasymunion {\ttlbrace}succ(x). x \isasymin r{\ttrbrace}
2.308
2.309 -\tdx{nat_case_def}: nat_case(a,b,k) ==
2.310 +\tdx{nat_case_def}: nat_case(a,b,k) ==
2.311 THE y. k=0 & y=a | ({\isasymexists}x. k=succ(x) & y=b(x))
2.312
2.313 -\tdx{nat_0I}: 0 \isasymin nat
2.314 -\tdx{nat_succI}: n \isasymin nat ==> succ(n) \isasymin nat
2.315 -
2.316 -\tdx{nat_induct}:
2.317 +\tdx{nat_0I}: 0 \isasymin nat
2.318 +\tdx{nat_succI}: n \isasymin nat ==> succ(n) \isasymin nat
2.319 +
2.320 +\tdx{nat_induct}:
2.321 [| n \isasymin nat; P(0); !!x. [| x \isasymin nat; P(x) |] ==> P(succ(x))
2.322 |] ==> P(n)
2.323
2.324 -\tdx{nat_case_0}: nat_case(a,b,0) = a
2.325 -\tdx{nat_case_succ}: nat_case(a,b,succ(m)) = b(m)
2.326 -
2.327 -\tdx{add_0_natify}: 0 #+ n = natify(n)
2.328 -\tdx{add_succ}: succ(m) #+ n = succ(m #+ n)
2.329 -
2.330 -\tdx{mult_type}: m #* n \isasymin nat
2.331 -\tdx{mult_0}: 0 #* n = 0
2.332 -\tdx{mult_succ}: succ(m) #* n = n #+ (m #* n)
2.333 -\tdx{mult_commute}: m #* n = n #* m
2.334 -\tdx{add_mult_dist}: (m #+ n) #* k = (m #* k) #+ (n #* k)
2.335 -\tdx{mult_assoc}: (m #* n) #* k = m #* (n #* k)
2.336 -\tdx{mod_div_equality} m \isasymin nat ==> (m div n)#*n #+ m mod n = m
2.337 -\end{ttbox}
2.338 +\tdx{nat_case_0}: nat_case(a,b,0) = a
2.339 +\tdx{nat_case_succ}: nat_case(a,b,succ(m)) = b(m)
2.340 +
2.341 +\tdx{add_0_natify}: 0 #+ n = natify(n)
2.342 +\tdx{add_succ}: succ(m) #+ n = succ(m #+ n)
2.343 +
2.344 +\tdx{mult_type}: m #* n \isasymin nat
2.345 +\tdx{mult_0}: 0 #* n = 0
2.346 +\tdx{mult_succ}: succ(m) #* n = n #+ (m #* n)
2.347 +\tdx{mult_commute}: m #* n = n #* m
2.348 +\tdx{add_mult_dist}: (m #+ n) #* k = (m #* k) #+ (n #* k)
2.349 +\tdx{mult_assoc}: (m #* n) #* k = m #* (n #* k)
2.350 +\tdx{mod_div_equality}: m \isasymin nat ==> (m div n)#*n #+ m mod n = m
2.351 +\end{alltt*}
2.352 \caption{The natural numbers} \label{zf-nat}
2.353 \end{figure}
2.354
2.355 @@ -1543,7 +1544,7 @@
2.356 \tt \$<= & $[i,i]\To o$ & Left 50 & $\le$ on integers
2.357 \end{constants}
2.358
2.359 -\begin{ttbox}\isastyleminor
2.360 +\begin{alltt*}\isastyleminor
2.361 \tdx{zadd_0_intify}: 0 $+ n = intify(n)
2.362
2.363 \tdx{zmult_type}: m $* n \isasymin int
2.364 @@ -1551,7 +1552,7 @@
2.365 \tdx{zmult_commute}: m $* n = n $* m
2.366 \tdx{zadd_zmult_dist}: (m $+ n) $* k = (m $* k) $+ (n $* k)
2.367 \tdx{zmult_assoc}: (m $* n) $* k = m $* (n $* k)
2.368 -\end{ttbox}
2.369 +\end{alltt*}
2.370 \caption{The integers} \label{zf-int}
2.371 \end{figure}
2.372
2.373 @@ -1637,34 +1638,34 @@
2.374
2.375 A simple example of a datatype is \isa{list}, which is built-in, and is
2.376 defined by
2.377 -\begin{ttbox}\isastyleminor
2.378 +\begin{alltt*}\isastyleminor
2.379 consts list :: "i=>i"
2.380 datatype "list(A)" = Nil | Cons ("a \isasymin A", "l \isasymin list(A)")
2.381 -\end{ttbox}
2.382 +\end{alltt*}
2.383 Note that the datatype operator must be declared as a constant first.
2.384 However, the package declares the constructors. Here, \isa{Nil} gets type
2.385 $i$ and \isa{Cons} gets type $[i,i]\To i$.
2.386
2.387 Trees and forests can be modelled by the mutually recursive datatype
2.388 definition
2.389 -\begin{ttbox}\isastyleminor
2.390 +\begin{alltt*}\isastyleminor
2.391 consts
2.392 tree :: "i=>i"
2.393 forest :: "i=>i"
2.394 tree_forest :: "i=>i"
2.395 datatype "tree(A)" = Tcons ("a{\isasymin}A", "f{\isasymin}forest(A)")
2.396 and "forest(A)" = Fnil | Fcons ("t{\isasymin}tree(A)", "f{\isasymin}forest(A)")
2.397 -\end{ttbox}
2.398 +\end{alltt*}
2.399 Here $\isa{tree}(A)$ is the set of trees over $A$, $\isa{forest}(A)$ is
2.400 the set of forests over $A$, and $\isa{tree_forest}(A)$ is the union of
2.401 the previous two sets. All three operators must be declared first.
2.402
2.403 The datatype \isa{term}, which is defined by
2.404 -\begin{ttbox}\isastyleminor
2.405 +\begin{alltt*}\isastyleminor
2.406 consts term :: "i=>i"
2.407 datatype "term(A)" = Apply ("a \isasymin A", "l \isasymin list(term(A))")
2.408 monos list_mono
2.409 -\end{ttbox}
2.410 +\end{alltt*}
2.411 is an example of nested recursion. (The theorem \isa{list_mono} is proved
2.412 in theory \isa{List}, and the \isa{term} example is developed in
2.413 theory
2.414 @@ -1698,17 +1699,17 @@
2.415 \isa{TF}. The rule \isa{tree_forest.induct} performs induction over a
2.416 single predicate~\isa{P}, which is presumed to be defined for both trees
2.417 and forests:
2.418 -\begin{ttbox}\isastyleminor
2.419 +\begin{alltt*}\isastyleminor
2.420 [| x \isasymin tree_forest(A);
2.421 !!a f. [| a \isasymin A; f \isasymin forest(A); P(f) |] ==> P(Tcons(a, f));
2.422 P(Fnil);
2.423 !!f t. [| t \isasymin tree(A); P(t); f \isasymin forest(A); P(f) |]
2.424 ==> P(Fcons(t, f))
2.425 |] ==> P(x)
2.426 -\end{ttbox}
2.427 +\end{alltt*}
2.428 The rule \isa{tree_forest.mutual_induct} performs induction over two
2.429 distinct predicates, \isa{P_tree} and \isa{P_forest}.
2.430 -\begin{ttbox}\isastyleminor
2.431 +\begin{alltt*}\isastyleminor
2.432 [| !!a f.
2.433 [| a{\isasymin}A; f{\isasymin}forest(A); P_forest(f) |] ==> P_tree(Tcons(a,f));
2.434 P_forest(Fnil);
2.435 @@ -1716,24 +1717,24 @@
2.436 ==> P_forest(Fcons(t, f))
2.437 |] ==> ({\isasymforall}za. za \isasymin tree(A) --> P_tree(za)) &
2.438 ({\isasymforall}za. za \isasymin forest(A) --> P_forest(za))
2.439 -\end{ttbox}
2.440 +\end{alltt*}
2.441
2.442 For datatypes with nested recursion, such as the \isa{term} example from
2.443 above, things are a bit more complicated. The rule \isa{term.induct}
2.444 refers to the monotonic operator, \isa{list}:
2.445 -\begin{ttbox}\isastyleminor
2.446 +\begin{alltt*}\isastyleminor
2.447 [| x \isasymin term(A);
2.448 - !!a l. [| a \isasymin A; l \isasymin list(Collect(term(A), P)) |] ==> P(Apply(a, l))
2.449 + !!a l. [| a\isasymin{}A; l\isasymin{}list(Collect(term(A), P)) |] ==> P(Apply(a,l))
2.450 |] ==> P(x)
2.451 -\end{ttbox}
2.452 +\end{alltt*}
2.453 The theory \isa{Induct/Term.thy} derives two higher-level induction rules,
2.454 one of which is particularly useful for proving equations:
2.455 -\begin{ttbox}\isastyleminor
2.456 +\begin{alltt*}\isastyleminor
2.457 [| t \isasymin term(A);
2.458 !!x zs. [| x \isasymin A; zs \isasymin list(term(A)); map(f, zs) = map(g, zs) |]
2.459 ==> f(Apply(x, zs)) = g(Apply(x, zs))
2.460 |] ==> f(t) = g(t)
2.461 -\end{ttbox}
2.462 +\end{alltt*}
2.463 How this can be generalized to other nested datatypes is a matter for future
2.464 research.
2.465
2.466 @@ -1863,10 +1864,10 @@
2.467
2.468 Let us define the set $\isa{bt}(A)$ of binary trees over~$A$. The theory
2.469 must contain these lines:
2.470 -\begin{ttbox}\isastyleminor
2.471 +\begin{alltt*}\isastyleminor
2.472 consts bt :: "i=>i"
2.473 datatype "bt(A)" = Lf | Br ("a\isasymin{}A", "t1\isasymin{}bt(A)", "t2\isasymin{}bt(A)")
2.474 -\end{ttbox}
2.475 +\end{alltt*}
2.476 After loading the theory, we can prove some theorem.
2.477 We begin by declaring the constructor's typechecking rules
2.478 as simplification rules:
2.479 @@ -1880,8 +1881,7 @@
2.480 the \isa{rule\_format} attribute will remove the quantifiers
2.481 before the theorem is stored.
2.482 \begin{isabelle}
2.483 -\isacommand{lemma}\ Br\_neq\_left\ [rule\_format]:\ "l\ \isasymin \
2.484 -bt(A)\ ==>\ \isasymforall x\ r.\ Br(x,l,r)\isasymnoteq{}l"\isanewline
2.485 +\isacommand{lemma}\ Br\_neq\_left\ [rule\_format]:\ "l\isasymin bt(A)\ ==>\ \isasymforall x\ r.\ Br(x,l,r)\isasymnoteq{}l"\isanewline
2.486 \ 1.\ l\ \isasymin \ bt(A)\ \isasymLongrightarrow \ \isasymforall x\ r.\ Br(x,\ l,\ r)\ \isasymnoteq \ l%
2.487 \end{isabelle}
2.488 This can be proved by the structural induction tactic:
2.489 @@ -1944,12 +1944,12 @@
2.490
2.491 Mixfix syntax is sometimes convenient. The theory \isa{Induct/PropLog} makes a
2.492 deep embedding of propositional logic:
2.493 -\begin{ttbox}\isastyleminor
2.494 +\begin{alltt*}\isastyleminor
2.495 consts prop :: i
2.496 datatype "prop" = Fls
2.497 | Var ("n \isasymin nat") ("#_" [100] 100)
2.498 | "=>" ("p \isasymin prop", "q \isasymin prop") (infixr 90)
2.499 -\end{ttbox}
2.500 +\end{alltt*}
2.501 The second constructor has a special $\#n$ syntax, while the third constructor
2.502 is an infixed arrow.
2.503
2.504 @@ -1957,7 +1957,7 @@
2.505 \subsubsection{A giant enumeration type}
2.506
2.507 This example shows a datatype that consists of 60 constructors:
2.508 -\begin{ttbox}\isastyleminor
2.509 +\begin{alltt*}\isastyleminor
2.510 consts enum :: i
2.511 datatype
2.512 "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
2.513 @@ -1967,7 +1967,7 @@
2.514 | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49
2.515 | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59
2.516 end
2.517 -\end{ttbox}
2.518 +\end{alltt*}
2.519 The datatype package scales well. Even though all properties are proved
2.520 rather than assumed, full processing of this definition takes around two seconds
2.521 (on a 1.8GHz machine). The constructors have a balanced representation,
2.522 @@ -2220,11 +2220,11 @@
2.523 Here is the output that results (with the flag set) when the
2.524 \isa{type_intros} and \isa{type_elims} are omitted from the inductive
2.525 definition above:
2.526 -\begin{ttbox}\isastyleminor
2.527 +\begin{alltt*}\isastyleminor
2.528 Inductive definition Finite.Fin
2.529 Fin(A) ==
2.530 lfp(Pow(A),
2.531 - \%X. {z \isasymin Pow(A) . z = 0 | ({\isasymexists}a b. z = cons(a, b) & a \isasymin A & b \isasymin X)})
2.532 + \%X. {z\isasymin{}Pow(A) . z = 0 | ({\isasymexists}a b. z = cons(a,b) & a\isasymin{}A & b\isasymin{}X)})
2.533 Proving monotonicity...
2.534 \ttbreak
2.535 Proving the introduction rules...
2.536 @@ -2236,11 +2236,11 @@
2.537 0 \isasymin Fin(A)
2.538 1. 0 \isasymin Pow(A)
2.539 *** prove_goal: tactic failed
2.540 -\end{ttbox}
2.541 +\end{alltt*}
2.542 We see the need to supply theorems to let the package prove
2.543 $\emptyset\in\isa{Pow}(A)$. Restoring the \isa{type_intros} but not the
2.544 \isa{type_elims}, we again get an error message:
2.545 -\begin{ttbox}\isastyleminor
2.546 +\begin{alltt*}\isastyleminor
2.547 The type-checking subgoal:
2.548 0 \isasymin Fin(A)
2.549 1. 0 \isasymin Pow(A)
2.550 @@ -2257,7 +2257,7 @@
2.551 cons(a, b) \isasymin Fin(A)
2.552 1. [| a \isasymin A; b \isasymin Pow(A) |] ==> cons(a, b) \isasymin Pow(A)
2.553 *** prove_goal: tactic failed
2.554 -\end{ttbox}
2.555 +\end{alltt*}
2.556 The first rule has been type-checked, but the second one has failed. The
2.557 simplest solution to such problems is to prove the failed subgoal separately
2.558 and to supply it under \isa{type_intros}. The solution actually used is
2.559 @@ -2341,12 +2341,12 @@
2.560 elsewhere~\cite{paulson-generic}. The theory first defines the
2.561 datatype
2.562 \isa{comb} of combinators:
2.563 -\begin{ttbox}\isastyleminor
2.564 +\begin{alltt*}\isastyleminor
2.565 consts comb :: i
2.566 datatype "comb" = K
2.567 | S
2.568 | "#" ("p \isasymin comb", "q \isasymin comb") (infixl 90)
2.569 -\end{ttbox}
2.570 +\end{alltt*}
2.571 The theory goes on to define contraction and parallel contraction
2.572 inductively. Then the theory \isa{Induct/Comb.thy} defines special
2.573 cases of contraction, such as this one:
2.574 @@ -2396,7 +2396,7 @@
2.575 not yet been written up anywhere. Here is a summary:
2.576 \begin{itemize}
2.577 \item Theory \isa{Rel} defines the basic properties of relations, such as
2.578 - (ir)reflexivity, (a)symmetry, and transitivity.
2.579 + reflexivity, symmetry and transitivity.
2.580
2.581 \item Theory \isa{EquivClass} develops a theory of equivalence
2.582 classes, not using the Axiom of Choice.