theory FirstSteps

imports Base

begin

chapter {* First Steps *}

text {*

  Isabelle programming is done in ML. Just like lemmas and proofs, ML-code

  in Isabelle is 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} FirstSteps\\

  \isacommand{imports} Main\\

  \isacommand{begin}\\

  \ldots

  \end{tabular}

  \end{quote}

  We also generally assume you are working with HOL. The given examples might

  need to be adapted if you work in a different logic.

*}

section {* Including ML-Code *}

text {*

  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}~@{text "\<verbopen>"}\isanewline

\hspace{5mm}@{ML "3 + 4"}\isanewline

@{text "\<verbclose>"}\isanewline

@{text "> 7"}\smallskip

\end{graybox}

\end{isabelle}

  Like normal Isabelle scripts, \isacommand{ML}-commands can be

  evaluated by using the advance and undo buttons of your Isabelle

  environment. The code inside the \isacommand{ML}-command can also contain

  value and function bindings, for example

*}

ML %gray {* 

  val r = ref 0

  fun f n = n + 1 

*}

text {*

  and even those can be undone when the proof

  script is retracted.  As mentioned in the Introduction, we will drop the

  \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} 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}~@{text "test:"}\isanewline

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

  \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline

  \isacommand{oops}

  \end{isabelle}

  \end{quote}

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

  arrange that the ML-code is defined outside of proofs, for example).

  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{use}. For example

  \begin{quote}

  \begin{tabular}{@ {}l}

  \isacommand{theory} FirstSteps\\

  \isacommand{imports} Main\\

  \isacommand{uses}~@{text "(\"file_to_be_included.ML\")"} @{text "\<dots>"}\\

  \isacommand{begin}\\

  \ldots\\

  \isacommand{use}~@{text "\"file_to_be_included.ML\""}\\

  \ldots

  \end{tabular}

  \end{quote}

  The \isacommand{uses}-command in the header of the theory is needed in order 

  to indicate the dependency of the theory on the ML-file. Alternatively, the 

  file can be included by just writing in the header

  \begin{quote}

  \begin{tabular}{@ {}l}

  \isacommand{theory} FirstSteps\\

  \isacommand{imports} Main\\

  \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\

  \isacommand{begin}\\

  \ldots

  \end{tabular}

  \end{quote}

  Note that no parentheses are given this time. Note also that the 

  included ML-file should not contain any

  \isacommand{use} itself. Otherwise Isabelle is unable to record all

  file dependencies, which is a nuisance if you have to track down

  errors.

*}

section {* Debugging and Printing\label{sec:printing} *}

text {*

  During development you might find it necessary to inspect some data

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

  the function @{ML [index] "writeln"}. For example 

  @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}

  will print out @{text [quotes] "any string"} inside the response buffer

  of Isabelle.  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 function @{ML PolyML.makestring}:

  @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} 

  However, @{ML [index] makestring in PolyML} only works if the type of what is converted is monomorphic 

  and not a function.

  The function @{ML "writeln"} should only be used for testing purposes, because any

  output this function generates will be overwritten as soon as an error is

  raised. For printing anything more serious and elaborate, the

  function @{ML [index] tracing} is more appropriate. This function writes all output into

  a separate tracing buffer. For example:

  @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}

  It is also possible to redirect the ``channel'' where the string @{text "foo"} is 

  printed to a separate file, e.g., to prevent ProofGeneral from choking on massive 

  amounts of trace output. This redirection can be achieved with the code:

*}

ML{*val strip_specials =

let

  fun strip ("\^A" :: _ :: cs) = strip cs

    | strip (c :: cs) = c :: strip cs

    | strip [] = [];

in implode o strip o explode end;

fun redirect_tracing stream =

 Output.tracing_fn := (fn s =>

    (TextIO.output (stream, (strip_specials s));

     TextIO.output (stream, "\n");

     TextIO.flushOut stream)) *}

text {*

  Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 

  will cause that all tracing information is printed into the file @{text "foo.bar"}.

  You can print out error messages with the function @{ML [index] error}; for example:

@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" 

"Exception- ERROR \"foo\" raised

At command \"ML\"."}

  (FIXME Mention how to work with @{ML [index] debug in Toplevel} and 

  @{ML [index] profiling in Toplevel}.)

*}

(*

ML {* reset Toplevel.debug *}

ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *}

ML {* fun innocent () = dodgy_fun () *}

ML {* exception_trace (fn () => cterm_of @{theory} (Bound 0)) *}

ML {* exception_trace (fn () => innocent ()) *}

ML {* Toplevel.program (fn () => cterm_of @{theory} (Bound 0)) *}

ML {* Toplevel.program (fn () => innocent ()) *}

*)

text {*

  Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} 

  or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing 

  them (see Section \ref{sec:pretty}), 

  but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform 

  a term into a string is to use the function @{ML [index] string_of_term in Syntax}.

  @{ML_response_fake [display,gray]

  "Syntax.string_of_term @{context} @{term \"1::nat\"}"

  "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}

  This produces a string with some additional information encoded in it. The string

  can be properly printed by using the function @{ML [index] writeln}.

  @{ML_response_fake [display,gray]

  "writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})"

  "\"1\""}

  A @{ML_type cterm} can be transformed into a string by the following function.

*}

ML{*fun string_of_cterm ctxt t =  

   Syntax.string_of_term ctxt (term_of t)*}

text {*

  In this example the function @{ML [index] term_of} extracts the @{ML_type term} from

  a @{ML_type cterm}.  If there are more than one @{ML_type cterm}s to be

  printed, you can use the function @{ML [index] commas} to separate them.

*} 

ML{*fun string_of_cterms ctxt ts =  

   commas (map (string_of_cterm ctxt) ts)*}

text {*

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

  into a @{ML_type cterm} using the function @{ML [index] crep_thm}. 

*}

ML{*fun string_of_thm ctxt thm =

  string_of_cterm ctxt (#prop (crep_thm thm))*}

text {*

  Theorems also include schematic variables, such as @{text "?P"}, 

  @{text "?Q"} and so on. 

  @{ML_response_fake [display, gray]

  "tracing (string_of_thm @{context} @{thm conjI})"

  "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}

  In order to improve the readability of theorems we convert

  these schematic variables into free variables using the 

  function @{ML [index] import in Variable}.

*}

ML{*fun no_vars ctxt thm =

let 

  val ((_, [thm']), _) = Variable.import true [thm] ctxt

in

  thm'

end

fun string_of_thm_no_vars ctxt thm =

  string_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}

text {* 

  Theorem @{thm [source] conjI} is now printed as follows:

  @{ML_response_fake [display, gray]

  "tracing (string_of_thm_no_vars @{context} @{thm conjI})"

  "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}

  Again the function @{ML commas} helps with printing more than one theorem. 

*}

ML{*fun string_of_thms ctxt thms =  

  commas (map (string_of_thm ctxt) thms)

fun string_of_thms_no_vars ctxt thms =  

  commas (map (string_of_thm_no_vars ctxt) thms) *}

section {* Combinators\label{sec:combinators} *}

text {*

  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 the code, but after getting familiar with them, they

  actually ease the understanding and also the programming.

  The simplest combinator is @{ML [index] I}, which is just the identity function defined as

*}

ML{*fun I x = x*}

text {* Another simple combinator is @{ML [index] K}, defined as *}

ML{*fun K x = fn _ => x*}

text {*

  @{ML [index] K} ``wraps'' a function around the argument @{text "x"}. However, this 

  function ignores its argument. As a result, @{ML K} defines a constant function 

  always returning @{text x}.

  The next combinator is reverse application, @{ML [index] "|>"}, defined as: 

*}

ML{*fun x |> f = f x*}

text {* 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 *}

ML %linenosgray{*fun inc_by_five x =

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

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

    |> fst

    |> (fn x => x + 4)*}

text {*

  which increments its argument @{text x} by 5. It proceeds 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 (for example by adding a definition, followed by

  lemmas and so on). The reverse application allows you to read what happens in 

  a top-down manner. This kind of coding should also 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

*}

ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}

text {* or *}

ML{*fun inc_by_five x = 

       ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}

text {* and typographically more economical than *}

ML{*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*}

text {* 

  Another reason why the let-bindings in the code above are better to be

  avoided: it is more than easy to get the intermediate values wrong, not to 

  mention the nightmares the maintenance of this code causes!

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

  the waterfall fashion might be the following code:

*}

ML %linenosgray{*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 *}

text {*

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

  type, then @{ML "apply_fresh_args"} returns the term with distinct variables 

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

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

  @{ML_response_fake [display,gray]

"let

  val t = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}

  val ctxt = @{context}

in 

  apply_fresh_args t ctxt

   |> Syntax.string_of_term ctxt

   |> tracing

end" 

  "P z za zb"}

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

  coded: in Line 2, the function @{ML [index] fastype_of} calculates the type of the

  term; @{ML [index] binder_types} in the next line produces the list of argument

  types (in the case above the list @{text "[nat, int, unit]"}); Line 4 

  pairs up each type with the string  @{text "z"}; the

  function @{ML [index] variant_frees in Variable} generates for each @{text "z"} a

  unique name avoiding the given @{text f}; 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 [index] list_comb} to the term. In this last step we have to 

  use the function @{ML [index] curry}, because @{ML [index] list_comb} expects the 

  function and the variables list as a pair. This kind of functions is often needed when

  constructing terms with fresh variables. The infrastructure helps tremendously 

  to avoid any name clashes. Consider for example: 

   @{ML_response_fake [display,gray]

"let

  val t = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}

  val ctxt = @{context}

in

  apply_fresh_args t ctxt 

   |> Syntax.string_of_term ctxt

   |> tracing