(*<*)
theory Isar
imports LaTeXsugar
begin
declare [[quick_and_dirty]]
(*>*)
text‹
 -scripts are unreadable and hard to maintain. The language of choice
  larger proofs is \concept{Isar}. The two key features of Isar are:
 begin{itemize}
 item It is structured, not linear.
 item It is readable without its being run because
  need to state what you are proving at any given point.
 end{itemize}
  apply-scripts are like assembly language programs, Isar proofs
  like structured programs with comments. A typical Isar proof looks like this:
 ›text‹
 begin{tabular}{@ {}l}
 isacom{proof}\\
 quad\isacom{assume} ‹"›$\mathit{formula}_0$‹"›\\
 quad\isacom{have} ‹"›$\mathit{formula}_1$‹"› \quad\isacom{by} ‹simp›\\
 quad\vdots\\
 quad\isacom{have} ‹"›$\mathit{formula}_n$‹"› \quad\isacom{by} ‹blast›\\
 quad\isacom{show} ‹"›$\mathit{formula}_{n+1}$‹"› \quad\isacom{by} ‹…›\\
 isacom{qed}
 end{tabular}
 ›text‹
  proves $\mathit{formula}_0 \Longrightarrow \mathit{formula}_{n+1}$
 provided each proof step succeeds).
  intermediate \isacom{have} statements are merely stepping stones
  the way towards the \isacom{show} statement that proves the actual
 . In more detail, this is the Isar core syntax:
 medskip

 begin{tabular}{@ {}lcl@ {}}
 textit{proof} &=& \indexed{\isacom{by}}{by} \textit{method}\\
 &$\mid$& \indexed{\isacom{proof}}{proof} [\textit{method}] \ \textit{step}$^*$ \ \indexed{\isacom{qed}}{qed}
 end{tabular}
 medskip

 begin{tabular}{@ {}lcl@ {}}
 textit{step} &=& \indexed{\isacom{fix}}{fix} \textit{variables} \\
 &$\mid$& \indexed{\isacom{assume}}{assume} \textit{proposition} \\
 &$\mid$& [\indexed{\isacom{from}}{from} \textit{fact}$^+$] (\indexed{\isacom{have}}{have} $\mid$ \indexed{\isacom{show}}{show}) \ \textit{proposition} \ \textit{proof}
 end{tabular}
 medskip

 begin{tabular}{@ {}lcl@ {}}
 textit{proposition} &=& [\textit{name}:] ‹"›\textit{formula}‹"›
 end{tabular}
 medskip

 begin{tabular}{@ {}lcl@ {}}
 textit{fact} &=& \textit{name} \ $\mid$ \ \dots
 end{tabular}
 medskip

 noindent A proof can either be an atomic \isacom{by} with a single proof
  which must finish off the statement being proved, for example ‹auto›, or it can be a \isacom{proof}--\isacom{qed} block of multiple
 . Such a block can optionally begin with a proof method that indicates
  to start off the proof, e.g., \mbox{‹(induction xs)›}.

  step either assumes a proposition or states a proposition
  with its proof. The optional \isacom{from} clause
  which facts are to be used in the proof.
  propositions are stated with \isacom{have}, the overall goal
  stated with \isacom{show}. A step can also introduce new local variables with
 isacom{fix}. Logically, \isacom{fix} introduces ‹∧›-quantified
 , \isacom{assume} introduces the assumption of an implication
 ‹==>›) and \isacom{have}/\isacom{show} introduce the conclusion.

  are optionally named formulas. These names can be referred to in
  \isacom{from} clauses. In the simplest case, a fact is such a name.
  facts can also be composed with ‹OF› and ‹of› as shown in
 autoref{sec:forward-proof} --- hence the \dots\ in the above grammar. Note
  assumptions, intermediate \isacom{have} statements and global lemmas all
  the same status and are thus collectively referred to as
 conceptidx{facts}{fact}.

  names can stand for whole lists of facts. For example, if ‹f› is
  by command \isacom{fun}, ‹f.simps› refers to the whole list of
  equations defining ‹f›. Individual facts can be selected by
  ‹f.simps(2)›, whole sublists by writing ‹f.simps(2-4)›.


 section{Isar by Example}

  show a number of proofs of Cantor's theorem that a function from a set to
  powerset cannot be surjective, illustrating various features of Isar. The
  const‹surj› is predefined.
 ›

lemma "¬ surj(f :: 'a → 'a set)"
proof
  assume 0: "surj f"
  from 0 have 1: "∀A. ∃a. A = f a" by(simp add: surj_def)
  from 1 have 2: "∃a. {x. x ∉ f x} = f a" by blast
  from 2 show "False" by blast
qed

text‹
  \isacom{proof} command lacks an explicit method by which to perform
  proof. In such cases Isabelle tries to use some standard introduction
 , in the above case for ‹¬›:
 [
 inferrule{
 mbox{@{thm (prem 1) notI}}}
 \mbox{@{thm (concl) notI}}}
 ]
  order to prove prop‹~ P›, assume ‹P› and show ‹False›.
  we may assume \mbox{\noquotes{@{prop [source] "surj f"}}}. The proof shows that names of propositions
  be (single!) digits --- meaningful names are hard to invent and are often
  necessary. Both \isacom{have} steps are obvious. The second one introduces
  diagonal set term‹{x. x ∉ f x}›, the key idea in the proof.
  you wonder why ‹2› directly implies ‹False›: from ‹2›
  follows that prop‹a ∉ f a ⟷ a ∈ f a›.

 subsection{\indexed{‹this›}{this}, \indexed{\isacom{then}}{then}, \indexed{\isacom{with}}{with}, \indexed{\isacom{hence}}{hence}, \indexed{\isacom{thus}}{thus}, \indexed{\isacom{using}}{using}}

  should be avoided. They interrupt the flow of the reader who has to
  the context for the point where the label was introduced. Ideally, the
  is a linear flow, where the output of one step becomes the input of the
  step, piping the previously proved fact into the next proof, like
  a UNIX pipe. In such cases the predefined name ‹this› can be used
  refer to the proposition proved in the previous step. This allows us to
  all labels from our proof (we suppress the \isacom{lemma} statement):
 ›
(*<*)
lemma "¬ surj(f :: 'a → 'a set)"
(*>*)
proof
  assume "surj f"
  from this have "∃a. {x. x ∉ f x} = f a" by(auto simp: surj_def)
  from this show "False" by blast
qed

text‹We have also taken the opportunity to compress the two \isacom{have}
  into one.

  compact the text further, Isar has a few convenient abbreviations:
 medskip

 begin{tabular}{r@ {\quad=\quad}l}
 isacom{then} & \isacom{from} ‹this›\\
 isacom{thus} & \isacom{then} \isacom{show}\\
 isacom{hence} & \isacom{then} \isacom{have}
 end{tabular}
 medskip

 noindent
  the help of these abbreviations the proof becomes
 ›
(*<*)
lemma "¬ surj(f :: 'a → 'a set)"
(*>*)
proof
  assume "surj f"
  hence "∃a. {x. x ∉ f x} = f a" by(auto simp: surj_def)
  thus "False" by blast
qed
text‹

  are two further linguistic variations:
 medskip

 begin{tabular}{r@ {\quad=\quad}l}
 \isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \indexed{\isacom{using}}{using} \ \textit{facts}
 
 isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\
 indexed{\isacom{with}}{with} \ \textit{facts} & \isacom{from} \ \textit{facts} \isa{this}
 end{tabular}
 medskip

 noindent The \isacom{using} idiom de-emphasizes the used facts by moving them
  the proposition.

 subsection{Structured Lemma Statements: \indexed{\isacom{fixes}}{fixes}, \indexed{\isacom{assumes}}{assumes}, \indexed{\isacom{shows}}{shows}}
 index{lemma@\isacom{lemma}}
  can also be stated in a more structured fashion. To demonstrate this
  with Cantor's theorem, we rephrase \noquotes{@{prop[source]"¬ surj f"}}
  little:
 ›

lemma
  fixes f :: "'a → 'a set"
  assumes s: "surj f"
  shows "False"

txt‹The optional \isacom{fixes} part allows you to state the types of
  up front rather than by decorating one of their occurrences in the
  with a type constraint. The key advantage of the structured format is
  \isacom{assumes} part that allows you to name each assumption; multiple
  can be separated by \isacom{and}. The
 isacom{shows} part gives the goal. The actual theorem that will come out of
  proof is \noquotes{@{prop[source]"surj f ==> False"}}, but during the proof the assumption
 noquotes{@{prop[source]"surj f"}} is available under the name ‹s› like any other fact.
 ›

proof -
  have "∃ a. {x. x ∉ f x} = f a" using s by(auto simp: surj_def)
  thus "False" by blast
qed

text‹
 begin{warn}
  the hyphen after the \isacom{proof} command.
  is the null method that does nothing to the goal. Leaving it out would be asking
  to try some suitable introduction rule on the goal const‹False› --- but
  is no such rule and \isacom{proof} would fail.
 end{warn}
  the \isacom{have} step the assumption \noquotes{@{prop[source]"surj f"}} is now
  by its name ‹s›. The duplication of \noquotes{@{prop[source]"surj f"}} in the
  proofs (once in the statement of the lemma, once in its proof) has been
 .

  a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the
  \indexed{‹assms›}{assms} that stands for the list of all assumptions. You can refer
  individual assumptions by ‹assms(1)›, ‹assms(2)›, etc.,
  obviating the need to name them individually.

 section{Proof Patterns}

  show a number of important basic proof patterns. Many of them arise from
  rules of natural deduction that are applied by \isacom{proof} by
 . The patterns are phrased in terms of \isacom{show} but work for
 isacom{have} and \isacom{lemma}, too.

 ifsem\else
 subsection{Logic}
 fi

  start with two forms of \concept{case analysis}:
  from a formula ‹P› we have the two cases ‹P› and
 prop‹~P›, and starting from a fact prop‹P ∨ Q›
  have the two cases ‹P› and ‹Q›:
 ›text_raw‹
 begin{tabular}{@ {}ll@ {}}
 begin{minipage}[t]{.4\textwidth}
 isa{%
 ›
(*<*)lemma "R" proof-(*>*)
show "R"
proof cases
  assume "P"
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "R" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
next
  assume "¬ P"
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "R" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
qed(*<*)oops(*>*)
text_raw ‹}
 end{minipage}\index{cases@‹cases›}
 
 begin{minipage}[t]{.4\textwidth}
 isa{%
 ›
(*<*)lemma "R" proof-(*>*)
have "P ∨ Q" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
then show "R"
proof
  assume "P"
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "R" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
next
  assume "Q"
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "R" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
qed(*<*)oops(*>*)

text_raw ‹}
 end{minipage}
 end{tabular}
 medskip
 begin{isamarkuptext}%
  to prove a logical equivalence:
 end{isamarkuptext}%
 isa{%
 ›
(*<*)lemma "P\<longleftrightarrow>Q" proof-(*>*)
show "P ⟷ Q"
proof
  assume "P"
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "Q" (*<*)sorry(*>*) text_raw\<open>\ \isasymproof\\\<close>
next
  assume "Q"
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "P" (*<*)sorry(*>*) text_raw\<open>\ \isasymproof\\\<close>
qed(*<*)qed(*>*)
text_raw ‹}
 medskip
 begin{isamarkuptext}%
  by contradiction (@{thm[source] ccontr} stands for ``classical contradiction''):
 end{isamarkuptext}%
 begin{tabular}{@ {}ll@ {}}
 begin{minipage}[t]{.4\textwidth}
 isa{%
 ›
(*<*)lemma "\<not> P" proof-(*>*)
show "¬ P"
proof
  assume "P"
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "False" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
qed(*<*)oops(*>*)

text_raw ‹}
 end{minipage}
 
 begin{minipage}[t]{.4\textwidth}
 isa{%
 ›
(*<*)lemma "P" proof-(*>*)
show "P"
proof (rule ccontr)
  assume "¬P"
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "False" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
qed(*<*)oops(*>*)

text_raw ‹}
 end{minipage}
 end{tabular}
 medskip
 begin{isamarkuptext}%
  to prove quantified formulas:
 end{isamarkuptext}%
 begin{tabular}{@ {}ll@ {}}
 begin{minipage}[t]{.4\textwidth}
 isa{%
 ›
(*<*)lemma "\<forall>x. P x" proof-(*>*)
show "∀x. P(x)"
proof
  fix x
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "P(x)" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
qed(*<*)oops(*>*)

text_raw ‹}
 end{minipage}
 
 begin{minipage}[t]{.4\textwidth}
 isa{%
 ›
(*<*)lemma "\<exists>x. P(x)" proof-(*>*)
show "∃x. P(x)"
proof
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "P(witness)" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
qed
(*<*)oops(*>*)

text_raw ‹}
 end{minipage}
 end{tabular}
 medskip
 begin{isamarkuptext}%
  the proof of \noquotes{@{prop[source]"∀x. P(x)"}},
  step \indexed{\isacom{fix}}{fix}~‹x› introduces a locally fixed variable ‹x›
  the subproof, the proverbial ``arbitrary but fixed value''.
  of ‹x› we could have chosen any name in the subproof.
  the proof of \noquotes{@{prop[source]"∃x. P(x)"}},
 ‹witness› is some arbitrary
  for which we can prove that it satisfies ‹P›.

  to reason forward from \noquotes{@{prop[source] "∃x. P(x)"}}:
 end{isamarkuptext}%
 ›
(*<*)lemma True proof- assume 1: "\<exists>x. P x"(*>*)
have "∃x. P(x)" (*<*)by(rule 1)(*>*)text_raw\<open>\ \isasymproof\\\<close>
then obtain x where p: "P(x)" by blast
(*<*)oops(*>*)
text‹
  the \indexed{\isacom{obtain}}{obtain} step, ‹x› (we could have chosen any name)
  a fixed local
 , and ‹p› is the name of the fact
 noquotes{@{prop[source] "P(x)"}}.
  pattern works for one or more ‹x›.
  an example of the \isacom{obtain} command, here is the proof of
 's theorem in more detail:
 ›

lemma "¬ surj(f :: 'a → 'a set)"
proof
  assume "surj f"
  hence  "∃a. {x. x ∉ f x} = f a" by(auto simp: surj_def)
  then obtain a where  "{x. x ∉ f x} = f a"  by blast
  hence  "a ∉ f a ⟷ a ∈ f a"  by blast
  thus "False" by blast
qed

text_raw‹
 begin{isamarkuptext}%

 , how to prove set equality and subset relationship:
 end{isamarkuptext}%
 begin{tabular}{@ {}ll@ {}}
 begin{minipage}[t]{.4\textwidth}
 isa{%
 ›
(*<*)lemma "A = (B::'a set)" proof-(*>*)
show "A = B"
proof
  show "A ⊆ B" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
next
  show "B ⊆ A" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
qed(*<*)qed(*>*)

text_raw ‹}
 end{minipage}
 
 begin{minipage}[t]{.4\textwidth}
 isa{%
 ›
(*<*)lemma "A <= (B::'a set)" proof-(*>*)
show "A ⊆ B"
proof
  fix x
  assume "x ∈ A"
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "x ∈ B" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
qed(*<*)qed(*>*)

text_raw ‹}
 end{minipage}
 end{tabular}
 begin{isamarkuptext}%

 ifsem\else
 subsection{Chains of (In)Equations}

  textbooks, chains of equations (and inequations) are often displayed like this:
 begin{quote}
 begin{tabular}{@ {}l@ {\qquad}l@ {}}
 t_1 = t_2$ & \isamath{\,\langle\mathit{justification}\rangle}\\
 \phantom{t_1} = t_3$ & \isamath{\,\langle\mathit{justification}\rangle}\\
 quad $\vdots$\\
 \phantom{t_1} = t_n$ & \isamath{\,\langle\mathit{justification}\rangle}
 end{tabular}
 end{quote}
  Isar equivalent is this:

 begin{samepage}
 begin{quote}
 isacom{have} ‹"t₁ = t₂"› \isasymproof\\
 isacom{also have} ‹"... = t₃"› \isasymproof\\
 quad $\vdots$\\
 isacom{also have} ‹"... = t_n"› \isasymproof \\
 isacom{finally show} ‹"t₁ = t_n"›\ \texttt{.}
 end{quote}
 end{samepage}

 noindent
  ``‹...›'' and ``‹.›'' deserve some explanation:
 begin{description}
 item[``‹...›''] is literally three dots. It is the name of an unknown that Isar
  instantiates with the right-hand side of the previous equation.
  general, if ‹this› is the theorem term‹p t<sub>1</sub> t<sub>2</sub>› then ``‹...›''
  for ‹t₂›.
 item[``‹.›''] (a single dot) is a proof method that solves a goal by one of the
 . This works here because the result of \isacom{finally}
  the theorem \mbox{‹t<sub>1</sub> = t<sub>n</sub>›},
 isacom{show} ‹"t<sub>1</sub> = t<sub>n</sub>"› states the theorem explicitly,
  ``‹.›'' proves the theorem with the result of \isacom{finally}.
 end{description}
  above proof template also works for arbitrary mixtures of ‹=›, ‹≤› and ‹<\<close>,
  example:
 begin{quote}
 isacom{have} ‹"t₁ < t₂"› \isasymproof\\
 isacom{also have} ‹"... = t₃"› \isasymproof\\
 quad $\vdots$\\
 isacom{also have} ‹"... ≤ t_n"› \isasymproof \\
 isacom{finally show} ‹"t₁ < t_n"›\ \texttt{.}
 end{quote}
  relation symbol in the \isacom{finally} step needs to be the most precise one
 . In the example above, you must not write ‹t₁ ≤ t_n› instead of \mbox{‹t₁ < t_n›}.

 begin{warn}
  only supports ‹=›, ‹≤› and ‹<\<close> but not ‹≥› and ‹>›
  (in)equation chains (by default).
 end{warn}

  you want to go beyond merely using the above proof patterns and want to
  what \isacom{also} and \isacom{finally} mean, read on.
  is an Isar theorem variable called ‹calculation›, similar to ‹this›.
  the first \isacom{also} in a chain is encountered, Isabelle sets
 ‹calculation := this›. In each subsequent \isacom{also} step,
  composes the theorems ‹calculation› and ‹this› (i.e.\ the two previous
 in)equalities) using some predefined set of rules including transitivity
  ‹=›, ‹≤› and ‹<\<close> but also mixed rules like prop‹[ x ≤ y; y < z ] ==> x < z›.
  result of this composition is assigned to ‹calculation›. Consider
 begin{quote}
 isacom{have} ‹"t₁ ≤ t₂"› \isasymproof\\
 isacom{also} \isacom{have} ‹"... < t₃"› \isasymproof\\
 isacom{also} \isacom{have} ‹"... = t₄"› \isasymproof\\
 isacom{finally show} ‹"t₁ < t₄"›\ \texttt{.}
 end{quote}
  the first \isacom{also}, ‹calculation› is ‹"t₁ ≤ t₂"›,
  after the second \isacom{also}, ‹calculation› is ‹"t₁ < t₃"›.
  command \isacom{finally} is short for \isacom{also from} ‹calculation›.
  the \isacom{also} hidden in \isacom{finally} sets ‹calculation›
  ‹t₁ < t₄› and the final ``\texttt{.}'' succeeds.

  more information on this style of proof see cite‹"BauerW-TPHOLs01"›.
 fi

 section{Streamlining Proofs}

 subsection{Pattern Matching and Quotations}

  the proof patterns shown above, formulas are often duplicated.
  can make the text harder to read, write and maintain. Pattern matching
  an abbreviation mechanism to avoid such duplication. Writing
 begin{quote}
 isacom{show} \ \textit{formula} ‹(›\indexed{\isacom{is}}{is} \textit{pattern}‹)›
 end{quote}
  the pattern against the formula, thus instantiating the unknowns in
  pattern for later use. As an example, consider the proof pattern for
 ‹⟷›:
 end{isamarkuptext}%
 ›
(*<*)lemma "formula₁ ⟷ formula₂" proof-(*>*)
show "formula₁ ⟷ formula₂" (is "?L ⟷ ?R")
proof
  assume "?L"
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "?R" (*<*)sorry(*>*) text_raw\<open>\ \isasymproof\\\<close>
next
  assume "?R"
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show "?L" (*<*)sorry(*>*) text_raw\<open>\ \isasymproof\\\<close>
qed(*<*)qed(*>*)

text‹Instead of duplicating ‹formula_i› in the text, we introduce
  two abbreviations ‹?L› and ‹?R› by pattern matching.
  matching works wherever a formula is stated, in particular
  \isacom{have} and \isacom{lemma}.

  unknown \indexed{‹?thesis›}{thesis} is implicitly matched against any goal stated by
 isacom{lemma} or \isacom{show}. Here is a typical example:›

lemma "formula"
proof -
  text_raw‹\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}›
  show ?thesis (*<*)sorry(*>*) text_raw\<open>\ \isasymproof\\\<close>
qed

text‹
  can also be instantiated with \indexed{\isacom{let}}{let} commands
 begin{quote}
 isacom{let} ‹?t› = ‹"›\textit{some-big-term}‹"›
 end{quote}
  proof steps can refer to ‹?t›:
 begin{quote}
 isacom{have} ‹"›\dots ‹?t› \dots‹"›
 end{quote}
 begin{warn}
  of facts are introduced with ‹name:› and refer to proved
 . Unknowns ‹?X› refer to terms or formulas.
 end{warn}

  abbreviations shorten the text, the reader needs to remember what
  stand for. Similarly for names of facts. Names like ‹1›, ‹2›
  ‹3› are not helpful and should only be used in short proofs. For
  proofs, descriptive names are better. But look at this example:
 begin{quote}
 isacom{have} \ ‹x_gr_0: "x > 0"›\\
 \vdots$\\
 isacom{from} ‹x_gr_0› \dots
 end{quote}
  name is longer than the fact it stands for! Short facts do not need names;
  can refer to them easily by quoting them:
 begin{quote}
 isacom{have} \ ‹"x > 0"›\\
 \vdots$\\
 isacom{from} ‹‹x > 0›› \dots\index{$IMP053@‹`...`›}
 end{quote}
  outside quotes in ‹‹x > 0›› are the standard renderings of the symbols \texttt{\textbackslash‹} and \texttt{\textbackslash›}.
  refer to the fact not by name but ``by value''.

 subsection{\indexed{\isacom{moreover}}{moreover}}
 index{ultimately@\isacom{ultimately}}

  one needs a number of facts to enable some deduction. Of course
  can name these facts individually, as shown on the right,
  one can also combine them with \isacom{moreover}, as shown on the left:
 ›text_raw‹
 begin{tabular}{@ {}ll@ {}}
 begin{minipage}[t]{.4\textwidth}
 isa{%
 ›
(*<*)lemma "P" proof-(*>*)
have "P₁" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
moreover have "P₂" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
moreover
text_raw‹\\$\vdots$\\\hspace{-1.4ex}›(*<*)have "True" ..(*>*)
moreover have "P_n" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
ultimately have "P"  (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
(*<*)oops(*>*)

text_raw ‹}
 end{minipage}
 
 qquad
 begin{minipage}[t]{.4\textwidth}
 isa{%
 ›
(*<*)lemma "P" proof-(*>*)
have lab₁: "P₁" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
have lab₂: "P₂" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\<close>
text_raw‹\\$\vdots$\\\hspace{-1.4ex}›
have lab_n: "P_n" (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
from lab₁ lab₂ text_raw‹\ $\dots$\\›
have "P"  (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
(*<*)oops(*>*)

text_raw ‹}
 end{minipage}
 end{tabular}
 begin{isamarkuptext}%
  \isacom{moreover} version is no shorter but expresses the structure
  bit more clearly and avoids new names.

 subsection{Local Lemmas}

  one would like to prove some lemma locally within a proof,
  lemma that shares the current context of assumptions but that
  its own assumptions and is generalized over its locally fixed
  at the end. This is simply an extension of the basic
 indexed{\isacom{have}}{have} construct:
 begin{quote}
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 \indexed{\isacom{for}}{for} ‹x₁ … x_n›\\
 isasymproof
 end{quote}
  ‹[ A₁; … ; A_m ] ==> B›
  all ‹x_i› have been replaced by unknowns ‹?x_i›.
  an example we prove a simple fact about divisibility on integers.
  definition of ‹dvd› is @{thm dvd_def}.
 end{isamarkuptext}%
 ›

lemma fixes a b :: int assumes "b dvd (a+b)" shows "b dvd a"
proof -
  have "∃k'. a = b*k'" if asm: "a+b = b*k" for k
  proof
    show "a = b*(k - 1)" using asm by(simp add: algebra_simps)
  qed
  then show ?thesis using assms by(auto simp add: dvd_def)
qed

text‹

 subsection*{Exercises}

 exercise
  a readable, structured proof of the following lemma:
 ›
lemma assumes T: "∀x y. T x y ∨ T y x"
  and A: "∀x y. A x y ∧ A y x ⟶ x = y"
  and TA: "∀x y. T x y ⟶ A x y" and "A x y"
  shows "T x y"
(*<*)oops(*>*)
text‹
 endexercise

 exercise
  a readable, structured proof of the following lemma:
 ›
lemma "∃ys zs. xs = ys @ zs ∧
            (length ys = length zs ∨ length ys = length zs + 1)"
(*<*)oops(*>*)
text‹
 : There are predefined functions @{const_typ take} and @{const_typ drop}
  that ‹take k [x₁,…] = [x₁,…,x_k]› and
 ‹drop k [x₁,…] = [x₊₁,…]›. Let sledgehammer find and apply
  relevant const‹take› and const‹drop› lemmas for you.
 endexercise


 section{Case Analysis and Induction}

 subsection{Datatype Case Analysis}
 index{case analysis|(}

  have seen case analysis on formulas. Now we want to distinguish
  form some term takes: is it ‹0› or of the form term‹Suc n›,
  it term‹[]› or of the form term‹x#xs›, etc. Here is a typical example
  by case analysis on the form of ‹xs›:
 ›

lemma "length(tl xs) = length xs - 1"
proof (cases xs)
  assume "xs = []"
  thus ?thesis by simp
next
  fix y ys assume "xs = y#ys"
  thus ?thesis by simp
qed

text‹\index{cases@‹cases›|(}Function ‹tl› (''tail'') is defined by @{thm list.sel(2)} and
 {thm list.sel(3)}. Note that the result type of const‹length› is typ‹nat›
  prop‹0 - 1 = (0::nat)›.

  proof pattern works for any term ‹t› whose type is a datatype.
  goal has to be proved for each constructor ‹C›:
 begin{quote}
 isacom{fix} \ ‹x₁ … x_n› \isacom{assume} ‹"t = C x₁ … x_n"›
 end{quote}\index{case@\isacom{case}|(}
  case can be written in a more compact form by means of the \isacom{case}
 :
 begin{quote}
 isacom{case} ‹(C x₁ … x_n)›
 end{quote}
  is equivalent to the explicit \isacom{fix}-\isacom{assume} line
  also gives the assumption ‹"t = C x₁ … x_n"› a name: ‹C›,
  the constructor.
  is the \isacom{case} version of the proof above:
 ›
(*<*)lemma "length(tl xs) = length xs - 1"(*>*)
proof (cases xs)
  case Nil
  thus ?thesis by simp
next
  case (Cons y ys)
  thus ?thesis by simp
qed

text‹Remember that ‹Nil› and ‹Cons› are the alphanumeric names
  ‹[]› and ‹#›. The names of the assumptions
  not used because they are directly piped (via \isacom{thus})
  the proof of the claim.
 index{case analysis|)}

 subsection{Structural Induction}
 index{induction|(}
 index{structural induction|(}

  illustrate structural induction with an example based on natural numbers:
  sum (‹∑›) of the first ‹n› natural numbers
 ‹{0..n::nat}›) is equal to \mbox{term‹n*(n+1) div 2::nat›}.
  mind the details, just focus on the pattern:
 ›

lemma "∑{0..n::nat} = n*(n+1) div 2"
proof (induction n)
  show "∑{0..0::nat} = 0*(0+1) div 2" by simp
next
  fix n assume "∑{0..n::nat} = n*(n+1) div 2"
  thus "∑{0..Suc n} = Suc n*(Suc n+1) div 2" by simp
qed

text‹Except for the rewrite steps, everything is explicitly given. This
  the proof easily readable, but the duplication means it is tedious to
  and maintain. Here is how pattern
  can completely avoid any duplication:›

lemma "∑{0..n::nat} = n*(n+1) div 2" (is "?P n")
proof (induction n)
  show "?P 0" by simp
next
  fix n assume "?P n"
  thus "?P(Suc n)" by simp
qed

text‹The first line introduces an abbreviation ‹?P n› for the goal.
  matching ‹?P n› with the goal instantiates ‹?P› to the
  term‹λn. ∑{0..n::nat} = n*(n+1) div 2›. Now the proposition to
  proved in the base case can be written as ‹?P 0›, the induction
  as ‹?P n›, and the conclusion of the induction step as
 ‹?P(Suc n)›.

  also provides the \isacom{case} idiom that abbreviates
  \isacom{fix}-\isacom{assume} step. The above proof becomes
 ›
(*<*)lemma "\<Sum>{0..n::nat} = n*(n+1) div 2"(*>*)
proof (induction n)
  case 0
  show ?case by simp
next
  case (Suc n)
  thus ?case by simp
qed

text‹
  unknown ‹?case›\index{case?@‹?case›|(} is set in each case to the required
 , i.e., ‹?P 0› and \mbox{‹?P(Suc n)›} in the above proof,
  requiring the user to define a ‹?P›. The general
  for induction over typ‹nat› is shown on the left-hand side:
 ›text_raw‹
 begin{tabular}{@ {}ll@ {}}
 begin{minipage}[t]{.4\textwidth}
 isa{%
 ›
(*<*)lemma "P(n::nat)" proof -(*>*)
show "P(n)"
proof (induction n)
  case 0
  text_raw‹\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}›
  show ?case (*<*)sorry(*>*) text_raw\<open>\ \isasymproof\\\<close>
next
  case (Suc n)
  text_raw‹\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}›
  show ?case (*<*)sorry(*>*) text_raw\<open>\ \isasymproof\\\<close>
qed(*<*)qed(*>*)

text_raw ‹}
 end{minipage}
 
 begin{minipage}[t]{.4\textwidth}
 \\
 \\
 isacom{let} ‹?case = "P(0)"›\\
 \\
 \\
 \\[1ex]
 isacom{fix} ‹n› \isacom{assume} ‹Suc: "P(n)"›\\
 isacom{let} ‹?case = "P(Suc n)"›\\
 end{minipage}
 end{tabular}
 medskip
 ›
text‹
  the right side you can see what the \isacom{case} command
  the left stands for.

  case the goal is an implication, induction does one more thing: the
  to be proved in each case is not the whole implication but only
  conclusion; the premises of the implication are immediately made
  of that case. That is, if in the above proof we replace
 isacom{show}~‹"P(n)"› by
 mbox{\isacom{show}~‹"A(n) ==> P(n)"›}
  \isacom{case}~‹0› stands for
 begin{quote}
 isacom{assume} \ ‹0: "A(0)"›\\
 isacom{let} ‹?case = "P(0)"›
 end{quote}
  \isacom{case}~‹(Suc n)› stands for
 begin{quote}
 isacom{fix} ‹n›\\
 isacom{assume} ‹Suc:›
 \begin{tabular}[t]{l}‹"A(n) ==> P(n)"›\\‹"A(Suc n)"›\end{tabular}\\
 isacom{let} ‹?case = "P(Suc n)"›
 end{quote}
  list of assumptions ‹Suc› is actually subdivided
  ‹Suc.IH›, the induction hypotheses (here ‹A(n) ==> P(n)›),
  ‹Suc.prems›, the premises of the goal being proved
 here ‹A(Suc n)›).

  works for any datatype.
  a goal ‹[ A₁(x); …; A_k(x) ] ==> P(x)›
  induction on ‹x› generates a proof obligation for each constructor
 ‹C› of the datatype. The command \isacom{case}~‹(C x₁ … x_n)›
  the following steps:
 begin{enumerate}
 item \isacom{fix} ‹x₁ … x_n›
 item \isacom{assume} the induction hypotheses (calling them ‹C.IH›\index{IH@‹.IH›})
 and the premises \mbox{‹A_i(C x₁ … x_n)›} (calling them ‹C.prems›\index{prems@‹.prems›})
 and calling the whole list ‹C›
 item \isacom{let} ‹?case = "P(C x₁ … x_n)"›
 end{enumerate}
 index{structural induction|)}


 ifsem\else
 subsection{Computation Induction}
 index{rule induction}

  \autoref{sec:recursive-funs} we introduced computation induction and
  realization in Isabelle: the definition
  a recursive function ‹f› via \isacom{fun} proves the corresponding computation
  rule called ‹f.induct›. Induction with this rule looks like in
 autoref{sec:recursive-funs}, but now with \isacom{proof} instead of \isacom{apply}:
 begin{quote}
 isacom{proof} (‹induction x₁ … x_k rule: f.induct›)
 end{quote}
  as for structural induction, this creates several cases, one for each
  equation for ‹f›. By default (if the equations have not been named
  the user), the cases are numbered. That is, they are started by
 begin{quote}
 isacom{case} (‹i x y ...›)
 end{quote}
  ‹i = 1,...,n›, ‹n› is the number of equations defining ‹f›,
  ‹x y ...› are the variables in equation ‹i›. Note the following:
 begin{itemize}
 item
  ‹i› is an Isar name, ‹i.IH› (or similar) is not. You need
  quotes: "‹i.IH›". When indexing the name, write "‹i.IH›"(1),
  "‹i.IH›(1)".
 item
  defining equations for ‹f› overlap, \isacom{fun} instantiates them to make
  nonoverlapping. This means that one user-provided equation may lead to
  equations and thus to several cases in the induction rule.
  have names of the form "‹i_j›", where ‹i› is the number of the original
  and the system-generated ‹j› indicates the subcase.
 end{itemize}
  Isabelle/jEdit, the ‹induction› proof method displays a proof skeleton
  all \isacom{case}s. This is particularly useful for computation induction
  the following rule induction.
 fi


 subsection{Rule Induction}
 index{rule induction|(}

  the inductive and recursive definitions of even numbers in
 autoref{sec:inductive-defs}:
 ›

inductive ev :: "nat → bool" where
ev0: "ev 0" |
evSS: "ev n ==> ev(Suc(Suc n))"

fun evn :: "nat → bool" where
"evn 0 = True" |
"evn (Suc 0) = False" |
"evn (Suc(Suc n)) = evn n"

text‹We recast the proof of prop‹ev n ==> evn n› in Isar. The
  column shows the actual proof text, the right column shows
  implicit effect of the two \isacom{case} commands:›text_raw‹
 begin{tabular}{@ {}l@ {\qquad}l@ {}}
 begin{minipage}[t]{.5\textwidth}
 isa{%
 ›

lemma "ev n ==> evn n"
proof(induction rule: ev.induct)
  case ev0
  show ?case by simp
next
  case evSS



  thus ?case by simp
qed

text_raw ‹}
 end{minipage}
 
 begin{minipage}[t]{.5\textwidth}
 \\
 \\
 isacom{let} ‹?case = "evn 0"›\\
 \\
 \\
 isacom{fix} ‹n›\\
 isacom{assume} ‹evSS:›
 \begin{tabular}[t]{l} ‹"ev n"›\\‹"evn n"›\end{tabular}\\
 isacom{let} ‹?case = "evn(Suc(Suc n))"›\\
 end{minipage}
 end{tabular}
 medskip
 ›
text‹
  proof resembles structural induction, but the induction rule is given
  and the names of the cases are the names of the rules in the
  definition.
  us examine the two assumptions named @{thm[source]evSS}:
 prop‹ev n› is the premise of rule @{thm[source]evSS}, which we may assume
  we are in the case where that rule was used; prop‹evn n›
  the induction hypothesis.
 begin{warn}
  each \isacom{case} command introduces a list of assumptions
  like the case name, which is the name of a rule of the inductive
 , those rules now need to be accessed with a qualified name, here
 {thm[source] ev.ev0} and @{thm[source] ev.evSS}.
 end{warn}

  the case @{thm[source]evSS} of the proof above we have pretended that the
  fixes a variable ‹n›. But unless the user provides the name
 ‹n›, the system will just invent its own name that cannot be referred
 . In the above proof, we do not need to refer to it, hence we do not give
  a specific name. In case one needs to refer to it one writes
 begin{quote}
 isacom{case} ‹(evSS m)›
 end{quote}
  \isacom{case}~‹(Suc n)› in earlier structural inductions.
  name ‹m› is an arbitrary choice. As a result,
  @{thm[source] evSS} is derived from a renamed version of
  @{thm[source] evSS}: ‹ev m ==> ev(Suc(Suc m))›.
  is an example with a (contrived) intermediate step that refers to ‹m›:
 ›

lemma "ev n ==> evn n"
proof(induction rule: ev.induct)
  case ev0 show ?case by simp
next
  case (evSS m)
  have "evn(Suc(Suc m)) = evn m" by simp
  thus ?case using `evn m` by blast
qed

text‹
 indent
  general, let ‹I› be a (for simplicity unary) inductively defined
  and let the rules in the definition of ‹I›
  called ‹rule₁›, \dots, ‹rule_n›. A proof by rule
  follows this pattern:\index{inductionrule@‹induction ... rule:›}
 ›

(*<*)
inductive I where rule₁: "I()" |  rule₂: "I()" |  rule_n: "I()"
lemma "I x ==> P x" proof-(*>*)
show "I x ==> P x"
proof(induction rule: I.induct)
  case rule₁
  text_raw‹\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}›
  show ?case (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
next
  text_raw‹\\[-.4ex]$\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}›
(*<*)
  case rule₂
  show ?case sorry
(*>*)
next
  case rule_n
  text_raw‹\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}›
  show ?case (*<*)sorry(*>*)text_raw\<open>\ \isasymproof\\\<close>
qed(*<*)qed(*>*)

text‹
  can provide explicit variable names by writing
 isacom{case}~‹(rule_i x₁ … x_k)›, thus renaming the first ‹k›
  variables in rule ‹i› to ‹x₁ … x_k›,
  through rule ‹i› from left to right.

 subsection{Assumption Naming}
 label{sec:assm-naming}

  any induction, \isacom{case}~‹name› sets up a list of assumptions
  called ‹name›, which is subdivided into three parts:
 begin{description}
 item[‹name.IH›]\index{IH@‹.IH›} contains the induction hypotheses.
 item[‹name.hyps›]\index{hyps@‹.hyps›} contains all the other hypotheses of this case in the
  rule. For rule inductions these are the hypotheses of rule
 ‹name›, for structural inductions these are empty.
 item[‹name.prems›]\index{prems@‹.prems›} contains the (suitably instantiated) premises
  the statement being proved, i.e., the ‹A_i› when
  ‹[ A₁; …; A_n ] ==> A›.
 end{description}
 begin{warn}
  method ‹induct› differs from ‹induction›
  in this naming policy: ‹induct› does not distinguish
 ‹IH› from ‹hyps› but subsumes ‹IH› under ‹hyps›.
 end{warn}

  complicated inductive proofs than the ones we have seen so far
  need to refer to specific assumptions --- just ‹name› or even
 ‹name.prems› and ‹name.IH› can be too unspecific.
  is where the indexing of fact lists comes in handy, e.g.,
 ‹name.IH(2)› or ‹name.prems(1-2)›.

 subsection{Rule Inversion}
 label{sec:rule-inversion}
 index{rule inversion|(}

  inversion is case analysis of which rule could have been used to
  some fact. The name \conceptnoidx{rule inversion} emphasizes that we are
  backwards: by which rules could some given fact have been proved?
  the inductive definition of const‹ev›, rule inversion can be summarized
  this:
 {prop[display]"ev n ==> n = 0 ∨ (∃k. n = Suc(Suc k) ∧ ev k)"}
  realisation in Isabelle is a case analysis.
  simple example is the proof that prop‹ev n ==> ev (n - 2)›. We
  went through the details informally in \autoref{sec:Logic:even}. This
  the Isar proof:
 ›
(*<*)
notepad
begin fix n
(*>*)
  assume "ev n"
  from this have "ev(n - 2)"
  proof cases
    case ev0 thus "ev(n - 2)" by (simp add: ev.ev0)
  next
    case (evSS k) thus "ev(n - 2)" by (simp add: ev.evSS)
  qed
(*<*)
end
(*>*)

text‹The key point here is that a case analysis over some inductively
  predicate is triggered by piping the given fact
 here: \isacom{from}~‹this›) into a proof by ‹cases›.
  us examine the assumptions available in each case. In case ‹ev0›
  have ‹n = 0› and in case ‹evSS› we have prop‹n = Suc(Suc k)›
  prop‹ev k›. In each case the assumptions are available under the name
  the case; there is no fine-grained naming schema like there is for induction.

  some rules could not have been used to derive the given fact
  constructors clash. As an extreme example consider
  inversion applied to prop‹ev(Suc 0)›: neither rule ‹ev0› nor
  ‹evSS› can yield prop‹ev(Suc 0)› because ‹Suc 0› unifies
  with ‹0› nor with term‹Suc(Suc n)›. Impossible cases do not
  to be proved. Hence we can prove anything from prop‹ev(Suc 0)›:
 ›
(*<*)
notepad begin fix P
(*>*)
  assume "ev(Suc 0)" then have P by cases
(*<*)
end
(*>*)

text‹That is, prop‹ev(Suc 0)› is simply not provable:›

lemma "¬ ev(Suc 0)"
proof
  assume "ev(Suc 0)" then show False by cases
qed

text‹Normally not all cases will be impossible. As a simple exercise,
  that \mbox{prop‹¬ ev(Suc(Suc(Suc 0)))›.}

 subsection{Advanced Rule Induction}
 label{sec:advanced-rule-induction}

  far, rule induction was always applied to goals of the form ‹I x y z ==> …›
  ‹I› is some inductively defined predicate and ‹x›, ‹y›, ‹z›
  variables. In some rare situations one needs to deal with an assumption where
  all arguments ‹r›, ‹s›, ‹t› are variables:
 begin{isabelle}
 isacom{lemma} ‹"I r s t ==> …"›
 end{isabelle}
  the standard form of
  induction in such a situation will lead to strange and typically unprovable goals.
  can easily reduce this situation to the standard one by introducing
  variables ‹x›, ‹y›, ‹z› and reformulating the goal like this:
 begin{isabelle}
 isacom{lemma} ‹"I x y z ==> x = r ==> y = s ==> z = t ==> …"›
 end{isabelle}
  rule induction will work fine now, provided the free variables in
 ‹r›, ‹s›, ‹t› are generalized via ‹arbitrary›.

 , induction can do the above transformation for us, behind the curtains, so we never
  to see the expanded version of the lemma. This is what we need to write:
 begin{isabelle}
 isacom{lemma} ‹"I r s t ==> …"›\isanewline
 isacom{proof}‹(induction "r" "s" "t" arbitrary: … rule: I.induct)›\index{inductionrule@‹induction ... rule:›}\index{arbitrary@‹arbitrary:›}
 end{isabelle}
  for rule inversion, cases that are impossible because of constructor clashes
  not show up at all. Here is a concrete example:›

lemma "ev (Suc m) ==> ¬ ev m"
proof(induction "Suc m" arbitrary: m rule: ev.induct)
  fix n assume IH: "∧m. n = Suc m ==> ¬ ev m"
  show "¬ ev (Suc n)"
  proof ― ‹contradiction›
    assume "ev(Suc n)"
    thus False
    proof cases ― ‹rule inversion›
      fix k assume "n = Suc k" "ev k"
      thus False using IH by auto
    qed
  qed
qed

text‹
 :
 begin{itemize}
 item
  of the \isacom{case} and ‹?case› magic we have spelled all formulas out.
  is merely for greater clarity.
 item
  only need to deal with one case because the @{thm[source] ev0} case is impossible.
 item
  form of the ‹IH› shows us that internally the lemma was expanded as explained
 : \noquotes{@{prop[source]"ev x ==> x = Suc m ==> ¬ ev m"}}.
 item
  goal prop‹¬ ev (Suc n)› may surprise. The expanded version of the lemma
  suggest that we have a \isacom{fix} ‹m› \isacom{assume} prop‹Suc(Suc n) = Suc m›
  need to show prop‹¬ ev m›. What happened is that Isabelle immediately
  prop‹Suc(Suc n) = Suc m› to prop‹Suc n = m› and could then eliminate
 ‹m›. Beware of such nice surprises with this advanced form of induction.
 end{itemize}
 begin{warn}
  advanced form of induction does not support the ‹IH›
  schema explained in \autoref{sec:assm-naming}:
  induction hypotheses are instead found under the name ‹hyps›,
  they are for the simpler
 ‹induct› method.
 end{warn}
 index{induction|)}
 index{cases@‹cases›|)}
 index{case@\isacom{case}|)}
 index{case?@‹?case›|)}
 index{rule induction|)}
 index{rule inversion|)}

 subsection*{Exercises}


 exercise
  a structured proof by rule inversion:
 ›

lemma assumes a: "ev(Suc(Suc n))" shows "ev n"
(*<*)oops(*>*)

text‹
 endexercise

 begin{exercise}
  a structured proof of prop‹¬ ev(Suc(Suc(Suc 0)))›
  rule inversions. If there are no cases to be proved you can close
  proof immediately with \isacom{qed}.
 end{exercise}

 begin{exercise}
  predicate ‹star› from \autoref{sec:star} and ‹iter›
  Exercise~\ref{exe:iter}. Prove prop‹iter r n x y ==> star r x y›
  a structured style; do not just sledgehammer each case of the
  induction.
 end{exercise}

 begin{exercise}
  a recursive function ‹elems ::› typ‹'a list → 'a set›
  prove prop‹x ∈ elems xs ==> ∃ys zs. xs = ys @ x # zs ∧ x ∉ elems ys›.
 end{exercise}

 begin{exercise}
  Exercise~\ref{exe:cfg} with a function that checks if some
 mbox{‹alpha list›} is a balanced
  of parentheses. More precisely, define a \mbox{recursive} function
 ‹balanced :: nat → alpha list → bool› such that term‹balanced n w›
  true iff (informally) ‹S (aⁿ @ w)›. Formally, prove that
 prop‹balanced n w ⟷ S (replicate n a @ w)› where
 const‹replicate› ‹::› typ‹nat → 'a → 'a list› is predefined
  term‹replicate n x› yields the list ‹[x, …, x]› of length ‹n›.
 end{exercise}
 ›

(*<*)
end
(*>*)