theory FirstSteps
imports Base
uses "FirstSteps.ML"
begin

chapter {* First Steps *}

text {*
  Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
  Isabelle must be part of a theory. If you want to follow the code given in
  this chapter, we assume you are working inside the theory starting with

  \begin{quote}
  \begin{tabular}{@ {}l}
  \isacommand{theory} FirstSteps\\
  \isacommand{imports} Main\\
  \isacommand{begin}\\
  \ldots
  \end{tabular}
  \end{quote}

  We also generally assume you are working with HOL. The given examples might
  need to be adapted if you work in a different logic.
*}

section {* Including ML-Code *}

text {*
  The easiest and quickest way to include code in a theory is by using the
  \isacommand{ML}-command. For example:

  \begin{isabelle}
  \begin{graybox}
  \isacommand{ML}~@{text "\<verbopen>"}\isanewline
  \hspace{5mm}@{ML "3 + 4"}\isanewline
  @{text "\<verbclose>"}\isanewline
  @{text "> 7"}\smallskip
  \end{graybox}
  \end{isabelle}

  Like normal Isabelle scripts, \isacommand{ML}-commands can be evaluated by
  using the advance and undo buttons of your Isabelle environment. The code
  inside the \isacommand{ML}-command can also contain value and function
  bindings, for example
*}

ML %gray {* 
  val r = ref 0
  fun f n = n + 1 
*}

text {*
  and even those can be undone when the proof script is retracted.  As
  mentioned in the Introduction, we will drop the \isacommand{ML}~@{text
  "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we show code. The lines
  prefixed with @{text [quotes] ">"} are not part of the code, rather they
  indicate what the response is when the code is evaluated.  There are also
  the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for including
  ML-code. The first evaluates the given code, but any effect on the theory,
  in which the code is embedded, is suppressed. The second needs to be used if
  ML-code is defined inside a proof. For example

  \begin{quote}
  \begin{isabelle}
  \isacommand{lemma}~@{text "test:"}\isanewline
  \isacommand{shows}~@{text [quotes] "True"}\isanewline
  \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline
  \isacommand{oops}
  \end{isabelle}
  \end{quote}

  However, both commands will only play minor roles in this tutorial (we will
  always arrange that the ML-code is defined outside of proofs, for example).

  Once a portion of code is relatively stable, you usually want to export it
  to a separate ML-file. Such files can then be included somewhere inside a 
  theory by using the command \isacommand{use}. For example

  \begin{quote}
  \begin{tabular}{@ {}l}
  \isacommand{theory} FirstSteps\\
  \isacommand{imports} Main\\
  \isacommand{uses}~@{text "(\"file_to_be_included.ML\")"} @{text "\<dots>"}\\
  \isacommand{begin}\\
  \ldots\\
  \isacommand{use}~@{text "\"file_to_be_included.ML\""}\\
  \ldots
  \end{tabular}
  \end{quote}

  The \isacommand{uses}-command in the header of the theory is needed in order 
  to indicate the dependency of the theory on the ML-file. Alternatively, the 
  file can be included by just writing in the header

  \begin{quote}
  \begin{tabular}{@ {}l}
  \isacommand{theory} FirstSteps\\
  \isacommand{imports} Main\\
  \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
  \isacommand{begin}\\
  \ldots
  \end{tabular}
  \end{quote}

  Note that no parentheses are given this time. Note also that the included
  ML-file should not contain any \isacommand{use} itself. Otherwise Isabelle
  is unable to record all file dependencies, which is a nuisance if you have
  to track down errors.
*}

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

text {*
  During development you might find it necessary to inspect some data in your
  code. This can be done in a ``quick-and-dirty'' fashion using the function
  @{ML_ind  "writeln"}. For example

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

  will print out @{text [quotes] "any string"} inside the response buffer of
  Isabelle.  This function expects a string as argument. If you develop under
  PolyML, then there is a convenient, though again ``quick-and-dirty'', method
  for converting values into strings, namely the function 
  @{ML_ind  makestring in PolyML}:

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

  However, @{ML makestring in PolyML} only works if the type of what
  is converted is monomorphic and not a function.

  The function @{ML "writeln"} should only be used for testing purposes,
  because any output this function generates will be overwritten as soon as an
  error is raised. For printing anything more serious and elaborate, the
  function @{ML_ind  tracing} is more appropriate. This function writes all
  output into a separate tracing buffer. For example:

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

  It is also possible to redirect the ``channel'' where the string @{text
  "foo"} is printed to a separate file, e.g., to prevent ProofGeneral from
  choking on massive amounts of trace output. This redirection can be achieved
  with the code:
*}

ML{*val strip_specials =
let
  fun strip ("\^A" :: _ :: cs) = strip cs
    | strip (c :: cs) = c :: strip cs
    | strip [] = [];
in 
  implode o strip o explode 
end

fun redirect_tracing stream =
 Output.tracing_fn := (fn s =>
    (TextIO.output (stream, (strip_specials s));
     TextIO.output (stream, "\n");
     TextIO.flushOut stream)) *}

text {*
  Calling now

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

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

  You can print out error messages with the function @{ML_ind  error}; for 
  example:

@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" 
"Exception- ERROR \"foo\" raised
At command \"ML\"."}

  This function raises the exception @{text ERROR}, which will then 
  be displayed by the infrastructure.


  (FIXME Mention how to work with @{ML_ind  debug in Toplevel} and 
  @{ML_ind  profiling in Toplevel}.)
*}

(* FIXME
ML {* reset Toplevel.debug *}

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

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

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

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

text {*
  Most often you want to inspect data of Isabelle's most basic data
  structures, namely @{ML_type term}, @{ML_type cterm} and @{ML_type
  thm}. Isabelle contains elaborate pretty-printing functions for printing
  them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
  are a bit unwieldy. One way to transform a term into a string is to use the
  function @{ML_ind  string_of_term in Syntax} in structure @{ML_struct
  Syntax}, which we bind for more convenience to the toplevel.
*}

ML{*val string_of_term = Syntax.string_of_term*}

text {*
  It can now be used as follows

  @{ML_response_fake [display,gray]
  "string_of_term @{context} @{term \"1::nat\"}"
  "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} 

  This produces a string corrsponding to the term @{term [show_types] "1::nat"} with some
  additional information encoded in it. The string can be properly printed by
  using either the function @{ML_ind  writeln} or @{ML_ind  tracing}:

  @{ML_response_fake [display,gray]
  "writeln (string_of_term @{context} @{term \"1::nat\"})"
  "\"1\""}

  or

  @{ML_response_fake [display,gray]
  "tracing (string_of_term @{context} @{term \"1::nat\"})"
  "\"1\""}

  If there are more than one @{ML_type term}s to be printed, you can use the 
  function @{ML_ind  commas} to separate them.
*} 

ML{*fun string_of_terms ctxt ts =  
  commas (map (string_of_term ctxt) ts)*}

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

ML{*fun string_of_cterm ctxt ct =  
  string_of_term ctxt (term_of ct)*}

text {*
  In this example the function @{ML_ind  term_of} extracts the @{ML_type
  term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can again be
  printed with @{ML_ind  commas}.
*} 

ML{*fun string_of_cterms ctxt cts =  
  commas (map (string_of_cterm ctxt) cts)*}

text {*
  The easiest way to get the string of a theorem is to transform it
  into a @{ML_type cterm} using the function @{ML_ind  crep_thm}. 
*}

ML{*fun string_of_thm ctxt thm =
  string_of_cterm ctxt (#prop (crep_thm thm))*}

text {*
  Theorems also include schematic variables, such as @{text "?P"}, 
  @{text "?Q"} and so on. They are needed in order to able to
  instantiate theorems when they are applied. For example the theorem 
  @{thm [source] conjI} shown below can be used for any (typable) 
  instantiation of @{text "?P"} and @{text "?Q"} 

  @{ML_response_fake [display, gray]
  "tracing (string_of_thm @{context} @{thm conjI})"
  "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}

  However, in order to improve the readability when printing theorems, we
  convert these schematic variables into free variables using the function
  @{ML_ind  import in Variable}. This is similar to statements like @{text
  "conjI[no_vars]"} from Isabelle's user-level.
*}

ML{*fun no_vars ctxt thm =
let 
  val ((_, [thm']), _) = Variable.import true [thm] ctxt
in
  thm'
end

fun string_of_thm_no_vars ctxt thm =
  string_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}

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

  @{ML_response_fake [display, gray]
  "tracing (string_of_thm_no_vars @{context} @{thm conjI})"
  "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
  
  Again the function @{ML commas} helps with printing more than one theorem. 
*}

ML{*fun string_of_thms ctxt thms =  
  commas (map (string_of_thm ctxt) thms)

fun string_of_thms_no_vars ctxt thms =  
  commas (map (string_of_thm_no_vars ctxt) thms) *}

text {*
  Note, that when printing out several parcels of information that
  semantically belong together, like a warning message consisting for example
  of a term and a type, you should try to keep this information together in a
  single string. So do not print out information as

@{ML_response_fake [display,gray]
"tracing \"First half,\"; 
tracing \"and second half.\""
"First half,
and second half."}

  but as a single string with appropriate formatting. For example

@{ML_response_fake [display,gray]
"tracing (\"First half,\" ^ \"\\n\" ^ \"and second half.\")"
"First half,
and second half."}
  
  To ease this kind of string manipulations, there are a number
  of library functions. For example,  the function @{ML_ind  cat_lines}
  concatenates a list of strings and inserts newlines. 

  @{ML_response [display, gray]
  "cat_lines [\"foo\", \"bar\"]"
  "\"foo\\nbar\""}

  Section \ref{sec:pretty} will also explain infrastructure that helps 
  with more elaborate pretty printing. 
*}


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

text {*
  For beginners perhaps the most puzzling parts in the existing code of Isabelle are
  the combinators. At first they seem to greatly obstruct the
  comprehension of the code, but after getting familiar with them, they
  actually ease the understanding and also the programming.

  The simplest combinator is @{ML_ind  I}, which is just the identity function defined as
*}

ML{*fun I x = x*}

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

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

text {*
  @{ML_ind  K} ``wraps'' a function around the argument @{text "x"}. However, this 
  function ignores its argument. As a result, @{ML K} defines a constant function 
  always returning @{text x}.

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

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

text {* While just syntactic sugar for the usual function application,
  the purpose of this combinator is to implement functions in a  
  ``waterfall fashion''. Consider for example the function *}

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

text {*
  which increments its argument @{text x} by 5. It proceeds by first incrementing 
  the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking 
  the first component of the pair (Line 4) and finally incrementing the first 
  component by 4 (Line 5). This kind of cascading manipulations of values is quite
  common when dealing with theories (for example by adding a definition, followed by
  lemmas and so on). The reverse application allows you to read what happens in 
  a top-down manner. This kind of coding should also be familiar, 
  if you have been exposed to Haskell's {\it do}-notation. Writing the function 
  @{ML inc_by_five} using the reverse application is much clearer than writing
*}

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

text {* or *}

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

text {* and typographically more economical than *}

ML{*fun inc_by_five x =
let val y1 = x + 1
    val y2 = (y1, y1)
    val y3 = fst y2
    val y4 = y3 + 4
in y4 end*}

text {* 
  Another reason why the let-bindings in the code above are better to be
  avoided: it is more than easy to get the intermediate values wrong, not to 
  mention the nightmares the maintenance of this code causes!

  In Isabelle, a ``real world'' example for a function written in 
  the waterfall fashion might be the following code:
*}

ML %linenosgray{*fun apply_fresh_args f ctxt =
    f |> fastype_of
      |> binder_types 
      |> map (pair "z")
      |> Variable.variant_frees ctxt [f]
      |> map Free  
      |> curry list_comb f *}

text {*
  This function takes a term and a context as argument. If the term is of function
  type, then @{ML "apply_fresh_args"} returns the term with distinct variables 
  applied to it. For example below variables are applied to the term 
  @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:

  @{ML_response_fake [display,gray]
"let
  val t = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
  val ctxt = @{context}
in 
  apply_fresh_args t ctxt
   |> string_of_term ctxt
   |> tracing
end" 
  "P z za zb"}

  You can read off this behaviour from how @{ML apply_fresh_args} is
  coded: in Line 2, the function @{ML_ind  fastype_of} calculates the type of the
  term; @{ML_ind  binder_types} in the next line produces the list of argument
  types (in the case above the list @{text "[nat, int, unit]"}); Line 4 
  pairs up each type with the string  @{text "z"}; the
  function @{ML_ind  variant_frees in Variable} generates for each @{text "z"} a
  unique name avoiding the given @{text f}; the list of name-type pairs is turned
  into a list of variable terms in Line 6, which in the last line is applied
  by the function @{ML_ind  list_comb} to the term. In this last step we have to 
  use the function @{ML_ind  curry}, because @{ML_ind  list_comb} expects the 
  function and the variables list as a pair. This kind of functions is often needed when
  constructing terms with fresh variables. The infrastructure helps tremendously 
  to avoid any name clashes. Consider for example: 

   @{ML_response_fake [display,gray]
"let
  val t = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
  val ctxt = @{context}
in
  apply_fresh_args t ctxt 
   |> string_of_term ctxt
   |> tracing
end"
  "za z zb"}
  
  where the @{text "za"} is correctly avoided.

  The combinator @{ML_ind  "#>"} is the reverse function composition. It can be
  used to define the following function
*}

ML{*val inc_by_six = 
      (fn x => x + 1)
   #> (fn x => x + 2)
   #> (fn x => x + 3)*}

text {* 
  which is the function composed of first the increment-by-one function and then
  increment-by-two, followed by increment-by-three. Again, the reverse function 
  composition allows you to read the code top-down.

  The remaining combinators described in this section add convenience for the
  ``waterfall method'' of writing functions. The combinator @{ML_ind  tap} allows
  you to get hold of an intermediate result (to do some side-calculations for
  instance). The function

 *}

ML %linenosgray{*fun inc_by_three x =
     x |> (fn x => x + 1)
       |> tap (fn x => tracing (PolyML.makestring x))
       |> (fn x => x + 2)*}

text {* 
  increments the argument first by @{text "1"} and then by @{text "2"}. In the
  middle (Line 3), however, it uses @{ML_ind  tap} for printing the ``plus-one''
  intermediate result inside the tracing buffer. The function @{ML_ind  tap} can
  only be used for side-calculations, because any value that is computed
  cannot be merged back into the ``main waterfall''. To do this, you can use
  the next combinator.

  The combinator @{ML_ind  "`"} (a backtick) is similar to @{ML tap}, but applies a
  function to the value and returns the result together with the value (as a
  pair). For example the function 
*}

ML{*fun inc_as_pair x =
     x |> `(fn x => x + 1)
       |> (fn (x, y) => (x, y + 1))*}

text {*
  takes @{text x} as argument, and then increments @{text x}, but also keeps
  @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
  for x}. After that, the function increments the right-hand component of the
  pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.

  The combinators @{ML_ind  "|>>"} and @{ML_ind  "||>"} are defined for 
  functions manipulating pairs. The first applies the function to
  the first component of the pair, defined as
*}

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

text {*
  and the second combinator to the second component, defined as
*}

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

text {*
  These two functions can, for example, be used to avoid explicit @{text "lets"} for
  intermediate values in functions that return pairs. As an example, suppose you
  want to separate a list of integers into two lists according to a
  treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}
  should be separated to @{ML "([1,2,3,4], [6,5])"}.  This function can be
  implemented as
*}

ML{*fun separate i [] = ([], [])
  | separate i (x::xs) =
      let 
        val (los, grs) = separate i xs
      in
        if i <= x then (los, x::grs) else (x::los, grs)
      end*}

text {*
  where however the return value of the recursive call is bound explicitly to
  the pair @{ML "(los, grs)" for los grs}. You can implement this function
  more concisely as
*}

ML{*fun separate i [] = ([], [])
  | separate i (x::xs) =
      if i <= x 
      then separate i xs ||> cons x
      else separate i xs |>> cons x*}

text {*
  avoiding the explicit @{text "let"}. While in this example the gain in
  conciseness is only small, in more complicated situations the benefit of
  avoiding @{text "lets"} can be substantial.

  With the combinator @{ML_ind  "|->"} you can re-combine the elements from a pair.
  This combinator is defined as
*}

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

text {* 
  and can be used to write the following roundabout version 
  of the @{text double} function: 
*}

ML{*fun double x =
      x |>  (fn x => (x, x))
        |-> (fn x => fn y => x + y)*}

text {* 
  The combinator @{ML_ind  ||>>} plays a central rôle whenever your task is to update a 
  theory and the update also produces a side-result (for example a theorem). Functions 
  for such tasks return a pair whose second component is the theory and the fist 
  component is the side-result. Using @{ML_ind  ||>>}, you can do conveniently the update 
  and also accumulate the side-results. Consider the following simple function. 
*}

ML %linenosgray{*fun acc_incs x =
    x |> (fn x => ("", x)) 
      ||>> (fn x => (x, x + 1))
      ||>> (fn x => (x, x + 1))
      ||>> (fn x => (x, x + 1))*}

text {*
  The purpose of Line 2 is to just pair up the argument with a dummy value (since
  @{ML_ind  "||>>"} operates on pairs). Each of the next three lines just increment 
  the value by one, but also nest the intermediate results to the left. For example 

  @{ML_response [display,gray]
  "acc_incs 1"
  "((((\"\", 1), 2), 3), 4)"}

  You can continue this chain with:
  
  @{ML_response [display,gray]
  "acc_incs 1 ||>> (fn x => (x, x + 2))"
  "(((((\"\", 1), 2), 3), 4), 6)"}

  (FIXME: maybe give a ``real world'' example for this combinator)
*}

text {*
  Recall that @{ML_ind  "|>"} is the reverse function application. Recall also that
  the related 
  reverse function composition is @{ML_ind  "#>"}. In fact all the combinators 
  @{ML_ind  "|->"}, @{ML_ind  "|>>"} , @{ML_ind  "||>"} and @{ML_ind  
  "||>>"} described above have related combinators for 
  function composition, namely @{ML_ind  "#->"}, @{ML_ind  "#>>"}, 
  @{ML_ind  "##>"} and @{ML_ind  "##>>"}. 
  Using @{ML_ind  "#->"}, for example, the function @{text double} can also be written as:
*}

ML{*val double =
            (fn x => (x, x))
        #-> (fn x => fn y => x + y)*}


text {* 
  When using combinators for writing functions in waterfall fashion, it is
  sometimes necessary to do some ``plumbing'' in order to fit functions
  together. We have already seen such plumbing in the function @{ML
  apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
  list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such 
  plumbing is also needed in situations where a functions operate over lists, 
  but one calculates only with a single entity. An example is the function 
  @{ML_ind  check_terms in Syntax}, whose purpose is to type-check a list 
  of terms.

  @{ML_response_fake [display, gray]
  "let
  val ctxt = @{context}
in
  map (Syntax.parse_term ctxt) [\"m + n\", \"m - (n::nat)\"] 
  |> Syntax.check_terms ctxt
  |> string_of_terms ctxt
  |> tracing
end"
  "m + n, m - n"}
*}

text {*
  In this example we obtain two terms with appropriate typing. However, if you
  have only a single term, then @{ML check_terms in Syntax} needs to be
  adapted. This can be done with the ``plumbing'' function @{ML
  singleton}.\footnote{There is already a function @{ML check_term in Syntax}
  in the Isabelle sources that is defined in terms of @{ML singleton} and @{ML
  check_terms in Syntax}.} For example

  @{ML_response_fake [display, gray]
  "let 
  val ctxt = @{context}
in
  Syntax.parse_term ctxt \"m - (n::nat)\" 
  |> singleton (Syntax.check_terms ctxt)
  |> string_of_term ctxt
  |> tracing
end"
  "m - n"}
   
  \begin{readmore}
  The most frequently used combinators are defined in the files @{ML_file
  "Pure/library.ML"}
  and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
  contains further information about combinators.
  \end{readmore}

  (FIXME: find a good exercise for combinators)

  (FIXME: say something about calling conventions) 
*}


section {* Antiquotations *}

text {*
  The main advantage of embedding all code in a theory is that the code can
  contain references to entities defined on the logical level of Isabelle. By
  this we mean definitions, theorems, terms and so on. This kind of reference is
  realised with antiquotations, sometimes also referred to as ML-antiquotations.  
  For example, one can print out the name of the current
  theory by typing

  
  @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
 
  where @{text "@{theory}"} is an antiquotation that is substituted with the
  current theory (remember that we assumed we are inside the theory 
  @{text FirstSteps}). The name of this theory can be extracted using
  the function @{ML_ind  theory_name in Context}. 

  Note, however, that antiquotations are statically linked, that is their value is
  determined at ``compile-time'', not ``run-time''. For example the function
*}

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

text {*

  does \emph{not} return the name of the current theory, if it is run in a 
  different theory. Instead, the code above defines the constant function 
  that always returns the string @{text [quotes] "FirstSteps"}, no matter where the
  function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is 
  \emph{not} replaced with code that will look up the current theory in 
  some data structure and return it. Instead, it is literally
  replaced with the value representing the theory name.

  In a similar way you can use antiquotations to refer to proved theorems: 
  @{text "@{thm \<dots>}"} for a single theorem

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

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

@{ML_response_fake [display,gray] "@{thms conj_ac}" 
"(?P \<and> ?Q) = (?Q \<and> ?P)
(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  

  The point of these antiquotations is that referring to theorems in this way
  makes your code independent from what theorems the user might have stored
  under this name (this becomes especially important when you deal with
  theorem lists; see Section \ref{sec:attributes}).

  You can also refer to the current simpset via an antiquotation. To illustrate 
  this we implement the function that extracts the theorem names stored in a 
  simpset.
*}

ML{*fun get_thm_names_from_ss simpset =
let
  val {simps,...} = MetaSimplifier.dest_ss simpset
in
  map #1 simps
end*}

text {*
  The function @{ML_ind  dest_ss in MetaSimplifier} returns a record containing all
  information stored in the simpset, but we are only interested in the names of the
  simp-rules. Now you can feed in the current simpset into this function. 
  The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.

  @{ML_response_fake [display,gray] 
  "get_thm_names_from_ss @{simpset}" 
  "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}

  Again, this way of referencing simpsets makes you independent from additions
  of lemmas to the simpset by the user that can potentially cause loops in your
  code.

  On the ML-level of Isabelle, you often have to work with qualified names.
  These are strings with some additional information, such as positional
  information and qualifiers. Such qualified names can be generated with the
  antiquotation @{text "@{binding \<dots>}"}. For example

  @{ML_response [display,gray]
  "@{binding \"name\"}"
  "name"}

  An example where a qualified name is needed is the function 
  @{ML_ind  define in LocalTheory}.  This function is used below to define 
  the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
*}
  
local_setup %gray {* 
  snd o LocalTheory.define Thm.internalK 
    ((@{binding "TrueConj"}, NoSyn), 
     (Attrib.empty_binding, @{term "True \<and> True"})) *}

text {* 
  Now querying the definition you obtain:

  \begin{isabelle}
  \isacommand{thm}~@{text "TrueConj_def"}\\
  @{text "> "}~@{thm TrueConj_def}
  \end{isabelle}

  (FIXME give a better example why bindings are important; maybe
  give a pointer to \isacommand{local\_setup}; if not, then explain
  why @{ML snd} is needed)

  It is also possible to define your own antiquotations. But you should
  exercise care when introducing new ones, as they can also make your code
  also difficult to read. In the next section we will see how the (build in)
  antiquotation @{text "@{term \<dots>}"} can be used to construct terms.  A
  restriction of this antiquotation is that it does not allow you to use
  schematic variables. If you want to have an antiquotation that does not have
  this restriction, you can implement your own using the function @{ML_ind 
  ML_Antiquote.inline}. The code is as follows.
*}

ML %linenosgray{*ML_Antiquote.inline "term_pat"
  (Args.context -- Scan.lift Args.name_source >>
     (fn (ctxt, s) =>
       s |> ProofContext.read_term_pattern ctxt
         |> ML_Syntax.print_term
         |> ML_Syntax.atomic))*}

text {*
  The parser in Line 2 provides us with a context and a string; this string is
  transformed into a term using the function @{ML_ind  read_term_pattern in
  ProofContext} (Line 4); the next two lines print the term so that the
  ML-system can understand them. An example of this antiquotation is as
  follows.

  @{ML_response_fake [display,gray]
  "@{term_pat \"Suc (?x::nat)\"}"
  "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}

  which is the internal representation of the term @{text "Suc ?x"}.

  \begin{readmore}
  The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
  for most antiquotations. 
  \end{readmore}

  Note one source of possible confusion about antiquotations. There are two kinds 
  of them in Isabelle, which have very different purpose and infrastructures. The 
  first kind, described in this section, are \emph{ML-antiquotations}. They are 
  used to refer to entities (like terms, types etc) from Isabelle's logic layer 
  inside ML-code. They are ``linked'' statically at compile-time, which  limits 
  sometimes their usefulness in  cases where, for example, terms needs to be 
  built up dynamically.  

  The other kind of antiquotations are \emph{document} antiquotations. 
  They are used only in the text parts of Isabelle and their purpose is to print 
  logical entities inside \LaTeX-documents. They are part of the user level and
  therefore we are not interested in them in this Tutorial, except in 
  Appendix \ref{rec:docantiquotations} where we show how to implement your 
  own document antiquotations. 
*}

(*
section {* Do Not Try This At Home! *}

ML {* val my_thms = ref ([]: thm list) *}

attribute_setup my_thm_bad =
  {* Scan.succeed (Thm.declaration_attribute (fn th => fn ctxt =>
      (my_thms := th :: ! my_thms; ctxt))) *} "bad attribute"

declare sym [my_thm_bad]
declare refl [my_thm_bad]

ML "!my_thms"
*)
end