theory FirstSteps

imports Base

begin

(*<*)

setup{*

open_file_with_prelude 

  "FirstSteps_Code.thy"

  ["theory FirstSteps", "imports Main", "begin"]

*}

(*>*)

chapter {* First Steps *}

text {*

   \begin{flushright}

  {\em

  ``We will most likely never realize the full importance of painting the Tower,\\ 

  that it is the essential element in the conservation of metal works and the\\ 

  more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]

  Gustave Eiffel, In his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been 

  re-painted 18 times since its initial construction, an average of once every 

  seven years. It takes more than one year for a team of 25 painters to paint the tower 

  from top to bottom.}

  \end{flushright}

  \medskip

  Isabelle programming is done in ML. 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} FirstSteps\\

  \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.

*}

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 = Unsynchronized.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).

  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 {* Printing and Debugging\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_ind  "writeln"}. For example

  @{ML_response_eq [display,gray] "writeln \"any string\"" "\"any string\"" with "(op =)"}

  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_ind  makestring in PolyML}:

  @{ML_response_eq [display,gray] "writeln (PolyML.makestring 1)" "\"1\"" with "(op =)"} 

  However, @{ML 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_ind  tracing} is more appropriate. This function writes all

  output into a separate tracing buffer. For example:

  @{ML_response_eq [display,gray] "tracing \"foo\"" "\"foo\"" with "(op =)"}

  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 now

  @{ML [display,gray] "redirect_tracing (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_ind  error}; for 

  example:

  @{ML_response_fake [display,gray] 

  "if 0=1 then true else (error \"foo\")" 

"Exception- ERROR \"foo\" raised

At command \"ML\"."}

  This function raises the exception @{text ERROR}, which will then 

  be displayed by the infrastructure.

  \footnote{\bf FIXME Mention how to work with @{ML_ind  debug in Toplevel} and 

  @{ML_ind  profiling in Toplevel}.}

*}

(* FIXME

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 Isabelle's basic data

  structures, namely @{ML_type term}, @{ML_type cterm} and @{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 a bit unwieldy. One way to transform a term into a string is to use the

  function @{ML_ind  string_of_term in Syntax} in the structure @{ML_struct

  Syntax}. For more convenience, we bind this function to the toplevel.

*}

ML{*val string_of_term = Syntax.string_of_term*}

text {*

  It can now be used as follows

  @{ML_response_fake [display,gray]

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

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

  We obtain a string corrsponding to the term @{term [show_types] "1::nat"} with some

  additional information encoded in it. The string can be properly printed by

  using either the function @{ML_ind  writeln} or @{ML_ind  tracing}:

  @{ML_response_fake [display,gray]

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

  "\"1\""}

  or

  @{ML_response_fake [display,gray]

  "tracing (string_of_term @{context} @{term \"1::nat\"})"

  "\"1\""}

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

  function @{ML_ind  commas} to separate them.

*} 

ML{*fun string_of_terms ctxt ts =  

  commas (map (string_of_term ctxt) ts)*}

text {*

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

*}

ML{*fun string_of_cterm ctxt ct =  

  string_of_term ctxt (term_of ct)*}

text {*

  In this example the function @{ML_ind term_of} extracts the @{ML_type

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

  printed with @{ML_ind commas}.

*} 

ML{*fun string_of_cterms ctxt cts =  

  commas (map (string_of_cterm ctxt) cts)*}

text {*

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

*}

ML{*fun string_of_thm ctxt thm =

  string_of_term ctxt (prop_of thm)*}

text {*

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

  @{text "?Q"} and so on. They are needed in Isabelle in order to able to

  instantiate theorems when they are applied. For example the theorem 

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

  instantiation of @{text "?P"} and @{text "?Q"}. 

  @{ML_response_fake [display, gray]

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

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

  However, in order to improve the readability when printing theorems, we

  convert these schematic variables into free variables using the function

  @{ML_ind  import in Variable}. This is similar to statements like @{text

  "conjI[no_vars]"} on Isabelle's user-level.

*}

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_term ctxt (prop_of (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) *}

text {*

  Note that when printing out several ``parcels'' of information that

  semantically belong together, like a warning message consisting of 

  a term and its type, you should try to keep this information together in a

  single string. Therefore do \emph{not} print out information as

@{ML_response_fake [display,gray]

"tracing \"First half,\"; 

tracing \"and second half.\""

"First half,

and second half."}

  but as a single string with appropriate formatting. For example

@{ML_response_fake [display,gray]

"tracing (\"First half,\" ^ \"\\n\" ^ \"and second half.\")"

"First half,

and second half."}

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

  of library functions. For example,  the function @{ML_ind  cat_lines}

  concatenates a list of strings and inserts newlines. 

  @{ML_response [display, gray]

  "cat_lines [\"foo\", \"bar\"]"

  "\"foo\\nbar\""}

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

  that helps with more elaborate pretty printing. 

  \begin{readmore}

  Most of the basic string functions of Isabelle are defined in 

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

  \end{readmore}

*}

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_ind I in Basic_Library}, which is just the 

  identity function defined as

*}

ML{*fun I x = x*}

text {* 

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

*}

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

text {*

  @{ML K} ``wraps'' a function around @{text "x"} that ignores its argument. As a 

  result, @{ML K} defines a constant function always returning @{text x}.

  The next combinator is reverse application, @{ML_ind  "|>" in Basics}, 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 {\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 three 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

   |> 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_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 @{text "[nat, int, unit]"}); Line

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

  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_ind list_comb in Term} to the 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. 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