--- a/doc-src/ZF/ZF.tex Wed Aug 20 11:12:48 2003 +0200
+++ b/doc-src/ZF/ZF.tex Wed Aug 20 13:05:22 2003 +0200
@@ -231,7 +231,7 @@
& | & term " -`` " term \\
& | & term " ` " term \\
& | & term " * " term \\
- & | & term " Int " term \\
+ & | & term " \isasyminter " term \\
& | & term " \isasymunion " term \\
& | & term " - " term \\
& | & term " -> " term \\
@@ -373,7 +373,7 @@
\tdx{Inter_def}: Inter(A) == {\ttlbrace}x \isasymin Union(A) . {\isasymforall}y \isasymin A. x \isasymin y{\ttrbrace}
\tdx{Un_def}: A \isasymunion B == Union(Upair(A,B))
-\tdx{Int_def}: A Int B == Inter(Upair(A,B))
+\tdx{Int_def}: A \isasyminter B == Inter(Upair(A,B))
\tdx{Diff_def}: A - B == {\ttlbrace}x \isasymin A . x \isasymnotin B{\ttrbrace}
\subcaption{Union, intersection, difference}
\end{alltt*}
@@ -434,7 +434,8 @@
same set, if $P(x,y)$ is single-valued. The nice syntax for replacement
expands to \isa{Replace}.
-Other consequences of replacement include functional replacement
+Other consequences of replacement include replacement for
+meta-level functions
(\cdx{RepFun}) and definite descriptions (\cdx{The}).
Axioms for separation (\cdx{Collect}) and unordered pairs
(\cdx{Upair}) are traditionally assumed, but they actually follow
@@ -617,10 +618,10 @@
\tdx{UnCI}: (c \isasymnotin B ==> c\isasymin{}A) ==> c\isasymin{}A \isasymunion B
\tdx{UnE}: [| c\isasymin{}A \isasymunion B; c\isasymin{}A ==> P; c\isasymin{}B ==> P |] ==> P
-\tdx{IntI}: [| c\isasymin{}A; c\isasymin{}B |] ==> c\isasymin{}A Int B
-\tdx{IntD1}: c\isasymin{}A Int B ==> c\isasymin{}A
-\tdx{IntD2}: c\isasymin{}A Int B ==> c\isasymin{}B
-\tdx{IntE}: [| c\isasymin{}A Int B; [| c\isasymin{}A; c\isasymin{}B |] ==> P |] ==> P
+\tdx{IntI}: [| c\isasymin{}A; c\isasymin{}B |] ==> c\isasymin{}A \isasyminter B
+\tdx{IntD1}: c\isasymin{}A \isasyminter B ==> c\isasymin{}A
+\tdx{IntD2}: c\isasymin{}A \isasyminter B ==> c\isasymin{}B
+\tdx{IntE}: [| c\isasymin{}A \isasyminter B; [| c\isasymin{}A; c\isasymin{}B |] ==> P |] ==> P
\tdx{DiffI}: [| c\isasymin{}A; c \isasymnotin B |] ==> c\isasymin{}A - B
\tdx{DiffD1}: c\isasymin{}A - B ==> c\isasymin{}A
@@ -715,12 +716,12 @@
\tdx{Un_upper2}: B \isasymsubseteq A \isasymunion B
\tdx{Un_least}: [| A \isasymsubseteq C; B \isasymsubseteq C |] ==> A \isasymunion B \isasymsubseteq C
-\tdx{Int_lower1}: A Int B \isasymsubseteq A
-\tdx{Int_lower2}: A Int B \isasymsubseteq B
-\tdx{Int_greatest}: [| C \isasymsubseteq A; C \isasymsubseteq B |] ==> C \isasymsubseteq A Int B
+\tdx{Int_lower1}: A \isasyminter B \isasymsubseteq A
+\tdx{Int_lower2}: A \isasyminter B \isasymsubseteq B
+\tdx{Int_greatest}: [| C \isasymsubseteq A; C \isasymsubseteq B |] ==> C \isasymsubseteq A \isasyminter B
\tdx{Diff_subset}: A-B \isasymsubseteq A
-\tdx{Diff_contains}: [| C \isasymsubseteq A; C Int B = 0 |] ==> C \isasymsubseteq A-B
+\tdx{Diff_contains}: [| C \isasymsubseteq A; C \isasyminter B = 0 |] ==> C \isasymsubseteq A-B
\tdx{Collect_subset}: Collect(A,P) \isasymsubseteq A
\end{alltt*}
@@ -825,9 +826,9 @@
\tdx{fieldCI}: (<c,a> \isasymnotin r ==> <a,b>\isasymin{}r) ==> a\isasymin{}field(r)
\tdx{fieldE}: [| a\isasymin{}field(r);
- !!x. <a,x>\isasymin{}r ==> P;
- !!x. <x,a>\isasymin{}r ==> P
- |] ==> P
+ !!x. <a,x>\isasymin{}r ==> P;
+ !!x. <x,a>\isasymin{}r ==> P
+ |] ==> P
\tdx{field_subset}: field(A*A) \isasymsubseteq A
\end{alltt*}
@@ -867,7 +868,7 @@
\begin{alltt*}\isastyleminor
\tdx{fun_is_rel}: f\isasymin{}Pi(A,B) ==> f \isasymsubseteq Sigma(A,B)
-\tdx{apply_equality}: [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> f`a = b
+\tdx{apply_equality}: [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> f`a = b
\tdx{apply_equality2}: [| <a,b>\isasymin{}f; <a,c>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> b=c
\tdx{apply_type}: [| f\isasymin{}Pi(A,B); a\isasymin{}A |] ==> f`a\isasymin{}B(a)
@@ -912,7 +913,7 @@
\tdx{fun_empty}: 0\isasymin{}0->0
\tdx{fun_single}: {\ttlbrace}<a,b>{\ttrbrace}\isasymin{}{\ttlbrace}a{\ttrbrace} -> {\ttlbrace}b{\ttrbrace}
-\tdx{fun_disjoint_Un}: [| f\isasymin{}A->B; g\isasymin{}C->D; A Int C = 0 |] ==>
+\tdx{fun_disjoint_Un}: [| f\isasymin{}A->B; g\isasymin{}C->D; A \isasyminter C = 0 |] ==>
(f \isasymunion g)\isasymin{}(A \isasymunion C) -> (B \isasymunion D)
\tdx{fun_disjoint_apply1}: [| a\isasymin{}A; f\isasymin{}A->B; g\isasymin{}C->D; A\isasyminter{}C = 0 |] ==>
@@ -955,28 +956,28 @@
\begin{figure}
\begin{alltt*}\isastyleminor
-\tdx{Int_absorb}: A Int A = A
-\tdx{Int_commute}: A Int B = B Int A
-\tdx{Int_assoc}: (A Int B) Int C = A Int (B Int C)
-\tdx{Int_Un_distrib}: (A \isasymunion B) Int C = (A Int C) \isasymunion (B Int C)
+\tdx{Int_absorb}: A \isasyminter A = A
+\tdx{Int_commute}: A \isasyminter B = B \isasyminter A
+\tdx{Int_assoc}: (A \isasyminter B) \isasyminter C = A \isasyminter (B \isasyminter C)
+\tdx{Int_Un_distrib}: (A \isasymunion B) \isasyminter C = (A \isasyminter C) \isasymunion (B \isasyminter C)
\tdx{Un_absorb}: A \isasymunion A = A
\tdx{Un_commute}: A \isasymunion B = B \isasymunion A
\tdx{Un_assoc}: (A \isasymunion B) \isasymunion C = A \isasymunion (B \isasymunion C)
-\tdx{Un_Int_distrib}: (A Int B) \isasymunion C = (A \isasymunion C) Int (B \isasymunion C)
+\tdx{Un_Int_distrib}: (A \isasyminter B) \isasymunion C = (A \isasymunion C) \isasyminter (B \isasymunion C)
\tdx{Diff_cancel}: A-A = 0
-\tdx{Diff_disjoint}: A Int (B-A) = 0
+\tdx{Diff_disjoint}: A \isasyminter (B-A) = 0
\tdx{Diff_partition}: A \isasymsubseteq B ==> A \isasymunion (B-A) = B
\tdx{double_complement}: [| A \isasymsubseteq B; B \isasymsubseteq C |] ==> (B - (C-A)) = A
-\tdx{Diff_Un}: A - (B \isasymunion C) = (A-B) Int (A-C)
-\tdx{Diff_Int}: A - (B Int C) = (A-B) \isasymunion (A-C)
+\tdx{Diff_Un}: A - (B \isasymunion C) = (A-B) \isasyminter (A-C)
+\tdx{Diff_Int}: A - (B \isasyminter C) = (A-B) \isasymunion (A-C)
\tdx{Union_Un_distrib}: Union(A \isasymunion B) = Union(A) \isasymunion Union(B)
\tdx{Inter_Un_distrib}: [| a \isasymin A; b \isasymin B |] ==>
- Inter(A \isasymunion B) = Inter(A) Int Inter(B)
-
-\tdx{Int_Union_RepFun}: A Int Union(B) = ({\isasymUnion}C \isasymin B. A Int C)
+ Inter(A \isasymunion B) = Inter(A) \isasyminter Inter(B)
+
+\tdx{Int_Union_RepFun}: A \isasyminter Union(B) = ({\isasymUnion}C \isasymin B. A \isasyminter C)
\tdx{Un_Inter_RepFun}: b \isasymin B ==>
A \isasymunion Inter(B) = ({\isasymInter}C \isasymin B. A \isasymunion C)
@@ -987,11 +988,11 @@
\tdx{SUM_Un_distrib2}: (SUM x \isasymin C. A(x) \isasymunion B(x)) =
(SUM x \isasymin C. A(x)) \isasymunion (SUM x \isasymin C. B(x))
-\tdx{SUM_Int_distrib1}: (SUM x \isasymin A Int B. C(x)) =
- (SUM x \isasymin A. C(x)) Int (SUM x \isasymin B. C(x))
-
-\tdx{SUM_Int_distrib2}: (SUM x \isasymin C. A(x) Int B(x)) =
- (SUM x \isasymin C. A(x)) Int (SUM x \isasymin C. B(x))
+\tdx{SUM_Int_distrib1}: (SUM x \isasymin A \isasyminter B. C(x)) =
+ (SUM x \isasymin A. C(x)) \isasyminter (SUM x \isasymin B. C(x))
+
+\tdx{SUM_Int_distrib2}: (SUM x \isasymin C. A(x) \isasyminter B(x)) =
+ (SUM x \isasymin C. A(x)) \isasyminter (SUM x \isasymin C. B(x))
\end{alltt*}
\caption{Equalities} \label{zf-equalities}
\end{figure}
@@ -1109,13 +1110,13 @@
\begin{figure}
\begin{alltt*}\isastyleminor
\tdx{bnd_mono_def}: bnd_mono(D,h) ==
- h(D) \isasymsubseteq D & ({\isasymforall}W X. W \isasymsubseteq X --> X \isasymsubseteq D --> h(W) \isasymsubseteq h(X))
+ h(D)\isasymsubseteq{}D & ({\isasymforall}W X. W\isasymsubseteq{}X --> X\isasymsubseteq{}D --> h(W)\isasymsubseteq{}h(X))
\tdx{lfp_def}: lfp(D,h) == Inter({\ttlbrace}X \isasymin Pow(D). h(X) \isasymsubseteq X{\ttrbrace})
\tdx{gfp_def}: gfp(D,h) == Union({\ttlbrace}X \isasymin Pow(D). X \isasymsubseteq h(X){\ttrbrace})
-\tdx{lfp_lowerbound} [| h(A) \isasymsubseteq A; A \isasymsubseteq D |] ==> lfp(D,h) \isasymsubseteq A
+\tdx{lfp_lowerbound}: [| h(A) \isasymsubseteq A; A \isasymsubseteq D |] ==> lfp(D,h) \isasymsubseteq A
\tdx{lfp_subset}: lfp(D,h) \isasymsubseteq D
@@ -1133,7 +1134,7 @@
!!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X)
|] ==> lfp(D,h) \isasymsubseteq lfp(E,i)
-\tdx{gfp_upperbound} [| A \isasymsubseteq h(A); A \isasymsubseteq D |] ==> A \isasymsubseteq gfp(D,h)
+\tdx{gfp_upperbound}: [| A \isasymsubseteq h(A); A \isasymsubseteq D |] ==> A \isasymsubseteq gfp(D,h)
\tdx{gfp_subset}: gfp(D,h) \isasymsubseteq D
@@ -1191,7 +1192,7 @@
\tdx{Fin_induct}
[| b \isasymin Fin(A);
P(0);
- !!x y. [| x \isasymin A; y \isasymin Fin(A); x \isasymnotin y; P(y) |] ==> P(cons(x,y))
+ !!x y. [| x\isasymin{}A; y\isasymin{}Fin(A); x\isasymnotin{}y; P(y) |] ==> P(cons(x,y))
|] ==> P(b)
\tdx{Fin_mono}: A \isasymsubseteq B ==> Fin(A) \isasymsubseteq Fin(B)
@@ -1216,8 +1217,8 @@
\underscoreon %%because @ is used here
\begin{alltt*}\isastyleminor
-\tdx{NilI}: Nil \isasymin list(A)
-\tdx{ConsI}: [| a \isasymin A; l \isasymin list(A) |] ==> Cons(a,l) \isasymin list(A)
+\tdx{NilI}: Nil \isasymin list(A)
+\tdx{ConsI}: [| a \isasymin A; l \isasymin list(A) |] ==> Cons(a,l) \isasymin list(A)
\tdx{List.induct}
[| l \isasymin list(A);
@@ -1230,11 +1231,11 @@
\tdx{list_mono}: A \isasymsubseteq B ==> list(A) \isasymsubseteq list(B)
-\tdx{map_ident}: l \isasymin list(A) ==> map(\%u. u, l) = l
-\tdx{map_compose}: l \isasymin list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l)
-\tdx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)
+\tdx{map_ident}: l\isasymin{}list(A) ==> map(\%u. u, l) = l
+\tdx{map_compose}: l\isasymin{}list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l)
+\tdx{map_app_distrib}: xs\isasymin{}list(A) ==> map(h, xs@ys) = map(h,xs)@map(h,ys)
\tdx{map_type}
- [| l \isasymin list(A); !!x. x \isasymin A ==> h(x) \isasymin B |] ==> map(h,l) \isasymin list(B)
+ [| l\isasymin{}list(A); !!x. x\isasymin{}A ==> h(x)\isasymin{}B |] ==> map(h,l)\isasymin{}list(B)
\tdx{map_flat}
ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))
\end{alltt*}
@@ -1265,40 +1266,39 @@
\tdx{comp_def}: r O s == {\ttlbrace}xz \isasymin domain(s)*range(r) .
{\isasymexists}x y z. xz=<x,z> & <x,y> \isasymin s & <y,z> \isasymin r{\ttrbrace}
\tdx{id_def}: id(A) == (lam x \isasymin A. x)
-\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}
-\tdx{surj_def}: surj(A,B) == {\ttlbrace} f \isasymin A->B . {\isasymforall}y \isasymin B. {\isasymexists}x \isasymin A. f`x=y {\ttrbrace}
-\tdx{bij_def}: bij(A,B) == inj(A,B) Int surj(A,B)
-
-
-\tdx{left_inverse}: [| f \isasymin inj(A,B); a \isasymin A |] ==> converse(f)`(f`a) = a
-\tdx{right_inverse}: [| f \isasymin inj(A,B); b \isasymin range(f) |] ==>
+\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}
+\tdx{surj_def}: surj(A,B) == {\ttlbrace} f\isasymin{}A->B . {\isasymforall}y\isasymin{}B. {\isasymexists}x\isasymin{}A. f`x=y {\ttrbrace}
+\tdx{bij_def}: bij(A,B) == inj(A,B) \isasyminter surj(A,B)
+
+
+\tdx{left_inverse}: [| f\isasymin{}inj(A,B); a\isasymin{}A |] ==> converse(f)`(f`a) = a
+\tdx{right_inverse}: [| f\isasymin{}inj(A,B); b\isasymin{}range(f) |] ==>
f`(converse(f)`b) = b
-\tdx{inj_converse_inj} f \isasymin inj(A,B) ==> converse(f) \isasymin inj(range(f), A)
-\tdx{bij_converse_bij} f \isasymin bij(A,B) ==> converse(f) \isasymin bij(B,A)
-
-\tdx{comp_type}: [| s \isasymsubseteq A*B; r \isasymsubseteq B*C |] ==> (r O s) \isasymsubseteq A*C
-\tdx{comp_assoc}: (r O s) O t = r O (s O t)
-
-\tdx{left_comp_id}: r \isasymsubseteq A*B ==> id(B) O r = r
-\tdx{right_comp_id}: r \isasymsubseteq A*B ==> r O id(A) = r
-
-\tdx{comp_func}: [| g \isasymin A->B; f \isasymin B->C |] ==> (f O g)
-\isasymin A ->C
-\tdx{comp_func_apply}: [| g \isasymin A->B; f \isasymin B->C; a \isasymin A |] ==> (f O g)`a = f`(g`a)
-
-\tdx{comp_inj}: [| g \isasymin inj(A,B); f \isasymin inj(B,C) |] ==> (f O g):inj(A,C)
-\tdx{comp_surj}: [| g \isasymin surj(A,B); f \isasymin surj(B,C) |] ==> (f O g):surj(A,C)
-\tdx{comp_bij}: [| g \isasymin bij(A,B); f \isasymin bij(B,C) |] ==> (f O g):bij(A,C)
-
-\tdx{left_comp_inverse}: f \isasymin inj(A,B) ==> converse(f) O f = id(A)
-\tdx{right_comp_inverse}: f \isasymin surj(A,B) ==> f O converse(f) = id(B)
+\tdx{inj_converse_inj}: f\isasymin{}inj(A,B) ==> converse(f) \isasymin inj(range(f),A)
+\tdx{bij_converse_bij}: f\isasymin{}bij(A,B) ==> converse(f) \isasymin bij(B,A)
+
+\tdx{comp_type}: [| s \isasymsubseteq A*B; r \isasymsubseteq B*C |] ==> (r O s) \isasymsubseteq A*C
+\tdx{comp_assoc}: (r O s) O t = r O (s O t)
+
+\tdx{left_comp_id}: r \isasymsubseteq A*B ==> id(B) O r = r
+\tdx{right_comp_id}: r \isasymsubseteq A*B ==> r O id(A) = r
+
+\tdx{comp_func}: [| g\isasymin{}A->B; f\isasymin{}B->C |] ==> (f O g) \isasymin A->C
+\tdx{comp_func_apply}: [| g\isasymin{}A->B; f\isasymin{}B->C; a\isasymin{}A |] ==> (f O g)`a = f`(g`a)
+
+\tdx{comp_inj}: [| g\isasymin{}inj(A,B); f\isasymin{}inj(B,C) |] ==> (f O g)\isasymin{}inj(A,C)
+\tdx{comp_surj}: [| g\isasymin{}surj(A,B); f\isasymin{}surj(B,C) |] ==> (f O g)\isasymin{}surj(A,C)
+\tdx{comp_bij}: [| g\isasymin{}bij(A,B); f\isasymin{}bij(B,C) |] ==> (f O g)\isasymin{}bij(A,C)
+
+\tdx{left_comp_inverse}: f\isasymin{}inj(A,B) ==> converse(f) O f = id(A)
+\tdx{right_comp_inverse}: f\isasymin{}surj(A,B) ==> f O converse(f) = id(B)
\tdx{bij_disjoint_Un}:
- [| f \isasymin bij(A,B); g \isasymin bij(C,D); A Int C = 0; B Int D = 0 |] ==>
- (f \isasymunion g) \isasymin bij(A \isasymunion C, B \isasymunion D)
-
-\tdx{restrict_bij}: [| f \isasymin inj(A,B); C \isasymsubseteq A |] ==> restrict(f,C) \isasymin bij(C, f``C)
+ [| f\isasymin{}bij(A,B); g\isasymin{}bij(C,D); A \isasyminter C = 0; B \isasyminter D = 0 |] ==>
+ (f \isasymunion g)\isasymin{}bij(A \isasymunion C, B \isasymunion D)
+
+\tdx{restrict_bij}: [| f\isasymin{}inj(A,B); C\isasymsubseteq{}A |] ==> restrict(f,C)\isasymin{}bij(C, f``C)
\end{alltt*}
\caption{Permutations} \label{zf-perm}
\end{figure}
@@ -1371,7 +1371,8 @@
essentially type-checking. Such proofs are built by applying rules such as
these:
\begin{ttbox}\isastyleminor
-[| ?P ==> ?a \isasymin ?A; ~?P ==> ?b \isasymin ?A |] ==> (if ?P then ?a else ?b) \isasymin ?A
+[| ?P ==> ?a \isasymin ?A; ~?P ==> ?b \isasymin ?A |]
+==> (if ?P then ?a else ?b) \isasymin ?A
[| ?m \isasymin nat; ?n \isasymin nat |] ==> ?m #+ ?n \isasymin nat
@@ -1394,7 +1395,7 @@
break down all subgoals using type-checking rules. You can add new
type-checking rules temporarily like this:
\begin{isabelle}
-\isacommand{apply}\ (typecheck add: inj_is_fun)
+\isacommand{apply}\ (typecheck add:\ inj_is_fun)
\end{isabelle}
@@ -1460,33 +1461,33 @@
\tt \#- & $[i,i]\To i$ & Left 65 & subtraction
\end{constants}
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
\tdx{nat_def}: nat == lfp(lam r \isasymin Pow(Inf). {\ttlbrace}0{\ttrbrace} \isasymunion {\ttlbrace}succ(x). x \isasymin r{\ttrbrace}
-\tdx{nat_case_def}: nat_case(a,b,k) ==
+\tdx{nat_case_def}: nat_case(a,b,k) ==
THE y. k=0 & y=a | ({\isasymexists}x. k=succ(x) & y=b(x))
-\tdx{nat_0I}: 0 \isasymin nat
-\tdx{nat_succI}: n \isasymin nat ==> succ(n) \isasymin nat
-
-\tdx{nat_induct}:
+\tdx{nat_0I}: 0 \isasymin nat
+\tdx{nat_succI}: n \isasymin nat ==> succ(n) \isasymin nat
+
+\tdx{nat_induct}:
[| n \isasymin nat; P(0); !!x. [| x \isasymin nat; P(x) |] ==> P(succ(x))
|] ==> P(n)
-\tdx{nat_case_0}: nat_case(a,b,0) = a
-\tdx{nat_case_succ}: nat_case(a,b,succ(m)) = b(m)
-
-\tdx{add_0_natify}: 0 #+ n = natify(n)
-\tdx{add_succ}: succ(m) #+ n = succ(m #+ n)
-
-\tdx{mult_type}: m #* n \isasymin nat
-\tdx{mult_0}: 0 #* n = 0
-\tdx{mult_succ}: succ(m) #* n = n #+ (m #* n)
-\tdx{mult_commute}: m #* n = n #* m
-\tdx{add_mult_dist}: (m #+ n) #* k = (m #* k) #+ (n #* k)
-\tdx{mult_assoc}: (m #* n) #* k = m #* (n #* k)
-\tdx{mod_div_equality} m \isasymin nat ==> (m div n)#*n #+ m mod n = m
-\end{ttbox}
+\tdx{nat_case_0}: nat_case(a,b,0) = a
+\tdx{nat_case_succ}: nat_case(a,b,succ(m)) = b(m)
+
+\tdx{add_0_natify}: 0 #+ n = natify(n)
+\tdx{add_succ}: succ(m) #+ n = succ(m #+ n)
+
+\tdx{mult_type}: m #* n \isasymin nat
+\tdx{mult_0}: 0 #* n = 0
+\tdx{mult_succ}: succ(m) #* n = n #+ (m #* n)
+\tdx{mult_commute}: m #* n = n #* m
+\tdx{add_mult_dist}: (m #+ n) #* k = (m #* k) #+ (n #* k)
+\tdx{mult_assoc}: (m #* n) #* k = m #* (n #* k)
+\tdx{mod_div_equality}: m \isasymin nat ==> (m div n)#*n #+ m mod n = m
+\end{alltt*}
\caption{The natural numbers} \label{zf-nat}
\end{figure}
@@ -1543,7 +1544,7 @@
\tt \$<= & $[i,i]\To o$ & Left 50 & $\le$ on integers
\end{constants}
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
\tdx{zadd_0_intify}: 0 $+ n = intify(n)
\tdx{zmult_type}: m $* n \isasymin int
@@ -1551,7 +1552,7 @@
\tdx{zmult_commute}: m $* n = n $* m
\tdx{zadd_zmult_dist}: (m $+ n) $* k = (m $* k) $+ (n $* k)
\tdx{zmult_assoc}: (m $* n) $* k = m $* (n $* k)
-\end{ttbox}
+\end{alltt*}
\caption{The integers} \label{zf-int}
\end{figure}
@@ -1637,34 +1638,34 @@
A simple example of a datatype is \isa{list}, which is built-in, and is
defined by
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
consts list :: "i=>i"
datatype "list(A)" = Nil | Cons ("a \isasymin A", "l \isasymin list(A)")
-\end{ttbox}
+\end{alltt*}
Note that the datatype operator must be declared as a constant first.
However, the package declares the constructors. Here, \isa{Nil} gets type
$i$ and \isa{Cons} gets type $[i,i]\To i$.
Trees and forests can be modelled by the mutually recursive datatype
definition
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
consts
tree :: "i=>i"
forest :: "i=>i"
tree_forest :: "i=>i"
datatype "tree(A)" = Tcons ("a{\isasymin}A", "f{\isasymin}forest(A)")
and "forest(A)" = Fnil | Fcons ("t{\isasymin}tree(A)", "f{\isasymin}forest(A)")
-\end{ttbox}
+\end{alltt*}
Here $\isa{tree}(A)$ is the set of trees over $A$, $\isa{forest}(A)$ is
the set of forests over $A$, and $\isa{tree_forest}(A)$ is the union of
the previous two sets. All three operators must be declared first.
The datatype \isa{term}, which is defined by
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
consts term :: "i=>i"
datatype "term(A)" = Apply ("a \isasymin A", "l \isasymin list(term(A))")
monos list_mono
-\end{ttbox}
+\end{alltt*}
is an example of nested recursion. (The theorem \isa{list_mono} is proved
in theory \isa{List}, and the \isa{term} example is developed in
theory
@@ -1698,17 +1699,17 @@
\isa{TF}. The rule \isa{tree_forest.induct} performs induction over a
single predicate~\isa{P}, which is presumed to be defined for both trees
and forests:
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
[| x \isasymin tree_forest(A);
!!a f. [| a \isasymin A; f \isasymin forest(A); P(f) |] ==> P(Tcons(a, f));
P(Fnil);
!!f t. [| t \isasymin tree(A); P(t); f \isasymin forest(A); P(f) |]
==> P(Fcons(t, f))
|] ==> P(x)
-\end{ttbox}
+\end{alltt*}
The rule \isa{tree_forest.mutual_induct} performs induction over two
distinct predicates, \isa{P_tree} and \isa{P_forest}.
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
[| !!a f.
[| a{\isasymin}A; f{\isasymin}forest(A); P_forest(f) |] ==> P_tree(Tcons(a,f));
P_forest(Fnil);
@@ -1716,24 +1717,24 @@
==> P_forest(Fcons(t, f))
|] ==> ({\isasymforall}za. za \isasymin tree(A) --> P_tree(za)) &
({\isasymforall}za. za \isasymin forest(A) --> P_forest(za))
-\end{ttbox}
+\end{alltt*}
For datatypes with nested recursion, such as the \isa{term} example from
above, things are a bit more complicated. The rule \isa{term.induct}
refers to the monotonic operator, \isa{list}:
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
[| x \isasymin term(A);
- !!a l. [| a \isasymin A; l \isasymin list(Collect(term(A), P)) |] ==> P(Apply(a, l))
+ !!a l. [| a\isasymin{}A; l\isasymin{}list(Collect(term(A), P)) |] ==> P(Apply(a,l))
|] ==> P(x)
-\end{ttbox}
+\end{alltt*}
The theory \isa{Induct/Term.thy} derives two higher-level induction rules,
one of which is particularly useful for proving equations:
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
[| t \isasymin term(A);
!!x zs. [| x \isasymin A; zs \isasymin list(term(A)); map(f, zs) = map(g, zs) |]
==> f(Apply(x, zs)) = g(Apply(x, zs))
|] ==> f(t) = g(t)
-\end{ttbox}
+\end{alltt*}
How this can be generalized to other nested datatypes is a matter for future
research.
@@ -1863,10 +1864,10 @@
Let us define the set $\isa{bt}(A)$ of binary trees over~$A$. The theory
must contain these lines:
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
consts bt :: "i=>i"
datatype "bt(A)" = Lf | Br ("a\isasymin{}A", "t1\isasymin{}bt(A)", "t2\isasymin{}bt(A)")
-\end{ttbox}
+\end{alltt*}
After loading the theory, we can prove some theorem.
We begin by declaring the constructor's typechecking rules
as simplification rules:
@@ -1880,8 +1881,7 @@
the \isa{rule\_format} attribute will remove the quantifiers
before the theorem is stored.
\begin{isabelle}
-\isacommand{lemma}\ Br\_neq\_left\ [rule\_format]:\ "l\ \isasymin \
-bt(A)\ ==>\ \isasymforall x\ r.\ Br(x,l,r)\isasymnoteq{}l"\isanewline
+\isacommand{lemma}\ Br\_neq\_left\ [rule\_format]:\ "l\isasymin bt(A)\ ==>\ \isasymforall x\ r.\ Br(x,l,r)\isasymnoteq{}l"\isanewline
\ 1.\ l\ \isasymin \ bt(A)\ \isasymLongrightarrow \ \isasymforall x\ r.\ Br(x,\ l,\ r)\ \isasymnoteq \ l%
\end{isabelle}
This can be proved by the structural induction tactic:
@@ -1944,12 +1944,12 @@
Mixfix syntax is sometimes convenient. The theory \isa{Induct/PropLog} makes a
deep embedding of propositional logic:
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
consts prop :: i
datatype "prop" = Fls
| Var ("n \isasymin nat") ("#_" [100] 100)
| "=>" ("p \isasymin prop", "q \isasymin prop") (infixr 90)
-\end{ttbox}
+\end{alltt*}
The second constructor has a special $\#n$ syntax, while the third constructor
is an infixed arrow.
@@ -1957,7 +1957,7 @@
\subsubsection{A giant enumeration type}
This example shows a datatype that consists of 60 constructors:
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
consts enum :: i
datatype
"enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
@@ -1967,7 +1967,7 @@
| C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49
| C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59
end
-\end{ttbox}
+\end{alltt*}
The datatype package scales well. Even though all properties are proved
rather than assumed, full processing of this definition takes around two seconds
(on a 1.8GHz machine). The constructors have a balanced representation,
@@ -2220,11 +2220,11 @@
Here is the output that results (with the flag set) when the
\isa{type_intros} and \isa{type_elims} are omitted from the inductive
definition above:
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
Inductive definition Finite.Fin
Fin(A) ==
lfp(Pow(A),
- \%X. {z \isasymin Pow(A) . z = 0 | ({\isasymexists}a b. z = cons(a, b) & a \isasymin A & b \isasymin X)})
+ \%X. {z\isasymin{}Pow(A) . z = 0 | ({\isasymexists}a b. z = cons(a,b) & a\isasymin{}A & b\isasymin{}X)})
Proving monotonicity...
\ttbreak
Proving the introduction rules...
@@ -2236,11 +2236,11 @@
0 \isasymin Fin(A)
1. 0 \isasymin Pow(A)
*** prove_goal: tactic failed
-\end{ttbox}
+\end{alltt*}
We see the need to supply theorems to let the package prove
$\emptyset\in\isa{Pow}(A)$. Restoring the \isa{type_intros} but not the
\isa{type_elims}, we again get an error message:
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
The type-checking subgoal:
0 \isasymin Fin(A)
1. 0 \isasymin Pow(A)
@@ -2257,7 +2257,7 @@
cons(a, b) \isasymin Fin(A)
1. [| a \isasymin A; b \isasymin Pow(A) |] ==> cons(a, b) \isasymin Pow(A)
*** prove_goal: tactic failed
-\end{ttbox}
+\end{alltt*}
The first rule has been type-checked, but the second one has failed. The
simplest solution to such problems is to prove the failed subgoal separately
and to supply it under \isa{type_intros}. The solution actually used is
@@ -2341,12 +2341,12 @@
elsewhere~\cite{paulson-generic}. The theory first defines the
datatype
\isa{comb} of combinators:
-\begin{ttbox}\isastyleminor
+\begin{alltt*}\isastyleminor
consts comb :: i
datatype "comb" = K
| S
| "#" ("p \isasymin comb", "q \isasymin comb") (infixl 90)
-\end{ttbox}
+\end{alltt*}
The theory goes on to define contraction and parallel contraction
inductively. Then the theory \isa{Induct/Comb.thy} defines special
cases of contraction, such as this one:
@@ -2396,7 +2396,7 @@
not yet been written up anywhere. Here is a summary:
\begin{itemize}
\item Theory \isa{Rel} defines the basic properties of relations, such as
- (ir)reflexivity, (a)symmetry, and transitivity.
+ reflexivity, symmetry and transitivity.
\item Theory \isa{EquivClass} develops a theory of equivalence
classes, not using the Axiom of Choice.