theory Essential

imports Base First_Steps

begin

chapter {* Isabelle Essentials *}

text {*

   \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

  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.

*}

section {* Terms and Types *}

text {*

  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{@{text "@{term \<dots>}"}}. For example

  @{ML_response [display,gray] 

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

"Const (\"HOL.eq\", \<dots>) $ 

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

  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: 

*}  

ML_val %linenosgray{*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 *}

text {*

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

  @{ML_response_fake [display, gray]

  "@{term \"\<lambda>x y. x y\"}"

  "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}

  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_response_fake [display, gray]

"@{term \"\<lambda>x y. x y\"}

  |> pretty_term @{context}

  |> pwriteln"

  "\<lambda>x. x"}

  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_response_fake [display, gray]

  "1"}

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

  value @{ML_ind show_abbrevs in Syntax}. For example

  @{ML_response_fake [display, gray]

  "(\<lambda>x y. x) 1 2"}

  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_response_fake [display, gray]

"let

  val v1 = Var ((\"x\", 3), @{typ bool})

  val v2 = Var ((\"x1\", 3), @{typ bool})

  val v3 = Free (\"x\", @{typ bool})

in

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

  |> pwriteln

end"

"?x3, ?x1.3, x"}

  When constructing terms, you are usually concerned with free

  variables (as mentioned earlier, you cannot construct schematic

  variables using the built in antiquotation \mbox{@{text "@{term

  \<dots>}"}}). 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_response_fake_both [display,gray]

  "@{term \"x x\"}"

  "Type unification failed: Occurs check!"}

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

  with the raw ML-constructors:

  @{ML_response_fake [display,gray] 

"let

  val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})

in 

  pwriteln (pretty_term @{context} omega)

end"

  "x x"}

  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 by inserting the 

  usually 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 (\"HOL.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). 

  The purpose of the @{text "Trueprop"}-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 

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

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

  The corresponding datatype is

*}

  Type  of string * typ list 

| TFree of string * sort 

| TVar  of indexname * sort *}

text {*

  Like with terms, there is the distinction between free type

  variables (term-constructor @{ML "TFree"}) and schematic

  type variables (term-constructor @{ML "TVar"} and printed with

  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 @{text "@{typ \"bool\"}"} we only see

  @{ML_response [display, gray]

  "@{typ \"bool\"}"

  "bool"}

  which is the pretty printed version of @{text "bool"}. However, in PolyML

  (version @{text "\<ge>"}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}).

*}

ML %grayML{*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*}

text {*

  We can install this pretty printer with the function 

  @{ML_ind addPrettyPrinter in PolyML} as follows.

*}

ML %grayML{*PolyML.addPrettyPrinter 

  (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)*}

text {*

  Now the type bool is printed out in full detail.

  @{ML_response [display,gray]

  "@{typ \"bool\"}"

  "Type (\"HOL.bool\", [])"}

  When printing out a list-type

  @{ML_response [display,gray]

  "@{typ \"'a list\"}"

  "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"}

  we can see the full name of the type is actually @{text "List.list"}, indicating

  that it is defined in the theory @{text "List"}. However, one has to be 

  careful with names of types, because even if

  @{text "fun"} is defined in the theory @{text "HOL"}, it is  

  still represented by their simple name.

   @{ML_response [display,gray]

  "@{typ \"bool \<Rightarrow> nat\"}"

  "Type (\"fun\", [Type (\"HOL.bool\", []), Type (\"Nat.nat\", [])])"}

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

  with the code

*}

ML %grayML{*PolyML.addPrettyPrinter 

  (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy)*}

text {*

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

  the standard Isabelle way.

  @{ML_response_fake [display, gray]

  "@{typ \"bool\"};

@{typ \"'a list\"}"

  "\"bool\"

\"'a List.list\""}

  \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\label{sec:terms_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 manually. For example, a

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

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

*}

ML %grayML{*fun make_imp P Q =

let

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

in 

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

end *}

text {*

  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.

*}

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

text {*

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

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

  the given arguments

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

"Const \<dots> $ 

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

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

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

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

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

"Const \<dots> $ 

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

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

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

  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_response_fake [display,gray]

"let

  val trm = @{term \"P::bool \<Rightarrow> bool \<Rightarrow> bool\"}

  val args = [@{term \"True\"}, @{term \"False\"}]

in

  list_comb (trm, args)

end"

"Free (\"P\", \"bool \<Rightarrow> bool \<Rightarrow> bool\") 

   $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}

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

  in a term. For example

  @{ML_response_fake [display,gray]

"let

  val x_nat = @{term \"x::nat\"}

  val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}

in

  lambda x_nat trm

end"

  "Abs (\"x\", \"Nat.nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}

  In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), 

  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 @{text "P"}, the variable @{text "x"} in @{text "P x"}

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

  as in

  @{ML_response_fake [display,gray]

"let

  val x_int = @{term \"x::int\"}

  val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}

in

  lambda x_int trm

end"

  "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}

  then the variable @{text "Free (\"x\", \"nat\")"} 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_response_fake [display,gray]

"let

  val sub1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})

  val sub2 = (@{term \"x::nat\"}, @{term \"True\"})

  val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}

in

  subst_free [sub1, sub2] trm

end"

  "Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}

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

  However it takes alpha-equivalence into account:

  @{ML_response_fake [display, gray]

"let

  val sub = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})

  val trm = @{term \"(\<lambda>x::nat. x)\"}

in

  subst_free [sub] trm

end"

  "Free (\"x\", \"nat\")"}

  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.

*}

ML %grayML{*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*}

text {*

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

  the body of the universal quantification. For example

  @{ML_response_fake [display, gray]

  "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"

"([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],

  Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}

  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.

*}

ML %grayML{*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))*}

text {*

  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_response_fake [display, gray, linenos]

  "let

  val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}

in 

  subst_bounds (rev vrs, trm) 

  |> pretty_term @{context}

  |> pwriteln

end"

  "x = y"}

  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

  @{ML subst_bounds} takes is the replacement for @{ML "Bound 0"}, the next

  element for @{ML "Bound 1"} and so on. 

  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

  @{ML_response_fake [display,gray]

  "let

  val body = Bound 0 $ Free (\"x\", @{typ nat})

in

  Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body)

end"

  "(\"xa\", Free (\"xa\", \"Nat.nat \<Rightarrow> bool\") $ Free (\"x\", \"Nat.nat\"))"}

  Sometimes it is necessary to manipulate de Bruijn indices in terms directly.

  There are many functions to do this. We describe only two. The first,

  @{ML_ind incr_boundvars in Term}, increases by an integer the indices 

  of the loose bound variables in a term. In the code below

@{ML_response_fake [display,gray]

"@{term \"\<forall>x y z u. z = u\"}