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 (*>*)