src/Doc/ProgProve/Bool_nat_list.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 55465 0d31c0546286
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 Bool_nat_list
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
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     7
text{*
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     8
\vspace{-4ex}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     9
\section{\texorpdfstring{Types @{typ bool}, @{typ nat} and @{text list}}{Types bool, nat and list}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    10
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    11
These are the most important predefined types. We go through them one by one.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    12
Based on examples we learn how to define (possibly recursive) functions and
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    13
prove theorems about them by induction and simplification.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    14
55317
834a84553e02 started index
nipkow
parents: 54508
diff changeset
    15
\subsection{Type \indexed{@{typ bool}}{bool}}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    16
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    17
The type of boolean values is a predefined datatype
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    18
@{datatype[display] bool}
55317
834a84553e02 started index
nipkow
parents: 54508
diff changeset
    19
with the two values \indexed{@{const True}}{True} and \indexed{@{const False}}{False} and
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    20
with many predefined functions:  @{text "\<not>"}, @{text "\<and>"}, @{text "\<or>"}, @{text
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    21
"\<longrightarrow>"} etc. Here is how conjunction could be defined by pattern matching:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    22
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    23
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    24
fun conj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    25
"conj True True = True" |
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    26
"conj _ _ = False"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    27
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    28
text{* Both the datatype and function definitions roughly follow the syntax
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    29
of functional programming languages.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    30
55317
834a84553e02 started index
nipkow
parents: 54508
diff changeset
    31
\subsection{Type \indexed{@{typ nat}}{nat}}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    32
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    33
Natural numbers are another predefined datatype:
55317
834a84553e02 started index
nipkow
parents: 54508
diff changeset
    34
@{datatype[display] nat}\index{Suc@@{const Suc}}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    35
All values of type @{typ nat} are generated by the constructors
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    36
@{text 0} and @{const Suc}. Thus the values of type @{typ nat} are
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    37
@{text 0}, @{term"Suc 0"}, @{term"Suc(Suc 0)"} etc.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    38
There are many predefined functions: @{text "+"}, @{text "*"}, @{text
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    39
"\<le>"}, etc. Here is how you could define your own addition:
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
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    42
fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    43
"add 0 n = n" |
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    44
"add (Suc m) n = Suc(add m n)"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    45
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    46
text{* And here is a proof of the fact that @{prop"add m 0 = m"}: *}
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
lemma add_02: "add m 0 = m"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    49
apply(induction m)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    50
apply(auto)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    51
done
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    52
(*<*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    53
lemma "add m 0 = m"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    54
apply(induction m)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    55
(*>*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    56
txt{* The \isacom{lemma} command starts the proof and gives the lemma
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    57
a name, @{text add_02}. Properties of recursively defined functions
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    58
need to be established by induction in most cases.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    59
Command \isacom{apply}@{text"(induction m)"} instructs Isabelle to
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    60
start a proof by induction on @{text m}. In response, it will show the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    61
following proof state:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    62
@{subgoals[display,indent=0]}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    63
The numbered lines are known as \emph{subgoals}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    64
The first subgoal is the base case, the second one the induction step.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    65
The prefix @{text"\<And>m."} is Isabelle's way of saying ``for an arbitrary but fixed @{text m}''. The @{text"\<Longrightarrow>"} separates assumptions from the conclusion.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    66
The command \isacom{apply}@{text"(auto)"} instructs Isabelle to try
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    67
and prove all subgoals automatically, essentially by simplifying them.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    68
Because both subgoals are easy, Isabelle can do it.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    69
The base case @{prop"add 0 0 = 0"} holds by definition of @{const add},
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    70
and the induction step is almost as simple:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    71
@{text"add\<^raw:~>(Suc m) 0 = Suc(add m 0) = Suc m"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    72
using first the definition of @{const add} and then the induction hypothesis.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    73
In summary, both subproofs rely on simplification with function definitions and
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    74
the induction hypothesis.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    75
As a result of that final \isacom{done}, Isabelle associates the lemma
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    76
just proved with its name. You can now inspect the lemma with the command
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    77
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    78
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    79
thm add_02
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    80
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    81
txt{* which displays @{thm[show_question_marks,display] add_02} The free
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    82
variable @{text m} has been replaced by the \concept{unknown}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    83
@{text"?m"}. There is no logical difference between the two but an
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    84
operational one: unknowns can be instantiated, which is what you want after
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    85
some lemma has been proved.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    86
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    87
Note that there is also a proof method @{text induct}, which behaves almost
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    88
like @{text induction}; the difference is explained in \autoref{ch:Isar}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    89
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    90
\begin{warn}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    91
Terminology: We use \concept{lemma}, \concept{theorem} and \concept{rule}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    92
interchangeably for propositions that have been proved.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    93
\end{warn}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    94
\begin{warn}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    95
  Numerals (@{text 0}, @{text 1}, @{text 2}, \dots) and most of the standard
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    96
  arithmetic operations (@{text "+"}, @{text "-"}, @{text "*"}, @{text"\<le>"},
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    97
  @{text"<"} etc) are overloaded: they are available
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    98
  not just for natural numbers but for other types as well.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    99
  For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   100
  that you are talking about natural numbers. Hence Isabelle can only infer
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   101
  that @{term x} is of some arbitrary type where @{text 0} and @{text"+"}
54508
nipkow
parents: 54467
diff changeset
   102
  exist. As a consequence, you will be unable to prove the goal.
nipkow
parents: 54467
diff changeset
   103
%  To alert you to such pitfalls, Isabelle flags numerals without a
nipkow
parents: 54467
diff changeset
   104
%  fixed type in its output: @ {prop"x+0 = x"}.
nipkow
parents: 54467
diff changeset
   105
  In this particular example, you need to include
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   106
  an explicit type constraint, for example @{text"x+0 = (x::nat)"}. If there
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   107
  is enough contextual information this may not be necessary: @{prop"Suc x =
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   108
  x"} automatically implies @{text"x::nat"} because @{term Suc} is not
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   109
  overloaded.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   110
\end{warn}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   111
52361
7d5ad23b8245 all headings in upper case
nipkow
parents: 48985
diff changeset
   112
\subsubsection{An Informal Proof}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   113
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   114
Above we gave some terse informal explanation of the proof of
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   115
@{prop"add m 0 = m"}. A more detailed informal exposition of the lemma
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   116
might look like this:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   117
\bigskip
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
\noindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   120
\textbf{Lemma} @{prop"add m 0 = m"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   121
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   122
\noindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   123
\textbf{Proof} by induction on @{text m}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   124
\begin{itemize}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   125
\item Case @{text 0} (the base case): @{prop"add 0 0 = 0"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   126
  holds by definition of @{const add}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   127
\item Case @{term"Suc m"} (the induction step):
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   128
  We assume @{prop"add m 0 = m"}, the induction hypothesis (IH),
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   129
  and we need to show @{text"add (Suc m) 0 = Suc m"}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   130
  The proof is as follows:\smallskip
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
  \begin{tabular}{@ {}rcl@ {\quad}l@ {}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   133
  @{term "add (Suc m) 0"} &@{text"="}& @{term"Suc(add m 0)"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   134
  & by definition of @{text add}\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   135
              &@{text"="}& @{term "Suc m"} & by IH
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   136
  \end{tabular}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   137
\end{itemize}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   138
Throughout this book, \concept{IH} will stand for ``induction hypothesis''.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   139
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   140
We have now seen three proofs of @{prop"add m 0 = 0"}: the Isabelle one, the
47711
c1cca2a052e4 doc update
nipkow
parents: 47306
diff changeset
   141
terse four lines explaining the base case and the induction step, and just now a
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   142
model of a traditional inductive proof. The three proofs differ in the level
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   143
of detail given and the intended reader: the Isabelle proof is for the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   144
machine, the informal proofs are for humans. Although this book concentrates
47711
c1cca2a052e4 doc update
nipkow
parents: 47306
diff changeset
   145
on Isabelle proofs, it is important to be able to rephrase those proofs
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   146
as informal text comprehensible to a reader familiar with traditional
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   147
mathematical proofs. Later on we will introduce an Isabelle proof language
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   148
that is closer to traditional informal mathematical language and is often
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   149
directly readable.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   150
55317
834a84553e02 started index
nipkow
parents: 54508
diff changeset
   151
\subsection{Type \indexed{@{text list}}{list}}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   152
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   153
Although lists are already predefined, we define our own copy just for
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   154
demonstration purposes:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   155
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   156
(*<*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   157
apply(auto)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   158
done 
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   159
declare [[names_short]]
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   160
(*>*)
47302
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   161
datatype 'a list = Nil | Cons 'a "'a list"
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   162
47302
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   163
text{*
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   164
\begin{itemize}
47711
c1cca2a052e4 doc update
nipkow
parents: 47306
diff changeset
   165
\item Type @{typ "'a list"} is the type of lists over elements of type @{typ 'a}. Because @{typ 'a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
47302
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   166
\item Lists have two constructors: @{const Nil}, the empty list, and @{const Cons}, which puts an element (of type @{typ 'a}) in front of a list (of type @{typ "'a list"}).
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   167
Hence all lists are of the form @{const Nil}, or @{term"Cons x Nil"},
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   168
or @{term"Cons x (Cons y Nil)"} etc.
47302
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   169
\item \isacom{datatype} requires no quotation marks on the
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   170
left-hand side, but on the right-hand side each of the argument
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   171
types of a constructor needs to be enclosed in quotation marks, unless
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   172
it is just an identifier (e.g.\ @{typ nat} or @{typ 'a}).
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   173
\end{itemize}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   174
We also define two standard functions, append and reverse: *}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   175
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   176
fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   177
"app Nil ys = ys" |
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   178
"app (Cons x xs) ys = Cons x (app xs ys)"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   179
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   180
fun rev :: "'a list \<Rightarrow> 'a list" where
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   181
"rev Nil = Nil" |
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   182
"rev (Cons x xs) = app (rev xs) (Cons x Nil)"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   183
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   184
text{* By default, variables @{text xs}, @{text ys} and @{text zs} are of
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   185
@{text list} type.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   186
55320
8a6ee5c1f2e0 tuned latex
nipkow
parents: 55318
diff changeset
   187
Command \indexed{\isacommand{value}}{value} evaluates a term. For example, *}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   188
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   189
value "rev(Cons True (Cons False Nil))"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   190
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   191
text{* yields the result @{value "rev(Cons True (Cons False Nil))"}. This works symbolically, too: *}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   192
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   193
value "rev(Cons a (Cons b Nil))"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   194
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   195
text{* yields @{value "rev(Cons a (Cons b Nil))"}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   196
\medskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   197
47302
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   198
Figure~\ref{fig:MyList} shows the theory created so far.
47719
8aac84627b84 the perennial doc problem of how to define lists a second time
nipkow
parents: 47711
diff changeset
   199
Because @{text list}, @{const Nil}, @{const Cons} etc are already predefined,
8aac84627b84 the perennial doc problem of how to define lists a second time
nipkow
parents: 47711
diff changeset
   200
 Isabelle prints qualified (long) names when executing this theory, for example, @{text MyList.Nil}
8aac84627b84 the perennial doc problem of how to define lists a second time
nipkow
parents: 47711
diff changeset
   201
 instead of @{const Nil}.
8aac84627b84 the perennial doc problem of how to define lists a second time
nipkow
parents: 47711
diff changeset
   202
 To suppress the qualified names you can insert the command
8aac84627b84 the perennial doc problem of how to define lists a second time
nipkow
parents: 47711
diff changeset
   203
 \texttt{declare [[names\_short]]}.
8aac84627b84 the perennial doc problem of how to define lists a second time
nipkow
parents: 47711
diff changeset
   204
 This is not recommended in general but just for this unusual example.
47302
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   205
% Notice where the
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   206
%quotations marks are needed that we mostly sweep under the carpet.  In
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   207
%particular, notice that \isacom{datatype} requires no quotation marks on the
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   208
%left-hand side, but that on the right-hand side each of the argument
70239da25ef6 towards showing " in the tutorial
nipkow
parents: 47269
diff changeset
   209
%types of a constructor needs to be enclosed in quotation marks.
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   210
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   211
\begin{figure}[htbp]
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   212
\begin{alltt}
48947
7eee8b2d2099 more standard document preparation within session context;
wenzelm
parents: 47719
diff changeset
   213
\input{MyList.thy}\end{alltt}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   214
\caption{A Theory of Lists}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   215
\label{fig:MyList}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   216
\end{figure}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   217
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   218
\subsubsection{Structural Induction for Lists}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   219
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   220
Just as for natural numbers, there is a proof principle of induction for
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   221
lists. Induction over a list is essentially induction over the length of
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   222
the list, although the length remains implicit. To prove that some property
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   223
@{text P} holds for all lists @{text xs}, i.e.\ \mbox{@{prop"P(xs)"}},
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   224
you need to prove
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   225
\begin{enumerate}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   226
\item the base case @{prop"P(Nil)"} and
47711
c1cca2a052e4 doc update
nipkow
parents: 47306
diff changeset
   227
\item the inductive case @{prop"P(Cons x xs)"} under the assumption @{prop"P(xs)"}, for some arbitrary but fixed @{text x} and @{text xs}.
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   228
\end{enumerate}
55318
nipkow
parents: 55317
diff changeset
   229
This is often called \concept{structural induction} for lists.
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   230
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   231
\subsection{The Proof Process}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   232
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   233
We will now demonstrate the typical proof process, which involves
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   234
the formulation and proof of auxiliary lemmas.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   235
Our goal is to show that reversing a list twice produces the original
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   236
list. *}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   237
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   238
theorem rev_rev [simp]: "rev(rev xs) = xs"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   239
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   240
txt{* Commands \isacom{theorem} and \isacom{lemma} are
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   241
interchangeable and merely indicate the importance we attach to a
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   242
proposition. Via the bracketed attribute @{text simp} we also tell Isabelle
55317
834a84553e02 started index
nipkow
parents: 54508
diff changeset
   243
to make the eventual theorem a \conceptnoidx{simplification rule}: future proofs
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   244
involving simplification will replace occurrences of @{term"rev(rev xs)"} by
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   245
@{term"xs"}. The proof is by induction: *}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   246
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   247
apply(induction xs)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   248
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   249
txt{*
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   250
As explained above, we obtain two subgoals, namely the base case (@{const Nil}) and the induction step (@{const Cons}):
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   251
@{subgoals[display,indent=0,margin=65]}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   252
Let us try to solve both goals automatically:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   253
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   254
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   255
apply(auto)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   256
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   257
txt{*Subgoal~1 is proved, and disappears; the simplified version
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   258
of subgoal~2 becomes the new subgoal~1:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   259
@{subgoals[display,indent=0,margin=70]}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   260
In order to simplify this subgoal further, a lemma suggests itself.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   261
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   262
\subsubsection{A First Lemma}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   263
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   264
We insert the following lemma in front of the main theorem:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   265
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   266
(*<*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   267
oops
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   268
(*>*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   269
lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   270
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   271
txt{* There are two variables that we could induct on: @{text xs} and
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   272
@{text ys}. Because @{const app} is defined by recursion on
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   273
the first argument, @{text xs} is the correct one:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   274
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   275
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   276
apply(induction xs)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   277
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   278
txt{* This time not even the base case is solved automatically: *}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   279
apply(auto)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   280
txt{*
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   281
\vspace{-5ex}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   282
@{subgoals[display,goals_limit=1]}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   283
Again, we need to abandon this proof attempt and prove another simple lemma
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   284
first.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   285
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   286
\subsubsection{A Second Lemma}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   287
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   288
We again try the canonical proof procedure:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   289
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   290
(*<*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   291
oops
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   292
(*>*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   293
lemma app_Nil2 [simp]: "app xs Nil = xs"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   294
apply(induction xs)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   295
apply(auto)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   296
done
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   297
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   298
text{*
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   299
Thankfully, this worked.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   300
Now we can continue with our stuck proof attempt of the first lemma:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   301
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   302
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   303
lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   304
apply(induction xs)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   305
apply(auto)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   306
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   307
txt{*
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   308
We find that this time @{text"auto"} solves the base case, but the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   309
induction step merely simplifies to
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   310
@{subgoals[display,indent=0,goals_limit=1]}
47711
c1cca2a052e4 doc update
nipkow
parents: 47306
diff changeset
   311
The missing lemma is associativity of @{const app},
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   312
which we insert in front of the failed lemma @{text rev_app}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   313
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   314
\subsubsection{Associativity of @{const app}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   315
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   316
The canonical proof procedure succeeds without further ado:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   317
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   318
(*<*)oops(*>*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   319
lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   320
apply(induction xs)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   321
apply(auto)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   322
done
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   323
(*<*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   324
lemma rev_app [simp]: "rev(app xs ys) = app (rev ys)(rev xs)"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   325
apply(induction xs)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   326
apply(auto)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   327
done
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   328
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   329
theorem rev_rev [simp]: "rev(rev xs) = xs"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   330
apply(induction xs)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   331
apply(auto)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   332
done
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   333
(*>*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   334
text{*
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   335
Finally the proofs of @{thm[source] rev_app} and @{thm[source] rev_rev}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   336
succeed, too.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   337
52361
7d5ad23b8245 all headings in upper case
nipkow
parents: 48985
diff changeset
   338
\subsubsection{Another Informal Proof}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   339
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   340
Here is the informal proof of associativity of @{const app}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   341
corresponding to the Isabelle proof above.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   342
\bigskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   343
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   344
\noindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   345
\textbf{Lemma} @{prop"app (app xs ys) zs = app xs (app ys zs)"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   346
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   347
\noindent
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   348
\textbf{Proof} by induction on @{text xs}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   349
\begin{itemize}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   350
\item Case @{text Nil}: \ @{prop"app (app Nil ys) zs = app ys zs"} @{text"="}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   351
  \mbox{@{term"app Nil (app ys zs)"}} \ holds by definition of @{text app}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   352
\item Case @{text"Cons x xs"}: We assume
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   353
  \begin{center} \hfill @{term"app (app xs ys) zs"} @{text"="}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   354
  @{term"app xs (app ys zs)"} \hfill (IH) \end{center}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   355
  and we need to show
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   356
  \begin{center} @{prop"app (app (Cons x xs) ys) zs = app (Cons x xs) (app ys zs)"}.\end{center}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   357
  The proof is as follows:\smallskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   358
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   359
  \begin{tabular}{@ {}l@ {\quad}l@ {}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   360
  @{term"app (app (Cons x xs) ys) zs"}\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   361
  @{text"= app (Cons x (app xs ys)) zs"} & by definition of @{text app}\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   362
  @{text"= Cons x (app (app xs ys) zs)"} & by definition of @{text app}\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   363
  @{text"= Cons x (app xs (app ys zs))"} & by IH\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   364
  @{text"= app (Cons x xs) (app ys zs)"} & by definition of @{text app}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   365
  \end{tabular}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   366
\end{itemize}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   367
\medskip
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   368
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   369
\noindent Didn't we say earlier that all proofs are by simplification? But
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   370
in both cases, going from left to right, the last equality step is not a
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   371
simplification at all! In the base case it is @{prop"app ys zs = app Nil (app
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   372
ys zs)"}. It appears almost mysterious because we suddenly complicate the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   373
term by appending @{text Nil} on the left. What is really going on is this:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   374
when proving some equality \mbox{@{prop"s = t"}}, both @{text s} and @{text t} are
54467
663a927fdc88 comments by Sean Seefried
nipkow
parents: 54436
diff changeset
   375
simplified until they ``meet in the middle''. This heuristic for equality proofs
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   376
works well for a functional programming context like ours. In the base case
54467
663a927fdc88 comments by Sean Seefried
nipkow
parents: 54436
diff changeset
   377
both @{term"app (app Nil ys) zs"} and @{term"app Nil (app
663a927fdc88 comments by Sean Seefried
nipkow
parents: 54436
diff changeset
   378
ys zs)"} are simplified to @{term"app ys zs"}, the term in the middle.
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   379
52361
7d5ad23b8245 all headings in upper case
nipkow
parents: 48985
diff changeset
   380
\subsection{Predefined Lists}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   381
\label{sec:predeflists}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   382
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   383
Isabelle's predefined lists are the same as the ones above, but with
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   384
more syntactic sugar:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   385
\begin{itemize}
55317
834a84553e02 started index
nipkow
parents: 54508
diff changeset
   386
\item @{text "[]"} is \indexed{@{const Nil}}{Nil},
834a84553e02 started index
nipkow
parents: 54508
diff changeset
   387
\item @{term"x # xs"} is @{term"Cons x xs"}\index{Cons@@{const Cons}},
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52842
diff changeset
   388
\item @{text"[x\<^sub>1, \<dots>, x\<^sub>n]"} is @{text"x\<^sub>1 # \<dots> # x\<^sub>n # []"}, and
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   389
\item @{term "xs @ ys"} is @{term"app xs ys"}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   390
\end{itemize}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   391
There is also a large library of predefined functions.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   392
The most important ones are the length function
55317
834a84553e02 started index
nipkow
parents: 54508
diff changeset
   393
@{text"length :: 'a list \<Rightarrow> nat"}\index{length@@{const length}} (with the obvious definition),
834a84553e02 started index
nipkow
parents: 54508
diff changeset
   394
and the \indexed{@{const map}}{map} function that applies a function to all elements of a list:
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   395
\begin{isabelle}
47306
56d72c923281 made sure that " is shown in tutorial text
nipkow
parents: 47302
diff changeset
   396
\isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"}\\
55465
0d31c0546286 merged 'List.map' and 'List.list.map'
blanchet
parents: 55320
diff changeset
   397
@{text"\""}@{thm list.map(1)}@{text"\" |"}\\
0d31c0546286 merged 'List.map' and 'List.list.map'
blanchet
parents: 55320
diff changeset
   398
@{text"\""}@{thm list.map(2)}@{text"\""}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   399
\end{isabelle}
52782
b11d73dbfb76 tuned intro
nipkow
parents: 52718
diff changeset
   400
b11d73dbfb76 tuned intro
nipkow
parents: 52718
diff changeset
   401
\ifsem
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   402
Also useful are the \concept{head} of a list, its first element,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   403
and the \concept{tail}, the rest of the list:
55317
834a84553e02 started index
nipkow
parents: 54508
diff changeset
   404
\begin{isabelle}\index{hd@@{const hd}}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   405
\isacom{fun} @{text"hd :: 'a list \<Rightarrow> 'a"}\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   406
@{prop"hd(x#xs) = x"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   407
\end{isabelle}
55317
834a84553e02 started index
nipkow
parents: 54508
diff changeset
   408
\begin{isabelle}\index{tl@@{const tl}}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   409
\isacom{fun} @{text"tl :: 'a list \<Rightarrow> 'a list"}\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   410
@{prop"tl [] = []"} @{text"|"}\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   411
@{prop"tl(x#xs) = xs"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   412
\end{isabelle}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   413
Note that since HOL is a logic of total functions, @{term"hd []"} is defined,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   414
but we do now know what the result is. That is, @{term"hd []"} is not undefined
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   415
but underdefined.
52782
b11d73dbfb76 tuned intro
nipkow
parents: 52718
diff changeset
   416
\fi
47306
56d72c923281 made sure that " is shown in tutorial text
nipkow
parents: 47302
diff changeset
   417
%
52593
aedf7b01c6e4 added exercises
nipkow
parents: 52361
diff changeset
   418
52842
3682e1b7ce86 tuned exercises
nipkow
parents: 52782
diff changeset
   419
From now on lists are always the predefined lists.
3682e1b7ce86 tuned exercises
nipkow
parents: 52782
diff changeset
   420
3682e1b7ce86 tuned exercises
nipkow
parents: 52782
diff changeset
   421
54436
nipkow
parents: 54121
diff changeset
   422
\subsection*{Exercises}
52593
aedf7b01c6e4 added exercises
nipkow
parents: 52361
diff changeset
   423
aedf7b01c6e4 added exercises
nipkow
parents: 52361
diff changeset
   424
\begin{exercise}
54121
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   425
Use the \isacom{value} command to evaluate the following expressions:
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   426
@{term[source] "1 + (2::nat)"}, @{term[source] "1 + (2::int)"},
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   427
@{term[source] "1 - (2::nat)"} and @{term[source] "1 - (2::int)"}.
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   428
\end{exercise}
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   429
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   430
\begin{exercise}
52842
3682e1b7ce86 tuned exercises
nipkow
parents: 52782
diff changeset
   431
Start from the definition of @{const add} given above.
54467
663a927fdc88 comments by Sean Seefried
nipkow
parents: 54436
diff changeset
   432
Prove that @{const add} is associative and commutative.
54121
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   433
Define a recursive function @{text double} @{text"::"} @{typ"nat \<Rightarrow> nat"}
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   434
and prove @{prop"double m = add m m"}.
52593
aedf7b01c6e4 added exercises
nipkow
parents: 52361
diff changeset
   435
\end{exercise}
52718
0faf89b8d928 tuned exercises
nipkow
parents: 52593
diff changeset
   436
52593
aedf7b01c6e4 added exercises
nipkow
parents: 52361
diff changeset
   437
\begin{exercise}
52842
3682e1b7ce86 tuned exercises
nipkow
parents: 52782
diff changeset
   438
Define a function @{text"count ::"} @{typ"'a \<Rightarrow> 'a list \<Rightarrow> nat"}
3682e1b7ce86 tuned exercises
nipkow
parents: 52782
diff changeset
   439
that counts the number of occurrences of an element in a list. Prove
3682e1b7ce86 tuned exercises
nipkow
parents: 52782
diff changeset
   440
@{prop"count x xs \<le> length xs"}.
3682e1b7ce86 tuned exercises
nipkow
parents: 52782
diff changeset
   441
\end{exercise}
3682e1b7ce86 tuned exercises
nipkow
parents: 52782
diff changeset
   442
3682e1b7ce86 tuned exercises
nipkow
parents: 52782
diff changeset
   443
\begin{exercise}
3682e1b7ce86 tuned exercises
nipkow
parents: 52782
diff changeset
   444
Define a recursive function @{text "snoc ::"} @{typ"'a list \<Rightarrow> 'a \<Rightarrow> 'a list"}
54121
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   445
that appends an element to the end of a list. With the help of @{text snoc}
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   446
define a recursive function @{text "reverse ::"} @{typ"'a list \<Rightarrow> 'a list"}
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   447
that reverses a list. Prove @{prop"reverse(reverse xs) = xs"}.
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   448
\end{exercise}
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   449
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   450
\begin{exercise}
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   451
Define a recursive function @{text "sum ::"} @{typ"nat \<Rightarrow> nat"} such that
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   452
\mbox{@{text"sum n"}} @{text"="} @{text"0 + ... + n"} and prove
4e7d71037bb6 tuned exercises
nipkow
parents: 53015
diff changeset
   453
@{prop" sum(n::nat) = n * (n+1) div 2"}.
52593
aedf7b01c6e4 added exercises
nipkow
parents: 52361
diff changeset
   454
\end{exercise}
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   455
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   456
(*<*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   457
end
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   458
(*>*)