|
1 (*<*) |
|
2 theory Basics |
|
3 imports Main |
|
4 begin |
|
5 (*>*) |
|
6 text{* |
|
7 This chapter introduces HOL as a functional programming language and shows |
|
8 how to prove properties of functional programs by induction. |
|
9 |
|
10 \section{Basics} |
|
11 |
|
12 \subsection{Types, Terms and Formulas} |
|
13 \label{sec:TypesTermsForms} |
|
14 |
|
15 HOL is a typed logic whose type system resembles that of functional |
|
16 programming languages. Thus there are |
|
17 \begin{description} |
|
18 \item[base types,] |
|
19 in particular @{typ bool}, the type of truth values, |
|
20 @{typ nat}, the type of natural numbers ($\mathbb{N}$), and \indexed{@{typ int}}{int}, |
|
21 the type of mathematical integers ($\mathbb{Z}$). |
|
22 \item[type constructors,] |
|
23 in particular @{text list}, the type of |
|
24 lists, and @{text set}, the type of sets. Type constructors are written |
|
25 postfix, i.e., after their arguments. For example, |
|
26 @{typ "nat list"} is the type of lists whose elements are natural numbers. |
|
27 \item[function types,] |
|
28 denoted by @{text"\<Rightarrow>"}. |
|
29 \item[type variables,] |
|
30 denoted by @{typ 'a}, @{typ 'b} etc., just like in ML\@. |
|
31 \end{description} |
|
32 Note that @{typ"'a \<Rightarrow> 'b list"} means @{typ[source]"'a \<Rightarrow> ('b list)"}, |
|
33 not @{typ"('a \<Rightarrow> 'b) list"}: postfix type constructors have precedence |
|
34 over @{text"\<Rightarrow>"}. |
|
35 |
|
36 \conceptidx{Terms}{term} are formed as in functional programming by |
|
37 applying functions to arguments. If @{text f} is a function of type |
|
38 @{text"\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2"} and @{text t} is a term of type |
|
39 @{text"\<tau>\<^sub>1"} then @{term"f t"} is a term of type @{text"\<tau>\<^sub>2"}. We write @{text "t :: \<tau>"} to mean that term @{text t} has type @{text \<tau>}. |
|
40 |
|
41 \begin{warn} |
|
42 There are many predefined infix symbols like @{text "+"} and @{text"\<le>"}. |
|
43 The name of the corresponding binary function is @{term"op +"}, |
|
44 not just @{text"+"}. That is, @{term"x + y"} is nice surface syntax |
|
45 (``syntactic sugar'') for \noquotes{@{term[source]"op + x y"}}. |
|
46 \end{warn} |
|
47 |
|
48 HOL also supports some basic constructs from functional programming: |
|
49 \begin{quote} |
|
50 @{text "(if b then t\<^sub>1 else t\<^sub>2)"}\\ |
|
51 @{text "(let x = t in u)"}\\ |
|
52 @{text "(case t of pat\<^sub>1 \<Rightarrow> t\<^sub>1 | \<dots> | pat\<^sub>n \<Rightarrow> t\<^sub>n)"} |
|
53 \end{quote} |
|
54 \begin{warn} |
|
55 The above three constructs must always be enclosed in parentheses |
|
56 if they occur inside other constructs. |
|
57 \end{warn} |
|
58 Terms may also contain @{text "\<lambda>"}-abstractions. For example, |
|
59 @{term "\<lambda>x. x"} is the identity function. |
|
60 |
|
61 \conceptidx{Formulas}{formula} are terms of type @{text bool}. |
|
62 There are the basic constants @{term True} and @{term False} and |
|
63 the usual logical connectives (in decreasing order of precedence): |
|
64 @{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"}, @{text"\<longrightarrow>"}. |
|
65 |
|
66 \conceptidx{Equality}{equality} is available in the form of the infix function @{text "="} |
|
67 of type @{typ "'a \<Rightarrow> 'a \<Rightarrow> bool"}. It also works for formulas, where |
|
68 it means ``if and only if''. |
|
69 |
|
70 \conceptidx{Quantifiers}{quantifier} are written @{prop"\<forall>x. P"} and @{prop"\<exists>x. P"}. |
|
71 |
|
72 Isabelle automatically computes the type of each variable in a term. This is |
|
73 called \concept{type inference}. Despite type inference, it is sometimes |
|
74 necessary to attach an explicit \concept{type constraint} (or \concept{type |
|
75 annotation}) to a variable or term. The syntax is @{text "t :: \<tau>"} as in |
|
76 \mbox{\noquotes{@{prop[source] "m < (n::nat)"}}}. Type constraints may be |
|
77 needed to |
|
78 disambiguate terms involving overloaded functions such as @{text "+"}, @{text |
|
79 "*"} and @{text"\<le>"}. |
|
80 |
|
81 Finally there are the universal quantifier @{text"\<And>"}\index{$4@\isasymAnd} and the implication |
|
82 @{text"\<Longrightarrow>"}\index{$3@\isasymLongrightarrow}. They are part of the Isabelle framework, not the logic |
|
83 HOL. Logically, they agree with their HOL counterparts @{text"\<forall>"} and |
|
84 @{text"\<longrightarrow>"}, but operationally they behave differently. This will become |
|
85 clearer as we go along. |
|
86 \begin{warn} |
|
87 Right-arrows of all kinds always associate to the right. In particular, |
|
88 the formula |
|
89 @{text"A\<^sub>1 \<Longrightarrow> A\<^sub>2 \<Longrightarrow> A\<^sub>3"} means @{text "A\<^sub>1 \<Longrightarrow> (A\<^sub>2 \<Longrightarrow> A\<^sub>3)"}. |
|
90 The (Isabelle specific) notation \mbox{@{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"}} |
|
91 is short for the iterated implication \mbox{@{text"A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> A"}}. |
|
92 Sometimes we also employ inference rule notation: |
|
93 \inferrule{\mbox{@{text "A\<^sub>1"}}\\ \mbox{@{text "\<dots>"}}\\ \mbox{@{text "A\<^sub>n"}}} |
|
94 {\mbox{@{text A}}} |
|
95 \end{warn} |
|
96 |
|
97 |
|
98 \subsection{Theories} |
|
99 \label{sec:Basic:Theories} |
|
100 |
|
101 Roughly speaking, a \concept{theory} is a named collection of types, |
|
102 functions, and theorems, much like a module in a programming language. |
|
103 All the Isabelle text that you ever type needs to go into a theory. |
|
104 The general format of a theory @{text T} is |
|
105 \begin{quote} |
|
106 \indexed{\isacom{theory}}{theory} @{text T}\\ |
|
107 \indexed{\isacom{imports}}{imports} @{text "T\<^sub>1 \<dots> T\<^sub>n"}\\ |
|
108 \isacom{begin}\\ |
|
109 \emph{definitions, theorems and proofs}\\ |
|
110 \isacom{end} |
|
111 \end{quote} |
|
112 where @{text "T\<^sub>1 \<dots> T\<^sub>n"} are the names of existing |
|
113 theories that @{text T} is based on. The @{text "T\<^sub>i"} are the |
|
114 direct \conceptidx{parent theories}{parent theory} of @{text T}. |
|
115 Everything defined in the parent theories (and their parents, recursively) is |
|
116 automatically visible. Each theory @{text T} must |
|
117 reside in a \concept{theory file} named @{text "T.thy"}. |
|
118 |
|
119 \begin{warn} |
|
120 HOL contains a theory @{theory Main}\index{Main@@{theory Main}}, the union of all the basic |
|
121 predefined theories like arithmetic, lists, sets, etc. |
|
122 Unless you know what you are doing, always include @{text Main} |
|
123 as a direct or indirect parent of all your theories. |
|
124 \end{warn} |
|
125 |
|
126 In addition to the theories that come with the Isabelle/HOL distribution |
|
127 (see @{url "http://isabelle.in.tum.de/library/HOL/"}) |
|
128 there is also the \emph{Archive of Formal Proofs} |
|
129 at @{url "http://afp.sourceforge.net"}, a growing collection of Isabelle theories |
|
130 that everybody can contribute to. |
|
131 |
|
132 \subsection{Quotation Marks} |
|
133 |
|
134 The textual definition of a theory follows a fixed syntax with keywords like |
|
135 \isacommand{begin} and \isacommand{datatype}. Embedded in this syntax are |
|
136 the types and formulas of HOL. To distinguish the two levels, everything |
|
137 HOL-specific (terms and types) must be enclosed in quotation marks: |
|
138 \texttt{"}\dots\texttt{"}. To lessen this burden, quotation marks around a |
|
139 single identifier can be dropped. When Isabelle prints a syntax error |
|
140 message, it refers to the HOL syntax as the \concept{inner syntax} and the |
|
141 enclosing theory language as the \concept{outer syntax}. |
|
142 *} |
|
143 (*<*) |
|
144 end |
|
145 (*>*) |