src/Doc/Prog_Prove/Bool_nat_list.thy

 theory Bool_nat_list
 imports Main
 begin
 (*>*)
 
-text{*
+text\<open>
 \vspace{-4ex}
 \section{\texorpdfstring{Types @{typ bool}, @{typ nat} and @{text list}}{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

 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:
-*}
+\<close>
 
 fun conj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
 "conj True True = True" |
 "conj _ _ = False"
 
-text{* Both the datatype and function definitions roughly follow the syntax
+text\<open>Both the datatype and function definitions roughly follow the syntax
 of functional programming languages.
 
 \subsection{Type \indexed{@{typ nat}}{nat}}
 
 Natural numbers are another predefined datatype:

 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:
-*}
+\<close>
 
 fun add :: "nat \<Rightarrow> nat \<Rightarrow> 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"}: *}
+text\<open>And here is a proof of the fact that @{prop"add m 0 = m"}:\<close>
 
 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
+txt\<open>The \isacom{lemma} command starts the proof and gives the lemma
 a name, @{text add_02}. 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
 following proof state\ifsem\footnote{See page \pageref{proof-state} for how to

 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{* which displays @{thm[show_question_marks,display] add_02} The free
+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
 operational one: unknowns can be instantiated, which is what you want after
 some lemma has been proved.
 

 
 \subsection{Type \indexed{@{text list}}{list}}
 
 Although lists are already predefined, we define our own copy for
 demonstration purposes:
-*}
+\<close>
 (*<*)
 apply(auto)
 done 
 declare [[names_short]]
 (*>*)
 datatype 'a list = Nil | Cons 'a "'a list"
 (*<*)
 for map: map
 (*>*)
 
-text{*
+text\<open>
 \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"}).
 Hence all lists are of the form @{const Nil}, or @{term"Cons x Nil"},
 or @{term"Cons x (Cons y Nil)"}, etc.
 \item \isacom{datatype} requires no quotation marks on the
 left-hand side, but on the right-hand side each of the argument
 types of a constructor needs to be enclosed in quotation marks, unless
 it is just an identifier (e.g., @{typ nat} or @{typ 'a}).
 \end{itemize}
-We also define two standard functions, append and reverse: *}
+We also define two standard functions, append and reverse:\<close>
 
 fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "app Nil ys = ys" |
 "app (Cons x xs) ys = Cons x (app xs ys)"
 
 fun rev :: "'a list \<Rightarrow> 'a list" where
 "rev Nil = Nil" |
 "rev (Cons x xs) = app (rev xs) (Cons x Nil)"
 
-text{* By default, variables @{text xs}, @{text ys} and @{text zs} are of
+text\<open>By default, variables @{text xs}, @{text ys} and @{text zs} are of
 @{text list} type.
 
-Command \indexed{\isacommand{value}}{value} evaluates a term. For example, *}
+Command \indexed{\isacommand{value}}{value} evaluates a term. For example,\<close>
 
 value "rev(Cons True (Cons False Nil))"
 
-text{* yields the result @{value "rev(Cons True (Cons False Nil))"}. This works symbolically, too: *}
+text\<open>yields the result @{value "rev(Cons True (Cons False Nil))"}. This works symbolically, too:\<close>
 
 value "rev(Cons a (Cons b Nil))"
 
-text{* yields @{value "rev(Cons a (Cons b 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}

 \subsection{The Proof Process}
 
 We will now demonstrate the typical proof process, which involves
 the formulation and proof of auxiliary lemmas.
 Our goal is to show that reversing a list twice produces the original
-list. *}
+list.\<close>
 
 theorem rev_rev [simp]: "rev(rev xs) = xs"
 
-txt{* Commands \isacom{theorem} and \isacom{lemma} are
+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
 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: *}
-
-apply(induction xs)
-
-txt{*
+@{term"xs"}. The proof is by induction:\<close>
+
+apply(induction xs)
+
+txt\<open>
 As explained above, we obtain two subgoals, namely the base case (@{const Nil}) and the induction step (@{const Cons}):
 @{subgoals[display,indent=0,margin=65]}
 Let us try to solve both goals automatically:
-*}
-
-apply(auto)
-
-txt{*Subgoal~1 is proved, and disappears; the simplified version
+\<close>
+
+apply(auto)
+
+txt\<open>Subgoal~1 is proved, and disappears; the simplified version
 of subgoal~2 becomes the new subgoal~1:
 @{subgoals[display,indent=0,margin=70]}
 In order to simplify this subgoal further, a lemma suggests itself.
 
 \subsubsection{A First Lemma}
 
 We insert the following lemma in front of the main theorem:
-*}
+\<close>
 (*<*)
 oops
 (*>*)
 lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"
 
-txt{* There are two variables that we could induct on: @{text xs} and
+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:
-*}
-
-apply(induction xs)
-
-txt{* This time not even the base case is solved automatically: *}
-apply(auto)
-txt{*
+\<close>
+
+apply(induction xs)
+
+txt\<open>This time not even the base case is solved automatically:\<close>
+apply(auto)
+txt\<open>
 \vspace{-5ex}
 @{subgoals[display,goals_limit=1]}
 Again, we need to abandon this proof attempt and prove another simple lemma
 first.
 
 \subsubsection{A Second Lemma}
 
 We again try the canonical proof procedure:
-*}
+\<close>
 (*<*)
 oops
 (*>*)
 lemma app_Nil2 [simp]: "app xs Nil = xs"
 apply(induction xs)
 apply(auto)
 done
 
-text{*
+text\<open>
 Thankfully, this worked.
 Now we can continue with our stuck proof attempt of the first lemma:
-*}
+\<close>
 
 lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"
 apply(induction xs)
 apply(auto)
 
-txt{*
+txt\<open>
 We find that this time @{text"auto"} 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}.
 
 \subsubsection{Associativity of @{const app}}
 
 The canonical proof procedure succeeds without further ado:
-*}
+\<close>
 (*<*)oops(*>*)
 lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)"
 apply(induction xs)
 apply(auto)
 done

 theorem rev_rev [simp]: "rev(rev xs) = xs"
 apply(induction xs)
 apply(auto)
 done
 (*>*)
-text{*
+text\<open>
 Finally the proofs of @{thm[source] rev_app} and @{thm[source] rev_rev}
 succeed, too.
 
 \subsubsection{Another Informal Proof}
 

 \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
 @{prop" sum_upto (n::nat) = n * (n+1) div 2"}.
 \end{exercise}
-*}
+\<close>
 (*<*)
 end
 (*>*)