(*<*)
theory Bool_nat_list
imports Complex_Main
begin
(*>*)

text‹
 vspace{-4ex}
 section{\texorpdfstring{Types typ‹bool›, typ‹nat› and ‹list›}{Types bool, nat and list}}

  are the most important predefined types. We go through them one by one.
  on examples we learn how to define (possibly recursive) functions and
  theorems about them by induction and simplification.

 subsection{Type \indexed{typ‹bool›}{bool}}

  type of boolean values is a predefined datatype
 {datatype[display] bool}
  the two values \indexed{const‹True›}{True} and \indexed{const‹False›}{False} and
  many predefined functions: ‹¬›, ‹∧›, ‹∨›, ‹⟶›, etc. Here is how conjunction could be defined by pattern matching:
 ›

fun conj :: "bool → bool → bool" where
"conj True True = True" |
"conj _ _ = False"

text‹Both the datatype and function definitions roughly follow the syntax
  functional programming languages.

 subsection{Type \indexed{typ‹nat›}{nat}}

  numbers are another predefined datatype:
 {datatype[display] nat}\index{Suc@const‹Suc›}
  values of type typ‹nat› are generated by the constructors
 ‹0› and const‹Suc›. Thus the values of type typ‹nat› are
 ‹0›, term‹Suc 0›, term‹Suc(Suc 0)›, etc.
  are many predefined functions: ‹+›, ‹*›, ‹≤›, etc. Here is how you could define your own addition:
 ›

fun add :: "nat → nat → nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)"

text‹And here is a proof of the fact that prop‹add m 0 = m›:›

lemma add_02: "add m 0 = m"
apply(induction m)
apply(auto)
done
(*<*)
lemma "add m 0 = m"
apply(induction m)
(*>*)
txt‹The \isacom{lemma} command starts the proof and gives the lemma
  name, ‹add_02›. Properties of recursively defined functions
  to be established by induction in most cases.
  \isacom{apply}‹(induction m)› instructs Isabelle to
  a proof by induction on ‹m›. In response, it will show the
  proof state\ifsem\footnote{See page \pageref{proof-state} for how to
  the proof state.}\fi:
 {subgoals[display,indent=0]}
  numbered lines are known as \emph{subgoals}.
  first subgoal is the base case, the second one the induction step.
  prefix ‹∧m.› is Isabelle's way of saying ``for an arbitrary but fixed ‹m›''. The ‹==>› separates assumptions from the conclusion.
  command \isacom{apply}‹(auto)› instructs Isabelle to try
  prove all subgoals automatically, essentially by simplifying them.
  both subgoals are easy, Isabelle can do it.
  base case prop‹add 0 0 = 0› holds by definition of const‹add›,
  the induction step is almost as simple:
 ‹add🚫‹~›(Suc m) 0 = Suc(add m 0) = Suc m›
  first the definition of const‹add› and then the induction hypothesis.
  summary, both subproofs rely on simplification with function definitions and
  induction hypothesis.
  a result of that final \isacom{done}, Isabelle associates the lemma
  proved with its name. You can now inspect the lemma with the command
 ›

thm add_02

txt‹which displays @{thm[show_question_marks,display] add_02} The free
  ‹m› has been replaced by the \concept{unknown}
 ‹?m›. There is no logical difference between the two but there is an
  one: unknowns can be instantiated, which is what you want after
  lemma has been proved.

  that there is also a proof method ‹induct›, which behaves almost
  ‹induction›; the difference is explained in \autoref{ch:Isar}.

 begin{warn}
 : We use \concept{lemma}, \concept{theorem} and \concept{rule}
  for propositions that have been proved.
 end{warn}
 begin{warn}
 Numerals (‹0›, ‹1›, ‹2›, \dots) and most of the standard
 arithmetic operations (‹+›, ‹-›, ‹*›, ‹≤›,
 ‹<\<close>, etc.) are overloaded: they are available
 not just for natural numbers but for other types as well.
 For example, given the goal ‹x + 0 = x›, 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 ‹0› and ‹+›
 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 ‹x+0 = (x::nat)›. If there
 is enough contextual information this may not be necessary: prop‹Suc x =
 x› automatically implies ‹x::nat› because term‹Suc› is not
 overloaded.
 end{warn}

 subsubsection{An Informal Proof}

  we gave some terse informal explanation of the proof of
 prop‹add m 0 = m›. A more detailed informal exposition of the lemma
  look like this:
 bigskip

 noindent
 textbf{Lemma} prop‹add m 0 = m›

 noindent
 textbf{Proof} by induction on ‹m›.
 begin{itemize}
 item Case ‹0› (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 ‹add (Suc m) 0 = Suc m›.
 The proof is as follows:\smallskip

 \begin{tabular}{@ {}rcl@ {\quad}l@ {}}
 term‹add (Suc m) 0› &‹=›& term‹Suc(add m 0)›
 & by definition of ‹add›\\
 &‹=›& term‹Suc m› & by IH
 \end{tabular}
 end{itemize}
  this book, \concept{IH} will stand for ``induction hypothesis''.

  have now seen three proofs of prop‹add m 0 = 0›: the Isabelle one, the
  four lines explaining the base case and the induction step, and just now a
  of a traditional inductive proof. The three proofs differ in the level
  detail given and the intended reader: the Isabelle proof is for the
 , the informal proofs are for humans. Although this book concentrates
  Isabelle proofs, it is important to be able to rephrase those proofs
  informal text comprehensible to a reader familiar with traditional
  proofs. Later on we will introduce an Isabelle proof language
  is closer to traditional informal mathematical language and is often
  readable.

 subsection{Type \indexed{‹list›}{list}}

  lists are already predefined, we define our own copy for
  purposes:
 ›
(*<*)
apply(auto)
done 
declare [[names_short]]
(*>*)
datatype 'a list = Nil | Cons 'a "'a list"
(*<*)
for map: map
(*>*)

text‹
 begin{itemize}
 item Type typ‹'a list› is the type of lists over elements of type typ‹'a›. Because typ‹'a› is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
 item Lists have two constructors: const‹Nil›, the empty list, and const‹Cons›, which puts an element (of type typ‹'a›) in front of a list (of type typ‹'a list›).
  all lists are of the form const‹Nil›, or term‹Cons x Nil›,
  term‹Cons x (Cons y Nil)›, etc.
 item \isacom{datatype} requires no quotation marks on the
 -hand side, but on the right-hand side each of the argument
  of a constructor needs to be enclosed in quotation marks, unless
  is just an identifier (e.g., typ‹nat› or typ‹'a›).
 end{itemize}
  also define two standard functions, append and reverse:›

fun app :: "'a list → 'a list → 'a list" where
"app Nil ys = ys" |
"app (Cons x xs) ys = Cons x (app xs ys)"

fun rev :: "'a list → 'a list" where
"rev Nil = Nil" |
"rev (Cons x xs) = app (rev xs) (Cons x Nil)"

text‹By default, variables ‹xs›, ‹ys› and ‹zs› are of
 ‹list› type.

  \indexed{\isacom{value}}{value} evaluates a term. For example,›

value "rev(Cons True (Cons False Nil))"

text‹yields the result 🚫‹rev(Cons True (Cons False Nil))›. This works symbolically, too:›

value "rev(Cons a (Cons b Nil))"

text‹yields 🚫‹rev(Cons a (Cons b Nil))›.
 medskip

 ~\ref{fig:MyList} shows the theory created so far.
  ‹list›, const‹Nil›, const‹Cons›, etc.\ are already predefined,
 Isabelle prints qualified (long) names when executing this theory, for example, ‹MyList.Nil›
 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
 quotations marks are needed that we mostly sweep under the carpet. In
 particular, notice that \isacom{datatype} requires no quotation marks on the
 left-hand side, but that on the right-hand side each of the argument
 types of a constructor needs to be enclosed in quotation marks.

 begin{figure}[htbp]
 begin{alltt}
 input{MyList.thy}\end{alltt}
 caption{A theory of lists}
 label{fig:MyList}
 index{comment}
 end{figure}

 subsubsection{Structural Induction for Lists}

  as for natural numbers, there is a proof principle of induction for
 . Induction over a list is essentially induction over the length of
  list, although the length remains implicit. To prove that some property
 ‹P› holds for all lists ‹xs›, i.e., \mbox{prop‹P(xs)›},
  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 ‹x› and ‹xs›.
 end{enumerate}
  is often called \concept{structural induction} for lists.

 subsection{The Proof Process}

  will now demonstrate the typical proof process, which involves
  formulation and proof of auxiliary lemmas.
  goal is to show that reversing a list twice produces the original
 .›

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

txt‹Commands \isacom{theorem} and \isacom{lemma} are
  and merely indicate the importance we attach to a
 . Via the bracketed attribute ‹simp› we also tell Isabelle
  make the eventual theorem a \conceptnoidx{simplification rule}: future proofs
  simplification will replace occurrences of term‹rev(rev xs)› by
 term‹xs›. The proof is by induction:›

apply(induction xs)

txt‹
  explained above, we obtain two subgoals, namely the base case (const‹Nil›) and the induction step (const‹Cons›):
 {subgoals[display,indent=0,margin=65]}
  us try to solve both goals automatically:
 ›

apply(auto)

txt‹Subgoal~1 is proved, 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.

 subsubsection{A First Lemma}

  insert the following lemma in front of the main theorem:
 ›
(*<*)
oops
(*>*)
lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"

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

apply(induction xs)

txt‹This time not even the base case is solved automatically:›
apply(auto)
txt‹
 vspace{-5ex}
 {subgoals[display,goals_limit=1]}
 , we need to abandon this proof attempt and prove another simple lemma
 .

 subsubsection{A Second Lemma}

  again try the canonical proof procedure:
 ›
(*<*)
oops
(*>*)
lemma app_Nil2 [simp]: "app xs Nil = xs"
apply(induction xs)
apply(auto)
done

text‹
 , this worked.
  we can continue with our stuck proof attempt of the first lemma:
 ›

lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"
apply(induction xs)
apply(auto)

txt‹
  find that this time ‹auto› solves the base case, but the
  step merely simplifies to
 {subgoals[display,indent=0,goals_limit=1]}
  missing lemma is associativity of const‹app›,
  we insert in front of the failed lemma ‹rev_app›.

 subsubsection{Associativity of const‹app›}

  canonical proof procedure succeeds without further ado:
 ›
(*<*)oops(*>*)
lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)"
apply(induction xs)
apply(auto)
done
(*<*)
lemma rev_app [simp]: "rev(app xs ys) = app (rev ys)(rev xs)"
apply(induction xs)
apply(auto)
done

theorem rev_rev [simp]: "rev(rev xs) = xs"
apply(induction xs)
apply(auto)
done
(*>*)
text‹
  the proofs of @{thm[source] rev_app} and @{thm[source] rev_rev}
 , too.

 subsubsection{Another Informal Proof}

  is the informal proof of associativity of const‹app›
  to the Isabelle proof above.
 bigskip

 noindent
 textbf{Lemma} prop‹app (app xs ys) zs = app xs (app ys zs)›

 noindent
 textbf{Proof} by induction on ‹xs›.
 begin{itemize}
 item Case ‹Nil›: \ prop‹app (app Nil ys) zs = app ys zs› ‹=›
 \mbox{term‹app Nil (app ys zs)›} \ holds by definition of ‹app›.
 item Case ‹Cons x xs›: We assume
 \begin{center} \hfill term‹app (app xs ys) zs› ‹=›
 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›\\
 ‹= app (Cons x (app xs ys)) zs› & by definition of ‹app›\\
 ‹= Cons x (app (app xs ys) zs)› & by definition of ‹app›\\
 ‹= Cons x (app xs (app ys zs))› & by IH\\
 ‹= app (Cons x xs) (app ys zs)› & by definition of ‹app›
 \end{tabular}
 end{itemize}
 medskip

 noindent Didn't we say earlier that all proofs are by simplification? But
  both cases, going from left to right, the last equality step is not a
  at all! In the base case it is prop‹app ys zs = app Nil (app
  zs)›. It appears almost mysterious because we suddenly complicate the
  by appending ‹Nil› on the left. What is really going on is this:
  proving some equality \mbox{prop‹s = t›}, both ‹s› and ‹t› are
  until they ``meet in the middle''. This heuristic for equality proofs
  well for a functional programming context like ours. In the base case
  term‹app (app Nil ys) zs› and term‹app Nil (app
  zs)› are simplified to term‹app ys zs›, the term in the middle.

 subsection{Predefined Lists}
 label{sec:predeflists}

 's predefined lists are the same as the ones above, but with
  syntactic sugar:
 begin{itemize}
 item ‹[]› is \indexed{const‹Nil›}{Nil},
 item term‹x # xs› is term‹Cons x xs›\index{Cons@const‹Cons›},
 item ‹[x₁, …, x_n]› is ‹x₁ # … # x_n # []›, and
 item term‹xs @ ys› is term‹app xs ys›.
 end{itemize}
  is also a large library of predefined functions.
  most important ones are the length function
 ‹length :: 'a list → nat›\index{length@const‹length›} (with the obvious definition),
  the \indexed{const‹map›}{map} function that applies a function to all elements of a list:
 begin{isabelle}
 isacom{fun} const‹map› ‹::› @{typ[source] "('a → 'b) → 'a list → 'b list"} \isacom{where}\\
 ‹"›@{thm list.map(1) [of f]}‹" |›\\
 ‹"›@{thm list.map(2) [of f x xs]}‹"›
 end{isabelle}

 ifsem
  useful are the \concept{head} of a list, its first element,
  the \concept{tail}, the rest of the list:
 begin{isabelle}\index{hd@const‹hd›}
 isacom{fun} ‹hd :: 'a list → 'a›\\
 prop‹hd(x#xs) = x›
 end{isabelle}
 begin{isabelle}\index{tl@const‹tl›}
 isacom{fun} ‹tl :: 'a list → 'a list›\\
 prop‹tl [] = []› ‹|›\\
 prop‹tl(x#xs) = xs›
 end{isabelle}
  that since HOL is a logic of total functions, term‹hd []› is defined,
  we do not know what the result is. That is, term‹hd []› is not undefined
  underdefined.
 fi
 

  now on lists are always the predefined lists.

 ifsem\else
 subsection{Types typ‹int› and typ‹real›}

  addition to typ‹nat› there are also the types typ‹int› and typ‹real›, the mathematical integers
  real numbers. As mentioned above, numerals and most of the standard arithmetic operations are overloaded.
  particular they are defined on typ‹int› and typ‹real›.

 begin{warn}
  are two infix exponentiation operators:
 term‹(^)› for typ‹nat› and typ‹int› (with exponent of type typ‹nat› in both cases)
  term‹(powr)› for typ‹real›.
 end{warn}
 begin{warn}
  typ‹int› is already part of theory 🚫‹Main›, but in order to use typ‹real› as well, you have to import
  🚫‹Complex_Main› instead of 🚫‹Main›.
 end{warn}

  are three coercion functions that are inclusions and do not lose information:
 begin{quote}
 begin{tabular}{rcl}
 const‹int› &‹::›& typ‹nat → int›\\
 const‹real› &‹::›& typ‹nat → real›\\
 const‹real_of_int› &‹::›& typ‹int → real›\\
 end{tabular}
 end{quote}

  inserts these inclusions automatically once you import ‹Complex_Main›.
  there are multiple type-correct completions, Isabelle chooses an arbitrary one.
  example, the input \noquotes{@{term[source] "(i::int) + (n::nat)"}} has the unique
 -correct completion term‹(i::int) + int(n::nat)›. In contrast,
 noquotes{@{term[source] "((n::nat) + n) :: real"}} has two type-correct completions,
 noquotes{@{term[source]"real(n+n)"}} and \noquotes{@{term[source]"real n + real n"}}.

  are also the coercion functions in the other direction:
 begin{quote}
 begin{tabular}{rcl}
 const‹nat› &‹::›& typ‹int → nat›\\
 const‹floor› &‹::›& typ‹real → int›\\
 const‹ceiling› &‹::›& typ‹real → int›\\
 end{tabular}
 end{quote}
 fi

 subsection*{Exercises}

 begin{exercise}
  the \isacom{value} command to evaluate the following expressions:
 {term[source] "1 + (2::nat)"}, @{term[source] "1 + (2::int)"},
 {term[source] "1 - (2::nat)"} and @{term[source] "1 - (2::int)"}.
 end{exercise}

 begin{exercise}
  from the definition of const‹add› given above.
  that const‹add› is associative and commutative.
  a recursive function ‹double› ‹::› typ‹nat → nat›
  prove prop‹double m = add m m›.
 end{exercise}

 begin{exercise}
  a function ‹count ::› typ‹'a → 'a list → nat›
  counts the number of occurrences of an element in a list. Prove
 prop‹count x xs ≤ length xs›.
 end{exercise}

 begin{exercise}
  a recursive function ‹snoc ::› typ‹'a list → 'a → 'a list›
  appends an element to the end of a list. With the help of ‹snoc›
  a recursive function ‹reverse ::› typ‹'a list → 'a list›
  reverses a list. Prove prop‹reverse(reverse xs) = xs›.
 end{exercise}

 begin{exercise}
  a recursive function ‹sum_upto ::› typ‹nat → nat› such that
 mbox{‹sum_upto n›} ‹=› ‹0 + ... + n› and prove
 prop‹ sum_upto (n::nat) = n * (n+1) div 2›.
 end{exercise}
 ›
(*<*)
end
(*>*)