Quelle  ToyList.thy

theory ToyList
imports Main
begin

text‹\noindent
  already has a predefined theory of lists called ‹List› ---
 ‹ToyList› is merely a small fragment of it chosen as an example.
  avoid some ambiguities caused by defining lists twice, we manipulate
  concrete syntax and name space of theory 🍋‹Main› as follows.
 ›

unbundle no list_syntax
no_notation append  (infixr "@" 65)
hide_type list
hide_const rev

datatype 'a list = Nil                          ("[]")
                 | Cons 'a "'a list"            (infixr "#" 65)

text‹\noindent
  datatype\index{datatype@\isacommand {datatype} (command)}
 tydx{list} introduces two
  \cdx{Nil} and \cdx{Cons}, the
 ~list and the operator that adds an element to the front of a list. For
 , the term \isa{Cons True (Cons False Nil)} is a value of
  🍋‹bool list›, namely the list with the elements term‹True› and
 term‹False›. Because this notation quickly becomes unwieldy, the
  declaration is annotated with an alternative syntax: instead of
 {term[source]Nil} and \isa{Cons x xs} we can write
 term‹[]›\index{$HOL2list@\isa{[]}|bold} and
 term‹x # xs›\index{$HOL2list@\isa{\#}|bold}. In fact, this
  syntax is the familiar one. Thus the list \isa{Cons True
 Cons False Nil)} becomes term‹True # False # []›. The annotation
 isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)}
  that ‹#› associates to
  right: the term term‹x # y # z› is read as ‹x # (y # z)›
  not as ‹(x # y) # z›.
  ‹65› is the priority of the infix ‹#›.

 begin{warn}
 Syntax annotations can be powerful, but they are difficult to master and
 are never necessary. You
 could drop them from theory ‹ToyList› and go back to the identifiers
 @{term[source]Nil} and @{term[source]Cons}. Novices should avoid using
 syntax annotations in their own theories.
 end{warn}
 , two functions ‹app› and \cdx{rev} are defined recursively,
  this order, because Isabelle insists on definition before use:
 ›

primrec app :: "'a list ==> 'a list ==> 'a list" (infixr "@" 65) where
"[] @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"

primrec rev :: "'a list ==> 'a list" where
"rev [] = []" |
"rev (x # xs) = (rev xs) @ (x # [])"

text‹\noindent
  function definition is of the form
 begin{center}
 isacommand{primrec} \textit{name} ‹::› \textit{type} \textit{(optional syntax)} \isakeyword{where} \textit{equations}
 end{center}
  equations must be separated by ‹|›.
 
  ‹app› is annotated with concrete syntax. Instead of the
  syntax ‹app xs ys› the infix
 term‹xs @ ys›\index{$HOL2list@\isa{\at}|bold} becomes the preferred
 .

 index{*rev (constant)|(}\index{append function|(}
  equations for ‹app› and term‹rev› hardly need comments:
 ‹app› appends two lists and term‹rev› reverses a list. The
  \commdx{primrec} indicates that the recursion is
  a particularly primitive kind where each recursive call peels off a datatype
  from one of the arguments. Thus the
  always terminates, i.e.\ the function is \textbf{total}.
 index{functions!total}

  termination requirement is absolutely essential in HOL, a logic of total
 . If we were to drop it, inconsistencies would quickly arise: the
 `definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
 f(n)$ on both sides.
  However, this is a subtle issue that we cannot discuss here further.

 begin{warn}
 As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
 because of totality that reasoning in HOL is comparatively easy. More
 generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
 function definitions whose totality has not been proved) because they
 quickly lead to inconsistencies. Instead, fixed constructs for introducing
 types and functions are offered (such as \isacommand{datatype} and
 \isacommand{primrec}) which are guaranteed to preserve consistency.
 end{warn}

 index{syntax}%
  remark about syntax. The textual definition of a theory follows a fixed
  with keywords like \isacommand{datatype} and \isacommand{end}.
  (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
  in this syntax are the types and formulae of HOL, whose syntax is
  (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators.
  distinguish the two levels, everything
 -specific (terms and types) should be enclosed in
 texttt{"}\dots\texttt{"}.
  lessen this burden, quotation marks around a single identifier can be
 , unless the identifier happens to be a keyword, for example
 isa{"end"}.
  Isabelle prints a syntax error message, it refers to the HOL syntax as
  \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.

 \index{comment} must be in enclosed in \texttt{(*}and\texttt{*)}.

 section{Evaluation}
 index{evaluation}

  you have processed the declarations and definitions of
 texttt{ToyList} presented so far, you may want to test your
  by running them. For example, what is the value of
 term‹rev(True#False#[])›? Command
 ›

value "rev (True # False # [])"

text‹\noindent yields the correct result term‹False # True # []›.
  we can go beyond mere functional programming and evaluate terms with
  in them, executing functions symbolically:›

value "rev (a # b # c # [])"

text‹\noindent yields term‹c # b # a # []›.

 section{An Introductory Proof}
 label{sec:intro-proof}

  convinced ourselves (as well as one can by testing) that our
  capture our intentions, we are ready to prove a few simple
 . This will illustrate not just the basic proof commands but
  the typical proof process.

 subsubsection*{Main Goal.}

  goal is to show that reversing a list twice produces the original
 .
 ›

theorem rev_rev [simp]: "rev(rev xs) = xs"

txt‹\index{theorem@\isacommand {theorem} (command)|bold}%
 noindent
  \isacommand{theorem} command does several things:
 begin{itemize}
 item
  establishes a new theorem to be proved, namely prop‹rev(rev xs) = xs›.
 item
  gives that theorem the name ‹rev_rev›, for later reference.
 item
  tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
  will replace occurrences of term‹rev(rev xs)› by
 term‹xs›.
 end{itemize}
  name and the simplification attribute are optional.
 's response is to print the initial proof state consisting
  some header information (like how many subgoals there are) followed by
 {subgoals[display,indent=0]}
  compactness reasons we omit the header in this tutorial.
  we have finished a proof, the \rmindex{proof state} proper
  looks like this:
 begin{isabelle}
 1.~$G\sb{1}$\isanewline
 ~\vdots~~\isanewline
 $n$.~$G\sb{n}$
 end{isabelle}
  numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$
  we need to prove to establish the main goal.\index{subgoals}
  there is only one subgoal, which is identical with the
  goal. (If you always want to see the main goal as well,
  the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)}
 -- this flag used to be set by default.)

  us now get back to prop‹rev(rev xs) = xs›. Properties of recursively
  functions are best established by induction. In this case there is
  obvious except induction on term‹xs›:
 ›

apply(induct_tac xs)

txt‹\noindent\index{*induct_tac (method)}%
  tells Isabelle to perform induction on variable term‹xs›. The suffix
 term‹tac› stands for \textbf{tactic},\index{tactics}
  synonym for ``theorem proving function''.
  default, induction acts on the first subgoal. The new proof state contains
  subgoals, namely the base case (@{term[source]Nil}) and the induction step
 @{term[source]Cons}):
 {subgoals[display,indent=0,margin=65]}

  induction step is an example of the general format of a subgoal:\index{subgoals}
 begin{isabelle}
 $i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
 end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
  prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
  most of the time, or simply treated as a list of variables local to
  subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
  {\it assumptions}\index{assumptions!of subgoal}
  the local assumptions for this subgoal and {\it
 conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved.
  proof steps
  add new assumptions are induction and case distinction. In our example
  only assumption is the induction hypothesis term‹rev (rev list) =
 list›, where term‹list› is a variable name chosen by Isabelle. If there
  multiple assumptions, they are enclosed in the bracket pair
 indexboldpos{\isasymlbrakk}{$Isabrl} and
 indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.

  us try to solve both goals automatically:
 ›

apply(auto)

txt‹\noindent
  command tells Isabelle to apply a proof strategy called
 ‹auto› to all subgoals. Essentially, ‹auto› tries to
  the subgoals. In our case, subgoal~1 is solved completely (thanks
  the equation prop‹rev [] = []›) and disappears; the simplified version
  subgoal~2 becomes the new subgoal~1:
 {subgoals[display,indent=0,margin=70]}
  order to simplify this subgoal further, a lemma suggests itself.
 ›
(*<*)
oops
(*>*)

subsubsection‹First Lemma›

text‹
 indexbold{abandoning a proof}\indexbold{proofs!abandoning}
  abandoning the above proof attempt (at the shell level type
 commdx{oops}) we start a new proof:
 ›

lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"

txt‹\noindent The keywords \commdx{theorem} and
 commdx{lemma} are interchangeable and merely indicate
  importance we attach to a proposition. Therefore we use the words
 emph{theorem} and \emph{lemma} pretty much interchangeably, too.

  are two variables that we could induct on: term‹xs› and
 term‹ys›. Because ‹@› is defined by recursion on
  first argument, term‹xs› is the correct one:
 ›

apply(induct_tac xs)

txt‹\noindent
  time not even the base case is solved automatically:
 ›

apply(auto)

txt‹
 {subgoals[display,indent=0,goals_limit=1]}
 , we need to abandon this proof attempt and prove another simple lemma
 . In the future the step of abandoning an incomplete proof before
  on the proof of a lemma usually remains implicit.
 ›
(*<*)
oops
(*>*)

subsubsection‹Second Lemma›

text‹
  again try the canonical proof procedure:
 ›

lemma app_Nil2 [simp]: "xs @ [] = xs"
apply(induct_tac xs)
apply(auto)

txt‹
 noindent
  works, yielding the desired message ‹No subgoals!›:
 {goals[display,indent=0]}
  still need to confirm that the proof is now finished:
 ›

done

text‹\noindent
  a result of that final \commdx{done}, Isabelle associates the lemma just proved
  its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
  it is obvious from the context that the proof is finished.

  Instead of \isacommand{apply} followed by a dot, you can simply write
  \isacommand{by}\indexbold{by}, which we do most of the time.
  that in lemma @{thm[source]app_Nil2},
  printed out after the final \isacommand{done}, the free variable term‹xs› has been
  by the unknown ‹?xs›, just as explained in
 S\ref{sec:variables}.

  back to the proof of the first lemma
 ›

lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
apply(induct_tac xs)
apply(auto)

txt‹
 noindent
  find that this time ‹auto› solves the base case, but the
  step merely simplifies to
 {subgoals[display,indent=0,goals_limit=1]}
  we need to remember that ‹@› associates to the right, and that
 ‹#› and ‹@› have the same priority (namely the ‹65›
  their \isacommand{infixr} annotation). Thus the conclusion really is
 begin{isabelle}
 ~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
 end{isabelle}
  the missing lemma is associativity of ‹@›.
 ›
(*<*)oops(*>*)

subsubsection‹Third Lemma›

text‹
  the previous attempt, the canonical proof procedure
  without further ado.
 ›

lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
apply(induct_tac xs)
apply(auto)
done

text‹
 noindent
  we can prove the first lemma:
 ›

lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
apply(induct_tac xs)
apply(auto)
done

text‹\noindent
 , we prove our main theorem:
 ›

theorem rev_rev [simp]: "rev(rev xs) = xs"
apply(induct_tac xs)
apply(auto)
done

text‹\noindent
  final \commdx{end} tells Isabelle to close the current theory because
  are finished with its development:%
 index{*rev (constant)|)}\index{append function|)}
 ›

end