theory General

imports Base FirstSteps

begin

chapter {* Isabelle -- The Good, the Bad and the Ugly *}

text {*

  Isabelle is build around a few central ideas. One is the LCF-approach to

  theorem proving where there is a small trusted core and everything else is

  build on top of this trusted core. The central data structures involved

  in this core are certified terms and types as well as theorems.

*}

section {* Terms and Types *}

text {*

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

  terms. The latter are called just 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>"}

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

  representation corresponding to the datatype @{ML_type  "term"} 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 lambda-terms typed in Church-style.

  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

  varaibles 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}) $ 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. It

  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"}). A type constant,

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

  of argument types. However, it is a bit difficult to show an

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

  Here is a contrived example:

  @{ML_response [display, gray]

  "if Type (\"bool\", []) = @{typ \"bool\"} then true else false"

  "true"}

  \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}, which takes a term

  and a list of terms as arguments, 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}, 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. 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} 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}, 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 (Const ("All", _) $ Abs (n, T, t)) =

         strip_alls t |>> cons (Free (n, T))

  | strip_alls t = ([], t) *}

text {*

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

  the body of the universal quantifications. 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}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. 

  There are many convenient functions that construct specific HOL-terms. 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 such 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

  second any term).

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

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

*}

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 than 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 @{text "Nil"} depends on the theory in which the

  term constructor 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"} and

  \mbox{@{text "(op *)"}}:

  @{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 function 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 {*

  The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.

  For example

  @{ML_response [display,gray]

  "@{type_name \"list\"}" "\"List.list\""}

  \footnote{\bf FIXME: Explain the following better; maybe put in a separate

  section and link with the comment in the antiquotation section.}

  Occasionally you have to calculate what the ``base'' name of a given

  constant is. For this you can use the function @{ML_ind  "Sign.extern_const"} or

  @{ML_ind  Long_Name.base_name}. For example:

  @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}

  The difference between both functions is that @{ML extern_const in Sign} returns

  the smallest name that is still unique, whereas @{ML base_name in Long_Name} always

  strips off all qualifiers.

  \begin{readmore}

  Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};

  functions about signatures in @{ML_file "Pure/sign.ML"}.

  \end{readmore}

  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 ty1 ty2 = Type ("fun", [ty1, ty2]) *}

text {* This can be equally written with the combinator @{ML_ind  "-->"} as: *}

ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}

text {*

  If you want to construct a function type with more than one argument

  type, then you can use @{ML_ind  "--->"}.

*}

ML{*fun make_fun_types tys ty = tys ---> ty *}

text {*

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

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

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

*}

ML{*fun nat_to_int ty =

  (case ty of

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

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

   | _ => ty)*}

text {*

  Here is an example:

@{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\")"}

  If you want to obtain the list of free type-variables of a term, you

  can use the function @{ML_ind  add_tfrees in Term} 

  (similarly @{ML_ind  add_tvars in Term} for the schematic type-variables). 

  One would expect that such functions

  take a term as input and return a list of types. But their type is actually 

  @{text[display] "Term.term -> (string * Term.sort) list -> (string * Term.sort) list"}

  that is they take, besides a term, also a list of type-variables as input. 

  So in order to obtain the list of type-variables of a term you have to 

  call them as follows

  @{ML_response [gray,display]

  "Term.add_tfrees @{term \"(a, b)\"} []"

  "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}

  The reason for this definition is that @{ML add_tfrees in Term} can

  be easily folded over a list of terms. Similarly for all functions

  named @{text "add_*"} in @{ML_file "Pure/term.ML"}.