6 specification and verification system. Isabelle is a generic system for |
6 specification and verification system. Isabelle is a generic system for |
7 implementing logical formalisms, and Isabelle/HOL is the specialization |
7 implementing logical formalisms, and Isabelle/HOL is the specialization |
8 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce |
8 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce |
9 HOL step by step following the equation |
9 HOL step by step following the equation |
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] |
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] |
11 We do not assume that the reader is familiar with mathematical logic but that |
11 We do not assume that you are familiar with mathematical logic but that |
12 (s)he is used to logical and set theoretic notation, such as covered |
12 you are used to logical and set theoretic notation, such as covered |
13 in a good discrete math course~\cite{Rosen-DMA}. In contrast, we do assume |
13 in a good discrete mathematics course~\cite{Rosen-DMA}. |
14 that the reader is familiar with the basic concepts of functional |
14 In contrast, we do assume |
|
15 that you are familiar with the basic concepts of functional |
15 programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}. |
16 programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}. |
16 Although this tutorial initially concentrates on functional programming, do |
17 Although this tutorial initially concentrates on functional programming, do |
17 not be misled: HOL can express most mathematical concepts, and functional |
18 not be misled: HOL can express most mathematical concepts, and functional |
18 programming is just one particularly simple and ubiquitous instance. |
19 programming is just one particularly simple and ubiquitous instance. |
19 |
20 |
20 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has |
21 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has |
21 influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant |
22 influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant |
22 for us because this tutorial is based on |
23 for us: this tutorial is based on |
23 Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides |
24 Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides |
24 the implementation language almost completely. Thus the full name of the |
25 the implementation language almost completely. Thus the full name of the |
25 system should be Isabelle/Isar/HOL, but that is a bit of a mouthful. |
26 system should be Isabelle/Isar/HOL, but that is a bit of a mouthful. |
26 |
27 |
27 There are other implementations of HOL, in particular the one by Mike Gordon |
28 There are other implementations of HOL, in particular the one by Mike Gordon |
|
29 \index{Gordon, Mike}% |
28 \emph{et al.}, which is usually referred to as ``the HOL system'' |
30 \emph{et al.}, which is usually referred to as ``the HOL system'' |
29 \cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes |
31 \cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes |
30 its incarnation Isabelle/HOL. |
32 its incarnation Isabelle/HOL\@. |
31 |
33 |
32 A tutorial is by definition incomplete. Currently the tutorial only |
34 A tutorial is by definition incomplete. Currently the tutorial only |
33 introduces the rudiments of Isar's proof language. To fully exploit the power |
35 introduces the rudiments of Isar's proof language. To fully exploit the power |
34 of Isar, in particular the ability to write readable and structured proofs, |
36 of Isar, in particular the ability to write readable and structured proofs, |
35 you need to consult the Isabelle/Isar Reference |
37 you need to consult the Isabelle/Isar Reference |
48 much like a module in a programming language or a specification in a |
50 much like a module in a programming language or a specification in a |
49 specification language. In fact, theories in HOL can be either. The general |
51 specification language. In fact, theories in HOL can be either. The general |
50 format of a theory \texttt{T} is |
52 format of a theory \texttt{T} is |
51 \begin{ttbox} |
53 \begin{ttbox} |
52 theory T = B\(@1\) + \(\cdots\) + B\(@n\): |
54 theory T = B\(@1\) + \(\cdots\) + B\(@n\): |
53 \(\textit{declarations, definitions, and proofs}\) |
55 {\rmfamily\textit{declarations, definitions, and proofs}} |
54 end |
56 end |
55 \end{ttbox} |
57 \end{ttbox} |
56 where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing |
58 where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing |
57 theories that \texttt{T} is based on and \texttt{\textit{declarations, |
59 theories that \texttt{T} is based on and \textit{declarations, |
58 definitions, and proofs}} represents the newly introduced concepts |
60 definitions, and proofs} represents the newly introduced concepts |
59 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the |
61 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the |
60 direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}. |
62 direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@. |
61 Everything defined in the parent theories (and their parents \dots) is |
63 Everything defined in the parent theories (and their parents, recursively) is |
62 automatically visible. To avoid name clashes, identifiers can be |
64 automatically visible. To avoid name clashes, identifiers can be |
63 \textbf{qualified} by theory names as in \texttt{T.f} and |
65 \textbf{qualified}\indexbold{identifiers!qualified} |
64 \texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must |
66 by theory names as in \texttt{T.f} and~\texttt{B.f}. |
|
67 Each theory \texttt{T} must |
65 reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}. |
68 reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}. |
66 |
69 |
67 This tutorial is concerned with introducing you to the different linguistic |
70 This tutorial is concerned with introducing you to the different linguistic |
68 constructs that can fill \textit{\texttt{declarations, definitions, and |
71 constructs that can fill the \textit{declarations, definitions, and |
69 proofs}} in the above theory template. A complete grammar of the basic |
72 proofs} above. A complete grammar of the basic |
70 constructs is found in the Isabelle/Isar Reference Manual. |
73 constructs is found in the Isabelle/Isar Reference Manual. |
71 |
74 |
72 HOL's theory collection is available online at |
75 HOL's theory collection is available online at |
73 \begin{center}\small |
76 \begin{center}\small |
74 \url{http://isabelle.in.tum.de/library/HOL/} |
77 \url{http://isabelle.in.tum.de/library/HOL/} |
90 \section{Types, Terms and Formulae} |
93 \section{Types, Terms and Formulae} |
91 \label{sec:TypesTermsForms} |
94 \label{sec:TypesTermsForms} |
92 |
95 |
93 Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed |
96 Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed |
94 logic whose type system resembles that of functional programming languages |
97 logic whose type system resembles that of functional programming languages |
95 like ML or Haskell. Thus there are\index{types} |
98 like ML or Haskell. Thus there are |
|
99 \index{types|(} |
96 \begin{description} |
100 \begin{description} |
97 \item[base types,] in particular \tydx{bool}, the type of truth values, |
101 \item[base types,] |
|
102 in particular \tydx{bool}, the type of truth values, |
98 and \tydx{nat}, the type of natural numbers. |
103 and \tydx{nat}, the type of natural numbers. |
99 \item[type constructors,] in particular \tydx{list}, the type of |
104 \item[type constructors,]\index{type constructors} |
|
105 in particular \tydx{list}, the type of |
100 lists, and \tydx{set}, the type of sets. Type constructors are written |
106 lists, and \tydx{set}, the type of sets. Type constructors are written |
101 postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are |
107 postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are |
102 natural numbers. Parentheses around single arguments can be dropped (as in |
108 natural numbers. Parentheses around single arguments can be dropped (as in |
103 \isa{nat list}), multiple arguments are separated by commas (as in |
109 \isa{nat list}), multiple arguments are separated by commas (as in |
104 \isa{(bool,nat)ty}). |
110 \isa{(bool,nat)ty}). |
105 \item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}. |
111 \item[function types,]\index{function types} |
|
112 denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}. |
106 In HOL \isasymFun\ represents \emph{total} functions only. As is customary, |
113 In HOL \isasymFun\ represents \emph{total} functions only. As is customary, |
107 \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means |
114 \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means |
108 \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also |
115 \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also |
109 supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$} |
116 supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$} |
110 which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$ |
117 which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$ |
111 \isasymFun~$\tau$}. |
118 \isasymFun~$\tau$}. |
112 \item[type variables,]\indexbold{type variables}\indexbold{variables!type} |
119 \item[type variables,]\index{type variables}\index{variables!type} |
113 denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise |
120 denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise |
114 to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity |
121 to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity |
115 function. |
122 function. |
116 \end{description} |
123 \end{description} |
117 \begin{warn} |
124 \begin{warn} |
123 called \bfindex{type inference}) and keeps quiet about it. Occasionally |
130 called \bfindex{type inference}) and keeps quiet about it. Occasionally |
124 this may lead to misunderstandings between you and the system. If anything |
131 this may lead to misunderstandings between you and the system. If anything |
125 strange happens, we recommend that you set the flag\index{flags} |
132 strange happens, we recommend that you set the flag\index{flags} |
126 \isa{show_types}\index{*show_types (flag)}. |
133 \isa{show_types}\index{*show_types (flag)}. |
127 Isabelle will then display type information |
134 Isabelle will then display type information |
128 that is usually suppressed. simply type |
135 that is usually suppressed. Simply type |
129 \begin{ttbox} |
136 \begin{ttbox} |
130 ML "set show_types" |
137 ML "set show_types" |
131 \end{ttbox} |
138 \end{ttbox} |
132 |
139 |
133 \noindent |
140 \noindent |
134 This can be reversed by \texttt{ML "reset show_types"}. Various other flags, |
141 This can be reversed by \texttt{ML "reset show_types"}. Various other flags, |
135 which we introduce as we go along, can be set and reset in the same manner.% |
142 which we introduce as we go along, can be set and reset in the same manner.% |
136 \index{flags!setting and resetting} |
143 \index{flags!setting and resetting} |
137 \end{warn} |
144 \end{warn}% |
138 |
145 \index{types|)} |
139 |
146 |
140 \textbf{Terms}\index{terms} are formed as in functional programming by |
147 |
|
148 \index{terms|(} |
|
149 \textbf{Terms} are formed as in functional programming by |
141 applying functions to arguments. If \isa{f} is a function of type |
150 applying functions to arguments. If \isa{f} is a function of type |
142 \isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type |
151 \isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type |
143 $\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports |
152 $\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports |
144 infix functions like \isa{+} and some basic constructs from functional |
153 infix functions like \isa{+} and some basic constructs from functional |
145 programming, such as conditional expressions: |
154 programming, such as conditional expressions: |
146 \begin{description} |
155 \begin{description} |
147 \item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if (symbol)} |
156 \item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions} |
148 Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type. |
157 Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type. |
149 \item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let (symbol)} |
158 \item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions} |
150 is equivalent to $u$ where all occurrences of $x$ have been replaced by |
159 is equivalent to $u$ where all occurrences of $x$ have been replaced by |
151 $t$. For example, |
160 $t$. For example, |
152 \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated |
161 \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated |
153 by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}. |
162 by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}. |
154 \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}] |
163 \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}] |
155 \indexbold{*case (symbol)} |
164 \index{*case expressions} |
156 evaluates to $e@i$ if $e$ is of the form $c@i$. |
165 evaluates to $e@i$ if $e$ is of the form $c@i$. |
157 \end{description} |
166 \end{description} |
158 |
167 |
159 Terms may also contain |
168 Terms may also contain |
160 \isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example, |
169 \isasymlambda-abstractions.\index{lambda@$\lambda$ expressions} |
|
170 For example, |
161 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and |
171 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and |
162 returns \isa{x+1}. Instead of |
172 returns \isa{x+1}. Instead of |
163 \isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write |
173 \isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write |
164 \isa{\isasymlambda{}x~y~z.~$t$}. |
174 \isa{\isasymlambda{}x~y~z.~$t$}.% |
165 |
175 \index{terms|)} |
166 \textbf{Formulae}\indexbold{formulae} are terms of type \tydx{bool}. |
176 |
|
177 \index{formulae|(}% |
|
178 \textbf{Formulae} are terms of type \tydx{bool}. |
167 There are the basic constants \cdx{True} and \cdx{False} and |
179 There are the basic constants \cdx{True} and \cdx{False} and |
168 the usual logical connectives (in decreasing order of priority): |
180 the usual logical connectives (in decreasing order of priority): |
169 \indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and}, |
181 \indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and}, |
170 \indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp}, |
182 \indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp}, |
171 all of which (except the unary \isasymnot) associate to the right. In |
183 all of which (except the unary \isasymnot) associate to the right. In |
172 particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B |
184 particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B |
173 \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B |
185 \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B |
174 \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}). |
186 \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}). |
175 |
187 |
176 Equality is available in the form of the infix function |
188 Equality\index{equality} is available in the form of the infix function |
177 \isa{=}\indexbold{$HOL0eq@\texttt{=}} of type \isa{'a \isasymFun~'a |
189 \isa{=} of type \isa{'a \isasymFun~'a |
178 \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$ |
190 \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$ |
179 and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type |
191 and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type |
180 \isa{bool}, \isa{=} acts as if-and-only-if. The formula |
192 \isa{bool} then \isa{=} acts as \rmindex{if-and-only-if}. |
|
193 The formula |
181 \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for |
194 \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for |
182 \isa{\isasymnot($t@1$ = $t@2$)}. |
195 \isa{\isasymnot($t@1$ = $t@2$)}. |
183 |
196 |
184 Quantifiers are written as |
197 Quantifiers\index{quantifiers} are written as |
185 \isa{\isasymforall{}x.~$P$}\index{$HOL0All@\isasymforall|bold} and |
198 \isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}. |
186 \isa{\isasymexists{}x.~$P$}\index{$HOL0Ex@\isasymexists|bold}. |
|
187 There is even |
199 There is even |
188 \isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which |
200 \isa{\isasymuniqex{}x.~$P$}, which |
189 means that there exists exactly one \isa{x} that satisfies \isa{$P$}. |
201 means that there exists exactly one \isa{x} that satisfies \isa{$P$}. |
190 Nested quantifications can be abbreviated: |
202 Nested quantifications can be abbreviated: |
191 \isa{\isasymforall{}x~y~z.~$P$} means |
203 \isa{\isasymforall{}x~y~z.~$P$} means |
192 \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}. |
204 \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.% |
|
205 \index{formulae|)} |
193 |
206 |
194 Despite type inference, it is sometimes necessary to attach explicit |
207 Despite type inference, it is sometimes necessary to attach explicit |
195 \bfindex{type constraints} to a term. The syntax is |
208 \bfindex{type constraints} to a term. The syntax is |
196 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that |
209 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that |
197 \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed |
210 \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed |
198 in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as |
211 in parentheses. For instance, |
199 \isa{(x < y)::nat}. The main reason for type constraints is overloading of |
212 \isa{x < y::nat} is ill-typed because it is interpreted as |
200 functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for |
213 \isa{(x < y)::nat}. Type constraints may be needed to disambiguate |
201 a full discussion of overloading and Table~\ref{tab:overloading} for the most |
214 expressions |
|
215 involving overloaded functions such as~\isa{+}, |
|
216 \isa{*} and~\isa{<}. Section~\ref{sec:overloading} |
|
217 discusses overloading, while Table~\ref{tab:overloading} presents the most |
202 important overloaded function symbols. |
218 important overloaded function symbols. |
203 |
219 |
204 \begin{warn} |
220 In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of |
205 In general, HOL's concrete syntax tries to follow the conventions of |
221 functional programming and mathematics. Here are the main rules that you |
206 functional programming and mathematics. Below we list the main rules that you |
222 should be familiar with to avoid certain syntactic traps: |
207 should be familiar with to avoid certain syntactic traps. A particular |
|
208 problem for novices can be the priority of operators. If you are unsure, use |
|
209 additional parentheses. In those cases where Isabelle echoes your |
|
210 input, you can see which parentheses are dropped --- they were superfluous. If |
|
211 you are unsure how to interpret Isabelle's output because you don't know |
|
212 where the (dropped) parentheses go, set the flag\index{flags} |
|
213 \isa{show_brackets}\index{*show_brackets (flag)}: |
|
214 \begin{ttbox} |
|
215 ML "set show_brackets"; \(\dots\); ML "reset show_brackets"; |
|
216 \end{ttbox} |
|
217 \end{warn} |
|
218 |
|
219 \begin{itemize} |
223 \begin{itemize} |
220 \item |
224 \item |
221 Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}! |
225 Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}! |
222 \item |
226 \item |
223 Isabelle allows infix functions like \isa{+}. The prefix form of function |
227 Isabelle allows infix functions like \isa{+}. The prefix form of function |
231 logical equivalence, enclose both operands in parentheses, as in \isa{(A |
235 logical equivalence, enclose both operands in parentheses, as in \isa{(A |
232 \isasymand~B) = (B \isasymand~A)}. |
236 \isasymand~B) = (B \isasymand~A)}. |
233 \item |
237 \item |
234 Constructs with an opening but without a closing delimiter bind very weakly |
238 Constructs with an opening but without a closing delimiter bind very weakly |
235 and should therefore be enclosed in parentheses if they appear in subterms, as |
239 and should therefore be enclosed in parentheses if they appear in subterms, as |
236 in \isa{(\isasymlambda{}x.~x) = f}. This includes \sdx{if}, |
240 in \isa{(\isasymlambda{}x.~x) = f}. This includes |
237 \sdx{let}, \sdx{case}, \isa{\isasymlambda}, and quantifiers. |
241 \isa{if},\index{*if expressions} |
|
242 \isa{let},\index{*let expressions} |
|
243 \isa{case},\index{*case expressions} |
|
244 \isa{\isasymlambda}, and quantifiers. |
238 \item |
245 \item |
239 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x} |
246 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x} |
240 because \isa{x.x} is always read as a single qualified identifier that |
247 because \isa{x.x} is always taken as a single qualified identifier that |
241 refers to an item \isa{x} in theory \isa{x}. Write |
248 refers to an item \isa{x} in theory \isa{x}. Write |
242 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead. |
249 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead. |
243 \item Identifiers\indexbold{identifier} may contain \isa{_} and \isa{'}. |
250 \item Identifiers\indexbold{identifiers} may contain the characters \isa{_} |
|
251 and~\isa{'}. |
244 \end{itemize} |
252 \end{itemize} |
245 |
253 |
246 For the sake of readability the usual mathematical symbols are used throughout |
254 For the sake of readability, we use the usual mathematical symbols throughout |
247 the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in |
255 the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in |
248 the appendix. |
256 the appendix. |
249 |
257 |
|
258 \begin{warn} |
|
259 A particular |
|
260 problem for novices can be the priority of operators. If you are unsure, use |
|
261 additional parentheses. In those cases where Isabelle echoes your |
|
262 input, you can see which parentheses are dropped --- they were superfluous. If |
|
263 you are unsure how to interpret Isabelle's output because you don't know |
|
264 where the (dropped) parentheses go, set the flag\index{flags} |
|
265 \isa{show_brackets}\index{*show_brackets (flag)}: |
|
266 \begin{ttbox} |
|
267 ML "set show_brackets"; \(\dots\); ML "reset show_brackets"; |
|
268 \end{ttbox} |
|
269 \end{warn} |
|
270 |
250 |
271 |
251 \section{Variables} |
272 \section{Variables} |
252 \label{sec:variables} |
273 \label{sec:variables} |
253 \indexbold{variable} |
274 \index{variables|(} |
254 |
275 |
255 Isabelle distinguishes free and bound variables just as is customary. Bound |
276 Isabelle distinguishes free and bound variables, as is customary. Bound |
256 variables are automatically renamed to avoid clashes with free variables. In |
277 variables are automatically renamed to avoid clashes with free variables. In |
257 addition, Isabelle has a third kind of variable, called a \textbf{schematic |
278 addition, Isabelle has a third kind of variable, called a \textbf{schematic |
258 variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns}, |
279 variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns}, |
259 which must a~\isa{?} as its first character. |
280 which must a~\isa{?} as its first character. |
260 Logically, an unknown is a free variable. But it may be |
281 Logically, an unknown is a free variable. But it may be |
264 to ordinary variables, which remain fixed. The programming language Prolog |
285 to ordinary variables, which remain fixed. The programming language Prolog |
265 calls unknowns {\em logical\/} variables. |
286 calls unknowns {\em logical\/} variables. |
266 |
287 |
267 Most of the time you can and should ignore unknowns and work with ordinary |
288 Most of the time you can and should ignore unknowns and work with ordinary |
268 variables. Just don't be surprised that after you have finished the proof of |
289 variables. Just don't be surprised that after you have finished the proof of |
269 a theorem, Isabelle will turn your free variables into unknowns: it merely |
290 a theorem, Isabelle will turn your free variables into unknowns. It |
270 indicates that Isabelle will automatically instantiate those unknowns |
291 indicates that Isabelle will automatically instantiate those unknowns |
271 suitably when the theorem is used in some other proof. |
292 suitably when the theorem is used in some other proof. |
272 Note that for readability we often drop the \isa{?}s when displaying a theorem. |
293 Note that for readability we often drop the \isa{?}s when displaying a theorem. |
273 \begin{warn} |
294 \begin{warn} |
274 If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential |
295 For historical reasons, Isabelle accepts \isa{?} as an ASCII representation |
275 quantifier, it needs to be followed by a space. Otherwise \isa{?x} is |
296 of the \(\exists\) symbol. However, the \isa{?} character must then be followed |
276 interpreted as a schematic variable. |
297 by a space, as in \isa{?~x. f(x) = 0}. Otherwise, \isa{?x} is |
277 \end{warn} |
298 interpreted as a schematic variable. The preferred ASCII representation of |
|
299 the \(\exists\) symbol is \isa{EX}\@. |
|
300 \end{warn}% |
|
301 \index{variables|)} |
278 |
302 |
279 \section{Interaction and Interfaces} |
303 \section{Interaction and Interfaces} |
280 |
304 |
281 Interaction with Isabelle can either occur at the shell level or through more |
305 Interaction with Isabelle can either occur at the shell level or through more |
282 advanced interfaces. To keep the tutorial independent of the interface, we |
306 advanced interfaces. To keep the tutorial independent of the interface, we |