# HG changeset patch # User nipkow # Date 774010155 -7200 # Node ID d4bf81734dfe51d583a5093e1d9a4d0d54cc2742 # Parent 552717636da4be396810bc844ca7db6128109abe Corrected HOL.tex diff -r 552717636da4 -r d4bf81734dfe doc-src/Logics/Old_HOL.tex --- a/doc-src/Logics/Old_HOL.tex Tue Jul 12 09:28:00 1994 +0200 +++ b/doc-src/Logics/Old_HOL.tex Tue Jul 12 12:49:15 1994 +0200 @@ -1268,14 +1268,14 @@ \[ c_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \] These functions have certain {\em freeness} properties: \begin{description} +\item[\tt distinct] They are distinct: +\[ c_i(x_1,\dots,x_{k_i}) \neq c_j(y_1,\dots,y_{k_j}) \qquad + \mbox{for all}~ i \neq j. +\] \item[\tt inject] They are injective: \[ (c_j(x_1,\dots,x_{k_j}) = c_j(y_1,\dots,y_{k_j})) = (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j}) \] -\item[\tt ineq] They are distinct: -\[ c_i(x_1,\dots,x_{k_i}) \neq c_j(y_1,\dots,y_{k_j}) \qquad - \mbox{for all}~ i \neq j. -\] \end{description} Because the number of inequalities is quadratic in the number of constructors, a different method is used if their number exceeds @@ -1288,7 +1288,7 @@ \mbox{\it t\_ord}(c_m(x_1,\dots,x_{k_m})) & = & m-1 \end{array} \] -and inequality of constructors is expressed by: +and distinctness of constructors is expressed by: \[ \mbox{\it t\_ord}(x) \neq \mbox{\it t\_ord}(y) \Imp x \neq y. \] @@ -1309,12 +1309,12 @@ = (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for all arguments of the recursive type. -The type also comes with an \ML-like {\tt case}-construct: +The type also comes with an \ML-like \sdx{case}-construct: \[ \begin{array}{rrcl} -\mbox{\tt case}~e~\mbox{\tt of} & c_1(y_{11},\dots,y_{1k_1}) & \To & e_1 \\ +\mbox{\tt case}~e~\mbox{\tt of} & c_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\ \vdots \\ - \mid & c_m(y_{m1},\dots,y_{mk_m}) & \To & e_m + \mid & c_m(x_{m1},\dots,x_{mk_m}) & \To & e_m \end{array} \] In contrast to \ML, {\em all} constructors must be present, their order is @@ -1346,27 +1346,28 @@ \label{datatype-grammar} \end{figure} -Reading the theory file produces a structure which, in addtion to the usual +Reading the theory file produces a structure which, in addition to the usual components, contains a structure named $t$ for each datatype $t$ defined in -the file\footnote{Otherwise multiple datatypes in the same theory file would - lead to name clashes.}. Each structure $t$ contains the following elements: +the file.\footnote{Otherwise multiple datatypes in the same theory file would + lead to name clashes.} Each structure $t$ contains the following elements: \begin{ttbox} -val induct : thm +val distinct : thm list val inject : thm list -val ineq : thm list +val induct : thm val cases : thm list val simps : thm list val induct_tac : string -> int -> tactic \end{ttbox} -{\tt induct}, {\tt inject} and {\tt ineq} contain the theorems described -above. For convenience {\tt ineq} contains inequalities in both directions. +{\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described +above. For convenience {\tt distinct} contains inequalities in both +directions. \begin{warn} If there are five or more constructors, the {\em t\_ord} scheme is used for - {\tt ineq}. In this case the theory {\tt Arith} must be contained - in the current theory, if necessary by adding it explicitly. + {\tt distinct}. In this case the theory {\tt Arith} must be contained + in the current theory, if necessary by including it explicitly. \end{warn} -The reduction rules of the {\tt case}-construct can be found in {\tt cases}. -All theorems from {\tt inject}, {\tt ineq} and {\tt cases} are combined in +The reduction rules of the {\tt case}-construct are in {\tt cases}. All +theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in {\tt simps} for use with the simplifier. The tactic ``{\verb$induct_tac$~{\em var i}\/}'' applies structural induction over variable {\em var} to subgoal {\em i}. @@ -1376,19 +1377,16 @@ \subsubsection{The datatype $\alpha~list$} -We want to define the type $\alpha~list$.\footnote{Of course there is -a list type in HOL already. But for now let us assume that we have to define -a new type.} To do this we have to build a new theory that contains the -type definition. We start from {\tt HOL}. +We want to define the type $\alpha~list$.\footnote{Of course there is a list + type in HOL already. This is only an example.} To do this we have to build +a new theory that contains the type definition. We start from {\tt HOL}. \begin{ttbox} MyList = HOL + datatype 'a list = Nil | Cons ('a, 'a list) end \end{ttbox} -After loading the theory with \verb$use_thy "MyList"$, we can prove -$Cons(x,xs)\neq xs$ using the new theory. First we build a suitable simpset -for the simplifier: - +After loading the theory (\verb$use_thy "MyList"$), we can prove +$Cons(x,xs)\neq xs$. First we build a suitable simpset for the simplifier: \begin{ttbox} val mylist_ss = HOL_ss addsimps MyList.list.simps; goal MyList.thy "!x. Cons(x,xs) ~= xs"; @@ -1406,8 +1404,8 @@ {\out ! x. Cons(x, list) ~= list ==>} {\out ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)} \end{ttbox} -The first subgoal can be proved with the simplifier and the {\tt ineq} axiom -that is part of \verb$mylist_ss$. +The first subgoal can be proved with the simplifier and the distinctness +axioms which are part of \verb$mylist_ss$. \begin{ttbox} by (simp_tac mylist_ss 1); {\out Level 2} @@ -1416,7 +1414,7 @@ {\out ! x. Cons(x, list) ~= list ==>} {\out ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)} \end{ttbox} -Using the {\tt inject} axiom we can quickly prove the remaining goal. +Using the freeness axioms we can quickly prove the remaining goal. \begin{ttbox} by (asm_simp_tac mylist_ss 1); {\out Level 3} @@ -1450,8 +1448,7 @@ Normally one wants to define functions dealing with a newly defined type and prove properties of these functions. As an example let us define \verb|@| for concatenation and {\tt ttl} for the (total) tail of a list, i.e.\ the list -without its first element. We do this in theory \verb|List_fun| which is an -extension of {\tt MyList}: +without its first element: \begin{ttbox} List_fun = MyList + consts ttl :: "'a list => 'a list" @@ -1513,8 +1510,8 @@ \end{ttbox} Because there are more than four constructors, the theory must be based on {\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although -the expression \verb|Mo ~= Tu| is not directly contained in {\tt ineq}, it -can be proved by the simplifier if \verb$arith_ss$ is used: +the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct}, +it can be proved by the simplifier if \verb$arith_ss$ is used: \begin{ttbox} val days_ss = arith_ss addsimps Days.days.simps; diff -r 552717636da4 -r d4bf81734dfe doc-src/Logics/logics.tex --- a/doc-src/Logics/logics.tex Tue Jul 12 09:28:00 1994 +0200 +++ b/doc-src/Logics/logics.tex Tue Jul 12 12:49:15 1994 +0200 @@ -35,7 +35,7 @@ \underscoreoff -\setcounter{secnumdepth}{1} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? \pagestyle{headings} \sloppy diff -r 552717636da4 -r d4bf81734dfe doc-src/Logics/logics.toc --- a/doc-src/Logics/logics.toc Tue Jul 12 09:28:00 1994 +0200 +++ b/doc-src/Logics/logics.toc Tue Jul 12 12:49:15 1994 +0200 @@ -10,22 +10,22 @@ \contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12} \contentsline {section}{\numberline {2.7}A classical example}{14} \contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{15} -\contentsline {subsection}{Deriving the introduction rule}{16} -\contentsline {subsection}{Deriving the elimination rule}{17} -\contentsline {subsection}{Using the derived rules}{17} -\contentsline {subsection}{Derived rules versus definitions}{19} +\contentsline {subsection}{\numberline {2.8.1}Deriving the introduction rule}{16} +\contentsline {subsection}{\numberline {2.8.2}Deriving the elimination rule}{17} +\contentsline {subsection}{\numberline {2.8.3}Using the derived rules}{17} +\contentsline {subsection}{\numberline {2.8.4}Derived rules versus definitions}{19} \contentsline {chapter}{\numberline {3}Zermelo-Fraenkel Set Theory}{22} \contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{22} \contentsline {section}{\numberline {3.2}The syntax of set theory}{23} \contentsline {section}{\numberline {3.3}Binding operators}{25} \contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{27} \contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{30} -\contentsline {subsection}{Fundamental lemmas}{30} -\contentsline {subsection}{Unordered pairs and finite sets}{32} -\contentsline {subsection}{Subset and lattice properties}{32} -\contentsline {subsection}{Ordered pairs}{36} -\contentsline {subsection}{Relations}{36} -\contentsline {subsection}{Functions}{37} +\contentsline {subsection}{\numberline {3.5.1}Fundamental lemmas}{30} +\contentsline {subsection}{\numberline {3.5.2}Unordered pairs and finite sets}{32} +\contentsline {subsection}{\numberline {3.5.3}Subset and lattice properties}{32} +\contentsline {subsection}{\numberline {3.5.4}Ordered pairs}{36} +\contentsline {subsection}{\numberline {3.5.5}Relations}{36} +\contentsline {subsection}{\numberline {3.5.6}Functions}{37} \contentsline {section}{\numberline {3.6}Further developments}{38} \contentsline {section}{\numberline {3.7}Simplification rules}{47} \contentsline {section}{\numberline {3.8}The examples directory}{47} @@ -34,42 +34,50 @@ \contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52} \contentsline {chapter}{\numberline {4}Higher-Order Logic}{55} \contentsline {section}{\numberline {4.1}Syntax}{55} -\contentsline {subsection}{Types}{57} -\contentsline {subsection}{Binders}{58} -\contentsline {subsection}{The {\ptt let} and {\ptt case} constructions}{58} +\contentsline {subsection}{\numberline {4.1.1}Types}{57} +\contentsline {subsection}{\numberline {4.1.2}Binders}{58} +\contentsline {subsection}{\numberline {4.1.3}The {\ptt let} and {\ptt case} constructions}{58} \contentsline {section}{\numberline {4.2}Rules of inference}{58} \contentsline {section}{\numberline {4.3}A formulation of set theory}{60} -\contentsline {subsection}{Syntax of set theory}{65} -\contentsline {subsection}{Axioms and rules of set theory}{69} +\contentsline {subsection}{\numberline {4.3.1}Syntax of set theory}{65} +\contentsline {subsection}{\numberline {4.3.2}Axioms and rules of set theory}{69} \contentsline {section}{\numberline {4.4}Generic packages and classical reasoning}{71} \contentsline {section}{\numberline {4.5}Types}{73} -\contentsline {subsection}{Product and sum types}{73} -\contentsline {subsection}{The type of natural numbers, {\ptt nat}}{73} -\contentsline {subsection}{The type constructor for lists, {\ptt list}}{76} -\contentsline {subsection}{The type constructor for lazy lists, {\ptt llist}}{76} -\contentsline {section}{\numberline {4.6}The examples directories}{79} -\contentsline {section}{\numberline {4.7}Example: Cantor's Theorem}{80} -\contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{82} -\contentsline {section}{\numberline {5.1}Unification for lists}{82} -\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{84} -\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{86} -\contentsline {section}{\numberline {5.4}Tactics for sequents}{87} -\contentsline {section}{\numberline {5.5}Packaging sequent rules}{88} -\contentsline {section}{\numberline {5.6}Proof procedures}{88} -\contentsline {subsection}{Method A}{89} -\contentsline {subsection}{Method B}{89} -\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{90} -\contentsline {section}{\numberline {5.8}A more complex proof}{91} -\contentsline {chapter}{\numberline {6}Constructive Type Theory}{93} -\contentsline {section}{\numberline {6.1}Syntax}{95} -\contentsline {section}{\numberline {6.2}Rules of inference}{95} -\contentsline {section}{\numberline {6.3}Rule lists}{101} -\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{101} -\contentsline {section}{\numberline {6.5}Rewriting tactics}{102} -\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{103} -\contentsline {section}{\numberline {6.7}A theory of arithmetic}{105} -\contentsline {section}{\numberline {6.8}The examples directory}{105} -\contentsline {section}{\numberline {6.9}Example: type inference}{105} -\contentsline {section}{\numberline {6.10}An example of logical reasoning}{107} -\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{110} -\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{111} +\contentsline {subsection}{\numberline {4.5.1}Product and sum types}{73} +\contentsline {subsection}{\numberline {4.5.2}The type of natural numbers, {\ptt nat}}{73} +\contentsline {subsection}{\numberline {4.5.3}The type constructor for lists, {\ptt list}}{76} +\contentsline {subsection}{\numberline {4.5.4}The type constructor for lazy lists, {\ptt llist}}{76} +\contentsline {section}{\numberline {4.6}Datatype declarations}{79} +\contentsline {subsection}{\numberline {4.6.1}Foundations}{79} +\contentsline {subsection}{\numberline {4.6.2}Defining datatypes}{80} +\contentsline {subsection}{\numberline {4.6.3}Examples}{82} +\contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$}{82} +\contentsline {subsubsection}{The datatype $\alpha \penalty \@M \ list$ with mixfix syntax}{83} +\contentsline {subsubsection}{Defining functions on datatypes}{83} +\contentsline {subsubsection}{A datatype for weekdays}{84} +\contentsline {section}{\numberline {4.7}The examples directories}{84} +\contentsline {section}{\numberline {4.8}Example: Cantor's Theorem}{85} +\contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{88} +\contentsline {section}{\numberline {5.1}Unification for lists}{88} +\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{90} +\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{92} +\contentsline {section}{\numberline {5.4}Tactics for sequents}{93} +\contentsline {section}{\numberline {5.5}Packaging sequent rules}{94} +\contentsline {section}{\numberline {5.6}Proof procedures}{94} +\contentsline {subsection}{\numberline {5.6.1}Method A}{95} +\contentsline {subsection}{\numberline {5.6.2}Method B}{95} +\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{96} +\contentsline {section}{\numberline {5.8}A more complex proof}{97} +\contentsline {chapter}{\numberline {6}Constructive Type Theory}{99} +\contentsline {section}{\numberline {6.1}Syntax}{101} +\contentsline {section}{\numberline {6.2}Rules of inference}{101} +\contentsline {section}{\numberline {6.3}Rule lists}{107} +\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{107} +\contentsline {section}{\numberline {6.5}Rewriting tactics}{108} +\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109} +\contentsline {section}{\numberline {6.7}A theory of arithmetic}{111} +\contentsline {section}{\numberline {6.8}The examples directory}{111} +\contentsline {section}{\numberline {6.9}Example: type inference}{111} +\contentsline {section}{\numberline {6.10}An example of logical reasoning}{113} +\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116} +\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117}