1 theory First_Steps

     2 imports Base

     3 begin

     4 

     5 (*<*)

     6 setup{*

     7 open_file_with_prelude 

     8   "First_Steps_Code.thy"

     9   ["theory First_Steps", "imports Main", "begin"]

    10 *}

    11 (*>*)

    12 

    13 chapter {* First Steps\label{chp:firststeps} *}

    14 

    15 text {*

    16    \begin{flushright}

    17   {\em

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

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

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

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

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

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

    24   from top to bottom.}

    25   \end{flushright}

    26 

    27   \medskip

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

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

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

    31 

    32   \begin{quote}

    33   \begin{tabular}{@ {}l}

    34   \isacommand{theory} First\_Steps\\

    35   \isacommand{imports} Main\\

    36   \isacommand{begin}\\

    37   \ldots

    38   \end{tabular}

    39   \end{quote}

    40 

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

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

    43 *}

    44 

    45 section {* Including ML-Code\label{sec:include} *}

    46 

    47 text {*

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

    49   \isacommand{ML}-command. For example:

    50 

    51   \begin{isabelle}

    52   \begin{graybox}

    53   \isacommand{ML}~@{text "\<verbopen>"}\isanewline

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

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

    56   @{text "> 7"}\smallskip

    57   \end{graybox}

    58   \end{isabelle}

    59 

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

    61   using the advance and undo buttons of your Isabelle environment. The code

    62   inside the \isacommand{ML}-command can also contain value and function

    63   bindings, for example

    64 *}

    65 

    66 ML %gray {* 

    67   val r = Unsynchronized.ref 0

    68   fun f n = n + 1 

    69 *}

    70 

    71 text {*

    72   and even those can be undone when the proof script is retracted.  As

    73   mentioned in the Introduction, we will drop the \isacommand{ML}~@{text

    74   "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we show code. The lines

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

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

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

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

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

    80   ML-code is defined inside a proof. For example

    81 

    82   \begin{quote}

    83   \begin{isabelle}

    84   \isacommand{lemma}~@{text "test:"}\isanewline

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

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

    87   \isacommand{oops}

    88   \end{isabelle}

    89   \end{quote}

    90 

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

    92   always arrange that the ML-code is defined outside proofs).

    93 

    94   

    95 

    96 

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

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

    99   theory by using the command \isacommand{use}. For example

   100 

   101   \begin{quote}

   102   \begin{tabular}{@ {}l}

   103   \isacommand{theory} First\_Steps\\

   104   \isacommand{imports} Main\\

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

   106   \isacommand{begin}\\

   107   \ldots\\

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

   109   \ldots

   110   \end{tabular}

   111   \end{quote}

   112 

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

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

   115   file can be included by just writing in the header

   116 

   117   \begin{quote}

   118   \begin{tabular}{@ {}l}

   119   \isacommand{theory} First\_Steps\\

   120   \isacommand{imports} Main\\

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

   122   \isacommand{begin}\\

   123   \ldots

   124   \end{tabular}

   125   \end{quote}

   126 

   127   Note that no parentheses are given in this case. Note also that the included

   128   ML-file should not contain any \isacommand{use} itself. Otherwise Isabelle

   129   is unable to record all file dependencies, which is a nuisance if you have

   130   to track down errors.

   131 *}

   132 

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

   134 

   135 text {*

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

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

   138   @{ML_ind writeln in Output}. For example

   139 

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

   141 

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

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

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

   145   for converting values into strings, namely the antiquotation 

   146   @{text "@{make_string}"}:

   147 

   148   @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""} 

   149 

   150   However, @{text "@{makes_tring}"} only works if the type of what

   151   is converted is monomorphic and not a function.

   152 

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

   154   because any output this function generates will be overwritten as soon as an

   155   error is raised. For printing anything more serious and elaborate, the

   156   function @{ML_ind tracing in Output} is more appropriate. This function writes all

   157   output into a separate tracing buffer. For example:

   158 

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

   160 

   161   It is also possible to redirect the ``channel'' where the string @{text

   162   "foo"} is printed to a separate file, e.g., in order to prevent ProofGeneral from

   163   choking on massive amounts of trace output. This redirection can be achieved

   164   with the code:

   165 *}

   166 

   167 ML{*val strip_specials =

   168 let

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

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

   171     | strip [] = [];

   172 in 

   173   implode o strip o explode 

   174 end

   175 

   176 fun redirect_tracing stream =

   177  Output.tracing_fn := (fn s =>

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

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

   180      TextIO.flushOut stream)) *}

   181 

   182 text {*

   183   Calling now

   184 

   185   @{ML [display,gray] "redirect_tracing (TextIO.openOut \"foo.bar\")"}

   186 

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

   188 

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

   190   example:

   191 

   192   @{ML_response_fake [display,gray] 

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

   194 "Exception- ERROR \"foo\" raised

   195 At command \"ML\"."}

   196 

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

   198   be displayed by the infrastructure. Note that this exception is meant 

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

   200 

   201   For messages where you want to indicate a genuine program error, then

   202   use the exception @{text Fail}. Here the infrastructure indicates that this 

   203   is a low-level exception, and also prints the source position of the ML 

   204   raise statement. 

   205 

   206 

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

   208   @{ML_ind profiling in Toplevel}.}

   209 

   210 *}

   211 

   212 (* FIXME*)

   213 (*

   214 ML {* reset Toplevel.debug *}

   215 

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

   217 

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

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

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

   221 

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

   223 

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

   225 *)

   226 

   227 text {*

   228   %Kernel exceptions TYPE, TERM, THM also have their place in situations 

   229   %where kernel-like operations are involved.  The printing is similar as for 

   230   %Fail, although there is some special treatment when Toplevel.debug is 

   231   %enabled.

   232 

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

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

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

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

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

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

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

   240 *}

   241 

   242 ML{*val pretty_term = Syntax.pretty_term

   243 val pwriteln = Pretty.writeln*}

   244 

   245 text {*

   246   They can now be used as follows

   247 

   248   @{ML_response_fake [display,gray]

   249   "pwriteln (pretty_term @{context} @{term \"1::nat\"})"

   250   "\"1\""}

   251 

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

   253   function @{ML_ind enum in Pretty} and commas to separate them.

   254 *} 

   255 

   256 ML{*fun pretty_terms ctxt ts =  

   257   Pretty.enum "," "" "" (map (pretty_term ctxt) ts)*}

   258 

   259 text {*

   260   You can also print out terms together with their typing information.

   261   For this you need to set the reference @{ML_ind show_types in Syntax} 

   262   to @{ML true}.

   263 *}

   264 

   265 ML{*show_types := true*}

   266 

   267 text {*

   268   Now @{ML pretty_term} prints out

   269 

   270   @{ML_response_fake [display, gray]

   271   "pwriteln (pretty_term @{context} @{term \"(1::nat, x)\"})"

   272   "(1::nat, x::'a)"}

   273 

   274   where @{text 1} and @{text x} are displayed with their inferred type.

   275   Even more type information can be printed by setting 

   276   the reference @{ML_ind show_all_types in Syntax} to @{ML true}. 

   277   In this case we obtain

   278 *}

   279 (*<*)ML %linenos {*show_all_types := true*}

   280 (*>*)

   281 text {*

   282   @{ML_response_fake [display, gray]

   283   "pwriteln (pretty_term @{context} @{term \"(1::nat, x)\"})"

   284   "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}

   285 

   286   where @{term Pair} is the term-constructor for products. 

   287   Other references that influence printing of terms are 

   288   @{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}. 

   289 *}

   290 (*<*)ML %linenos {*show_types := false; show_all_types := false*}

   291 (*>*)

   292 text {*

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

   294 *}

   295 

   296 ML{*fun pretty_cterm ctxt ct =  

   297   pretty_term ctxt (term_of ct)*}

   298 

   299 text {*

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

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

   302   printed again with @{ML enum in Pretty}.

   303 *} 

   304 

   305 ML{*fun pretty_cterms ctxt cts =  

   306   Pretty.enum "," "" "" (map (pretty_cterm ctxt) cts)*}

   307 

   308 text {*

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

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

   311 *}

   312 

   313 ML{*fun pretty_thm ctxt thm =

   314   pretty_term ctxt (prop_of thm)*}

   315 

   316 text {*

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

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

   319   instantiate theorems when they are applied. For example the theorem 

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

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

   322 

   323   @{ML_response_fake [display, gray]

   324   "pwriteln (pretty_thm @{context} @{thm conjI})"

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

   326 

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

   328   convert these schematic variables into free variables using the function

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

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

   331 *}

   332 

   333 ML{*fun no_vars ctxt thm =

   334 let 

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

   336 in

   337   thm'

   338 end

   339 

   340 fun pretty_thm_no_vars ctxt thm =

   341   pretty_term ctxt (prop_of (no_vars ctxt thm))*}

   342 

   343 

   344 text {* 

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

   346 

   347   @{ML_response_fake [display, gray]

   348   "pwriteln (pretty_thm_no_vars @{context} @{thm conjI})"

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

   350   

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

   352 *}

   353 

   354 ML{*fun pretty_thms ctxt thms =  

   355   Pretty.enum "," "" "" (map (pretty_thm ctxt) thms)

   356 

   357 fun pretty_thms_no_vars ctxt thms =  

   358   Pretty.enum "," "" "" (map (pretty_thm_no_vars ctxt) thms)*}

   359 

   360 text {*

   361   The printing functions for types are

   362 *}

   363 

   364 ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty

   365 fun pretty_typs ctxt tys = Pretty.commas (map (pretty_typ ctxt) tys)*}

   366 

   367 text {*

   368   respectively ctypes

   369 *}

   370 

   371 ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)

   372 fun pretty_ctyps ctxt ctys = Pretty.commas (map (pretty_ctyp ctxt) ctys)*}

   373 

   374 text {*

   375   \begin{readmore}

   376   The simple conversion functions from Isabelle's main datatypes to 

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

   378   The references that change the printing information are declared in 

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

   380   \end{readmore}

   381 

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

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

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

   385   \emph{not} print out information as

   386 

   387 @{ML_response_fake [display,gray]

   388 "writeln \"First half,\"; 

   389 writeln \"and second half.\""

   390 "First half,

   391 and second half."}

   392 

   393   but as a single string with appropriate formatting. For example

   394 

   395 @{ML_response_fake [display,gray]

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

   397 "First half,

   398 and second half."}

   399   

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

   401   of library functions in Isabelle. For example,  the function 

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

   403   and inserts newlines in between each element. 

   404 

   405   @{ML_response_fake [display, gray]

   406   "writeln (cat_lines [\"foo\", \"bar\"])"

   407   "foo

   408 bar"}

   409 

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

   411   provides for more elaborate pretty printing. 

   412 

   413   \begin{readmore}

   414   Most of the basic string functions of Isabelle are defined in 

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

   416   \end{readmore}

   417 *}

   418 

   419 

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

   421 

   422 text {*

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

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

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

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

   427 

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

   429   identity function defined as

   430 *}

   431 

   432 ML{*fun I x = x*}

   433 

   434 text {* 

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

   436 *}

   437 

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

   439 

   440 text {*

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

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

   443 

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

   445 *}

   446 

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

   448 

   449 text {* While just syntactic sugar for the usual function application,

   450   the purpose of this combinator is to implement functions in a  

   451   ``waterfall fashion''. Consider for example the function *}

   452 

   453 ML %linenosgray{*fun inc_by_five x =

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

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

   456     |> fst

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

   458 

   459 text {*

   460   which increments its argument @{text x} by 5. It does this by first

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

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

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

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

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

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

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

   468   the reverse application is much clearer than writing

   469 *}

   470 

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

   472 

   473 text {* or *}

   474 

   475 ML{*fun inc_by_five x = 

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

   477 

   478 text {* and typographically more economical than *}

   479 

   480 ML{*fun inc_by_five x =

   481 let val y1 = x + 1

   482     val y2 = (y1, y1)

   483     val y3 = fst y2

   484     val y4 = y3 + 4

   485 in y4 end*}

   486 

   487 text {* 

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

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

   490   mention the nightmares the maintenance of this code causes!

   491 

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

   493   the waterfall fashion might be the following code:

   494 *}

   495 

   496 ML %linenosgray{*fun apply_fresh_args f ctxt =

   497     f |> fastype_of

   498       |> binder_types 

   499       |> map (pair "z")

   500       |> Variable.variant_frees ctxt [f]

   501       |> map Free  

   502       |> curry list_comb f *}

   503 

   504 text {*

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

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

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

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

   509 

   510   @{ML_response_fake [display,gray]

   511 "let

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

   513   val ctxt = @{context}

   514 in 

   515   apply_fresh_args trm ctxt

   516    |> pretty_term ctxt

   517    |> pwriteln

   518 end" 

   519   "P z za zb"}

   520 

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

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

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

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

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

   526   variant_frees in Variable} generates for each @{text "z"} a unique name

   527   avoiding the given @{text f}; the list of name-type pairs is turned into a

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

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

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

   531   expects the function and the variables list as a pair. 

   532   

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

   534   terms involving fresh variables. For this the infrastructure helps

   535   tremendously to avoid any name clashes. Consider for example:

   536 

   537    @{ML_response_fake [display,gray]

   538 "let

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

   540   val ctxt = @{context}

   541 in

   542   apply_fresh_args trm ctxt 

   543    |> pretty_term ctxt

   544    |> pwriteln

   545 end"

   546   "za z zb"}

   547   

   548   where the @{text "za"} is correctly avoided.

   549 

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

   551   It can be used to define the following function

   552 *}

   553 

   554 ML{*val inc_by_six = 

   555   (fn x => x + 1) #> 

   556   (fn x => x + 2) #> 

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

   558 

   559 text {* 

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

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

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

   563   is often used for setup functions inside the

   564   \isacommand{setup}-command. These functions have to be of type @{ML_type

   565   "theory -> theory"}. More than one such setup function can be composed with

   566   @{ML "#>"}. For example

   567 *}

   568 

   569 setup %gray {* let

   570   val (ival1, setup_ival1) = Attrib.config_int "ival1" (K 1)

   571   val (ival2, setup_ival2) = Attrib.config_int "ival2" (K 2)

   572 in

   573   setup_ival1 #>

   574   setup_ival2

   575 end *}

   576 

   577 text {*

   578   after this the configuration values @{text ival1} and @{text ival2} are known

   579   in the current theory and can be manipulated by the user (for more information 

   580   about configuration values see Section~\ref{sec:storing}, for more about setup 

   581   functions see Section~\ref{sec:theories}). 

   582   

   583   The remaining combinators we describe in this section add convenience for the

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

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

   586   side-calculations for instance). The function

   587  *}

   588 

   589 ML %linenosgray{*fun inc_by_three x =

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

   591        |> tap (fn x => tracing (PolyML.makestring x))

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

   593 

   594 text {* 

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

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

   597   intermediate result. The function @{ML tap} can only be used for

   598   side-calculations, because any value that is computed cannot be merged back

   599   into the ``main waterfall''. To do this, you can use the next combinator.

   600 

   601   The combinator @{ML_ind "`" in Basics} (a backtick) is similar to @{ML tap},

   602   but applies a function to the value and returns the result together with the

   603   value (as a pair). It is defined as

   604 *}

   605 

   606 ML{*fun `f = fn x => (f x, x)*}

   607 

   608 text {*

   609   An example for this combinator is the function

   610 *}

   611 

   612 ML{*fun inc_as_pair x =

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

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

   615 

   616 text {*

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

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

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

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

   621 

   622   The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are

   623   defined for functions manipulating pairs. The first applies the function to

   624   the first component of the pair, defined as

   625 *}

   626 

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

   628 

   629 text {*

   630   and the second combinator to the second component, defined as

   631 *}

   632 

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

   634 

   635 text {*

   636   These two functions can, for example, be used to avoid explicit @{text "lets"} for

   637   intermediate values in functions that return pairs. As an example, suppose you

   638   want to separate a list of integers into two lists according to a

   639   threshold. If the threshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}

   640   should be separated as @{ML "([1,2,3,4], [6,5])"}.  Such a function can be

   641   implemented as

   642 *}

   643 

   644 ML{*fun separate i [] = ([], [])

   645   | separate i (x::xs) =

   646       let 

   647         val (los, grs) = separate i xs

   648       in

   649         if i <= x then (los, x::grs) else (x::los, grs)

   650       end*}

   651 

   652 text {*

   653   where the return value of the recursive call is bound explicitly to

   654   the pair @{ML "(los, grs)" for los grs}. However, this function

   655   can be implemented more concisely as

   656 *}

   657 

   658 ML{*fun separate i [] = ([], [])

   659   | separate i (x::xs) =

   660       if i <= x 

   661       then separate i xs ||> cons x

   662       else separate i xs |>> cons x*}

   663 

   664 text {*

   665   avoiding the explicit @{text "let"}. While in this example the gain in

   666   conciseness is only small, in more complicated situations the benefit of

   667   avoiding @{text "lets"} can be substantial.

   668 

   669   With the combinator @{ML_ind "|->" in Basics} you can re-combine the 

   670   elements from a pair. This combinator is defined as

   671 *}

   672 

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

   674 

   675 text {* 

   676   and can be used to write the following roundabout version 

   677   of the @{text double} function: 

   678 *}

   679 

   680 ML{*fun double x =

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

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

   683 

   684 text {* 

   685   The combinator @{ML_ind ||>> in Basics} plays a central rôle whenever your

   686   task is to update a theory and the update also produces a side-result (for

   687   example a theorem). Functions for such tasks return a pair whose second

   688   component is the theory and the fist component is the side-result. Using

   689   @{ML ||>>}, you can do conveniently the update and also

   690   accumulate the side-results. Consider the following simple function.

   691 *}

   692 

   693 ML %linenosgray{*fun acc_incs x =

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

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

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

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

   698 

   699 text {*

   700   The purpose of Line 2 is to just pair up the argument with a dummy value (since

   701   @{ML ||>>} operates on pairs). Each of the next three lines just increment 

   702   the value by one, but also nest the intermediate results to the left. For example 

   703 

   704   @{ML_response [display,gray]

   705   "acc_incs 1"

   706   "((((\"\", 1), 2), 3), 4)"}

   707 

   708   You can continue this chain with:

   709   

   710   @{ML_response [display,gray]

   711   "acc_incs 1 ||>> (fn x => (x, x + 2))"

   712   "(((((\"\", 1), 2), 3), 4), 6)"}

   713 

   714   \footnote{\bf FIXME: maybe give a ``real world'' example for this combinator.}

   715 *}

   716 

   717 text {*

   718   Recall that @{ML "|>"} is the reverse function application. Recall also that

   719   the related reverse function composition is @{ML "#>"}. In fact all the

   720   combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}

   721   described above have related combinators for function composition, namely

   722   @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in

   723   Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the

   724   function @{text double} can also be written as:

   725 *}

   726 

   727 ML{*val double =

   728             (fn x => (x, x))

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

   730 

   731 

   732 text {* 

   733   When using combinators for writing functions in waterfall fashion, it is

   734   sometimes necessary to do some ``plumbing'' in order to fit functions

   735   together. We have already seen such plumbing in the function @{ML

   736   apply_fresh_args}, where @{ML curry} is needed for making the function @{ML

   737   list_comb}, which works over pairs, to fit with the combinator @{ML "|>"}. Such 

   738   plumbing is also needed in situations where a function operates over lists, 

   739   but one calculates only with a single element. An example is the function 

   740   @{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check 

   741   a list of terms. Consider the code:

   742 

   743   @{ML_response_fake [display, gray]

   744   "let

   745   val ctxt = @{context}

   746 in

   747   map (Syntax.parse_term ctxt) [\"m + n\", \"m * n\", \"m - (n::nat)\"] 

   748   |> Syntax.check_terms ctxt

   749   |> pretty_terms ctxt

   750   |> pwriteln

   751 end"

   752   "m + n, m * n, m - n"}

   753 *}

   754 

   755 text {*

   756   In this example we obtain three terms (using the function 

   757   @{ML_ind parse_term in Syntax}) whose variables @{text m} and @{text n} 

   758   are of type @{typ "nat"}. If you have only a single term, then @{ML

   759   check_terms in Syntax} needs plumbing. This can be done with the function

   760   @{ML_ind singleton in Library}.\footnote{There is already a function @{ML check_term in

   761   Syntax} in the file @{ML_file "Pure/Syntax/syntax.ML"} that is implemented 

   762   in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example

   763 

   764   @{ML_response_fake [display, gray, linenos]

   765   "let 

   766   val ctxt = @{context}

   767 in

   768   Syntax.parse_term ctxt \"m - (n::nat)\" 

   769   |> singleton (Syntax.check_terms ctxt)

   770   |> pretty_term ctxt

   771   |> pwriteln

   772 end"

   773   "m - n"}

   774    

   775   where in Line 5, the function operating over lists fits with the

   776   single term generated in Line 4.

   777 

   778   \begin{readmore}

   779   The most frequently used combinators are defined in the files @{ML_file

   780   "Pure/library.ML"}

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

   782   contains further information about combinators.

   783   \end{readmore}

   784 

   785   \footnote{\bf FIXME: find a good exercise for combinators}

   786   \begin{exercise}

   787   Find out what the combinator @{ML "K I"} does.

   788   \end{exercise}

   789 

   790 

   791   \footnote{\bf FIXME: say something about calling conventions} 

   792 *}

   793 

   794 

   795 section {* ML-Antiquotations\label{sec:antiquote} *}

   796 

   797 text {*

   798   Recall from Section \ref{sec:include} that code in Isabelle is always

   799   embedded in a theory.  The main advantage of this is that the code can

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

   801   this we mean references to definitions, theorems, terms and so on. These

   802   reference are realised in Isabelle with ML-antiquotations, often just called

   803   antiquotations.\footnote{Note that there are two kinds of antiquotations in

   804   Isabelle, which have very different purposes and infrastructures. The first

   805   kind, described in this section, are \emph{\index*{ML-antiquotation}}. They

   806   are used to refer to entities (like terms, types etc) from Isabelle's logic

   807   layer inside ML-code. The other kind of antiquotations are

   808   \emph{document}\index{document antiquotation} antiquotations. They are used

   809   only in the text parts of Isabelle and their purpose is to print logical

   810   entities inside \LaTeX-documents. Document antiquotations are part of the

   811   user level and therefore we are not interested in them in this Tutorial,

   812   except in Appendix \ref{rec:docantiquotations} where we show how to

   813   implement your own document antiquotations.}  Syntactically antiquotations

   814   are indicated by the @{ML_text @}-sign followed by text wrapped in @{text

   815   "{\<dots>}"}.  For example, one can print out the name of the current theory with

   816   the code

   817   

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

   819  

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

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

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

   823   the function @{ML_ind theory_name in Context}. 

   824 

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

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

   827 *}

   828 

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

   830 

   831 text {*

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

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

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

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

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

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

   838   replaced with the value representing the theory.

   839 

   840   Another important antiquotation is @{text "@{context}"}. (What the

   841   difference between a theory and a context is will be described in Chapter

   842   \ref{chp:advanced}.) A context is for example needed in order to use the

   843   function @{ML print_abbrevs in ProofContext} that list of all currently

   844   defined abbreviations.

   845 

   846   @{ML_response_fake [display, gray]

   847   "ProofContext.print_abbrevs @{context}"

   848 "Code_Evaluation.valtermify \<equiv> \<lambda>x. (x, \<lambda>u. Code_Evaluation.termify x)

   849 INTER \<equiv> INFI

   850 Inter \<equiv> Inf

   851 \<dots>"}

   852 

   853   You can also use antiquotations to refer to proved theorems: 

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

   855 

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

   857 

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

   859 

   860 @{ML_response_fake [display,gray] 

   861   "@{thms conj_ac}" 

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

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

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

   865 

   866   The thm-antiquotations can also be used for manipulating theorems. For 

   867   example, if you need the version of te theorem @{thm [source] refl} that 

   868   has a meta-equality instead of an equality, you can write

   869 

   870 @{ML_response_fake [display,gray] 

   871   "@{thm refl[THEN eq_reflection]}"

   872   "?x \<equiv> ?x"}

   873 

   874   The point of these antiquotations is that referring to theorems in this way

   875   makes your code independent from what theorems the user might have stored

   876   under this name (this becomes especially important when you deal with

   877   theorem lists; see Section \ref{sec:storing}).

   878 

   879   It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"}

   880   whose first argument is a statement (possibly many of them separated by @{text "and"})

   881   and the second is a proof. For example

   882 *}

   883 

   884 ML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}

   885 

   886 text {*

   887   The result can be printed out as follows.

   888 

   889   @{ML_response_fake [gray,display]

   890 "foo_thm |> pretty_thms_no_vars @{context}

   891         |> pwriteln"

   892   "True, False \<Longrightarrow> P"}

   893 

   894   You can also refer to the current simpset via an antiquotation. To illustrate 

   895   this we implement the function that extracts the theorem names stored in a 

   896   simpset.

   897 *}

   898 

   899 ML{*fun get_thm_names_from_ss simpset =

   900 let

   901   val {simps,...} = MetaSimplifier.dest_ss simpset

   902 in

   903   map #1 simps

   904 end*}

   905 

   906 text {*

   907   The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing all

   908   information stored in the simpset, but here we are only interested in the names of the

   909   simp-rules. Now you can feed in the current simpset into this function. 

   910   The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.

   911 

   912   @{ML_response_fake [display,gray] 

   913   "get_thm_names_from_ss @{simpset}" 

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

   915 

   916   Again, this way of referencing simpsets makes you independent from additions

   917   of lemmas to the simpset by the user, which can potentially cause loops in your

   918   code.

   919 

   920   It is also possible to define your own antiquotations. But you should

   921   exercise care when introducing new ones, as they can also make your code

   922   also difficult to read. In the next chapter we describe how to construct

   923   terms with the (build in) antiquotation @{text "@{term \<dots>}"}.  A restriction

   924   of this antiquotation is that it does not allow you to use schematic

   925   variables in terms. If you want to have an antiquotation that does not have

   926   this restriction, you can implement your own using the function @{ML_ind

   927   inline in ML_Antiquote} from the structure @{ML_struct ML_Antiquote}. The code

   928   for the antiquotation @{text "term_pat"} is as follows.

   929 *}

   930 

   931 ML %linenosgray{*let

   932   val parser = Args.context -- Scan.lift Args.name_source

   933 

   934   fun term_pat (ctxt, str) =

   935      str |> ProofContext.read_term_pattern ctxt

   936          |> ML_Syntax.print_term

   937          |> ML_Syntax.atomic

   938 in

   939   ML_Antiquote.inline "term_pat" (parser >> term_pat)

   940 end*}

   941 

   942 text {*

   943   The parser in Line 2 provides us with a context and a string; this string is

   944   transformed into a term using the function @{ML_ind read_term_pattern in

   945   ProofContext} (Line 5); the next two lines transform the term into a string

   946   so that the ML-system can understand it. (All these functions will be explained

   947   in more detail in later sections.) An example for this antiquotation is:

   948 

   949   @{ML_response_fake [display,gray]

   950   "@{term_pat \"Suc (?x::nat)\"}"

   951   "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}

   952 

   953   which shows the internal representation of the term @{text "Suc ?x"}. Similarly

   954   we can write an antiquotation for type patterns.

   955 *}

   956 

   957 ML{*let

   958   val parser = Args.context -- Scan.lift Args.name_source

   959 

   960   fun typ_pat (ctxt, str) =

   961      str |> Syntax.parse_typ ctxt

   962          |> ML_Syntax.print_typ

   963          |> ML_Syntax.atomic

   964 in

   965   ML_Antiquote.inline "typ_pat" (parser >> typ_pat)

   966 end*}

   967 

   968 text {*

   969   \begin{readmore}

   970   The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions

   971   for most antiquotations. Most of the basic operations on ML-syntax are implemented 

   972   in @{ML_file "Pure/ML/ml_syntax.ML"}.

   973   \end{readmore}

   974 *}

   975 

   976 section {* Storing Data in Isabelle\label{sec:storing} *}

   977 

   978 text {*

   979   Isabelle provides mechanisms for storing (and retrieving) arbitrary

   980   data. Before we delve into the details, let us digress a bit. Conventional

   981   wisdom has it that the type-system of ML ensures that  an

   982   @{ML_type "'a list"}, say, can only hold elements of the same type, namely

   983   @{ML_type "'a"}. Despite this wisdom, however, it is possible to implement a

   984   universal type in ML, although by some arguably accidental features of ML.

   985   This universal type can be used to store data of different type into a single list.

   986   In fact, it allows one to inject and to project data of \emph{arbitrary} type. This is

   987   in contrast to datatypes, which only allow injection and projection of data for

   988   some \emph{fixed} collection of types. In light of the conventional wisdom cited

   989   above it is important to keep in mind that the universal type does not

   990   destroy type-safety of ML: storing and accessing the data can only be done

   991   in a type-safe manner.

   992 

   993   \begin{readmore}

   994   In Isabelle the universal type is implemented as the type @{ML_type

   995   Universal.universal} in the file

   996   @{ML_file "Pure/ML-Systems/universal.ML"}.

   997   \end{readmore}

   998 

   999   We will show the usage of the universal type by storing an integer and

  1000   a boolean into a single list. Let us first define injection and projection 

  1001   functions for booleans and integers into and from the type @{ML_type Universal.universal}.

  1002 *}

  1003 

  1004 ML{*local

  1005   val fn_int  = Universal.tag () : int  Universal.tag

  1006   val fn_bool = Universal.tag () : bool Universal.tag

  1007 in

  1008   val inject_int   = Universal.tagInject fn_int;

  1009   val inject_bool  = Universal.tagInject fn_bool;

  1010   val project_int  = Universal.tagProject fn_int;

  1011   val project_bool = Universal.tagProject fn_bool

  1012 end*}

  1013 

  1014 text {*

  1015   Using the injection functions, we can inject the integer @{ML_text "13"} 

  1016   and the boolean value @{ML_text "true"} into @{ML_type Universal.universal}, and

  1017   then store them in a @{ML_type "Universal.universal list"} as follows:

  1018 *}

  1019 

  1020 ML{*val foo_list = 

  1021 let

  1022   val thirteen  = inject_int 13

  1023   val truth_val = inject_bool true

  1024 in

  1025   [thirteen, truth_val]

  1026 end*}

  1027 

  1028 text {*

  1029   The data can be retrieved with the projection functions defined above.

  1030   

  1031   @{ML_response_fake [display, gray]

  1032 "project_int (nth foo_list 0); 

  1033 project_bool (nth foo_list 1)" 

  1034 "13

  1035 true"}

  1036 

  1037   Notice that we access the integer as an integer and the boolean as

  1038   a boolean. If we attempt to access the integer as a boolean, then we get 

  1039   a runtime error. 

  1040   

  1041   @{ML_response_fake [display, gray]

  1042 "project_bool (nth foo_list 0)"  

  1043 "*** Exception- Match raised"}

  1044 

  1045   This runtime error is the reason why ML is still type-sound despite

  1046   containing a universal type.

  1047 

  1048   Now, Isabelle heavily uses this mechanism for storing all sorts of

  1049   data: theorem lists, simpsets, facts etc.  Roughly speaking, there are two

  1050   places where data can be stored in Isabelle: in \emph{theories} and in \emph{proof

  1051   contexts}. Data such as simpsets are ``global'' and therefore need to be stored

  1052   in a theory (simpsets need to be maintained across proofs and even across

  1053   theories).  On the other hand, data such as facts change inside a proof and

  1054   are only relevant to the proof at hand. Therefore such data needs to be 

  1055   maintained inside a proof context, which represents ``local'' data.

  1056 

  1057   For theories and proof contexts there are, respectively, the functors 

  1058   @{ML_funct_ind Theory_Data} and @{ML_funct_ind Proof_Data} that help

  1059   with the data storage. Below we show how to implement a table in which you

  1060   can store theorems and look them up according to a string key. The

  1061   intention in this example is to be able to look up introduction rules for logical

  1062   connectives. Such a table might be useful in an automatic proof procedure

  1063   and therefore it makes sense to store this data inside a theory.  

  1064   Consequently we use the functor @{ML_funct Theory_Data}.

  1065   The code for the table is:

  1066 *}

  1067 

  1068 ML %linenosgray{*structure Data = Theory_Data

  1069   (type T = thm Symtab.table

  1070    val empty = Symtab.empty

  1071    val extend = I

  1072    val merge = Symtab.merge (K true))*}

  1073 

  1074 text {*

  1075   In order to store data in a theory, we have to specify the type of the data

  1076   (Line 2). In this case we specify the type @{ML_type "thm Symtab.table"},

  1077   which stands for a table in which @{ML_type string}s can be looked up

  1078   producing an associated @{ML_type thm}. We also have to specify four

  1079   functions to use this functor: namely how to initialise the data storage

  1080   (Line 3), how to extend it (Line 4) and how two

  1081   tables should be merged (Line 5). These functions correspond roughly to the

  1082   operations performed on theories and we just give some sensible 

  1083   defaults.\footnote{\bf FIXME: Say more about the

  1084   assumptions of these operations.} The result structure @{ML_text Data}

  1085   contains functions for accessing the table (@{ML Data.get}) and for updating

  1086   it (@{ML Data.map}). There is also the functions @{ML Data.put}, which however is 

  1087   not relevant here. Below we define two

  1088   auxiliary functions, which help us with accessing the table.

  1089 *}

  1090 

  1091 ML{*val lookup = Symtab.lookup o Data.get

  1092 fun update k v = Data.map (Symtab.update (k, v))*}

  1093 

  1094 text {*

  1095   Since we want to store introduction rules associated with their 

  1096   logical connective, we can fill the table as follows.

  1097 *}

  1098 

  1099 setup %gray {*

  1100   update "op &"   @{thm conjI} #>

  1101   update "op -->" @{thm impI}  #>

  1102   update "All"    @{thm allI}

  1103 *}

  1104 

  1105 text {*

  1106   The use of the command \isacommand{setup} makes sure the table in the 

  1107   \emph{current} theory is updated (this is explained further in 

  1108   section~\ref{sec:theories}). The lookup can now be performed as follows.

  1109 

  1110   @{ML_response_fake [display, gray]

  1111 "lookup @{theory} \"op &\""

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

  1113 

  1114   An important point to note is that these tables (and data in general)

  1115   need to be treated in a purely functional fashion. Although

  1116   we can update the table as follows

  1117 *}

  1118 

  1119 setup %gray {* update "op &" @{thm TrueI} *}

  1120 

  1121 text {*

  1122   and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}

  1123   

  1124 @{ML_response_fake [display, gray]

  1125 "lookup @{theory} \"op &\""

  1126 "SOME \"True\""}

  1127 

  1128   there are no references involved. This is one of the most fundamental

  1129   coding conventions for programming in Isabelle. References  

  1130   interfere with the multithreaded execution model of Isabelle and also

  1131   defeat its undo-mechanism. To see the latter, consider the 

  1132   following data container where we maintain a reference to a list of 

  1133   integers.

  1134 *}