author  wenzelm 
Tue, 31 Mar 2015 22:31:05 +0200  
changeset 59886  e0dc738eb08c 
parent 58655  46a19b1d3dd2 
child 61431  f6e314c1e9c4 
permissions  rwrr 
47269  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 

52361  12 
\subsection{Types, Terms and Formulas} 
47269  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, 

55317  20 
@{typ nat}, the type of natural numbers ($\mathbb{N}$), and \indexed{@{typ int}}{int}, 
47269  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 

54467  25 
postfix, i.e., after their arguments. For example, 
26 
@{typ "nat list"} is the type of lists whose elements are natural numbers. 

47269  27 
\item[function types,] 
28 
denoted by @{text"\<Rightarrow>"}. 

29 
\item[type variables,] 

58521  30 
denoted by @{typ 'a}, @{typ 'b}, etc., like in ML\@. 
47269  31 
\end{description} 
52045  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>"}. 

47269  35 

55317  36 
\conceptidx{Terms}{term} are formed as in functional programming by 
47269  37 
applying functions to arguments. If @{text f} is a function of type 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52361
diff
changeset

38 
@{text"\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2"} and @{text t} is a term of type 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52361
diff
changeset

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>}. 
47269  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 +"}, 

54467  44 
not just @{text"+"}. That is, @{term"x + y"} is nice surface syntax 
45 
(``syntactic sugar'') for \noquotes{@{term[source]"op + x y"}}. 

47269  46 
\end{warn} 
47 

48 
HOL also supports some basic constructs from functional programming: 

49 
\begin{quote} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52361
diff
changeset

50 
@{text "(if b then t\<^sub>1 else t\<^sub>2)"}\\ 
47269  51 
@{text "(let x = t in u)"}\\ 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52361
diff
changeset

52 
@{text "(case t of pat\<^sub>1 \<Rightarrow> t\<^sub>1  \<dots>  pat\<^sub>n \<Rightarrow> t\<^sub>n)"} 
47269  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 

55317  61 
\conceptidx{Formulas}{formula} are terms of type @{text bool}. 
47269  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 

55317  66 
\conceptidx{Equality}{equality} is available in the form of the infix function @{text "="} 
47269  67 
of type @{typ "'a \<Rightarrow> 'a \<Rightarrow> bool"}. It also works for formulas, where 
68 
it means ``if and only if''. 

69 

55317  70 
\conceptidx{Quantifiers}{quantifier} are written @{prop"\<forall>x. P"} and @{prop"\<exists>x. P"}. 
47269  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 

55317  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 

57804  76 
\mbox{\noquotes{@{term[source] "m + (n::nat)"}}}. Type constraints may be 
47269  77 
needed to 
57804  78 
disambiguate terms involving overloaded functions such as @{text "+"}. 
47269  79 

55348  80 
Finally there are the universal quantifier @{text"\<And>"}\index{$4@\isasymAnd} and the implication 
81 
@{text"\<Longrightarrow>"}\index{$3@\isasymLongrightarrow}. They are part of the Isabelle framework, not the logic 

47269  82 
HOL. Logically, they agree with their HOL counterparts @{text"\<forall>"} and 
83 
@{text"\<longrightarrow>"}, but operationally they behave differently. This will become 

84 
clearer as we go along. 

85 
\begin{warn} 

86 
Rightarrows of all kinds always associate to the right. In particular, 

87 
the formula 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52361
diff
changeset

88 
@{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)"}. 
58655  89 
The (Isabellespecific\footnote{To display implications in this style in 
90 
Isabelle/jedit you need to set Plugins $>$ Plugin Options $>$ Isabelle/General $>$ Print Mode to ``\texttt{brackets}'' and restart.}) notation \mbox{@{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"}} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52361
diff
changeset

91 
is short for the iterated implication \mbox{@{text"A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> A"}}. 
47269  92 
Sometimes we also employ inference rule notation: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52361
diff
changeset

93 
\inferrule{\mbox{@{text "A\<^sub>1"}}\\ \mbox{@{text "\<dots>"}}\\ \mbox{@{text "A\<^sub>n"}}} 
47269  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. 

57804  103 
All Isabelle text needs to go into a theory. 
47269  104 
The general format of a theory @{text T} is 
105 
\begin{quote} 

55348  106 
\indexed{\isacom{theory}}{theory} @{text T}\\ 
107 
\indexed{\isacom{imports}}{imports} @{text "T\<^sub>1 \<dots> T\<^sub>n"}\\ 

47269  108 
\isacom{begin}\\ 
109 
\emph{definitions, theorems and proofs}\\ 

110 
\isacom{end} 

111 
\end{quote} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52361
diff
changeset

112 
where @{text "T\<^sub>1 \<dots> T\<^sub>n"} are the names of existing 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52361
diff
changeset

113 
theories that @{text T} is based on. The @{text "T\<^sub>i"} are the 
55317  114 
direct \conceptidx{parent theories}{parent theory} of @{text T}. 
47269  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} 

55317  120 
HOL contains a theory @{theory Main}\index{Main@@{theory Main}}, the union of all the basic 
47269  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 

54703  127 
(see @{url "http://isabelle.in.tum.de/library/HOL/"}) 
47269  128 
there is also the \emph{Archive of Formal Proofs} 
54703  129 
at @{url "http://afp.sourceforge.net"}, a growing collection of Isabelle theories 
47269  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 

52361  136 
the types and formulas of HOL. To distinguish the two levels, everything 
47269  137 
HOLspecific (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 
(*>*) 