doc-src/ZF/ZF.tex
 changeset 14158 15bab630ae31 parent 14154 3bc0128e2c74 child 14202 643fc73e2910
--- 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) |] ==> fa = b
+\tdx{apply_equality}:  [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> fa = 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 |] ==> fa\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. fw=fx --> w=x {\ttrbrace}
-\tdx{surj_def}: surj(A,B) == {\ttlbrace} f \isasymin A->B . {\isasymforall}y \isasymin B. {\isasymexists}x \isasymin A. fx=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)(fa) = 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. fw=fx --> w=x {\ttrbrace}
+\tdx{surj_def}: surj(A,B) == {\ttlbrace} f\isasymin{}A->B . {\isasymforall}y\isasymin{}B. {\isasymexists}x\isasymin{}A. fx=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)(fa) = 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(ga)
-
-\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(ga)
+
+\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, fC)
+    [| 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, fC)
\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}
\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*}
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.