theory FirstSteps

imports Base

begin

chapter {* First Steps *}

text {*

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

  in Isabelle is part of a theory. If you want to follow the code given in

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

  \begin{center}

  \begin{tabular}{@ {}l}

  \isacommand{theory} FirstSteps\\

  \isacommand{imports} Main\\

  \isacommand{begin}\\

  \ldots

  \end{tabular}

  \end{center}

*}

section {* Including ML-Code *}

text {*

  The easiest and quickest way to include code in a theory is

  by using the \isacommand{ML}-command. For example:

\begin{isabelle}

\begin{graybox}

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

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

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

@{text "> 7"}\smallskip

\end{graybox}

\end{isabelle}

  Like normal Isabelle proof scripts, \isacommand{ML}-commands can be

  evaluated by using the advance and undo buttons of your Isabelle

  environment. The code inside the \isacommand{ML}-command can also contain

  value and function bindings, and even those can be undone when the proof

  script is retracted. As mentioned earlier, we will drop the

  \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we

  show code. The lines prefixed with @{text [quotes] ">"} are not part of the

  code, rather they indicate what the response is when the code is evaluated.

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

  to a separate ML-file. Such files can then be included in a theory by using

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

  \begin{center}

  \begin{tabular}{@ {}l}

  \isacommand{theory} FirstSteps\\

  \isacommand{imports} Main\\

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

  \isacommand{begin}\\

  \ldots

  \end{tabular}

  \end{center}

*}

section {* Debugging and Printing *}

text {*

  During development you might find it necessary to inspect some data

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

  the function @{ML "warning"}. For example 

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

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

  of Isabelle.  This function expects a string as argument. If you develop under PolyML,

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

  converting values into strings, namely the function @{ML makestring}:

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

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

  and not a function.

  The function @{ML "warning"} should only be used for testing purposes, because any

  output this function generates will be overwritten as soon as an error is

  raised. For printing anything more serious and elaborate, the

  function @{ML tracing} is more appropriate. This function writes all output into

  a separate tracing buffer. For example:

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

  It is also possible to redirect the ``channel'' where the string @{text "foo"} is 

  printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive 

  amounts of trace output. This redirection can be achieved with the code:

*}

ML{*val strip_specials =

let

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

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

    | strip [] = [];

in implode o strip o explode end;

fun redirect_tracing stream =

 Output.tracing_fn := (fn s =>

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

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

     TextIO.flushOut stream)) *}

text {*

  Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 

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

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

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

"Exception- ERROR \"foo\" raised

At command \"ML\"."}

  Section~\ref{sec:printing} will give more information about printing 

  the main data structures of Isabelle, namely @{ML_type term}, @{ML_type cterm} 

  and @{ML_type thm}.

*}

section {* Antiquotations *}

text {*

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

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

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

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

  theory by typing

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

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

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

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

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

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

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

*}

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

text {*

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

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

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

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

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

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

  replaced with the value representing the theory name.

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

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

  and current simpsets:

  @{ML_response_fake [display,gray] 

"let

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

in

  map #name (Net.entries rules)

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

  The code about simpsets extracts the theorem names stored in the

  simpset.  You can get hold of the current simpset with the antiquotation 

  @{text "@{simpset}"}.  The function @{ML rep_ss in MetaSimplifier} returns a record

  containing all information about the simpset. The rules of a simpset are

  stored in a \emph{discrimination net} (a data structure for fast

  indexing). From this net you can extract the entries using the function @{ML

  Net.entries}.

  \begin{readmore}

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

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

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

  \end{readmore}

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

  to avoid explicit bindings for theorems such as:

*}

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

text {*

  These bindings are difficult to maintain and also can be accidentally

  overwritten by the user. This often breakes Isabelle

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

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

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

  course of this introduction, you will learn more about these antiquotations:

  they can simplify Isabelle programming since one can directly access all

  kinds of logical elements from th ML-level.

*}

section {* Terms and Types *}

text {*

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

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

  @{ML_response [display,gray] 

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

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

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

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

  representation of this term. This internal representation corresponds to the 

  datatype @{ML_type "term"}.

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

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

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

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

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

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

  \begin{readmore}

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

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

  \end{readmore}

  Sometimes the internal representation of terms can be surprisingly different

  from what you see at the user level, because the layers of

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

  \begin{exercise}

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

  find out why they are represented like this:

  \begin{itemize}

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

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

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

  \end{itemize}

  Hint: The third term is already quite big, and the pretty printer

  may omit parts of it by default. If you want to see all of it, you

  can use the following ML-function to set the printing depth to a higher 

  value:

  @{ML [display,gray] "print_depth 50"}

  \end{exercise}

  The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 

  inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 

  Consider for example the pairs

  @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),

 Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}

  where a coercion is inserted in the second component and 

  @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 

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

  where it is not (since it is already constructed by a meta-implication). 

  Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example:

  @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}

  \begin{readmore}

  Types are described in detail in \isccite{sec:types}. Their

  definition and many useful operations are implemented 

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

  \end{readmore}

*}

section {* Constructing Terms and Types Manually *} 

text {*

  While antiquotations are very convenient for constructing terms, they can

  only construct fixed terms (remember they are ``linked'' at compile-time).

  However, you often need to construct terms dynamically. For example, a

  function that returns the implication @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking

  @{term P}, @{term Q} and the type @{term "\<tau>"} as arguments can only be

  written as:

*}

ML{*fun make_imp P Q tau =

  let

    val x = Free ("x",tau)

  in 

    Logic.all x (Logic.mk_implies (P $ x, Q $ x))

  end *}

text {*

  The reason is that you cannot pass the arguments @{term P}, @{term Q} and 

  @{term "tau"} into an antiquotation. For example the following does \emph{not} work.

*}

ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}

text {*

  To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 

  to both functions. With @{ML make_imp} we obtain the intended term involving 

  the given arguments

  @{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}" 

    "Const \<dots> $ 

    Abs (\"x\", Type (\"nat\",[]),

      Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ 

                  (Free (\"T\",\<dots>) $ \<dots>))"}

  whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"} 

  and @{text "Q"} from the antiquotation.

  @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}" 

    "Const \<dots> $ 

    Abs (\"x\", \<dots>,

      Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 

                  (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}

  Although types of terms can often be inferred, there are many

  situations where you need to construct types manually, especially  

  when defining constants. For example the function returning a function 

  type is as follows:

*} 

ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}

text {* This can be equally written as: *}

ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}

text {*

  \begin{readmore}

  There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and

  @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 

  and types easier.\end{readmore}

  Have a look at these files and try to solve the following two exercises:

*}

text {*

  \begin{exercise}\label{fun:revsum}

  Write a function @{text "rev_sum : term -> term"} that takes a

  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero)

  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume

  the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 

  associates to the left. Try your function on some examples. 

  \end{exercise}

  \begin{exercise}\label{fun:makesum}

  Write a function which takes two terms representing natural numbers

  in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the

  number representing their sum.

  \end{exercise}

  A handy function for manipulating terms is @{ML map_types}: it takes a 

  function and applies it to every type in the term. You can, for example,

  change every @{typ nat} in a term into an @{typ int} using the function:

*}

ML{*fun nat_to_int t =

  (case t of

     @{typ nat} => @{typ int}

   | Type (s, ts) => Type (s, map nat_to_int ts)

   | _ => t)*}

text {*

  An example as follows:

@{ML_response_fake [display,gray] 

"map_types nat_to_int @{term \"a = (1::nat)\"}" 

"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")

           $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}

  There are a few subtle issues with constants. They usually crop up when

  pattern matching terms or constructing terms. While it is perfectly ok

  to write the function @{text is_true} as follows

*}

ML{*fun is_true @{term True} = true

  | is_true _ = false*}

text {*

  this does not work for picking out @{text "\<forall>"}-quantified terms. Because

  the function 

*}

ML{*fun is_all (@{term All} $ _) = true

  | is_all _ = false*}

text {* 

  will not correctly match the formula @{prop "\<forall>x::nat. P x"}: 

  @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}

  The problem is that the @{text "@term"}-antiquotation in the pattern 

  fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for 

  an arbitrary, but fixed type @{typ "'a"}. A properly working alternative 

  for this function is

*}

ML{*fun is_all (Const ("All", _) $ _) = true

  | is_all _ = false*}

text {* 

  because now

@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}

  matches correctly (the wildcard in the pattern matches any type).

  However there is still a problem: consider the similar function that

  attempts to pick out a @{text "Nil"}-term:

*}

ML{*fun is_nil (Const ("Nil", _)) = true

  | is_nil _ = false *}

text {* 

  Unfortunately, also this function does \emph{not} work as expected, since

  @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}

  The problem is that on the ML-level the name of a constant is more

  subtle as you might expect. The function @{ML is_all} worked correctly,

  because @{term "All"} is such a fundamental constant, which can be referenced

  by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at

  @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}

  the name of the constant depends on the theory in which the term constructor

  @{text "Nil"} is defined (@{text "List"}) and also in which datatype 

  (@{text "list"}). Even worse, some constants have a name involving 

  type-classes. Consider for example the constants for @{term "zero"} 

  @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" 

  "(Const (\"HOL.zero_class.zero\", \<dots>), 

 Const (\"HOL.times_class.times\", \<dots>))"}

  While you could use the complete name, for example 

  @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or

  matching against @{text "Nil"}, this would make the code rather brittle. 

  The reason is that the theory and the name of the datatype can easily change. 

  To make the code more robust, it is better to use the antiquotation 

  @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the 

  variable parts of the constant's name. Therefore a functions for 

  matching against constants that have a polymorphic type should 

  be written as follows.

*}

ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true

  | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true

  | is_nil_or_all _ = false *}

text {*

  \begin{readmore}