99 Figure~\ref{hol-constants} lists the constants (including infixes and
100 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
107   if-and-only-if typically has the lowest priority.  Thus, $\lnot\lnot P=P$
115 particular the equality symbol and quantifiers are polymorphic over
126 either using the primitive \texttt{typedef} or the more convenient
131 \cldx{power} --- permit overloading of the operators {\tt+},\index{*"+
135 They are overloaded to denote the obvious arithmetic operations on types
136 \tdx{nat}, \tdx{int} and~\tdx{real}. (With the \verb|^| operator, the
138 done: the operator {\tt-} can denote set difference, while \verb|^| can
143 The constant \cdx{0} is also overloaded.  It serves as the zero element of
144 several types, of which the most important is \tdx{nat} (the natural
146 and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$.  These
147 types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also
151 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order
153 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and
154 the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass
155 \cldx{order} of \cldx{ord} which axiomatizes the types that are partially
158 For details, see the file \texttt{Ord.thy}.
161 type constraints.  Type inference may otherwise make the goal more
162 polymorphic than you intended, with confusing results.  For example, the
163 variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type
165 numeric type, e.g. $nat$.  Instead you should have stated the goal as
191 P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}.
204 basic Isabelle/HOL binders have two notations.  Apart from the usual
206 supports the original notation of Gordon's {\sc hol} system: \texttt{!}\ 
207 and~\texttt{?}.  In the latter case, the existential quantifier \emph{must} be
210 ``\ttindexbold{HOL}'' governs the output notation.  If enabled (e.g.\ by
211 passing option \texttt{-m HOL} to the \texttt{isabelle} executable),
217 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined
218 to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see
229 parenthesis when they occur in the context of other operations.  For example,
237 the constant~\cdx{Let}.  It can be expanded by rewriting with its
240 HOL also defines the basic syntax
244 logical meaning.  By declaring translations, you can cause instances of the
251 quantifiers, which requires additional enclosing parentheses in the context
273 Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with
274 their~{\ML} names.  Some of the rules deserve additional comments:
279 \item[\tdx{someI}] gives the defining property of the Hilbert
280   $\varepsilon$-operator.  It is a form of the Axiom of Choice.  The derived rule
282 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In
283     fact, the $\varepsilon$-operator already makes the logic classical, as
310 are taken as primitive, with the remainder defined obscurely
311 (Fig.\ts\ref{hol-defs}).  Gordon's {\sc hol} system expresses the
319 only.  Instead users should reason in terms of the derived rules shown below
323 Some of the rules mention type variables; for example, \texttt{refl}
324 mentions the type variable~{\tt'a}.  This allows you to instantiate
410 for the logical connectives, as well as sequent-style elimination rules for
413 Note the equality rules: \tdx{ssubst} performs substitution in
423   $P$ for subgoal $i$: the latter is replaced by two identical subgoals with
424   the added assumptions $P$ and $\lnot P$, respectively.
430   then it replaces the universally quantified implication by $Q \vec{a}$. 
440   \verb|{}|     & $\alpha\,set$         & the empty set \\
493 \caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax}
543 \caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2}
560 Although sets may contain other sets as elements, the containing set must
563 Finite unions and intersections have the same behaviour in HOL as they do
564 in~ZF.  In HOL the intersection of the empty set is well-defined, denoting the
565 universal set for the given type.
569 the same as $\alpha\To bool$.  The new type is defined for clarity and to
571 between the two types are declared explicitly.  They are very natural:
573 maps in the other direction (ignoring argument order).
575 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
576 translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new
578 and $A\int B$), the subset and membership relations, and the image
583 the obvious manner using~\texttt{insert} and~$\{\}$:
593 the type of~$x$ implicitly restricts the comprehension.
616 \sdx{INT}~\hbox{\tt$x$.\ $B[x]$}.  They are equivalent to the previous
617 union and intersection operators when $A$ is the universal set.
649 \caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}
738 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}.  The
740 that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms.  Of
741 course, \hbox{\tt op :} also serves as the membership relation.
743 All the other axioms are definitions.  They include the empty set, bounded
744 quantifiers, unions, intersections, complements and the subset relation.
749 %The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the
751 %definition, $f$ is the abstraction function and $A$ is the set of valid
835 reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are
837 \tdx{equalityCE} supports classical reasoning about extensionality, after the
838 fashion of \tdx{iffCE}.  See the file \texttt{HOL/Set.ML} for proofs
841 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
844 reasoning about the membership relation.  See the file \texttt{HOL/subset.ML}.
848 intersections and complements.  For a complete listing see the file {\tt
853 Hence you seldom need to refer to the theorems above.
881 of~$f$.  See the file \texttt{HOL/Fun.ML} for a complete listing of the derived
882 rules.  Reasoning about function composition (the operator~\sdx{o}) and the
883 predicate~\cdx{surj} is done simply by expanding the definitions.
886 on sets in the file \texttt{HOL/mono.ML}.
891 Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
896 the file \texttt{HOL/simpdata.ML} for a complete listing of the basic
899 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
905   left part of a conjunction helps in simplifying the right part.  This effect
911   By default only the condition of an \ttindex{if} is simplified but not the
912   \texttt{then} and \texttt{else} parts. Of course the latter are simplified
913   once the condition simplifies to \texttt{True} or \texttt{False}. To ensure
915   \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$.
918 If the simplifier cannot use a certain rewrite rule --- either because
922 \item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,
925   may be necessary to select the desired ones.
927 If $thm$ is a conditional equality, the instantiated condition becomes an
931 HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an
939 containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots}
940 often require a case distinction on $b$. This is expressed by the theorem
952 Because $(*)$ is too general as a rewrite rule for the simplifier (the
953 left-hand side is not a higher-order pattern in the sense of
954 \iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}%
966 It turns out that using \texttt{split_if} is almost always the right thing to
967 do. Hence \texttt{split_if} is already included in the default simpset. If
969 the inverse of \texttt{addsplits}:
974 In general, \texttt{addsplits} accepts rules of the form
978 where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the
979 right form because internally the left-hand side is
990 for adding splitting rules to, and deleting them from the current simpset.
996 types in general.  The most important type construction, the
1041 Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type
1042 $\alpha\times\beta$, with the ordered pair syntax $(a, b)$.  General
1043 tuples are simulated by pairs nested to the right:
1068   by the parser and printer.  Thus the internal and external form of a term
1069   may differ, which can affects proofs.  For example the term {\tt
1070   (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the
1096 Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit}
1097 which contains only a single element named {\tt()} with the property
1103 Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$
1104 which associates to the right and has a lower priority than $*$: $\tau@1 +
1108 shown.  The constructions are fairly standard and can be found in the
1109 respective theory files. Although the sum and product types are
1190 \caption{Recursion equations for the arithmetic operators} \label{hol-nat2}
1196 The theory \thydx{Nat} defines the natural numbers in a roundabout but
1200 for~0 and using the injective operation to take successors.  This is a least
1203 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded
1209 Theory \thydx{NatArith} develops arithmetic on the natural numbers.  It defines
1211 division, remainder and the ``divides'' relation.  The numerous theorems
1214 recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on
1215 \texttt{nat} are part of the default simpset.
1219 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following
1220 the standard convention.
1227 of the form
1232 the order of the two cases.
1242 %The transitive closure of \cdx{pred_nat} is~$<$.  Many functions on the
1246 in subgoal~$i$ using theorem \texttt{nat_induct}.  There is also the derived
1255 The integers (type \tdx{int}) are also available in HOL, and the reals (type
1256 \tdx{real}) are available in the logic image \texttt{HOL-Complex}.  They support
1257 the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and
1258 multiplication (\texttt{*}), and much else.  Type \tdx{int} provides the
1261 they inherit the relational operators and all the usual properties of linear
1262 orderings.  For full details, please survey the theories in subdirectories
1265 All three numeric types admit numerals of the form \texttt{$sd\ldots d$},
1268 allows numerical calculations to be performed by rewriting.  For example, the
1270 seconds.  By default, the simplifier cancels like terms on the opposite sites
1276 match a pattern of the form \texttt{Suc $k$}.  You can re-arrange the form of
1278 \texttt{n+3 = Suc (Suc (Suc n))}.  As an alternative, you can disable the
1280 rather than the default one, \texttt{simpset()}.
1285 decision procedure automatically. If this is not sufficent, you can invoke the
1291 existential. The running time is exponential in the number of
1296 by case distinctions, again blowing up the running time.
1297 If the formula involves explicit quantifiers, \texttt{Lin_Arith.tac} may take
1301 the library.  The theories \texttt{Nat} and \texttt{NatArith} contain
1428 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
1430 defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}.
1431 As a result the generic structural induction and case analysis tactics
1433 lists.  A \sdx{case} construct of the form
1473 It also offers to represent existing types as datatypes giving the advantage
1480 A general \texttt{datatype} definition is of the following form:
1494   admissible} types containing at most the type variables $\alpha@1, \ldots,
1498 \item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the
1502 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$
1505 type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined
1509 of the form
1514 example of a datatype is the type \texttt{list}, which can be defined by
1520 by the mutually recursive datatype definition
1544 Types in HOL must be non-empty. Each of the new datatypes
1546 constructor $C^j@i$ with the following property: for all argument types
1547 $\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype
1550 If there are no nested occurrences of the newly defined datatypes, obviously
1551 at least one of the newly defined datatypes $(\vec{\alpha})t@j$
1553   case}, to ensure that the new types are non-empty. If there are nested
1559 \subsubsection{Freeness of the constructors}
1575 Since the number of distinctness inequalities is quadratic in the number of
1576 constructors, the datatype package avoids proving them separately if there are
1579 of the default simpset, may be referred to by the ML identifier
1585 datatypes without nested recursion, this is of the following form:
1621 i.e.\ the properties $P@j$ can be assumed for all recursive arguments.
1623 For datatypes with nested recursion, such as the \texttt{term} example from
1637 Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt
1639 the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing
1640 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for
1641 \texttt{term} gets the form
1651 Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term}
1652 and one for the type \texttt{(('a, 'b) term) list}.
1654 For a datatype with function types such as \texttt{'a tree}, the induction rule
1655 is of the form
1664 the following derived constructions are automatically provided for any
1677 where the $x@{i,j}$ are either identifiers or nested tuple patterns as in
1681   are not supported (with the exception of tuples).  Violating this
1686 the theorem $t@j.$\texttt{split} is provided:
1697 where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.
1701 Case splitting on assumption works as well, by using the rule
1702 $t@j.$\texttt{split_asm} in the same manner.  Both rules are available under
1706   By default only the selector expression ($e$ above) in a
1709   the arms of the \texttt{case}-construct exposed and simplified. To ensure
1711   $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for
1719 by overloading according to the following scheme:
1732 where $Rec^j@i$ is defined above.  Viewing datatypes as generalised trees, the
1733 size of a leaf is 0 and the size of a node is the sum of the sizes of its
1738 The theory syntax for datatype definitions is given in the
1740 datatype definition has to obey the rules stated in the previous
1741 section.  As a result the theory is extended with the new types, the
1742 constructors, and the theorems listed in the previous section.
1744 Most of the theorems about datatypes become part of the default simpset and
1745 you never need to see them again because the simplifier applies them
1749  applies structural induction on variable $x$ to subgoal $i$, provided the
1753   structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$.  This
1754   is the canonical way to prove properties of mutually recursive datatypes
1759 constructors of the datatype suffices.
1762  performs a case analysis for the term $u$ whose type  must be a datatype.
1763  If the datatype has $k@j$ constructors  $C^j@1$, \dots $C^j@{k@j}$, subgoal
1764  $i$ is replaced by $k@j$ new subgoals which  contain the additional
1769 among the premises of the subgoal. Case distinction applies to arbitrary terms.
1774 For the technically minded, we exhibit some more details.  Processing the
1775 theory file produces an \ML\ structure which, in addition to the usual
1777 the file.  Each structure $t$ contains the following elements:
1791 and \texttt{split} contain the theorems
1793 inequalities in both directions.  The reduction rules of the {\tt
1805 supply a well-founded relation that governs the recursion.  Recursive
1806 calls are only allowed if they make the argument decrease under the
1818 call makes the argument smaller in a suitable sense, which you specify by
1821 Here is a simple example, the Fibonacci function.  The first line declares
1823 the natural numbers).  Pattern-matching is used here: \texttt{1} is a
1835 disambiguates overlapping patterns by taking the order of rules into account.
1836 For missing patterns, the function is defined to return a default value.
1838 %For example, here is a declaration of the list function \cdx{hd}:
1844 %Because this function is not recursive, we may supply the empty well-founded
1847 The well-founded relation defines a notion of ``smaller'' for the function's
1851 If the function's argument has type~$\tau$, then $\prec$ has to be a relation
1856 these operators and automatically proves that the constructed relation is
1859 \item \texttt{less_than} is ``less than'' on the natural numbers.
1862 \item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the
1865   Typically, $f$ takes the recursive function's arguments (as a tuple) and
1866   returns a result expressed in terms of the function \texttt{size}.  It is
1876 \item $R@1\texttt{<*lex*>}R@2$ is the lexicographic product of two relations.
1883 \item \texttt{finite_psubset} is the proper subset relation on finite sets.
1886 We can use \texttt{measure} to declare Euclid's algorithm for the greatest
1887 common divisor.  The measure function, $\lambda(m,n). n$, specifies that the
1903 \item \textit{function} is the name of the function, either as an \textit{id}
1906 \item \textit{rel} is a HOL expression for the well-founded termination
1912 \item The \textit{simplification set} is used to prove that the supplied
1913   relation is well-founded.  It is also used to prove the \textbf{termination
1916   is sufficient to prove well-foundedness for the built-in relations listed
1920   left-hand side must have the form $f\,t$, where $f$ is the function and $t$
1925   The \ML\ identifier $f$\texttt{.simps} contains the reduction rules as
1929 With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to
1930 prove one termination condition.  It remains as a precondition of the
1939 conditions afterwards.  The function \texttt{Tfl.tgoalw} is like the standard
1941 should be the identifier $f$\texttt{.simps} and its effect is to set up a
1942 proof of the termination conditions:
1949 This subgoal has a one-step proof using \texttt{simp_tac}.  Once the theorem
1950 is proved, it can be used to eliminate the termination conditions from
1952 more complicated example of this process, where the termination conditions can
1953 only be proved by complicated reasoning involving the recursive function
1956 Isabelle/HOL can prove the \texttt{gcd} function's termination condition
1957 automatically if supplied with the right simpset.
1965 is added to the simpset automatically, just as in \texttt{primrec}. 
1970 clauses from the simpset. Note that a single clause may give rise to a set of
1971 simplification rules in order to capture the fact that if clauses overlap,
1975 the recursive function.  For the \texttt{gcd} function above, the induction
1981 This rule should be used to reason inductively about the \texttt{gcd}
1982 function.  It usually makes the induction hypothesis available at all
1998 Viewing types as sets, $\alpha\To bool$ represents the powerset
2002 The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and
2003 the operator \cdx{range}.
2008 quantified variable so that we may inspect the subset found by the proof.
2038 Now we use a bit of creativity.  Suppose that~$\Var{S}$ has the form of a
2041 instantiates~$\Var{S}$ and creates the new assumption.
2049 Forcing a contradiction between the two assumptions of subgoal~1
2050 completes the instantiation of~$S$.  It is now the set $\{x. x\not\in
2051 f~x\}$, which is the standard diagonal construction.
2058 The rest should be easy.  To apply \tdx{CollectI} to the negated
2073 rules for most of the constructs of HOL's set theory.  We must augment it with
2076 through the large search space.  \index{search!best-first}
2090 Otherwise the default claset may not contain the rules for set theory.

Indexes created Sun Jun 23 19:15:37 MDT 2024