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{center}

  \begin{tabular}{@ {}l}

  \isacommand{theory} FirstSteps\\

  \isacommand{imports} Main\\

  \isacommand{begin}\\

  \ldots

  \end{tabular}

  \end{center}

*}

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 proof 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, and even those can be undone when the proof

  script is retracted. As mentioned earlier, 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.

  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 in a theory by using

  the \isacommand{uses}-command in the header of the theory, like:

  \begin{center}

  \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{center}

*}

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 "warning"}. For example 

  @{ML_response_fake [display,gray] "warning \"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 makestring}:

  @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} 

  However @{ML makestring} only works if the type of what is converted is monomorphic 

  and not a function.

  The function @{ML "warning"} 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 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 error}; for example:

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

"Exception- ERROR \"foo\" raised

At command \"ML\"."}

  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, 

  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 Syntax.string_of_term}.

  @{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 warning}.

  @{ML_response_fake [display,gray]

  "warning (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 str_of_cterm ctxt t =  

   Syntax.string_of_term ctxt (term_of t)*}

text {*

  In this example the function @{ML 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 commas} to separate them.

*} 

ML{*fun str_of_cterms ctxt ts =  

   commas (map (str_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 crep_thm}.

*}

ML{*fun str_of_thm ctxt thm =

  let

    val {prop, ...} = crep_thm thm

  in 

    str_of_cterm ctxt prop

  end*}

text {* 

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

*}

ML{*fun str_of_thms ctxt thms =  

  commas (map (str_of_thm 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 I}, which is just the identity function defined as

*}

ML{*fun I x = x*}

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

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

text {*

  @{ML 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 "|>"}, 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 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 (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 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!

  (FIXME: give a real world example involving theories)

  Similarly, the combinator @{ML "#>"} is the reverse function 

  composition. It can be used to define the following function

*}

ML{*val inc_by_six = 

      (fn x => x + 1)

   #> (fn x => x + 2)

   #> (fn x => x + 3)*}

text {* 

  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.

  The remaining combinators described in this section add convenience for the

  ``waterfall method'' of writing functions. The combinator @{ML tap} allows

  you to get hold of an intermediate result (to do some side-calculations for

  instance). The function

 *}

ML %linenosgray{*fun inc_by_three x =

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

       |> tap (fn x => tracing (makestring x))

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

text {* 

  increments the argument first by @{text "1"} and then by @{text "2"}. In the

  middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''

  intermediate result inside the tracing buffer. The function @{ML tap} can

  only be used for side-calculations, because any value that is computed

  cannot be merged back into the ``main waterfall''. To do this, you can use

  the next combinator.

  The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value

  and returns the result together with the value (as a pair). For example

  the function 

*}

ML{*fun inc_as_pair x =

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

       |> (fn (x, y) => (x, y + 1))*}

text {*

  takes @{text x} as argument, and then increments @{text x}, but also keeps

  @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"

  for x}. After that, the function increments the right-hand component of the

  pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.

  The combinators @{ML "|>>"} and @{ML "||>"} are defined for 

  functions manipulating pairs. The first applies the function to

  the first component of the pair, defined as

*}

ML{*fun (x, y) |>> f = (f x, y)*}

text {*

  and the second combinator to the second component, defined as

*}

ML{*fun (x, y) ||> f = (x, f y)*}

text {*

  With the combinator @{ML "|->"} you can re-combine the elements from a pair.

  This combinator is defined as

*}

ML{*fun (x, y) |-> f = f x y*}

text {* and can be used to write the following roundabout version 

  of the @{text double} function: 

*}

ML{*fun double x =

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

        |-> (fn x => fn y => x + y)*}

text {*

  Recall that @{ML "|>"} is the reverse function applications. Recall also that the related 

  reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},

  @{ML "|>>"} and @{ML "||>"} described above have related combinators for function

  composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, 

  for example, the function @{text double} can also be written as:

*}

ML{*val double =

            (fn x => (x, x))

        #-> (fn x => fn y => x + y)*}

text {*

  (FIXME: find a good exercise for combinators)

  \begin{readmore}

  The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}

  and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 

  contains further information about combinators.

  \end{readmore}

*}

section {* Antiquotations *}

text {*

  The main advantage of embedding all code in a theory is that the code can

  contain references to entities defined on the logical level of Isabelle. By

  this we mean definitions, theorems, terms and so on. This kind of reference is

  realised with antiquotations.  For example, one can print out the name of the current

  theory by typing

  @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}

  where @{text "@{theory}"} is an antiquotation that is substituted with the

  current theory (remember that we assumed we are inside the theory 

  @{text FirstSteps}). The name of this theory can be extracted using

  the function @{ML "Context.theory_name"}. 

  Note, however, that antiquotations are statically linked, that is their value is

  determined at ``compile-time'', not ``run-time''. For example the function

*}

ML{*fun not_current_thyname () = Context.theory_name @{theory} *}

text {*

  does \emph{not} return the name of the current theory, if it is run in a 

  different theory. Instead, the code above defines the constant function 

  that always returns the string @{text [quotes] "FirstSteps"}, no matter where the

  function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is 

  \emph{not} replaced with code that will look up the current theory in 

  some data structure and return it. Instead, it is literally

  replaced with the value representing the theory name.

  In a similar way you can use antiquotations to refer to proved theorems: 

  @{text "@{thm \<dots>}"} for a single theorem

  @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}

  and @{text "@{thms \<dots>}"} for more than one

@{ML_response_fake [display,gray] "@{thms conj_ac}" 

"(?P \<and> ?Q) = (?Q \<and> ?P)

(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)

((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  

  You can also refer to the current simpset. To illustrate this we implement the

  function that extracts the theorem names stored in a simpset.

*}

ML{*fun get_thm_names_from_ss simpset =

let

  val ({rules,...}, _) = MetaSimplifier.rep_ss simpset

in

  map #name (Net.entries rules)

end*}

text {*

  The function @{ML rep_ss in MetaSimplifier} returns a record containing all

  information about the simpset. The rules of a simpset are stored in a

  \emph{discrimination net} (a data structure for fast indexing). From this

  net you can extract the entries using the function @{ML Net.entries}.

  You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored

  in the current simpset. This simpset can be referred to using the antiquotation

  @{text "@{simpset}"}.

  @{ML_response_fake [display,gray] 

  "get_thm_names_from_ss @{simpset}" 

  "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}

  Again, this way or referencing simpsets makes you independent from additions

  of lemmas to the simpset by the user that potentially cause loops.

  \begin{readmore}

  The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}

  and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented

  in @{ML_file "Pure/net.ML"}.

  \end{readmore}

  While antiquotations have many applications, they were originally introduced in order 

  to avoid explicit bindings for theorems such as:

*}

ML{*val allI = thm "allI" *}

text {*

  These bindings are difficult to maintain and also can be accidentally

  overwritten by the user. This often broke Isabelle

  packages. Antiquotations solve this problem, since they are ``linked''

  statically at compile-time.  However, this static linkage also limits their

  usefulness in cases where data needs to be build up dynamically. In the

  course of this chapter you will learn more about these antiquotations:

  they can simplify Isabelle programming since one can directly access all

  kinds of logical elements from th ML-level.

*}

section {* Terms and Types *}

text {*

  One way to construct terms of Isabelle is by using the antiquotation 

  \mbox{@{text "@{term \<dots>}"}}. For example:

  @{ML_response [display,gray] 

"@{term \"(a::nat) + b = c\"}" 

"Const (\"op =\", \<dots>) $ 

  (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}

  This will show the term @{term "(a::nat) + b = c"}, but printed using the internal

  representation of this term. This internal representation corresponds to the 

  datatype @{ML_type "term"}.

  The internal representation of terms uses the usual de Bruijn index mechanism where bound 

  variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to

  the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that

  binds the corresponding variable. However, in Isabelle the names of bound variables are 

  kept at abstractions for printing purposes, and so should be treated only as ``comments''. 

  Application in Isabelle is realised with the term-constructor @{ML $}.

  \begin{readmore}

  Terms are described in detail in \isccite{sec:terms}. Their

  definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.

  \end{readmore}

  Sometimes the internal representation of terms can be surprisingly different

  parsing/type-checking/pretty printing can be quite elaborate. 

  \begin{exercise}

  Look at the internal term representation of the following terms, and

  find out why they are represented like this:

  \begin{itemize}

  \item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"}  

  \item @{term "\<lambda>(x,y). P y x"}  

  \item @{term "{ [x::int] | x. x \<le> -2 }"}  

  \end{itemize}