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