Quelle  AdvancedInd.thy

(*<*)
theory AdvancedInd imports Main begin
(*>*)

text‹\noindent
  that we have learned about rules and logic, we take another look at the
  points of induction. We consider two questions: what to do if the
  to be proved is not directly amenable to induction
 \S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
  even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
  an extended example of induction (\S\ref{sec:CTL-revisited}).
 ›

subsection‹Massaging the Proposition›

text‹\label{sec:ind-var-in-prems}
  we have assumed that the theorem to be proved is already in a form
  is amenable to induction, but sometimes it isn't.
  is an example.
  term‹hd› and term‹last› return the first and last element of a
 -empty list, this lemma looks easy to prove:
 ›

lemma "xs ≠ [] ==> hd(rev xs) = last xs"
apply(induct_tac xs)

txt‹\noindent
  induction produces the warning
 begin{quote}\tt
  variable occurs also among premises!
 end{quote}
  leads to the base case
 {subgoals[display,indent=0,goals_limit=1]}
  reduces the base case to this:
 begin{isabelle}
  1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
 end{isabelle}
  cannot prove this equality because we do not know what term‹hd› and
 term‹last› return when applied to term‹[]›.

  should not have ignored the warning. Because the induction
  is only the conclusion, induction does not affect the occurrence of term‹xs› in the premises.
  the case that should have been trivial
  unprovable. Fortunately, the solution is easy:\footnote{A similar
  applies to rule inductions; see \S\ref{sec:rtc}.}
 begin{quote}
 emph{Pull all occurrences of the induction variable into the conclusion
  ‹⟶›.}
 end{quote}
  we should state the lemma as an ordinary
 ~(‹⟶›), letting
 attrdx{rule_format} (\S\ref{sec:forward}) convert the
  to the usual ‹==>› form:
 ›
(*<*)oops(*>*)
lemma hd_rev [rule_format]: "xs ≠ [] ⟶ hd(rev xs) = last xs"
(*<*)
apply(induct_tac xs)
(*>*)

txt‹\noindent
  time, induction leaves us with a trivial base case:
 {subgoals[display,indent=0,goals_limit=1]}
  ‹auto› completes the proof.

  there are multiple premises $A@1$, \dots, $A@n$ containing the
  variable, you should turn the conclusion $C$ into
 [ A@1 \longrightarrow \cdots A@n \longrightarrow C. \]
 , you may also have to universally quantify some other variables,
  can yield a fairly complex conclusion. However, ‹rule_format›
  remove any number of occurrences of ‹∀› and
 ‹⟶›.

 index{induction!on a term}%
  second reason why your proposition may not be amenable to induction is that
  want to induct on a complex term, rather than a variable. In
 , induction on a term~$t$ requires rephrasing the conclusion~$C$
 
 begin{equation}\label{eqn:ind-over-term}
 forall y@1 \dots y@n.~ x = t \longrightarrow C.
 end{equation}
  $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
  you can perform induction on~$x$. An example appears in
 S\ref{sec:complete-ind} below.

  very same problem may occur in connection with rule induction. Remember
  it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is
  inductively defined set and the $x@i$ are variables. If instead we have
  premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we
  it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
 [ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \]
  an example see \S\ref{sec:CTL-revisited} below.

  course, all premises that share free variables with $t$ need to be pulled into
  conclusion as well, under the ‹∀›, again using ‹⟶› as shown above.

  who are puzzled by the form of statement
 \ref{eqn:ind-over-term}) above should remember that the
  is only performed to permit induction. Once induction
  been applied, the statement can be transformed back into something quite
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 \prec$) to (\ref{eqn:ind-over-term}) and transforming the result a
  leads to the goal
 [ \bigwedge\overline{y}.\ 
 \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z}
 \ \Longrightarrow\ C\,\overline{y} \]
  $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and
 C$ on the free variables of $t$ has been made explicit.
 , this induction schema cannot be expressed as a
  theorem because it depends on the number of free variables in $t$ ---
  notation $\overline{y}$ is merely an informal device.
 ›
(*<*)by auto(*>*)

subsection‹Beyond Structural and Recursion Induction›

text‹\label{sec:complete-ind}
  far, inductive proofs were by structural induction for
  recursive functions and recursion induction for total recursive
 . But sometimes structural induction is awkward and there is no
  function that could furnish a more appropriate
  schema. In such cases a general-purpose induction schema can
  helpful. We show how to apply such induction schemas by an example.

  induction on 🍋‹nat› is
  known as mathematical induction. There is also \textbf{complete}
 index{induction!complete}%
 , where you prove $P(n)$ under the assumption that $P(m)$
  for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}:
 {thm[display]"nat_less_induct"[no_vars]}
  an application, we prove a property of the following
 :
 ›

axiomatization f :: "nat ==> nat"
  where f_ax: "f(f(n)) < f(Suc(n))" for n :: nat

text‹
 begin{warn}
  discourage the use of axioms because of the danger of
 . Axiom ‹f_ax› does
  introduce an inconsistency because, for example, the identity function
  it. Axioms can be useful in exploratory developments, say when
  assume some well-known theorems so that you can quickly demonstrate some
  about methodology. If your example turns into a substantial proof
 , you should replace axioms by theorems.
 end{warn}\noindent
  axiom for term‹f› implies prop‹n <= f n›, which can
  proved by induction on \mbox{term‹f n›}. Following the recipe outlined
 , we have to phrase the proposition as follows to allow induction:
 ›

lemma f_incr_lem: "∀i. k = f i ⟶ i ≤ f i"

txt‹\noindent
  perform induction on term‹k› using @{thm[source]nat_less_induct}, we use
  same general induction method as for recursion induction (see
 S\ref{sec:fun-induction}):
 ›

apply(induct_tac k rule: nat_less_induct)

txt‹\noindent
  get the following proof state:
 {subgoals[display,indent=0,margin=65]}
  stripping the ‹∀i›, the proof continues with a case
  on term‹i›. The case prop‹i = (0::nat)› is trivial and we focus on
  other case:
 ›

apply(rule allI)
apply(case_tac i)
 apply(simp)
txt‹
 {subgoals[display,indent=0]}
 ›
by(blast intro!: f_ax Suc_leI intro: le_less_trans)

text‹\noindent
  you find the last step puzzling, here are the two lemmas it employs:
 begin{isabelle}
 {thm Suc_leI[no_vars]}
 rulename{Suc_leI}\isanewline
 {thm le_less_trans[no_vars]}
 rulename{le_less_trans}
 end{isabelle}
 
  proof goes like this (writing term‹j› instead of 🍋‹nat›).
  prop‹i = Suc j› it suffices to show
 hbox{prop‹j < f(Suc j)›},
  @{thm[source]Suc_leI}\@. This is
  as follows. From @{thm[source]f_ax} we have prop‹f (f j) < f (Suc j)›
 1) which implies prop‹f j <= f (f j)› by the induction hypothesis.
  (1) once more we obtain prop‹f j < f(Suc j)› (2) by the transitivity
  @{thm[source]le_less_trans}.
  the induction hypothesis once more we obtain prop‹j <= f j›
 , together with (2) yields prop‹j < f (Suc j)› (again by
 {thm[source]le_less_trans}).

  last step shows both the power and the danger of automatic proofs. They
  usually not tell you how the proof goes, because it can be hard to
  the internal proof into a human-readable format. Automatic
  are easy to write but hard to read and understand.

  desired result, prop‹i <= f i›, follows from @{thm[source]f_incr_lem}:
 ›

lemmas f_incr = f_incr_lem[rule_format, OF refl]

text‹\noindent
  final @{thm[source]refl} gets rid of the premise ‹?k = f ?i›.
  could have included this derivation in the original statement of the lemma:
 ›

lemma f_incr[rule_format, OF refl]: "∀i. k = f i ⟶ i ≤ f i"
(*<*)oops(*>*)

text‹
 begin{exercise}
  the axiom and lemma for term‹f›, show that term‹f› is the
  function.
 end{exercise}

  \methdx{induct_tac} can be applied with any rule $r$
  conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
  is
 begin{quote}
 isacommand{apply}‹(induct_tac› $y@1 \dots y@n$ ‹rule:› $r$‹)›
 end{quote}
  $y@1, \dots, y@n$ are variables in the conclusion of the first subgoal.

  further useful induction rule is @{thm[source]length_induct},
  on the length of a list\indexbold{*length_induct}
 {thm[display]length_induct[no_vars]}
  is a special case of @{thm[source]measure_induct}
 {thm[display]measure_induct[no_vars]}
  term‹f› may be any function into type 🍋‹nat›.
 ›

subsection‹Derivation of New Induction Schemas›

text‹\label{sec:derive-ind}
 index{induction!deriving new schemas}%
  schemas are ordinary theorems and you can derive new ones
  you wish. This section shows you how, using the example
  @{thm[source]nat_less_induct}. Assume we only have structural induction
  for 🍋‹nat› and want to derive complete induction. We
  generalize the statement as shown:
 ›

lemma induct_lem: "(∧n::nat. ∀m<n. P m ==> P n) ==> ∀m<n. P m"
apply(induct_tac n)

txt‹\noindent
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
  n›) we distinguish two cases: case prop‹m < n› is true by induction
  and case prop‹m = n› follows from the assumption, again using
  induction hypothesis:
 ›
 apply(blast)
by(blast elim: less_SucE)

text‹\noindent
  elimination rule @{thm[source]less_SucE} expresses the case distinction:
 {thm[display]"less_SucE"[no_vars]}

  it is straightforward to derive the original version of
 {thm[source]nat_less_induct} by manipulating the conclusion of the above
 : instantiate term‹n› by term‹Suc n› and term‹m› by term‹n›
  remove the trivial condition prop‹n < Suc n›. Fortunately, this
  automatically when we add the lemma as a new premise to the
  goal:
 ›

theorem nat_less_induct: "(∧n::nat. ∀m<n. P m ==> P n) ==> P n"
by(insert induct_lem, blast)

text‹
  already provides the mother of
  inductions, well-founded induction (see \S\ref{sec:Well-founded}). For
  theorem @{thm[source]nat_less_induct} is
  special case of @{thm[source]wf_induct} where term‹r› is ‹<\<close> on
 🍋‹nat›. The details can be found in theory \isa{Wellfounded_Recursion}.
 ›
(*<*)end(*>*)