doc-src/Logics/HOL.tex
 author berghofe Mon Jul 15 10:41:30 1996 +0200 (1996-07-15) changeset 1859 2ea3f7ebeccb parent 1854 563dd2b25e37 child 2495 82ec47e0a8d3 permissions -rw-r--r--
updated syntax of primrec definitions
     1 %% $Id$

     2 \chapter{Higher-Order Logic}

     3 \index{higher-order logic|(}

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

     5

     6 The theory~\thydx{HOL} implements higher-order logic.  It is based on

     7 Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on

     8 Church's original paper~\cite{church40}.  Andrews's book~\cite{andrews86} is a

     9 full description of higher-order logic.  Experience with the {\sc hol} system

    10 has demonstrated that higher-order logic is useful for hardware verification;

    11 beyond this, it is widely applicable in many areas of mathematics.  It is

    12 weaker than {\ZF} set theory but for most applications this does not matter.

    13 If you prefer {\ML} to Lisp, you will probably prefer \HOL\ to~{\ZF}.

    14

    15 The syntax of Isabelle's \HOL\ has recently been changed to look more like the

    16 traditional syntax of higher-order logic.  Function application is now

    17 curried.  To apply the function~$f$ to the arguments~$a$ and~$b$ in \HOL, you

    18 must write $f\,a\,b$.  Note that $f(a,b)$ means $f$ applied to the pair

    19 $(a,b)$'' in \HOL.  We write ordered pairs as $(a,b)$, not $\langle   20 a,b\rangle$ as in {\ZF} and earlier versions of \HOL.  Early releases of

    21 Isabelle included still another version of~\HOL, with explicit type inference

    22 rules~\cite{paulson-COLOG}.  This version no longer exists, but \thydx{ZF}

    23 supports a similar style of reasoning.

    24

    25 \HOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It

    26 identifies object-level types with meta-level types, taking advantage of

    27 Isabelle's built-in type checker.  It identifies object-level functions

    28 with meta-level functions, so it uses Isabelle's operations for abstraction

    29 and application.  There is no apply' operator: function applications are

    30 written as simply~$f~a$ rather than $f{\tt}a$.

    31

    32 These identifications allow Isabelle to support \HOL\ particularly nicely,

    33 but they also mean that \HOL\ requires more sophistication from the user

    34 --- in particular, an understanding of Isabelle's type system.  Beginners

    35 should work with {\tt show_types} set to {\tt true}.  Gain experience by

    36 working in first-order logic before attempting to use higher-order logic.

    37 This chapter assumes familiarity with~{\FOL{}}.

    38

    39

    40 \begin{figure}

    41 \begin{constants}

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

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

    44   \cdx{not}     & $bool\To bool$                & negation ($\neg$) \\

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

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

    47   \cdx{If}      & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\

    48   \cdx{Inv}     & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\

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

    50 \end{constants}

    51 \subcaption{Constants}

    52

    53 \begin{constants}

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

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

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

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

    58   \tt\at & \cdx{Eps}  & $(\alpha\To bool)\To\alpha::term$ &

    59         Hilbert description ($\epsilon$) \\

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

    61         universal quantifier ($\forall$) \\

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

    63         existential quantifier ($\exists$) \\

    64   {\tt?!} or {\tt EX!}  & \cdx{Ex1}  & $(\alpha::term\To bool)\To bool$ &

    65         unique existence ($\exists!$)

    66 \end{constants}

    67 \subcaption{Binders}

    68

    69 \begin{constants}

    70 \index{*"= symbol}

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

    72 \index{*"| symbol}

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

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

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

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

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

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

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

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

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

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

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

    84 \end{constants}

    85 \subcaption{Infixes}

    86 \caption{Syntax of {\tt HOL}} \label{hol-constants}

    87 \end{figure}

    88

    89

    90 \begin{figure}

    91 \index{*let symbol}

    92 \index{*in symbol}

    93 \dquotes

    94 $\begin{array}{rclcl}   95 term & = & \hbox{expression of class~term} \\   96 & | & "\at~" id~id^* " . " formula \\   97 & | &   98 \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\   99 & | &   100 \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\[2ex]   101 formula & = & \hbox{expression of type~bool} \\   102 & | & term " = " term \\   103 & | & term " \ttilde= " term \\   104 & | & term " < " term \\   105 & | & term " <= " term \\   106 & | & "\ttilde\ " formula \\   107 & | & formula " \& " formula \\   108 & | & formula " | " formula \\   109 & | & formula " --> " formula \\   110 & | & "!~~~" id~id^* " . " formula   111 & | & "ALL~" id~id^* " . " formula \\   112 & | & "?~~~" id~id^* " . " formula   113 & | & "EX~~" id~id^* " . " formula \\   114 & | & "?!~~" id~id^* " . " formula   115 & | & "EX!~" id~id^* " . " formula   116 \end{array}   117$

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

   119 \end{figure}

   120

   121

   122 \section{Syntax}

   123 The type class of higher-order terms is called~\cldx{term}.  Type variables

   124 range over this class by default.  The equality symbol and quantifiers are

   125 polymorphic over class {\tt term}.

   126

   127 Class \cldx{ord} consists of all ordered types; the relations $<$ and

   128 $\leq$ are polymorphic over this class, as are the functions

   129 \cdx{mono}, \cdx{min} and \cdx{max}.  Three other

   130 type classes --- \cldx{plus}, \cldx{minus} and \cldx{times} --- permit

   131 overloading of the operators {\tt+}, {\tt-} and {\tt*}.  In particular,

   132 {\tt-} is overloaded for set difference and subtraction.

   133 \index{*"+ symbol}

   134 \index{*"- symbol}

   135 \index{*"* symbol}

   136

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

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

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

   140 $\neg(a=b)$.

   141

   142 \begin{warn}

   143   \HOL\ has no if-and-only-if connective; logical equivalence is expressed

   144   using equality.  But equality has a high priority, as befitting a

   145   relation, while if-and-only-if typically has the lowest priority.  Thus,

   146   $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.

   147   When using $=$ to mean logical equivalence, enclose both operands in

   148   parentheses.

   149 \end{warn}

   150

   151 \subsection{Types}\label{hol-types}

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

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

   154 types, is overloaded with arity {\tt(term,term)term}.  Thus, $\sigma\To\tau$

   155 belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification

   156 over functions.

   157

   158 HOL offers various methods for introducing new types. For details

   159 see~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}.

   160

   161

   162 \subsection{Binders}

   163 Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$

   164 satisfying~$P[a]$, if such exists.  Since all terms in \HOL\ denote

   165 something, a description is always meaningful, but we do not know its value

   166 unless $P[x]$ defines it uniquely.  We may write descriptions as

   167 \cdx{Eps}($P$) or use the syntax

   168 \hbox{\tt \at $x$.$P[x]$}.

   169

   170 Existential quantification is defined by

   171 $\exists x.P~x \;\equiv\; P(\epsilon x.P~x).$

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

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

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

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

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

   177

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

   179 Quantifiers have two notations.  As in Gordon's {\sc hol} system, \HOL\

   180 uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$.  The

   181 existential quantifier must be followed by a space; thus {\tt?x} is an

   182 unknown, while \verb'? x.f x=y' is a quantification.  Isabelle's usual

   183 notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also

   184 available.  Both notations are accepted for input.  The {\ML} reference

   185 \ttindexbold{HOL_quantifiers} governs the output notation.  If set to {\tt

   186 true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default.  If set

   187 to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.

   188

   189 All these binders have priority 10.

   190

   191

   192 \subsection{The \sdx{let} and \sdx{case} constructions}

   193 Local abbreviations can be introduced by a {\tt let} construct whose

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

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

   196 definition, \tdx{Let_def}.

   197

   198 \HOL\ also defines the basic syntax

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

   200 as a uniform means of expressing {\tt case} constructs.  Therefore {\tt case}

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

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

   203 {\tt case} construct to denote applications of particular case operators.

   204 This is what happens automatically for each {\tt datatype} declaration. For

   205 example \verb$datatype nat = Z | S nat$ declares a translation between

   206 \verb$case x of Z => a | S n => b$ and \verb$nat_case a (%n.b) x$, where

   207 \verb$nat_case$ is some appropriate function.

   208

   209

   210 \begin{figure}

   211 \begin{ttbox}\makeatother

   212 \tdx{refl}           t = t

   213 \tdx{subst}          [| s=t; P s |] ==> P t

   214 \tdx{ext}            (!!x. f x = g x) ==> (\%x.f x) = (\%x.g x)

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

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

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

   218 \tdx{selectI}        P(x) ==> P(@x.P x)

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

   220 \end{ttbox}

   221 \caption{The {\tt HOL} rules} \label{hol-rules}

   222 \end{figure}

   223

   224

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

   226 \begin{ttbox}\makeatother

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

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

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

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

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

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

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

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

   235

   236 \tdx{Inv_def}    Inv      == (\%f y. @x. f x = y)

   237 \tdx{o_def}      op o     == (\%f g x. f(g x))

   238 \tdx{if_def}     If P x y == (\%P x y.@z.(P=True --> z=x) & (P=False --> z=y))

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

   240 \end{ttbox}

   241 \caption{The {\tt HOL} definitions} \label{hol-defs}

   242 \end{figure}

   243

   244

   245 \section{Rules of inference}

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

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

   248 \begin{ttdescription}

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

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

   251   equal.

   252 \item[\tdx{selectI}] gives the defining property of the Hilbert

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

   254   \tdx{select_equality} (see below) is often easier to use.

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

   256     fact, the $\epsilon$-operator already makes the logic classical, as

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

   258 \end{ttdescription}

   259

   260 \HOL{} follows standard practice in higher-order logic: only a few

   261 connectives are taken as primitive, with the remainder defined obscurely

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

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

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

   265 higher-order logic may equate formulae and even functions over formulae.

   266 But theory~\HOL{}, like all other Isabelle theories, uses

   267 meta-equality~({\tt==}) for definitions.

   268

   269 Some of the rules mention type variables; for example, {\tt refl}

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

   271 type variables explicitly by calling {\tt res_inst_tac}.  By default,

   272 explicit type variables have class \cldx{term}.

   273

   274 Include type constraints whenever you state a polymorphic goal.  Type

   275 inference may otherwise make the goal more polymorphic than you intended,

   276 with confusing results.

   277

   278 \begin{warn}

   279   If resolution fails for no obvious reason, try setting

   280   \ttindex{show_types} to {\tt true}, causing Isabelle to display types of

   281   terms.  Possibly set \ttindex{show_sorts} to {\tt true} as well, causing

   282   Isabelle to display sorts.

   283

   284   \index{unification!incompleteness of}

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

   286   guarantee to find instantiations for type variables automatically.  Be

   287   prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac},

   288   possibly instantiating type variables.  Setting

   289   \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to report

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

   291 \end{warn}

   292

   293

   294 \begin{figure}

   295 \begin{ttbox}

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

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

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

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

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

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

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

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

   304 \subcaption{Equality}

   305

   306 \tdx{TrueI}       True

   307 \tdx{FalseE}      False ==> P

   308

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

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

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

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

   313

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

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

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

   317

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

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

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

   321 \subcaption{Propositional logic}

   322

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

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

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

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

   327 %

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

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

   330 \subcaption{Logical equivalence}

   331

   332 \end{ttbox}

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

   334 \end{figure}

   335

   336

   337 \begin{figure}

   338 \begin{ttbox}\makeatother

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

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

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

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

   343

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

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

   346

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

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

   349           |] ==> R

   350

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

   352 \subcaption{Quantifiers and descriptions}

   353

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

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

   356 \tdx{excluded_middle} ~P | P

   357

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

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

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

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

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

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

   364 \subcaption{Classical logic}

   365

   366 %\tdx{if_True}         (if True then x else y) = x

   367 %\tdx{if_False}        (if False then x else y) = y

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

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

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

   371 \subcaption{Conditionals}

   372 \end{ttbox}

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

   374 \end{figure}

   375

   376

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

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

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

   380 conjunctions, implications, and universal quantifiers.

   381

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

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

   384 simplifying both sides of an equation.

   385

   386 The following simple tactics are occasionally useful:

   387 \begin{ttdescription}

   388 \item[\ttindexbold{strip_tac} $i$] applies {\tt allI} and {\tt impI}

   389   repeatedly to remove all outermost universal quantifiers and implications

   390   from subgoal $i$.

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

   392   on $P$ for subgoal $i$: the latter is replaced by two identical subgoals

   393   with the added assumptions $P$ and $\neg P$, respectively.

   394 \end{ttdescription}

   395

   396

   397 \begin{figure}

   398 \begin{center}

   399 \begin{tabular}{rrr}

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

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

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

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

   404         & insertion of element \\

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

   406         & comprehension \\

   407   \cdx{Compl}   & $(\alpha\,set)\To\alpha\,set$

   408         & complement \\

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

   410         & intersection over a set\\

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

   412         & union over a set\\

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

   414         &set of sets intersection \\

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

   416         &set of sets union \\

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

   418         & powerset \$1ex]   419 \cdx{range} & (\alpha\To\beta )\To\beta\,set   420 & range of a function \\[1ex]   421 \cdx{Ball}~~\cdx{Bex} & [\alpha\,set,\alpha\To bool]\To bool   422 & bounded quantifiers \\   423 \cdx{mono} & (\alpha\,set\To\beta\,set)\To bool   424 & monotonicity \\   425 \cdx{inj}~~\cdx{surj}& (\alpha\To\beta )\To bool   426 & injective/surjective \\   427 \cdx{inj_onto} & [\alpha\To\beta ,\alpha\,set]\To bool   428 & injective over subset   429 \end{tabular}   430 \end{center}   431 \subcaption{Constants}   432   433 \begin{center}   434 \begin{tabular}{llrrr}   435 \it symbol &\it name &\it meta-type & \it priority & \it description \\   436 \sdx{INT} & \cdx{INTER1} & (\alpha\To\beta\,set)\To\beta\,set & 10 &   437 intersection over a type\\   438 \sdx{UN} & \cdx{UNION1} & (\alpha\To\beta\,set)\To\beta\,set & 10 &   439 union over a type   440 \end{tabular}   441 \end{center}   442 \subcaption{Binders}   443   444 \begin{center}   445 \index{*"" symbol}   446 \index{*": symbol}   447 \index{*"<"= symbol}   448 \begin{tabular}{rrrr}   449 \it symbol & \it meta-type & \it priority & \it description \\   450 \tt  & [\alpha\To\beta ,\alpha\,set]\To (\beta\,set)   451 & Left 90 & image \\   452 \sdx{Int} & [\alpha\,set,\alpha\,set]\To\alpha\,set   453 & Left 70 & intersection (\inter) \\   454 \sdx{Un} & [\alpha\,set,\alpha\,set]\To\alpha\,set   455 & Left 65 & union (\union) \\   456 \tt: & [\alpha ,\alpha\,set]\To bool   457 & Left 50 & membership (\in) \\   458 \tt <= & [\alpha\,set,\alpha\,set]\To bool   459 & Left 50 & subset (\subseteq)   460 \end{tabular}   461 \end{center}   462 \subcaption{Infixes}   463 \caption{Syntax of the theory {\tt Set}} \label{hol-set-syntax}   464 \end{figure}   465   466   467 \begin{figure}   468 \begin{center} \tt\frenchspacing   469 \index{*"! symbol}   470 \begin{tabular}{rrr}   471 \it external & \it internal & \it description \\   472 a \ttilde: b & \ttilde(a : b) & \rm non-membership\\   473 \{a@1, \ldots\} & insert a@1 \ldots \{\} & \rm finite set \\   474 \{x.P[x]\} & Collect(\lambda x.P[x]) &   475 \rm comprehension \\   476 \sdx{INT} x:A.B[x] & INTER A \lambda x.B[x] &   477 \rm intersection \\   478 \sdx{UN}{\tt\ } x:A.B[x] & UNION A \lambda x.B[x] &   479 \rm union \\   480 \tt ! x:A.P[x] or \sdx{ALL} x:A.P[x] &   481 Ball A \lambda x.P[x] &   482 \rm bounded \forall \\   483 \sdx{?} x:A.P[x] or \sdx{EX}{\tt\ } x:A.P[x] &   484 Bex A \lambda x.P[x] & \rm bounded \exists   485 \end{tabular}   486 \end{center}   487 \subcaption{Translations}   488   489 \dquotes   490 \[\begin{array}{rclcl}   491 term & = & \hbox{other terms\ldots} \\   492 & | & "\{\}" \\   493 & | & "\{ " term\; ("," term)^* " \}" \\   494 & | & "\{ " id " . " formula " \}" \\   495 & | & term "  " term \\   496 & | & term " Int " term \\   497 & | & term " Un " term \\   498 & | & "INT~~" id ":" term " . " term \\   499 & | & "UN~~~" id ":" term " . " term \\   500 & | & "INT~~" id~id^* " . " term \\   501 & | & "UN~~~" id~id^* " . " term \\[2ex]   502 formula & = & \hbox{other formulae\ldots} \\   503 & | & term " : " term \\   504 & | & term " \ttilde: " term \\   505 & | & term " <= " term \\   506 & | & "!~" id ":" term " . " formula   507 & | & "ALL " id ":" term " . " formula \\   508 & | & "?~" id ":" term " . " formula   509 & | & "EX~~" id ":" term " . " formula   510 \end{array}   511$

   512 \subcaption{Full Grammar}

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

   514 \end{figure}

   515

   516

   517 \section{A formulation of set theory}

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

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

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

   521 theory, and behave more like {\ZF} classes.

   522 \begin{itemize}

   523 \item

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

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

   526 \item

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

   528 may be defined by absolute comprehension.

   529 \item

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

   531 have a more complex type.

   532 \end{itemize}

   533 Finite unions and intersections have the same behaviour in \HOL\ as they

   534 do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,

   535 denoting the universal set for the given type.

   536

   537 % FIXME: define set via typedef

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

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

   540 essentially the same as $\alpha\To bool$.  The new type is defined for

   541 clarity and to avoid complications involving function types in unification.

   542 Since Isabelle does not support type definitions (as mentioned in

   543 \S\ref{hol-types}), the isomorphisms between the two types are declared

   544 explicitly.  Here they are natural: {\tt Collect} maps $\alpha\To bool$ to

   545 $\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring

   546 argument order).

   547

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

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

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

   551 and $A\inter B$), the subset and membership relations, and the image

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

   553 $\neg(a\in b)$.

   554

   555 The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the

   556 obvious manner using~{\tt insert} and~$\{\}$:

   557 \begin{eqnarray*}

   558   \{a@1, \ldots, a@n\}  & \equiv &

   559   {\tt insert}~a@1~({\tt insert}\ldots({\tt insert}~a@n~\{\})\ldots)

   560 \end{eqnarray*}

   561

   562 The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)

   563 that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free

   564 occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda   565 x.P[x])$.  It defines sets by absolute comprehension, which is impossible

   566 in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.

   567

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

   569 \begin{eqnarray*}

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

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

   572 \end{eqnarray*}

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

   574 accordingly.  Instead of {\tt Ball $A$ $P$} and {\tt Bex $A$ $P$} we may

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

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

   577 %

   578 \hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}.  Isabelle's

   579 usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted

   580 for input.  As with the primitive quantifiers, the {\ML} reference

   581 \ttindex{HOL_quantifiers} specifies which notation to use for output.

   582

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

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

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

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

   587

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

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

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

   592

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

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

   595 respectively.

   596

   597

   598 % FIXME: remove the two laws connecting mem and Collect

   599 \begin{figure} \underscoreon

   600 \begin{ttbox}

   601 \tdx{mem_Collect_eq}    (a : \{x.P x\}) = P a

   602 \tdx{Collect_mem_eq}    \{x.x:A\} = A

   603

   604 \tdx{empty_def}         \{\}          == \{x.False\}

   605 \tdx{insert_def}        insert a B  == \{x.x=a\} Un B

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

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

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

   609 \tdx{Un_def}            A Un B      == \{x.x:A | x:B\}

   610 \tdx{Int_def}           A Int B     == \{x.x:A & x:B\}

   611 \tdx{set_diff_def}      A - B       == \{x.x:A & x~:B\}

   612 \tdx{Compl_def}         Compl A     == \{x. ~ x:A\}

   613 \tdx{INTER_def}         INTER A B   == \{y. ! x:A. y: B x\}

   614 \tdx{UNION_def}         UNION A B   == \{y. ? x:A. y: B x\}

   615 \tdx{INTER1_def}        INTER1 B    == INTER \{x.True\} B

   616 \tdx{UNION1_def}        UNION1 B    == UNION \{x.True\} B

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

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

   619 \tdx{Pow_def}           Pow A       == \{B. B <= A\}

   620 \tdx{image_def}         fA        == \{y. ? x:A. y=f x\}

   621 \tdx{range_def}         range f     == \{y. ? x. y=f x\}

   622 \tdx{mono_def}          mono f      == !A B. A <= B --> f A <= f B

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

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

   625 \tdx{inj_onto_def}      inj_onto f A == !x:A. !y:A. f x=f y --> x=y

   626 \end{ttbox}

   627 \caption{Rules of the theory {\tt Set}} \label{hol-set-rules}

   628 \end{figure}

   629

   630

   631 \begin{figure} \underscoreon

   632 \begin{ttbox}

   633 \tdx{CollectI}        [| P a |] ==> a : \{x.P x\}

   634 \tdx{CollectD}        [| a : \{x.P x\} |] ==> P a

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

   636

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

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

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

   640

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

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

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

   644 \subcaption{Comprehension and Bounded quantifiers}

   645

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

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

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

   649

   650 \tdx{subset_refl}     A <= A

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

   652

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

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

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

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

   657

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

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

   660                 |]  ==>  P

   661 \subcaption{The subset and equality relations}

   662 \end{ttbox}

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

   664 \end{figure}

   665

   666

   667 \begin{figure} \underscoreon

   668 \begin{ttbox}

   669 \tdx{emptyE}   a : \{\} ==> P

   670

   671 \tdx{insertI1} a : insert a B

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

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

   674

   675 \tdx{ComplI}   [| c:A ==> False |] ==> c : Compl A

   676 \tdx{ComplD}   [| c : Compl A |] ==> ~ c:A

   677

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

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

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

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

   682

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

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

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

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

   687

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

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

   690

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

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

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

   694

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

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

   697

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

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

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

   701

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

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

   704 \end{ttbox}

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

   706 \end{figure}

   707

   708

   709 \subsection{Axioms and rules of set theory}

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

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

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

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

   714

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

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

   717 They also include straightforward properties of functions: image~({\tt}) and

   718 {\tt range}, and predicates concerning monotonicity, injectiveness and

   719 surjectiveness.

   720

   721 The predicate \cdx{inj_onto} is used for simulating type definitions.

   722 The statement ${\tt inj_onto}~f~A$ asserts that $f$ is injective on the

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

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

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

   726

   727 \begin{figure} \underscoreon

   728 \begin{ttbox}

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

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

   731

   732 %\tdx{Inv_injective}

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

   734 %

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

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

   737

   738 \tdx{rangeI}     f x : range f

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

   740

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

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

   743

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

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

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

   747

   748 \tdx{inj_ontoI}  (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_onto f A

   749 \tdx{inj_ontoD}  [| inj_onto f A;  f x=f y;  x:A;  y:A |] ==> x=y

   750

   751 \tdx{inj_onto_inverseI}

   752     (!!x. x:A ==> g(f x) = x) ==> inj_onto f A

   753 \tdx{inj_onto_contraD}

   754     [| inj_onto f A;  x~=y;  x:A;  y:A |] ==> ~ f x=f y

   755 \end{ttbox}

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

   757 \end{figure}

   758

   759

   760 \begin{figure} \underscoreon

   761 \begin{ttbox}

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

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

   764

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

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

   767

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

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

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

   771

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

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

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

   775 \end{ttbox}

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

   777 \end{figure}

   778

   779

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

   781 \begin{ttbox}

   782 \tdx{Int_absorb}        A Int A = A

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

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

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

   786

   787 \tdx{Un_absorb}         A Un A = A

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

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

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

   791

   792 \tdx{Compl_disjoint}    A Int (Compl A) = \{x.False\}

   793 \tdx{Compl_partition}   A Un  (Compl A) = \{x.True\}

   794 \tdx{double_complement} Compl(Compl A) = A

   795 \tdx{Compl_Un}          Compl(A Un B)  = (Compl A) Int (Compl B)

   796 \tdx{Compl_Int}         Compl(A Int B) = (Compl A) Un (Compl B)

   797

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

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

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

   801

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

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

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

   805 \end{ttbox}

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

   807 \end{figure}

   808

   809

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

   811 obvious and resemble rules of Isabelle's {\ZF} set theory.  Certain rules,

   812 such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},

   813 are designed for classical reasoning; the rules \tdx{subsetD},

   814 \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not

   815 strictly necessary but yield more natural proofs.  Similarly,

   816 \tdx{equalityCE} supports classical reasoning about extensionality,

   817 after the fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for

   818 proofs pertaining to set theory.

   819

   820 Figure~\ref{hol-fun} presents derived inference rules involving functions.

   821 They also include rules for \cdx{Inv}, which is defined in theory~{\tt

   822   HOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an

   823 inverse of~$f$.  They also include natural deduction rules for the image

   824 and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.

   825 Reasoning about function composition (the operator~\sdx{o}) and the

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

   827 the file {\tt HOL/fun.ML} for a complete listing of the derived rules.

   828

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

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

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

   832 reasoning about the membership relation.  See the file {\tt HOL/subset.ML}.

   833

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

   835 include commutative, associative and distributive laws involving unions,

   836 intersections and complements.  The proofs are mostly trivial, using the

   837 classical reasoner; see file {\tt HOL/equalities.ML}.

   838

   839

   840 \section{Generic packages}

   841 \HOL\ instantiates most of Isabelle's generic packages;

   842 see {\tt HOL/ROOT.ML} for details.

   843

   844 \subsection{Substitution and simplification}

   845

   846 Because it includes a general substitution rule, \HOL\ instantiates the

   847 tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a

   848 subgoal and its hypotheses.

   849

   850 It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the

   851 simplification set for higher-order logic.  Equality~($=$), which also

   852 expresses logical equivalence, may be used for rewriting.  See the file {\tt

   853 HOL/simpdata.ML} for a complete listing of the simplification rules.

   854

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

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

   857 and simplification.

   858

   859 \begin{warn}\index{simplification!of conjunctions}

   860   The simplifier is not set up to reduce, for example, \verb$a = b & ...a...$

   861   to \verb$a = b & ...b...$: it does not use the left part of a conjunction

   862   while simplifying the right part. This can be changed by including

   863   \ttindex{conj_cong} in a simpset: \verb$addcongs [conj_cong]$. It can slow

   864   down rewriting and is therefore not included by default.

   865 \end{warn}

   866

   867 In case a rewrite rule cannot be dealt with by the simplifier (either because

   868 of nontermination or because its left-hand side is too flexible), HOL

   869 provides {\tt stac}:

   870 \begin{ttdescription}

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

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

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

   874   may be necessary to select the desired ones.

   875 \end{ttdescription}

   876

   877

   878 \subsection{Classical reasoning}

   879

   880 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as

   881 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap

   882 rule; recall Fig.\ts\ref{hol-lemmas2} above.

   883

   884 The classical reasoner is set up as the structure

   885 {\tt Classical}.  This structure is open, so {\ML} identifiers such

   886 as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.

   887 \HOL\ defines the following classical rule sets:

   888 \begin{ttbox}

   889 prop_cs    : claset

   890 HOL_cs     : claset

   891 set_cs     : claset

   892 \end{ttbox}

   893 \begin{ttdescription}

   894 \item[\ttindexbold{prop_cs}] contains the propositional rules, namely

   895 those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,

   896 along with the rule~{\tt refl}.

   897

   898 \item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules

   899   {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE}

   900   and~{\tt exI}, as well as rules for unique existence.  Search using

   901   this classical set is incomplete: quantified formulae are used at most

   902   once.

   903

   904 \item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded

   905   quantifiers, subsets, comprehensions, unions and intersections,

   906   complements, finite sets, images and ranges.

   907 \end{ttdescription}

   908 \noindent

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

   910         {Chap.\ts\ref{chap:classical}}

   911 for more discussion of classical proof methods.

   912

   913

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

   915 This section describes HOL's basic predefined types (\verb$*$, \verb$+$, {\tt

   916   nat} and {\tt list}) and ways for introducing new types. The most important

   917 type construction, the {\tt datatype}, is treated separately in

   918 \S\ref{sec:HOL:datatype}.

   919

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

   921

   922 \begin{figure}

   923 \begin{constants}

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

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

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

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

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

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

   930         & & generalized projection\\

   931   \cdx{Sigma}  &

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

   933         & general sum of sets

   934 \end{constants}

   935 \begin{ttbox}\makeatletter

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

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

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

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

   940

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

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

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

   944

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

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

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

   948

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

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

   951

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

   953 \tdx{SigmaE}       [| c: Sigma A B;

   954                 !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P

   955 \end{ttbox}

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

   957 \end{figure}

   958

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

   960 $\alpha\times\beta$, with the ordered pair syntax {\tt($a$,$b$)}. Tuples are

   961 simulated by pairs nested to the right:

   962 \begin{center}

   963 \begin{tabular}{|c|c|}

   964 \hline

   965 external & internal \\

   966 \hline

   967 $\tau@1 * \dots * \tau@n$ & $\tau@1 * (\dots (\tau@{n-1} * \tau@n)\dots)$ \\

   968 \hline

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

   970 \hline

   971 \end{tabular}

   972 \end{center}

   973 In addition, it is possible to use tuples

   974 as patterns in abstractions:

   975 \begin{center}

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

   977 \end{center}

   978 Nested patterns are possible and are translated stepwise:

   979 {\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$

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

   981   $z$.$t$))}. The reverse translation is performed upon printing.

   982 \begin{warn}

   983   The translation between patterns and {\tt split} is performed automatically

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

   985   may differ, whichs affects proofs.  For example the term {\tt

   986     (\%(x,y).(y,x))(a,b)} requires the theorem {\tt split} to rewrite to

   987   {\tt(b,a)}.

   988 \end{warn}

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

   990 variable binding construct which is internally described by a

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

   992 \begin{description}

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

   994 \item[Quantifiers:] {\tt !~{\it pattern}:$A$.~$P$}

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

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

   997 \item[Sets:] {\tt \{~{\it pattern}~.~$P$~\}}

   998 \end{description}

   999

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

  1001 \begin{ttdescription}

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

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

  1004   each component. A simple example:

  1005 \begin{ttbox}

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

  1007 by(split_all_tac 1);

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

  1009 \end{ttbox}

  1010 \end{ttdescription}

  1011

  1012 Theory {\tt Prod} also introduces the degenerate product type {\tt unit}

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

  1014 \begin{ttbox}

  1015 \tdx{unit_eq}       u = ()

  1016 \end{ttbox}

  1017 \bigskip

  1018

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

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

  1022

  1023 The definition of products and sums in terms of existing types is not shown.

  1024 The constructions are fairly standard and can be found in the respective {\tt

  1025   thy}-files.

  1026

  1027 \begin{figure}

  1028 \begin{constants}

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

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

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

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

  1033         & & conditional

  1034 \end{constants}

  1035 \begin{ttbox}\makeatletter

  1036 %\tdx{sum_case_def}   sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) &

  1037 %                                        (!y. p=Inr y --> z=g y))

  1038 %

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

  1040

  1041 \tdx{inj_Inl}        inj Inl

  1042 \tdx{inj_Inr}        inj Inr

  1043

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

  1045

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

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

  1048

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

  1050 \tdx{expand_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &

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

  1052 \end{ttbox}

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

  1054 \end{figure}

  1055

  1056 \begin{figure}

  1057 \index{*"< symbol}

  1058 \index{*"* symbol}

  1059 \index{*div symbol}

  1060 \index{*mod symbol}

  1061 \index{*"+ symbol}

  1062 \index{*"- symbol}

  1063 \begin{constants}

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

  1065   \cdx{0}       & $nat$         & & zero \\

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

  1067   \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$

  1068         & & conditional\\

  1069   \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$

  1070         & & primitive recursor\\

  1071   \tt *         & $[nat,nat]\To nat$    &  Left 70      & multiplication \\

  1072   \tt div       & $[nat,nat]\To nat$    &  Left 70      & division\\

  1073   \tt mod       & $[nat,nat]\To nat$    &  Left 70      & modulus\\

  1074   \tt +         & $[nat,nat]\To nat$    &  Left 65      & addition\\

  1075   \tt -         & $[nat,nat]\To nat$    &  Left 65      & subtraction

  1076 \end{constants}

  1077 \subcaption{Constants and infixes}

  1078

  1079 \begin{ttbox}\makeatother

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

  1081

  1082 \tdx{Suc_not_Zero}   Suc m ~= 0

  1083 \tdx{inj_Suc}        inj Suc

  1084 \tdx{n_not_Suc_n}    n~=Suc n

  1085 \subcaption{Basic properties}

  1086 \end{ttbox}

  1087 \caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}

  1088 \end{figure}

  1089

  1090

  1091 \begin{figure}

  1092 \begin{ttbox}\makeatother

  1093 \tdx{nat_case_0}     nat_case a f 0 = a

  1094 \tdx{nat_case_Suc}   nat_case a f (Suc k) = f k

  1095

  1096 \tdx{nat_rec_0}      nat_rec 0 c h = c

  1097 \tdx{nat_rec_Suc}    nat_rec (Suc n) c h = h n (nat_rec n c h)

  1098

  1099 \tdx{add_0}        0+n           = n

  1100 \tdx{add_Suc}      (Suc m)+n     = Suc(m+n)

  1101 \tdx{diff_0}       m-0           = m

  1102 \tdx{diff_0_eq_0}  0-n           = n

  1103 \tdx{diff_Suc_Suc} Suc(m)-Suc(n) = m-n

  1104 \tdx{mult_def}     0*n           = 0

  1105 \tdx{mult_Suc}     Suc(m)*n      = n + m*n

  1106

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

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

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

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

  1111 \subcaption{Recursion equations}

  1112

  1113 \tdx{less_trans}     [| i<j;  j<k |] ==> i<k

  1114 \tdx{lessI}          n < Suc n

  1115 \tdx{zero_less_Suc}  0 < Suc n

  1116

  1117 \tdx{less_not_sym}   n<m --> ~ m<n

  1118 \tdx{less_not_refl}  ~ n<n

  1119 \tdx{not_less0}      ~ n<0

  1120

  1121 \tdx{Suc_less_eq}    (Suc m < Suc n) = (m<n)

  1122 \tdx{less_induct}    [| !!n. [| ! m. m<n --> P m |] ==> P n |]  ==>  P n

  1123

  1124 \tdx{less_linear}    m<n | m=n | n<m

  1125 \subcaption{The less-than relation}

  1126 \end{ttbox}

  1127 \caption{Derived rules for {\tt nat}} \label{hol-nat2}

  1128 \end{figure}

  1129

  1130 \subsection{The type of natural numbers, {\tt nat}}

  1131 %FIXME: introduce separate type proto_nat

  1132

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

  1134 traditional way.  The axiom of infinity postulates an type~\tydx{ind} of

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

  1136 The natural numbers are inductively generated by choosing an arbitrary

  1137 individual for~0 and using the injective operation to take successors.  As

  1138 usual, the isomorphisms between~\tydx{nat} and its representation are made

  1139 explicitly. For details see the file {\tt Nat.thy}.

  1140

  1141 %The definition makes use of a least fixed point operator \cdx{lfp},

  1142 %defined using the Knaster-Tarski theorem.  This is used to define the

  1143 %operator \cdx{trancl}, for taking the transitive closure of a relation.

  1144 %Primitive recursion makes use of \cdx{wfrec}, an operator for recursion

  1145 %along arbitrary well-founded relations.  The corresponding theories are

  1146 %called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@.  Elsewhere I have described

  1147 %similar constructions in the context of set theory~\cite{paulson-set-II}.

  1148

  1149 Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which

  1150 overloads $<$ and $\leq$ on the natural numbers.

  1151

  1152 Theory \thydx{Arith} develops arithmetic on the natural numbers.  It

  1153 defines addition, multiplication, subtraction, division, and remainder.

  1154 Many of their properties are proved: commutative, associative and

  1155 distributive laws, identity and cancellation laws, etc.  The most

  1156 interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$.

  1157 Division and remainder are defined by repeated subtraction, which requires

  1158 well-founded rather than primitive recursion.  See Figs.\ts\ref{hol-nat1}

  1159 and~\ref{hol-nat2}.

  1160

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

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

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

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

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

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

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

  1168

  1169 The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the

  1170 variable~$n$ in subgoal~$i$.

  1171

  1172 %FIXME add nth

  1173 \begin{figure}

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

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

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

  1177 \begin{constants}

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

  1179   \tt[]    & $\alpha list$ & & empty list\\

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

  1181         list constructor \\

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

  1183   \cdx{hd}      & $\alpha list \To \alpha$ & & head \\

  1184   \cdx{tl}      & $\alpha list \To \alpha list$ & & tail \\

  1185   \cdx{ttl}     & $\alpha list \To \alpha list$ & & total tail \\

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

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

  1188         & & mapping functional\\

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

  1190         & & filter functional\\

  1191   \cdx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$

  1192         & & forall functional\\

  1193   \sdx{mem}  & $[\alpha,\alpha list]\To bool$    &  Left 55   & membership\\

  1194   \cdx{length}  & $\alpha list \To nat$ & & length \\

  1195 %  \cdx{nth}  & $nat \To \alpha list \To \alpha$ & & indexing \\

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

  1197   & iteration \\

  1198   \cdx{flat}   & $(\alpha list) list\To \alpha list$ & & flattening \\

  1199   \cdx{rev}     & $\alpha list \To \alpha list$ & & reverse \\

  1200 \end{constants}

  1201 \subcaption{Constants and infixes}

  1202

  1203 \begin{center} \tt\frenchspacing

  1204 \begin{tabular}{rrr}

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

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

  1207         \rm finite list \\{}

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

  1209         \rm list comprehension

  1210 \end{tabular}

  1211 \end{center}

  1212 \subcaption{Translations}

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

  1214 \end{figure}

  1215

  1216

  1217 \begin{figure}

  1218 \begin{ttbox}\makeatother

  1219 \tdx{null_Nil}        null [] = True

  1220 \tdx{null_Cons}       null (x#xs) = False

  1221

  1222 \tdx{hd_Cons}         hd (x#xs) = x

  1223 \tdx{tl_Cons}         tl (x#xs) = xs

  1224

  1225 \tdx{ttl_Nil}         ttl [] = []

  1226 \tdx{ttl_Cons}        ttl (x#xs) = xs

  1227

  1228 \tdx{append_Nil}      [] @ ys = ys

  1229 \tdx{append_Cons}     (x#xs) @ ys = x # xs @ ys

  1230

  1231 \tdx{map_Nil}         map f [] = []

  1232 \tdx{map_Cons}        map f (x#xs) = f x # map f xs

  1233

  1234 \tdx{filter_Nil}      filter P [] = []

  1235 \tdx{filter_Cons}     filter P (x#xs) = (if P x then x#filter P xs else filter P xs)

  1236

  1237 \tdx{list_all_Nil}    list_all P [] = True

  1238 \tdx{list_all_Cons}   list_all P (x#xs) = (P x & list_all P xs)

  1239

  1240 \tdx{mem_Nil}         x mem [] = False

  1241 \tdx{mem_Cons}        x mem (y#ys) = (if y=x then True else x mem ys)

  1242

  1243 \tdx{length_Nil}      length([]) = 0

  1244 \tdx{length_Cons}     length(x#xs) = Suc(length(xs))

  1245

  1246 \tdx{foldl_Nil}       foldl f a [] = a

  1247 \tdx{foldl_Cons}      foldl f a (x#xs) = foldl f (f a x) xs

  1248

  1249 \tdx{flat_Nil}        flat([]) = []

  1250 \tdx{flat_Cons}       flat(x#xs) = x @ flat(xs)

  1251

  1252 \tdx{rev_Nil}         rev([]) = []

  1253 \tdx{rev_Cons}        rev(x#xs) = rev(xs) @ [x]

  1254 \end{ttbox}

  1255 \caption{Rewrite rules for lists} \label{fig:HOL:list-simps}

  1256 \end{figure}

  1257

  1258

  1259 \subsection{The type constructor for lists, {\tt list}}

  1260 \index{*list type}

  1261

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

  1263 operations with their types and syntax. The type constructor {\tt list} is

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

  1265 yields an induction tactic {\tt list.induct_tac} and a list of freeness

  1266 theorems {\tt list.simps}.

  1267 A \sdx{case} construct of the form

  1268 \begin{center}\tt

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

  1270 \end{center}

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

  1272

  1273 {\tt List} provides a basic library of list processing functions defined by

  1274 primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations

  1275 are shown in Fig.\ts\ref{fig:HOL:list-simps}.

  1276

  1277

  1278 \subsection{Introducing new types}

  1279

  1280 The \HOL-methodology dictates that all extension to a theory should be

  1281 conservative and thus preserve consistency. There are two basic type

  1282 extension mechanisms which meet this criterion: {\em type synonyms\/} and

  1283 {\em type definitions\/}. The former are inherited from {\tt Pure} and are

  1284 described elsewhere.

  1285 \begin{warn}

  1286   Types in \HOL\ must be non-empty; otherwise the quantifier rules would be

  1287   unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}.

  1288 \end{warn}

  1289 A \bfindex{type definition} identifies the new type with a subset of an

  1290 existing type. More precisely, the new type is defined by exhibiting an

  1291 existing type~$\tau$, a set~$A::(\tau)set$, and a theorem of the form $x:A$.

  1292 Thus~$A$ is a non-empty subset of~$\tau$, and the new type denotes this

  1293 subset.  New functions are generated to establish an isomorphism between the

  1294 new type and the subset.  If type~$\tau$ involves type variables $\alpha@1$,

  1295 \ldots, $\alpha@n$, then the type definition creates a type constructor

  1296 $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.

  1297

  1298 \begin{figure}[htbp]

  1299 \begin{rail}

  1300 typedef  : 'typedef' ( () | '(' tname ')') type '=' set witness;

  1301 type    : typevarlist name ( () | '(' infix ')' );

  1302 tname   : name;

  1303 set     : string;

  1304 witness : () | '(' id ')';

  1305 \end{rail}

  1306 \caption{Syntax of type definition}

  1307 \label{fig:HOL:typedef}

  1308 \end{figure}

  1309

  1310 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For

  1311 the definition of typevarlist'' and infix'' see

  1312 \iflabelundefined{chap:classical}

  1313 {the appendix of the {\em Reference Manual\/}}%

  1314 {Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the

  1315 following meaning:

  1316 \begin{description}

  1317 \item[\it type]: the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with

  1318   optional infix annotation.

  1319 \item[\it tname]: an alphanumeric name $T$ for the type constructor $ty$, in

  1320   case $ty$ is a symbolic name. Default: $ty$.

  1321 \item[\it set]: the representing subset $A$.

  1322 \item[\it witness]: name of a theorem of the form $a:A$ proving

  1323   non-emptiness. Can be omitted in case Isabelle manages to prove

  1324   non-emptiness automatically.

  1325 \end{description}

  1326 If all context conditions are met (no duplicate type variables in

  1327 'typevarlist', no extra type variables in 'set', and no free term variables

  1328 in 'set'), the following components are added to the theory:

  1329 \begin{itemize}

  1330 \item a type $ty :: (term,\dots)term$;

  1331 \item constants

  1332 \begin{eqnarray*}

  1333 T &::& (\tau)set \\

  1334 Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\

  1335 Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty

  1336 \end{eqnarray*}

  1337 \item a definition and three axioms

  1338 $  1339 \begin{array}{ll}   1340 T{\tt_def} & T \equiv A \\   1341 {\tt Rep_}T & Rep_T(x) : T \\   1342 {\tt Rep_}T{\tt_inverse} & Abs_T(Rep_T(x)) = x \\   1343 {\tt Abs_}T{\tt_inverse} & y:T \Imp Rep_T(Abs_T(y)) = y   1344 \end{array}   1345$

  1346 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$

  1347 and its inverse $Abs_T$.

  1348 \end{itemize}

  1349 Here are two simple examples where emptiness is proved automatically:

  1350 \begin{ttbox}

  1351 typedef unit = "\{False\}"

  1352

  1353 typedef (prod)

  1354   ('a, 'b) "*"    (infixr 20)

  1355       = "\{f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b)\}"

  1356 \end{ttbox}

  1357

  1358 Type definitions permit the introduction of abstract data types in a safe

  1359 way, namely by providing models based on already existing types. Given some

  1360 abstract axiomatic description $P$ of a type, this involves two steps:

  1361 \begin{enumerate}

  1362 \item Find an appropriate type $\tau$ and subset $A$ which has the desired

  1363   properties $P$, and make the above type definition based on this

  1364   representation.

  1365 \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.

  1366 \end{enumerate}

  1367 You can now forget about the representation and work solely in terms of the

  1368 abstract properties $P$.

  1369

  1370 \begin{warn}

  1371 If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by

  1372 declaring the type and its operations and by stating the desired axioms, you

  1373 should make sure the type has a non-empty model. You must also have a clause

  1374 \par

  1375 \begin{ttbox}

  1376 arities $$ty$$: (term,$$\dots$$,term)term

  1377 \end{ttbox}

  1378 in your theory file to tell Isabelle that elements of type $ty$ are in class

  1379 {\tt term}, the class of all HOL terms.

  1380 \end{warn}

  1381

  1382 \section{Datatype declarations}

  1383 \label{sec:HOL:datatype}

  1384 \index{*datatype|(}

  1385

  1386 \underscoreon

  1387

  1388 It is often necessary to extend a theory with \ML-like datatypes.  This

  1389 extension consists of the new type, declarations of its constructors and

  1390 rules that describe the new type. The theory definition section {\tt

  1391   datatype} represents a compact way of doing this.

  1392

  1393

  1394 \subsection{Foundations}

  1395

  1396 A datatype declaration has the following general structure:

  1397 $\mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~   1398 C_1~\tau_{11}~\dots~\tau_{1k_1} ~\mid~ \dots ~\mid~   1399 C_m~\tau_{m1}~\dots~\tau_{mk_m}   1400$

  1401 where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and

  1402 $\tau_{ij}$ are one of the following:

  1403 \begin{itemize}

  1404 \item type variables $\alpha_1,\dots,\alpha_n$,

  1405 \item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared

  1406   type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq   1407 \{\alpha_1,\dots,\alpha_n\}$,

  1408 \item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This

  1409     makes it a recursive type. To ensure that the new type is not empty at

  1410     least one constructor must consist of only non-recursive type

  1411     components.}

  1412 \end{itemize}

  1413 If you would like one of the $\tau_{ij}$ to be a complex type expression

  1414 $\tau$ you need to declare a new type synonym $syn = \tau$ first and use

  1415 $syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the

  1416 recursive type itself, thus ruling out problematic cases like $\mbox{\tt   1417 datatype}~ t ~=~ C(t \To t)$ together with unproblematic ones like $  1418 \mbox{\tt datatype}~ t ~=~ C(t~list).$

  1419

  1420 The constructors are automatically defined as functions of their respective

  1421 type:

  1422 $C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t$

  1423 These functions have certain {\em freeness} properties:

  1424 \begin{description}

  1425 \item[\tt distinct] They are distinct:

  1426 $C_i~x_1~\dots~x_{k_i} \neq C_j~y_1~\dots~y_{k_j} \qquad   1427 \mbox{for all}~ i \neq j.   1428$

  1429 \item[\tt inject] They are injective:

  1430 $(C_j~x_1~\dots~x_{k_j} = C_j~y_1~\dots~y_{k_j}) =   1431 (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j})   1432$

  1433 \end{description}

  1434 Because the number of inequalities is quadratic in the number of

  1435 constructors, a different method is used if their number exceeds

  1436 a certain value, currently 4. In that case every constructor is mapped to a

  1437 natural number

  1438 $  1439 \begin{array}{lcl}   1440 \mbox{\it t\_ord}(C_1~x_1~\dots~x_{k_1}) & = & 0 \\   1441 & \vdots & \\   1442 \mbox{\it t\_ord}(C_m x_1~\dots~x_{k_m}) & = & m-1   1443 \end{array}   1444$

  1445 and distinctness of constructors is expressed by:

  1446 $  1447 \mbox{\it t\_ord}~x \neq \mbox{\it t\_ord}~y \Imp x \neq y.   1448$

  1449 In addition a structural induction axiom {\tt induct} is provided:

  1450 $  1451 \infer{P x}   1452 {\begin{array}{lcl}   1453 \Forall x_1\dots x_{k_1}.   1454 \List{P~x_{r_{11}}; \dots; P~x_{r_{1l_1}}} &   1455 \Imp & P(C_1~x_1~\dots~x_{k_1}) \\   1456 & \vdots & \\   1457 \Forall x_1\dots x_{k_m}.   1458 \List{P~x_{r_{m1}}; \dots; P~x_{r_{ml_m}}} &   1459 \Imp & P(C_m~x_1~\dots~x_{k_m})   1460 \end{array}}   1461$

  1462 where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji}   1463 = (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for

  1464 all arguments of the recursive type.

  1465

  1466 The type also comes with an \ML-like \sdx{case}-construct:

  1467 $  1468 \begin{array}{rrcl}   1469 \mbox{\tt case}~e~\mbox{\tt of} & C_1~x_{11}~\dots~x_{1k_1} & \To & e_1 \\   1470 \vdots \\   1471 \mid & C_m~x_{m1}~\dots~x_{mk_m} & \To & e_m   1472 \end{array}   1473$

  1474 In contrast to \ML, {\em all} constructors must be present, their order is

  1475 fixed, and nested patterns are not supported.

  1476

  1477

  1478 \subsection{Defining datatypes}

  1479

  1480 A datatype is defined in a theory definition file using the keyword {\tt

  1481   datatype}. The definition following {\tt datatype} must conform to the

  1482 syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and must

  1483 obey the rules in the previous section. As a result the theory is extended

  1484 with the new type, the constructors, and the theorems listed in the previous

  1485 section.

  1486

  1487 \begin{figure}

  1488 \begin{rail}

  1489 typedecl : typevarlist id '=' (cons + '|')

  1490          ;

  1491 cons     : name (typ *) ( () | mixfix )

  1492          ;

  1493 typ      : id | tid | ('(' typevarlist id ')')

  1494          ;

  1495 \end{rail}

  1496 \caption{Syntax of datatype declarations}

  1497 \label{datatype-grammar}

  1498 \end{figure}

  1499

  1500 Reading the theory file produces a structure which, in addition to the usual

  1501 components, contains a structure named $t$ for each datatype $t$ defined in

  1502 the file.\footnote{Otherwise multiple datatypes in the same theory file would

  1503   lead to name clashes.} Each structure $t$ contains the following elements:

  1504 \begin{ttbox}

  1505 val distinct : thm list

  1506 val inject : thm list

  1507 val induct : thm

  1508 val cases : thm list

  1509 val simps : thm list

  1510 val induct_tac : string -> int -> tactic

  1511 \end{ttbox}

  1512 {\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described

  1513 above. For convenience {\tt distinct} contains inequalities in both

  1514 directions.

  1515 \begin{warn}

  1516   If there are five or more constructors, the {\em t\_ord} scheme is used for

  1517   {\tt distinct}.  In this case the theory {\tt Arith} must be contained

  1518   in the current theory, if necessary by including it explicitly.

  1519 \end{warn}

  1520 The reduction rules of the {\tt case}-construct are in {\tt cases}.  All

  1521 theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in

  1522 {\tt simps} for use with the simplifier. The tactic {\verb$induct_tac$~{\em

  1523     var i}\/} applies structural induction over variable {\em var} to

  1524 subgoal {\em i}.

  1525

  1526

  1527 \subsection{Examples}

  1528

  1529 \subsubsection{The datatype $\alpha~list$}

  1530

  1531 We want to define the type $\alpha~list$.\footnote{Of course there is a list

  1532   type in HOL already. This is only an example.} To do this we have to build

  1533 a new theory that contains the type definition. We start from {\tt HOL}.

  1534 \begin{ttbox}

  1535 MyList = HOL +

  1536   datatype 'a list = Nil | Cons 'a ('a list)

  1537 end

  1538 \end{ttbox}

  1539 After loading the theory (\verb$use_thy "MyList"$), we can prove

  1540 $Cons~x~xs\neq xs$.  First we build a suitable simpset for the simplifier:

  1541 \begin{ttbox}

  1542 val mylist_ss = HOL_ss addsimps MyList.list.simps;

  1543 goal MyList.thy "!x. Cons x xs ~= xs";

  1544 {\out Level 0}

  1545 {\out ! x. Cons x xs ~= xs}

  1546 {\out  1. ! x. Cons x xs ~= xs}

  1547 \end{ttbox}

  1548 This can be proved by the structural induction tactic:

  1549 \begin{ttbox}

  1550 by (MyList.list.induct_tac "xs" 1);

  1551 {\out Level 1}

  1552 {\out ! x. Cons x xs ~= xs}

  1553 {\out  1. ! x. Cons x Nil ~= Nil}

  1554 {\out  2. !!a list.}

  1555 {\out        ! x. Cons x list ~= list ==>}

  1556 {\out        ! x. Cons x (Cons a list) ~= Cons a list}

  1557 \end{ttbox}

  1558 The first subgoal can be proved with the simplifier and the distinctness

  1559 axioms which are part of \verb$mylist_ss$.

  1560 \begin{ttbox}

  1561 by (simp_tac mylist_ss 1);

  1562 {\out Level 2}

  1563 {\out ! x. Cons x xs ~= xs}

  1564 {\out  1. !!a list.}

  1565 {\out        ! x. Cons x list ~= list ==>}

  1566 {\out        ! x. Cons x (Cons a list) ~= Cons a list}

  1567 \end{ttbox}

  1568 Using the freeness axioms we can quickly prove the remaining goal.

  1569 \begin{ttbox}

  1570 by (asm_simp_tac mylist_ss 1);

  1571 {\out Level 3}

  1572 {\out ! x. Cons x xs ~= xs}

  1573 {\out No subgoals!}

  1574 \end{ttbox}

  1575 Because both subgoals were proved by almost the same tactic we could have

  1576 done that in one step using

  1577 \begin{ttbox}

  1578 by (ALLGOALS (asm_simp_tac mylist_ss));

  1579 \end{ttbox}

  1580

  1581

  1582 \subsubsection{The datatype $\alpha~list$ with mixfix syntax}

  1583

  1584 In this example we define the type $\alpha~list$ again but this time we want

  1585 to write {\tt []} instead of {\tt Nil} and we want to use the infix operator

  1586 \verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations

  1587 after the constructor declarations as follows:

  1588 \begin{ttbox}

  1589 MyList = HOL +

  1590   datatype 'a list = "[]" ("[]")

  1591                    | "#" 'a ('a list) (infixr 70)

  1592 end

  1593 \end{ttbox}

  1594 Now the theorem in the previous example can be written \verb|x#xs ~= xs|. The

  1595 proof is the same.

  1596

  1597

  1598 \subsubsection{A datatype for weekdays}

  1599

  1600 This example shows a datatype that consists of more than four constructors:

  1601 \begin{ttbox}

  1602 Days = Arith +

  1603   datatype days = Mo | Tu | We | Th | Fr | Sa | So

  1604 end

  1605 \end{ttbox}

  1606 Because there are more than four constructors, the theory must be based on

  1607 {\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although

  1608 the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct},

  1609 it can be proved by the simplifier if \verb$arith_ss$ is used:

  1610 \begin{ttbox}

  1611 val days_ss = arith_ss addsimps Days.days.simps;

  1612

  1613 goal Days.thy "Mo ~= Tu";

  1614 by (simp_tac days_ss 1);

  1615 \end{ttbox}

  1616 Note that usually it is not necessary to derive these inequalities explicitly

  1617 because the simplifier will dispose of them automatically.

  1618

  1619 \subsection{Primitive recursive functions}

  1620 \label{sec:HOL:primrec}

  1621 \index{primitive recursion|(}

  1622 \index{*primrec|(}

  1623

  1624 Datatypes come with a uniform way of defining functions, {\bf primitive

  1625   recursion}. Although it is possible to define primitive recursive functions

  1626 by asserting their reduction rules as new axioms, e.g.\

  1627 \begin{ttbox}

  1628 Append = MyList +

  1629 consts app :: ['a list,'a list] => 'a list

  1630 rules

  1631    app_Nil   "app [] ys = ys"

  1632    app_Cons  "app (x#xs) ys = x#app xs ys"

  1633 end

  1634 \end{ttbox}

  1635 this carries with it the danger of accidentally asserting an inconsistency,

  1636 as in \verb$app [] ys = us$. Therefore primitive recursive functions on

  1637 datatypes can be defined with a special syntax:

  1638 \begin{ttbox}

  1639 Append = MyList +

  1640 consts app :: ['a list,'a list] => 'a list

  1641 primrec app MyList.list

  1642    app_Nil   "app [] ys = ys"

  1643    app_Cons  "app (x#xs) ys = x#app xs ys"

  1644 end

  1645 \end{ttbox}

  1646 The system will now check that the two rules \verb$app_Nil$ and

  1647 \verb$app_Cons$ do indeed form a primitive recursive definition, thus

  1648 ensuring that consistency is maintained. For example

  1649 \begin{ttbox}

  1650 primrec app MyList.list

  1651     app_Nil   "app [] ys = us"

  1652 \end{ttbox}

  1653 is rejected:

  1654 \begin{ttbox}

  1655 Extra variables on rhs

  1656 \end{ttbox}

  1657 \bigskip

  1658

  1659 The general form of a primitive recursive definition is

  1660 \begin{ttbox}

  1661 primrec {\it function} {\it type}

  1662     {\it reduction rules}

  1663 \end{ttbox}

  1664 where

  1665 \begin{itemize}

  1666 \item {\it function} is the name of the function, either as an {\it id} or a

  1667   {\it string}. The function must already have been declared.

  1668 \item {\it type} is the name of the datatype, either as an {\it id} or in the

  1669   long form {\it Thy.t}, where {\it Thy} is the name of the parent theory the

  1670   datatype was declared in, and $t$ the name of the datatype. The long form

  1671   is required if the {\tt datatype} and the {\tt primrec} sections are in

  1672   different theories.

  1673 \item {\it reduction rules} specify one or more named equations of the form

  1674   {\it id\/}~{\it string}, where the identifier gives the name of the rule in

  1675   the result structure, and {\it string} is a reduction rule of the form $  1676 f~x_1~\dots~x_m~(C~y_1~\dots~y_k)~z_1~\dots~z_n = r$ such that $C$ is a

  1677   constructor of the datatype, $r$ contains only the free variables on the

  1678   left-hand side, and all recursive calls in $r$ are of the form

  1679   $f~\dots~y_i~\dots$ for some $i$. There must be exactly one reduction

  1680   rule for each constructor. Since these reduction rules are mainly used via

  1681   the implicit simpset, their names may be omitted.

  1682 \end{itemize}

  1683 A theory file may contain any number of {\tt primrec} sections which may be

  1684 intermixed with other declarations.

  1685

  1686 For the consistency-sensitive user it may be reassuring to know that {\tt

  1687   primrec} does not assert the reduction rules as new axioms but derives them

  1688 as theorems from an explicit definition of the recursive function in terms of

  1689 a recursion operator on the datatype.

  1690

  1691 The primitive recursive function can also use infix or mixfix syntax:

  1692 \begin{ttbox}

  1693 Append = MyList +

  1694 consts "@"  :: ['a list,'a list] => 'a list  (infixr 60)

  1695 primrec "op @" MyList.list

  1696    app_Nil   "[] @ ys = ys"

  1697    app_Cons  "(x#xs) @ ys = x#(xs @ ys)"

  1698 end

  1699 \end{ttbox}

  1700

  1701 The reduction rules become part of the ML structure \verb$Append$ and can

  1702 be used to prove theorems about the function:

  1703 \begin{ttbox}

  1704 val append_ss = HOL_ss addsimps [Append.app_Nil,Append.app_Cons];

  1705

  1706 goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)";

  1707 by (MyList.list.induct_tac "xs" 1);

  1708 by (ALLGOALS(asm_simp_tac append_ss));

  1709 \end{ttbox}

  1710

  1711 %Note that underdefined primitive recursive functions are allowed:

  1712 %\begin{ttbox}

  1713 %Tl = MyList +

  1714 %consts tl  :: 'a list => 'a list

  1715 %primrec tl MyList.list

  1716 %   tl_Cons "tl(x#xs) = xs"

  1717 %end

  1718 %\end{ttbox}

  1719 %Nevertheless {\tt tl} is total, although we do not know what the result of

  1720 %\verb$tl([])$ is.

  1721

  1722 \index{primitive recursion|)}

  1723 \index{*primrec|)}

  1724 \index{*datatype|)}

  1725

  1726

  1727 \section{Inductive and coinductive definitions}

  1728 \index{*inductive|(}

  1729 \index{*coinductive|(}

  1730

  1731 An {\bf inductive definition} specifies the least set closed under given

  1732 rules.  For example, a structural operational semantics is an inductive

  1733 definition of an evaluation relation.  Dually, a {\bf coinductive

  1734   definition} specifies the greatest set closed under given rules.  An

  1735 important example is using bisimulation relations to formalize equivalence

  1736 of processes and infinite data structures.

  1737

  1738 A theory file may contain any number of inductive and coinductive

  1739 definitions.  They may be intermixed with other declarations; in

  1740 particular, the (co)inductive sets {\bf must} be declared separately as

  1741 constants, and may have mixfix syntax or be subject to syntax translations.

  1742

  1743 Each (co)inductive definition adds definitions to the theory and also

  1744 proves some theorems.  Each definition creates an ML structure, which is a

  1745 substructure of the main theory structure.

  1746

  1747 This package is derived from the ZF one, described in a

  1748 separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a

  1749   longer version is distributed with Isabelle.} which you should refer to

  1750 in case of difficulties.  The package is simpler than ZF's, thanks to HOL's

  1751 automatic type-checking.  The type of the (co)inductive determines the

  1752 domain of the fixedpoint definition, and the package does not use inference

  1753 rules for type-checking.

  1754

  1755

  1756 \subsection{The result structure}

  1757 Many of the result structure's components have been discussed in the paper;

  1758 others are self-explanatory.

  1759 \begin{description}

  1760 \item[\tt thy] is the new theory containing the recursive sets.

  1761

  1762 \item[\tt defs] is the list of definitions of the recursive sets.

  1763

  1764 \item[\tt mono] is a monotonicity theorem for the fixedpoint operator.

  1765

  1766 \item[\tt unfold] is a fixedpoint equation for the recursive set (the union of

  1767 the recursive sets, in the case of mutual recursion).

  1768

  1769 \item[\tt intrs] is the list of introduction rules, now proved as theorems, for

  1770 the recursive sets.  The rules are also available individually, using the

  1771 names given them in the theory file.

  1772

  1773 \item[\tt elim] is the elimination rule.

  1774

  1775 \item[\tt mk\_cases] is a function to create simplified instances of {\tt

  1776 elim}, using freeness reasoning on some underlying datatype.

  1777 \end{description}

  1778

  1779 For an inductive definition, the result structure contains two induction rules,

  1780 {\tt induct} and \verb|mutual_induct|.  For a coinductive definition, it

  1781 contains the rule \verb|coinduct|.

  1782

  1783 Figure~\ref{def-result-fig} summarizes the two result signatures,

  1784 specifying the types of all these components.

  1785

  1786 \begin{figure}

  1787 \begin{ttbox}

  1788 sig

  1789 val thy          : theory

  1790 val defs         : thm list

  1791 val mono         : thm

  1792 val unfold       : thm

  1793 val intrs        : thm list

  1794 val elim         : thm

  1795 val mk_cases     : thm list -> string -> thm

  1796 {\it(Inductive definitions only)}

  1797 val induct       : thm

  1798 val mutual_induct: thm

  1799 {\it(Coinductive definitions only)}

  1800 val coinduct    : thm

  1801 end

  1802 \end{ttbox}

  1803 \hrule

  1804 \caption{The result of a (co)inductive definition} \label{def-result-fig}

  1805 \end{figure}

  1806

  1807 \subsection{The syntax of a (co)inductive definition}

  1808 An inductive definition has the form

  1809 \begin{ttbox}

  1810 inductive    {\it inductive sets}

  1811   intrs      {\it introduction rules}

  1812   monos      {\it monotonicity theorems}

  1813   con_defs   {\it constructor definitions}

  1814 \end{ttbox}

  1815 A coinductive definition is identical, except that it starts with the keyword

  1816 {\tt coinductive}.

  1817

  1818 The {\tt monos} and {\tt con\_defs} sections are optional.  If present,

  1819 each is specified as a string, which must be a valid ML expression of type

  1820 {\tt thm list}.  It is simply inserted into the {\tt .thy.ML} file; if it

  1821 is ill-formed, it will trigger ML error messages.  You can then inspect the

  1822 file on your directory.

  1823

  1824 \begin{itemize}

  1825 \item The {\it inductive sets} are specified by one or more strings.

  1826

  1827 \item The {\it introduction rules} specify one or more introduction rules in

  1828   the form {\it ident\/}~{\it string}, where the identifier gives the name of

  1829   the rule in the result structure.

  1830

  1831 \item The {\it monotonicity theorems} are required for each operator

  1832   applied to a recursive set in the introduction rules.  There {\bf must}

  1833   be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each

  1834   premise $t\in M(R_i)$ in an introduction rule!

  1835

  1836 \item The {\it constructor definitions} contain definitions of constants

  1837   appearing in the introduction rules.  In most cases it can be omitted.

  1838 \end{itemize}

  1839

  1840 The package has a few notable restrictions:

  1841 \begin{itemize}

  1842 \item The theory must separately declare the recursive sets as

  1843   constants.

  1844

  1845 \item The names of the recursive sets must be identifiers, not infix

  1846 operators.

  1847

  1848 \item Side-conditions must not be conjunctions.  However, an introduction rule

  1849 may contain any number of side-conditions.

  1850

  1851 \item Side-conditions of the form $x=t$, where the variable~$x$ does not

  1852   occur in~$t$, will be substituted through the rule \verb|mutual_induct|.

  1853 \end{itemize}

  1854

  1855

  1856 \subsection{Example of an inductive definition}

  1857 Two declarations, included in a theory file, define the finite powerset

  1858 operator.  First we declare the constant~{\tt Fin}.  Then we declare it

  1859 inductively, with two introduction rules:

  1860 \begin{ttbox}

  1861 consts Fin :: 'a set => 'a set set

  1862 inductive "Fin A"

  1863   intrs

  1864     emptyI  "\{\} : Fin A"

  1865     insertI "[| a: A;  b: Fin A |] ==> insert a b : Fin A"

  1866 \end{ttbox}

  1867 The resulting theory structure contains a substructure, called~{\tt Fin}.

  1868 It contains the {\tt Fin}$~A$ introduction rules as the list {\tt Fin.intrs},

  1869 and also individually as {\tt Fin.emptyI} and {\tt Fin.consI}.  The induction

  1870 rule is {\tt Fin.induct}.

  1871

  1872 For another example, here is a theory file defining the accessible part of a

  1873 relation.  The main thing to note is the use of~{\tt Pow} in the sole

  1874 introduction rule, and the corresponding mention of the rule

  1875 \verb|Pow_mono| in the {\tt monos} list.  The paper discusses a ZF version

  1876 of this example in more detail.

  1877 \begin{ttbox}

  1878 Acc = WF +

  1879 consts pred :: "['b, ('a * 'b)set] => 'a set"   (*Set of predecessors*)

  1880        acc  :: "('a * 'a)set => 'a set"         (*Accessible part*)

  1881 defs   pred_def  "pred x r == {y. (y,x):r}"

  1882 inductive "acc r"

  1883   intrs

  1884      pred "pred a r: Pow(acc r) ==> a: acc r"

  1885   monos   "[Pow_mono]"

  1886 end

  1887 \end{ttbox}

  1888 The HOL distribution contains many other inductive definitions, such as the

  1889 theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}.  The

  1890 theory {\tt HOL/ex/LList.thy} contains coinductive definitions.

  1891

  1892 \index{*coinductive|)} \index{*inductive|)} \underscoreoff

  1893

  1894

  1895 \section{The examples directories}

  1896 Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of

  1897 substitutions and unifiers.  It is based on Paulson's previous

  1898 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's

  1899 theory~\cite{mw81}.

  1900

  1901 Directory {\tt HOL/IMP} contains a formalization of the denotational,

  1902 operational and axiomatic semantics of a simple while-language, including an

  1903 equivalence proof between denotational and operational semantics and a

  1904 soundness and part of a completeness proof of the Hoare rules w.r.t.\ the

  1905 denotational semantics. The whole development is taken from

  1906 Winskel~\cite{winskel93}.  In addition, a verification-condition-generator is

  1907 proved sound and complete w.r.t. the Hoare rules.

  1908

  1909 Directory {\tt HOL/Hoare} contains a user friendly surface syntax for Hoare

  1910 logic, including a tactic for generating verification-conditions.

  1911

  1912 Directory {\tt HOL/ex} contains other examples and experimental proofs in

  1913 {\HOL}.  Here is an overview of the more interesting files.

  1914 \begin{itemize}

  1915 \item File {\tt cla.ML} demonstrates the classical reasoner on over sixty

  1916   predicate calculus theorems, ranging from simple tautologies to

  1917   moderately difficult problems involving equality and quantifiers.

  1918

  1919 \item File {\tt meson.ML} contains an experimental implementation of the {\sc

  1920     meson} proof procedure, inspired by Plaisted~\cite{plaisted90}.  It is

  1921   much more powerful than Isabelle's classical reasoner.  But it is less

  1922   useful in practice because it works only for pure logic; it does not

  1923   accept derived rules for the set theory primitives, for example.

  1924

  1925 \item File {\tt mesontest.ML} contains test data for the {\sc meson} proof

  1926   procedure.  These are mostly taken from Pelletier \cite{pelletier86}.

  1927

  1928 \item File {\tt set.ML} proves Cantor's Theorem, which is presented in

  1929   \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.

  1930

  1931 \item The definition of lazy lists demonstrates methods for handling

  1932   infinite data structures and coinduction in higher-order

  1933   logic~\cite{paulson-coind}.  Theory \thydx{LList} defines an operator for

  1934   corecursion on lazy lists, which is used to define a few simple functions

  1935   such as map and append.  Corecursion cannot easily define operations such

  1936   as filter, which can compute indefinitely before yielding the next

  1937   element (if any!) of the lazy list.  A coinduction principle is defined

  1938   for proving equations on lazy lists.

  1939

  1940 \item Theory {\tt PropLog} proves the soundness and completeness of

  1941   classical propositional logic, given a truth table semantics.  The only

  1942   connective is $\imp$.  A Hilbert-style axiom system is specified, and its

  1943   set of theorems defined inductively.  A similar proof in \ZF{} is

  1944   described elsewhere~\cite{paulson-set-II}.

  1945

  1946 \item Theory {\tt Term} develops an experimental recursive type definition;

  1947   the recursion goes through the type constructor~\tydx{list}.

  1948

  1949 \item Theory {\tt Simult} constructs mutually recursive sets of trees and

  1950   forests, including induction and recursion rules.

  1951

  1952 \item Theory {\tt MT} contains Jacob Frost's formalization~\cite{frost93} of

  1953   Milner and Tofte's coinduction example~\cite{milner-coind}.  This

  1954   substantial proof concerns the soundness of a type system for a simple

  1955   functional language.  The semantics of recursion is given by a cyclic

  1956   environment, which makes a coinductive argument appropriate.

  1957 \end{itemize}

  1958

  1959

  1960 \goodbreak

  1961 \section{Example: Cantor's Theorem}\label{sec:hol-cantor}

  1962 Cantor's Theorem states that every set has more subsets than it has

  1963 elements.  It has become a favourite example in higher-order logic since

  1964 it is so easily expressed:

  1965 $\forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.   1966 \forall x::\alpha. f~x \not= S   1967$

  1968 %

  1969 Viewing types as sets, $\alpha\To bool$ represents the powerset

  1970 of~$\alpha$.  This version states that for every function from $\alpha$ to

  1971 its powerset, some subset is outside its range.

  1972

  1973 The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and

  1974 the operator \cdx{range}.  The set~$S$ is given as an unknown instead of a

  1975 quantified variable so that we may inspect the subset found by the proof.

  1976 \begin{ttbox}

  1977 goal Set.thy "~ ?S : range(f :: 'a=>'a set)";

  1978 {\out Level 0}

  1979 {\out ~ ?S : range f}

  1980 {\out  1. ~ ?S : range f}

  1981 \end{ttbox}

  1982 The first two steps are routine.  The rule \tdx{rangeE} replaces

  1983 $\Var{S}\in {\tt range} f$ by $\Var{S}=f~x$ for some~$x$.

  1984 \begin{ttbox}

  1985 by (resolve_tac [notI] 1);

  1986 {\out Level 1}

  1987 {\out ~ ?S : range f}

  1988 {\out  1. ?S : range f ==> False}

  1989 \ttbreak

  1990 by (eresolve_tac [rangeE] 1);

  1991 {\out Level 2}

  1992 {\out ~ ?S : range f}

  1993 {\out  1. !!x. ?S = f x ==> False}

  1994 \end{ttbox}

  1995 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$,

  1996 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for

  1997 any~$\Var{c}$.

  1998 \begin{ttbox}

  1999 by (eresolve_tac [equalityCE] 1);

  2000 {\out Level 3}

  2001 {\out ~ ?S : range f}

  2002 {\out  1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False}

  2003 {\out  2. !!x. [| ~ ?c3 x : ?S; ~ ?c3 x : f x |] ==> False}

  2004 \end{ttbox}

  2005 Now we use a bit of creativity.  Suppose that~$\Var{S}$ has the form of a

  2006 comprehension.  Then $\Var{c}\in\{x.\Var{P}~x\}$ implies

  2007 $\Var{P}~\Var{c}$.   Destruct-resolution using \tdx{CollectD}

  2008 instantiates~$\Var{S}$ and creates the new assumption.

  2009 \begin{ttbox}

  2010 by (dresolve_tac [CollectD] 1);

  2011 {\out Level 4}

  2012 {\out ~ \{x. ?P7 x\} : range f}

  2013 {\out  1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False}

  2014 {\out  2. !!x. [| ~ ?c3 x : \{x. ?P7 x\}; ~ ?c3 x : f x |] ==> False}

  2015 \end{ttbox}

  2016 Forcing a contradiction between the two assumptions of subgoal~1 completes

  2017 the instantiation of~$S$.  It is now the set $\{x. x\not\in f~x\}$, which

  2018 is the standard diagonal construction.

  2019 \begin{ttbox}

  2020 by (contr_tac 1);

  2021 {\out Level 5}

  2022 {\out ~ \{x. ~ x : f x\} : range f}

  2023 {\out  1. !!x. [| ~ x : \{x. ~ x : f x\}; ~ x : f x |] ==> False}

  2024 \end{ttbox}

  2025 The rest should be easy.  To apply \tdx{CollectI} to the negated

  2026 assumption, we employ \ttindex{swap_res_tac}:

  2027 \begin{ttbox}

  2028 by (swap_res_tac [CollectI] 1);

  2029 {\out Level 6}

  2030 {\out ~ \{x. ~ x : f x\} : range f}

  2031 {\out  1. !!x. [| ~ x : f x; ~ False |] ==> ~ x : f x}

  2032 \ttbreak

  2033 by (assume_tac 1);

  2034 {\out Level 7}

  2035 {\out ~ \{x. ~ x : f x\} : range f}

  2036 {\out No subgoals!}

  2037 \end{ttbox}

  2038 How much creativity is required?  As it happens, Isabelle can prove this

  2039 theorem automatically.  The classical set \ttindex{set_cs} contains rules

  2040 for most of the constructs of \HOL's set theory.  We must augment it with

  2041 \tdx{equalityCE} to break up set equalities, and then apply best-first

  2042 search.  Depth-first search would diverge, but best-first search

  2043 successfully navigates through the large search space.

  2044 \index{search!best-first}

  2045 \begin{ttbox}

  2046 choplev 0;

  2047 {\out Level 0}

  2048 {\out ~ ?S : range f}

  2049 {\out  1. ~ ?S : range f}

  2050 \ttbreak

  2051 by (best_tac (set_cs addSEs [equalityCE]) 1);

  2052 {\out Level 1}

  2053 {\out ~ \{x. ~ x : f x\} : range f}

  2054 {\out No subgoals!}

  2055 \end{ttbox}

  2056

  2057 \index{higher-order logic|)}