doc-src/HOL/HOL.tex
 author wenzelm Wed Jul 25 12:38:54 2012 +0200 (2012-07-25) changeset 48497 ba61aceaa18a parent 43270 bc72c1ccc89e permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
     1 \chapter{Higher-Order Logic}

     2 \index{higher-order logic|(}

     3 \index{HOL system@{\sc hol} system}

     4

     5 \begin{figure}

     6 \begin{constants}

     7   \it name      &\it meta-type  & \it description \\

     8   \cdx{Trueprop}& $bool\To prop$                & coercion to $prop$\\

     9   \cdx{Not}     & $bool\To bool$                & negation ($\lnot$) \\

    10   \cdx{True}    & $bool$                        & tautology ($\top$) \\

    11   \cdx{False}   & $bool$                        & absurdity ($\bot$) \\

    12   \cdx{If}      & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\

    13   \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder

    14 \end{constants}

    15 \subcaption{Constants}

    16

    17 \begin{constants}

    18 \index{"@@{\tt\at} symbol}

    19 \index{*"! symbol}\index{*"? symbol}

    20 \index{*"?"! symbol}\index{*"E"X"! symbol}

    21   \it symbol &\it name     &\it meta-type & \it description \\

    22   \sdx{SOME} or \tt\at & \cdx{Eps}  & $(\alpha\To bool)\To\alpha$ &

    23         Hilbert description ($\varepsilon$) \\

    24   \sdx{ALL} or {\tt!~} & \cdx{All}  & $(\alpha\To bool)\To bool$ &

    25         universal quantifier ($\forall$) \\

    26   \sdx{EX} or {\tt?~}  & \cdx{Ex}   & $(\alpha\To bool)\To bool$ &

    27         existential quantifier ($\exists$) \\

    28   \texttt{EX!} or {\tt?!} & \cdx{Ex1}  & $(\alpha\To bool)\To bool$ &

    29         unique existence ($\exists!$)\\

    30   \texttt{LEAST}  & \cdx{Least}  & $(\alpha::ord \To bool)\To\alpha$ &

    31         least element

    32 \end{constants}

    33 \subcaption{Binders}

    34

    35 \begin{constants}

    36 \index{*"= symbol}

    37 \index{&@{\tt\&} symbol}

    38 \index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working

    39 \index{*"-"-"> symbol}

    40   \it symbol    & \it meta-type & \it priority & \it description \\

    41   \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &

    42         Left 55 & composition ($\circ$) \\

    43   \tt =         & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\

    44   \tt <         & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\

    45   \tt <=        & $[\alpha::ord,\alpha]\To bool$ & Left 50 &

    46                 less than or equals ($\leq$)\\

    47   \tt \&        & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\

    48   \tt |         & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\

    49   \tt -->       & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)

    50 \end{constants}

    51 \subcaption{Infixes}

    52 \caption{Syntax of \texttt{HOL}} \label{hol-constants}

    53 \end{figure}

    54

    55

    56 \begin{figure}

    57 \index{*let symbol}

    58 \index{*in symbol}

    59 \dquotes

    60 $\begin{array}{rclcl}   61 term & = & \hbox{expression of class~term} \\   62 & | & "SOME~" id " . " formula   63 & | & "\at~" id " . " formula \\   64 & | &   65 \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\   66 & | &   67 \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\   68 & | & "LEAST"~ id " . " formula \\[2ex]   69 formula & = & \hbox{expression of type~bool} \\   70 & | & term " = " term \\   71 & | & term " \ttilde= " term \\   72 & | & term " < " term \\   73 & | & term " <= " term \\   74 & | & "\ttilde\ " formula \\   75 & | & formula " \& " formula \\   76 & | & formula " | " formula \\   77 & | & formula " --> " formula \\   78 & | & "ALL~" id~id^* " . " formula   79 & | & "!~~~" id~id^* " . " formula \\   80 & | & "EX~~" id~id^* " . " formula   81 & | & "?~~~" id~id^* " . " formula \\   82 & | & "EX!~" id~id^* " . " formula   83 & | & "?!~~" id~id^* " . " formula \\   84 \end{array}   85$

    86 \caption{Full grammar for HOL} \label{hol-grammar}

    87 \end{figure}

    88

    89

    90 \section{Syntax}

    91

    92 Figure~\ref{hol-constants} lists the constants (including infixes and

    93 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of

    94 higher-order logic.  Note that $a$\verb|~=|$b$ is translated to

    95 $\lnot(a=b)$.

    96

    97 \begin{warn}

    98   HOL has no if-and-only-if connective; logical equivalence is expressed using

    99   equality.  But equality has a high priority, as befitting a relation, while

   100   if-and-only-if typically has the lowest priority.  Thus, $\lnot\lnot P=P$

   101   abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$.  When using $=$

   102   to mean logical equivalence, enclose both operands in parentheses.

   103 \end{warn}

   104

   105 \subsection{Types and overloading}

   106 The universal type class of higher-order terms is called~\cldx{term}.

   107 By default, explicit type variables have class \cldx{term}.  In

   108 particular the equality symbol and quantifiers are polymorphic over

   109 class \texttt{term}.

   110

   111 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,

   112 formulae are terms.  The built-in type~\tydx{fun}, which constructs

   113 function types, is overloaded with arity {\tt(term,\thinspace

   114   term)\thinspace term}.  Thus, $\sigma\To\tau$ belongs to class~{\tt

   115   term} if $\sigma$ and~$\tau$ do, allowing quantification over

   116 functions.

   117

   118 HOL allows new types to be declared as subsets of existing types,

   119 either using the primitive \texttt{typedef} or the more convenient

   120 \texttt{datatype} (see~{\S}\ref{sec:HOL:datatype}).

   121

   122 Several syntactic type classes --- \cldx{plus}, \cldx{minus},

   123 \cldx{times} and

   124 \cldx{power} --- permit overloading of the operators {\tt+},\index{*"+

   125   symbol} {\tt-}\index{*"- symbol}, {\tt*}.\index{*"* symbol}

   126 and \verb|^|.\index{^@\verb.^. symbol}

   127 %

   128 They are overloaded to denote the obvious arithmetic operations on types

   129 \tdx{nat}, \tdx{int} and~\tdx{real}. (With the \verb|^| operator, the

   130 exponent always has type~\tdx{nat}.)  Non-arithmetic overloadings are also

   131 done: the operator {\tt-} can denote set difference, while \verb|^| can

   132 denote exponentiation of relations (iterated composition).  Unary minus is

   133 also written as~{\tt-} and is overloaded like its 2-place counterpart; it even

   134 can stand for set complement.

   135

   136 The constant \cdx{0} is also overloaded.  It serves as the zero element of

   137 several types, of which the most important is \tdx{nat} (the natural

   138 numbers).  The type class \cldx{plus_ac0} comprises all types for which 0

   139 and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$.  These

   140 types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also

   141 multisets.  The summation operator \cdx{setsum} is available for all types in

   142 this class.

   143

   144 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order

   145 signatures.  The relations $<$ and $\leq$ are polymorphic over this

   146 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and

   147 the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass

   148 \cldx{order} of \cldx{ord} which axiomatizes the types that are partially

   149 ordered with respect to~$\leq$.  A further subclass \cldx{linorder} of

   150 \cldx{order} axiomatizes linear orderings.

   151 For details, see the file \texttt{Ord.thy}.

   152

   153 If you state a goal containing overloaded functions, you may need to include

   154 type constraints.  Type inference may otherwise make the goal more

   155 polymorphic than you intended, with confusing results.  For example, the

   156 variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type

   157 $\alpha::\{ord,plus\}$, although you may have expected them to have some

   158 numeric type, e.g. $nat$.  Instead you should have stated the goal as

   159 $(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have

   160 type $nat$.

   161

   162 \begin{warn}

   163   If resolution fails for no obvious reason, try setting

   164   \ttindex{show_types} to \texttt{true}, causing Isabelle to display

   165   types of terms.  Possibly set \ttindex{show_sorts} to \texttt{true} as

   166   well, causing Isabelle to display type classes and sorts.

   167

   168   \index{unification!incompleteness of}

   169   Where function types are involved, Isabelle's unification code does not

   170   guarantee to find instantiations for type variables automatically.  Be

   171   prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},

   172   possibly instantiating type variables.  Setting

   173   \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report

   174   omitted search paths during unification.\index{tracing!of unification}

   175 \end{warn}

   176

   177

   178 \subsection{Binders}

   179

   180 Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$

   181 satisfying~$P$, if such exists.  Since all terms in HOL denote something, a

   182 description is always meaningful, but we do not know its value unless $P$

   183 defines it uniquely.  We may write descriptions as \cdx{Eps}($\lambda x.   184 P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}.

   185

   186 Existential quantification is defined by

   187 $\exists x. P~x \;\equiv\; P(\varepsilon x. P~x).$

   188 The unique existence quantifier, $\exists!x. P$, is defined in terms

   189 of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested

   190 quantifications.  For instance, $\exists!x\,y. P\,x\,y$ abbreviates

   191 $\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there

   192 exists a unique pair $(x,y)$ satisfying~$P\,x\,y$.

   193

   194 \medskip

   195

   196 \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The

   197 basic Isabelle/HOL binders have two notations.  Apart from the usual

   198 \texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also

   199 supports the original notation of Gordon's {\sc hol} system: \texttt{!}\

   200 and~\texttt{?}.  In the latter case, the existential quantifier \emph{must} be

   201 followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a

   202 quantification.  Both notations are accepted for input.  The print mode

   203 \ttindexbold{HOL}'' governs the output notation.  If enabled (e.g.\ by

   204 passing option \texttt{-m HOL} to the \texttt{isabelle} executable),

   205 then~{\tt!}\ and~{\tt?}\ are displayed.

   206

   207 \medskip

   208

   209 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a

   210 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined

   211 to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see

   212 Fig.~\ref{hol-defs}).  The definition uses Hilbert's $\varepsilon$

   213 choice operator, so \texttt{Least} is always meaningful, but may yield

   214 nothing useful in case there is not a unique least element satisfying

   215 $P$.\footnote{Class $ord$ does not require much of its instances, so

   216   $\leq$ need not be a well-ordering, not even an order at all!}

   217

   218 \medskip All these binders have priority 10.

   219

   220 \begin{warn}

   221 The low priority of binders means that they need to be enclosed in

   222 parenthesis when they occur in the context of other operations.  For example,

   223 instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$.

   224 \end{warn}

   225

   226

   227 \subsection{The let and case constructions}

   228 Local abbreviations can be introduced by a \texttt{let} construct whose

   229 syntax appears in Fig.\ts\ref{hol-grammar}.  Internally it is translated into

   230 the constant~\cdx{Let}.  It can be expanded by rewriting with its

   231 definition, \tdx{Let_def}.

   232

   233 HOL also defines the basic syntax

   234 $\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n$

   235 as a uniform means of expressing \texttt{case} constructs.  Therefore \texttt{case}

   236 and \sdx{of} are reserved words.  Initially, this is mere syntax and has no

   237 logical meaning.  By declaring translations, you can cause instances of the

   238 \texttt{case} construct to denote applications of particular case operators.

   239 This is what happens automatically for each \texttt{datatype} definition

   240 (see~{\S}\ref{sec:HOL:datatype}).

   241

   242 \begin{warn}

   243 Both \texttt{if} and \texttt{case} constructs have as low a priority as

   244 quantifiers, which requires additional enclosing parentheses in the context

   245 of most other operations.  For example, instead of $f~x = {\tt if\dots   246 then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots   247 else\dots})$.

   248 \end{warn}

   249

   250 \section{Rules of inference}

   251

   252 \begin{figure}

   253 \begin{ttbox}\makeatother

   254 \tdx{refl}          t = (t::'a)

   255 \tdx{subst}         [| s = t; P s |] ==> P (t::'a)

   256 \tdx{ext}           (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x)

   257 \tdx{impI}          (P ==> Q) ==> P-->Q

   258 \tdx{mp}            [| P-->Q;  P |] ==> Q

   259 \tdx{iff}           (P-->Q) --> (Q-->P) --> (P=Q)

   260 \tdx{someI}         P(x::'a) ==> P(@x. P x)

   261 \tdx{True_or_False} (P=True) | (P=False)

   262 \end{ttbox}

   263 \caption{The \texttt{HOL} rules} \label{hol-rules}

   264 \end{figure}

   265

   266 Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with

   267 their~{\ML} names.  Some of the rules deserve additional comments:

   268 \begin{ttdescription}

   269 \item[\tdx{ext}] expresses extensionality of functions.

   270 \item[\tdx{iff}] asserts that logically equivalent formulae are

   271   equal.

   272 \item[\tdx{someI}] gives the defining property of the Hilbert

   273   $\varepsilon$-operator.  It is a form of the Axiom of Choice.  The derived rule

   274   \tdx{some_equality} (see below) is often easier to use.

   275 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In

   276     fact, the $\varepsilon$-operator already makes the logic classical, as

   277     shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}

   278 \end{ttdescription}

   279

   280

   281 \begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message

   282 \begin{ttbox}\makeatother

   283 \tdx{True_def}   True     == ((\%x::bool. x)=(\%x. x))

   284 \tdx{All_def}    All      == (\%P. P = (\%x. True))

   285 \tdx{Ex_def}     Ex       == (\%P. P(@x. P x))

   286 \tdx{False_def}  False    == (!P. P)

   287 \tdx{not_def}    not      == (\%P. P-->False)

   288 \tdx{and_def}    op &     == (\%P Q. !R. (P-->Q-->R) --> R)

   289 \tdx{or_def}     op |     == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)

   290 \tdx{Ex1_def}    Ex1      == (\%P. ? x. P x & (! y. P y --> y=x))

   291

   292 \tdx{o_def}      op o     == (\%(f::'b=>'c) g x::'a. f(g x))

   293 \tdx{if_def}     If P x y ==

   294               (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))

   295 \tdx{Let_def}    Let s f  == f s

   296 \tdx{Least_def}  Least P  == @x. P(x) & (ALL y. P(y) --> x <= y)"

   297 \end{ttbox}

   298 \caption{The \texttt{HOL} definitions} \label{hol-defs}

   299 \end{figure}

   300

   301

   302 HOL follows standard practice in higher-order logic: only a few connectives

   303 are taken as primitive, with the remainder defined obscurely

   304 (Fig.\ts\ref{hol-defs}).  Gordon's {\sc hol} system expresses the

   305 corresponding definitions \cite[page~270]{mgordon-hol} using

   306 object-equality~({\tt=}), which is possible because equality in higher-order

   307 logic may equate formulae and even functions over formulae.  But theory~HOL,

   308 like all other Isabelle theories, uses meta-equality~({\tt==}) for

   309 definitions.

   310 \begin{warn}

   311 The definitions above should never be expanded and are shown for completeness

   312 only.  Instead users should reason in terms of the derived rules shown below

   313 or, better still, using high-level tactics.

   314 \end{warn}

   315

   316 Some of the rules mention type variables; for example, \texttt{refl}

   317 mentions the type variable~{\tt'a}.  This allows you to instantiate

   318 type variables explicitly by calling \texttt{res_inst_tac}.

   319

   320

   321 \begin{figure}

   322 \begin{ttbox}

   323 \tdx{sym}         s=t ==> t=s

   324 \tdx{trans}       [| r=s; s=t |] ==> r=t

   325 \tdx{ssubst}      [| t=s; P s |] ==> P t

   326 \tdx{box_equals}  [| a=b;  a=c;  b=d |] ==> c=d

   327 \tdx{arg_cong}    x = y ==> f x = f y

   328 \tdx{fun_cong}    f = g ==> f x = g x

   329 \tdx{cong}        [| f = g; x = y |] ==> f x = g y

   330 \tdx{not_sym}     t ~= s ==> s ~= t

   331 \subcaption{Equality}

   332

   333 \tdx{TrueI}       True

   334 \tdx{FalseE}      False ==> P

   335

   336 \tdx{conjI}       [| P; Q |] ==> P&Q

   337 \tdx{conjunct1}   [| P&Q |] ==> P

   338 \tdx{conjunct2}   [| P&Q |] ==> Q

   339 \tdx{conjE}       [| P&Q;  [| P; Q |] ==> R |] ==> R

   340

   341 \tdx{disjI1}      P ==> P|Q

   342 \tdx{disjI2}      Q ==> P|Q

   343 \tdx{disjE}       [| P | Q; P ==> R; Q ==> R |] ==> R

   344

   345 \tdx{notI}        (P ==> False) ==> ~ P

   346 \tdx{notE}        [| ~ P;  P |] ==> R

   347 \tdx{impE}        [| P-->Q;  P;  Q ==> R |] ==> R

   348 \subcaption{Propositional logic}

   349

   350 \tdx{iffI}        [| P ==> Q;  Q ==> P |] ==> P=Q

   351 \tdx{iffD1}       [| P=Q; P |] ==> Q

   352 \tdx{iffD2}       [| P=Q; Q |] ==> P

   353 \tdx{iffE}        [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R

   354 \subcaption{Logical equivalence}

   355

   356 \end{ttbox}

   357 \caption{Derived rules for HOL} \label{hol-lemmas1}

   358 \end{figure}

   359 %

   360 %\tdx{eqTrueI}     P ==> P=True

   361 %\tdx{eqTrueE}     P=True ==> P

   362

   363

   364 \begin{figure}

   365 \begin{ttbox}\makeatother

   366 \tdx{allI}      (!!x. P x) ==> !x. P x

   367 \tdx{spec}      !x. P x ==> P x

   368 \tdx{allE}      [| !x. P x;  P x ==> R |] ==> R

   369 \tdx{all_dupE}  [| !x. P x;  [| P x; !x. P x |] ==> R |] ==> R

   370

   371 \tdx{exI}       P x ==> ? x. P x

   372 \tdx{exE}       [| ? x. P x; !!x. P x ==> Q |] ==> Q

   373

   374 \tdx{ex1I}      [| P a;  !!x. P x ==> x=a |] ==> ?! x. P x

   375 \tdx{ex1E}      [| ?! x. P x;  !!x. [| P x;  ! y. P y --> y=x |] ==> R

   376           |] ==> R

   377

   378 \tdx{some_equality}   [| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a

   379 \subcaption{Quantifiers and descriptions}

   380

   381 \tdx{ccontr}          (~P ==> False) ==> P

   382 \tdx{classical}       (~P ==> P) ==> P

   383 \tdx{excluded_middle} ~P | P

   384

   385 \tdx{disjCI}       (~Q ==> P) ==> P|Q

   386 \tdx{exCI}         (! x. ~ P x ==> P a) ==> ? x. P x

   387 \tdx{impCE}        [| P-->Q; ~ P ==> R; Q ==> R |] ==> R

   388 \tdx{iffCE}        [| P=Q;  [| P;Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R

   389 \tdx{notnotD}      ~~P ==> P

   390 \tdx{swap}         ~P ==> (~Q ==> P) ==> Q

   391 \subcaption{Classical logic}

   392

   393 \tdx{if_P}         P ==> (if P then x else y) = x

   394 \tdx{if_not_P}     ~ P ==> (if P then x else y) = y

   395 \tdx{split_if}     P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))

   396 \subcaption{Conditionals}

   397 \end{ttbox}

   398 \caption{More derived rules} \label{hol-lemmas2}

   399 \end{figure}

   400

   401 Some derived rules are shown in Figures~\ref{hol-lemmas1}

   402 and~\ref{hol-lemmas2}, with their {\ML} names.  These include natural rules

   403 for the logical connectives, as well as sequent-style elimination rules for

   404 conjunctions, implications, and universal quantifiers.

   405

   406 Note the equality rules: \tdx{ssubst} performs substitution in

   407 backward proofs, while \tdx{box_equals} supports reasoning by

   408 simplifying both sides of an equation.

   409

   410 The following simple tactics are occasionally useful:

   411 \begin{ttdescription}

   412 \item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI}

   413   repeatedly to remove all outermost universal quantifiers and implications

   414   from subgoal $i$.

   415 \item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on

   416   $P$ for subgoal $i$: the latter is replaced by two identical subgoals with

   417   the added assumptions $P$ and $\lnot P$, respectively.

   418 \item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then

   419   \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining

   420   from an induction hypothesis. As a generalization of \texttt{mp_tac},

   421   if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and

   422   $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables)

   423   then it replaces the universally quantified implication by $Q \vec{a}$.

   424   It may instantiate unknowns. It fails if it can do nothing.

   425 \end{ttdescription}

   426

   427

   428 \begin{figure}

   429 \begin{center}

   430 \begin{tabular}{rrr}

   431   \it name      &\it meta-type  & \it description \\

   432 \index{{}@\verb'{}' symbol}

   433   \verb|{}|     & $\alpha\,set$         & the empty set \\

   434   \cdx{insert}  & $[\alpha,\alpha\,set]\To \alpha\,set$

   435         & insertion of element \\

   436   \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$

   437         & comprehension \\

   438   \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$

   439         & intersection over a set\\

   440   \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$

   441         & union over a set\\

   442   \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$

   443         &set of sets intersection \\

   444   \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$

   445         &set of sets union \\

   446   \cdx{Pow}   & $\alpha\,set \To (\alpha\,set)set$

   447         & powerset \$1ex]   448 \cdx{range} & (\alpha\To\beta )\To\beta\,set   449 & range of a function \\[1ex]   450 \cdx{Ball}~~\cdx{Bex} & [\alpha\,set,\alpha\To bool]\To bool   451 & bounded quantifiers   452 \end{tabular}   453 \end{center}   454 \subcaption{Constants}   455   456 \begin{center}   457 \begin{tabular}{llrrr}   458 \it symbol &\it name &\it meta-type & \it priority & \it description \\   459 \sdx{INT} & \cdx{INTER1} & (\alpha\To\beta\,set)\To\beta\,set & 10 &   460 intersection\\   461 \sdx{UN} & \cdx{UNION1} & (\alpha\To\beta\,set)\To\beta\,set & 10 &   462 union   463 \end{tabular}   464 \end{center}   465 \subcaption{Binders}   466   467 \begin{center}   468 \index{*"" symbol}   469 \index{*": symbol}   470 \index{*"<"= symbol}   471 \begin{tabular}{rrrr}   472 \it symbol & \it meta-type & \it priority & \it description \\   473 \tt  & [\alpha\To\beta ,\alpha\,set]\To \beta\,set   474 & Left 90 & image \\   475 \sdx{Int} & [\alpha\,set,\alpha\,set]\To\alpha\,set   476 & Left 70 & intersection (\int) \\   477 \sdx{Un} & [\alpha\,set,\alpha\,set]\To\alpha\,set   478 & Left 65 & union (\un) \\   479 \tt: & [\alpha ,\alpha\,set]\To bool   480 & Left 50 & membership (\in) \\   481 \tt <= & [\alpha\,set,\alpha\,set]\To bool   482 & Left 50 & subset (\subseteq)   483 \end{tabular}   484 \end{center}   485 \subcaption{Infixes}   486 \caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax}   487 \end{figure}   488   489   490 \begin{figure}   491 \begin{center} \tt\frenchspacing   492 \index{*"! symbol}   493 \begin{tabular}{rrr}   494 \it external & \it internal & \it description \\   495 a \ttilde: b & \ttilde(a : b) & \rm not in\\   496 {\ttlbrace}a@1, \ldots{\ttrbrace} & insert a@1 \ldots {\ttlbrace}{\ttrbrace} & \rm finite set \\   497 {\ttlbrace}x. P[x]{\ttrbrace} & Collect(\lambda x. P[x]) &   498 \rm comprehension \\   499 \sdx{INT} x:A. B[x] & INTER A \lambda x. B[x] &   500 \rm intersection \\   501 \sdx{UN}{\tt\ } x:A. B[x] & UNION A \lambda x. B[x] &   502 \rm union \\   503 \sdx{ALL} x:A.\ P[x] or \texttt{!} x:A.\ P[x] &   504 Ball A \lambda x.\ P[x] &   505 \rm bounded \forall \\   506 \sdx{EX}{\tt\ } x:A.\ P[x] or \texttt{?} x:A.\ P[x] &   507 Bex A \lambda x.\ P[x] & \rm bounded \exists   508 \end{tabular}   509 \end{center}   510 \subcaption{Translations}   511   512 \dquotes   513 \[\begin{array}{rclcl}   514 term & = & \hbox{other terms\ldots} \\   515 & | & "{\ttlbrace}{\ttrbrace}" \\   516 & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\   517 & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\   518 & | & term "  " term \\   519 & | & term " Int " term \\   520 & | & term " Un " term \\   521 & | & "INT~~" id ":" term " . " term \\   522 & | & "UN~~~" id ":" term " . " term \\   523 & | & "INT~~" id~id^* " . " term \\   524 & | & "UN~~~" id~id^* " . " term \\[2ex]   525 formula & = & \hbox{other formulae\ldots} \\   526 & | & term " : " term \\   527 & | & term " \ttilde: " term \\   528 & | & term " <= " term \\   529 & | & "ALL " id ":" term " . " formula   530 & | & "!~" id ":" term " . " formula \\   531 & | & "EX~~" id ":" term " . " formula   532 & | & "?~" id ":" term " . " formula \\   533 \end{array}   534$

   535 \subcaption{Full Grammar}

   536 \caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2}

   537 \end{figure}

   538

   539

   540 \section{A formulation of set theory}

   541 Historically, higher-order logic gives a foundation for Russell and

   542 Whitehead's theory of classes.  Let us use modern terminology and call them

   543 {\bf sets}, but note that these sets are distinct from those of ZF set theory,

   544 and behave more like ZF classes.

   545 \begin{itemize}

   546 \item

   547 Sets are given by predicates over some type~$\sigma$.  Types serve to

   548 define universes for sets, but type-checking is still significant.

   549 \item

   550 There is a universal set (for each type).  Thus, sets have complements, and

   551 may be defined by absolute comprehension.

   552 \item

   553 Although sets may contain other sets as elements, the containing set must

   554 have a more complex type.

   555 \end{itemize}

   556 Finite unions and intersections have the same behaviour in HOL as they do

   557 in~ZF.  In HOL the intersection of the empty set is well-defined, denoting the

   558 universal set for the given type.

   559

   560 \subsection{Syntax of set theory}\index{*set type}

   561 HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is essentially

   562 the same as $\alpha\To bool$.  The new type is defined for clarity and to

   563 avoid complications involving function types in unification.  The isomorphisms

   564 between the two types are declared explicitly.  They are very natural:

   565 \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}

   566 maps in the other direction (ignoring argument order).

   567

   568 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax

   569 translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new

   570 constructs.  Infix operators include union and intersection ($A\un B$

   571 and $A\int B$), the subset and membership relations, and the image

   572 operator~{\tt}\@.  Note that $a$\verb|~:|$b$ is translated to

   573 $\lnot(a\in b)$.

   574

   575 The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in

   576 the obvious manner using~\texttt{insert} and~$\{\}$:

   577 \begin{eqnarray*}

   578   \{a, b, c\} & \equiv &

   579   \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))

   580 \end{eqnarray*}

   581

   582 The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of

   583 suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain

   584 free occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda x.   585 P[x])$.  It defines sets by absolute comprehension, which is impossible in~ZF;

   586 the type of~$x$ implicitly restricts the comprehension.

   587

   588 The set theory defines two {\bf bounded quantifiers}:

   589 \begin{eqnarray*}

   590    \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\

   591    \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]

   592 \end{eqnarray*}

   593 The constants~\cdx{Ball} and~\cdx{Bex} are defined

   594 accordingly.  Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may

   595 write\index{*"! symbol}\index{*"? symbol}

   596 \index{*ALL symbol}\index{*EX symbol}

   597 %

   598 \hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}.  The

   599 original notation of Gordon's {\sc hol} system is supported as well:

   600 \texttt{!}\ and \texttt{?}.

   601

   602 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and

   603 $\bigcap@{x\in A}B[x]$, are written

   604 \sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and

   605 \sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}.

   606

   607 Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x   608 B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and

   609 \sdx{INT}~\hbox{\tt$x$.\ $B[x]$}.  They are equivalent to the previous

   610 union and intersection operators when $A$ is the universal set.

   611

   612 The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets.  They are

   613 not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,

   614 respectively.

   615

   616

   617

   618 \begin{figure} \underscoreon

   619 \begin{ttbox}

   620 \tdx{mem_Collect_eq}    (a : {\ttlbrace}x. P x{\ttrbrace}) = P a

   621 \tdx{Collect_mem_eq}    {\ttlbrace}x. x:A{\ttrbrace} = A

   622

   623 \tdx{empty_def}         {\ttlbrace}{\ttrbrace}          == {\ttlbrace}x. False{\ttrbrace}

   624 \tdx{insert_def}        insert a B  == {\ttlbrace}x. x=a{\ttrbrace} Un B

   625 \tdx{Ball_def}          Ball A P    == ! x. x:A --> P x

   626 \tdx{Bex_def}           Bex A P     == ? x. x:A & P x

   627 \tdx{subset_def}        A <= B      == ! x:A. x:B

   628 \tdx{Un_def}            A Un B      == {\ttlbrace}x. x:A | x:B{\ttrbrace}

   629 \tdx{Int_def}           A Int B     == {\ttlbrace}x. x:A & x:B{\ttrbrace}

   630 \tdx{set_diff_def}      A - B       == {\ttlbrace}x. x:A & x~:B{\ttrbrace}

   631 \tdx{Compl_def}         -A          == {\ttlbrace}x. ~ x:A{\ttrbrace}

   632 \tdx{INTER_def}         INTER A B   == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace}

   633 \tdx{UNION_def}         UNION A B   == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace}

   634 \tdx{INTER1_def}        INTER1 B    == INTER {\ttlbrace}x. True{\ttrbrace} B

   635 \tdx{UNION1_def}        UNION1 B    == UNION {\ttlbrace}x. True{\ttrbrace} B

   636 \tdx{Inter_def}         Inter S     == (INT x:S. x)

   637 \tdx{Union_def}         Union S     == (UN  x:S. x)

   638 \tdx{Pow_def}           Pow A       == {\ttlbrace}B. B <= A{\ttrbrace}

   639 \tdx{image_def}         fA        == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace}

   640 \tdx{range_def}         range f     == {\ttlbrace}y. ? x. y=f x{\ttrbrace}

   641 \end{ttbox}

   642 \caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}

   643 \end{figure}

   644

   645

   646 \begin{figure} \underscoreon

   647 \begin{ttbox}

   648 \tdx{CollectI}        [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace}

   649 \tdx{CollectD}        [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a

   650 \tdx{CollectE}        [| a : {\ttlbrace}x. P x{\ttrbrace};  P a ==> W |] ==> W

   651

   652 \tdx{ballI}           [| !!x. x:A ==> P x |] ==> ! x:A. P x

   653 \tdx{bspec}           [| ! x:A. P x;  x:A |] ==> P x

   654 \tdx{ballE}           [| ! x:A. P x;  P x ==> Q;  ~ x:A ==> Q |] ==> Q

   655

   656 \tdx{bexI}            [| P x;  x:A |] ==> ? x:A. P x

   657 \tdx{bexCI}           [| ! x:A. ~ P x ==> P a;  a:A |] ==> ? x:A. P x

   658 \tdx{bexE}            [| ? x:A. P x;  !!x. [| x:A; P x |] ==> Q  |] ==> Q

   659 \subcaption{Comprehension and Bounded quantifiers}

   660

   661 \tdx{subsetI}         (!!x. x:A ==> x:B) ==> A <= B

   662 \tdx{subsetD}         [| A <= B;  c:A |] ==> c:B

   663 \tdx{subsetCE}        [| A <= B;  ~ (c:A) ==> P;  c:B ==> P |] ==> P

   664

   665 \tdx{subset_refl}     A <= A

   666 \tdx{subset_trans}    [| A<=B;  B<=C |] ==> A<=C

   667

   668 \tdx{equalityI}       [| A <= B;  B <= A |] ==> A = B

   669 \tdx{equalityD1}      A = B ==> A<=B

   670 \tdx{equalityD2}      A = B ==> B<=A

   671 \tdx{equalityE}       [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P

   672

   673 \tdx{equalityCE}      [| A = B;  [| c:A; c:B |] ==> P;

   674                            [| ~ c:A; ~ c:B |] ==> P

   675                 |]  ==>  P

   676 \subcaption{The subset and equality relations}

   677 \end{ttbox}

   678 \caption{Derived rules for set theory} \label{hol-set1}

   679 \end{figure}

   680

   681

   682 \begin{figure} \underscoreon

   683 \begin{ttbox}

   684 \tdx{emptyE}   a : {\ttlbrace}{\ttrbrace} ==> P

   685

   686 \tdx{insertI1} a : insert a B

   687 \tdx{insertI2} a : B ==> a : insert b B

   688 \tdx{insertE}  [| a : insert b A;  a=b ==> P;  a:A ==> P |] ==> P

   689

   690 \tdx{ComplI}   [| c:A ==> False |] ==> c : -A

   691 \tdx{ComplD}   [| c : -A |] ==> ~ c:A

   692

   693 \tdx{UnI1}     c:A ==> c : A Un B

   694 \tdx{UnI2}     c:B ==> c : A Un B

   695 \tdx{UnCI}     (~c:B ==> c:A) ==> c : A Un B

   696 \tdx{UnE}      [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P

   697

   698 \tdx{IntI}     [| c:A;  c:B |] ==> c : A Int B

   699 \tdx{IntD1}    c : A Int B ==> c:A

   700 \tdx{IntD2}    c : A Int B ==> c:B

   701 \tdx{IntE}     [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P

   702

   703 \tdx{UN_I}     [| a:A;  b: B a |] ==> b: (UN x:A. B x)

   704 \tdx{UN_E}     [| b: (UN x:A. B x);  !!x.[| x:A;  b:B x |] ==> R |] ==> R

   705

   706 \tdx{INT_I}    (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)

   707 \tdx{INT_D}    [| b: (INT x:A. B x);  a:A |] ==> b: B a

   708 \tdx{INT_E}    [| b: (INT x:A. B x);  b: B a ==> R;  ~ a:A ==> R |] ==> R

   709

   710 \tdx{UnionI}   [| X:C;  A:X |] ==> A : Union C

   711 \tdx{UnionE}   [| A : Union C;  !!X.[| A:X;  X:C |] ==> R |] ==> R

   712

   713 \tdx{InterI}   [| !!X. X:C ==> A:X |] ==> A : Inter C

   714 \tdx{InterD}   [| A : Inter C;  X:C |] ==> A:X

   715 \tdx{InterE}   [| A : Inter C;  A:X ==> R;  ~ X:C ==> R |] ==> R

   716

   717 \tdx{PowI}     A<=B ==> A: Pow B

   718 \tdx{PowD}     A: Pow B ==> A<=B

   719

   720 \tdx{imageI}   [| x:A |] ==> f x : fA

   721 \tdx{imageE}   [| b : fA;  !!x.[| b=f x;  x:A |] ==> P |] ==> P

   722

   723 \tdx{rangeI}   f x : range f

   724 \tdx{rangeE}   [| b : range f;  !!x.[| b=f x |] ==> P |] ==> P

   725 \end{ttbox}

   726 \caption{Further derived rules for set theory} \label{hol-set2}

   727 \end{figure}

   728

   729

   730 \subsection{Axioms and rules of set theory}

   731 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}.  The

   732 axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert

   733 that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms.  Of

   734 course, \hbox{\tt op :} also serves as the membership relation.

   735

   736 All the other axioms are definitions.  They include the empty set, bounded

   737 quantifiers, unions, intersections, complements and the subset relation.

   738 They also include straightforward constructions on functions: image~({\tt})

   739 and \texttt{range}.

   740

   741 %The predicate \cdx{inj_on} is used for simulating type definitions.

   742 %The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the

   743 %set~$A$, which specifies a subset of its domain type.  In a type

   744 %definition, $f$ is the abstraction function and $A$ is the set of valid

   745 %representations; we should not expect $f$ to be injective outside of~$A$.

   746

   747 %\begin{figure} \underscoreon

   748 %\begin{ttbox}

   749 %\tdx{Inv_f_f}    inj f ==> Inv f (f x) = x

   750 %\tdx{f_Inv_f}    y : range f ==> f(Inv f y) = y

   751 %

   752 %\tdx{Inv_injective}

   753 %    [| Inv f x=Inv f y; x: range f;  y: range f |] ==> x=y

   754 %

   755 %

   756 %\tdx{monoI}      [| !!A B. A <= B ==> f A <= f B |] ==> mono f

   757 %\tdx{monoD}      [| mono f;  A <= B |] ==> f A <= f B

   758 %

   759 %\tdx{injI}       [| !! x y. f x = f y ==> x=y |] ==> inj f

   760 %\tdx{inj_inverseI}              (!!x. g(f x) = x) ==> inj f

   761 %\tdx{injD}       [| inj f; f x = f y |] ==> x=y

   762 %

   763 %\tdx{inj_onI}  (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A

   764 %\tdx{inj_onD}  [| inj_on f A;  f x=f y;  x:A;  y:A |] ==> x=y

   765 %

   766 %\tdx{inj_on_inverseI}

   767 %    (!!x. x:A ==> g(f x) = x) ==> inj_on f A

   768 %\tdx{inj_on_contraD}

   769 %    [| inj_on f A;  x~=y;  x:A;  y:A |] ==> ~ f x=f y

   770 %\end{ttbox}

   771 %\caption{Derived rules involving functions} \label{hol-fun}

   772 %\end{figure}

   773

   774

   775 \begin{figure} \underscoreon

   776 \begin{ttbox}

   777 \tdx{Union_upper}     B:A ==> B <= Union A

   778 \tdx{Union_least}     [| !!X. X:A ==> X<=C |] ==> Union A <= C

   779

   780 \tdx{Inter_lower}     B:A ==> Inter A <= B

   781 \tdx{Inter_greatest}  [| !!X. X:A ==> C<=X |] ==> C <= Inter A

   782

   783 \tdx{Un_upper1}       A <= A Un B

   784 \tdx{Un_upper2}       B <= A Un B

   785 \tdx{Un_least}        [| A<=C;  B<=C |] ==> A Un B <= C

   786

   787 \tdx{Int_lower1}      A Int B <= A

   788 \tdx{Int_lower2}      A Int B <= B

   789 \tdx{Int_greatest}    [| C<=A;  C<=B |] ==> C <= A Int B

   790 \end{ttbox}

   791 \caption{Derived rules involving subsets} \label{hol-subset}

   792 \end{figure}

   793

   794

   795 \begin{figure} \underscoreon   \hfuzz=4pt%suppress "Overfull \hbox" message

   796 \begin{ttbox}

   797 \tdx{Int_absorb}        A Int A = A

   798 \tdx{Int_commute}       A Int B = B Int A

   799 \tdx{Int_assoc}         (A Int B) Int C  =  A Int (B Int C)

   800 \tdx{Int_Un_distrib}    (A Un B)  Int C  =  (A Int C) Un (B Int C)

   801

   802 \tdx{Un_absorb}         A Un A = A

   803 \tdx{Un_commute}        A Un B = B Un A

   804 \tdx{Un_assoc}          (A Un B)  Un C  =  A Un (B Un C)

   805 \tdx{Un_Int_distrib}    (A Int B) Un C  =  (A Un C) Int (B Un C)

   806

   807 \tdx{Compl_disjoint}    A Int (-A) = {\ttlbrace}x. False{\ttrbrace}

   808 \tdx{Compl_partition}   A Un  (-A) = {\ttlbrace}x. True{\ttrbrace}

   809 \tdx{double_complement} -(-A) = A

   810 \tdx{Compl_Un}          -(A Un B)  = (-A) Int (-B)

   811 \tdx{Compl_Int}         -(A Int B) = (-A) Un (-B)

   812

   813 \tdx{Union_Un_distrib}  Union(A Un B) = (Union A) Un (Union B)

   814 \tdx{Int_Union}         A Int (Union B) = (UN C:B. A Int C)

   815

   816 \tdx{Inter_Un_distrib}  Inter(A Un B) = (Inter A) Int (Inter B)

   817 \tdx{Un_Inter}          A Un (Inter B) = (INT C:B. A Un C)

   818

   819 \end{ttbox}

   820 \caption{Set equalities} \label{hol-equalities}

   821 \end{figure}

   822 %\tdx{Un_Union_image}    (UN x:C.(A x) Un (B x)) = Union(AC) Un Union(BC)

   823 %\tdx{Int_Inter_image}   (INT x:C.(A x) Int (B x)) = Inter(AC) Int Inter(BC)

   824

   825 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most are

   826 obvious and resemble rules of Isabelle's ZF set theory.  Certain rules, such

   827 as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical

   828 reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are

   829 not strictly necessary but yield more natural proofs.  Similarly,

   830 \tdx{equalityCE} supports classical reasoning about extensionality, after the

   831 fashion of \tdx{iffCE}.  See the file \texttt{HOL/Set.ML} for proofs

   832 pertaining to set theory.

   833

   834 Figure~\ref{hol-subset} presents lattice properties of the subset relation.

   835 Unions form least upper bounds; non-empty intersections form greatest lower

   836 bounds.  Reasoning directly about subsets often yields clearer proofs than

   837 reasoning about the membership relation.  See the file \texttt{HOL/subset.ML}.

   838

   839 Figure~\ref{hol-equalities} presents many common set equalities.  They

   840 include commutative, associative and distributive laws involving unions,

   841 intersections and complements.  For a complete listing see the file {\tt

   842 HOL/equalities.ML}.

   843

   844 \begin{warn}

   845 \texttt{Blast_tac} proves many set-theoretic theorems automatically.

   846 Hence you seldom need to refer to the theorems above.

   847 \end{warn}

   848

   849 \begin{figure}

   850 \begin{center}

   851 \begin{tabular}{rrr}

   852   \it name      &\it meta-type  & \it description \\

   853   \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$

   854         & injective/surjective \\

   855   \cdx{inj_on}        & $[\alpha\To\beta ,\alpha\,set]\To bool$

   856         & injective over subset\\

   857   \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function

   858 \end{tabular}

   859 \end{center}

   860

   861 \underscoreon

   862 \begin{ttbox}

   863 \tdx{inj_def}         inj f      == ! x y. f x=f y --> x=y

   864 \tdx{surj_def}        surj f     == ! y. ? x. y=f x

   865 \tdx{inj_on_def}      inj_on f A == !x:A. !y:A. f x=f y --> x=y

   866 \tdx{inv_def}         inv f      == (\%y. @x. f(x)=y)

   867 \end{ttbox}

   868 \caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}

   869 \end{figure}

   870

   871 \subsection{Properties of functions}\nopagebreak

   872 Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions.

   873 Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse

   874 of~$f$.  See the file \texttt{HOL/Fun.ML} for a complete listing of the derived

   875 rules.  Reasoning about function composition (the operator~\sdx{o}) and the

   876 predicate~\cdx{surj} is done simply by expanding the definitions.

   877

   878 There is also a large collection of monotonicity theorems for constructions

   879 on sets in the file \texttt{HOL/mono.ML}.

   880

   881

   882 \section{Simplification and substitution}

   883

   884 Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset

   885 (\texttt{simpset()}), which works for most purposes.  A quite minimal

   886 simplification set for higher-order logic is~\ttindexbold{HOL_ss};

   887 even more frugal is \ttindexbold{HOL_basic_ss}.  Equality~($=$), which

   888 also expresses logical equivalence, may be used for rewriting.  See

   889 the file \texttt{HOL/simpdata.ML} for a complete listing of the basic

   890 simplification rules.

   891

   892 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%

   893 {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution

   894 and simplification.

   895

   896 \begin{warn}\index{simplification!of conjunctions}%

   897   Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous.  The

   898   left part of a conjunction helps in simplifying the right part.  This effect

   899   is not available by default: it can be slow.  It can be obtained by

   900   including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.

   901 \end{warn}

   902

   903 \begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}%

   904   By default only the condition of an \ttindex{if} is simplified but not the

   905   \texttt{then} and \texttt{else} parts. Of course the latter are simplified

   906   once the condition simplifies to \texttt{True} or \texttt{False}. To ensure

   907   full simplification of all parts of a conditional you must remove

   908   \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$.

   909 \end{warn}

   910

   911 If the simplifier cannot use a certain rewrite rule --- either because

   912 of nontermination or because its left-hand side is too flexible ---

   913 then you might try \texttt{stac}:

   914 \begin{ttdescription}

   915 \item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,

   916   replaces in subgoal $i$ instances of $lhs$ by corresponding instances of

   917   $rhs$.  In case of multiple instances of $lhs$ in subgoal $i$, backtracking

   918   may be necessary to select the desired ones.

   919

   920 If $thm$ is a conditional equality, the instantiated condition becomes an

   921 additional (first) subgoal.

   922 \end{ttdescription}

   923

   924 HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an

   925 equality throughout a subgoal and its hypotheses.  This tactic uses HOL's

   926 general substitution rule.

   927

   928 \subsection{Case splitting}

   929 \label{subsec:HOL:case:splitting}

   930

   931 HOL also provides convenient means for case splitting during rewriting. Goals

   932 containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots}

   933 often require a case distinction on $b$. This is expressed by the theorem

   934 \tdx{split_if}:

   935 $$  936 \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~   937 ((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y})))   938 \eqno{(*)}   939$$

   940 For example, a simple instance of $(*)$ is

   941 $  942 x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~   943 ((x \in A \to x \in A) \land (x \notin A \to x \in \{x\}))   944$

   945 Because $(*)$ is too general as a rewrite rule for the simplifier (the

   946 left-hand side is not a higher-order pattern in the sense of

   947 \iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}%

   948 {Chap.\ts\ref{chap:simplification}}), there is a special infix function

   949 \ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset}

   950 (analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a

   951 simpset, as in

   952 \begin{ttbox}

   953 by(simp_tac (simpset() addsplits [split_if]) 1);

   954 \end{ttbox}

   955 The effect is that after each round of simplification, one occurrence of

   956 \texttt{if} is split acording to \texttt{split_if}, until all occurences of

   957 \texttt{if} have been eliminated.

   958

   959 It turns out that using \texttt{split_if} is almost always the right thing to

   960 do. Hence \texttt{split_if} is already included in the default simpset. If

   961 you want to delete it from a simpset, use \ttindexbold{delsplits}, which is

   962 the inverse of \texttt{addsplits}:

   963 \begin{ttbox}

   964 by(simp_tac (simpset() delsplits [split_if]) 1);

   965 \end{ttbox}

   966

   967 In general, \texttt{addsplits} accepts rules of the form

   968 $  969 \Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs   970$

   971 where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the

   972 right form because internally the left-hand side is

   973 $\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples

   974 are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list}

   975 and~{\S}\ref{subsec:datatype:basics}).

   976

   977 Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also

   978 imperative versions of \texttt{addsplits} and \texttt{delsplits}

   979 \begin{ttbox}

   980 \ttindexbold{Addsplits}: thm list -> unit

   981 \ttindexbold{Delsplits}: thm list -> unit

   982 \end{ttbox}

   983 for adding splitting rules to, and deleting them from the current simpset.

   984

   985

   986 \section{Types}\label{sec:HOL:Types}

   987 This section describes HOL's basic predefined types ($\alpha \times \beta$,

   988 $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new

   989 types in general.  The most important type construction, the

   990 \texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}.

   991

   992

   993 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}

   994 \label{subsec:prod-sum}

   995

   996 \begin{figure}[htbp]

   997 \begin{constants}

   998   \it symbol    & \it meta-type &           & \it description \\

   999   \cdx{Pair}    & $[\alpha,\beta]\To \alpha\times\beta$

  1000         & & ordered pairs $(a,b)$ \\

  1001   \cdx{fst}     & $\alpha\times\beta \To \alpha$        & & first projection\\

  1002   \cdx{snd}     & $\alpha\times\beta \To \beta$         & & second projection\\

  1003   \cdx{split}   & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$

  1004         & & generalized projection\\

  1005   \cdx{Sigma}  &

  1006         $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &

  1007         & general sum of sets

  1008 \end{constants}

  1009 %\tdx{fst_def}      fst p     == @a. ? b. p = (a,b)

  1010 %\tdx{snd_def}      snd p     == @b. ? a. p = (a,b)

  1011 %\tdx{split_def}    split c p == c (fst p) (snd p)

  1012 \begin{ttbox}\makeatletter

  1013 \tdx{Sigma_def}    Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}

  1014

  1015 \tdx{Pair_eq}      ((a,b) = (a',b')) = (a=a' & b=b')

  1016 \tdx{Pair_inject}  [| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R

  1017 \tdx{PairE}        [| !!x y. p = (x,y) ==> Q |] ==> Q

  1018

  1019 \tdx{fst_conv}     fst (a,b) = a

  1020 \tdx{snd_conv}     snd (a,b) = b

  1021 \tdx{surjective_pairing}  p = (fst p,snd p)

  1022

  1023 \tdx{split}        split c (a,b) = c a b

  1024 \tdx{split_split}  R(split c p) = (! x y. p = (x,y) --> R(c x y))

  1025

  1026 \tdx{SigmaI}    [| a:A;  b:B a |] ==> (a,b) : Sigma A B

  1027

  1028 \tdx{SigmaE}    [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P

  1029           |] ==> P

  1030 \end{ttbox}

  1031 \caption{Type $\alpha\times\beta$}\label{hol-prod}

  1032 \end{figure}

  1033

  1034 Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type

  1035 $\alpha\times\beta$, with the ordered pair syntax $(a, b)$.  General

  1036 tuples are simulated by pairs nested to the right:

  1037 \begin{center}

  1038 \begin{tabular}{c|c}

  1039 external & internal \\

  1040 \hline

  1041 $\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\

  1042 \hline

  1043 $(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\

  1044 \end{tabular}

  1045 \end{center}

  1046 In addition, it is possible to use tuples

  1047 as patterns in abstractions:

  1048 \begin{center}

  1049 {\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)}

  1050 \end{center}

  1051 Nested patterns are also supported.  They are translated stepwise:

  1052 \begin{eqnarray*}

  1053 \hbox{\tt\%($x$,$y$,$z$).\ $t$}

  1054    & \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\

  1055    & \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\

  1056    & \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))}

  1057 \end{eqnarray*}

  1058 The reverse translation is performed upon printing.

  1059 \begin{warn}

  1060   The translation between patterns and \texttt{split} is performed automatically

  1061   by the parser and printer.  Thus the internal and external form of a term

  1062   may differ, which can affects proofs.  For example the term {\tt

  1063   (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the

  1064   default simpset) to rewrite to {\tt(b,a)}.

  1065 \end{warn}

  1066 In addition to explicit $\lambda$-abstractions, patterns can be used in any

  1067 variable binding construct which is internally described by a

  1068 $\lambda$-abstraction.  Some important examples are

  1069 \begin{description}

  1070 \item[Let:] \texttt{let {\it pattern} = $t$ in $u$}

  1071 \item[Quantifiers:] \texttt{ALL~{\it pattern}:$A$.~$P$}

  1072 \item[Choice:] {\underscoreon \tt SOME~{\it pattern}.~$P$}

  1073 \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}

  1074 \item[Sets:] \texttt{{\ttlbrace}{\it pattern}.~$P${\ttrbrace}}

  1075 \end{description}

  1076

  1077 There is a simple tactic which supports reasoning about patterns:

  1078 \begin{ttdescription}

  1079 \item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all

  1080   {\tt!!}-quantified variables of product type by individual variables for

  1081   each component.  A simple example:

  1082 \begin{ttbox}

  1083 {\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p}

  1084 by(split_all_tac 1);

  1085 {\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)}

  1086 \end{ttbox}

  1087 \end{ttdescription}

  1088

  1089 Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit}

  1090 which contains only a single element named {\tt()} with the property

  1091 \begin{ttbox}

  1092 \tdx{unit_eq}       u = ()

  1093 \end{ttbox}

  1094 \bigskip

  1095

  1096 Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$

  1097 which associates to the right and has a lower priority than $*$: $\tau@1 +   1098 \tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.

  1099

  1100 The definition of products and sums in terms of existing types is not

  1101 shown.  The constructions are fairly standard and can be found in the

  1102 respective theory files. Although the sum and product types are

  1103 constructed manually for foundational reasons, they are represented as

  1104 actual datatypes later.

  1105

  1106 \begin{figure}

  1107 \begin{constants}

  1108   \it symbol    & \it meta-type &           & \it description \\

  1109   \cdx{Inl}     & $\alpha \To \alpha+\beta$    & & first injection\\

  1110   \cdx{Inr}     & $\beta \To \alpha+\beta$     & & second injection\\

  1111   \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$

  1112         & & conditional

  1113 \end{constants}

  1114 \begin{ttbox}\makeatletter

  1115 \tdx{Inl_not_Inr}    Inl a ~= Inr b

  1116

  1117 \tdx{inj_Inl}        inj Inl

  1118 \tdx{inj_Inr}        inj Inr

  1119

  1120 \tdx{sumE}           [| !!x. P(Inl x);  !!y. P(Inr y) |] ==> P s

  1121

  1122 \tdx{sum_case_Inl}   sum_case f g (Inl x) = f x

  1123 \tdx{sum_case_Inr}   sum_case f g (Inr x) = g x

  1124

  1125 \tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s

  1126 \tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &

  1127                                      (! y. s = Inr(y) --> R(g(y))))

  1128 \end{ttbox}

  1129 \caption{Type $\alpha+\beta$}\label{hol-sum}

  1130 \end{figure}

  1131

  1132 \begin{figure}

  1133 \index{*"< symbol}

  1134 \index{*"* symbol}

  1135 \index{*div symbol}

  1136 \index{*mod symbol}

  1137 \index{*dvd symbol}

  1138 \index{*"+ symbol}

  1139 \index{*"- symbol}

  1140 \begin{constants}

  1141   \it symbol    & \it meta-type & \it priority & \it description \\

  1142   \cdx{0}       & $\alpha$  & & zero \\

  1143   \cdx{Suc}     & $nat \To nat$ & & successor function\\

  1144   \tt *    & $[\alpha,\alpha]\To \alpha$    &  Left 70 & multiplication \\

  1145   \tt div  & $[\alpha,\alpha]\To \alpha$    &  Left 70 & division\\

  1146   \tt mod  & $[\alpha,\alpha]\To \alpha$    &  Left 70 & modulus\\

  1147   \tt dvd  & $[\alpha,\alpha]\To bool$     &  Left 70 & divides'' relation\\

  1148   \tt +    & $[\alpha,\alpha]\To \alpha$    &  Left 65 & addition\\

  1149   \tt -    & $[\alpha,\alpha]\To \alpha$    &  Left 65 & subtraction

  1150 \end{constants}

  1151 \subcaption{Constants and infixes}

  1152

  1153 \begin{ttbox}\makeatother

  1154 \tdx{nat_induct}     [| P 0; !!n. P n ==> P(Suc n) |]  ==> P n

  1155

  1156 \tdx{Suc_not_Zero}   Suc m ~= 0

  1157 \tdx{inj_Suc}        inj Suc

  1158 \tdx{n_not_Suc_n}    n~=Suc n

  1159 \subcaption{Basic properties}

  1160 \end{ttbox}

  1161 \caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1}

  1162 \end{figure}

  1163

  1164

  1165 \begin{figure}

  1166 \begin{ttbox}\makeatother

  1167               0+n           = n

  1168               (Suc m)+n     = Suc(m+n)

  1169

  1170               m-0           = m

  1171               0-n           = n

  1172               Suc(m)-Suc(n) = m-n

  1173

  1174               0*n           = 0

  1175               Suc(m)*n      = n + m*n

  1176

  1177 \tdx{mod_less}      m<n ==> m mod n = m

  1178 \tdx{mod_geq}       [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n

  1179

  1180 \tdx{div_less}      m<n ==> m div n = 0

  1181 \tdx{div_geq}       [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)

  1182 \end{ttbox}

  1183 \caption{Recursion equations for the arithmetic operators} \label{hol-nat2}

  1184 \end{figure}

  1185

  1186 \subsection{The type of natural numbers, \textit{nat}}

  1187 \index{nat@{\textit{nat}} type|(}

  1188

  1189 The theory \thydx{Nat} defines the natural numbers in a roundabout but

  1190 traditional way.  The axiom of infinity postulates a type~\tydx{ind} of

  1191 individuals, which is non-empty and closed under an injective operation.  The

  1192 natural numbers are inductively generated by choosing an arbitrary individual

  1193 for~0 and using the injective operation to take successors.  This is a least

  1194 fixedpoint construction.

  1195

  1196 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded

  1197 functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min},

  1198 \cdx{max} and \cdx{LEAST}) available on \tydx{nat}.  Theory \thydx{Nat}

  1199 also shows that {\tt<=} is a linear order, so \tydx{nat} is

  1200 also an instance of class \cldx{linorder}.

  1201

  1202 Theory \thydx{NatArith} develops arithmetic on the natural numbers.  It defines

  1203 addition, multiplication and subtraction.  Theory \thydx{Divides} defines

  1204 division, remainder and the divides'' relation.  The numerous theorems

  1205 proved include commutative, associative, distributive, identity and

  1206 cancellation laws.  See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}.  The

  1207 recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on

  1208 \texttt{nat} are part of the default simpset.

  1209

  1210 Functions on \tydx{nat} can be defined by primitive or well-founded recursion;

  1211 see {\S}\ref{sec:HOL:recursive}.  A simple example is addition.

  1212 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following

  1213 the standard convention.

  1214 \begin{ttbox}

  1215 \sdx{primrec}

  1216       "0 + n = n"

  1217   "Suc m + n = Suc (m + n)"

  1218 \end{ttbox}

  1219 There is also a \sdx{case}-construct

  1220 of the form

  1221 \begin{ttbox}

  1222 case $$e$$ of 0 => $$a$$ | Suc $$m$$ => $$b$$

  1223 \end{ttbox}

  1224 Note that Isabelle insists on precisely this format; you may not even change

  1225 the order of the two cases.

  1226 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator

  1227 \cdx{nat_rec}, which is available because \textit{nat} is represented as

  1228 a datatype.

  1229

  1230 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.

  1231 %Recursion along this relation resembles primitive recursion, but is

  1232 %stronger because we are in higher-order logic; using primitive recursion to

  1233 %define a higher-order function, we can easily Ackermann's function, which

  1234 %is not primitive recursive \cite[page~104]{thompson91}.

  1235 %The transitive closure of \cdx{pred_nat} is~$<$.  Many functions on the

  1236 %natural numbers are most easily expressed using recursion along~$<$.

  1237

  1238 Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$

  1239 in subgoal~$i$ using theorem \texttt{nat_induct}.  There is also the derived

  1240 theorem \tdx{less_induct}:

  1241 \begin{ttbox}

  1242 [| !!n. [| ! m. m<n --> P m |] ==> P n |]  ==>  P n

  1243 \end{ttbox}

  1244

  1245

  1246 \subsection{Numerical types and numerical reasoning}

  1247

  1248 The integers (type \tdx{int}) are also available in HOL, and the reals (type

  1249 \tdx{real}) are available in the logic image \texttt{HOL-Complex}.  They support

  1250 the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and

  1251 multiplication (\texttt{*}), and much else.  Type \tdx{int} provides the

  1252 \texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real

  1253 division and other operations.  Both types belong to class \cldx{linorder}, so

  1254 they inherit the relational operators and all the usual properties of linear

  1255 orderings.  For full details, please survey the theories in subdirectories

  1256 \texttt{Integ}, \texttt{Real}, and \texttt{Complex}.

  1257

  1258 All three numeric types admit numerals of the form \texttt{$sd\ldots d$},

  1259 where $s$ is an optional minus sign and $d\ldots d$ is a string of digits.

  1260 Numerals are represented internally by a datatype for binary notation, which

  1261 allows numerical calculations to be performed by rewriting.  For example, the

  1262 integer division of \texttt{54342339} by \texttt{3452} takes about five

  1263 seconds.  By default, the simplifier cancels like terms on the opposite sites

  1264 of relational operators (reducing \texttt{z+x<x+y} to \texttt{z<y}, for

  1265 instance.  The simplifier also collects like terms, replacing \texttt{x+y+x*3}

  1266 by \texttt{4*x+y}.

  1267

  1268 Sometimes numerals are not wanted, because for example \texttt{n+3} does not

  1269 match a pattern of the form \texttt{Suc $k$}.  You can re-arrange the form of

  1270 an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such as

  1271 \texttt{n+3 = Suc (Suc (Suc n))}.  As an alternative, you can disable the

  1272 fancier simplifications by using a basic simpset such as \texttt{HOL_ss}

  1273 rather than the default one, \texttt{simpset()}.

  1274

  1275 Reasoning about arithmetic inequalities can be tedious.  Fortunately, HOL

  1276 provides a decision procedure for \emph{linear arithmetic}: formulae involving

  1277 addition and subtraction. The simplifier invokes a weak version of this

  1278 decision procedure automatically. If this is not sufficent, you can invoke the

  1279 full procedure \ttindex{Lin_Arith.tac} explicitly.  It copes with arbitrary

  1280 formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt

  1281   min}, {\tt max} and numerical constants. Other subterms are treated as

  1282 atomic, while subformulae not involving numerical types are ignored. Quantified

  1283 subformulae are ignored unless they are positive universal or negative

  1284 existential. The running time is exponential in the number of

  1285 occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case

  1286 distinctions.

  1287 If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and

  1288 {\tt k dvd} are also supported. The former two are eliminated

  1289 by case distinctions, again blowing up the running time.

  1290 If the formula involves explicit quantifiers, \texttt{Lin_Arith.tac} may take

  1291 super-exponential time and space.

  1292

  1293 If \texttt{Lin_Arith.tac} fails, try to find relevant arithmetic results in

  1294 the library.  The theories \texttt{Nat} and \texttt{NatArith} contain

  1295 theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.

  1296 Theory \texttt{Divides} contains theorems about \texttt{div} and

  1297 \texttt{mod}.  Use Proof General's \emph{find} button (or other search

  1298 facilities) to locate them.

  1299

  1300 \index{nat@{\textit{nat}} type|)}

  1301

  1302

  1303 \begin{figure}

  1304 \index{#@{\tt[]} symbol}

  1305 \index{#@{\tt\#} symbol}

  1306 \index{"@@{\tt\at} symbol}

  1307 \index{*"! symbol}

  1308 \begin{constants}

  1309   \it symbol & \it meta-type & \it priority & \it description \\

  1310   \tt[]    & $\alpha\,list$ & & empty list\\

  1311   \tt \#   & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 &

  1312         list constructor \\

  1313   \cdx{null}    & $\alpha\,list \To bool$ & & emptiness test\\

  1314   \cdx{hd}      & $\alpha\,list \To \alpha$ & & head \\

  1315   \cdx{tl}      & $\alpha\,list \To \alpha\,list$ & & tail \\

  1316   \cdx{last}    & $\alpha\,list \To \alpha$ & & last element \\

  1317   \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\

  1318   \tt\at  & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\

  1319   \cdx{map}     & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$

  1320         & & apply to all\\

  1321   \cdx{filter}  & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$

  1322         & & filter functional\\

  1323   \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\

  1324   \sdx{mem}  & $\alpha \To \alpha\,list \To bool$  &  Left 55   & membership\\

  1325   \cdx{foldl}   & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &

  1326   & iteration \\

  1327   \cdx{concat}   & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\

  1328   \cdx{rev}     & $\alpha\,list \To \alpha\,list$ & & reverse \\

  1329   \cdx{length}  & $\alpha\,list \To nat$ & & length \\

  1330   \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\

  1331   \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&

  1332     take/drop a prefix \\

  1333   \cdx{takeWhile},\\

  1334   \cdx{dropWhile} &

  1335     $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ &&

  1336     take/drop a prefix

  1337 \end{constants}

  1338 \subcaption{Constants and infixes}

  1339

  1340 \begin{center} \tt\frenchspacing

  1341 \begin{tabular}{rrr}

  1342   \it external        & \it internal  & \it description \\{}

  1343   [$x@1$, $\dots$, $x@n$]  &  $x@1$ \# $\cdots$ \# $x@n$ \# [] &

  1344         \rm finite list \\{}

  1345   [$x$:$l$. $P$]  & filter ($\lambda x{.}P$) $l$ &

  1346         \rm list comprehension

  1347 \end{tabular}

  1348 \end{center}

  1349 \subcaption{Translations}

  1350 \caption{The theory \thydx{List}} \label{hol-list}

  1351 \end{figure}

  1352

  1353

  1354 \begin{figure}

  1355 \begin{ttbox}\makeatother

  1356 null [] = True

  1357 null (x#xs) = False

  1358

  1359 hd (x#xs) = x

  1360

  1361 tl (x#xs) = xs

  1362 tl [] = []

  1363

  1364 [] @ ys = ys

  1365 (x#xs) @ ys = x # xs @ ys

  1366

  1367 set [] = \ttlbrace\ttrbrace

  1368 set (x#xs) = insert x (set xs)

  1369

  1370 x mem [] = False

  1371 x mem (y#ys) = (if y=x then True else x mem ys)

  1372

  1373 concat([]) = []

  1374 concat(x#xs) = x @ concat(xs)

  1375

  1376 rev([]) = []

  1377 rev(x#xs) = rev(xs) @ [x]

  1378

  1379 length([]) = 0

  1380 length(x#xs) = Suc(length(xs))

  1381

  1382 xs!0 = hd xs

  1383 xs!(Suc n) = (tl xs)!n

  1384 \end{ttbox}

  1385 \caption{Simple list processing functions}

  1386 \label{fig:HOL:list-simps}

  1387 \end{figure}

  1388

  1389 \begin{figure}

  1390 \begin{ttbox}\makeatother

  1391 map f [] = []

  1392 map f (x#xs) = f x # map f xs

  1393

  1394 filter P [] = []

  1395 filter P (x#xs) = (if P x then x#filter P xs else filter P xs)

  1396

  1397 foldl f a [] = a

  1398 foldl f a (x#xs) = foldl f (f a x) xs

  1399

  1400 take n [] = []

  1401 take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)

  1402

  1403 drop n [] = []

  1404 drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)

  1405

  1406 takeWhile P [] = []

  1407 takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])

  1408

  1409 dropWhile P [] = []

  1410 dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)

  1411 \end{ttbox}

  1412 \caption{Further list processing functions}

  1413 \label{fig:HOL:list-simps2}

  1414 \end{figure}

  1415

  1416

  1417 \subsection{The type constructor for lists, \textit{list}}

  1418 \label{subsec:list}

  1419 \index{list@{\textit{list}} type|(}

  1420

  1421 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list

  1422 operations with their types and syntax.  Type $\alpha \; list$ is

  1423 defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}.

  1424 As a result the generic structural induction and case analysis tactics

  1425 \texttt{induct\_tac} and \texttt{cases\_tac} also become available for

  1426 lists.  A \sdx{case} construct of the form

  1427 \begin{center}\tt

  1428 case $e$ of [] => $a$  |  $$x$$\#$$xs$$ => b

  1429 \end{center}

  1430 is defined by translation.  For details see~{\S}\ref{sec:HOL:datatype}. There

  1431 is also a case splitting rule \tdx{split_list_case}

  1432 $  1433 \begin{array}{l}   1434 P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~   1435 x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\   1436 ((e = \texttt{[]} \to P(a)) \land   1437 (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs)))   1438 \end{array}   1439$

  1440 which can be fed to \ttindex{addsplits} just like

  1441 \texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).

  1442

  1443 \texttt{List} provides a basic library of list processing functions defined by

  1444 primitive recursion.  The recursion equations

  1445 are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}.

  1446

  1447 \index{list@{\textit{list}} type|)}

  1448

  1449

  1450 \section{Datatype definitions}

  1451 \label{sec:HOL:datatype}

  1452 \index{*datatype|(}

  1453

  1454 Inductive datatypes, similar to those of \ML, frequently appear in

  1455 applications of Isabelle/HOL.  In principle, such types could be defined by

  1456 hand via \texttt{typedef}, but this would be far too

  1457 tedious.  The \ttindex{datatype} definition package of Isabelle/HOL (cf.\

  1458 \cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores.  It generates an

  1459 appropriate \texttt{typedef} based on a least fixed-point construction, and

  1460 proves freeness theorems and induction rules, as well as theorems for

  1461 recursion and case combinators.  The user just has to give a simple

  1462 specification of new inductive types using a notation similar to {\ML} or

  1463 Haskell.

  1464

  1465 The current datatype package can handle both mutual and indirect recursion.

  1466 It also offers to represent existing types as datatypes giving the advantage

  1467 of a more uniform view on standard theories.

  1468

  1469

  1470 \subsection{Basics}

  1471 \label{subsec:datatype:basics}

  1472

  1473 A general \texttt{datatype} definition is of the following form:

  1474 $  1475 \begin{array}{llcl}   1476 \mathtt{datatype} & (\vec{\alpha})t@1 & = &   1477 C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~   1478 C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\   1479 & & \vdots \\   1480 \mathtt{and} & (\vec{\alpha})t@n & = &   1481 C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~   1482 C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}}   1483 \end{array}   1484$

  1485 where $\vec{\alpha} = (\alpha@1,\ldots,\alpha@h)$ is a list of type variables,

  1486 $C^j@i$ are distinct constructor names and $\tau^j@{i,i'}$ are {\em

  1487   admissible} types containing at most the type variables $\alpha@1, \ldots,   1488 \alpha@h$. A type $\tau$ occurring in a \texttt{datatype} definition is {\em

  1489   admissible} if and only if

  1490 \begin{itemize}

  1491 \item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the

  1492 newly defined type constructors $t@1,\ldots,t@n$, or

  1493 \item $\tau = (\vec{\alpha})t@{j'}$ where $1 \leq j' \leq n$, or

  1494 \item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is

  1495 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$

  1496 are admissible types.

  1497 \item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible

  1498 type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined

  1499 types are {\em strictly positive})

  1500 \end{itemize}

  1501 If some $(\vec{\alpha})t@{j'}$ occurs in a type $\tau^j@{i,i'}$

  1502 of the form

  1503 $  1504 (\ldots,\ldots ~ (\vec{\alpha})t@{j'} ~ \ldots,\ldots)t'   1505$

  1506 this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple

  1507 example of a datatype is the type \texttt{list}, which can be defined by

  1508 \begin{ttbox}

  1509 datatype 'a list = Nil

  1510                  | Cons 'a ('a list)

  1511 \end{ttbox}

  1512 Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled

  1513 by the mutually recursive datatype definition

  1514 \begin{ttbox}

  1515 datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)

  1516                  | Sum ('a aexp) ('a aexp)

  1517                  | Diff ('a aexp) ('a aexp)

  1518                  | Var 'a

  1519                  | Num nat

  1520 and      'a bexp = Less ('a aexp) ('a aexp)

  1521                  | And ('a bexp) ('a bexp)

  1522                  | Or ('a bexp) ('a bexp)

  1523 \end{ttbox}

  1524 The datatype \texttt{term}, which is defined by

  1525 \begin{ttbox}

  1526 datatype ('a, 'b) term = Var 'a

  1527                        | App 'b ((('a, 'b) term) list)

  1528 \end{ttbox}

  1529 is an example for a datatype with nested recursion. Using nested recursion

  1530 involving function spaces, we may also define infinitely branching datatypes, e.g.

  1531 \begin{ttbox}

  1532 datatype 'a tree = Atom 'a | Branch "nat => 'a tree"

  1533 \end{ttbox}

  1534

  1535 \medskip

  1536

  1537 Types in HOL must be non-empty. Each of the new datatypes

  1538 $(\vec{\alpha})t@j$ with $1 \leq j \leq n$ is non-empty if and only if it has a

  1539 constructor $C^j@i$ with the following property: for all argument types

  1540 $\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype

  1541 $(\vec{\alpha})t@{j'}$ is non-empty.

  1542

  1543 If there are no nested occurrences of the newly defined datatypes, obviously

  1544 at least one of the newly defined datatypes $(\vec{\alpha})t@j$

  1545 must have a constructor $C^j@i$ without recursive arguments, a \emph{base

  1546   case}, to ensure that the new types are non-empty. If there are nested

  1547 occurrences, a datatype can even be non-empty without having a base case

  1548 itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t

  1549   list)} is non-empty as well.

  1550

  1551

  1552 \subsubsection{Freeness of the constructors}

  1553

  1554 The datatype constructors are automatically defined as functions of their

  1555 respective type:

  1556 $C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j$

  1557 These functions have certain {\em freeness} properties.  They construct

  1558 distinct values:

  1559 $  1560 C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad   1561 \mbox{for all}~ i \neq i'.   1562$

  1563 The constructor functions are injective:

  1564 $  1565 (C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =   1566 (x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})   1567$

  1568 Since the number of distinctness inequalities is quadratic in the number of

  1569 constructors, the datatype package avoids proving them separately if there are

  1570 too many constructors. Instead, specific inequalities are proved by a suitable

  1571 simplification procedure on demand.\footnote{This procedure, which is already part

  1572 of the default simpset, may be referred to by the ML identifier

  1573 \texttt{DatatypePackage.distinct_simproc}.}

  1574

  1575 \subsubsection{Structural induction}

  1576

  1577 The datatype package also provides structural induction rules.  For

  1578 datatypes without nested recursion, this is of the following form:

  1579 $  1580 \infer{P@1~x@1 \land \dots \land P@n~x@n}   1581 {\begin{array}{lcl}   1582 \Forall x@1 \dots x@{m^1@1}.   1583 \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots;   1584 P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp &   1585 P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\   1586 & \vdots \\   1587 \Forall x@1 \dots x@{m^1@{k@1}}.   1588 \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots;   1589 P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp &   1590 P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\   1591 & \vdots \\   1592 \Forall x@1 \dots x@{m^n@1}.   1593 \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots;   1594 P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp &   1595 P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\   1596 & \vdots \\   1597 \Forall x@1 \dots x@{m^n@{k@n}}.   1598 \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots   1599 P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp &   1600 P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right)   1601 \end{array}}   1602$

  1603 where

  1604 $  1605 \begin{array}{rcl}   1606 Rec^j@i & := &   1607 \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,   1608 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex]   1609 && \left\{(i',i'')~\left|~   1610 1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land   1611 \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}   1612 \end{array}   1613$

  1614 i.e.\ the properties $P@j$ can be assumed for all recursive arguments.

  1615

  1616 For datatypes with nested recursion, such as the \texttt{term} example from

  1617 above, things are a bit more complicated.  Conceptually, Isabelle/HOL unfolds

  1618 a definition like

  1619 \begin{ttbox}

  1620 datatype ('a,'b) term = Var 'a

  1621                       | App 'b ((('a, 'b) term) list)

  1622 \end{ttbox}

  1623 to an equivalent definition without nesting:

  1624 \begin{ttbox}

  1625 datatype ('a,'b) term      = Var

  1626                            | App 'b (('a, 'b) term_list)

  1627 and      ('a,'b) term_list = Nil'

  1628                            | Cons' (('a,'b) term) (('a,'b) term_list)

  1629 \end{ttbox}

  1630 Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt

  1631   Nil'} and \texttt{Cons'} are not really introduced.  One can directly work with

  1632 the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing

  1633 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for

  1634 \texttt{term} gets the form

  1635 $  1636 \infer{P@1~x@1 \land P@2~x@2}   1637 {\begin{array}{l}   1638 \Forall x.~P@1~(\mathtt{Var}~x) \\   1639 \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\   1640 P@2~\mathtt{Nil} \\   1641 \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2)   1642 \end{array}}   1643$

  1644 Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term}

  1645 and one for the type \texttt{(('a, 'b) term) list}.

  1646

  1647 For a datatype with function types such as \texttt{'a tree}, the induction rule

  1648 is of the form

  1649 $  1650 \infer{P~t}   1651 {\Forall a.~P~(\mathtt{Atom}~a) &   1652 \Forall ts.~(\forall x.~P~(ts~x)) \Imp P~(\mathtt{Branch}~ts)}   1653$

  1654

  1655 \medskip In principle, inductive types are already fully determined by

  1656 freeness and structural induction.  For convenience in applications,

  1657 the following derived constructions are automatically provided for any

  1658 datatype.

  1659

  1660 \subsubsection{The \sdx{case} construct}

  1661

  1662 The type comes with an \ML-like \texttt{case}-construct:

  1663 $  1664 \begin{array}{rrcl}   1665 \mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\   1666 \vdots \\   1667 \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j}   1668 \end{array}   1669$

  1670 where the $x@{i,j}$ are either identifiers or nested tuple patterns as in

  1671 {\S}\ref{subsec:prod-sum}.

  1672 \begin{warn}

  1673   All constructors must be present, their order is fixed, and nested patterns

  1674   are not supported (with the exception of tuples).  Violating this

  1675   restriction results in strange error messages.

  1676 \end{warn}

  1677

  1678 To perform case distinction on a goal containing a \texttt{case}-construct,

  1679 the theorem $t@j.$\texttt{split} is provided:

  1680 $  1681 \begin{array}{@{}rcl@{}}   1682 P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=&   1683 \!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to   1684 P(f@1~x@1\dots x@{m^j@1})) \\   1685 &&\!\!\! ~\land~ \dots ~\land \\   1686 &&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to   1687 P(f@{k@j}~x@1\dots x@{m^j@{k@j}})))   1688 \end{array}   1689$

  1690 where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.

  1691 This theorem can be added to a simpset via \ttindex{addsplits}

  1692 (see~{\S}\ref{subsec:HOL:case:splitting}).

  1693

  1694 Case splitting on assumption works as well, by using the rule

  1695 $t@j.$\texttt{split_asm} in the same manner.  Both rules are available under

  1696 $t@j.$\texttt{splits} (this name is \emph{not} bound in ML, though).

  1697

  1698 \begin{warn}\index{simplification!of \texttt{case}}%

  1699   By default only the selector expression ($e$ above) in a

  1700   \texttt{case}-construct is simplified, in analogy with \texttt{if} (see

  1701   page~\pageref{if-simp}). Only if that reduces to a constructor is one of

  1702   the arms of the \texttt{case}-construct exposed and simplified. To ensure

  1703   full simplification of all parts of a \texttt{case}-construct for datatype

  1704   $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for

  1705   example by \texttt{delcongs [thm "$t$.weak_case_cong"]}.

  1706 \end{warn}

  1707

  1708 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}

  1709

  1710 Theory \texttt{NatArith} declares a generic function \texttt{size} of type

  1711 $\alpha\To nat$.  Each datatype defines a particular instance of \texttt{size}

  1712 by overloading according to the following scheme:

  1713 %%% FIXME: This formula is too big and is completely unreadable

  1714 $  1715 size(C^j@i~x@1~\dots~x@{m^j@i}) = \!   1716 \left\{   1717 \begin{array}{ll}   1718 0 & \!\mbox{if Rec^j@i = \emptyset} \\   1719 1+\sum\limits@{h=1}^{l^j@i}size~x@{r^j@{i,h}} &   1720 \!\mbox{if Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,   1721 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}}   1722 \end{array}   1723 \right.   1724$

  1725 where $Rec^j@i$ is defined above.  Viewing datatypes as generalised trees, the

  1726 size of a leaf is 0 and the size of a node is the sum of the sizes of its

  1727 subtrees ${}+1$.

  1728

  1729 \subsection{Defining datatypes}

  1730

  1731 The theory syntax for datatype definitions is given in the

  1732 Isabelle/Isar reference manual.  In order to be well-formed, a

  1733 datatype definition has to obey the rules stated in the previous

  1734 section.  As a result the theory is extended with the new types, the

  1735 constructors, and the theorems listed in the previous section.

  1736

  1737 Most of the theorems about datatypes become part of the default simpset and

  1738 you never need to see them again because the simplifier applies them

  1739 automatically.  Only induction or case distinction are usually invoked by hand.

  1740 \begin{ttdescription}

  1741 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$]

  1742  applies structural induction on variable $x$ to subgoal $i$, provided the

  1743  type of $x$ is a datatype.

  1744 \item[\texttt{induct_tac}

  1745   {\tt"}$x@1$ $\ldots$ $x@n${\tt"} $i$] applies simultaneous

  1746   structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$.  This

  1747   is the canonical way to prove properties of mutually recursive datatypes

  1748   such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as

  1749   \texttt{term}.

  1750 \end{ttdescription}

  1751 In some cases, induction is overkill and a case distinction over all

  1752 constructors of the datatype suffices.

  1753 \begin{ttdescription}

  1754 \item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$]

  1755  performs a case analysis for the term $u$ whose type  must be a datatype.

  1756  If the datatype has $k@j$ constructors  $C^j@1$, \dots $C^j@{k@j}$, subgoal

  1757  $i$ is replaced by $k@j$ new subgoals which  contain the additional

  1758  assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for  $i'=1$, $\dots$,~$k@j$.

  1759 \end{ttdescription}

  1760

  1761 Note that induction is only allowed on free variables that should not occur

  1762 among the premises of the subgoal. Case distinction applies to arbitrary terms.

  1763

  1764 \bigskip

  1765

  1766

  1767 For the technically minded, we exhibit some more details.  Processing the

  1768 theory file produces an \ML\ structure which, in addition to the usual

  1769 components, contains a structure named $t$ for each datatype $t$ defined in

  1770 the file.  Each structure $t$ contains the following elements:

  1771 \begin{ttbox}

  1772 val distinct : thm list

  1773 val inject : thm list

  1774 val induct : thm

  1775 val exhaust : thm

  1776 val cases : thm list

  1777 val split : thm

  1778 val split_asm : thm

  1779 val recs : thm list

  1780 val size : thm list

  1781 val simps : thm list

  1782 \end{ttbox}

  1783 \texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size}

  1784 and \texttt{split} contain the theorems

  1785 described above.  For user convenience, \texttt{distinct} contains

  1786 inequalities in both directions.  The reduction rules of the {\tt

  1787   case}-construct are in \texttt{cases}.  All theorems from {\tt

  1788   distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}.

  1789 In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct}

  1790 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.

  1791

  1792

  1793 \section{Old-style recursive function definitions}\label{sec:HOL:recursive}

  1794 \index{recursion!general|(}

  1795 \index{*recdef|(}

  1796

  1797 Old-style recursive definitions via \texttt{recdef} requires that you

  1798 supply a well-founded relation that governs the recursion.  Recursive

  1799 calls are only allowed if they make the argument decrease under the

  1800 relation.  Complicated recursion forms, such as nested recursion, can

  1801 be dealt with.  Termination can even be proved at a later time, though

  1802 having unsolved termination conditions around can make work

  1803 difficult.%

  1804 \footnote{This facility is based on Konrad Slind's TFL

  1805   package~\cite{slind-tfl}.  Thanks are due to Konrad for implementing

  1806   TFL and assisting with its installation.}

  1807

  1808 Using \texttt{recdef}, you can declare functions involving nested recursion

  1809 and pattern-matching.  Recursion need not involve datatypes and there are few

  1810 syntactic restrictions.  Termination is proved by showing that each recursive

  1811 call makes the argument smaller in a suitable sense, which you specify by

  1812 supplying a well-founded relation.

  1813

  1814 Here is a simple example, the Fibonacci function.  The first line declares

  1815 \texttt{fib} to be a constant.  The well-founded relation is simply~$<$ (on

  1816 the natural numbers).  Pattern-matching is used here: \texttt{1} is a

  1817 macro for \texttt{Suc~0}.

  1818 \begin{ttbox}

  1819 consts fib  :: "nat => nat"

  1820 recdef fib "less_than"

  1821     "fib 0 = 0"

  1822     "fib 1 = 1"

  1823     "fib (Suc(Suc x)) = (fib x + fib (Suc x))"

  1824 \end{ttbox}

  1825

  1826 With \texttt{recdef}, function definitions may be incomplete, and patterns may

  1827 overlap, as in functional programming.  The \texttt{recdef} package

  1828 disambiguates overlapping patterns by taking the order of rules into account.

  1829 For missing patterns, the function is defined to return a default value.

  1830

  1831 %For example, here is a declaration of the list function \cdx{hd}:

  1832 %\begin{ttbox}

  1833 %consts hd :: 'a list => 'a

  1834 %recdef hd "\{\}"

  1835 %    "hd (x#l) = x"

  1836 %\end{ttbox}

  1837 %Because this function is not recursive, we may supply the empty well-founded

  1838 %relation, $\{\}$.

  1839

  1840 The well-founded relation defines a notion of smaller'' for the function's

  1841 argument type.  The relation $\prec$ is \textbf{well-founded} provided it

  1842 admits no infinitely decreasing chains

  1843 $\cdots\prec x@n\prec\cdots\prec x@1.$

  1844 If the function's argument has type~$\tau$, then $\prec$ has to be a relation

  1845 over~$\tau$: it must have type $(\tau\times\tau)set$.

  1846

  1847 Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection

  1848 of operators for building well-founded relations.  The package recognises

  1849 these operators and automatically proves that the constructed relation is

  1850 well-founded.  Here are those operators, in order of importance:

  1851 \begin{itemize}

  1852 \item \texttt{less_than} is less than'' on the natural numbers.

  1853   (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$.

  1854

  1855 \item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the

  1856   relation~$\prec$ on type~$\tau$ such that $x\prec y$ if and only if

  1857   $f(x)<f(y)$.

  1858   Typically, $f$ takes the recursive function's arguments (as a tuple) and

  1859   returns a result expressed in terms of the function \texttt{size}.  It is

  1860   called a \textbf{measure function}.  Recall that \texttt{size} is overloaded

  1861   and is defined on all datatypes (see {\S}\ref{sec:HOL:size}).

  1862

  1863 \item $\mathop{\mathtt{inv_image}} R\;f$ is a generalisation of

  1864   \texttt{measure}.  It specifies a relation such that $x\prec y$ if and only

  1865   if $f(x)$

  1866   is less than $f(y)$ according to~$R$, which must itself be a well-founded

  1867   relation.

  1868

  1869 \item $R@1\texttt{<*lex*>}R@2$ is the lexicographic product of two relations.

  1870   It

  1871   is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ if and only

  1872   if $x@1$

  1873   is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$

  1874   is less than $y@2$ according to~$R@2$.

  1875

  1876 \item \texttt{finite_psubset} is the proper subset relation on finite sets.

  1877 \end{itemize}

  1878

  1879 We can use \texttt{measure} to declare Euclid's algorithm for the greatest

  1880 common divisor.  The measure function, $\lambda(m,n). n$, specifies that the

  1881 recursion terminates because argument~$n$ decreases.

  1882 \begin{ttbox}

  1883 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"

  1884     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"

  1885 \end{ttbox}

  1886

  1887 The general form of a well-founded recursive definition is

  1888 \begin{ttbox}

  1889 recdef {\it function} {\it rel}

  1890     congs   {\it congruence rules}      {\bf(optional)}

  1891     simpset {\it simplification set}      {\bf(optional)}

  1892    {\it reduction rules}

  1893 \end{ttbox}

  1894 where

  1895 \begin{itemize}

  1896 \item \textit{function} is the name of the function, either as an \textit{id}

  1897   or a \textit{string}.

  1898

  1899 \item \textit{rel} is a HOL expression for the well-founded termination

  1900   relation.

  1901

  1902 \item \textit{congruence rules} are required only in highly exceptional

  1903   circumstances.

  1904

  1905 \item The \textit{simplification set} is used to prove that the supplied

  1906   relation is well-founded.  It is also used to prove the \textbf{termination

  1907     conditions}: assertions that arguments of recursive calls decrease under

  1908   \textit{rel}.  By default, simplification uses \texttt{simpset()}, which

  1909   is sufficient to prove well-foundedness for the built-in relations listed

  1910   above.

  1911

  1912 \item \textit{reduction rules} specify one or more recursion equations.  Each

  1913   left-hand side must have the form $f\,t$, where $f$ is the function and $t$

  1914   is a tuple of distinct variables.  If more than one equation is present then

  1915   $f$ is defined by pattern-matching on components of its argument whose type

  1916   is a \texttt{datatype}.

  1917

  1918   The \ML\ identifier $f$\texttt{.simps} contains the reduction rules as

  1919   a list of theorems.

  1920 \end{itemize}

  1921

  1922 With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to

  1923 prove one termination condition.  It remains as a precondition of the

  1924 recursion theorems:

  1925 \begin{ttbox}

  1926 gcd.simps;

  1927 {\out ["! m n. n ~= 0 --> m mod n < n}

  1928 {\out   ==> gcd (?m,?n) = (if ?n=0 then ?m else gcd (?n, ?m mod ?n))"] }

  1929 {\out : thm list}

  1930 \end{ttbox}

  1931 The theory \texttt{HOL/ex/Primes} illustrates how to prove termination

  1932 conditions afterwards.  The function \texttt{Tfl.tgoalw} is like the standard

  1933 function \texttt{goalw}, which sets up a goal to prove, but its argument

  1934 should be the identifier $f$\texttt{.simps} and its effect is to set up a

  1935 proof of the termination conditions:

  1936 \begin{ttbox}

  1937 Tfl.tgoalw thy [] gcd.simps;

  1938 {\out Level 0}

  1939 {\out ! m n. n ~= 0 --> m mod n < n}

  1940 {\out  1. ! m n. n ~= 0 --> m mod n < n}

  1941 \end{ttbox}

  1942 This subgoal has a one-step proof using \texttt{simp_tac}.  Once the theorem

  1943 is proved, it can be used to eliminate the termination conditions from

  1944 elements of \texttt{gcd.simps}.  Theory \texttt{HOL/Subst/Unify} is a much

  1945 more complicated example of this process, where the termination conditions can

  1946 only be proved by complicated reasoning involving the recursive function

  1947 itself.

  1948

  1949 Isabelle/HOL can prove the \texttt{gcd} function's termination condition

  1950 automatically if supplied with the right simpset.

  1951 \begin{ttbox}

  1952 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"

  1953   simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]"

  1954     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"

  1955 \end{ttbox}

  1956

  1957 If all termination conditions were proved automatically, $f$\texttt{.simps}

  1958 is added to the simpset automatically, just as in \texttt{primrec}.

  1959 The simplification rules corresponding to clause $i$ (where counting starts

  1960 at 0) are called $f$\texttt{.}$i$ and can be accessed as \texttt{thms

  1961   "$f$.$i$"},

  1962 which returns a list of theorems. Thus you can, for example, remove specific

  1963 clauses from the simpset. Note that a single clause may give rise to a set of

  1964 simplification rules in order to capture the fact that if clauses overlap,

  1965 their order disambiguates them.

  1966

  1967 A \texttt{recdef} definition also returns an induction rule specialised for

  1968 the recursive function.  For the \texttt{gcd} function above, the induction

  1969 rule is

  1970 \begin{ttbox}

  1971 gcd.induct;

  1972 {\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm}

  1973 \end{ttbox}

  1974 This rule should be used to reason inductively about the \texttt{gcd}

  1975 function.  It usually makes the induction hypothesis available at all

  1976 recursive calls, leading to very direct proofs.  If any termination conditions

  1977 remain unproved, they will become additional premises of this rule.

  1978

  1979 \index{recursion!general|)}

  1980 \index{*recdef|)}

  1981

  1982

  1983 \section{Example: Cantor's Theorem}\label{sec:hol-cantor}

  1984 Cantor's Theorem states that every set has more subsets than it has

  1985 elements.  It has become a favourite example in higher-order logic since

  1986 it is so easily expressed:

  1987 $\forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool.   1988 \forall x::\alpha. f~x \not= S   1989$

  1990 %

  1991 Viewing types as sets, $\alpha\To bool$ represents the powerset

  1992 of~$\alpha$.  This version states that for every function from $\alpha$ to

  1993 its powerset, some subset is outside its range.

  1994

  1995 The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and

  1996 the operator \cdx{range}.

  1997 \begin{ttbox}

  1998 context Set.thy;

  1999 \end{ttbox}

  2000 The set~$S$ is given as an unknown instead of a

  2001 quantified variable so that we may inspect the subset found by the proof.

  2002 \begin{ttbox}

  2003 Goal "?S ~: range\thinspace(f :: 'a=>'a set)";

  2004 {\out Level 0}

  2005 {\out ?S ~: range f}

  2006 {\out  1. ?S ~: range f}

  2007 \end{ttbox}

  2008 The first two steps are routine.  The rule \tdx{rangeE} replaces

  2009 $\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$.

  2010 \begin{ttbox}

  2011 by (resolve_tac [notI] 1);

  2012 {\out Level 1}

  2013 {\out ?S ~: range f}

  2014 {\out  1. ?S : range f ==> False}

  2015 \ttbreak

  2016 by (eresolve_tac [rangeE] 1);

  2017 {\out Level 2}

  2018 {\out ?S ~: range f}

  2019 {\out  1. !!x. ?S = f x ==> False}

  2020 \end{ttbox}

  2021 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$,

  2022 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for

  2023 any~$\Var{c}$.

  2024 \begin{ttbox}

  2025 by (eresolve_tac [equalityCE] 1);

  2026 {\out Level 3}

  2027 {\out ?S ~: range f}

  2028 {\out  1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False}

  2029 {\out  2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False}

  2030 \end{ttbox}

  2031 Now we use a bit of creativity.  Suppose that~$\Var{S}$ has the form of a

  2032 comprehension.  Then $\Var{c}\in\{x.\Var{P}~x\}$ implies

  2033 $\Var{P}~\Var{c}$.   Destruct-resolution using \tdx{CollectD}

  2034 instantiates~$\Var{S}$ and creates the new assumption.

  2035 \begin{ttbox}

  2036 by (dresolve_tac [CollectD] 1);

  2037 {\out Level 4}

  2038 {\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f}

  2039 {\out  1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False}

  2040 {\out  2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False}

  2041 \end{ttbox}

  2042 Forcing a contradiction between the two assumptions of subgoal~1

  2043 completes the instantiation of~$S$.  It is now the set $\{x. x\not\in   2044 f~x\}$, which is the standard diagonal construction.

  2045 \begin{ttbox}

  2046 by (contr_tac 1);

  2047 {\out Level 5}

  2048 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}

  2049 {\out  1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False}

  2050 \end{ttbox}

  2051 The rest should be easy.  To apply \tdx{CollectI} to the negated

  2052 assumption, we employ \ttindex{swap_res_tac}:

  2053 \begin{ttbox}

  2054 by (swap_res_tac [CollectI] 1);

  2055 {\out Level 6}

  2056 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}

  2057 {\out  1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x}

  2058 \ttbreak

  2059 by (assume_tac 1);

  2060 {\out Level 7}

  2061 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}

  2062 {\out No subgoals!}

  2063 \end{ttbox}

  2064 How much creativity is required?  As it happens, Isabelle can prove this

  2065 theorem automatically.  The default classical set \texttt{claset()} contains

  2066 rules for most of the constructs of HOL's set theory.  We must augment it with

  2067 \tdx{equalityCE} to break up set equalities, and then apply best-first search.

  2068 Depth-first search would diverge, but best-first search successfully navigates

  2069 through the large search space.  \index{search!best-first}

  2070 \begin{ttbox}

  2071 choplev 0;

  2072 {\out Level 0}

  2073 {\out ?S ~: range f}

  2074 {\out  1. ?S ~: range f}

  2075 \ttbreak

  2076 by (best_tac (claset() addSEs [equalityCE]) 1);

  2077 {\out Level 1}

  2078 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}

  2079 {\out No subgoals!}

  2080 \end{ttbox}

  2081 If you run this example interactively, make sure your current theory contains

  2082 theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}.

  2083 Otherwise the default claset may not contain the rules for set theory.

  2084 \index{higher-order logic|)}

  2085

  2086 %%% Local Variables:

  2087 %%% mode: latex

  2088 %%% TeX-master: "logics-HOL"

  2089 %%% End: