doc-src/Logics/HOL.tex
 author paulson Tue Jan 23 11:10:39 1996 +0100 (1996-01-23) changeset 1448 77379ae9ff0d parent 1429 1f0009009219 child 1471 b088c0a1f2bd permissions -rw-r--r--
Stylistic changes to discussion of pattern-matching
     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::'a)

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

   214 \tdx{ext}            (!!x::'a. (f x::'b) = 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::'a) ==> 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::'a=>'b) y. @x. f x=y)

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

   238 \tdx{if_def}     If P x y == (\%P x y.@z::'a.(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::'a)

   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 \subcaption{Equality}

   303

   304 \tdx{TrueI}       True

   305 \tdx{FalseE}      False ==> P

   306

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

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

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

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

   311

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

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

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

   315

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

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

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

   319 \subcaption{Propositional logic}

   320

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

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

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

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

   325

   326 \tdx{eqTrueI}     P ==> P=True

   327 \tdx{eqTrueE}     P=True ==> P

   328 \subcaption{Logical equivalence}

   329

   330 \end{ttbox}

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

   332 \end{figure}

   333

   334

   335 \begin{figure}

   336 \begin{ttbox}\makeatother

   337 \tdx{allI}      (!!x::'a. P x) ==> !x. P x

   338 \tdx{spec}      !x::'a.P x ==> P x

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

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

   341

   342 \tdx{exI}       P x ==> ? x::'a.P x

   343 \tdx{exE}       [| ? x::'a.P x; !!x. P x ==> Q |] ==> Q

   344

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

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

   347           |] ==> R

   348

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

   350 \subcaption{Quantifiers and descriptions}

   351

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

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

   354 \tdx{excluded_middle} ~P | P

   355

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

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

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

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

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

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

   362 \subcaption{Classical logic}

   363

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

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

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

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

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

   369 \subcaption{Conditionals}

   370 \end{ttbox}

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

   372 \end{figure}

   373

   374

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

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

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

   378 conjunctions, implications, and universal quantifiers.

   379

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

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

   382 simplifying both sides of an equation.

   383

   384

   385 \begin{figure}

   386 \begin{center}

   387 \begin{tabular}{rrr}

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

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

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

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

   392         & insertion of element \\

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

   394         & comprehension \\

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

   396         & complement \\

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

   398         & intersection over a set\\

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

   400         & union over a set\\

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

   402         &set of sets intersection \\

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

   404         &set of sets union \\

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

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

   500 \subcaption{Full Grammar}

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

   502 \end{figure}

   503

   504

   505 \section{A formulation of set theory}

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

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

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

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

   510 \begin{itemize}

   511 \item

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

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

   514 \item

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

   516 may be defined by absolute comprehension.

   517 \item

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

   519 have a more complex type.

   520 \end{itemize}

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

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

   523 denoting the universal set for the given type.

   524

   525 % FIXME: define set via typedef

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

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

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

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

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

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

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

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

   534 argument order).

   535

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

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

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

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

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

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

   542

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

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

   545 \begin{eqnarray*}

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

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

   548 \end{eqnarray*}

   549

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

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

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

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

   555

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

   557 \begin{eqnarray*}

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

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

   560 \end{eqnarray*}

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

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

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

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

   565 %

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

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

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

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

   570

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

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

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

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

   575

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

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

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

   580

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

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

   583 respectively.

   584

   585

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

   587 \begin{figure} \underscoreon

   588 \begin{ttbox}

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

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

   591

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   614 \end{ttbox}

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

   616 \end{figure}

   617

   618

   619 \begin{figure} \underscoreon

   620 \begin{ttbox}

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

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

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

   624

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

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

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

   628

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

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

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

   632 \subcaption{Comprehension and Bounded quantifiers}

   633

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

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

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

   637

   638 \tdx{subset_refl}     A <= A

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

   640

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

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

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

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

   645

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

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

   648                 |]  ==>  P

   649 \subcaption{The subset and equality relations}

   650 \end{ttbox}

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

   652 \end{figure}

   653

   654

   655 \begin{figure} \underscoreon

   656 \begin{ttbox}

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

   658

   659 \tdx{insertI1} a : insert a B

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

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

   662

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

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

   665

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

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

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

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

   670

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

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

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

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

   675

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

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

   678

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

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

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

   682

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

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

   685

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

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

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

   689

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

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

   692 \end{ttbox}

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

   694 \end{figure}

   695

   696

   697 \subsection{Axioms and rules of set theory}

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

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

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

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

   702

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

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

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

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

   707 surjectiveness.

   708

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

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

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

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

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

   714

   715 \begin{figure} \underscoreon

   716 \begin{ttbox}

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

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

   719

   720 %\tdx{Inv_injective}

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

   722 %

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

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

   725

   726 \tdx{rangeI}     f x : range f

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

   728

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

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

   731

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

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

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

   735

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

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

   738

   739 \tdx{inj_onto_inverseI}

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

   741 \tdx{inj_onto_contraD}

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

   743 \end{ttbox}

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

   745 \end{figure}

   746

   747

   748 \begin{figure} \underscoreon

   749 \begin{ttbox}

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

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

   752

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

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

   755

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

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

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

   759

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

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

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

   763 \end{ttbox}

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

   765 \end{figure}

   766

   767

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

   769 \begin{ttbox}

   770 \tdx{Int_absorb}        A Int A = A

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

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

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

   774

   775 \tdx{Un_absorb}         A Un A = A

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

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

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

   779

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

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

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

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

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

   785

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

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

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

   789

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

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

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

   793 \end{ttbox}

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

   795 \end{figure}

   796

   797

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

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

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

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

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

   803 strictly necessary but yield more natural proofs.  Similarly,

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

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

   806 proofs pertaining to set theory.

   807

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

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

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

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

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

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

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

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

   816

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

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

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

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

   821

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

   823 include commutative, associative and distributive laws involving unions,

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

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

   826

   827

   828 \section{Generic packages}

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

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

   831

   832 \subsection{Substitution and simplification}

   833

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

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

   836 subgoal and its hypotheses.

   837

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

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

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

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

   842

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

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

   845 and simplification.

   846

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

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

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

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

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

   852   down rewriting and is therefore not included by default.

   853 \end{warn}

   854

   855 \subsection{Classical reasoning}

   856

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

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

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

   860

   861 The classical reasoner is set up as the structure

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

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

   864 \HOL\ defines the following classical rule sets:

   865 \begin{ttbox}

   866 prop_cs    : claset

   867 HOL_cs     : claset

   868 set_cs     : claset

   869 \end{ttbox}

   870 \begin{ttdescription}

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

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

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

   874

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

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

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

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

   879   once.

   880

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

   882   quantifiers, subsets, comprehensions, unions and intersections,

   883   complements, finite sets, images and ranges.

   884 \end{ttdescription}

   885 \noindent

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

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

   888 for more discussion of classical proof methods.

   889

   890

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

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

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

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

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

   896

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

   898

   899 \begin{figure}

   900 \begin{constants}

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

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

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

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

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

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

   907         & & generalized projection\\

   908   \cdx{Sigma}  &

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

   910         & general sum of sets

   911 \end{constants}

   912 \begin{ttbox}\makeatletter

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

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

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

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

   917

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

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

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

   921

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

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

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

   925

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

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

   928

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

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

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

   932 \end{ttbox}

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

   934 \end{figure}

   935

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

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

   938 simulated by pairs nested to the right:

   939 \begin{center}

   940 \begin{tabular}{|c|c|}

   941 \hline

   942 external & internal \\

   943 \hline

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

   945 \hline

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

   947 \hline

   948 \end{tabular}

   949 \end{center}

   950 In addition, it is possible to use tuples

   951 as patterns in abstractions:

   952 \begin{center}

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

   954 \end{center}

   955 Nested patterns are possible and are translated stepwise:

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

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

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

   959 \begin{warn}

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

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

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

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

   964   {\tt(b,a)}.

   965 \end{warn}

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

   967 variable binding construct which is internally described by a

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

   969 \begin{description}

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

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

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

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

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

   975 \end{description}

   976 % FIXME: remove comment in HOL/Prod.thy concerning printing

   977 % FIXME: remove ML code from HOL/Prod.thy

   978

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

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

   981 \begin{ttbox}

   982 \tdx{unit_eq}       u = ()

   983 \end{ttbox}

   984 \bigskip

   985

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

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

   989

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

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

   992   thy}-files.

   993

   994 \begin{figure}

   995 \begin{constants}

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

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

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

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

  1000         & & conditional

  1001 \end{constants}

  1002 \begin{ttbox}\makeatletter

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

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

  1005 %

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

  1007

  1008 \tdx{inj_Inl}        inj Inl

  1009 \tdx{inj_Inr}        inj Inr

  1010

  1011 \tdx{sumE}           [| !!x::'a. P(Inl x);  !!y::'b. P(Inr y) |] ==> P s

  1012

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

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

  1015

  1016 \tdx{surjective_sum} sum_case (\%x::'a. f(Inl x)) (\%y::'b. f(Inr y)) s = f s

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

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

  1019 \end{ttbox}

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

  1021 \end{figure}

  1022

  1023 \begin{figure}

  1024 \index{*"< symbol}

  1025 \index{*"* symbol}

  1026 \index{*div symbol}

  1027 \index{*mod symbol}

  1028 \index{*"+ symbol}

  1029 \index{*"- symbol}

  1030 \begin{constants}

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

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

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

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

  1035         & & conditional\\

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

  1037         & & primitive recursor\\

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

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

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

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

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

  1043 \end{constants}

  1044 \subcaption{Constants and infixes}

  1045

  1046 \begin{ttbox}\makeatother

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

  1048

  1049 \tdx{Suc_not_Zero}   Suc m ~= 0

  1050 \tdx{inj_Suc}        inj Suc

  1051 \tdx{n_not_Suc_n}    n~=Suc n

  1052 \subcaption{Basic properties}

  1053 \end{ttbox}

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

  1055 \end{figure}

  1056

  1057

  1058 \begin{figure}

  1059 \begin{ttbox}\makeatother

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

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

  1062

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

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

  1065

  1066 \tdx{add_0}        0+n           = n

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

  1068 \tdx{diff_0}       m-0           = m

  1069 \tdx{diff_0_eq_0}  0-n           = n

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

  1071 \tdx{mult_def}     0*n           = 0

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

  1073

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

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

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

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

  1078 \subcaption{Recursion equations}

  1079

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

  1081 \tdx{lessI}          n < Suc n

  1082 \tdx{zero_less_Suc}  0 < Suc n

  1083

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

  1085 \tdx{less_not_refl}  ~ n<n

  1086 \tdx{not_less0}      ~ n<0

  1087

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

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

  1090

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

  1092 \subcaption{The less-than relation}

  1093 \end{ttbox}

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

  1095 \end{figure}

  1096

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

  1098 %FIXME: introduce separate type proto_nat

  1099

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

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

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

  1103 The natural numbers are inductively generated by choosing an arbitrary

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

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

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

  1107

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

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

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

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

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

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

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

  1115

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

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

  1118

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

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

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

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

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

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

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

  1126 and~\ref{hol-nat2}.

  1127

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

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

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

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

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

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

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

  1135

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

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

  1138

  1139 %FIXME add nth

  1140 \begin{figure}

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

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

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

  1144 \begin{constants}

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

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

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

  1148         list constructor \\

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

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

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

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

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

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

  1155         & & mapping functional\\

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

  1157         & & filter functional\\

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

  1159         & & forall functional\\

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

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

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

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

  1164   & iteration \\

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

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

  1167 \end{constants}

  1168 \subcaption{Constants and infixes}

  1169

  1170 \begin{center} \tt\frenchspacing

  1171 \begin{tabular}{rrr}

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

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

  1174         \rm finite list \\{}

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

  1176         \rm list comprehension

  1177 \end{tabular}

  1178 \end{center}

  1179 \subcaption{Translations}

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

  1181 \end{figure}

  1182

  1183

  1184 \begin{figure}

  1185 \begin{ttbox}\makeatother

  1186 \tdx{null_Nil}        null [] = True

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

  1188

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

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

  1191

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

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

  1194

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

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

  1197

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

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

  1200

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

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

  1203

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

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

  1206

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

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

  1209

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

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

  1212

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

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

  1215

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

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

  1218

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

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

  1221 \end{ttbox}

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

  1223 \end{figure}

  1224

  1225

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

  1227 \index{*list type}

  1228

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

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

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

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

  1233 theorems {\tt list.simps}.

  1234 A \sdx{case} construct of the form

  1235 \begin{center}\tt

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

  1237 \end{center}

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

  1239

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

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

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

  1243

  1244

  1245 \subsection{Introducing new types}

  1246 %FIXME: syntax of typedef: subtype -> typedef; name -> id

  1247 %FIXME: typevarlist and infix/mixfix in Ref manual and in sec:datatype

  1248

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

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

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

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

  1253 described elsewhere.

  1254 \begin{warn}

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

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

  1257 \end{warn}

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

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

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

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

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

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

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

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

  1266

  1267 \begin{figure}[htbp]

  1268 \begin{rail}

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

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

  1271 tname   : name;

  1272 set     : string;

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

  1274 \end{rail}

  1275 \caption{Syntax of type definition}

  1276 \label{fig:HOL:typedef}

  1277 \end{figure}

  1278

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

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

  1281 \iflabelundefined{chap:classical}

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

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

  1284 following meaning:

  1285 \begin{description}

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

  1287   optional infix annotation.

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

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

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

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

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

  1293   non-emptiness automatically.

  1294 \end{description}

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

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

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

  1298 \begin{itemize}

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

  1300 \item constants

  1301 \begin{eqnarray*}

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

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

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

  1305 \end{eqnarray*}

  1306 \item a definition and three axioms

  1307 $  1308 \begin{array}{ll}   1309 T{\tt_def} & T \equiv A \\   1310 {\tt Rep_}T & Rep_T(x) : T \\   1311 {\tt Rep_}T{\tt_inverse} & Abs_T(Rep_T(x)) = x \\   1312 {\tt Abs_}T{\tt_inverse} & y:T \Imp Rep_T(Abs_T(y)) = y   1313 \end{array}   1314$

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

  1316 and its inverse $Abs_T$.

  1317 \end{itemize}

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

  1319 \begin{ttbox}

  1320 typedef unit = "\{False\}"

  1321

  1322 typedef (prod)

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

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

  1325 \end{ttbox}

  1326

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

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

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

  1330 \begin{enumerate}

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

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

  1333   representation.

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

  1335 \end{enumerate}

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

  1337 abstract properties $P$.

  1338

  1339 \begin{warn}

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

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

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

  1343 \par

  1344 \begin{ttbox}

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

  1346 \end{ttbox}

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

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

  1349 \end{warn}

  1350

  1351 \section{Datatype declarations}

  1352 \label{sec:HOL:datatype}

  1353 \index{*datatype|(}

  1354

  1355 \underscoreon

  1356

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

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

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

  1360   datatype} represents a compact way of doing this.

  1361

  1362

  1363 \subsection{Foundations}

  1364

  1365 A datatype declaration has the following general structure:

  1366 $\mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~   1367 C_1~\tau_{11}~\dots~\tau_{1k_1} ~\mid~ \dots ~\mid~   1368 C_m~\tau_{m1}~\dots~\tau_{mk_m}   1369$

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

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

  1372 \begin{itemize}

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

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

  1375   type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq   1376 \{\alpha_1,\dots,\alpha_n\}$,

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

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

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

  1380     components.}

  1381 \end{itemize}

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

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

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

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

  1388

  1389 The constructors are automatically defined as functions of their respective

  1390 type:

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

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

  1393 \begin{description}

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

  1395 $C_i~x_1~\dots~x_{k_i} \neq C_j~y_1~\dots~y_{k_j} \qquad   1396 \mbox{for all}~ i \neq j.   1397$

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

  1399 $(C_j~x_1~\dots~x_{k_j} = C_j~y_1~\dots~y_{k_j}) =   1400 (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j})   1401$

  1402 \end{description}

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

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

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

  1406 natural number

  1407 $  1408 \begin{array}{lcl}   1409 \mbox{\it t\_ord}(C_1~x_1~\dots~x_{k_1}) & = & 0 \\   1410 & \vdots & \\   1411 \mbox{\it t\_ord}(C_m x_1~\dots~x_{k_m}) & = & m-1   1412 \end{array}   1413$

  1414 and distinctness of constructors is expressed by:

  1415 $  1416 \mbox{\it t\_ord}~x \neq \mbox{\it t\_ord}~y \Imp x \neq y.   1417$

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

  1419 $  1420 \infer{P x}   1421 {\begin{array}{lcl}   1422 \Forall x_1\dots x_{k_1}.   1423 \List{P~x_{r_{11}}; \dots; P~x_{r_{1l_1}}} &   1424 \Imp & P(C_1~x_1~\dots~x_{k_1}) \\   1425 & \vdots & \\   1426 \Forall x_1\dots x_{k_m}.   1427 \List{P~x_{r_{m1}}; \dots; P~x_{r_{ml_m}}} &   1428 \Imp & P(C_m~x_1~\dots~x_{k_m})   1429 \end{array}}   1430$

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

  1433 all arguments of the recursive type.

  1434

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

  1436 $  1437 \begin{array}{rrcl}   1438 \mbox{\tt case}~e~\mbox{\tt of} & C_1~x_{11}~\dots~x_{1k_1} & \To & e_1 \\   1439 \vdots \\   1440 \mid & C_m~x_{m1}~\dots~x_{mk_m} & \To & e_m   1441 \end{array}   1442$

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

  1444 fixed, and nested patterns are not supported.

  1445

  1446

  1447 \subsection{Defining datatypes}

  1448

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

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

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

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

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

  1454 section.

  1455

  1456 \begin{figure}

  1457 \begin{rail}

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

  1459          ;

  1460 cons     : (id | string) ( () | '(' (typ + ',') ')' ) ( () | mixfix )

  1461          ;

  1462 typ      : typevarlist id

  1463            | tid

  1464          ;

  1465 typevarlist : () | tid | '(' (tid + ',') ')'

  1466          ;

  1467 \end{rail}

  1468 \caption{Syntax of datatype declarations}

  1469 \label{datatype-grammar}

  1470 \end{figure}

  1471

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

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

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

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

  1476 \begin{ttbox}

  1477 val distinct : thm list

  1478 val inject : thm list

  1479 val induct : thm

  1480 val cases : thm list

  1481 val simps : thm list

  1482 val induct_tac : string -> int -> tactic

  1483 \end{ttbox}

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

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

  1486 directions.

  1487 \begin{warn}

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

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

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

  1491 \end{warn}

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

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

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

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

  1496 subgoal {\em i}.

  1497

  1498

  1499 \subsection{Examples}

  1500

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

  1502

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

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

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

  1506 \begin{ttbox}

  1507 MyList = HOL +

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

  1509 end

  1510 \end{ttbox}

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

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

  1513 \begin{ttbox}

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

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

  1516 {\out Level 0}

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

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

  1519 \end{ttbox}

  1520 This can be proved by the structural induction tactic:

  1521 \begin{ttbox}

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

  1523 {\out Level 1}

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

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

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

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

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

  1529 \end{ttbox}

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

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

  1532 \begin{ttbox}

  1533 by (simp_tac mylist_ss 1);

  1534 {\out Level 2}

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

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

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

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

  1539 \end{ttbox}

  1540 Using the freeness axioms we can quickly prove the remaining goal.

  1541 \begin{ttbox}

  1542 by (asm_simp_tac mylist_ss 1);

  1543 {\out Level 3}

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

  1545 {\out No subgoals!}

  1546 \end{ttbox}

  1547 Because both subgoals were proved by almost the same tactic we could have

  1548 done that in one step using

  1549 \begin{ttbox}

  1550 by (ALLGOALS (asm_simp_tac mylist_ss));

  1551 \end{ttbox}

  1552

  1553

  1554 \subsubsection{The datatype $\alpha~list$ with mixfix syntax}

  1555

  1556 In this example we define the type $\alpha~list$ again but this time we want

  1557 to write {\tt []} instead of {\tt Nil} and we want to use the infix operator

  1558 \verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations

  1559 after the constructor declarations as follows:

  1560 \begin{ttbox}

  1561 MyList = HOL +

  1562   datatype 'a list = "[]" ("[]")

  1563                    | "#" 'a ('a list) (infixr 70)

  1564 end

  1565 \end{ttbox}

  1566 Now the theorem in the previous example can be written \verb|x#xs ~= xs|. The

  1567 proof is the same.

  1568

  1569

  1570 \subsubsection{A datatype for weekdays}

  1571

  1572 This example shows a datatype that consists of more than four constructors:

  1573 \begin{ttbox}

  1574 Days = Arith +

  1575   datatype days = Mo | Tu | We | Th | Fr | Sa | So

  1576 end

  1577 \end{ttbox}

  1578 Because there are more than four constructors, the theory must be based on

  1579 {\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although

  1580 the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct},

  1581 it can be proved by the simplifier if \verb$arith_ss$ is used:

  1582 \begin{ttbox}

  1583 val days_ss = arith_ss addsimps Days.days.simps;

  1584

  1585 goal Days.thy "Mo ~= Tu";

  1586 by (simp_tac days_ss 1);

  1587 \end{ttbox}

  1588 Note that usually it is not necessary to derive these inequalities explicitly

  1589 because the simplifier will dispose of them automatically.

  1590

  1591 \subsection{Primitive recursive functions}

  1592 \label{sec:HOL:primrec}

  1593 \index{primitive recursion|(}

  1594 \index{*primrec|(}

  1595

  1596 Datatypes come with a uniform way of defining functions, {\bf primitive

  1597   recursion}. Although it is possible to define primitive recursive functions

  1598 by asserting their reduction rules as new axioms, e.g.\

  1599 \begin{ttbox}

  1600 Append = MyList +

  1601 consts app :: ['a list,'a list] => 'a list

  1602 rules

  1603    app_Nil   "app [] ys = ys"

  1604    app_Cons  "app (x#xs) ys = x#app xs ys"

  1605 end

  1606 \end{ttbox}

  1607 this carries with it the danger of accidentally asserting an inconsistency,

  1608 as in \verb$app [] ys = us$. Therefore primitive recursive functions on

  1609 datatypes can be defined with a special syntax:

  1610 \begin{ttbox}

  1611 Append = MyList +

  1612 consts app :: ['a list,'a list] => 'a list

  1613 primrec app MyList.list

  1614    app_Nil   "app [] ys = ys"

  1615    app_Cons  "app (x#xs) ys = x#app xs ys"

  1616 end

  1617 \end{ttbox}

  1618 The system will now check that the two rules \verb$app_Nil$ and

  1619 \verb$app_Cons$ do indeed form a primitive recursive definition, thus

  1620 ensuring that consistency is maintained. For example

  1621 \begin{ttbox}

  1622 primrec app MyList.list

  1623     app_Nil   "app [] ys = us"

  1624 \end{ttbox}

  1625 is rejected:

  1626 \begin{ttbox}

  1627 Extra variables on rhs

  1628 \end{ttbox}

  1629 \bigskip

  1630

  1631 The general form of a primitive recursive definition is

  1632 \begin{ttbox}

  1633 primrec {\it function} {\it type}

  1634     {\it reduction rules}

  1635 \end{ttbox}

  1636 where

  1637 \begin{itemize}

  1638 \item {\it function} is the name of the function, either as an {\it id} or a

  1639   {\it string}. The function must already have been declared.

  1640 \item {\it type} is the name of the datatype, either as an {\it id} or in the

  1641   long form {\it Thy.t}, where {\it Thy} is the name of the parent theory the

  1642   datatype was declared in, and $t$ the name of the datatype. The long form

  1643   is required if the {\tt datatype} and the {\tt primrec} sections are in

  1644   different theories.

  1645 \item {\it reduction rules} specify one or more named equations of the form

  1646   {\it id\/}~{\it string}, where the identifier gives the name of the rule in

  1647   the result structure, and {\it string} is a reduction rule of the form $  1648 f~x_1~\dots~x_m~(C~y_1~\dots~y_k)~z_1~\dots~z_n = r$ such that $C$ is a

  1649   constructor of the datatype, $r$ contains only the free variables on the

  1650   left-hand side, and all recursive calls in $r$ are of the form

  1651   $f~\dots~y_i~\dots$ for some $i$. There must be exactly one reduction

  1652   rule for each constructor.

  1653 \end{itemize}

  1654 A theory file may contain any number of {\tt primrec} sections which may be

  1655 intermixed with other declarations.

  1656

  1657 For the consistency-sensitive user it may be reassuring to know that {\tt

  1658   primrec} does not assert the reduction rules as new axioms but derives them

  1659 as theorems from an explicit definition of the recursive function in terms of

  1660 a recursion operator on the datatype.

  1661

  1662 The primitive recursive function can also use infix or mixfix syntax:

  1663 \begin{ttbox}

  1664 Append = MyList +

  1665 consts "@"  :: ['a list,'a list] => 'a list  (infixr 60)

  1666 primrec "op @" MyList.list

  1667    app_Nil   "[] @ ys = ys"

  1668    app_Cons  "(x#xs) @ ys = x#(xs @ ys)"

  1669 end

  1670 \end{ttbox}

  1671

  1672 The reduction rules become part of the ML structure \verb$Append$ and can

  1673 be used to prove theorems about the function:

  1674 \begin{ttbox}

  1675 val append_ss = HOL_ss addsimps [Append.app_Nil,Append.app_Cons];

  1676

  1677 goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)";

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

  1679 by (ALLGOALS(asm_simp_tac append_ss));

  1680 \end{ttbox}

  1681

  1682 %Note that underdefined primitive recursive functions are allowed:

  1683 %\begin{ttbox}

  1684 %Tl = MyList +

  1685 %consts tl  :: 'a list => 'a list

  1686 %primrec tl MyList.list

  1687 %   tl_Cons "tl(x#xs) = xs"

  1688 %end

  1689 %\end{ttbox}

  1690 %Nevertheless {\tt tl} is total, although we do not know what the result of

  1691 %\verb$tl([])$ is.

  1692

  1693 \index{primitive recursion|)}

  1694 \index{*primrec|)}

  1695 \index{*datatype|)}

  1696

  1697

  1698 \section{Inductive and coinductive definitions}

  1699 \index{*inductive|(}

  1700 \index{*coinductive|(}

  1701

  1702 An {\bf inductive definition} specifies the least set closed under given

  1703 rules.  For example, a structural operational semantics is an inductive

  1704 definition of an evaluation relation.  Dually, a {\bf coinductive

  1705   definition} specifies the greatest set closed under given rules.  An

  1706 important example is using bisimulation relations to formalize equivalence

  1707 of processes and infinite data structures.

  1708

  1709 A theory file may contain any number of inductive and coinductive

  1710 definitions.  They may be intermixed with other declarations; in

  1711 particular, the (co)inductive sets {\bf must} be declared separately as

  1712 constants, and may have mixfix syntax or be subject to syntax translations.

  1713

  1714 Each (co)inductive definition adds definitions to the theory and also

  1715 proves some theorems.  Each definition creates an ML structure, which is a

  1716 substructure of the main theory structure.

  1717

  1718 This package is derived from the ZF one, described in a

  1719 separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a

  1720   longer version is distributed with Isabelle.} which you should refer to

  1721 in case of difficulties.  The package is simpler than ZF's, thanks to HOL's

  1722 automatic type-checking.  The type of the (co)inductive determines the

  1723 domain of the fixedpoint definition, and the package does not use inference

  1724 rules for type-checking.

  1725

  1726

  1727 \subsection{The result structure}

  1728 Many of the result structure's components have been discussed in the paper;

  1729 others are self-explanatory.

  1730 \begin{description}

  1731 \item[\tt thy] is the new theory containing the recursive sets.

  1732

  1733 \item[\tt defs] is the list of definitions of the recursive sets.

  1734

  1735 \item[\tt mono] is a monotonicity theorem for the fixedpoint operator.

  1736

  1737 \item[\tt unfold] is a fixedpoint equation for the recursive set (the union of

  1738 the recursive sets, in the case of mutual recursion).

  1739

  1740 \item[\tt intrs] is the list of introduction rules, now proved as theorems, for

  1741 the recursive sets.  The rules are also available individually, using the

  1742 names given them in the theory file.

  1743

  1744 \item[\tt elim] is the elimination rule.

  1745

  1746 \item[\tt mk\_cases] is a function to create simplified instances of {\tt

  1747 elim}, using freeness reasoning on some underlying datatype.

  1748 \end{description}

  1749

  1750 For an inductive definition, the result structure contains two induction rules,

  1751 {\tt induct} and \verb|mutual_induct|.  For a coinductive definition, it

  1752 contains the rule \verb|coinduct|.

  1753

  1754 Figure~\ref{def-result-fig} summarizes the two result signatures,

  1755 specifying the types of all these components.

  1756

  1757 \begin{figure}

  1758 \begin{ttbox}

  1759 sig

  1760 val thy          : theory

  1761 val defs         : thm list

  1762 val mono         : thm

  1763 val unfold       : thm

  1764 val intrs        : thm list

  1765 val elim         : thm

  1766 val mk_cases     : thm list -> string -> thm

  1767 {\it(Inductive definitions only)}

  1768 val induct       : thm

  1769 val mutual_induct: thm

  1770 {\it(Coinductive definitions only)}

  1771 val coinduct    : thm

  1772 end

  1773 \end{ttbox}

  1774 \hrule

  1775 \caption{The result of a (co)inductive definition} \label{def-result-fig}

  1776 \end{figure}

  1777

  1778 \subsection{The syntax of a (co)inductive definition}

  1779 An inductive definition has the form

  1780 \begin{ttbox}

  1781 inductive    {\it inductive sets}

  1782   intrs      {\it introduction rules}

  1783   monos      {\it monotonicity theorems}

  1784   con_defs   {\it constructor definitions}

  1785 \end{ttbox}

  1786 A coinductive definition is identical, except that it starts with the keyword

  1787 {\tt coinductive}.

  1788

  1789 The {\tt monos} and {\tt con\_defs} sections are optional.  If present,

  1790 each is specified as a string, which must be a valid ML expression of type

  1791 {\tt thm list}.  It is simply inserted into the {\tt .thy.ML} file; if it

  1792 is ill-formed, it will trigger ML error messages.  You can then inspect the

  1793 file on your directory.

  1794

  1795 \begin{itemize}

  1796 \item The {\it inductive sets} are specified by one or more strings.

  1797

  1798 \item The {\it introduction rules} specify one or more introduction rules in

  1799   the form {\it ident\/}~{\it string}, where the identifier gives the name of

  1800   the rule in the result structure.

  1801

  1802 \item The {\it monotonicity theorems} are required for each operator

  1803   applied to a recursive set in the introduction rules.  There {\bf must}

  1804   be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each

  1805   premise $t\in M(R_i)$ in an introduction rule!

  1806

  1807 \item The {\it constructor definitions} contain definitions of constants

  1808   appearing in the introduction rules.  In most cases it can be omitted.

  1809 \end{itemize}

  1810

  1811 The package has a few notable restrictions:

  1812 \begin{itemize}

  1813 \item The theory must separately declare the recursive sets as

  1814   constants.

  1815

  1816 \item The names of the recursive sets must be identifiers, not infix

  1817 operators.

  1818

  1819 \item Side-conditions must not be conjunctions.  However, an introduction rule

  1820 may contain any number of side-conditions.

  1821

  1822 \item Side-conditions of the form $x=t$, where the variable~$x$ does not

  1823   occur in~$t$, will be substituted through the rule \verb|mutual_induct|.

  1824 \end{itemize}

  1825

  1826

  1827 \subsection{Example of an inductive definition}

  1828 Two declarations, included in a theory file, define the finite powerset

  1829 operator.  First we declare the constant~{\tt Fin}.  Then we declare it

  1830 inductively, with two introduction rules:

  1831 \begin{ttbox}

  1832 consts Fin :: 'a set => 'a set set

  1833 inductive "Fin A"

  1834   intrs

  1835     emptyI  "\{\} : Fin A"

  1836     insertI "[| a: A;  b: Fin A |] ==> insert a b : Fin A"

  1837 \end{ttbox}

  1838 The resulting theory structure contains a substructure, called~{\tt Fin}.

  1839 It contains the {\tt Fin}$~A$ introduction rules as the list {\tt Fin.intrs},

  1840 and also individually as {\tt Fin.emptyI} and {\tt Fin.consI}.  The induction

  1841 rule is {\tt Fin.induct}.

  1842

  1843 For another example, here is a theory file defining the accessible part of a

  1844 relation.  The main thing to note is the use of~{\tt Pow} in the sole

  1845 introduction rule, and the corresponding mention of the rule

  1846 \verb|Pow_mono| in the {\tt monos} list.  The paper discusses a ZF version

  1847 of this example in more detail.

  1848 \begin{ttbox}

  1849 Acc = WF +

  1850 consts pred :: "['b, ('a * 'b)set] => 'a set"   (*Set of predecessors*)

  1851        acc  :: "('a * 'a)set => 'a set"         (*Accessible part*)

  1852 defs   pred_def  "pred x r == {y. (y,x):r}"

  1853 inductive "acc r"

  1854   intrs

  1855      pred "pred a r: Pow(acc r) ==> a: acc r"

  1856   monos   "[Pow_mono]"

  1857 end

  1858 \end{ttbox}

  1859 The HOL distribution contains many other inductive definitions, such as the

  1860 theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}.  The

  1861 theory {\tt HOL/ex/LList.thy} contains coinductive definitions.

  1862

  1863 \index{*coinductive|)} \index{*inductive|)} \underscoreoff

  1864

  1865

  1866 \section{The examples directories}

  1867 Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of

  1868 substitutions and unifiers.  It is based on Paulson's previous

  1869 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's

  1870 theory~\cite{mw81}.

  1871

  1872 Directory {\tt HOL/IMP} contains a mechanised version of a semantic

  1873 equivalence proof taken from Winskel~\cite{winskel93}.  It formalises the

  1874 denotational and operational semantics of a simple while-language, then

  1875 proves the two equivalent.  It contains several datatype and inductive

  1876 definitions, and demonstrates their use.

  1877

  1878 Directory {\tt HOL/ex} contains other examples and experimental proofs in

  1879 {\HOL}.  Here is an overview of the more interesting files.

  1880 \begin{itemize}

  1881 \item File {\tt cla.ML} demonstrates the classical reasoner on over sixty

  1882   predicate calculus theorems, ranging from simple tautologies to

  1883   moderately difficult problems involving equality and quantifiers.

  1884

  1885 \item File {\tt meson.ML} contains an experimental implementation of the {\sc

  1886     meson} proof procedure, inspired by Plaisted~\cite{plaisted90}.  It is

  1887   much more powerful than Isabelle's classical reasoner.  But it is less

  1888   useful in practice because it works only for pure logic; it does not

  1889   accept derived rules for the set theory primitives, for example.

  1890

  1891 \item File {\tt mesontest.ML} contains test data for the {\sc meson} proof

  1892   procedure.  These are mostly taken from Pelletier \cite{pelletier86}.

  1893

  1894 \item File {\tt set.ML} proves Cantor's Theorem, which is presented in

  1895   \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.

  1896

  1897 \item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of

  1898   insertion sort and quick sort.

  1899

  1900 \item The definition of lazy lists demonstrates methods for handling

  1901   infinite data structures and coinduction in higher-order

  1902   logic~\cite{paulson-coind}.  Theory \thydx{LList} defines an operator for

  1903   corecursion on lazy lists, which is used to define a few simple functions

  1904   such as map and append.  Corecursion cannot easily define operations such

  1905   as filter, which can compute indefinitely before yielding the next

  1906   element (if any!) of the lazy list.  A coinduction principle is defined

  1907   for proving equations on lazy lists.

  1908

  1909 \item Theory {\tt PropLog} proves the soundness and completeness of

  1910   classical propositional logic, given a truth table semantics.  The only

  1911   connective is $\imp$.  A Hilbert-style axiom system is specified, and its

  1912   set of theorems defined inductively.  A similar proof in \ZF{} is

  1913   described elsewhere~\cite{paulson-set-II}.

  1914

  1915 \item Theory {\tt Term} develops an experimental recursive type definition;

  1916   the recursion goes through the type constructor~\tydx{list}.

  1917

  1918 \item Theory {\tt Simult} constructs mutually recursive sets of trees and

  1919   forests, including induction and recursion rules.

  1920

  1921 \item Theory {\tt MT} contains Jacob Frost's formalization~\cite{frost93} of

  1922   Milner and Tofte's coinduction example~\cite{milner-coind}.  This

  1923   substantial proof concerns the soundness of a type system for a simple

  1924   functional language.  The semantics of recursion is given by a cyclic

  1925   environment, which makes a coinductive argument appropriate.

  1926 \end{itemize}

  1927

  1928

  1929 \goodbreak

  1930 \section{Example: Cantor's Theorem}\label{sec:hol-cantor}

  1931 Cantor's Theorem states that every set has more subsets than it has

  1932 elements.  It has become a favourite example in higher-order logic since

  1933 it is so easily expressed:

  1934 $\forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.   1935 \forall x::\alpha. f~x \not= S   1936$

  1937 %

  1938 Viewing types as sets, $\alpha\To bool$ represents the powerset

  1939 of~$\alpha$.  This version states that for every function from $\alpha$ to

  1940 its powerset, some subset is outside its range.

  1941

  1942 The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and

  1943 the operator \cdx{range}.  The set~$S$ is given as an unknown instead of a

  1944 quantified variable so that we may inspect the subset found by the proof.

  1945 \begin{ttbox}

  1946 goal Set.thy "~ ?S : range(f :: 'a=>'a set)";

  1947 {\out Level 0}

  1948 {\out ~ ?S : range f}

  1949 {\out  1. ~ ?S : range f}

  1950 \end{ttbox}

  1951 The first two steps are routine.  The rule \tdx{rangeE} replaces

  1952 $\Var{S}\in {\tt range} f$ by $\Var{S}=f~x$ for some~$x$.

  1953 \begin{ttbox}

  1954 by (resolve_tac [notI] 1);

  1955 {\out Level 1}

  1956 {\out ~ ?S : range f}

  1957 {\out  1. ?S : range f ==> False}

  1958 \ttbreak

  1959 by (eresolve_tac [rangeE] 1);

  1960 {\out Level 2}

  1961 {\out ~ ?S : range f}

  1962 {\out  1. !!x. ?S = f x ==> False}

  1963 \end{ttbox}

  1964 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$,

  1965 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for

  1966 any~$\Var{c}$.

  1967 \begin{ttbox}

  1968 by (eresolve_tac [equalityCE] 1);

  1969 {\out Level 3}

  1970 {\out ~ ?S : range f}

  1971 {\out  1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False}

  1972 {\out  2. !!x. [| ~ ?c3 x : ?S; ~ ?c3 x : f x |] ==> False}

  1973 \end{ttbox}

  1974 Now we use a bit of creativity.  Suppose that~$\Var{S}$ has the form of a

  1975 comprehension.  Then $\Var{c}\in\{x.\Var{P}~x\}$ implies

  1976 $\Var{P}~\Var{c}$.   Destruct-resolution using \tdx{CollectD}

  1977 instantiates~$\Var{S}$ and creates the new assumption.

  1978 \begin{ttbox}

  1979 by (dresolve_tac [CollectD] 1);

  1980 {\out Level 4}

  1981 {\out ~ \{x. ?P7 x\} : range f}

  1982 {\out  1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False}

  1983 {\out  2. !!x. [| ~ ?c3 x : \{x. ?P7 x\}; ~ ?c3 x : f x |] ==> False}

  1984 \end{ttbox}

  1985 Forcing a contradiction between the two assumptions of subgoal~1 completes

  1986 the instantiation of~$S$.  It is now the set $\{x. x\not\in f~x\}$, which

  1987 is the standard diagonal construction.

  1988 \begin{ttbox}

  1989 by (contr_tac 1);

  1990 {\out Level 5}

  1991 {\out ~ \{x. ~ x : f x\} : range f}

  1992 {\out  1. !!x. [| ~ x : \{x. ~ x : f x\}; ~ x : f x |] ==> False}

  1993 \end{ttbox}

  1994 The rest should be easy.  To apply \tdx{CollectI} to the negated

  1995 assumption, we employ \ttindex{swap_res_tac}:

  1996 \begin{ttbox}

  1997 by (swap_res_tac [CollectI] 1);

  1998 {\out Level 6}

  1999 {\out ~ \{x. ~ x : f x\} : range f}

  2000 {\out  1. !!x. [| ~ x : f x; ~ False |] ==> ~ x : f x}

  2001 \ttbreak

  2002 by (assume_tac 1);

  2003 {\out Level 7}

  2004 {\out ~ \{x. ~ x : f x\} : range f}

  2005 {\out No subgoals!}

  2006 \end{ttbox}

  2007 How much creativity is required?  As it happens, Isabelle can prove this

  2008 theorem automatically.  The classical set \ttindex{set_cs} contains rules

  2009 for most of the constructs of \HOL's set theory.  We must augment it with

  2010 \tdx{equalityCE} to break up set equalities, and then apply best-first

  2011 search.  Depth-first search would diverge, but best-first search

  2012 successfully navigates through the large search space.

  2013 \index{search!best-first}

  2014 \begin{ttbox}

  2015 choplev 0;

  2016 {\out Level 0}

  2017 {\out ~ ?S : range f}

  2018 {\out  1. ~ ?S : range f}

  2019 \ttbreak

  2020 by (best_tac (set_cs addSEs [equalityCE]) 1);

  2021 {\out Level 1}

  2022 {\out ~ \{x. ~ x : f x\} : range f}

  2023 {\out No subgoals!}

  2024 \end{ttbox}

  2025

  2026 \index{higher-order logic|)}