src/Doc/Prog_Prove/Bool_nat_list.thy

 begin
 (*>*)
 
 text\<open>
 \vspace{-4ex}
-\section{\texorpdfstring{Types @{typ bool}, @{typ nat} and @{text list}}{Types bool, nat and list}}
+\section{\texorpdfstring{Types @{typ bool}, @{typ nat} and \<open>list\<close>}{Types bool, nat and list}}
 
 These are the most important predefined types. We go through them one by one.
 Based on examples we learn how to define (possibly recursive) functions and
 prove theorems about them by induction and simplification.
 
 \subsection{Type \indexed{@{typ bool}}{bool}}
 
 The type of boolean values is a predefined datatype
 @{datatype[display] bool}
 with the two values \indexed{@{const True}}{True} and \indexed{@{const False}}{False} and
-with many predefined functions:  @{text "\<not>"}, @{text "\<and>"}, @{text "\<or>"}, @{text
-"\<longrightarrow>"}, etc. Here is how conjunction could be defined by pattern matching:
+with many predefined functions:  \<open>\<not>\<close>, \<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<longrightarrow>\<close>, etc. Here is how conjunction could be defined by pattern matching:
 \<close>
 
 fun conj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
 "conj True True = True" |
 "conj _ _ = False"

 \subsection{Type \indexed{@{typ nat}}{nat}}
 
 Natural numbers are another predefined datatype:
 @{datatype[display] nat}\index{Suc@@{const Suc}}
 All values of type @{typ nat} are generated by the constructors
-@{text 0} and @{const Suc}. Thus the values of type @{typ nat} are
-@{text 0}, @{term"Suc 0"}, @{term"Suc(Suc 0)"}, etc.
-There are many predefined functions: @{text "+"}, @{text "*"}, @{text
-"\<le>"}, etc. Here is how you could define your own addition:
+\<open>0\<close> and @{const Suc}. Thus the values of type @{typ nat} are
+\<open>0\<close>, @{term"Suc 0"}, @{term"Suc(Suc 0)"}, etc.
+There are many predefined functions: \<open>+\<close>, \<open>*\<close>, \<open>\<le>\<close>, etc. Here is how you could define your own addition:
 \<close>
 
 fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 "add 0 n = n" |
 "add (Suc m) n = Suc(add m n)"

 (*<*)
 lemma "add m 0 = m"
 apply(induction m)
 (*>*)
 txt\<open>The \isacom{lemma} command starts the proof and gives the lemma
-a name, @{text add_02}. Properties of recursively defined functions
+a name, \<open>add_02\<close>. Properties of recursively defined functions
 need to be established by induction in most cases.
-Command \isacom{apply}@{text"(induction m)"} instructs Isabelle to
-start a proof by induction on @{text m}. In response, it will show the
+Command \isacom{apply}\<open>(induction m)\<close> instructs Isabelle to
+start a proof by induction on \<open>m\<close>. In response, it will show the
 following proof state\ifsem\footnote{See page \pageref{proof-state} for how to
 display the proof state.}\fi:
 @{subgoals[display,indent=0]}
 The numbered lines are known as \emph{subgoals}.
 The first subgoal is the base case, the second one the induction step.
-The prefix @{text"\<And>m."} is Isabelle's way of saying ``for an arbitrary but fixed @{text m}''. The @{text"\<Longrightarrow>"} separates assumptions from the conclusion.
-The command \isacom{apply}@{text"(auto)"} instructs Isabelle to try
+The prefix \<open>\<And>m.\<close> is Isabelle's way of saying ``for an arbitrary but fixed \<open>m\<close>''. The \<open>\<Longrightarrow>\<close> separates assumptions from the conclusion.
+The command \isacom{apply}\<open>(auto)\<close> instructs Isabelle to try
 and prove all subgoals automatically, essentially by simplifying them.
 Because both subgoals are easy, Isabelle can do it.
 The base case @{prop"add 0 0 = 0"} holds by definition of @{const add},
 and the induction step is almost as simple:
-@{text"add\<^latex>\<open>~\<close>(Suc m) 0 = Suc(add m 0) = Suc m"}
+\<open>add\<^latex>\<open>~\<close>(Suc m) 0 = Suc(add m 0) = Suc m\<close>
 using first the definition of @{const add} and then the induction hypothesis.
 In summary, both subproofs rely on simplification with function definitions and
 the induction hypothesis.
 As a result of that final \isacom{done}, Isabelle associates the lemma
 just proved with its name. You can now inspect the lemma with the command
 \<close>
 
 thm add_02
 
 txt\<open>which displays @{thm[show_question_marks,display] add_02} The free
-variable @{text m} has been replaced by the \concept{unknown}
-@{text"?m"}. There is no logical difference between the two but there is an
+variable \<open>m\<close> has been replaced by the \concept{unknown}
+\<open>?m\<close>. There is no logical difference between the two but there is an
 operational one: unknowns can be instantiated, which is what you want after
 some lemma has been proved.
 
-Note that there is also a proof method @{text induct}, which behaves almost
-like @{text induction}; the difference is explained in \autoref{ch:Isar}.
+Note that there is also a proof method \<open>induct\<close>, which behaves almost
+like \<open>induction\<close>; the difference is explained in \autoref{ch:Isar}.
 
 \begin{warn}
 Terminology: We use \concept{lemma}, \concept{theorem} and \concept{rule}
 interchangeably for propositions that have been proved.
 \end{warn}
 \begin{warn}
-  Numerals (@{text 0}, @{text 1}, @{text 2}, \dots) and most of the standard
-  arithmetic operations (@{text "+"}, @{text "-"}, @{text "*"}, @{text"\<le>"},
-  @{text"<"}, etc.) are overloaded: they are available
+  Numerals (\<open>0\<close>, \<open>1\<close>, \<open>2\<close>, \dots) and most of the standard
+  arithmetic operations (\<open>+\<close>, \<open>-\<close>, \<open>*\<close>, \<open>\<le>\<close>,
+  \<open><\<close>, etc.) are overloaded: they are available
   not just for natural numbers but for other types as well.
-  For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate
+  For example, given the goal \<open>x + 0 = x\<close>, there is nothing to indicate
   that you are talking about natural numbers. Hence Isabelle can only infer
-  that @{term x} is of some arbitrary type where @{text 0} and @{text"+"}
+  that @{term x} is of some arbitrary type where \<open>0\<close> and \<open>+\<close>
   exist. As a consequence, you will be unable to prove the goal.
 %  To alert you to such pitfalls, Isabelle flags numerals without a
 %  fixed type in its output: @ {prop"x+0 = x"}.
   In this particular example, you need to include
-  an explicit type constraint, for example @{text"x+0 = (x::nat)"}. If there
+  an explicit type constraint, for example \<open>x+0 = (x::nat)\<close>. If there
   is enough contextual information this may not be necessary: @{prop"Suc x =
-  x"} automatically implies @{text"x::nat"} because @{term Suc} is not
+  x"} automatically implies \<open>x::nat\<close> because @{term Suc} is not
   overloaded.
 \end{warn}
 
 \subsubsection{An Informal Proof}
 

 
 \noindent
 \textbf{Lemma} @{prop"add m 0 = m"}
 
 \noindent
-\textbf{Proof} by induction on @{text m}.
+\textbf{Proof} by induction on \<open>m\<close>.
 \begin{itemize}
-\item Case @{text 0} (the base case): @{prop"add 0 0 = 0"}
+\item Case \<open>0\<close> (the base case): @{prop"add 0 0 = 0"}
   holds by definition of @{const add}.
 \item Case @{term"Suc m"} (the induction step):
   We assume @{prop"add m 0 = m"}, the induction hypothesis (IH),
-  and we need to show @{text"add (Suc m) 0 = Suc m"}.
+  and we need to show \<open>add (Suc m) 0 = Suc m\<close>.
   The proof is as follows:\smallskip
 
   \begin{tabular}{@ {}rcl@ {\quad}l@ {}}
-  @{term "add (Suc m) 0"} &@{text"="}& @{term"Suc(add m 0)"}
-  & by definition of @{text add}\\
-              &@{text"="}& @{term "Suc m"} & by IH
+  @{term "add (Suc m) 0"} &\<open>=\<close>& @{term"Suc(add m 0)"}
+  & by definition of \<open>add\<close>\\
+              &\<open>=\<close>& @{term "Suc m"} & by IH
   \end{tabular}
 \end{itemize}
 Throughout this book, \concept{IH} will stand for ``induction hypothesis''.
 
 We have now seen three proofs of @{prop"add m 0 = 0"}: the Isabelle one, the

 as informal text comprehensible to a reader familiar with traditional
 mathematical proofs. Later on we will introduce an Isabelle proof language
 that is closer to traditional informal mathematical language and is often
 directly readable.
 
-\subsection{Type \indexed{@{text list}}{list}}
+\subsection{Type \indexed{\<open>list\<close>}{list}}
 
 Although lists are already predefined, we define our own copy for
 demonstration purposes:
 \<close>
 (*<*)

 
 fun rev :: "'a list \<Rightarrow> 'a list" where
 "rev Nil = Nil" |
 "rev (Cons x xs) = app (rev xs) (Cons x Nil)"
 
-text\<open>By default, variables @{text xs}, @{text ys} and @{text zs} are of
-@{text list} type.
+text\<open>By default, variables \<open>xs\<close>, \<open>ys\<close> and \<open>zs\<close> are of
+\<open>list\<close> type.
 
 Command \indexed{\isacommand{value}}{value} evaluates a term. For example,\<close>
 
 value "rev(Cons True (Cons False Nil))"
 

 
 text\<open>yields @{value "rev(Cons a (Cons b Nil))"}.
 \medskip
 
 Figure~\ref{fig:MyList} shows the theory created so far.
-Because @{text list}, @{const Nil}, @{const Cons}, etc.\ are already predefined,
- Isabelle prints qualified (long) names when executing this theory, for example, @{text MyList.Nil}
+Because \<open>list\<close>, @{const Nil}, @{const Cons}, etc.\ are already predefined,
+ Isabelle prints qualified (long) names when executing this theory, for example, \<open>MyList.Nil\<close>
  instead of @{const Nil}.
  To suppress the qualified names you can insert the command
  \texttt{declare [[names\_short]]}.
  This is not recommended in general but is convenient for this unusual example.
 % Notice where the

 \subsubsection{Structural Induction for Lists}
 
 Just as for natural numbers, there is a proof principle of induction for
 lists. Induction over a list is essentially induction over the length of
 the list, although the length remains implicit. To prove that some property
-@{text P} holds for all lists @{text xs}, i.e., \mbox{@{prop"P(xs)"}},
+\<open>P\<close> holds for all lists \<open>xs\<close>, i.e., \mbox{@{prop"P(xs)"}},
 you need to prove
 \begin{enumerate}
 \item the base case @{prop"P(Nil)"} and
-\item the inductive case @{prop"P(Cons x xs)"} under the assumption @{prop"P(xs)"}, for some arbitrary but fixed @{text x} and @{text xs}.
+\item the inductive case @{prop"P(Cons x xs)"} under the assumption @{prop"P(xs)"}, for some arbitrary but fixed \<open>x\<close> and \<open>xs\<close>.
 \end{enumerate}
 This is often called \concept{structural induction} for lists.
 
 \subsection{The Proof Process}
 

 
 theorem rev_rev [simp]: "rev(rev xs) = xs"
 
 txt\<open>Commands \isacom{theorem} and \isacom{lemma} are
 interchangeable and merely indicate the importance we attach to a
-proposition. Via the bracketed attribute @{text simp} we also tell Isabelle
+proposition. Via the bracketed attribute \<open>simp\<close> we also tell Isabelle
 to make the eventual theorem a \conceptnoidx{simplification rule}: future proofs
 involving simplification will replace occurrences of @{term"rev(rev xs)"} by
 @{term"xs"}. The proof is by induction:\<close>
 
 apply(induction xs)

 (*<*)
 oops
 (*>*)
 lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"
 
-txt\<open>There are two variables that we could induct on: @{text xs} and
-@{text ys}. Because @{const app} is defined by recursion on
-the first argument, @{text xs} is the correct one:
+txt\<open>There are two variables that we could induct on: \<open>xs\<close> and
+\<open>ys\<close>. Because @{const app} is defined by recursion on
+the first argument, \<open>xs\<close> is the correct one:
 \<close>
 
 apply(induction xs)
 
 txt\<open>This time not even the base case is solved automatically:\<close>

 lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"
 apply(induction xs)
 apply(auto)
 
 txt\<open>
-We find that this time @{text"auto"} solves the base case, but the
+We find that this time \<open>auto\<close> solves the base case, but the
 induction step merely simplifies to
 @{subgoals[display,indent=0,goals_limit=1]}
 The missing lemma is associativity of @{const app},
-which we insert in front of the failed lemma @{text rev_app}.
+which we insert in front of the failed lemma \<open>rev_app\<close>.
 
 \subsubsection{Associativity of @{const app}}
 
 The canonical proof procedure succeeds without further ado:
 \<close>

 
 \noindent
 \textbf{Lemma} @{prop"app (app xs ys) zs = app xs (app ys zs)"}
 
 \noindent
-\textbf{Proof} by induction on @{text xs}.
+\textbf{Proof} by induction on \<open>xs\<close>.
 \begin{itemize}
-\item Case @{text Nil}: \ @{prop"app (app Nil ys) zs = app ys zs"} @{text"="}
-  \mbox{@{term"app Nil (app ys zs)"}} \ holds by definition of @{text app}.
-\item Case @{text"Cons x xs"}: We assume
-  \begin{center} \hfill @{term"app (app xs ys) zs"} @{text"="}
+\item Case \<open>Nil\<close>: \ @{prop"app (app Nil ys) zs = app ys zs"} \<open>=\<close>
+  \mbox{@{term"app Nil (app ys zs)"}} \ holds by definition of \<open>app\<close>.
+\item Case \<open>Cons x xs\<close>: We assume
+  \begin{center} \hfill @{term"app (app xs ys) zs"} \<open>=\<close>
   @{term"app xs (app ys zs)"} \hfill (IH) \end{center}
   and we need to show
   \begin{center} @{prop"app (app (Cons x xs) ys) zs = app (Cons x xs) (app ys zs)"}.\end{center}
   The proof is as follows:\smallskip
 
   \begin{tabular}{@ {}l@ {\quad}l@ {}}
   @{term"app (app (Cons x xs) ys) zs"}\\
-  @{text"= app (Cons x (app xs ys)) zs"} & by definition of @{text app}\\
-  @{text"= Cons x (app (app xs ys) zs)"} & by definition of @{text app}\\
-  @{text"= Cons x (app xs (app ys zs))"} & by IH\\
-  @{text"= app (Cons x xs) (app ys zs)"} & by definition of @{text app}
+  \<open>= app (Cons x (app xs ys)) zs\<close> & by definition of \<open>app\<close>\\
+  \<open>= Cons x (app (app xs ys) zs)\<close> & by definition of \<open>app\<close>\\
+  \<open>= Cons x (app xs (app ys zs))\<close> & by IH\\
+  \<open>= app (Cons x xs) (app ys zs)\<close> & by definition of \<open>app\<close>
   \end{tabular}
 \end{itemize}
 \medskip
 
 \noindent Didn't we say earlier that all proofs are by simplification? But
 in both cases, going from left to right, the last equality step is not a
 simplification at all! In the base case it is @{prop"app ys zs = app Nil (app
 ys zs)"}. It appears almost mysterious because we suddenly complicate the
-term by appending @{text Nil} on the left. What is really going on is this:
-when proving some equality \mbox{@{prop"s = t"}}, both @{text s} and @{text t} are
+term by appending \<open>Nil\<close> on the left. What is really going on is this:
+when proving some equality \mbox{@{prop"s = t"}}, both \<open>s\<close> and \<open>t\<close> are
 simplified until they ``meet in the middle''. This heuristic for equality proofs
 works well for a functional programming context like ours. In the base case
 both @{term"app (app Nil ys) zs"} and @{term"app Nil (app
 ys zs)"} are simplified to @{term"app ys zs"}, the term in the middle.
 

 \label{sec:predeflists}
 
 Isabelle's predefined lists are the same as the ones above, but with
 more syntactic sugar:
 \begin{itemize}
-\item @{text "[]"} is \indexed{@{const Nil}}{Nil},
+\item \<open>[]\<close> is \indexed{@{const Nil}}{Nil},
 \item @{term"x # xs"} is @{term"Cons x xs"}\index{Cons@@{const Cons}},
-\item @{text"[x\<^sub>1, \<dots>, x\<^sub>n]"} is @{text"x\<^sub>1 # \<dots> # x\<^sub>n # []"}, and
+\item \<open>[x\<^sub>1, \<dots>, x\<^sub>n]\<close> is \<open>x\<^sub>1 # \<dots> # x\<^sub>n # []\<close>, and
 \item @{term "xs @ ys"} is @{term"app xs ys"}.
 \end{itemize}
 There is also a large library of predefined functions.
 The most important ones are the length function
-@{text"length :: 'a list \<Rightarrow> nat"}\index{length@@{const length}} (with the obvious definition),
+\<open>length :: 'a list \<Rightarrow> nat\<close>\index{length@@{const length}} (with the obvious definition),
 and the \indexed{@{const map}}{map} function that applies a function to all elements of a list:
 \begin{isabelle}
-\isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"} \isacom{where}\\
-@{text"\""}@{thm list.map(1) [of f]}@{text"\" |"}\\
-@{text"\""}@{thm list.map(2) [of f x xs]}@{text"\""}
+\isacom{fun} @{const map} \<open>::\<close> @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"} \isacom{where}\\
+\<open>"\<close>@{thm list.map(1) [of f]}\<open>" |\<close>\\
+\<open>"\<close>@{thm list.map(2) [of f x xs]}\<open>"\<close>
 \end{isabelle}
 
 \ifsem
 Also useful are the \concept{head} of a list, its first element,
 and the \concept{tail}, the rest of the list:
 \begin{isabelle}\index{hd@@{const hd}}
-\isacom{fun} @{text"hd :: 'a list \<Rightarrow> 'a"}\\
+\isacom{fun} \<open>hd :: 'a list \<Rightarrow> 'a\<close>\\
 @{prop"hd(x#xs) = x"}
 \end{isabelle}
 \begin{isabelle}\index{tl@@{const tl}}
-\isacom{fun} @{text"tl :: 'a list \<Rightarrow> 'a list"}\\
-@{prop"tl [] = []"} @{text"|"}\\
+\isacom{fun} \<open>tl :: 'a list \<Rightarrow> 'a list\<close>\\
+@{prop"tl [] = []"} \<open>|\<close>\\
 @{prop"tl(x#xs) = xs"}
 \end{isabelle}
 Note that since HOL is a logic of total functions, @{term"hd []"} is defined,
 but we do not know what the result is. That is, @{term"hd []"} is not undefined
 but underdefined.

 \end{exercise}
 
 \begin{exercise}
 Start from the definition of @{const add} given above.
 Prove that @{const add} is associative and commutative.
-Define a recursive function @{text double} @{text"::"} @{typ"nat \<Rightarrow> nat"}
+Define a recursive function \<open>double\<close> \<open>::\<close> @{typ"nat \<Rightarrow> nat"}
 and prove @{prop"double m = add m m"}.
 \end{exercise}
 
 \begin{exercise}
-Define a function @{text"count ::"} @{typ"'a \<Rightarrow> 'a list \<Rightarrow> nat"}
+Define a function \<open>count ::\<close> @{typ"'a \<Rightarrow> 'a list \<Rightarrow> nat"}
 that counts the number of occurrences of an element in a list. Prove
 @{prop"count x xs \<le> length xs"}.
 \end{exercise}
 
 \begin{exercise}
-Define a recursive function @{text "snoc ::"} @{typ"'a list \<Rightarrow> 'a \<Rightarrow> 'a list"}
-that appends an element to the end of a list. With the help of @{text snoc}
-define a recursive function @{text "reverse ::"} @{typ"'a list \<Rightarrow> 'a list"}
+Define a recursive function \<open>snoc ::\<close> @{typ"'a list \<Rightarrow> 'a \<Rightarrow> 'a list"}
+that appends an element to the end of a list. With the help of \<open>snoc\<close>
+define a recursive function \<open>reverse ::\<close> @{typ"'a list \<Rightarrow> 'a list"}
 that reverses a list. Prove @{prop"reverse(reverse xs) = xs"}.
 \end{exercise}
 
 \begin{exercise}
-Define a recursive function @{text "sum_upto ::"} @{typ"nat \<Rightarrow> nat"} such that
-\mbox{@{text"sum_upto n"}} @{text"="} @{text"0 + ... + n"} and prove
+Define a recursive function \<open>sum_upto ::\<close> @{typ"nat \<Rightarrow> nat"} such that
+\mbox{\<open>sum_upto n\<close>} \<open>=\<close> \<open>0 + ... + n\<close> and prove
 @{prop" sum_upto (n::nat) = n * (n+1) div 2"}.
 \end{exercise}
 \<close>
 (*<*)
 end