theory Essential

imports Base FirstSteps

begin

(*<*)

setup{*

open_file_with_prelude 

  "Essential_Code.thy"

  ["theory Essential", "imports Base FirstSteps", "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

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

  LCF-approach to theorem proving where there is a small trusted core and

  everything else is built on top of this trusted core 

  \cite{GordonMilnerWadsworth79}. 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 (\"op =\", \<dots>) $ 

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

  explicitly recorded in variables, constants and abstractions.  As can be

  seen in Line 5, terms use the usual de Bruijn index mechanism for

  representing bound variables.  For example in

  @{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 $}.

  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

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

  |> tracing

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

  antiquotation @{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

  @{ML_response_fake [display,gray] 

"let

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

in 

  tracing (string_of_term @{context} omega)

end"

  "x x"}

  with the raw ML-constructors.

  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 (\"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

*}

ML_val{*datatype typ =

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

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

  (version 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{*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{*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 (\"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"}, @{text "bool"} and @{text "nat"} are defined in the 

  theories @{text "HOL"} and @{text "Nat"}, respectively, they are 

  still represented by their simple name.

   @{ML_response [display,gray]

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

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

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

  with the code

*}

ML{*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{*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{*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\",[]),

    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::nat\"}

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

in

  list_comb (trm, args)

end"

"Free (\"P\", \"nat\") $ 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\", 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\", \"int\")"} 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 quantifiers in a term.

*}

ML{*fun strip_alls t =

let 

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

in

  case t of

    Const ("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)"}

  After calling @{ML strip_alls}, you obtain a term with lose bound variables. With

  the function @{ML subst_bounds}, you can replace these lose @{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) 

  |> string_of_term @{context}

  |> tracing

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 lose 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 \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}

  There are also many convenient functions that construct specific HOL-terms

  in the structure @{ML_struct HOLogic}. For

  example @{ML_ind mk_eq in HOLogic} constructs an equality out of two terms.

  The types needed in this equality are calculated from the type of the

  arguments. For example

@{ML_response_fake [gray,display]

"let

  val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})

in

  string_of_term @{context} eq

  |> tracing

end"

  "True = False"}

*}

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 manual

  constructions of terms and types easier.

  \end{readmore}

  When constructing terms manually, there are a few subtle issues with

  constants. They usually crop up when pattern matching terms or types, or

  when constructing them. 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[source] "\<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 first wildcard in the pattern matches any type and the