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