theory First_Steps

imports Base

begin

chapter \<open>First Steps\label{chp:firststeps}\<close>

text \<open>

  \begin{flushright}

  {\em ``The most effective debugging tool is still careful thought,\\ 

  coupled with judiciously placed print statements.''} \\[1ex]

  Brian Kernighan, in {\em Unix for Beginners}, 1979

  \end{flushright}

  \medskip

  Isabelle programming is done in ML @{cite "isa-imp"}. Just like lemmas and proofs, ML-code for

  Isabelle must be part of a theory. If you want to follow the code given in

  this chapter, we assume you are working inside the theory starting with

  \begin{quote}

  \begin{tabular}{@ {}l}

  \isacommand{theory} First\_Steps\\

  \isacommand{imports} Main\\

  \isacommand{begin}\\

  \ldots

  \end{tabular}

  \end{quote}

  We also generally assume you are working with the logic HOL. The examples

  that will be given might need to be adapted if you work in a different logic.

\<close>

section \<open>Including ML-Code\label{sec:include}\<close>

text \<open>

  The easiest and quickest way to include code in a theory is by using the

  \isacommand{ML}-command. For example:

  \begin{isabelle}

  \begin{graybox}

  \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline

  \<open>\<verbclose>\<close>\isanewline

  \<open>> 7\<close>\smallskip

  \end{graybox}

  \end{isabelle}

  If you work with the

  Isabelle/jEdit, then you just have to hover the cursor over the code 

  and you see the evaluated result in the ``Output'' window.

  As mentioned in the Introduction, we will drop the \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> scaffolding whenever we show code. The lines

  prefixed with @{text [quotes] ">"} are not part of the code, rather they

  indicate what the response is when the code is evaluated.  There are also

  the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for including

  ML-code. The first evaluates the given code, but any effect on the theory,

  in which the code is embedded, is suppressed. The second needs to be used if

  ML-code is defined inside a proof. For example

  \begin{quote}

  \begin{isabelle}

  \isacommand{lemma}~\<open>test:\<close>\isanewline

  \isacommand{shows}~@{text [quotes] "True"}\isanewline

  \isacommand{oops}

  \end{isabelle}

  \end{quote}

  However, both commands will only play minor roles in this tutorial (we most of

  the time make sure that the ML-code is defined outside proofs).

  Once a portion of code is relatively stable, you usually want to export it

  to a separate ML-file. Such files can then be included somewhere inside a 

  theory by using the command \isacommand{ML\_file}. For example

  \begin{quote}

  \begin{tabular}{@ {}l}

  \isacommand{theory} First\_Steps\\

  \isacommand{imports} Main\\

  \isacommand{begin}\\

  \ldots\\

  \isacommand{ML\_file}~\<open>"file_to_be_included.ML"\<close>\\

  \ldots

  \end{tabular}

  \end{quote}

\<close>

section \<open>Printing and Debugging\label{sec:printing}\<close>

text \<open>

  During development you might find it necessary to inspect data in your

  code. This can be done in a ``quick-and-dirty'' fashion using the function

  @{ML_ind writeln in Output}. For example

  will print out @{text [quotes] "any string"}.  

  This function expects a string as argument. If you develop under

  PolyML, then there is a convenient, though again ``quick-and-dirty'', method

  for converting values into strings, namely the antiquotation 

  \<open>@{make_string}\<close>:

  @{ML_matchresult_fake [display,gray] \<open>writeln (@{make_string} 1)\<close> \<open>"1"\<close>} 

  However, \<open>@{make_string}\<close> only works if the type of what

  is converted is monomorphic and not a function. 

  You can print out error messages with the function @{ML_ind error in Library}; 

  for example:

  @{ML_matchresult_fake [display,gray] 

  This function raises the exception \<open>ERROR\<close>, which will then 

  be displayed by the infrastructure indicating that it is an error by

  painting the output red. Note that this exception is meant 

  for ``user-level'' error messages seen by the ``end-user''. 

  For messages where you want to indicate a genuine program error

  use the exception \<open>Fail\<close>. 

  Most often you want to inspect contents of Isabelle's basic data structures,

  namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}

  and @{ML_type thm}. Isabelle provides elaborate pretty-printing functions,

  which we will explain in more detail in Section \ref{sec:pretty}. For now

  we just use the functions @{ML_ind writeln in Pretty}  from the structure

  @{ML_structure Pretty} and @{ML_ind pretty_term in Syntax} from the structure

  @{ML_structure Syntax}. For more convenience, we bind them to the toplevel.

\<close>

ML %grayML\<open>val pretty_term = Syntax.pretty_term

val pwriteln = Pretty.writeln\<close>

text \<open>

  They can be used as follows

  @{ML_matchresult_fake [display,gray]

  If there is more than one term to be printed, you can use the 

  function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty} 

  to separate them.

\<close> 

ML %grayML\<open>fun pretty_terms ctxt trms =  

  Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))\<close>

text \<open>

  To print out terms together with their typing information,

  set the configuration value

  @{ML_ind show_types in Syntax} to @{ML true}.

\<close>

ML %grayML\<open>val show_types_ctxt = Config.put show_types true @{context}\<close>

text \<open>

  Now by using this context @{ML pretty_term} prints out

  @{ML_matchresult_fake [display, gray]

  where \<open>1\<close> and \<open>x\<close> are displayed with their inferred types.

  Other configuration values that influence

  printing of terms include 

  \begin{itemize}

  \item @{ML_ind show_brackets in Syntax} 

  \item @{ML_ind show_sorts in Syntax}

  \item @{ML_ind eta_contract in Syntax}

  \end{itemize}

  A @{ML_type cterm} can be printed with the following function.

\<close>

ML %grayML %grayML\<open>fun pretty_cterm ctxt ctrm =  

  pretty_term ctxt (Thm.term_of ctrm)\<close>

text \<open>

  Here the function @{ML_ind term_of in Thm} extracts the @{ML_type

  term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can be

  printed again with @{ML commas in Pretty}.

\<close> 

ML %grayML\<open>fun pretty_cterms ctxt ctrms =  

  Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))\<close>

text \<open>

  The easiest way to get the string of a theorem is to transform it

  into a @{ML_type term} using the function @{ML_ind prop_of in Thm}. 

\<close>

ML %grayML\<open>fun pretty_thm ctxt thm =

  pretty_term ctxt (Thm.prop_of thm)\<close>

text \<open>

  Theorems include schematic variables, such as \<open>?P\<close>, 

  \<open>?Q\<close> and so on. They are instantiated by Isabelle when a theorem is applied.

  For example, the theorem 

  @{thm [source] conjI} shown below can be used for any (typable) 

  instantiation of \<open>?P\<close> and \<open>?Q\<close>. 

  @{ML_matchresult_fake [display, gray]

  However, to improve the readability when printing theorems, we

  can switch off the question marks as follows:

\<close>

ML %grayML\<open>fun pretty_thm_no_vars ctxt thm =

let

  val ctxt' = Config.put show_question_marks false ctxt

in

  pretty_term ctxt' (Thm.prop_of thm)

end\<close>

text \<open>

  With this function, theorem @{thm [source] conjI} is now printed as follows:

  @{ML_matchresult_fake [display, gray]

  Again the functions @{ML commas} and @{ML block in Pretty} help 

  with printing more than one theorem. 

\<close>

ML %grayML\<open>fun pretty_thms ctxt thms =  

  Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms))

fun pretty_thms_no_vars ctxt thms =  

  Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))\<close>

text \<open>

  Printing functions for @{ML_type typ} are

\<close>

ML %grayML\<open>fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty

fun pretty_typs ctxt tys = 

  Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))\<close>

text \<open>

  respectively @{ML_type ctyp}

\<close>

ML %grayML\<open>fun pretty_ctyp ctxt cty = pretty_typ ctxt (Thm.typ_of cty)

fun pretty_ctyps ctxt ctys = 

  Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))\<close>

text \<open>

  \begin{readmore}

  The simple conversion functions from Isabelle's main datatypes to 

  @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. 

  The configuration values that change the printing information are declared in 

  @{ML_file "Pure/Syntax/printer.ML"}.

  \end{readmore}

  Note that for printing out several ``parcels'' of information that belong

  together, like a warning message consisting of a term and its type, you

  should try to print these parcels together in a single string. Therefore do

  \emph{not} print out information as

@{ML_matchresult_fake [display,gray]

  but as a single string with appropriate formatting. For example

@{ML_matchresult_fake [display,gray]

  To ease this kind of string manipulations, there are a number

  of library functions in Isabelle. For example,  the function 

  @{ML_ind cat_lines in Library} concatenates a list of strings 

  and inserts newlines in between each element. 

  @{ML_matchresult_fake [display, gray]

  Section \ref{sec:pretty} will explain the infrastructure that Isabelle 

  provides for more elaborate pretty printing. 

  \begin{readmore}

  Most of the basic string functions of Isabelle are defined in 

  @{ML_file "Pure/library.ML"}.

  \end{readmore}

\<close>

section \<open>Combinators\label{sec:combinators}\<close>

text \<open>

  For beginners perhaps the most puzzling parts in the existing code of

  Isabelle are the combinators. At first they seem to greatly obstruct the

  comprehension of code, but after getting familiar with them and handled with

  care, they actually ease the understanding and also the programming.

  The simplest combinator is @{ML_ind I in Library}, which is just the 

  identity function defined as

\<close>

ML %grayML\<open>fun I x = x\<close>

text \<open>

  Another simple combinator is @{ML_ind K in Library}, defined as 

\<close>

ML %grayML\<open>fun K x = fn _ => x\<close>

text \<open>

  @{ML K} ``wraps'' a function around \<open>x\<close> that ignores its argument. As a 

  result, @{ML K} defines a constant function always returning \<open>x\<close>.

  The next combinator is reverse application, @{ML_ind  "|>" in Basics}, defined as: 

\<close>

ML %grayML\<open>fun x |> f = f x\<close>

text \<open>While just syntactic sugar for the usual function application,

  the purpose of this combinator is to implement functions in a  

  ``waterfall fashion''. Consider for example the function\<close>

ML %linenosgray\<open>fun inc_by_five x =

  x |> (fn x => x + 1)

    |> (fn x => (x, x))

    |> fst

    |> (fn x => x + 4)\<close>

text \<open>

  which increments its argument \<open>x\<close> by 5. It does this by first

  incrementing the argument by 1 (Line 2); then storing the result in a pair

  (Line 3); taking the first component of the pair (Line 4) and finally

  incrementing the first component by 4 (Line 5). This kind of cascading

  manipulations of values is quite common when dealing with theories. The

  reverse application allows you to read what happens in a top-down

  manner. This kind of coding should be familiar, if you have been exposed to

  Haskell's {\it do}-notation. Writing the function @{ML inc_by_five} using

  the reverse application is much clearer than writing

\<close>

ML %grayML\<open>fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4\<close>

text \<open>or\<close>

ML %grayML\<open>fun inc_by_five x = 

  ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x\<close>

text \<open>and typographically more economical than\<close>

ML %grayML\<open>fun inc_by_five x =

let val y1 = x + 1

    val y2 = (y1, y1)

    val y3 = fst y2

    val y4 = y3 + 4

in y4 end\<close>

text \<open>

  Another reasons to avoid the let-bindings in the code above:

  it is easy to get the intermediate values wrong and

  the resulting code is difficult to maintain.

  In Isabelle a ``real world'' example for a function written in 

  the waterfall fashion might be the following code:

\<close>

ML %linenosgray\<open>fun apply_fresh_args f ctxt =

    f |> fastype_of

      |> binder_types 

      |> map (pair "z")

      |> Variable.variant_frees ctxt [f]

      |> map Free  

      |> curry list_comb f\<close>

text \<open>

  This function takes a term and a context as arguments. If the term is of function

  applied to it. For example, below three variables are applied to the term 

  @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:

  @{ML_matchresult_fake [display,gray]

  val ctxt = @{context}

in 

  apply_fresh_args trm ctxt

   |> pretty_term ctxt

   |> pwriteln

  You can read off this behaviour from how @{ML apply_fresh_args} is coded: in

  Line 2, the function @{ML_ind fastype_of in Term} calculates the type of the

  term; @{ML_ind binder_types in Term} in the next line produces the list of

  argument types (in the case above the list \<open>[nat, int, unit]\<close>); Line

  4 pairs up each type with the string \<open>z\<close>; the function @{ML_ind

  variant_frees in Variable} generates for each \<open>z\<close> a unique name

  avoiding the given \<open>f\<close>; the list of name-type pairs is turned into a

  list of variable terms in Line 6, which in the last line is applied by the

  function @{ML_ind list_comb in Term} to the original term. In this last step we have

  to use the function @{ML_ind curry in Library}, because @{ML list_comb}

  expects the function and the variables list as a pair. 

  Functions like @{ML apply_fresh_args} are often needed when constructing

  terms involving fresh variables. For this the infrastructure helps

  tremendously to avoid any name clashes. Consider for example:

   @{ML_matchresult_fake [display,gray]

  val ctxt = @{context}

in

  apply_fresh_args trm ctxt 

   |> pretty_term ctxt

   |> pwriteln

  where the \<open>za\<close> is correctly avoided.

  The combinator @{ML_ind "#>" in Basics} is the reverse function composition. 

  It can be used to define the following function

\<close>

ML %grayML\<open>val inc_by_six = 

  (fn x => x + 1) #> 

  (fn x => x + 2) #> 

  (fn x => x + 3)\<close>

text \<open>

  which is the function composed of first the increment-by-one function and

  then increment-by-two, followed by increment-by-three. Again, the reverse

  function composition allows you to read the code top-down. This combinator

  is often used for setup functions inside the

  \isacommand{setup}- or \isacommand{local\_setup}-command. These functions 

  have to be of type @{ML_type "theory -> theory"}, respectively 

  @{ML_type "local_theory -> local_theory"}. More than one such setup function 

  where we store the theorems @{thm [source] conjI}, @{thm [source] conjunct1} 

  and @{thm [source] conjunct2} under alternative names.

\<close>  

local_setup %graylinenos \<open>

let  

  fun my_note name thm = Local_Theory.note ((name, []), [thm]) #> snd

in

  my_note @{binding "foo_conjI"} @{thm conjI} #>

  my_note @{binding "bar_conjunct1"} @{thm conjunct1} #>

  my_note @{binding "bar_conjunct2"} @{thm conjunct2}

end\<close>

text \<open>

  The function @{ML_text "my_note"} in line 3 is just a wrapper for the function 

  @{ML_ind note in Local_Theory} in the structure @{ML_structure Local_Theory}; 

  it stores a theorem under a name. 

  In lines 5 to 6 we call this function to give alternative names for the three

  The remaining combinators we describe in this section add convenience for

  the ``waterfall method'' of writing functions. The combinator @{ML_ind tap

  in Basics} allows you to get hold of an intermediate result (to do some

  side-calculations or print out an intermediate result, for instance). The

  function

\<close>