(*<*)
theory Logic
imports LaTeXsugar
begin
(*>*)
text‹
 vspace{-5ex}
 section{Formulas}

  core syntax of formulas (\textit{form} below)
  the standard logical constructs, in decreasing order of precedence:
 [
 begin{array}{rcl}

 mathit{form} & ::= &
 ‹(form)› ~\mid~
 const‹True› ~\mid~
 const‹False› ~\mid~
 prop‹term = term›\\
 &\mid& prop‹¬ form›\index{$HOL4@\isasymnot} ~\mid~
 prop‹form ∧ form›\index{$HOL0@\isasymand} ~\mid~
 prop‹form ∨ form›\index{$HOL1@\isasymor} ~\mid~
 prop‹form ⟶ form›\index{$HOL2@\isasymlongrightarrow}\\
 &\mid& prop‹∀x. form›\index{$HOL6@\isasymforall} ~\mid~ prop‹∃x. form›\index{$HOL7@\isasymexists}
 end{array}
 ]
  are the ones we have seen all along, built from constants, variables,
  application and ‹λ›-abstraction, including all the syntactic
  like infix symbols, ‹if›, ‹case›, etc.
 begin{warn}
  that formulas are simply terms of type ‹bool›. Hence
 ‹=› also works for formulas. Beware that ‹=› has a higher
  than the other logical operators. Hence prop‹s = t ∧ A› means
 ‹(s = t) ∧ A›, and prop‹A∧B = B∧A› means ‹A ∧ (B = B) ∧ A›.
  equivalence can also be written with
 ‹⟷› instead of ‹=›, where ‹⟷› has the same low
  as ‹⟶›. Hence ‹A ∧ B ⟷ B ∧ A› really means
 ‹(A ∧ B) ⟷ (B ∧ A)›.
 end{warn}
 begin{warn}
  need to be enclosed in parentheses if they are nested within
  constructs (just like ‹if›, ‹case› and ‹let›).
 end{warn}
  most frequent logical symbols and their ASCII representations are shown
  Fig.~\ref{fig:log-symbols}.
 begin{figure}
 begin{center}
 begin{tabular}{l@ {\qquad}l@ {\qquad}l}
 ‹∀› & \xsymbol{forall} & \texttt{ALL}\\
 ‹∃› & \xsymbol{exists} & \texttt{EX}\\
 ‹λ› & \xsymbol{lambda} & \texttt{\%}\\
 ‹⟶› & \texttt{-{\kern0pt}->}\\
 ‹⟷› & \texttt{🚫}\\
 ‹∧› & \texttt{/\char`\\} & >\texttt{\&}\\
 ‹∨› & \texttt{\char`\\/} & >\texttt{|}\\
 ‹¬› & \xsymbol{not} & \texttt{\char`~}\\
 ‹≠› & \xsymbol{noteq} & \texttt{\char`~=}
 end{tabular}
 end{center}
 caption{Logical symbols and their ASCII forms}
 label{fig:log-symbols}
 end{figure}
  first column shows the symbols, the other columns ASCII representations.
  \texttt{\char`\\}\texttt{<...>} form is always converted into the symbolic form
  the Isabelle interfaces, the treatment of the other ASCII forms
  on the interface. The ASCII forms \texttt{/\char`\\} and
 texttt{\char`\\/}
  special in that they are merely keyboard shortcuts for the interface and
  logical symbols by themselves.
 begin{warn}
  implication ‹==>› is part of the Isabelle framework. It structures
  and proof states, separating assumptions from conclusions.
  implication ‹⟶› is part of the logic HOL and can occur inside the
  that make up the assumptions and conclusion.
  should be of the form ‹[ A₁; …; A_n ] ==> A›,
  ‹A₁ ∧ … ∧ A_n ⟶ A›. Both are logically equivalent
  the first one works better when using the theorem in further proofs.

  ASCII representation of ‹[› and ‹]› is \texttt{[|} and \texttt{|]}.
 end{warn}

 section{Sets}
 label{sec:Sets}

  of elements of type typ‹'a› have type typ‹'a set›\index{set@‹set›}.
  can be finite or infinite. Sets come with the usual notation:
 begin{itemize}
 item \indexed{term‹{}›}{$IMP042},\quad ‹{e₁,…,e_n}›
 item prop‹e ∈ A›\index{$HOLSet0@\isasymin},\quad prop‹A ⊆ B›\index{$HOLSet2@\isasymsubseteq}
 item term‹A ∪ B›\index{$HOLSet4@\isasymunion},\quad term‹A ∩ B›\index{$HOLSet5@\isasyminter},\quad term‹A - B›,\quad term‹-A›
 end{itemize}
 where term‹A-B› and ‹-A› are set difference and complement)
  much more. const‹UNIV› is the set of all elements of some type.
  comprehension\index{set comprehension} is written
 term‹{x. P}›\index{$IMP042@term‹{x. P}›} rather than ‹{x | P}›.
 begin{warn}
  term‹{x. P}› the ‹x› must be a variable. Set comprehension
  a proper term ‹t› must be written
 noquotes{@{term[source] "{t | x y. P}"}}\index{$IMP042@‹{t |x. P}›},
  ‹x y› are those free variables in ‹t›
  occur in ‹P›.
  is just a shorthand for term‹{v. ∃x y. v = t ∧ P}›, where
 ‹v› is a new variable. For example, term‹{x+y|x. x ∈ A}›
  short for \noquotes{@{term[source]"{v. ∃x. v = x+y ∧ x ∈ A}"}}.
 end{warn}

  are the ASCII representations of the mathematical symbols:
 begin{center}
 begin{tabular}{l@ {\quad}l@ {\quad}l}
 ‹∈› & \texttt{\char`\\\char`∈} & \texttt{:}\\
 ‹⊆› & \texttt{\char`\\\char`⊆} & \texttt{<=}\\
 ‹∪› & \texttt{\char`\\\char`∪} & \texttt{Un}\\
 ‹∩› & \texttt{\char`\\\char`∩} & \texttt{Int}
 end{tabular}
 end{center}
  also allow bounded quantifications prop‹∀x ∈ A. P› and
 prop‹∃x ∈ A. P›.

  the more ambitious, there are also ‹∪›\index{$HOLSet6@\isasymUnion}
  ‹∩›\index{$HOLSet7@\isasymInter}:
 begin{center}
 {thm Union_eq} \qquad @{thm Inter_eq}
 end{center}
  ASCII forms of ‹∪› are \texttt{\char`\\\char`∪} and \texttt{Union},
  of ‹∩› are \texttt{\char`\\\char`∩} and \texttt{Inter}.
  are also indexed unions and intersections:
 begin{center}
 {thm[eta_contract=false] UNION_eq} \\ @{thm[eta_contract=false] INTER_eq}
 end{center}
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
  \texttt{x} may occur in \texttt{B}.
  \texttt{A} is \texttt{UNIV} you can write \ \texttt{UN x.~B} \ and \ \texttt{INT x. B}.

  other frequently useful functions on sets are the following:
 begin{center}
 begin{tabular}{l@ {\quad}l}
 {const_typ set}\index{set@const‹set›} & converts a list to the set of its elements\\
 {const_typ finite}\index{finite@const‹finite›} & is true iff its argument is finite\\
 noquotes{@{term[source] "card :: 'a set → nat"}}\index{card@const‹card›} & is the cardinality of a finite setle='color:turquoise'>\\
 & and is ‹0› for all infinite sets\\
 {thm image_def}\index{$IMP042@term‹f ` A›} & is the image of a function over a set
 end{tabular}
 end{center}
  cite‹"Nipkow-Main"› for the wealth of further predefined functions in theory
 🚫‹Main›.


 subsection*{Exercises}

 exercise
  from the data type of binary trees defined earlier:
 ›

datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"

text‹
  a function ‹set ::› typ‹'a tree → 'a set›
  returns the elements in a tree and a function
 ‹ord ::› typ‹int tree → bool›
  tests if an typ‹int tree› is ordered.

  a function ‹ins› that inserts an element into an ordered typ‹int tree›
  maintaining the order of the tree. If the element is already in the tree, the
  tree should be returned. Prove correctness of ‹ins›:
 prop‹set(ins x t) = {x} ∪ set t› and prop‹ord t ==> ord(ins i t)›.
 endexercise


 section{Proof Automation}

  far we have only seen ‹simp› and \indexed{‹auto›}{auto}: Both perform
 , both can also prove linear arithmetic facts (no multiplication),
  ‹auto› is also able to prove simple logical or set-theoretic goals:
 ›

lemma "∀x. ∃y. x = y"
by auto

lemma "A ⊆ B ∩ C ==> A ⊆ B ∪ C"
by auto

text‹where
 begin{quote}
 isacom{by} \textit{proof-method}
 end{quote}
  short for
 begin{quote}
 isacom{apply} \textit{proof-method}\\
 isacom{done}
 end{quote}
  key characteristics of both ‹simp› and ‹auto› are
 begin{itemize}
 item They show you where they got stuck, giving you an idea how to continue.
 item They perform the obvious steps but are highly incomplete.
 end{itemize}
  proof method is \conceptnoidx{complete} if it can prove all true formulas.
  is no complete proof method for HOL, not even in theory.
  all our proof methods only differ in how incomplete they are.

  proof method that is still incomplete but tries harder than ‹auto› is
 indexed{‹fastforce›}{fastforce}. It either succeeds or fails, it acts on the first
  only, and it can be modified like ‹auto›, e.g.,
  ‹simp add›. Here is a typical example of what ‹fastforce›
  do:
 ›

lemma "[ ∀xs ∈ A. ∃ys. xs = ys @ ys; us ∈ A ]
   ==> ∃n. length us = n+n"
by fastforce

text‹This lemma is out of reach for ‹auto› because of the
 . Even ‹fastforce› fails when the quantifier structure
  more complicated. In a few cases, its slow version ‹force›
  where ‹fastforce› fails.

  method of choice for complex logical goals is \indexed{‹blast›}{blast}. In the
  example, ‹T› and ‹A› are two binary predicates. It
  shown that if ‹T› is total, ‹A› is antisymmetric and ‹T› is
  subset of ‹A›, then ‹A› is a subset of ‹T›:
 ›

lemma
  "[ ∀x y. T x y ∨ T y x;
     ∀x y. A x y ∧ A y x ⟶ x = y;
     ∀x y. T x y ⟶ A x y ]
   ==> ∀x y. A x y ⟶ T x y"
by blast

text‹
  leave it to the reader to figure out why this lemma is true.
  ‹blast›
 begin{itemize}
 item is (in principle) a complete proof procedure for first-order formulas,
 a fragment of HOL. In practice there is a search bound.
 item does no rewriting and knows very little about equality.
 item covers logic, sets and relations.
 item either succeeds or fails.
 end{itemize}
  of its strength in logic and sets and its weakness in equality reasoning, it complements the earlier proof methods.


 subsection{\concept{Sledgehammer}}

  \isacom{sledgehammer} calls a number of external automatic
  provers (ATPs) that run for up to 30 seconds searching for a
 . Some of these ATPs are part of the Isabelle installation, others are
  over the internet. If successful, a proof command is generated and can
  inserted into your proof. The biggest win of \isacom{sledgehammer} is
  it will take into account the whole lemma library and you do not need to
  in any lemma explicitly. For example,›

lemma "[ xs @ ys = ys @ xs; length xs = length ys ] ==> xs = ys"

txt‹cannot be solved by any of the standard proof methods, but
 isacom{sledgehammer} finds the following proof:›

by (metis append_eq_conv_conj)

text‹We do not explain how the proof was found but what this command
 . For a start, Isabelle does not trust external tools (and in particular
  the translations from Isabelle's logic to those tools!)
  insists on a proof that it can check. This is what \indexed{‹metis›}{metis} does.
  is given a list of lemmas and tries to find a proof using just those lemmas
 and pure logic). In contrast to using ‹simp› and friends who know a lot of
  already, using ‹metis› manually is tedious because one has
  find all the relevant lemmas first. But that is precisely what
 isacom{sledgehammer} does for us.
  this case lemma @{thm[source]append_eq_conv_conj} alone suffices:
 {thm[display] append_eq_conv_conj}
  leave it to the reader to figure out why this lemma suffices to prove
  above lemma, even without any knowledge of what the functions const‹take›
  const‹drop› do. Keep in mind that the variables in the two lemmas
  independent of each other, despite the same names, and that you can
  arbitrary values for the free variables in a lemma.

  as for the other proof methods we have seen, there is no guarantee that
 isacom{sledgehammer} will find a proof if it exists. Nor is
 isacom{sledgehammer} superior to the other proof methods. They are
 . Therefore it is recommended to apply ‹simp› or ‹auto› before invoking \isacom{sledgehammer} on what is left.

 subsection{Arithmetic}

  arithmetic formulas we mean formulas involving variables, numbers, ‹+›, ‹-›, ‹=›, ‹<\<close>, ‹≤› and the usual logical
  ‹¬›, ‹∧›, ‹∨›, ‹⟶›,
 ‹⟷›. Strictly speaking, this is known as \concept{linear arithmetic}
  it does not involve multiplication, although multiplication with
 , e.g., ‹2*n›, is allowed. Such formulas can be proved by
 indexed{‹arith›}{arith}:
 ›

  "[ (a::nat) ≤ x + b; 2*x < c ] ==> 2*a + 1 ≤ 2*b + c"
  arith

 ‹In fact, ‹auto› and ‹simp› can prove many linear
  formulas already, like the one above, by calling a weak but fast
  of ‹arith›. Hence it is usually not necessary to invoke
 ‹arith› explicitly.

  above example involves natural numbers, but integers (type typ‹int›)
  real numbers (type ‹real›) are supported as well. As are a number
  further operators like const‹min› and const‹max›. On typ‹nat› and
 typ‹int›, ‹arith› can even prove theorems with quantifiers in them,
  we will not enlarge on that here.


 subsection{Trying Them All}

  you want to try all of the above automatic proof methods you simply type
 begin{isabelle}
 isacom{try}
 end{isabelle}
  is also a lightweight variant \isacom{try0} that does not call
 . If desired, specific simplification and introduction rules
  be added:
 begin{isabelle}
 isacom{try0} ‹simp: … intro: …›
 end{isabelle}

 section{Single Step Proofs}

  automation is nice, it often fails, at least initially, and you need
  find out why. When ‹fastforce› or ‹blast› simply fail, you have
  clue why. At this point, the stepwise
  of proof rules may be necessary. For example, if ‹blast›
  on prop‹A ∧ B›, you want to attack the two
  ‹A› and ‹B› separately. This can
  achieved by applying \emph{conjunction introduction}
 [ @{thm[mode=Rule,show_question_marks]conjI}\ ‹conjI›
 ]
  the proof state. We will now examine the details of this process.

 subsection{Instantiating Unknowns}

  had briefly mentioned earlier that after proving some theorem,
  replaces all free variables ‹x› by so called \conceptidx{unknowns}{unknown}
 ‹?x›. We can see this clearly in rule @{thm[source] conjI}.
  unknowns can later be instantiated explicitly or implicitly:
 begin{itemize}
 item By hand, using \indexed{‹of›}{of}.
  expression ‹conjI[of "a=b" "False"]›
  the unknowns in @{thm[source] conjI} from left to right with the
  formulas ‹a=b› and ‹False›, yielding the rule
 {thm[display,mode=Rule,margin=100]conjI[of "a=b" False]}

  general, ‹th[of string₁ … string_n]› instantiates
  unknowns in the theorem ‹th› from left to right with the terms
 ‹string₁› to ‹string_n›.

 item By unification. \conceptidx{Unification}{unification} is the process of making two
  syntactically equal by suitable instantiations of unknowns. For example,
  ‹?P ∧ ?Q› with \mbox{prop‹a=b ∧ False›} instantiates
 ‹?P› with prop‹a=b› and ‹?Q› with prop‹False›.
 end{itemize}
  need not instantiate all unknowns. If we want to skip a particular one we
  write ‹_› instead, for example ‹conjI[of _ "False"]›.
  can also be instantiated by name using \indexed{‹where›}{where}, for example
 ‹conjI[where ?P = "a=b"› \isacom{and} ‹?Q = "False"]›.


 subsection{Rule Application}

 conceptidx{Rule application}{rule application} means applying a rule backwards to a proof state.
  example, applying rule @{thm[source]conjI} to a proof state
 begin{quote}
 ‹1. … ==> A ∧ B›
 end{quote}
  in two subgoals, one for each premise of @{thm[source]conjI}:
 begin{quote}
 ‹1. … ==> A›\\
 ‹2. … ==> B›
 end{quote}
  general, the application of a rule ‹[ A₁; …; A_n ] ==> A›
  a subgoal \mbox{‹… ==> C›} proceeds in two steps:
 begin{enumerate}
 item
  ‹A› and ‹C›, thus instantiating the unknowns in the rule.
 item
  the subgoal ‹C› with ‹n› new subgoals ‹A₁› to ‹A_n›.
 end{enumerate}
  is the command to apply rule ‹xyz›:
 begin{quote}
 isacom{apply}‹(rule xyz)›\index{rule@‹rule›}
 end{quote}
  is also called \concept{backchaining} with rule ‹xyz›.

 subsection{Introduction Rules}

  introduction (@{thm[source] conjI}) is one example of a whole
  of rules known as \conceptidx{introduction rules}{introduction rule}. They explain under which
  some logical construct can be introduced. Here are some further
  introduction rules:
 [
 inferrule*[right=\mbox{‹impI›}]{\mbox{‹?P ==> ?Q›}}{\mbox{‹?P ⟶ ?Q›}}
 qquad
 inferrule*[right=\mbox{‹allI›}]{\mbox{‹∧x. ?P x›}}{\mbox{‹∀x. ?P x›}}
 ]
 [
 inferrule*[right=\mbox{‹iffI›}]{\mbox{‹?P ==> ?Q›} \\ \mbox{‹?Q ==> ?P›}}
 {\mbox{‹?P = ?Q›}}
 ]
  rules are part of the logical system of \concept{natural deduction}
 e.g., cite‹HuthRyan›). Although we intentionally de-emphasize the basic rules
  logic in favour of automatic proof methods that allow you to take bigger
 , these rules are helpful in locating where and why automation fails.
  applied backwards, these rules decompose the goal:
 begin{itemize}
 item @{thm[source] conjI} and @{thm[source]iffI} split the goal into two subgoals,
 item @{thm[source] impI} moves the left-hand side of a HOL implication into the list of assumptions,
 item and @{thm[source] allI} removes a ‹∀› by turning the quantified variable into a fixed local variable of the subgoal.
 end{itemize}
  knows about these and a number of other introduction rules.
  command
 begin{quote}
 isacom{apply} ‹rule›\index{rule@‹rule›}
 end{quote}
  selects the appropriate rule for the current subgoal.

  can also turn your own theorems into introduction rules by giving them
  \indexed{‹intro›}{intro} attribute, analogous to the ‹simp› attribute. In
  case ‹blast›, ‹fastforce› and (to a limited extent) ‹auto› will automatically backchain with those theorems. The ‹intro›
  should be used with care because it increases the search space and
  lead to nontermination. Sometimes it is better to use it only in
  calls of ‹blast› and friends. For example,
 {thm[source] le_trans}, transitivity of ‹≤› on type typ‹nat›,
  not an introduction rule by default because of the disastrous effect
  the search space, but can be useful in specific situations:
 ›

  "[ (a::nat) ≤ b; b ≤ c; c ≤ d; d ≤ e ] ==> a ≤ e"
 (blast intro: le_trans)

 ‹
  course this is just an example and could be proved by ‹arith›, too.

 subsection{Forward Proof}
 label{sec:forward-proof}

  proof means deriving new theorems from old theorems. We have already
  a very simple form of forward proof: the ‹of› operator for
  unknowns in a theorem. The big brother of ‹of› is
 indexed{‹OF›}{OF} for applying one theorem to others. Given a theorem prop‹A ==> B› called
 ‹r› and a theorem ‹A'› called ‹r'›, the theorem ‹r[OF r']› is the result of applying ‹r› to ‹r'›, where ‹r› should be viewed as a function taking a theorem ‹A› and returning
 ‹B›. More precisely, ‹A› and ‹A'› are unified, thus
  the unknowns in ‹B›, and the result is the instantiated
 ‹B›. Of course, unification may also fail.
 begin{warn}
  of rules to other rules operates in the forward direction: from
  premises to the conclusion of the rule; application of rules to proof
  operates in the backward direction, from the conclusion to the
 .
 end{warn}

  general ‹r› can be of the form ‹[ A₁; …; A_n ] ==> A›
  there can be multiple argument theorems ‹r₁› to ‹r_m›
 with ‹m ≤ n›), in which case ‹r[OF r₁ … r_m]› is obtained
  unifying and thus proving ‹A_i› with ‹r_i›, ‹i = 1…m›.
  is an example, where @{thm[source]refl} is the theorem
 {thm[show_question_marks] refl}:
 ›

  conjI[OF refl[of "a"] refl[of "b"]]

 ‹yields the theorem @{thm conjI[OF refl[of "a"] refl[of "b"]]}.
  command \isacom{thm} merely displays the result.

  reasoning also makes sense in connection with proof states.
  ‹blast›, ‹fastforce› and ‹auto› support a modifier
 ‹dest› which instructs the proof method to use certain rules in a
  fashion. If ‹r› is of the form \mbox{‹A ==> B›}, the modifier
 mbox{‹dest: r›}\index{dest@‹dest:›}
  proof search to reason forward with ‹r›, i.e.,
  replace an assumption ‹A'›, where ‹A'› unifies with ‹A›,
  the correspondingly instantiated ‹B›. For example, @{thm[source,show_question_marks] Suc_leD} is the theorem \mbox{@{thm Suc_leD}}, which works well for forward reasoning:
 ›

  "Suc(Suc(Suc a)) ≤ b ==> a ≤ b"
 (blast dest: Suc_leD)

 ‹In this particular example we could have backchained with
 {thm[source] Suc_leD}, too, but because the premise is more complicated than the conclusion this can easily lead to nontermination.

 \subsection{Finding Theorems}
 
 Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current
 theory. Search criteria include pattern matching on terms and on names.
 For details see the Isabelle/Isar Reference Manual~cite‹IsarRef›.
 \bigskip

 begin{warn}
  ease readability we will drop the question marks
  front of unknowns from now on.
 end{warn}


 section{Inductive Definitions}
 label{sec:inductive-defs}\index{inductive definition|(}

  definitions are the third important definition facility, after
  and recursive function.
 ifsem
  fact, they are the key construct in the
  of operational semantics in the second part of the book.
 fi

 subsection{An Example: Even Numbers}
 label{sec:Logic:even}

  is a simple example of an inductively defined predicate:
 begin{itemize}
 item 0 is even
 item If $n$ is even, so is $n+2$.
 end{itemize}
  operative word ``inductive'' means that these are the only even numbers.
  Isabelle we give the two rules the names ‹ev0› and ‹evSS›
  write
 ›

  ev :: "nat → bool" where
 : "ev 0" |
evSS:  (*<*)"ev n ==> ev (Suc(Suc n))"(*>*)
text_raw‹@{prop[source]"ev n ==> ev (n + 2)"}›

text‹To get used to inductive definitions, we will first prove a few
  of const‹ev› informally before we descend to the Isabelle level.

  do we prove that some number is even, e.g., prop‹ev 4›? Simply by combining the defining rules for const‹ev›:
 begin{quote}
 ‹ev 0 ==> ev (0 + 2) ==> ev((0 + 2) + 2) = ev 4›
 end{quote}

 subsubsection{Rule Induction}\index{rule induction|(}

  that all even numbers have some property is more complicated. For
 , let us prove that the inductive definition of even numbers agrees
  the following recursive one:›

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

text‹We prove prop‹ev m ==> evn m›. That is, we
  prop‹ev m› and by induction on the form of its derivation
  prop‹evn m›. There are two cases corresponding to the two rules
  const‹ev›:
 begin{description}
 item[Case @{thm[source]ev0}:]
 prop‹ev m› was derived by rule prop‹ev 0›: \\
 ‹==>› prop‹m=(0::nat)› ‹==>› ‹evn m = evn 0 = True›
 item[Case @{thm[source]evSS}:]
 prop‹ev m› was derived by rule prop‹ev n ==> ev(n+2)›: \\
 ‹==>› prop‹m=n+(2::nat)› and by induction hypothesis prop‹evn n›\\
 ‹==>› ‹evn m = evn(n + 2) = evn n = True›
 end{description}

  we have just seen is a special case of \concept{rule induction}.
  induction applies to propositions of this form
 begin{quote}
 prop‹ev n ==> P n›
 end{quote}
  is, we want to prove a property prop‹P n›
  all even ‹n›. But if we assume prop‹ev n›, then there must be
  derivation of this assumption using the two defining rules for
 const‹ev›. That is, we must prove
 begin{description}
 item[Case @{thm[source]ev0}:] prop‹P(0::nat)›
 item[Case @{thm[source]evSS}:] prop‹[ ev n; P n ] ==> P(n + 2::nat)›
 end{description}
  corresponding rule is called @{thm[source] ev.induct} and looks like this:
 [
 inferrule{
 mbox{@{thm (prem 1) ev.induct[of "n"]}}\\
 mbox{@{thm (prem 2) ev.induct}}\\
 mbox{prop‹!!n. [ ev n; P n ] ==> P(n+2)›}}
 \mbox{@{thm (concl) ev.induct[of "n"]}}}
 ]
  first premise prop‹ev n› enforces that this rule can only be applied
  situations where we know that ‹n› is even.

  that in the induction step we may not just assume prop‹P n› but also
 mbox{prop‹ev n›}, which is simply the premise of rule @{thm[source]
 }. Here is an example where the local assumption prop‹ev n› comes in
 : we prove prop‹ev m ==> ev(m - 2)› by induction on prop‹ev m›.
  @{thm[source]ev0} requires us to prove prop‹ev(0 - 2)›, which follows
  prop‹ev 0› because prop‹0 - 2 = (0::nat)› on type typ‹nat›. In
  @{thm[source]evSS} we have \mbox{prop‹m = n+(2::nat)›} and may assume
 prop‹ev n›, which implies prop‹ev (m - 2)› because ‹m - 2 = (n +
 ) - 2 = n›. We did not need the induction hypothesis at all for this proof (it
  just a case analysis of which rule was used) but having prop‹ev n›
  our disposal in case @{thm[source]evSS} was essential.
  case analysis of rules is also called ``rule inversion''
  is discussed in more detail in \autoref{ch:Isar}.

 subsubsection{In Isabelle}

  us now recast the above informal proofs in Isabelle. For a start,
  use const‹Suc› terms instead of numerals in rule @{thm[source]evSS}:
 {thm[display] evSS}
  avoids the difficulty of unifying ‹n+2› with some numeral,
  is not automatic.

  simplest way to prove prop‹ev(Suc(Suc(Suc(Suc 0))))› is in a forward
 : ‹evSS[OF evSS[OF ev0]]› yields the theorem @{thm evSS[OF
 [OF ev0]]}. Alternatively, you can also prove it as a lemma in backwards
 . Although this is more verbose, it allows us to demonstrate how each
  application changes the proof state:›

lemma "ev(Suc(Suc(Suc(Suc 0))))"
txt‹
 {subgoals[display,indent=0,goals_limit=1]}
 ›
apply(rule evSS)
txt‹
 {subgoals[display,indent=0,goals_limit=1]}
 ›
apply(rule evSS)
txt‹
 {subgoals[display,indent=0,goals_limit=1]}
 ›
apply(rule ev0)
done

text‹\indent
  induction is applied by giving the induction rule explicitly via the
 ‹rule:› modifier:\index{inductionrule@‹induction ... rule:›}›

lemma "ev m ==> evn m"
apply(induction rule: ev.induct)
by(simp_all)

text‹Both cases are automatic. Note that if there are multiple assumptions
  the form prop‹ev t›, method ‹induction› will induct on the leftmost
 .

  a bonus, we also prove the remaining direction of the equivalence of
 const‹ev› and const‹evn›:
 ›

lemma "evn n ==> ev n"
apply(induction n rule: evn.induct)

txt‹This is a proof by computation induction on ‹n› (see
 autoref{sec:recursive-funs}) that sets up three subgoals corresponding to
  three equations for const‹evn›:
 {subgoals[display,indent=0]}
  first and third subgoals follow with @{thm[source]ev0} and @{thm[source]evSS}, and the second subgoal is trivially true because prop‹evn(Suc 0)› is const‹False›:
 ›

by (simp_all add: ev0 evSS)

text‹The rules for const‹ev› make perfect simplification and introduction
  because their premises are always smaller than the conclusion. It
  sense to turn them into simplification and introduction rules
 , to enhance proof automation. They are named @{thm[source] ev.intros}
 index{intros@‹.intros›} by Isabelle:›

declare ev.intros[simp,intro]

text‹The rules of an inductive definition are not simplification rules by
  because, in contrast to recursive functions, there is no termination
  for inductive definitions.

 subsubsection{Inductive Versus Recursive}

  have seen two definitions of the notion of evenness, an inductive and a
  one. Which one is better? Much of the time, the recursive one is
  convenient: it allows us to do rewriting in the middle of terms, and it
  both the positive information (which numbers are even) and the
  information (which numbers are not even) directly. An inductive
  only expresses the positive information directly. The negative
 , for example, that ‹1› is not even, has to be proved from
  (by induction or rule inversion). On the other hand, rule induction is
 -made for proving \mbox{prop‹ev n ==> P n›} because it only asks you
  prove the positive cases. In the proof of prop‹evn n ==> P n› by
  induction via @{thm[source]evn.induct}, we are also presented
  the trivial negative cases. If you want the convenience of both
  and rule induction, you can make two definitions and show their
  (as above) or make one definition and prove additional properties
  it, for example rule induction from computation induction.

  many concepts do not admit a recursive definition at all because there is
  datatype for the recursion (for example, the transitive closure of a
 ), or the recursion would not terminate (for example,
  interpreter for a programming language). Even if there is a recursive
 , if we are only interested in the positive information, the
  definition may be much simpler.

 subsection{The Reflexive Transitive Closure}
 label{sec:star}

  is really more conveniently expressed recursively than inductively.
  a second and very typical example of an inductive definition we define the
  transitive closure.
 ifsem
  will also be an important building block for
  of the semantics considered in the second part of the book.
 fi

  reflexive transitive closure, called ‹star› below, is a function
  maps a binary predicate to another binary predicate: if ‹r› is of
  ‹τ → τ → bool› then term‹star r› is again of type ‹τ →
 τ → bool›, and prop‹star r x y› means that ‹x› and ‹y› are in
  relation term‹star r›. Think term‹r^*› when you see term‹star
 ›, because ‹star r› is meant to be the reflexive transitive closure.
  is, prop‹star r x y› is meant to be true if from ‹x› we can
  ‹y› in finitely many ‹r› steps. This concept is naturally
  inductively:›

inductive star :: "('a → 'a → bool) → 'a → 'a → bool"  for r where
refl:  "star r x x" |
step:  "r x y ==> star r y z ==> star r x z"

text‹The base case @{thm[source] refl} is reflexivity: term‹x=y›. The
  case @{thm[source]step} combines an ‹r› step (from ‹x› to
 ‹y›) and a term‹star r› step (from ‹y› to ‹z›) into a
 term‹star r› step (from ‹x› to ‹z›).
  ``\isacom{for}~‹r›'' in the header is merely a hint to Isabelle
  ‹r› is a fixed parameter of const‹star›, in contrast to the
  parameters of const‹star›, which change. As a result, Isabelle
  a simpler induction rule.

  definition term‹star r› is reflexive. It is also transitive, but we
  rule induction to prove that:›

lemma star_trans: "star r x y ==> star r y z ==> star r x z"
apply(induction rule: star.induct)
(*<*)
defer
apply(rename_tac u x y)
defer
(*>*)
txt‹The induction is over prop‹star r x y› (the first matching assumption)
  we try to prove \mbox{prop‹star r y z ==> star r x z›},
  we abbreviate by prop‹P x y›. These are our two subgoals:
 {subgoals[display,indent=0]}
  first one is prop‹P x x›, the result of case @{thm[source]refl},
  it is trivial:\index{assumption@‹assumption›}
 ›
apply(assumption)
txt‹Let us examine subgoal ‹2›, case @{thm[source] step}.
  prop‹r u x› and \mbox{prop‹star r x y›}
  the premises of rule @{thm[source]step}.
  prop‹star r y z ==> star r x z› is \mbox{prop‹P x y›},
  IH coming from prop‹star r x y›. We have to prove prop‹P u y›,
  we do by assuming prop‹star r y z› and proving prop‹star r u z›.
  proof itself is straightforward: from \mbox{prop‹star r y z›} the IH
  to prop‹star r x z› which, together with prop‹r u x›,
  to \mbox{prop‹star r u z›} via rule @{thm[source]step}:
 ›
apply(metis step)
done

text‹\index{rule induction|)}

 subsection{The General Case}

  definitions have approximately the following general form:
 begin{quote}
 isacom{inductive} ‹I :: "τ → bool"› \isacom{where}
 end{quote}
  by a sequence of (possibly named) rules of the form
 begin{quote}
 ‹[ I a₁; …; I a_n ] ==> I a›
 end{quote}
  by ‹|›. As usual, ‹n› can be 0.
  corresponding rule induction principle
 ‹I.induct› applies to propositions of the form
 begin{quote}
 prop‹I x ==> P x›
 end{quote}
  ‹P› may itself be a chain of implications.
 begin{warn}
  induction is always on the leftmost premise of the goal.
  ‹I x› must be the first premise.
 end{warn}
  prop‹I x ==> P x› by rule induction means proving
  every rule of ‹I› that ‹P› is invariant:
 begin{quote}
 ‹[ I a₁; P a₁; …; I a_n; P a_n ] ==> P a›
 end{quote}

  above format for inductive definitions is simplified in a number of
 . ‹I› can have any number of arguments and each rule can have
  premises not involving ‹I›, so-called \conceptidx{side
 }{side condition}. In rule inductions, these side conditions appear as additional
 . The \isacom{for} clause seen in the definition of the reflexive
  closure simplifies the induction rule.
 index{inductive definition|)}

 subsection*{Exercises}

 begin{exercise}
  the following definition of palindromes
 begin{itemize}
 item The empty list and a singleton list are palindromes.
 item If ‹xs› is a palindrome, so is term‹a # xs @ [a]›.
 end{itemize}
  an inductive predicate ‹palindrome ::› typ‹'a list → bool›
  prove that prop‹rev xs = xs› if ‹xs› is a palindrome.
 end{exercise}

 exercise
  could also have defined const‹star› as follows:
 ›

inductive star' :: "('a → 'a → bool) → 'a → 'a → bool" for r where
refl': "star' r x x" |
step': "star' r x y ==> r y z ==> star' r x z"

text‹
  single ‹r› step is performed after rather than before the ‹star'›
 . Prove prop‹star' r x y ==> star r x y› and
 prop‹star r x y ==> star' r x y›. You may need lemmas.
  that rule induction fails
  the assumption about the inductive predicate is not the first assumption.
 endexercise

 begin{exercise}\label{exe:iter}
  to const‹star›, give an inductive definition of the ‹n›-fold iteration
  a relation ‹r›: term‹iter r n x y› should hold if there are ‹x₀›, \dots, ‹x_n›
  that prop‹x = x₀›, prop‹x_n = y› and ‹r x x₊₁› for
  prop‹i < n›. Correct and prove the following claim:
 prop‹star r x y ==> iter r n x y›.
 end{exercise}

 begin{exercise}\label{exe:cfg}
  context-free grammar can be seen as an inductive definition where each
  $A$ is an inductively defined predicate on lists of terminal
 : $A(w)$ means that $w$ is in the language generated by $A$.
  example, the production $S \to a S b$ can be viewed as the implication
 prop‹S w ==> S (a # w @ [b])› where ‹a› and ‹b› are terminal symbols,
 .e., elements of some alphabet. The alphabet can be defined like this:
 isacom{datatype} ‹alpha = a | b | …›

  the two grammars (where $\varepsilon$ is the empty word)
 [
 begin{array}{r@ {\quad}c@ {\quad}l}
  &\to& \varepsilon \quad\mid\quad aSb \quad\mid\quad SS \\
  &\to& \varepsilon \quad\mid\quad TaTb
 end{array}
 ]
  two inductive predicates.
  you think of ‹a› and ‹b› as ``‹(›'' and ``‹)›'',
  grammars define balanced strings of parentheses.
  prop‹T w ==> S w› and \mbox{prop‹S w ==> T w›} separately and conclude
 prop‹S w = T w›.
 end{exercise}

 ifsem
 begin{exercise}
  \autoref{sec:AExp} we defined a recursive evaluation function
 ‹aval :: aexp → state → val›.
  an inductive evaluation predicate
 ‹aval_rel :: aexp → state → val → bool›
  prove that it agrees with the recursive function:
 prop‹aval_rel a s v ==> aval a s = v›,
 prop‹aval a s = v ==> aval_rel a s v› and thus
 noquotes{@{prop [source] "aval_rel a s v ⟷ aval a s = v"}}.
 end{exercise}

 begin{exercise}
  the stack machine from Chapter~3
  recall the concept of \concept{stack underflow}
  Exercise~\ref{exe:stack-underflow}.
  an inductive predicate
 ‹ok :: nat → instr list → nat → bool›
  that ‹ok n is n'› means that with any initial stack of length
 ‹n› the instructions ‹is› can be executed
  stack underflow and that the final stack has length ‹n'›.
  that ‹ok› correctly computes the final stack size
 {prop[display] "[ok n is n'; length stk = n] ==> length (exec is s stk) = n'"}
  that instruction sequences generated by ‹comp›
  cause stack underflow: \ ‹ok n (comp a) ?› \ for
  suitable value of ‹?›.
 end{exercise}
 fi
 ›
(*<*)
end
(*>*)