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