src/Doc/Prog_Prove/Isar.thy
author nipkow
Thu Nov 09 10:24:00 2017 +0100 (19 months ago)
changeset 67039 690b4b334889
parent 65437 b8fc7e2e1b35
child 67299 ba52a058942f
permissions -rw-r--r--
Replaced Raw Proof Blocks by Local Lemmas
nipkow@47269
     1
(*<*)
nipkow@47269
     2
theory Isar
nipkow@47269
     3
imports LaTeXsugar
nipkow@47269
     4
begin
wenzelm@52059
     5
declare [[quick_and_dirty]]
nipkow@47269
     6
(*>*)
nipkow@47269
     7
text{*
nipkow@47269
     8
Apply-scripts are unreadable and hard to maintain. The language of choice
nipkow@47269
     9
for larger proofs is \concept{Isar}. The two key features of Isar are:
nipkow@47269
    10
\begin{itemize}
nipkow@47269
    11
\item It is structured, not linear.
nipkow@56989
    12
\item It is readable without its being run because
nipkow@47269
    13
you need to state what you are proving at any given point.
nipkow@47269
    14
\end{itemize}
nipkow@47269
    15
Whereas apply-scripts are like assembly language programs, Isar proofs
nipkow@47269
    16
are like structured programs with comments. A typical Isar proof looks like this:
nipkow@47269
    17
*}text{*
nipkow@47269
    18
\begin{tabular}{@ {}l}
nipkow@47269
    19
\isacom{proof}\\
nipkow@47269
    20
\quad\isacom{assume} @{text"\""}$\mathit{formula}_0$@{text"\""}\\
nipkow@47269
    21
\quad\isacom{have} @{text"\""}$\mathit{formula}_1$@{text"\""} \quad\isacom{by} @{text simp}\\
nipkow@47269
    22
\quad\vdots\\
nipkow@47269
    23
\quad\isacom{have} @{text"\""}$\mathit{formula}_n$@{text"\""} \quad\isacom{by} @{text blast}\\
nipkow@47269
    24
\quad\isacom{show} @{text"\""}$\mathit{formula}_{n+1}$@{text"\""} \quad\isacom{by} @{text \<dots>}\\
nipkow@47269
    25
\isacom{qed}
nipkow@47269
    26
\end{tabular}
nipkow@47269
    27
*}text{*
nipkow@47269
    28
It proves $\mathit{formula}_0 \Longrightarrow \mathit{formula}_{n+1}$
nipkow@47704
    29
(provided each proof step succeeds).
nipkow@47269
    30
The intermediate \isacom{have} statements are merely stepping stones
nipkow@47269
    31
on the way towards the \isacom{show} statement that proves the actual
nipkow@47269
    32
goal. In more detail, this is the Isar core syntax:
nipkow@47269
    33
\medskip
nipkow@47269
    34
nipkow@47269
    35
\begin{tabular}{@ {}lcl@ {}}
nipkow@55359
    36
\textit{proof} &=& \indexed{\isacom{by}}{by} \textit{method}\\
nipkow@55359
    37
      &$\mid$& \indexed{\isacom{proof}}{proof} [\textit{method}] \ \textit{step}$^*$ \ \indexed{\isacom{qed}}{qed}
nipkow@47269
    38
\end{tabular}
nipkow@47269
    39
\medskip
nipkow@47269
    40
nipkow@47269
    41
\begin{tabular}{@ {}lcl@ {}}
nipkow@55359
    42
\textit{step} &=& \indexed{\isacom{fix}}{fix} \textit{variables} \\
nipkow@55359
    43
      &$\mid$& \indexed{\isacom{assume}}{assume} \textit{proposition} \\
nipkow@55359
    44
      &$\mid$& [\indexed{\isacom{from}}{from} \textit{fact}$^+$] (\indexed{\isacom{have}}{have} $\mid$ \indexed{\isacom{show}}{show}) \ \textit{proposition} \ \textit{proof}
nipkow@47269
    45
\end{tabular}
nipkow@47269
    46
\medskip
nipkow@47269
    47
nipkow@47269
    48
\begin{tabular}{@ {}lcl@ {}}
nipkow@47269
    49
\textit{proposition} &=& [\textit{name}:] @{text"\""}\textit{formula}@{text"\""}
nipkow@47269
    50
\end{tabular}
nipkow@47269
    51
\medskip
nipkow@47269
    52
nipkow@47269
    53
\begin{tabular}{@ {}lcl@ {}}
nipkow@47269
    54
\textit{fact} &=& \textit{name} \ $\mid$ \ \dots
nipkow@47269
    55
\end{tabular}
nipkow@47269
    56
\medskip
nipkow@47269
    57
nipkow@47269
    58
\noindent A proof can either be an atomic \isacom{by} with a single proof
nipkow@47269
    59
method which must finish off the statement being proved, for example @{text
nipkow@56989
    60
auto},  or it can be a \isacom{proof}--\isacom{qed} block of multiple
nipkow@47269
    61
steps. Such a block can optionally begin with a proof method that indicates
nipkow@58504
    62
how to start off the proof, e.g., \mbox{@{text"(induction xs)"}}.
nipkow@47269
    63
nipkow@47269
    64
A step either assumes a proposition or states a proposition
nipkow@47269
    65
together with its proof. The optional \isacom{from} clause
nipkow@47269
    66
indicates which facts are to be used in the proof.
nipkow@47269
    67
Intermediate propositions are stated with \isacom{have}, the overall goal
nipkow@56989
    68
is stated with \isacom{show}. A step can also introduce new local variables with
nipkow@47269
    69
\isacom{fix}. Logically, \isacom{fix} introduces @{text"\<And>"}-quantified
nipkow@47269
    70
variables, \isacom{assume} introduces the assumption of an implication
nipkow@56989
    71
(@{text"\<Longrightarrow>"}) and \isacom{have}/\isacom{show} introduce the conclusion.
nipkow@47269
    72
nipkow@47269
    73
Propositions are optionally named formulas. These names can be referred to in
nipkow@47269
    74
later \isacom{from} clauses. In the simplest case, a fact is such a name.
nipkow@47269
    75
But facts can also be composed with @{text OF} and @{text of} as shown in
nipkow@58602
    76
\autoref{sec:forward-proof} --- hence the \dots\ in the above grammar.  Note
nipkow@47269
    77
that assumptions, intermediate \isacom{have} statements and global lemmas all
nipkow@47269
    78
have the same status and are thus collectively referred to as
nipkow@55317
    79
\conceptidx{facts}{fact}.
nipkow@47269
    80
nipkow@47269
    81
Fact names can stand for whole lists of facts. For example, if @{text f} is
nipkow@47269
    82
defined by command \isacom{fun}, @{text"f.simps"} refers to the whole list of
nipkow@47269
    83
recursion equations defining @{text f}. Individual facts can be selected by
nipkow@56989
    84
writing @{text"f.simps(2)"}, whole sublists by writing @{text"f.simps(2-4)"}.
nipkow@47269
    85
nipkow@47269
    86
nipkow@52361
    87
\section{Isar by Example}
nipkow@47269
    88
nipkow@47704
    89
We show a number of proofs of Cantor's theorem that a function from a set to
nipkow@47269
    90
its powerset cannot be surjective, illustrating various features of Isar. The
nipkow@47269
    91
constant @{const surj} is predefined.
nipkow@47269
    92
*}
nipkow@47269
    93
nipkow@47269
    94
lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
nipkow@47269
    95
proof
nipkow@47269
    96
  assume 0: "surj f"
nipkow@47269
    97
  from 0 have 1: "\<forall>A. \<exists>a. A = f a" by(simp add: surj_def)
nipkow@47269
    98
  from 1 have 2: "\<exists>a. {x. x \<notin> f x} = f a" by blast
nipkow@47269
    99
  from 2 show "False" by blast
nipkow@47269
   100
qed
nipkow@47269
   101
nipkow@47269
   102
text{*
nipkow@56989
   103
The \isacom{proof} command lacks an explicit method by which to perform
nipkow@47269
   104
the proof. In such cases Isabelle tries to use some standard introduction
nipkow@47269
   105
rule, in the above case for @{text"\<not>"}:
nipkow@47269
   106
\[
nipkow@47269
   107
\inferrule{
nipkow@47269
   108
\mbox{@{thm (prem 1) notI}}}
nipkow@47269
   109
{\mbox{@{thm (concl) notI}}}
nipkow@47269
   110
\]
nipkow@47269
   111
In order to prove @{prop"~ P"}, assume @{text P} and show @{text False}.
nipkow@64852
   112
Thus we may assume \mbox{\noquotes{@{prop [source] "surj f"}}}. The proof shows that names of propositions
nipkow@58602
   113
may be (single!) digits --- meaningful names are hard to invent and are often
nipkow@47269
   114
not necessary. Both \isacom{have} steps are obvious. The second one introduces
nipkow@47269
   115
the diagonal set @{term"{x. x \<notin> f x}"}, the key idea in the proof.
nipkow@47269
   116
If you wonder why @{text 2} directly implies @{text False}: from @{text 2}
nipkow@47269
   117
it follows that @{prop"a \<notin> f a \<longleftrightarrow> a \<in> f a"}.
nipkow@47269
   118
nipkow@55359
   119
\subsection{\indexed{@{text this}}{this}, \indexed{\isacom{then}}{then}, \indexed{\isacom{hence}}{hence} and \indexed{\isacom{thus}}{thus}}
nipkow@47269
   120
nipkow@47269
   121
Labels should be avoided. They interrupt the flow of the reader who has to
nipkow@47269
   122
scan the context for the point where the label was introduced. Ideally, the
nipkow@47269
   123
proof is a linear flow, where the output of one step becomes the input of the
nipkow@58605
   124
next step, piping the previously proved fact into the next proof, like
nipkow@47269
   125
in a UNIX pipe. In such cases the predefined name @{text this} can be used
nipkow@47269
   126
to refer to the proposition proved in the previous step. This allows us to
nipkow@47269
   127
eliminate all labels from our proof (we suppress the \isacom{lemma} statement):
nipkow@47269
   128
*}
nipkow@47269
   129
(*<*)
nipkow@47269
   130
lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
nipkow@47269
   131
(*>*)
nipkow@47269
   132
proof
nipkow@47269
   133
  assume "surj f"
nipkow@47269
   134
  from this have "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
nipkow@47269
   135
  from this show "False" by blast
nipkow@47269
   136
qed
nipkow@47269
   137
nipkow@47269
   138
text{* We have also taken the opportunity to compress the two \isacom{have}
nipkow@47269
   139
steps into one.
nipkow@47269
   140
nipkow@47269
   141
To compact the text further, Isar has a few convenient abbreviations:
nipkow@47269
   142
\medskip
nipkow@47269
   143
nipkow@54839
   144
\begin{tabular}{r@ {\quad=\quad}l}
nipkow@54839
   145
\isacom{then} & \isacom{from} @{text this}\\
nipkow@54839
   146
\isacom{thus} & \isacom{then} \isacom{show}\\
nipkow@54839
   147
\isacom{hence} & \isacom{then} \isacom{have}
nipkow@47269
   148
\end{tabular}
nipkow@47269
   149
\medskip
nipkow@47269
   150
nipkow@47269
   151
\noindent
nipkow@47269
   152
With the help of these abbreviations the proof becomes
nipkow@47269
   153
*}
nipkow@47269
   154
(*<*)
nipkow@47269
   155
lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
nipkow@47269
   156
(*>*)
nipkow@47269
   157
proof
nipkow@47269
   158
  assume "surj f"
nipkow@47269
   159
  hence "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
nipkow@47269
   160
  thus "False" by blast
nipkow@47269
   161
qed
nipkow@47269
   162
text{*
nipkow@47269
   163
nipkow@47269
   164
There are two further linguistic variations:
nipkow@47269
   165
\medskip
nipkow@47269
   166
nipkow@54839
   167
\begin{tabular}{r@ {\quad=\quad}l}
nipkow@55359
   168
(\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \indexed{\isacom{using}}{using} \ \textit{facts}
nipkow@54839
   169
&
nipkow@47269
   170
\isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\
nipkow@55359
   171
\indexed{\isacom{with}}{with} \ \textit{facts} & \isacom{from} \ \textit{facts} \isa{this}
nipkow@47269
   172
\end{tabular}
nipkow@47269
   173
\medskip
nipkow@47269
   174
nipkow@47711
   175
\noindent The \isacom{using} idiom de-emphasizes the used facts by moving them
nipkow@47269
   176
behind the proposition.
nipkow@47269
   177
nipkow@55359
   178
\subsection{Structured Lemma Statements: \indexed{\isacom{fixes}}{fixes}, \indexed{\isacom{assumes}}{assumes}, \indexed{\isacom{shows}}{shows}}
nipkow@55359
   179
\index{lemma@\isacom{lemma}}
nipkow@47269
   180
Lemmas can also be stated in a more structured fashion. To demonstrate this
nipkow@64852
   181
feature with Cantor's theorem, we rephrase \noquotes{@{prop[source]"\<not> surj f"}}
nipkow@47269
   182
a little:
nipkow@47269
   183
*}
nipkow@47269
   184
nipkow@47269
   185
lemma
nipkow@47269
   186
  fixes f :: "'a \<Rightarrow> 'a set"
nipkow@47269
   187
  assumes s: "surj f"
nipkow@47269
   188
  shows "False"
nipkow@47269
   189
nipkow@47269
   190
txt{* The optional \isacom{fixes} part allows you to state the types of
nipkow@47269
   191
variables up front rather than by decorating one of their occurrences in the
nipkow@47269
   192
formula with a type constraint. The key advantage of the structured format is
nipkow@47306
   193
the \isacom{assumes} part that allows you to name each assumption; multiple
nipkow@47306
   194
assumptions can be separated by \isacom{and}. The
nipkow@47269
   195
\isacom{shows} part gives the goal. The actual theorem that will come out of
nipkow@64852
   196
the proof is \noquotes{@{prop[source]"surj f \<Longrightarrow> False"}}, but during the proof the assumption
nipkow@64852
   197
\noquotes{@{prop[source]"surj f"}} is available under the name @{text s} like any other fact.
nipkow@47269
   198
*}
nipkow@47269
   199
nipkow@47269
   200
proof -
nipkow@47269
   201
  have "\<exists> a. {x. x \<notin> f x} = f a" using s
nipkow@47269
   202
    by(auto simp: surj_def)
nipkow@47269
   203
  thus "False" by blast
nipkow@47269
   204
qed
nipkow@47269
   205
nipkow@56312
   206
text{*
nipkow@56312
   207
\begin{warn}
nipkow@56312
   208
Note the hyphen after the \isacom{proof} command.
nipkow@56989
   209
It is the null method that does nothing to the goal. Leaving it out would be asking
nipkow@58602
   210
Isabelle to try some suitable introduction rule on the goal @{const False} --- but
nipkow@56312
   211
there is no such rule and \isacom{proof} would fail.
nipkow@56312
   212
\end{warn}
nipkow@64852
   213
In the \isacom{have} step the assumption \noquotes{@{prop[source]"surj f"}} is now
nipkow@64852
   214
referenced by its name @{text s}. The duplication of \noquotes{@{prop[source]"surj f"}} in the
nipkow@47269
   215
above proofs (once in the statement of the lemma, once in its proof) has been
nipkow@47269
   216
eliminated.
nipkow@47269
   217
nipkow@47704
   218
Stating a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the
nipkow@55359
   219
name \indexed{@{text assms}}{assms} that stands for the list of all assumptions. You can refer
nipkow@58521
   220
to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"}, etc.,
nipkow@47269
   221
thus obviating the need to name them individually.
nipkow@47269
   222
nipkow@52361
   223
\section{Proof Patterns}
nipkow@47269
   224
nipkow@47269
   225
We show a number of important basic proof patterns. Many of them arise from
nipkow@47269
   226
the rules of natural deduction that are applied by \isacom{proof} by
nipkow@47269
   227
default. The patterns are phrased in terms of \isacom{show} but work for
nipkow@47269
   228
\isacom{have} and \isacom{lemma}, too.
nipkow@47269
   229
nipkow@65348
   230
\ifsem\else
nipkow@65348
   231
\subsection{Logic}
nipkow@65348
   232
\fi
nipkow@65348
   233
nipkow@47711
   234
We start with two forms of \concept{case analysis}:
nipkow@47269
   235
starting from a formula @{text P} we have the two cases @{text P} and
nipkow@47269
   236
@{prop"~P"}, and starting from a fact @{prop"P \<or> Q"}
nipkow@47269
   237
we have the two cases @{text P} and @{text Q}:
nipkow@47269
   238
*}text_raw{*
nipkow@47269
   239
\begin{tabular}{@ {}ll@ {}}
nipkow@47269
   240
\begin{minipage}[t]{.4\textwidth}
nipkow@47269
   241
\isa{%
nipkow@47269
   242
*}
nipkow@47269
   243
(*<*)lemma "R" proof-(*>*)
nipkow@47269
   244
show "R"
nipkow@47269
   245
proof cases
nipkow@47269
   246
  assume "P"
wenzelm@58999
   247
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   248
  show "R" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   249
next
nipkow@47269
   250
  assume "\<not> P"
wenzelm@58999
   251
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   252
  show "R" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   253
qed(*<*)oops(*>*)
nipkow@47269
   254
text_raw {* }
nipkow@55361
   255
\end{minipage}\index{cases@@{text cases}}
nipkow@47269
   256
&
nipkow@47269
   257
\begin{minipage}[t]{.4\textwidth}
nipkow@47269
   258
\isa{%
nipkow@47269
   259
*}
nipkow@47269
   260
(*<*)lemma "R" proof-(*>*)
nipkow@65348
   261
have "P \<or> Q" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   262
then show "R"
nipkow@47269
   263
proof
nipkow@47269
   264
  assume "P"
wenzelm@58999
   265
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   266
  show "R" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   267
next
nipkow@47269
   268
  assume "Q"
wenzelm@58999
   269
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   270
  show "R" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   271
qed(*<*)oops(*>*)
nipkow@47269
   272
nipkow@47269
   273
text_raw {* }
nipkow@47269
   274
\end{minipage}
nipkow@47269
   275
\end{tabular}
nipkow@47269
   276
\medskip
nipkow@47269
   277
\begin{isamarkuptext}%
nipkow@47269
   278
How to prove a logical equivalence:
nipkow@47269
   279
\end{isamarkuptext}%
nipkow@47269
   280
\isa{%
nipkow@47269
   281
*}
nipkow@47269
   282
(*<*)lemma "P\<longleftrightarrow>Q" proof-(*>*)
nipkow@47269
   283
show "P \<longleftrightarrow> Q"
nipkow@47269
   284
proof
nipkow@47269
   285
  assume "P"
wenzelm@58999
   286
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   287
  show "Q" (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
nipkow@47269
   288
next
nipkow@47269
   289
  assume "Q"
wenzelm@58999
   290
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   291
  show "P" (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
nipkow@47269
   292
qed(*<*)qed(*>*)
nipkow@47269
   293
text_raw {* }
nipkow@47269
   294
\medskip
nipkow@47269
   295
\begin{isamarkuptext}%
nipkow@55361
   296
Proofs by contradiction (@{thm[source] ccontr} stands for ``classical contradiction''):
nipkow@47269
   297
\end{isamarkuptext}%
nipkow@47269
   298
\begin{tabular}{@ {}ll@ {}}
nipkow@47269
   299
\begin{minipage}[t]{.4\textwidth}
nipkow@47269
   300
\isa{%
nipkow@47269
   301
*}
nipkow@47269
   302
(*<*)lemma "\<not> P" proof-(*>*)
nipkow@47269
   303
show "\<not> P"
nipkow@47269
   304
proof
nipkow@47269
   305
  assume "P"
wenzelm@58999
   306
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   307
  show "False" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   308
qed(*<*)oops(*>*)
nipkow@47269
   309
nipkow@47269
   310
text_raw {* }
nipkow@47269
   311
\end{minipage}
nipkow@47269
   312
&
nipkow@47269
   313
\begin{minipage}[t]{.4\textwidth}
nipkow@47269
   314
\isa{%
nipkow@47269
   315
*}
nipkow@47269
   316
(*<*)lemma "P" proof-(*>*)
nipkow@47269
   317
show "P"
nipkow@47269
   318
proof (rule ccontr)
nipkow@47269
   319
  assume "\<not>P"
wenzelm@58999
   320
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   321
  show "False" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   322
qed(*<*)oops(*>*)
nipkow@47269
   323
nipkow@47269
   324
text_raw {* }
nipkow@47269
   325
\end{minipage}
nipkow@47269
   326
\end{tabular}
nipkow@47269
   327
\medskip
nipkow@47269
   328
\begin{isamarkuptext}%
nipkow@47269
   329
How to prove quantified formulas:
nipkow@47269
   330
\end{isamarkuptext}%
nipkow@47269
   331
\begin{tabular}{@ {}ll@ {}}
nipkow@47269
   332
\begin{minipage}[t]{.4\textwidth}
nipkow@47269
   333
\isa{%
nipkow@47269
   334
*}
nipkow@47269
   335
(*<*)lemma "ALL x. P x" proof-(*>*)
nipkow@47269
   336
show "\<forall>x. P(x)"
nipkow@47269
   337
proof
nipkow@47269
   338
  fix x
wenzelm@58999
   339
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   340
  show "P(x)" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   341
qed(*<*)oops(*>*)
nipkow@47269
   342
nipkow@47269
   343
text_raw {* }
nipkow@47269
   344
\end{minipage}
nipkow@47269
   345
&
nipkow@47269
   346
\begin{minipage}[t]{.4\textwidth}
nipkow@47269
   347
\isa{%
nipkow@47269
   348
*}
nipkow@47269
   349
(*<*)lemma "EX x. P(x)" proof-(*>*)
nipkow@47269
   350
show "\<exists>x. P(x)"
nipkow@47269
   351
proof
wenzelm@58999
   352
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   353
  show "P(witness)" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   354
qed
nipkow@47269
   355
(*<*)oops(*>*)
nipkow@47269
   356
nipkow@47269
   357
text_raw {* }
nipkow@47269
   358
\end{minipage}
nipkow@47269
   359
\end{tabular}
nipkow@47269
   360
\medskip
nipkow@47269
   361
\begin{isamarkuptext}%
nipkow@47269
   362
In the proof of \noquotes{@{prop[source]"\<forall>x. P(x)"}},
nipkow@55361
   363
the step \indexed{\isacom{fix}}{fix}~@{text x} introduces a locally fixed variable @{text x}
nipkow@47269
   364
into the subproof, the proverbial ``arbitrary but fixed value''.
nipkow@47269
   365
Instead of @{text x} we could have chosen any name in the subproof.
nipkow@47269
   366
In the proof of \noquotes{@{prop[source]"\<exists>x. P(x)"}},
nipkow@47269
   367
@{text witness} is some arbitrary
nipkow@47269
   368
term for which we can prove that it satisfies @{text P}.
nipkow@47269
   369
nipkow@47269
   370
How to reason forward from \noquotes{@{prop[source] "\<exists>x. P(x)"}}:
nipkow@47269
   371
\end{isamarkuptext}%
nipkow@47269
   372
*}
nipkow@47269
   373
(*<*)lemma True proof- assume 1: "EX x. P x"(*>*)
nipkow@65348
   374
have "\<exists>x. P(x)" (*<*)by(rule 1)(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   375
then obtain x where p: "P(x)" by blast
nipkow@47269
   376
(*<*)oops(*>*)
nipkow@47269
   377
text{*
nipkow@55389
   378
After the \indexed{\isacom{obtain}}{obtain} step, @{text x} (we could have chosen any name)
nipkow@47269
   379
is a fixed local
nipkow@47269
   380
variable, and @{text p} is the name of the fact
nipkow@47269
   381
\noquotes{@{prop[source] "P(x)"}}.
nipkow@47269
   382
This pattern works for one or more @{text x}.
nipkow@47269
   383
As an example of the \isacom{obtain} command, here is the proof of
nipkow@47269
   384
Cantor's theorem in more detail:
nipkow@47269
   385
*}
nipkow@47269
   386
nipkow@47269
   387
lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
nipkow@47269
   388
proof
nipkow@47269
   389
  assume "surj f"
nipkow@47269
   390
  hence  "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
nipkow@47269
   391
  then obtain a where  "{x. x \<notin> f x} = f a"  by blast
nipkow@47269
   392
  hence  "a \<notin> f a \<longleftrightarrow> a \<in> f a"  by blast
nipkow@47269
   393
  thus "False" by blast
nipkow@47269
   394
qed
nipkow@47269
   395
nipkow@47269
   396
text_raw{*
nipkow@47269
   397
\begin{isamarkuptext}%
nipkow@47306
   398
nipkow@47306
   399
Finally, how to prove set equality and subset relationship:
nipkow@47269
   400
\end{isamarkuptext}%
nipkow@47269
   401
\begin{tabular}{@ {}ll@ {}}
nipkow@47269
   402
\begin{minipage}[t]{.4\textwidth}
nipkow@47269
   403
\isa{%
nipkow@47269
   404
*}
nipkow@47269
   405
(*<*)lemma "A = (B::'a set)" proof-(*>*)
nipkow@47269
   406
show "A = B"
nipkow@47269
   407
proof
nipkow@65348
   408
  show "A \<subseteq> B" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   409
next
nipkow@65348
   410
  show "B \<subseteq> A" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   411
qed(*<*)qed(*>*)
nipkow@47269
   412
nipkow@47269
   413
text_raw {* }
nipkow@47269
   414
\end{minipage}
nipkow@47269
   415
&
nipkow@47269
   416
\begin{minipage}[t]{.4\textwidth}
nipkow@47269
   417
\isa{%
nipkow@47269
   418
*}
nipkow@47269
   419
(*<*)lemma "A <= (B::'a set)" proof-(*>*)
nipkow@47269
   420
show "A \<subseteq> B"
nipkow@47269
   421
proof
nipkow@47269
   422
  fix x
nipkow@47269
   423
  assume "x \<in> A"
wenzelm@58999
   424
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   425
  show "x \<in> B" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   426
qed(*<*)qed(*>*)
nipkow@47269
   427
nipkow@47269
   428
text_raw {* }
nipkow@47269
   429
\end{minipage}
nipkow@47269
   430
\end{tabular}
nipkow@47269
   431
\begin{isamarkuptext}%
nipkow@65348
   432
nipkow@65348
   433
\ifsem\else
nipkow@65348
   434
\subsection{Chains of (In)Equations}
nipkow@65348
   435
nipkow@65348
   436
In textbooks, chains of equations (and inequations) are often displayed like this:
nipkow@65348
   437
\begin{quote}
nipkow@65348
   438
\begin{tabular}{@ {}l@ {\qquad}l@ {}}
nipkow@65348
   439
$t_1 = t_2$ & \isamath{\,\langle\mathit{justification}\rangle}\\
nipkow@65348
   440
$\phantom{t_1} = t_3$ & \isamath{\,\langle\mathit{justification}\rangle}\\
nipkow@65348
   441
\quad $\vdots$\\
nipkow@65348
   442
$\phantom{t_1} = t_n$ & \isamath{\,\langle\mathit{justification}\rangle}
nipkow@65348
   443
\end{tabular}
nipkow@65348
   444
\end{quote}
nipkow@65348
   445
The Isar equivalent is this:
nipkow@65348
   446
nipkow@65348
   447
\begin{samepage}
nipkow@65348
   448
\begin{quote}
nipkow@65348
   449
\isakeyword{have} \<open>"t\<^sub>1 = t\<^sub>2"\<close> \isasymproof\\
nipkow@65348
   450
\isakeyword{also have} \<open>"... = t\<^sub>3"\<close> \isasymproof\\
nipkow@65348
   451
\quad $\vdots$\\
nipkow@65348
   452
\isakeyword{also have} \<open>"... = t\<^sub>n"\<close> \isasymproof \\
nipkow@65349
   453
\isakeyword{finally show} \<open>"t\<^sub>1 = t\<^sub>n"\<close>\ \texttt{.}
nipkow@65348
   454
\end{quote}
nipkow@65348
   455
\end{samepage}
nipkow@65348
   456
nipkow@65348
   457
\noindent
nipkow@65348
   458
The ``\<open>...\<close>'' and ``\<open>.\<close>'' deserve some explanation:
nipkow@65348
   459
\begin{description}
nipkow@65348
   460
\item[``\<open>...\<close>''] is literally three dots. It is the name of an unknown that Isar
nipkow@65348
   461
automatically instantiates with the right-hand side of the previous equation.
nipkow@65348
   462
In general, if \<open>this\<close> is the theorem @{term "p t\<^sub>1 t\<^sub>2"} then ``\<open>...\<close>''
nipkow@65348
   463
stands for \<open>t\<^sub>2\<close>.
nipkow@65349
   464
\item[``\<open>.\<close>''] (a single dot) is a proof method that solves a goal by one of the
nipkow@65352
   465
assumptions. This works here because the result of \isakeyword{finally}
nipkow@65349
   466
is the theorem \mbox{\<open>t\<^sub>1 = t\<^sub>n\<close>},
nipkow@65349
   467
\isakeyword{show} \<open>"t\<^sub>1 = t\<^sub>n"\<close> states the theorem explicitly,
nipkow@65349
   468
and ``\<open>.\<close>'' proves the theorem with the result of \isakeyword{finally}.
nipkow@65348
   469
\end{description}
nipkow@65348
   470
The above proof template also works for arbitrary mixtures of \<open>=\<close>, \<open>\<le>\<close> and \<open><\<close>,
nipkow@65348
   471
for example:
nipkow@65348
   472
\begin{quote}
nipkow@65348
   473
\isakeyword{have} \<open>"t\<^sub>1 < t\<^sub>2"\<close> \isasymproof\\
nipkow@65348
   474
\isakeyword{also have} \<open>"... = t\<^sub>3"\<close> \isasymproof\\
nipkow@65348
   475
\quad $\vdots$\\
nipkow@65348
   476
\isakeyword{also have} \<open>"... \<le> t\<^sub>n"\<close> \isasymproof \\
nipkow@65349
   477
\isakeyword{finally show} \<open>"t\<^sub>1 < t\<^sub>n"\<close>\ \texttt{.}
nipkow@65348
   478
\end{quote}
nipkow@65349
   479
The relation symbol in the \isakeyword{finally} step needs to be the most precise one
nipkow@65349
   480
possible. In the example above, you must not write \<open>t\<^sub>1 \<le> t\<^sub>n\<close> instead of \mbox{\<open>t\<^sub>1 < t\<^sub>n\<close>}.
nipkow@65348
   481
nipkow@65348
   482
\begin{warn}
nipkow@65348
   483
Isabelle only supports \<open>=\<close>, \<open>\<le>\<close> and \<open><\<close> but not \<open>\<ge>\<close> and \<open>>\<close>
nipkow@65348
   484
in (in)equation chains (by default).
nipkow@65348
   485
\end{warn}
nipkow@65348
   486
nipkow@65348
   487
If you want to go beyond merely using the above proof patterns and want to
nipkow@65348
   488
understand what \isakeyword{also} and \isakeyword{finally} mean, read on.
nipkow@65348
   489
There is an Isar theorem variable called \<open>calculation\<close>, similar to \<open>this\<close>.
nipkow@65348
   490
When the first \isakeyword{also} in a chain is encountered, Isabelle sets
nipkow@65348
   491
\<open>calculation := this\<close>. In each subsequent \isakeyword{also} step,
nipkow@65348
   492
Isabelle composes the theorems \<open>calculation\<close> and \<open>this\<close> (i.e.\ the two previous
nipkow@65348
   493
(in)equalities) using some predefined set of rules including transitivity
nipkow@65348
   494
of \<open>=\<close>, \<open>\<le>\<close> and \<open><\<close> but also mixed rules like @{prop"\<lbrakk> x \<le> y; y < z \<rbrakk> \<Longrightarrow> x < z"}.
nipkow@65348
   495
The result of this composition is assigned to \<open>calculation\<close>. Consider
nipkow@65348
   496
\begin{quote}
nipkow@65348
   497
\isakeyword{have} \<open>"t\<^sub>1 \<le> t\<^sub>2"\<close> \isasymproof\\
nipkow@65348
   498
\isakeyword{also} \isakeyword{have} \<open>"... < t\<^sub>3"\<close> \isasymproof\\
nipkow@65348
   499
\isakeyword{also} \isakeyword{have} \<open>"... = t\<^sub>4"\<close> \isasymproof\\
nipkow@65349
   500
\isakeyword{finally show} \<open>"t\<^sub>1 < t\<^sub>4"\<close>\ \texttt{.}
nipkow@65348
   501
\end{quote}
nipkow@65348
   502
After the first \isakeyword{also}, \<open>calculation\<close> is \<open>"t\<^sub>1 \<le> t\<^sub>2"\<close>,
nipkow@65348
   503
and after the second \isakeyword{also}, \<open>calculation\<close> is \<open>"t\<^sub>1 < t\<^sub>3"\<close>.
nipkow@65348
   504
The command \isakeyword{finally} is short for \isakeyword{also from} \<open>calculation\<close>.
nipkow@65348
   505
Therefore the \isakeyword{also} hidden in \isakeyword{finally} sets \<open>calculation\<close>
nipkow@65348
   506
to \<open>t\<^sub>1 < t\<^sub>4\<close> and the final ``\texttt{.}'' succeeds.
nipkow@65348
   507
nipkow@65348
   508
For more information on this style of proof see \cite{BauerW-TPHOLs01}.
nipkow@65348
   509
\fi
nipkow@65348
   510
nipkow@52361
   511
\section{Streamlining Proofs}
nipkow@47269
   512
nipkow@52361
   513
\subsection{Pattern Matching and Quotations}
nipkow@47269
   514
nipkow@47269
   515
In the proof patterns shown above, formulas are often duplicated.
nipkow@47269
   516
This can make the text harder to read, write and maintain. Pattern matching
nipkow@47269
   517
is an abbreviation mechanism to avoid such duplication. Writing
nipkow@47269
   518
\begin{quote}
nipkow@55359
   519
\isacom{show} \ \textit{formula} @{text"("}\indexed{\isacom{is}}{is} \textit{pattern}@{text")"}
nipkow@47269
   520
\end{quote}
nipkow@47269
   521
matches the pattern against the formula, thus instantiating the unknowns in
nipkow@47269
   522
the pattern for later use. As an example, consider the proof pattern for
nipkow@47269
   523
@{text"\<longleftrightarrow>"}:
nipkow@47269
   524
\end{isamarkuptext}%
nipkow@47269
   525
*}
wenzelm@53015
   526
(*<*)lemma "formula\<^sub>1 \<longleftrightarrow> formula\<^sub>2" proof-(*>*)
wenzelm@53015
   527
show "formula\<^sub>1 \<longleftrightarrow> formula\<^sub>2" (is "?L \<longleftrightarrow> ?R")
nipkow@47269
   528
proof
nipkow@47269
   529
  assume "?L"
wenzelm@58999
   530
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   531
  show "?R" (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
nipkow@47269
   532
next
nipkow@47269
   533
  assume "?R"
wenzelm@58999
   534
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   535
  show "?L" (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
nipkow@47269
   536
qed(*<*)qed(*>*)
nipkow@47269
   537
wenzelm@53015
   538
text{* Instead of duplicating @{text"formula\<^sub>i"} in the text, we introduce
nipkow@47269
   539
the two abbreviations @{text"?L"} and @{text"?R"} by pattern matching.
nipkow@47269
   540
Pattern matching works wherever a formula is stated, in particular
nipkow@47269
   541
with \isacom{have} and \isacom{lemma}.
nipkow@47269
   542
nipkow@55359
   543
The unknown \indexed{@{text"?thesis"}}{thesis} is implicitly matched against any goal stated by
nipkow@47269
   544
\isacom{lemma} or \isacom{show}. Here is a typical example: *}
nipkow@47269
   545
nipkow@47269
   546
lemma "formula"
nipkow@47269
   547
proof -
wenzelm@58999
   548
  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
nipkow@65348
   549
  show ?thesis (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
nipkow@47269
   550
qed
nipkow@47269
   551
nipkow@47269
   552
text{* 
nipkow@55359
   553
Unknowns can also be instantiated with \indexed{\isacom{let}}{let} commands
nipkow@47269
   554
\begin{quote}
nipkow@47269
   555
\isacom{let} @{text"?t"} = @{text"\""}\textit{some-big-term}@{text"\""}
nipkow@47269
   556
\end{quote}
nipkow@47269
   557
Later proof steps can refer to @{text"?t"}:
nipkow@47269
   558
\begin{quote}
nipkow@47269
   559
\isacom{have} @{text"\""}\dots @{text"?t"} \dots@{text"\""}
nipkow@47269
   560
\end{quote}
nipkow@47269
   561
\begin{warn}
nipkow@47269
   562
Names of facts are introduced with @{text"name:"} and refer to proved
nipkow@47269
   563
theorems. Unknowns @{text"?X"} refer to terms or formulas.
nipkow@47269
   564
\end{warn}
nipkow@47269
   565
nipkow@47269
   566
Although abbreviations shorten the text, the reader needs to remember what
nipkow@47269
   567
they stand for. Similarly for names of facts. Names like @{text 1}, @{text 2}
nipkow@47269
   568
and @{text 3} are not helpful and should only be used in short proofs. For
nipkow@47704
   569
longer proofs, descriptive names are better. But look at this example:
nipkow@47269
   570
\begin{quote}
nipkow@47269
   571
\isacom{have} \ @{text"x_gr_0: \"x > 0\""}\\
nipkow@47269
   572
$\vdots$\\
nipkow@47269
   573
\isacom{from} @{text "x_gr_0"} \dots
nipkow@47269
   574
\end{quote}
nipkow@56989
   575
The name is longer than the fact it stands for! Short facts do not need names;
nipkow@47269
   576
one can refer to them easily by quoting them:
nipkow@47269
   577
\begin{quote}
nipkow@47269
   578
\isacom{have} \ @{text"\"x > 0\""}\\
nipkow@47269
   579
$\vdots$\\
nipkow@55359
   580
\isacom{from} @{text "`x>0`"} \dots\index{$IMP053@@{text"`...`"}}
nipkow@47269
   581
\end{quote}
nipkow@55317
   582
Note that the quotes around @{text"x>0"} are \conceptnoidx{back quotes}.
nipkow@47269
   583
They refer to the fact not by name but by value.
nipkow@47269
   584
nipkow@55359
   585
\subsection{\indexed{\isacom{moreover}}{moreover}}
nipkow@55359
   586
\index{ultimately@\isacom{ultimately}}
nipkow@47269
   587
nipkow@47269
   588
Sometimes one needs a number of facts to enable some deduction. Of course
nipkow@47269
   589
one can name these facts individually, as shown on the right,
nipkow@47269
   590
but one can also combine them with \isacom{moreover}, as shown on the left:
nipkow@47269
   591
*}text_raw{*
nipkow@47269
   592
\begin{tabular}{@ {}ll@ {}}
nipkow@47269
   593
\begin{minipage}[t]{.4\textwidth}
nipkow@47269
   594
\isa{%
nipkow@47269
   595
*}
nipkow@47269
   596
(*<*)lemma "P" proof-(*>*)
nipkow@65348
   597
have "P\<^sub>1" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@65348
   598
moreover have "P\<^sub>2" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   599
moreover
wenzelm@58999
   600
text_raw{*\\$\vdots$\\\hspace{-1.4ex}*}(*<*)have "True" ..(*>*)
nipkow@65348
   601
moreover have "P\<^sub>n" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@65348
   602
ultimately have "P"  (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   603
(*<*)oops(*>*)
nipkow@47269
   604
nipkow@47269
   605
text_raw {* }
nipkow@47269
   606
\end{minipage}
nipkow@47269
   607
&
nipkow@47269
   608
\qquad
nipkow@47269
   609
\begin{minipage}[t]{.4\textwidth}
nipkow@47269
   610
\isa{%
nipkow@47269
   611
*}
nipkow@47269
   612
(*<*)lemma "P" proof-(*>*)
nipkow@65348
   613
have lab\<^sub>1: "P\<^sub>1" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@65348
   614
have lab\<^sub>2: "P\<^sub>2" (*<*)sorry(*>*)text_raw{*\ \isasymproof*}
wenzelm@58999
   615
text_raw{*\\$\vdots$\\\hspace{-1.4ex}*}
nipkow@65348
   616
have lab\<^sub>n: "P\<^sub>n" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
wenzelm@58999
   617
from lab\<^sub>1 lab\<^sub>2 text_raw{*\ $\dots$\\*}
nipkow@65348
   618
have "P"  (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
   619
(*<*)oops(*>*)
nipkow@47269
   620
nipkow@47269
   621
text_raw {* }
nipkow@47269
   622
\end{minipage}
nipkow@47269
   623
\end{tabular}
nipkow@47269
   624
\begin{isamarkuptext}%
nipkow@65348
   625
The \isacom{moreover} version is no shorter but expresses the structure
nipkow@65348
   626
a bit more clearly and avoids new names.
nipkow@47269
   627
nipkow@67039
   628
\subsection{Local Lemmas}
nipkow@47269
   629
nipkow@56989
   630
Sometimes one would like to prove some lemma locally within a proof,
nipkow@56989
   631
a lemma that shares the current context of assumptions but that
nipkow@58502
   632
has its own assumptions and is generalized over its locally fixed
nipkow@67039
   633
variables at the end. This is simply an extension of the basic
nipkow@67039
   634
\indexed{\isacom{have}}{have} construct:
nipkow@67039
   635
\begin{quote}
nipkow@67039
   636
\indexed{\isacom{have}}{have} @{text"B"}\
nipkow@67039
   637
 \indexed{\isacom{if}}{if} \<open>name:\<close> @{text"A\<^sub>1 \<dots> A\<^sub>m"}\
nipkow@67039
   638
 \indexed{\isacom{for}}{for} @{text"x\<^sub>1 \<dots> x\<^sub>n"}\\
nipkow@67039
   639
\isasymproof
nipkow@47269
   640
\end{quote}
wenzelm@53015
   641
proves @{text"\<lbrakk> A\<^sub>1; \<dots> ; A\<^sub>m \<rbrakk> \<Longrightarrow> B"}
wenzelm@53015
   642
where all @{text"x\<^sub>i"} have been replaced by unknowns @{text"?x\<^sub>i"}.
nipkow@47269
   643
As an example we prove a simple fact about divisibility on integers.
nipkow@47269
   644
The definition of @{text "dvd"} is @{thm dvd_def}.
nipkow@47269
   645
\end{isamarkuptext}%
nipkow@47269
   646
*}
nipkow@47269
   647
nipkow@47269
   648
lemma fixes a b :: int assumes "b dvd (a+b)" shows "b dvd a"
nipkow@47269
   649
proof -
nipkow@67039
   650
  have "\<exists>k'. a = b*k'" if asm: "a+b = b*k" for k
nipkow@67039
   651
  proof
nipkow@67039
   652
    show "a = b*(k - 1)" using asm by(simp add: algebra_simps)
nipkow@67039
   653
  qed
nipkow@47269
   654
  then show ?thesis using assms by(auto simp add: dvd_def)
nipkow@47269
   655
qed
nipkow@47269
   656
nipkow@67039
   657
text{*
nipkow@47269
   658
nipkow@54436
   659
\subsection*{Exercises}
nipkow@52706
   660
nipkow@52661
   661
\exercise
nipkow@52661
   662
Give a readable, structured proof of the following lemma:
nipkow@52661
   663
*}
nipkow@54218
   664
lemma assumes T: "\<forall>x y. T x y \<or> T y x"
nipkow@54218
   665
  and A: "\<forall>x y. A x y \<and> A y x \<longrightarrow> x = y"
nipkow@54218
   666
  and TA: "\<forall>x y. T x y \<longrightarrow> A x y" and "A x y"
nipkow@54218
   667
  shows "T x y"
nipkow@52661
   668
(*<*)oops(*>*)
nipkow@52661
   669
text{*
nipkow@52661
   670
\endexercise
nipkow@52661
   671
nipkow@52706
   672
\exercise
nipkow@52706
   673
Give a readable, structured proof of the following lemma:
nipkow@52706
   674
*}
nipkow@67039
   675
lemma "\<exists>ys zs. xs = ys @ zs \<and>
nipkow@67039
   676
            (length ys = length zs \<or> length ys = length zs + 1)"
nipkow@52706
   677
(*<*)oops(*>*)
nipkow@52706
   678
text{*
nipkow@52706
   679
Hint: There are predefined functions @{const_typ take} and @{const_typ drop}
nipkow@52706
   680
such that @{text"take k [x\<^sub>1,\<dots>] = [x\<^sub>1,\<dots>,x\<^sub>k]"} and
nipkow@54218
   681
@{text"drop k [x\<^sub>1,\<dots>] = [x\<^bsub>k+1\<^esub>,\<dots>]"}. Let sledgehammer find and apply
nipkow@54218
   682
the relevant @{const take} and @{const drop} lemmas for you.
nipkow@52706
   683
\endexercise
nipkow@52706
   684
nipkow@54218
   685
nipkow@52361
   686
\section{Case Analysis and Induction}
nipkow@55361
   687
nipkow@52361
   688
\subsection{Datatype Case Analysis}
nipkow@55361
   689
\index{case analysis|(}
nipkow@47269
   690
nipkow@47711
   691
We have seen case analysis on formulas. Now we want to distinguish
nipkow@47269
   692
which form some term takes: is it @{text 0} or of the form @{term"Suc n"},
nipkow@47269
   693
is it @{term"[]"} or of the form @{term"x#xs"}, etc. Here is a typical example
nipkow@47711
   694
proof by case analysis on the form of @{text xs}:
nipkow@47269
   695
*}
nipkow@47269
   696
nipkow@47269
   697
lemma "length(tl xs) = length xs - 1"
nipkow@47269
   698
proof (cases xs)
nipkow@47269
   699
  assume "xs = []"
nipkow@47269
   700
  thus ?thesis by simp
nipkow@47269
   701
next
nipkow@47269
   702
  fix y ys assume "xs = y#ys"
nipkow@47269
   703
  thus ?thesis by simp
nipkow@47269
   704
qed
nipkow@47269
   705
blanchet@55417
   706
text{*\index{cases@@{text"cases"}|(}Function @{text tl} (''tail'') is defined by @{thm list.sel(2)} and
blanchet@55417
   707
@{thm list.sel(3)}. Note that the result type of @{const length} is @{typ nat}
nipkow@47269
   708
and @{prop"0 - 1 = (0::nat)"}.
nipkow@47269
   709
nipkow@47269
   710
This proof pattern works for any term @{text t} whose type is a datatype.
nipkow@47269
   711
The goal has to be proved for each constructor @{text C}:
nipkow@47269
   712
\begin{quote}
wenzelm@53015
   713
\isacom{fix} \ @{text"x\<^sub>1 \<dots> x\<^sub>n"} \isacom{assume} @{text"\"t = C x\<^sub>1 \<dots> x\<^sub>n\""}
nipkow@55361
   714
\end{quote}\index{case@\isacom{case}|(}
nipkow@47269
   715
Each case can be written in a more compact form by means of the \isacom{case}
nipkow@47269
   716
command:
nipkow@47269
   717
\begin{quote}
wenzelm@53015
   718
\isacom{case} @{text "(C x\<^sub>1 \<dots> x\<^sub>n)"}
nipkow@47269
   719
\end{quote}
nipkow@47704
   720
This is equivalent to the explicit \isacom{fix}-\isacom{assume} line
wenzelm@53015
   721
but also gives the assumption @{text"\"t = C x\<^sub>1 \<dots> x\<^sub>n\""} a name: @{text C},
nipkow@47269
   722
like the constructor.
nipkow@47269
   723
Here is the \isacom{case} version of the proof above:
nipkow@47269
   724
*}
nipkow@47269
   725
(*<*)lemma "length(tl xs) = length xs - 1"(*>*)
nipkow@47269
   726
proof (cases xs)
nipkow@47269
   727
  case Nil
nipkow@47269
   728
  thus ?thesis by simp
nipkow@47269
   729
next
nipkow@47269
   730
  case (Cons y ys)
nipkow@47269
   731
  thus ?thesis by simp
nipkow@47269
   732
qed
nipkow@47269
   733
nipkow@47269
   734
text{* Remember that @{text Nil} and @{text Cons} are the alphanumeric names
nipkow@47269
   735
for @{text"[]"} and @{text"#"}. The names of the assumptions
nipkow@47269
   736
are not used because they are directly piped (via \isacom{thus})
nipkow@47269
   737
into the proof of the claim.
nipkow@55361
   738
\index{case analysis|)}
nipkow@47269
   739
nipkow@52361
   740
\subsection{Structural Induction}
nipkow@55361
   741
\index{induction|(}
nipkow@55361
   742
\index{structural induction|(}
nipkow@47269
   743
nipkow@47269
   744
We illustrate structural induction with an example based on natural numbers:
nipkow@47269
   745
the sum (@{text"\<Sum>"}) of the first @{text n} natural numbers
nipkow@47269
   746
(@{text"{0..n::nat}"}) is equal to \mbox{@{term"n*(n+1) div 2::nat"}}.
nipkow@47269
   747
Never mind the details, just focus on the pattern:
nipkow@47269
   748
*}
nipkow@47269
   749
nipkow@47711
   750
lemma "\<Sum>{0..n::nat} = n*(n+1) div 2"
nipkow@47269
   751
proof (induction n)
nipkow@47269
   752
  show "\<Sum>{0..0::nat} = 0*(0+1) div 2" by simp
nipkow@47269
   753
next
nipkow@47269
   754
  fix n assume "\<Sum>{0..n::nat} = n*(n+1) div 2"
nipkow@47711
   755
  thus "\<Sum>{0..Suc n} = Suc n*(Suc n+1) div 2" by simp
nipkow@47269
   756
qed
nipkow@47269
   757
nipkow@47269
   758
text{* Except for the rewrite steps, everything is explicitly given. This
nipkow@47269
   759
makes the proof easily readable, but the duplication means it is tedious to
nipkow@47269
   760
write and maintain. Here is how pattern
nipkow@47269
   761
matching can completely avoid any duplication: *}
nipkow@47269
   762
nipkow@47269
   763
lemma "\<Sum>{0..n::nat} = n*(n+1) div 2" (is "?P n")
nipkow@47269
   764
proof (induction n)
nipkow@47269
   765
  show "?P 0" by simp
nipkow@47269
   766
next
nipkow@47269
   767
  fix n assume "?P n"
nipkow@47269
   768
  thus "?P(Suc n)" by simp
nipkow@47269
   769
qed
nipkow@47269
   770
nipkow@47269
   771
text{* The first line introduces an abbreviation @{text"?P n"} for the goal.
nipkow@47269
   772
Pattern matching @{text"?P n"} with the goal instantiates @{text"?P"} to the
nipkow@47269
   773
function @{term"\<lambda>n. \<Sum>{0..n::nat} = n*(n+1) div 2"}.  Now the proposition to
nipkow@47269
   774
be proved in the base case can be written as @{text"?P 0"}, the induction
nipkow@47269
   775
hypothesis as @{text"?P n"}, and the conclusion of the induction step as
nipkow@47269
   776
@{text"?P(Suc n)"}.
nipkow@47269
   777
nipkow@47269
   778
Induction also provides the \isacom{case} idiom that abbreviates
nipkow@47269
   779
the \isacom{fix}-\isacom{assume} step. The above proof becomes
nipkow@47269
   780
*}
nipkow@47269
   781
(*<*)lemma "\<Sum>{0..n::nat} = n*(n+1) div 2"(*>*)
nipkow@47269
   782
proof (induction n)
nipkow@47269
   783
  case 0
nipkow@47269
   784
  show ?case by simp
nipkow@47269
   785
next
nipkow@47269
   786
  case (Suc n)
nipkow@47269
   787
  thus ?case by simp
nipkow@47269
   788
qed
nipkow@47269
   789
nipkow@47269
   790
text{*
nipkow@55361
   791
The unknown @{text"?case"}\index{case?@@{text"?case"}|(} is set in each case to the required
nipkow@58504
   792
claim, i.e., @{text"?P 0"} and \mbox{@{text"?P(Suc n)"}} in the above proof,
nipkow@47269
   793
without requiring the user to define a @{text "?P"}. The general
nipkow@47269
   794
pattern for induction over @{typ nat} is shown on the left-hand side:
nipkow@47269
   795
*}text_raw{*
nipkow@47269
   796
\begin{tabular}{@ {}ll@ {}}
nipkow@47269
   797
\begin{minipage}[t]{.4\textwidth}
nipkow@47269
   798
\isa{%
nipkow@47269
   799
*}
nipkow@47269
   800
(*<*)lemma "P(n::nat)" proof -(*>*)
nipkow@47269
   801
show "P(n)"
nipkow@47269
   802
proof (induction n)
nipkow@47269
   803
  case 0
wenzelm@58999
   804
  text_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*}
nipkow@65348
   805
  show ?case (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
nipkow@47269
   806
next
nipkow@47269
   807
  case (Suc n)
wenzelm@58999
   808
  text_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*}
nipkow@65348
   809
  show ?case (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
nipkow@47269
   810
qed(*<*)qed(*>*)
nipkow@47269
   811
nipkow@47269
   812
text_raw {* }
nipkow@47269
   813
\end{minipage}
nipkow@47269
   814
&
nipkow@47269
   815
\begin{minipage}[t]{.4\textwidth}
nipkow@47269
   816
~\\
nipkow@47269
   817
~\\
nipkow@47269
   818
\isacom{let} @{text"?case = \"P(0)\""}\\
nipkow@47269
   819
~\\
nipkow@47269
   820
~\\
nipkow@47269
   821
~\\[1ex]
nipkow@47269
   822
\isacom{fix} @{text n} \isacom{assume} @{text"Suc: \"P(n)\""}\\
nipkow@47269
   823
\isacom{let} @{text"?case = \"P(Suc n)\""}\\
nipkow@47269
   824
\end{minipage}
nipkow@47269
   825
\end{tabular}
nipkow@47269
   826
\medskip
nipkow@47269
   827
*}
nipkow@47269
   828
text{*
nipkow@47269
   829
On the right side you can see what the \isacom{case} command
nipkow@47269
   830
on the left stands for.
nipkow@47269
   831
nipkow@47269
   832
In case the goal is an implication, induction does one more thing: the
nipkow@47269
   833
proposition to be proved in each case is not the whole implication but only
nipkow@47269
   834
its conclusion; the premises of the implication are immediately made
nipkow@47269
   835
assumptions of that case. That is, if in the above proof we replace
nipkow@49837
   836
\isacom{show}~@{text"\"P(n)\""} by
nipkow@49837
   837
\mbox{\isacom{show}~@{text"\"A(n) \<Longrightarrow> P(n)\""}}
nipkow@47269
   838
then \isacom{case}~@{text 0} stands for
nipkow@47269
   839
\begin{quote}
nipkow@47269
   840
\isacom{assume} \ @{text"0: \"A(0)\""}\\
nipkow@47269
   841
\isacom{let} @{text"?case = \"P(0)\""}
nipkow@47269
   842
\end{quote}
nipkow@47269
   843
and \isacom{case}~@{text"(Suc n)"} stands for
nipkow@47269
   844
\begin{quote}
nipkow@47269
   845
\isacom{fix} @{text n}\\
nipkow@47269
   846
\isacom{assume} @{text"Suc:"}
nipkow@47306
   847
  \begin{tabular}[t]{l}@{text"\"A(n) \<Longrightarrow> P(n)\""}\\@{text"\"A(Suc n)\""}\end{tabular}\\
nipkow@47269
   848
\isacom{let} @{text"?case = \"P(Suc n)\""}
nipkow@47269
   849
\end{quote}
nipkow@47269
   850
The list of assumptions @{text Suc} is actually subdivided
nipkow@56989
   851
into @{text"Suc.IH"}, the induction hypotheses (here @{text"A(n) \<Longrightarrow> P(n)"}),
nipkow@47269
   852
and @{text"Suc.prems"}, the premises of the goal being proved
nipkow@47269
   853
(here @{text"A(Suc n)"}).
nipkow@47269
   854
nipkow@47269
   855
Induction works for any datatype.
wenzelm@53015
   856
Proving a goal @{text"\<lbrakk> A\<^sub>1(x); \<dots>; A\<^sub>k(x) \<rbrakk> \<Longrightarrow> P(x)"}
nipkow@47269
   857
by induction on @{text x} generates a proof obligation for each constructor
nipkow@55361
   858
@{text C} of the datatype. The command \isacom{case}~@{text"(C x\<^sub>1 \<dots> x\<^sub>n)"}
nipkow@47269
   859
performs the following steps:
nipkow@47269
   860
\begin{enumerate}
wenzelm@53015
   861
\item \isacom{fix} @{text"x\<^sub>1 \<dots> x\<^sub>n"}
nipkow@55361
   862
\item \isacom{assume} the induction hypotheses (calling them @{text C.IH}\index{IH@@{text".IH"}})
nipkow@55361
   863
 and the premises \mbox{@{text"A\<^sub>i(C x\<^sub>1 \<dots> x\<^sub>n)"}} (calling them @{text"C.prems"}\index{prems@@{text".prems"}})
nipkow@47269
   864
 and calling the whole list @{text C}
wenzelm@53015
   865
\item \isacom{let} @{text"?case = \"P(C x\<^sub>1 \<dots> x\<^sub>n)\""}
nipkow@47269
   866
\end{enumerate}
nipkow@55361
   867
\index{structural induction|)}
nipkow@47269
   868
nipkow@65437
   869
nipkow@65437
   870
\ifsem\else
nipkow@65437
   871
\subsection{Computation Induction}
nipkow@65437
   872
\index{rule induction}
nipkow@65437
   873
nipkow@65437
   874
In \autoref{sec:recursive-funs} we introduced computation induction and
nipkow@65437
   875
its realization in Isabelle: the definition
nipkow@65437
   876
of a recursive function \<open>f\<close> via \isacom{fun} proves the corresponding computation
nipkow@65437
   877
induction rule called \<open>f.induct\<close>. Induction with this rule looks like in
nipkow@65437
   878
\autoref{sec:recursive-funs}, but now with \isacom{proof} instead of \isacom{apply}:
nipkow@65437
   879
\begin{quote}
nipkow@65437
   880
\isacom{proof} (\<open>induction x\<^sub>1 \<dots> x\<^sub>k rule: f.induct\<close>)
nipkow@65437
   881
\end{quote}
nipkow@65437
   882
Just as for structural induction, this creates several cases, one for each
nipkow@65437
   883
defining equation for \<open>f\<close>. By default (if the equations have not been named
nipkow@65437
   884
by the user), the cases are numbered. That is, they are started by
nipkow@65437
   885
\begin{quote}
nipkow@65437
   886
\isacom{case} (\<open>i x y ...\<close>)
nipkow@65437
   887
\end{quote}
nipkow@65437
   888
where \<open>i = 1,...,n\<close>, \<open>n\<close> is the number of equations defining \<open>f\<close>,
nipkow@65437
   889
and \<open>x y ...\<close> are the variables in equation \<open>i\<close>. Note the following:
nipkow@65437
   890
\begin{itemize}
nipkow@65437
   891
\item
nipkow@65437
   892
Although \<open>i\<close> is an Isar name, \<open>i.IH\<close> (or similar) is not. You need
nipkow@65437
   893
double quotes: "\<open>i.IH\<close>". When indexing the name, write "\<open>i.IH\<close>"(1),
nipkow@65437
   894
not "\<open>i.IH\<close>(1)".
nipkow@65437
   895
\item
nipkow@65437
   896
If defining equations for \<open>f\<close> overlap, \isacom{fun} instantiates them to make
nipkow@65437
   897
them nonoverlapping. This means that one user-provided equation may lead to
nipkow@65437
   898
several equations and thus to several cases in the induction rule.
nipkow@65437
   899
These have names of the form "\<open>i_j\<close>", where \<open>i\<close> is the number of the original
nipkow@65437
   900
equation and the system-generated \<open>j\<close> indicates the subcase.
nipkow@65437
   901
\end{itemize}
nipkow@65437
   902
In Isabelle/jEdit, the \<open>induction\<close> proof method displays a proof skeleton
nipkow@65437
   903
with all \isacom{case}s. This is particularly useful for computation induction
nipkow@65437
   904
and the following rule induction.
nipkow@65437
   905
\fi
nipkow@65437
   906
nipkow@65437
   907
nipkow@52361
   908
\subsection{Rule Induction}
nipkow@55361
   909
\index{rule induction|(}
nipkow@47269
   910
nipkow@47269
   911
Recall the inductive and recursive definitions of even numbers in
nipkow@47269
   912
\autoref{sec:inductive-defs}:
nipkow@47269
   913
*}
nipkow@47269
   914
nipkow@47269
   915
inductive ev :: "nat \<Rightarrow> bool" where
nipkow@47269
   916
ev0: "ev 0" |
nipkow@47269
   917
evSS: "ev n \<Longrightarrow> ev(Suc(Suc n))"
nipkow@47269
   918
nipkow@61429
   919
fun evn :: "nat \<Rightarrow> bool" where
nipkow@61429
   920
"evn 0 = True" |
nipkow@61429
   921
"evn (Suc 0) = False" |
nipkow@61429
   922
"evn (Suc(Suc n)) = evn n"
nipkow@47269
   923
nipkow@61429
   924
text{* We recast the proof of @{prop"ev n \<Longrightarrow> evn n"} in Isar. The
nipkow@47269
   925
left column shows the actual proof text, the right column shows
nipkow@47269
   926
the implicit effect of the two \isacom{case} commands:*}text_raw{*
nipkow@47269
   927
\begin{tabular}{@ {}l@ {\qquad}l@ {}}
nipkow@47269
   928
\begin{minipage}[t]{.5\textwidth}
nipkow@47269
   929
\isa{%
nipkow@47269
   930
*}
nipkow@47269
   931
nipkow@61429
   932
lemma "ev n \<Longrightarrow> evn n"
nipkow@47269
   933
proof(induction rule: ev.induct)
nipkow@47269
   934
  case ev0
nipkow@47269
   935
  show ?case by simp
nipkow@47269
   936
next
nipkow@47269
   937
  case evSS
nipkow@47269
   938
nipkow@47269
   939
nipkow@47269
   940
nipkow@47269
   941
  thus ?case by simp
nipkow@47269
   942
qed
nipkow@47269
   943
nipkow@47269
   944
text_raw {* }
nipkow@47269
   945
\end{minipage}
nipkow@47269
   946
&
nipkow@47269
   947
\begin{minipage}[t]{.5\textwidth}
nipkow@47269
   948
~\\
nipkow@47269
   949
~\\
nipkow@61429
   950
\isacom{let} @{text"?case = \"evn 0\""}\\
nipkow@47269
   951
~\\
nipkow@47269
   952
~\\
nipkow@47269
   953
\isacom{fix} @{text n}\\
nipkow@47269
   954
\isacom{assume} @{text"evSS:"}
nipkow@61429
   955
  \begin{tabular}[t]{l} @{text"\"ev n\""}\\@{text"\"evn n\""}\end{tabular}\\
nipkow@61429
   956
\isacom{let} @{text"?case = \"evn(Suc(Suc n))\""}\\
nipkow@47269
   957
\end{minipage}
nipkow@47269
   958
\end{tabular}
nipkow@47269
   959
\medskip
nipkow@47269
   960
*}
nipkow@47269
   961
text{*
nipkow@47269
   962
The proof resembles structural induction, but the induction rule is given
nipkow@47269
   963
explicitly and the names of the cases are the names of the rules in the
nipkow@47269
   964
inductive definition.
nipkow@47269
   965
Let us examine the two assumptions named @{thm[source]evSS}:
nipkow@47269
   966
@{prop "ev n"} is the premise of rule @{thm[source]evSS}, which we may assume
nipkow@61429
   967
because we are in the case where that rule was used; @{prop"evn n"}
nipkow@47269
   968
is the induction hypothesis.
nipkow@47269
   969
\begin{warn}
nipkow@47269
   970
Because each \isacom{case} command introduces a list of assumptions
nipkow@47269
   971
named like the case name, which is the name of a rule of the inductive
nipkow@47269
   972
definition, those rules now need to be accessed with a qualified name, here
nipkow@58522
   973
@{thm[source] ev.ev0} and @{thm[source] ev.evSS}.
nipkow@47269
   974
\end{warn}
nipkow@47269
   975
nipkow@47269
   976
In the case @{thm[source]evSS} of the proof above we have pretended that the
nipkow@47269
   977
system fixes a variable @{text n}.  But unless the user provides the name
nipkow@47269
   978
@{text n}, the system will just invent its own name that cannot be referred
nipkow@47269
   979
to.  In the above proof, we do not need to refer to it, hence we do not give
nipkow@47269
   980
it a specific name. In case one needs to refer to it one writes
nipkow@47269
   981
\begin{quote}
nipkow@47269
   982
\isacom{case} @{text"(evSS m)"}
nipkow@47269
   983
\end{quote}
nipkow@58605
   984
like \isacom{case}~@{text"(Suc n)"} in earlier structural inductions.
nipkow@47269
   985
The name @{text m} is an arbitrary choice. As a result,
nipkow@47269
   986
case @{thm[source] evSS} is derived from a renamed version of
nipkow@47269
   987
rule @{thm[source] evSS}: @{text"ev m \<Longrightarrow> ev(Suc(Suc m))"}.
nipkow@47269
   988
Here is an example with a (contrived) intermediate step that refers to @{text m}:
nipkow@47269
   989
*}
nipkow@47269
   990
nipkow@61429
   991
lemma "ev n \<Longrightarrow> evn n"
nipkow@47269
   992
proof(induction rule: ev.induct)
nipkow@47269
   993
  case ev0 show ?case by simp
nipkow@47269
   994
next
nipkow@47269
   995
  case (evSS m)
nipkow@61429
   996
  have "evn(Suc(Suc m)) = evn m" by simp
nipkow@61429
   997
  thus ?case using `evn m` by blast
nipkow@47269
   998
qed
nipkow@47269
   999
nipkow@47269
  1000
text{*
nipkow@47269
  1001
\indent
nipkow@47269
  1002
In general, let @{text I} be a (for simplicity unary) inductively defined
nipkow@47269
  1003
predicate and let the rules in the definition of @{text I}
wenzelm@53015
  1004
be called @{text "rule\<^sub>1"}, \dots, @{text "rule\<^sub>n"}. A proof by rule
nipkow@55361
  1005
induction follows this pattern:\index{inductionrule@@{text"induction ... rule:"}}
nipkow@47269
  1006
*}
nipkow@47269
  1007
nipkow@47269
  1008
(*<*)
wenzelm@53015
  1009
inductive I where rule\<^sub>1: "I()" |  rule\<^sub>2: "I()" |  rule\<^sub>n: "I()"
nipkow@47269
  1010
lemma "I x \<Longrightarrow> P x" proof-(*>*)
nipkow@47269
  1011
show "I x \<Longrightarrow> P x"
nipkow@47269
  1012
proof(induction rule: I.induct)
wenzelm@53015
  1013
  case rule\<^sub>1
wenzelm@58999
  1014
  text_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
nipkow@65348
  1015
  show ?case (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
  1016
next
wenzelm@58999
  1017
  text_raw{*\\[-.4ex]$\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
nipkow@47269
  1018
(*<*)
wenzelm@53015
  1019
  case rule\<^sub>2
nipkow@47269
  1020
  show ?case sorry
nipkow@47269
  1021
(*>*)
nipkow@47269
  1022
next
wenzelm@53015
  1023
  case rule\<^sub>n
wenzelm@58999
  1024
  text_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
nipkow@65348
  1025
  show ?case (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
nipkow@47269
  1026
qed(*<*)qed(*>*)
nipkow@47269
  1027
nipkow@47269
  1028
text{*
nipkow@47269
  1029
One can provide explicit variable names by writing
wenzelm@53015
  1030
\isacom{case}~@{text"(rule\<^sub>i x\<^sub>1 \<dots> x\<^sub>k)"}, thus renaming the first @{text k}
wenzelm@53015
  1031
free variables in rule @{text i} to @{text"x\<^sub>1 \<dots> x\<^sub>k"},
nipkow@47269
  1032
going through rule @{text i} from left to right.
nipkow@47269
  1033
nipkow@52361
  1034
\subsection{Assumption Naming}
nipkow@51443
  1035
\label{sec:assm-naming}
nipkow@47269
  1036
nipkow@47269
  1037
In any induction, \isacom{case}~@{text name} sets up a list of assumptions
nipkow@47269
  1038
also called @{text name}, which is subdivided into three parts:
nipkow@47269
  1039
\begin{description}
nipkow@55361
  1040
\item[@{text name.IH}]\index{IH@@{text".IH"}} contains the induction hypotheses.
nipkow@55361
  1041
\item[@{text name.hyps}]\index{hyps@@{text".hyps"}} contains all the other hypotheses of this case in the
nipkow@47269
  1042
induction rule. For rule inductions these are the hypotheses of rule
nipkow@47269
  1043
@{text name}, for structural inductions these are empty.
nipkow@55361
  1044
\item[@{text name.prems}]\index{prems@@{text".prems"}} contains the (suitably instantiated) premises
nipkow@58504
  1045
of the statement being proved, i.e., the @{text A\<^sub>i} when
wenzelm@53015
  1046
proving @{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"}.
nipkow@47269
  1047
\end{description}
nipkow@47269
  1048
\begin{warn}
nipkow@47269
  1049
Proof method @{text induct} differs from @{text induction}
nipkow@47269
  1050
only in this naming policy: @{text induct} does not distinguish
nipkow@47269
  1051
@{text IH} from @{text hyps} but subsumes @{text IH} under @{text hyps}.
nipkow@47269
  1052
\end{warn}
nipkow@47269
  1053
nipkow@47269
  1054
More complicated inductive proofs than the ones we have seen so far
nipkow@58602
  1055
often need to refer to specific assumptions --- just @{text name} or even
nipkow@47269
  1056
@{text name.prems} and @{text name.IH} can be too unspecific.
nipkow@58504
  1057
This is where the indexing of fact lists comes in handy, e.g.,
nipkow@47269
  1058
@{text"name.IH(2)"} or @{text"name.prems(1-2)"}.
nipkow@47269
  1059
nipkow@52361
  1060
\subsection{Rule Inversion}
nipkow@52361
  1061
\label{sec:rule-inversion}
nipkow@55361
  1062
\index{rule inversion|(}
nipkow@47269
  1063
nipkow@47711
  1064
Rule inversion is case analysis of which rule could have been used to
nipkow@55361
  1065
derive some fact. The name \conceptnoidx{rule inversion} emphasizes that we are
nipkow@47269
  1066
reasoning backwards: by which rules could some given fact have been proved?
nipkow@47269
  1067
For the inductive definition of @{const ev}, rule inversion can be summarized
nipkow@47269
  1068
like this:
nipkow@47269
  1069
@{prop[display]"ev n \<Longrightarrow> n = 0 \<or> (EX k. n = Suc(Suc k) \<and> ev k)"}
nipkow@47711
  1070
The realisation in Isabelle is a case analysis.
nipkow@47269
  1071
A simple example is the proof that @{prop"ev n \<Longrightarrow> ev (n - 2)"}. We
nipkow@47269
  1072
already went through the details informally in \autoref{sec:Logic:even}. This
nipkow@47269
  1073
is the Isar proof:
nipkow@47269
  1074
*}
nipkow@47269
  1075
(*<*)
nipkow@47269
  1076
notepad
nipkow@47269
  1077
begin fix n
nipkow@47269
  1078
(*>*)
nipkow@47269
  1079
  assume "ev n"
nipkow@47269
  1080
  from this have "ev(n - 2)"
nipkow@47269
  1081
  proof cases
nipkow@47269
  1082
    case ev0 thus "ev(n - 2)" by (simp add: ev.ev0)
nipkow@47269
  1083
  next
nipkow@47269
  1084
    case (evSS k) thus "ev(n - 2)" by (simp add: ev.evSS)
nipkow@47269
  1085
  qed
nipkow@47269
  1086
(*<*)
nipkow@47269
  1087
end
nipkow@47269
  1088
(*>*)
nipkow@47269
  1089
nipkow@47711
  1090
text{* The key point here is that a case analysis over some inductively
nipkow@47269
  1091
defined predicate is triggered by piping the given fact
nipkow@47269
  1092
(here: \isacom{from}~@{text this}) into a proof by @{text cases}.
nipkow@47269
  1093
Let us examine the assumptions available in each case. In case @{text ev0}
nipkow@47269
  1094
we have @{text"n = 0"} and in case @{text evSS} we have @{prop"n = Suc(Suc k)"}
nipkow@47269
  1095
and @{prop"ev k"}. In each case the assumptions are available under the name
nipkow@56989
  1096
of the case; there is no fine-grained naming schema like there is for induction.
nipkow@47269
  1097
nipkow@47704
  1098
Sometimes some rules could not have been used to derive the given fact
nipkow@47269
  1099
because constructors clash. As an extreme example consider
nipkow@47269
  1100
rule inversion applied to @{prop"ev(Suc 0)"}: neither rule @{text ev0} nor
nipkow@47269
  1101
rule @{text evSS} can yield @{prop"ev(Suc 0)"} because @{text"Suc 0"} unifies
nipkow@47269
  1102
neither with @{text 0} nor with @{term"Suc(Suc n)"}. Impossible cases do not
nipkow@47269
  1103
have to be proved. Hence we can prove anything from @{prop"ev(Suc 0)"}:
nipkow@47269
  1104
*}
nipkow@47269
  1105
(*<*)
nipkow@47269
  1106
notepad begin fix P
nipkow@47269
  1107
(*>*)
nipkow@47269
  1108
  assume "ev(Suc 0)" then have P by cases
nipkow@47269
  1109
(*<*)
nipkow@47269
  1110
end
nipkow@47269
  1111
(*>*)
nipkow@47269
  1112
nipkow@47269
  1113
text{* That is, @{prop"ev(Suc 0)"} is simply not provable: *}
nipkow@47269
  1114
nipkow@47269
  1115
lemma "\<not> ev(Suc 0)"
nipkow@47269
  1116
proof
nipkow@47269
  1117
  assume "ev(Suc 0)" then show False by cases
nipkow@47269
  1118
qed
nipkow@47269
  1119
nipkow@47269
  1120
text{* Normally not all cases will be impossible. As a simple exercise,
nipkow@47269
  1121
prove that \mbox{@{prop"\<not> ev(Suc(Suc(Suc 0)))"}.}
nipkow@51443
  1122
nipkow@52361
  1123
\subsection{Advanced Rule Induction}
nipkow@51445
  1124
\label{sec:advanced-rule-induction}
nipkow@51443
  1125
nipkow@51443
  1126
So far, rule induction was always applied to goals of the form @{text"I x y z \<Longrightarrow> \<dots>"}
nipkow@51443
  1127
where @{text I} is some inductively defined predicate and @{text x}, @{text y}, @{text z}
nipkow@51443
  1128
are variables. In some rare situations one needs to deal with an assumption where
nipkow@51443
  1129
not all arguments @{text r}, @{text s}, @{text t} are variables:
nipkow@51443
  1130
\begin{isabelle}
nipkow@61517
  1131
\isacom{lemma} @{text"\"I r s t \<Longrightarrow> \<dots>\""}
nipkow@51443
  1132
\end{isabelle}
nipkow@51443
  1133
Applying the standard form of
nipkow@54577
  1134
rule induction in such a situation will lead to strange and typically unprovable goals.
nipkow@51443
  1135
We can easily reduce this situation to the standard one by introducing
nipkow@51443
  1136
new variables @{text x}, @{text y}, @{text z} and reformulating the goal like this:
nipkow@51443
  1137
\begin{isabelle}
nipkow@61517
  1138
\isacom{lemma} @{text"\"I x y z \<Longrightarrow> x = r \<Longrightarrow> y = s \<Longrightarrow> z = t \<Longrightarrow> \<dots>\""}
nipkow@51443
  1139
\end{isabelle}
nipkow@56989
  1140
Standard rule induction will work fine now, provided the free variables in
nipkow@58502
  1141
@{text r}, @{text s}, @{text t} are generalized via @{text"arbitrary"}.
nipkow@51443
  1142
nipkow@51443
  1143
However, induction can do the above transformation for us, behind the curtains, so we never
nipkow@51443
  1144
need to see the expanded version of the lemma. This is what we need to write:
nipkow@51443
  1145
\begin{isabelle}
nipkow@61517
  1146
\isacom{lemma} @{text"\"I r s t \<Longrightarrow> \<dots>\""}\isanewline
nipkow@55361
  1147
\isacom{proof}@{text"(induction \"r\" \"s\" \"t\" arbitrary: \<dots> rule: I.induct)"}\index{inductionrule@@{text"induction ... rule:"}}\index{arbitrary@@{text"arbitrary:"}}
nipkow@51443
  1148
\end{isabelle}
nipkow@58605
  1149
Like for rule inversion, cases that are impossible because of constructor clashes
nipkow@51443
  1150
will not show up at all. Here is a concrete example: *}
nipkow@51443
  1151
nipkow@51443
  1152
lemma "ev (Suc m) \<Longrightarrow> \<not> ev m"
nipkow@51443
  1153
proof(induction "Suc m" arbitrary: m rule: ev.induct)
nipkow@51443
  1154
  fix n assume IH: "\<And>m. n = Suc m \<Longrightarrow> \<not> ev m"
nipkow@51443
  1155
  show "\<not> ev (Suc n)"
nipkow@54577
  1156
  proof --"contradiction"
nipkow@51443
  1157
    assume "ev(Suc n)"
nipkow@51443
  1158
    thus False
nipkow@51443
  1159
    proof cases --"rule inversion"
nipkow@51443
  1160
      fix k assume "n = Suc k" "ev k"
nipkow@51443
  1161
      thus False using IH by auto
nipkow@51443
  1162
    qed
nipkow@51443
  1163
  qed
nipkow@51443
  1164
qed
nipkow@51443
  1165
nipkow@51443
  1166
text{*
nipkow@51443
  1167
Remarks:
nipkow@51443
  1168
\begin{itemize}
nipkow@51443
  1169
\item 
nipkow@51443
  1170
Instead of the \isacom{case} and @{text ?case} magic we have spelled all formulas out.
nipkow@51443
  1171
This is merely for greater clarity.
nipkow@51443
  1172
\item
nipkow@51443
  1173
We only need to deal with one case because the @{thm[source] ev0} case is impossible.
nipkow@51443
  1174
\item
nipkow@51443
  1175
The form of the @{text IH} shows us that internally the lemma was expanded as explained
nipkow@51443
  1176
above: \noquotes{@{prop[source]"ev x \<Longrightarrow> x = Suc m \<Longrightarrow> \<not> ev m"}}.
nipkow@51443
  1177
\item
nipkow@61013
  1178
The goal @{prop"\<not> ev (Suc n)"} may surprise. The expanded version of the lemma
nipkow@51443
  1179
would suggest that we have a \isacom{fix} @{text m} \isacom{assume} @{prop"Suc(Suc n) = Suc m"}
nipkow@51443
  1180
and need to show @{prop"\<not> ev m"}. What happened is that Isabelle immediately
nipkow@51443
  1181
simplified @{prop"Suc(Suc n) = Suc m"} to @{prop"Suc n = m"} and could then eliminate
nipkow@51443
  1182
@{text m}. Beware of such nice surprises with this advanced form of induction.
nipkow@51443
  1183
\end{itemize}
nipkow@51443
  1184
\begin{warn}
nipkow@51443
  1185
This advanced form of induction does not support the @{text IH}
nipkow@51443
  1186
naming schema explained in \autoref{sec:assm-naming}:
nipkow@56989
  1187
the induction hypotheses are instead found under the name @{text hyps},
nipkow@56989
  1188
as they are for the simpler
nipkow@51443
  1189
@{text induct} method.
nipkow@51443
  1190
\end{warn}
nipkow@55361
  1191
\index{induction|)}
nipkow@55361
  1192
\index{cases@@{text"cases"}|)}
nipkow@55361
  1193
\index{case@\isacom{case}|)}
nipkow@55361
  1194
\index{case?@@{text"?case"}|)}
nipkow@55361
  1195
\index{rule induction|)}
nipkow@55361
  1196
\index{rule inversion|)}
nipkow@54218
  1197
nipkow@54436
  1198
\subsection*{Exercises}
nipkow@52593
  1199
nipkow@54232
  1200
nipkow@54232
  1201
\exercise
nipkow@54292
  1202
Give a structured proof by rule inversion:
nipkow@54232
  1203
*}
nipkow@54232
  1204
nipkow@54232
  1205
lemma assumes a: "ev(Suc(Suc n))" shows "ev n"
nipkow@54232
  1206
(*<*)oops(*>*)
nipkow@54232
  1207
nipkow@54232
  1208
text{*
nipkow@54232
  1209
\endexercise
nipkow@54232
  1210
nipkow@52593
  1211
\begin{exercise}
nipkow@54232
  1212
Give a structured proof of @{prop "\<not> ev(Suc(Suc(Suc 0)))"}
nipkow@54232
  1213
by rule inversions. If there are no cases to be proved you can close
nipkow@61013
  1214
a proof immediately with \isacom{qed}.
nipkow@54218
  1215
\end{exercise}
nipkow@54218
  1216
nipkow@54218
  1217
\begin{exercise}
nipkow@54292
  1218
Recall predicate @{text star} from \autoref{sec:star} and @{text iter}
nipkow@54292
  1219
from Exercise~\ref{exe:iter}. Prove @{prop "iter r n x y \<Longrightarrow> star r x y"}
nipkow@56989
  1220
in a structured style; do not just sledgehammer each case of the
nipkow@54292
  1221
required induction.
nipkow@54292
  1222
\end{exercise}
nipkow@54292
  1223
nipkow@54292
  1224
\begin{exercise}
nipkow@52593
  1225
Define a recursive function @{text "elems ::"} @{typ"'a list \<Rightarrow> 'a set"}
nipkow@52593
  1226
and prove @{prop "x : elems xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> elems ys"}.
nipkow@52593
  1227
\end{exercise}
nipkow@61012
  1228
nipkow@61012
  1229
\begin{exercise}
nipkow@61012
  1230
Extend Exercise~\ref{exe:cfg} with a function that checks if some
nipkow@61012
  1231
\mbox{@{text "alpha list"}} is a balanced
nipkow@61022
  1232
string of parentheses. More precisely, define a \mbox{recursive} function
nipkow@61012
  1233
@{text "balanced :: nat \<Rightarrow> alpha list \<Rightarrow> bool"} such that @{term"balanced n w"}
nipkow@61022
  1234
is true iff (informally) @{text"S (a\<^sup>n @ w)"}. Formally, prove that
nipkow@61022
  1235
@{prop "balanced n w \<longleftrightarrow> S (replicate n a @ w)"} where
nipkow@61012
  1236
@{const replicate} @{text"::"} @{typ"nat \<Rightarrow> 'a \<Rightarrow> 'a list"} is predefined
nipkow@61012
  1237
and @{term"replicate n x"} yields the list @{text"[x, \<dots>, x]"} of length @{text n}.
nipkow@61012
  1238
\end{exercise}
nipkow@47269
  1239
*}
nipkow@47269
  1240
nipkow@47269
  1241
(*<*)
nipkow@47269
  1242
end
nipkow@47269
  1243
(*>*)