# HG changeset patch # User paulson # Date 1061377522 -7200 # Node ID 15bab630ae312244d47349039f500acdb28f0fa9 # Parent 8bf06363bbb5a5cadfb55887f665e2f3e14bcf29 finished conversion to Isar format diff -r 8bf06363bbb5 -r 15bab630ae31 doc-src/ZF/FOL.tex --- a/doc-src/ZF/FOL.tex Wed Aug 20 11:12:48 2003 +0200 +++ b/doc-src/ZF/FOL.tex Wed Aug 20 13:05:22 2003 +0200 @@ -259,8 +259,9 @@ IntPr.fast_tac : int -> tactic IntPr.best_tac : int -> tactic \end{ttbox} -Most of these belong to the structure \ML{} \texttt{IntPr} and resemble the -tactics of Isabelle's classical reasoner. Note that you can use the +Most of these belong to the structure \ML{} structure \texttt{IntPr} and resemble the +tactics of Isabelle's classical reasoner. There are no corresponding +Isar methods, but you can use the \isa{tactic} method to call \ML{} tactics in an Isar script: \begin{isabelle} \isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*}) @@ -350,12 +351,14 @@ \section{An intuitionistic example} -Here is a session similar to one in {\em Logic and Computation} -\cite[pages~222--3]{paulson87}. Isabelle treats quantifiers differently -from {\sc lcf}-based theorem provers such as {\sc hol}. +Here is a session similar to one in the book {\em Logic and Computation} +\cite[pages~222--3]{paulson87}. It illustrates the treatment of +quantifier reasoning, which is different in Isabelle than it is in +{\sc lcf}-based theorem provers such as {\sc hol}. -The theory header must specify that we are working in intuitionistic -logic: +The theory header specifies that we are working in intuitionistic +logic by designating \isa{IFOL} rather than \isa{FOL} as the parent +theory: \begin{isabelle} \isacommand{theory}\ IFOL\_examples\ =\ IFOL: \end{isabelle} @@ -524,7 +527,7 @@ $\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise $\all{x}P(x)$ is true. Either way the theorem holds. First, we must -work in a theory based on classical logic: +work in a theory based on classical logic, the theory \isa{FOL}: \begin{isabelle} \isacommand{theory}\ FOL\_examples\ =\ FOL: \end{isabelle} diff -r 8bf06363bbb5 -r 15bab630ae31 doc-src/ZF/ZF.tex --- 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}: ( \isasymnotin r ==> \isasymin{}r) ==> a\isasymin{}field(r) \tdx{fieldE}: [| a\isasymin{}field(r); - !!x. \isasymin{}r ==> P; - !!x. \isasymin{}r ==> P - |] ==> P + !!x. \isasymin{}r ==> P; + !!x. \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}: [| \isasymin{}f; f\isasymin{}Pi(A,B) |] ==> f`a = b +\tdx{apply_equality}: [| \isasymin{}f; f\isasymin{}Pi(A,B) |] ==> f`a = b \tdx{apply_equality2}: [| \isasymin{}f; \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}{\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= & \isasymin s & \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.