1 theory FirstSteps

     2 imports Base

     3 begin

     4 

     5 (*<*)

     6 setup{*

     7 open_file_with_prelude 

     8   "FirstSteps_Code.thy"

     9   ["theory FirstSteps", "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} FirstSteps\\

    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} FirstSteps\\

   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} FirstSteps\\

   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_eq [display,gray] "writeln \"any string\"" "\"any string\"" with "(op =)"}

   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_eq [display,gray] "tracing \"foo\"" "\"foo\"" with "(op =)"}

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

   243 ML{*val pretty_term = Syntax.pretty_term*}

   244 ML{*val pwriteln = Pretty.writeln*}

   245 

   246 text {*

   247   They can now be used as follows

   248 

   249   @{ML_response_fake [display,gray]

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

   251   "\"1\""}

   252 

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

   254   function @{ML_ind enum in Pretty} to separate them.

   255 *} 

   256 

   257 ML{*fun string_of_terms ctxt ts =  

   258   commas (map (string_of_term ctxt) ts)*}

   259 ML{*fun pretty_terms ctxt ts =  

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

   261 

   262 text {*

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

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

   265   to @{ML true}.

   266 *}

   267 

   268 ML{*show_types := true*}

   269 

   270 text {*

   271   Now @{ML pretty_term} prints out

   272 

   273   @{ML_response_fake [display, gray]

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

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

   276 

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

   278   Even more type information can be printed by setting 

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

   280   In this case we obtain

   281 *}

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

   283 (*>*)

   284 text {*

   285   @{ML_response_fake [display, gray]

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

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

   288 

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

   290   Other references that influence printing of terms are 

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

   292 *}

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

   294 (*>*)

   295 text {*

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

   297 *}

   298 

   299 ML{*fun string_of_cterm ctxt ct =  

   300   string_of_term ctxt (term_of ct)*}

   301 ML{*fun pretty_cterm ctxt ct =  

   302   pretty_term ctxt (term_of ct)*}

   303 

   304 text {*

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

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

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

   308 *} 

   309 

   310 ML{*fun string_of_cterms ctxt cts =  

   311   commas (map (string_of_cterm ctxt) cts)*}

   312 ML{*fun pretty_cterms ctxt cts =  

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

   314 

   315 text {*

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

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

   318 *}

   319 

   320 ML{*fun pretty_thm ctxt thm =

   321   pretty_term ctxt (prop_of thm)*}

   322 

   323 text {*

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

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

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

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

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

   329 

   330   @{ML_response_fake [display, gray]

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

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

   333 

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

   335   convert these schematic variables into free variables using the function

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

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

   338 *}

   339 

   340 ML{*fun no_vars ctxt thm =

   341 let 

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

   343 in

   344   thm'

   345 end

   346 

   347 fun pretty_thm_no_vars ctxt thm =

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

   349 

   350 

   351 text {* 

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

   353 

   354   @{ML_response_fake [display, gray]

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

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

   357   

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

   359 *}

   360 

   361 ML{*fun pretty_thms ctxt thms =  

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

   363 

   364 fun pretty_thms_no_vars ctxt thms =  

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

   366 

   367 text {*

   368   The printing functions for types are

   369 *}

   370 

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

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

   373 

   374 text {*

   375   respectively ctypes

   376 *}

   377 

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

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

   380 

   381 text {*

   382   \begin{readmore}

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

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

   385   The references that change the printing information are declared in 

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

   387   \end{readmore}

   388 

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

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

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

   392   \emph{not} print out information as

   393 

   394 @{ML_response_fake [display,gray]

   395 "writeln \"First half,\"; 

   396 writeln \"and second half.\""

   397 "First half,

   398 and second half."}

   399 

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

   401 

   402 @{ML_response_fake [display,gray]

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

   404 "First half,

   405 and second half."}

   406   

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

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

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

   410   and inserts newlines in between each element. 

   411 

   412   @{ML_response_fake [display, gray]

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

   414   "foo

   415 bar"}

   416 

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

   418   provides for more elaborate pretty printing. 

   419 

   420   \begin{readmore}

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

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

   423   \end{readmore}

   424 *}

   425 

   426 

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

   428 

   429 text {*

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

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

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

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

   434 

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

   436   identity function defined as

   437 *}

   438 

   439 ML{*fun I x = x*}

   440 

   441 text {* 

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

   443 *}

   444 

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

   446 

   447 text {*

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

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

   450 

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

   452 *}

   453 

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

   455 

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

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

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

   459 

   460 ML %linenosgray{*fun inc_by_five x =

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

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

   463     |> fst

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

   465 

   466 text {*

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

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

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

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

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

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

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

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

   475   the reverse application is much clearer than writing

   476 *}

   477 

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

   479 

   480 text {* or *}

   481 

   482 ML{*fun inc_by_five x = 

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

   484 

   485 text {* and typographically more economical than *}

   486 

   487 ML{*fun inc_by_five x =

   488 let val y1 = x + 1

   489     val y2 = (y1, y1)

   490     val y3 = fst y2

   491     val y4 = y3 + 4

   492 in y4 end*}

   493 

   494 text {* 

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

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

   497   mention the nightmares the maintenance of this code causes!

   498 

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

   500   the waterfall fashion might be the following code:

   501 *}

   502 

   503 ML %linenosgray{*fun apply_fresh_args f ctxt =

   504     f |> fastype_of

   505       |> binder_types 

   506       |> map (pair "z")

   507       |> Variable.variant_frees ctxt [f]

   508       |> map Free  

   509       |> curry list_comb f *}

   510 

   511 text {*

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

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

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

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

   516 

   517   @{ML_response_fake [display,gray]

   518 "let

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

   520   val ctxt = @{context}

   521 in 

   522   apply_fresh_args trm ctxt

   523    |> string_of_term ctxt

   524    |> tracing

   525 end" 

   526   "P z za zb"}

   527 

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

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

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

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

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

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

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

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

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

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

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

   539   

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

   541   terms involving fresh variables. For this the infrastructure helps

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

   543 

   544    @{ML_response_fake [display,gray]

   545 "let

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

   547   val ctxt = @{context}

   548 in

   549   apply_fresh_args trm ctxt 

   550    |> string_of_term ctxt

   551    |> tracing

   552 end"

   553   "za z zb"}

   554   

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

   556 

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

   558   It can be used to define the following function

   559 *}

   560 

   561 ML{*val inc_by_six = 

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

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

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

   565 

   566 text {* 

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

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

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

   570   is often used for setup functions inside the

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

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

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

   574 *}

   575 

   576 setup %gray {* let

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

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

   579 in

   580   setup_ival1 #>

   581   setup_ival2

   582 end *}

   583 

   584 text {*

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

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

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

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

   589   

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

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

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

   593   side-calculations for instance). The function

   594  *}

   595 

   596 ML %linenosgray{*fun inc_by_three x =

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

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

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

   600 

   601 text {* 

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

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

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

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

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

   607 

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

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

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

   611 *}

   612 

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

   614 

   615 text {*

   616   An example for this combinator is the function

   617 *}

   618 

   619 ML{*fun inc_as_pair x =

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

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

   622 

   623 text {*

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

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

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

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

   628 

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

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

   631   the first component of the pair, defined as

   632 *}

   633 

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

   635 

   636 text {*

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

   638 *}

   639 

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

   641 

   642 text {*

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

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

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

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

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

   648   implemented as

   649 *}

   650 

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

   652   | separate i (x::xs) =

   653       let 

   654         val (los, grs) = separate i xs

   655       in

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

   657       end*}

   658 

   659 text {*

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

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

   662   can be implemented more concisely as

   663 *}

   664 

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

   666   | separate i (x::xs) =

   667       if i <= x 

   668       then separate i xs ||> cons x

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

   670 

   671 text {*

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

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

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

   675 

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

   677   elements from a pair. This combinator is defined as

   678 *}

   679 

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

   681 

   682 text {* 

   683   and can be used to write the following roundabout version 

   684   of the @{text double} function: 

   685 *}

   686 

   687 ML{*fun double x =

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

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

   690 

   691 text {* 

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

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

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

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

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

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

   698 *}

   699 

   700 ML %linenosgray{*fun acc_incs x =

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

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

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

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

   705 

   706 text {*

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

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

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

   710 

   711   @{ML_response [display,gray]

   712   "acc_incs 1"

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

   714 

   715   You can continue this chain with:

   716   

   717   @{ML_response [display,gray]

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

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

   720 

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

   722 *}

   723 

   724 text {*

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

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

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

   728   described above have related combinators for function composition, namely

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

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

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

   732 *}

   733 

   734 ML{*val double =

   735             (fn x => (x, x))

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

   737 

   738 

   739 text {* 

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

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

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

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

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

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

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

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

   748   a list of terms. Consider the code:

   749 

   750   @{ML_response_fake [display, gray]

   751   "let

   752   val ctxt = @{context}

   753 in

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

   755   |> Syntax.check_terms ctxt

   756   |> string_of_terms ctxt

   757   |> tracing

   758 end"

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

   760 *}

   761 

   762 text {*

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

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

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

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

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

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

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

   770 

   771   @{ML_response_fake [display, gray, linenos]

   772   "let 

   773   val ctxt = @{context}

   774 in

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

   776   |> singleton (Syntax.check_terms ctxt)

   777   |> string_of_term ctxt

   778   |> tracing

   779 end"

   780   "m - n"}

   781    

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

   783   single term generated in Line 4.

   784 

   785   \begin{readmore}

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

   787   "Pure/library.ML"}

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

   789   contains further information about combinators.

   790   \end{readmore}

   791 

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

   793   \begin{exercise}

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

   795   \end{exercise}

   796 

   797 

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

   799 *}

   800 

   801 

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

   803 

   804 text {*

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   820   implement your own document antiquotations.}  Syntactically antiquotations

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

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

   823   the code

   824   

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

   826  

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

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

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

   830   the function @{ML_ind theory_name in Context}. 

   831 

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

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

   834 *}

   835 

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

   837 

   838 text {*

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

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

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

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

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

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

   845   replaced with the value representing the theory.

   846 

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

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

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

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

   851   defined abbreviations.

   852 

   853   @{ML_response_fake [display, gray]

   854   "ProofContext.print_abbrevs @{context}"

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

   856 INTER \<equiv> INFI

   857 Inter \<equiv> Inf

   858 \<dots>"}

   859 

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

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

   862 

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

   864 

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

   866 

   867 @{ML_response_fake [display,gray] 

   868   "@{thms conj_ac}" 

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

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

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

   872 

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

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

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

   876 

   877 @{ML_response_fake [display,gray] 

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

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

   880 

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

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

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

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

   885 

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

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

   888   and the second is a proof. For example

   889 *}

   890 

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

   892 

   893 ML {* 

   894 pretty_thms_no_vars

   895 *}

   896 

   897 text {*

   898   The result can be printed out as follows.

   899 

   900   @{ML_response_fake [gray,display]

   901 "foo_thm |> pretty_thms_no_vars @{context}

   902         |> pwriteln"

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

   904 

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

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

   907   simpset.

   908 *}

   909 

   910 ML{*fun get_thm_names_from_ss simpset =

   911 let

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

   913 in

   914   map #1 simps

   915 end*}

   916 

   917 text {*

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

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

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

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

   922 

   923   @{ML_response_fake [display,gray] 

   924   "get_thm_names_from_ss @{simpset}" 

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

   926 

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

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

   929   code.

   930 

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

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

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

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

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

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

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

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

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

   940 *}

   941 

   942 ML %linenosgray{*let

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

   944 

   945   fun term_pat (ctxt, str) =

   946      str |> ProofContext.read_term_pattern ctxt

   947          |> ML_Syntax.print_term

   948          |> ML_Syntax.atomic

   949 in

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

   951 end*}

   952 

   953 text {*

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

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

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

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

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

   959 

   960   @{ML_response_fake [display,gray]

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

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

   963 

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

   965   we can write an antiquotation for type patterns.

   966 *}

   967 

   968 ML{*let

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

   970 

   971   fun typ_pat (ctxt, str) =

   972      str |> Syntax.parse_typ ctxt

   973          |> ML_Syntax.print_typ

   974          |> ML_Syntax.atomic

   975 in

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

   977 end*}

   978 

   979 text {*

   980   \begin{readmore}

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

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

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

   984   \end{readmore}

   985 *}

   986 

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

   988 

   989 text {*

   990   Isabelle provides mechanisms for storing (and retrieving) arbitrary

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

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

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

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

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

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

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

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

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

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

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

  1002   in a type-safe manner.

  1003 

  1004   \begin{readmore}

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

  1006   Universal.universal} in the file

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

  1008   \end{readmore}

  1009 

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

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

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

  1013 *}

  1014 

  1015 ML{*local

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

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

  1018 in

  1019   val inject_int   = Universal.tagInject fn_int;

  1020   val inject_bool  = Universal.tagInject fn_bool;

  1021   val project_int  = Universal.tagProject fn_int;

  1022   val project_bool = Universal.tagProject fn_bool

  1023 end*}

  1024 

  1025 text {*

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

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

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

  1029 *}

  1030 

  1031 ML{*val foo_list = 

  1032 let

  1033   val thirteen  = inject_int 13

  1034   val truth_val = inject_bool true

  1035 in

  1036   [thirteen, truth_val]

  1037 end*}

  1038 

  1039 text {*

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

  1041   

  1042   @{ML_response_fake [display, gray]

  1043 "project_int (nth foo_list 0); 

  1044 project_bool (nth foo_list 1)" 

  1045 "13

  1046 true"}

  1047 

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

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

  1050   a runtime error. 

  1051   

  1052   @{ML_response_fake [display, gray]

  1053 "project_bool (nth foo_list 0)"  

  1054 "*** Exception- Match raised"}

  1055 

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

  1057   containing a universal type.

  1058 

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

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

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

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

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

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

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

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

  1067 

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

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

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

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

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

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

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

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

  1076   The code for the table is:

  1077 *}

  1078 

  1079 ML %linenosgray{*structure Data = Theory_Data

  1080   (type T = thm Symtab.table

  1081    val empty = Symtab.empty

  1082    val extend = I

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

  1084 

  1085 text {*

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

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

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

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

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

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

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

  1093   operations performed on theories and we just give some sensible 

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

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

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

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

  1098   not relevant here. Below we define two

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

  1100 *}

  1101 

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

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

  1104 

  1105 text {*

  1106   Since we want to store introduction rules associated with their 

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

  1108 *}

  1109 

  1110 setup %gray {*

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

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

  1113   update "All"    @{thm allI}

  1114 *}

  1115 

  1116 text {*

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

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

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

  1120 

  1121   @{ML_response_fake [display, gray]

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

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

  1124 

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

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

  1127   we can update the table as follows

  1128 *}

  1129 

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

  1131 

  1132 text {*

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

  1134   

  1135 @{ML_response_fake [display, gray]