theory Essential

imports Base First_Steps

begin

chapter \<open>Isabelle Essentials\<close>

text \<open>

   \begin{flushright}

  {\em One man's obfuscation is another man's abstraction.} \\[1ex]

  Frank Ch.~Eigler on the Linux Kernel Mailing List,\\ 

  24~Nov.~2009

  \end{flushright}

  \medskip

  Isabelle is built around a few central ideas. One central idea is the

  LCF-approach to theorem proving \cite{GordonMilnerWadsworth79} where there

  is a small trusted core and everything else is built on top of this trusted

  core. The fundamental data structures involved in this core are certified

  terms and certified types, as well as theorems.

\<close>

section \<open>Terms and Types\<close>

text \<open>

  In Isabelle, there are certified terms and uncertified terms (respectively types). 

  Uncertified terms are often just called terms. One way to construct them is by 

  using the antiquotation \mbox{\<open>@{term \<dots>}\<close>}. For example

  @{ML_matchresult [display,gray] 

  constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using 

  the internal representation corresponding to the datatype @{ML_type_ind "term"}, 

  which is defined as follows: 

\<close>  

ML_val %linenosgray\<open>datatype term =

  Const of string * typ 

| Free of string * typ 

| Var of indexname * typ 

| Bound of int 

| Abs of string * typ * term 

| $ of term * term\<close>

text \<open>

  This datatype implements Church-style lambda-terms, where types are

  explicitly recorded in variables, constants and abstractions.  The

  important point of having terms is that you can pattern-match against them;

  this cannot be done with certified terms. As can be seen in Line 5,

  terms use the usual de Bruijn index mechanism for representing bound

  variables.  For example in

  @{ML_matchresult_fake [display, gray]

  the indices refer to the number of Abstractions (@{ML Abs}) that we need to

  skip until we hit the @{ML Abs} that binds the corresponding

  variable. Constructing a term with dangling de Bruijn indices is possible,

  but will be flagged as ill-formed when you try to typecheck or certify it

  (see Section~\ref{sec:typechecking}). Note that 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 $}.

  Be careful if you pretty-print terms. Consider pretty-printing the abstraction

  term shown above:

  @{ML_matchresult_fake [display, gray]

  |> pretty_term @{context}

  This is one common source for puzzlement in Isabelle, which has 

  tacitly eta-contracted the output. You obtain a similar result 

  with beta-redexes

  @{ML_matchresult_fake [display, gray]

in

  pretty_term @{context} (redex $ arg1 $ arg2)

  |> pwriteln

  There is a dedicated configuration value for switching off tacit

  eta-contractions, namely @{ML_ind eta_contract in Syntax} (see Section

  \ref{sec:printing}), but none for beta-contractions. However you can avoid

  the beta-contractions by switching off abbreviations using the configuration

  value @{ML_ind show_abbrevs in Syntax}. For example

  @{ML_matchresult_fake [display, gray]

  val ctxt = Config.put show_abbrevs false @{context}

in

  pretty_term ctxt (redex $ arg1 $ arg2)

  |> pwriteln

  Isabelle makes a distinction between \emph{free} variables (term-constructor

  @{ML Free} and written on the user level in blue colour) and

  \emph{schematic} variables (term-constructor @{ML Var} and written with a

  leading question mark). Consider the following two examples

  @{ML_matchresult_fake [display, gray]

in

  pretty_terms @{context} [v1, v2, v3]

  |> pwriteln

  When constructing terms, you are usually concerned with free

  variables (as mentioned earlier, you cannot construct schematic

  variables using the built-in antiquotation \mbox{\<open>@{term

  \<dots>}\<close>}). If you deal with theorems, you have to, however, observe the

  distinction. The reason is that only schematic variables can be

  instantiated with terms when a theorem is applied. A similar

  distinction between free and schematic variables holds for types

  (see below).

  \begin{readmore}

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

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

  For constructing terms involving HOL constants, many helper functions are defined

  in @{ML_file "HOL/Tools/hologic.ML"}.

  \end{readmore}

  Constructing terms via antiquotations has the advantage that only typable

  terms can be constructed. For example

  @{ML_matchresult_fake_both [display,gray]

  raises a typing error, while it is perfectly ok to construct the term

  with the raw ML-constructors:

  @{ML_matchresult_fake [display,gray] 

in 

  pwriteln (pretty_term @{context} omega)

  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

  need to set the printing depth to a higher value by 

  \end{exercise}

\<close>

declare [[ML_print_depth = 50]]

text \<open>

  The antiquotation \<open>@{prop \<dots>}\<close> constructs terms by inserting the 

  usually invisible \<open>Trueprop\<close>-coercions whenever necessary. 

  Consider for example the pairs

  where a coercion is inserted in the second component and 

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

  The purpose of the \<open>Trueprop\<close>-coercion is to embed formulae of

  an object logic, for example HOL, into the meta-logic of Isabelle. The coercion

  is needed whenever a term is constructed that will be proved as a theorem. 

  As already seen above, types can be constructed using the antiquotation 

  \<open>@{typ _}\<close>. For example:

  The corresponding datatype is

\<close>

ML_val %grayML\<open>datatype typ =

  Type  of string * typ list 

| TFree of string * sort 

| TVar  of indexname * sort\<close>

text \<open>

  Like with terms, there is the distinction between free type

  a leading question mark). A type constant,

  like @{typ "int"} or @{typ bool}, are types with an empty list

  of argument types. However, it needs a bit of effort to show an

  example, because Isabelle always pretty prints types (unlike terms).

  Using just the antiquotation \<open>@{typ "bool"}\<close> we only see

  @{ML_matchresult [display, gray]

  which is the pretty printed version of \<open>bool\<close>. However, in PolyML

  (version \<open>\<ge>\<close>5.3) it is easy to install your own pretty printer. With the

  function below we mimic the behaviour of the usual pretty printer for

  datatypes (it uses pretty-printing functions which will be explained in more

  detail in Section~\ref{sec:pretty}).

\<close>

ML %grayML\<open>local

  fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]

  fun pp_list xs = Pretty.list "[" "]" xs

  fun pp_str s   = Pretty.str s

  fun pp_qstr s  = Pretty.quote (pp_str s)

  fun pp_int i   = pp_str (string_of_int i)

  fun pp_sort S  = pp_list (map pp_qstr S)

  fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]

in

fun raw_pp_typ (TVar ((a, i), S)) = 

      pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))

  | raw_pp_typ (TFree (a, S)) = 

      pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))

  | raw_pp_typ (Type (a, tys)) = 

      pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))

end\<close>

text \<open>

  We can install this pretty printer with the function 

  @{ML_ind ML_system_pp} as follows.

\<close>

ML %grayML\<open>ML_system_pp

  (fn _ => fn _ => Pretty.to_polyml o raw_pp_typ)\<close>

ML \<open>@{typ "bool"}\<close>

text \<open>

  Now the type bool is printed out in full detail.

  @{ML_matchresult [display,gray]

  When printing out a list-type

  @{ML_matchresult [display,gray]

  we can see the full name of the type is actually \<open>List.list\<close>, indicating

  that it is defined in the theory \<open>List\<close>. However, one has to be 

  careful with names of types, because even if

  \<open>fun\<close> is defined in the theory \<open>HOL\<close>, it is  

  still represented by its simple name.

   @{ML_matchresult [display,gray]

  We can restore the usual behaviour of Isabelle's pretty printer

  with the code

\<close>

ML %grayML\<open>ML_system_pp

  (fn depth => fn _ => ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure)\<close>

text \<open>

  After that the types for booleans, lists and so on are printed out again 

  the standard Isabelle way.

  @{ML_matchresult_fake [display, gray]

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

\<close>

section \<open>Constructing Terms and Types Manually\label{sec:terms_types_manually}\<close> 

text \<open>

  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 manually. For example, a

  function that returns the implication \<open>\<And>(x::nat). P x \<Longrightarrow> Q x\<close> taking

  @{term P} and @{term Q} as arguments can only be written as:

\<close>

ML %grayML\<open>fun make_imp P Q =

let

  val x = Free ("x", @{typ nat})

in 

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

end\<close>

text \<open>

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

  into an antiquotation.\footnote{At least not at the moment.} For example 

  the following does \emph{not} work.

\<close>

ML %grayML\<open>fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"}\<close>

text \<open>

  To see this, apply \<open>@{term S}\<close> and \<open>@{term T}\<close> 

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

  the given arguments

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

  and \<open>Q\<close> from the antiquotation.

  There are a number of handy functions that are frequently used for

  constructing terms. One is the function @{ML_ind list_comb in Term}, which

  takes as argument a term and a list of terms, and produces as output the

  term list applied to the term. For example

@{ML_matchresult_fake [display,gray]

in

  list_comb (trm, args)

  Another handy function is @{ML_ind lambda in Term}, which abstracts a variable 

  in a term. For example

  @{ML_matchresult_fake [display,gray]

in

  lambda x_nat trm

  and an abstraction, where it also records the type of the abstracted

  variable and for printing purposes also its name.  Note that because of the

  typing annotation on \<open>P\<close>, the variable \<open>x\<close> in \<open>P x\<close>

  is of the same type as the abstracted variable. If it is of different type,

  as in

  @{ML_matchresult_fake [display,gray]

in

  lambda x_int trm

  then the variable \<open>Free ("x", "nat")\<close> is \emph{not} abstracted. 

  This is a fundamental principle

  of Church-style typing, where variables with the same name still differ, if they 

  have different type.

  There is also the function @{ML_ind subst_free in Term} with which terms can be

  replaced by other terms. For example below, we will replace in @{term

  "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by

  @{term y}, and @{term x} by @{term True}.

  @{ML_matchresult_fake [display,gray]

in

  subst_free [sub1, sub2] trm

  As can be seen, @{ML subst_free} does not take typability into account.

  However it takes alpha-equivalence into account:

  @{ML_matchresult_fake [display, gray]

in

  subst_free [sub] trm

  Similarly the function @{ML_ind subst_bounds in Term}, replaces lose bound 

  variables with terms. To see how this function works, let us implement a

  function that strips off the outermost forall quantifiers in a term.

\<close>

ML %grayML\<open>fun strip_alls t =

let 

  fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T))

in

  case t of

    Const (@{const_name All}, _) $ Abs body => aux body

  | _ => ([], t)

end\<close>

text \<open>

  The function returns a pair consisting of the stripped off variables and

  the body of the universal quantification. For example

  @{ML_matchresult_fake [display, gray]

  Note that we produced in the body two dangling de Bruijn indices. 

  Later on we will also use the inverse function that

  builds the quantification from a body and a list of (free) variables.

\<close>

ML %grayML\<open>fun build_alls ([], t) = t

  | build_alls (Free (x, T) :: vs, t) = 

      Const (@{const_name "All"}, (T --> @{typ bool}) --> @{typ bool}) 

        $ Abs (x, T, build_alls (vs, t))\<close>

text \<open>

  As said above, after calling @{ML strip_alls}, you obtain a term with loose

  bound variables. With the function @{ML subst_bounds}, you can replace these

  loose @{ML_ind Bound in Term}s with the stripped off variables.

  @{ML_matchresult_fake [display, gray, linenos]

in 

  subst_bounds (rev vrs, trm) 

  |> pretty_term @{context}

  |> pwriteln

  Note that in Line 4 we had to reverse the list of variables that @{ML

  strip_alls} returned. The reason is that the head of the list the function

  Notice also that this function might introduce name clashes, since we

  substitute just a variable with the name recorded in an abstraction. This

  name is by no means unique. If clashes need to be avoided, then we should

  use the function @{ML_ind dest_abs in Term}, which returns the body where

  the loose de Bruijn index is replaced by a unique free variable. For example