1 theory Essential

     2 imports Base FirstSteps

     3 begin

     4 

     5 (*<*)

     6 setup{*

     7 open_file_with_prelude 

     8   "Esseantial_Code.thy"

     9   ["theory General", "imports Base FirstSteps", "begin"]

    10 *}

    11 (*>*)

    12 

    13 

    14 chapter {* Isabelle Essentials *}

    15 

    16 text {*

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

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

    19   everything else is build on top of this trusted core 

    20   \cite{GordonMilnerWadsworth79}. The fundamental data

    21   structures involved in this core are certified terms and certified types, 

    22   as well as theorems.

    23 *}

    24 

    25 

    26 section {* Terms and Types *}

    27 

    28 text {*

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

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

    31   using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example

    32 

    33   @{ML_response [display,gray] 

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

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

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

    37 

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

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

    40   which is defined as follows: 

    41 *}  

    42 

    43 ML_val %linenosgray{*datatype term =

    44   Const of string * typ 

    45 | Free of string * typ 

    46 | Var of indexname * typ 

    47 | Bound of int 

    48 | Abs of string * typ * term 

    49 | $ of term * term *}

    50 

    51 text {*

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

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

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

    55   representing bound variables.  For example in

    56 

    57   @{ML_response_fake [display, gray]

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

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

    60 

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

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

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

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

    65   (see Section~\ref{sec:typechecking}). Note that the names of bound variables

    66   are kept at abstractions for printing purposes, and so should be treated

    67   only as ``comments''.  Application in Isabelle is realised with the

    68   term-constructor @{ML $}.

    69 

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

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

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

    73   leading question mark). Consider the following two examples

    74   

    75   @{ML_response_fake [display, gray]

    76 "let

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

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

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

    80 in

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

    82   |> tracing

    83 end"

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

    85 

    86   When constructing terms, you are usually concerned with free variables (as

    87   mentioned earlier, you cannot construct schematic variables using the

    88   antiquotation @{text "@{term \<dots>}"}). If you deal with theorems, you have to,

    89   however, observe the distinction. The reason is that only schematic

    90   variables can be instantiated with terms when a theorem is applied. A

    91   similar distinction between free and schematic variables holds for types

    92   (see below).

    93 

    94   \begin{readmore}

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

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

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

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

    99   \end{readmore}

   100   

   101   Constructing terms via antiquotations has the advantage that only typable

   102   terms can be constructed. For example

   103 

   104   @{ML_response_fake_both [display,gray]

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

   106   "Type unification failed: Occurs check!"}

   107 

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

   109 

   110   @{ML_response_fake [display,gray] 

   111 "let

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

   113 in 

   114   tracing (string_of_term @{context} omega)

   115 end"

   116   "x x"}

   117 

   118   with the raw ML-constructors.

   119   

   120   Sometimes the internal representation of terms can be surprisingly different

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

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

   123 

   124   \begin{exercise}

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

   126   find out why they are represented like this:

   127 

   128   \begin{itemize}

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

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

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

   132   \end{itemize}

   133 

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

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

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

   137   value:

   138 

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

   140   \end{exercise}

   141 

   142   The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the 

   143   usually invisible @{text "Trueprop"}-coercions whenever necessary. 

   144   Consider for example the pairs

   145 

   146 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 

   147 "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),

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

   149  

   150   where a coercion is inserted in the second component and 

   151 

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

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

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

   155 

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

   157   The purpose of the @{text "Trueprop"}-coercion is to embed formulae of

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

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

   160 

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

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

   163 

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

   165 

   166   The corresponding datatype is

   167 *}

   168   

   169 ML_val{*datatype typ =

   170   Type  of string * typ list 

   171 | TFree of string * sort 

   172 | TVar  of indexname * sort *}

   173 

   174 text {*

   175   Like with terms, there is the distinction between free type

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

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

   178   a leading question mark). A type constant,

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

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

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

   182   Using just the antiquotation @{text "@{typ \"bool\"}"} we only see

   183 

   184   @{ML_response [display, gray]

   185   "@{typ \"bool\"}"

   186   "bool"}

   187 

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

   189   (version 5.3) it is easy to install your own pretty printer. With the

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

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

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

   193 *}

   194 

   195 ML{*local

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

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

   198   fun pp_str s   = Pretty.str s

   199   fun pp_qstr s  = Pretty.quote (pp_str s)

   200   fun pp_int i   = pp_str (string_of_int i)

   201   fun pp_sort S  = pp_list (map pp_qstr S)

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

   203 in

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

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

   206   | raw_pp_typ (TFree (a, S)) = 

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

   208   | raw_pp_typ (Type (a, tys)) = 

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

   210 end*}

   211 

   212 text {*

   213   We can install this pretty printer with the function 

   214   @{ML_ind addPrettyPrinter in PolyML} as follows.

   215 *}

   216 

   217 ML{*PolyML.addPrettyPrinter 

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

   219 

   220 text {*

   221   Now the type bool is printed out in full detail.

   222 

   223   @{ML_response [display,gray]

   224   "@{typ \"bool\"}"

   225   "Type (\"bool\", [])"}

   226 

   227   When printing out a list-type

   228   

   229   @{ML_response [display,gray]

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

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

   232 

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

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

   235   careful with names of types, because even if

   236   @{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the 

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

   238   still represented by their simple name.

   239 

   240    @{ML_response [display,gray]

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

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

   243 

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

   245   with the code

   246 *}

   247 

   248 ML{*PolyML.addPrettyPrinter 

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

   250 

   251 text {*

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

   253   the standard Isabelle way.

   254 

   255   @{ML_response_fake [display, gray]

   256   "@{typ \"bool\"};

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

   258   "\"bool\"

   259 \"'a List.list\""}

   260 

   261   \begin{readmore}

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

   263   definition and many useful operations are implemented 

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

   265   \end{readmore}

   266 *}

   267 

   268 section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} 

   269 

   270 text {*

   271   While antiquotations are very convenient for constructing terms, they can

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

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

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

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

   276 

   277 *}

   278 

   279 ML{*fun make_imp P Q =

   280 let

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

   282 in 

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

   284 end *}

   285 

   286 text {*

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

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

   289   the following does \emph{not} work.

   290 *}

   291 

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

   293 

   294 text {*

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

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

   297   the given arguments

   298 

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

   300 "Const \<dots> $ 

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

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

   303 

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

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

   306 

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

   308 "Const \<dots> $ 

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

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

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

   312 

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

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

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

   316   term list applied to the term. For example

   317 

   318 

   319 @{ML_response_fake [display,gray]

   320 "let

   321   val trm = @{term \"P::nat\"}

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

   323 in

   324   list_comb (trm, args)

   325 end"

   326 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}

   327 

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

   329   in a term. For example

   330 

   331   @{ML_response_fake [display,gray]

   332 "let

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

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

   335 in

   336   lambda x_nat trm

   337 end"

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

   339 

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

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

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

   343   typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}

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

   345   as in

   346 

   347   @{ML_response_fake [display,gray]

   348 "let

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

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

   351 in

   352   lambda x_int trm

   353 end"

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

   355 

   356   then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted. 

   357   This is a fundamental principle

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

   359   have different type.

   360 

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

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

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

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

   365 

   366   @{ML_response_fake [display,gray]

   367 "let

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

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

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

   371 in

   372   subst_free [sub1, sub2] trm

   373 end"

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

   375 

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

   377   However it takes alpha-equivalence into account:

   378 

   379   @{ML_response_fake [display, gray]

   380 "let

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

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

   383 in

   384   subst_free [sub] trm

   385 end"

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

   387 

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

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

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

   391 *}

   392 

   393 ML{*fun strip_alls t =

   394 let 

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

   396 in

   397   case t of

   398     Const ("All", _) $ Abs body => aux body

   399   | _ => ([], t)

   400 end*}

   401 

   402 text {*

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

   404   the body of the universal quantification. For example

   405 

   406   @{ML_response_fake [display, gray]

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

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

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

   410 

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

   412   the function @{ML subst_bounds}, you can replace these lose @{ML_ind 

   413   Bound in Term}s with the stripped off variables.

   414 

   415   @{ML_response_fake [display, gray, linenos]

   416   "let

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

   418 in 

   419   subst_bounds (rev vrs, trm) 

   420   |> string_of_term @{context}

   421   |> tracing

   422 end"

   423   "x = y"}

   424 

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

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

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

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

   429 

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

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

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

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

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

   435 

   436 

   437   @{ML_response_fake [display,gray]

   438   "let

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

   440 in

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

   442 end"

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

   444 

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

   446   in the structure @{ML_struct HOLogic}. For

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

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

   449   arguments. For example

   450 

   451 @{ML_response_fake [gray,display]

   452 "let

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

   454 in

   455   string_of_term @{context} eq

   456   |> tracing

   457 end"

   458   "True = False"}

   459 *}

   460 

   461 text {*

   462   \begin{readmore}

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

   464   "Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make manual

   465   constructions of terms and types easier.

   466   \end{readmore}

   467 

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

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

   470   when constructing them. While it is perfectly ok to write the function

   471   @{text is_true} as follows

   472 *}

   473 

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

   475   | is_true _ = false*}

   476 

   477 text {*

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

   479   the function 

   480 *}

   481 

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

   483   | is_all _ = false*}

   484 

   485 text {* 

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

   487 

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

   489 

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

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

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

   493   for this function is

   494 *}

   495 

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

   497   | is_all _ = false*}

   498 

   499 text {* 

   500   because now

   501 

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

   503 

   504   matches correctly (the first wildcard in the pattern matches any type and the

   505   second any term).

   506 

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

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

   509 *}

   510 

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

   512   | is_nil _ = false *}

   513 

   514 text {* 

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

   516 

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

   518 

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

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

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

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

   523 

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

   525 

   526   the name of the constant @{text "Nil"} depends on the theory in which the

   527   term constructor is defined (@{text "List"}) and also in which datatype

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

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

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

   531 

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

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

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

   535 

   536   While you could use the complete name, for example 

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

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

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

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

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

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

   543   matching against constants that have a polymorphic type should 

   544   be written as follows.

   545 *}

   546 

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

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

   549   | is_nil_or_all _ = false *}

   550 

   551 text {*

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

   553   For example

   554 

   555   @{ML_response [display,gray]

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

   557 

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

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

   560 

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

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

   563   @{ML_ind  Long_Name.base_name}. For example:

   564 

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

   566 

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

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

   569   strips off all qualifiers.

   570 

   571   \begin{readmore}

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

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

   574   \end{readmore}

   575 

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

   577   situations where you need to construct types manually, especially  

   578   when defining constants. For example the function returning a function 

   579   type is as follows:

   580 

   581 *} 

   582 

   583 ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}

   584 

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

   586 

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

   588 

   589 text {*

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

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

   592 *}

   593 

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

   595 

   596 text {*

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

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

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

   600 *}

   601 

   602 ML{*fun nat_to_int ty =

   603   (case ty of

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

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

   606    | _ => ty)*}

   607 

   608 text {*

   609   Here is an example:

   610 

   611 @{ML_response_fake [display,gray] 

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

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

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

   615 

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

   617   can use the function @{ML_ind  add_tfrees in Term} 

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

   619   One would expect that such functions

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

   621 

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

   623 

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

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

   626   call them as follows

   627 

   628   @{ML_response [gray,display]

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

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

   631 

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

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

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

   635 

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

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

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

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

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

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

   642   \end{exercise}

   643 

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

   645   Write a function that takes two terms representing natural numbers

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

   647   number representing their sum.

   648   \end{exercise}

   649 

   650   \begin{exercise}\label{ex:debruijn}

   651   Implement the function, which we below name deBruijn, that depends on a natural

   652   number n$>$0 and constructs terms of the form:

   653   

   654   \begin{center}

   655   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}

   656   {\it rhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n.  P\,i}\\

   657   {\it lhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n. P\,i = P (i + 1 mod n)}

   658                         $\longrightarrow$ {\it rhs n}\\

   659   {\it deBruijn n} & $\dn$ & {\it lhs n} $\longrightarrow$ {\it rhs n}\\

   660   \end{tabular}

   661   \end{center}

   662 

   663   This function returns for n=3 the term

   664 

   665   \begin{center}

   666   \begin{tabular}{l}

   667   (P 1 = P 2 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\wedge$\\

   668   (P 2 = P 3 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\wedge$\\ 

   669   (P 3 = P 1 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3

   670   \end{tabular}

   671   \end{center}

   672 

   673   Make sure you use the functions defined in @{ML_file "HOL/Tools/hologic.ML"}

   674   for constructing the terms for the logical connectives.\footnote{Thanks to Roy

   675   Dyckhoff for suggesting this exercise and working out the details.} 

   676   \end{exercise}

   677 *}

   678 

   679 section {* Unification and Matching *}

   680 

   681 text {* 

   682   As seen earlier, Isabelle's terms and types may contain schematic term variables

   683   (term-constructor @{ML Var}) and schematic type variables (term-constructor

   684   @{ML TVar}). These variables stand for unknown entities, which can be made

   685   more concrete by instantiations. Such instantiations might be a result of

   686   unification or matching. While in case of types, unification and matching is

   687   relatively straightforward, in case of terms the algorithms are

   688   substantially more complicated, because terms need higher-order versions of

   689   the unification and matching algorithms. Below we shall use the

   690   antiquotations @{text "@{typ_pat \<dots>}"} and @{text "@{term_pat \<dots>}"} from

   691   Section~\ref{sec:antiquote} in order to construct examples involving

   692   schematic variables.

   693 

   694   Let us begin with describing the unification and matching function for

   695   types.  Both return type environments (ML-type @{ML_type "Type.tyenv"})

   696   which map schematic type variables to types and sorts. Below we use the

   697   function @{ML_ind typ_unify in Sign} from the structure @{ML_struct Sign}

   698   for unifying the types @{text "?'a * ?'b"} and @{text "?'b list *

   699   nat"}. This will produce the mapping, or type environment, @{text "[?'a :=

   700   ?'b list, ?'b := nat]"}.

   701 *}

   702 

   703 ML %linenosgray{*val (tyenv_unif, _) = let

   704   val ty1 = @{typ_pat "?'a * ?'b"}

   705   val ty2 = @{typ_pat "?'b list * nat"}

   706 in

   707   Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) 

   708 end*}

   709 

   710 text {* 

   711   The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type

   712   environment, which is needed for starting the unification without any

   713   (pre)instantiations. The @{text 0} is an integer index that will be explained

   714   below. In case of failure @{ML typ_unify in Sign} will throw the exception

   715   @{text TUNIFY}.  We can print out the resulting type environment bound to 

   716   @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the

   717   structure @{ML_struct Vartab}.

   718 

   719   @{ML_response_fake [display,gray]

   720   "Vartab.dest tyenv_unif"

   721   "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")), 

   722  ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"} 

   723 *}

   724 

   725 text_raw {*

   726   \begin{figure}[t]

   727   \begin{minipage}{\textwidth}

   728   \begin{isabelle}*}

   729 ML{*fun pretty_helper aux env =

   730   env |> Vartab.dest  

   731       |> map ((fn (s1, s2) => s1 ^ " := " ^ s2) o aux) 

   732       |> commas 

   733       |> enclose "[" "]" 

   734       |> tracing

   735 

   736 fun pretty_tyenv ctxt tyenv =

   737 let

   738   fun get_typs (v, (s, T)) = (TVar (v, s), T)

   739   val print = pairself (Syntax.string_of_typ ctxt)

   740 in 

   741   pretty_helper (print o get_typs) tyenv

   742 end*}

   743 text_raw {*

   744   \end{isabelle}

   745   \end{minipage}

   746   \caption{A pretty printing function for type environments, which are 

   747   produced by unification and matching.\label{fig:prettyenv}}

   748   \end{figure}

   749 *}

   750 

   751 text {*

   752   The first components in this list stand for the schematic type variables and

   753   the second are the associated sorts and types. In this example the sort is

   754   the default sort @{text "HOL.type"}. Instead of @{ML "Vartab.dest"}, we will

   755   use in what follows our own pretty-printing function from

   756   Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s. For the type

   757   environment in the example this function prints out the more legible:

   758 

   759 

   760   @{ML_response_fake [display, gray]

   761   "pretty_tyenv @{context} tyenv_unif"

   762   "[?'a := ?'b list, ?'b := nat]"}

   763 

   764   The way the unification function @{ML typ_unify in Sign} is implemented 

   765   using an initial type environment and initial index makes it easy to

   766   unify more than two terms. For example 

   767 *}

   768 

   769 ML %linenosgray{*val (tyenvs, _) = let

   770   val tys1 = (@{typ_pat "?'a"}, @{typ_pat "?'b list"})

   771   val tys2 = (@{typ_pat "?'b"}, @{typ_pat "nat"})

   772 in

   773   fold (Sign.typ_unify @{theory}) [tys1, tys2] (Vartab.empty, 0) 

   774 end*}

   775 

   776 text {*

   777   The index @{text 0} in Line 5 is the maximal index of the schematic type

   778   variables occurring in @{text tys1} and @{text tys2}. This index will be

   779   increased whenever a new schematic type variable is introduced during

   780   unification.  This is for example the case when two schematic type variables

   781   have different, incomparable sorts. Then a new schematic type variable is

   782   introduced with the combined sorts. To show this let us assume two sorts,

   783   say @{text "s1"} and @{text "s2"}, which we attach to the schematic type

   784   variables @{text "?'a"} and @{text "?'b"}. Since we do not make any

   785   assumption about the sorts, they are incomparable.

   786 *}

   787 

   788 ML{*val (tyenv, index) = let

   789   val ty1 = @{typ_pat "?'a::s1"}

   790   val ty2 = @{typ_pat "?'b::s2"}

   791 in

   792   Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) 

   793 end*}

   794 

   795 text {*

   796   To print out the result type environment we switch on the printing 

   797   of sort information by setting @{ML_ind show_sorts in Syntax} to 

   798   true. This allows us to inspect the typing environment.

   799 

   800   @{ML_response_fake [display,gray]

   801   "pretty_tyenv @{context} tyenv"

   802   "[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]"}

   803 

   804   As can be seen, the type variables @{text "?'a"} and @{text "?'b"} are instantiated

   805   with a new type variable @{text "?'a1"} with sort @{text "{s1, s2}"}. Since a new

   806   type variable has been introduced the @{ML index}, originally being @{text 0}, 

   807   has been increased to @{text 1}.

   808 

   809   @{ML_response [display,gray]

   810   "index"

   811   "1"}

   812 

   813   Let us now return to the unification problem @{text "?'a * ?'b"} and 

   814   @{text "?'b list * nat"} from the beginning of this section, and the 

   815   calculated type environment @{ML tyenv_unif}:

   816 

   817   @{ML_response_fake [display, gray]

   818   "pretty_tyenv @{context} tyenv_unif"

   819   "[?'a := ?'b list, ?'b := nat]"}

   820 

   821   Observe that the type environment which the function @{ML typ_unify in

   822   Sign} returns is in \emph{not} an instantiation in fully solved form: while @{text

   823   "?'b"} is instantiated to @{typ nat}, this is not propagated to the

   824   instantiation for @{text "?'a"}.  In unification theory, this is often

   825   called an instantiation in \emph{triangular form}. These triangular 

   826   instantiations, or triangular type environments, are used because of 

   827   performance reasons. To apply such a type environment to a type, say @{text "?'a *

   828   ?'b"}, you should use the function @{ML_ind norm_type in Envir}:

   829 

   830   @{ML_response_fake [display, gray]

   831   "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"

   832   "nat list * nat"}

   833 

   834   Matching of types can be done with the function @{ML_ind typ_match in Sign}

   835   also from the structure @{ML_struct Sign}. This function returns a @{ML_type

   836   Type.tyenv} as well, but might raise the exception @{text TYPE_MATCH} in case

   837   of failure. For example

   838 *}

   839 

   840 ML{*val tyenv_match = let

   841   val pat = @{typ_pat "?'a * ?'b"}

   842   and ty  = @{typ_pat "bool list * nat"}

   843 in

   844   Sign.typ_match @{theory} (pat, ty) Vartab.empty 

   845 end*}

   846 

   847 text {*

   848   Printing out the calculated matcher gives

   849 

   850   @{ML_response_fake [display,gray]

   851   "pretty_tyenv @{context} tyenv_match"

   852   "[?'a := bool list, ?'b := nat]"}

   853   

   854   Unlike unification, which uses the function @{ML norm_type in Envir}, 

   855   applying the matcher to a type needs to be done with the function

   856   @{ML_ind subst_type in Envir}. For example

   857 

   858   @{ML_response_fake [display, gray]

   859   "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"

   860   "bool list * nat"}

   861 

   862   Be careful to observe the difference: use always 

   863   @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir} 

   864   for unifiers. To show the difference, let us calculate the 

   865   following matcher:

   866 *}

   867 

   868 ML{*val tyenv_match' = let

   869   val pat = @{typ_pat "?'a * ?'b"}

   870   and ty  = @{typ_pat "?'b list * nat"}

   871 in

   872   Sign.typ_match @{theory} (pat, ty) Vartab.empty 

   873 end*}

   874 

   875 text {*

   876   Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. If we apply 

   877   @{ML norm_type in Envir} to the type @{text "?'a * ?'b"} we obtain

   878 

   879   @{ML_response_fake [display, gray]

   880   "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"

   881   "nat list * nat"}

   882 

   883   which does not solve the matching problem, and if

   884   we apply @{ML subst_type in Envir} to the same type we obtain

   885 

   886   @{ML_response_fake [display, gray]

   887   "Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"

   888   "?'b list * nat"}

   889   

   890   which does not solve the unification problem.

   891 

   892   \begin{readmore}

   893   Unification and matching for types is implemented

   894   in @{ML_file "Pure/type.ML"}. The ``interface'' functions for them

   895   are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments

   896   as results. These are implemented in @{ML_file "Pure/envir.ML"}.

   897   This file also includes the substitution and normalisation functions,

   898   which apply a type environment to a type. Type environments are lookup 

   899   tables which are implemented in @{ML_file "Pure/term_ord.ML"}.

   900   \end{readmore}

   901 *}

   902 

   903 text {*

   904   Unification and matching of terms is substantially more complicated than the

   905   type-case. The reason is that terms have abstractions and, in this context,  

   906   unification or matching modulo plain equality is often not meaningful. 

   907   Nevertheless, Isabelle implements the function @{ML_ind

   908   first_order_match in Pattern} for terms.  This matching function returns a

   909   type environment and a term environment.  To pretty print the latter we use

   910   the function @{text "pretty_env"}:

   911 *}

   912 

   913 ML{*fun pretty_env ctxt env =

   914 let

   915   fun get_trms (v, (T, t)) = (Var (v, T), t) 

   916   val print = pairself (string_of_term ctxt)

   917 in

   918   pretty_helper (print o get_trms) env 

   919 end*}

   920 

   921 text {*

   922   As can be seen from the @{text "get_trms"}-function, a term environment associates 

   923   a schematic term variable with a type and a term.  An example of a first-order 

   924   matching problem is the term @{term "P (\<lambda>a b. Q b a)"} and the pattern 

   925   @{text "?X ?Y"}.

   926 *}

   927 

   928 ML{*val (_, fo_env) = let

   929   val fo_pat = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}

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

   931   val trm_b = @{term "\<lambda>a b. (Q::nat\<Rightarrow>nat\<Rightarrow>nat) b a"}

   932   val init = (Vartab.empty, Vartab.empty) 

   933 in

   934   Pattern.first_order_match @{theory} (fo_pat, trm_a $ trm_b) init

   935 end *}

   936 

   937 text {*

   938   In this example we annotated explicitly types because then 

   939   the type environment is empty and can be ignored. The 

   940   resulting term environment is

   941 

   942   @{ML_response_fake [display, gray]

   943   "pretty_env @{context} fo_env"

   944   "[?X := P, ?Y := \<lambda>a b. Q b a]"}

   945 

   946   The matcher can be applied to a term using the function @{ML_ind subst_term

   947   in Envir} (remember the same convention for types applies to terms: @{ML

   948   subst_term in Envir} is for matchers and @{ML norm_term in Envir} for

   949   unifiers). The function @{ML subst_term in Envir} expects a type environment,

   950   which is set to empty in the example below, and a term environment.

   951 

   952   @{ML_response_fake [display, gray]

   953   "let

   954   val trm = @{term_pat \"(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y\"}

   955 in

   956   Envir.subst_term (Vartab.empty, fo_env) trm

   957   |> string_of_term @{context}

   958   |> tracing

   959 end"

   960   "P (\<lambda>a b. Q b a)"}

   961 

   962   First-order matching is useful for matching against applications and

   963   variables. It can deal also with abstractions and a limited form of

   964   alpha-equivalence, but this kind of matching should be used with care, since

   965   it is not clear whether the result is meaningful. A meaningful example is

   966   matching @{text "\<lambda>x. P x"} against the pattern @{text "\<lambda>y. ?X y"}. In this

   967   case, first-order matching produces @{text "[?X := P]"}.

   968 

   969   @{ML_response_fake [display, gray]

   970   "let

   971   val fo_pat = @{term_pat \"\<lambda>y. (?X::nat\<Rightarrow>bool) y\"}

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

   973   val init = (Vartab.empty, Vartab.empty) 

   974 in

   975   Pattern.first_order_match @{theory} (fo_pat, trm) init

   976   |> snd 

   977   |> pretty_env @{context} 

   978 end"

   979   "[?X := P]"}

   980 *}

   981 

   982 text {*

   983   Unification of abstractions is more thoroughly studied in the context

   984   of higher-order pattern unification and higher-order pattern matching.  A

   985   \emph{\index*{pattern}} is an abstraction term whose ``head symbol'' (that is the

   986   first symbol under an abstraction) is either a constant, a schematic or a free

   987   variable. If it is a schematic variable then it can be only applied with

   988   distinct bound variables. This excludes terms where a schematic variable is an

   989   argument of another one and where a schematic variable is applied

   990   twice with the same bound variable. The function @{ML_ind pattern in Pattern}

   991   in the structure @{ML_struct Pattern} tests whether a term satisfies these

   992   restrictions.

   993 

   994   @{ML_response [display, gray]

   995   "let

   996   val trm_list = 

   997         [@{term_pat \"?X\"},              @{term_pat \"a\"},

   998          @{term_pat \"\<lambda>a b. ?X a b\"},    @{term_pat \"\<lambda>a b. (op +) a b\"},

   999          @{term_pat \"\<lambda>a. (op +) a ?Y\"}, @{term_pat \"?X ?Y\"},

  1000          @{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"}] 

  1001 in

  1002   map Pattern.pattern trm_list

  1003 end"

  1004   "[true, true, true, true, true, false, false, false]"}

  1005 

  1006   The point of the restriction to patterns is that unification and matching 

  1007   are decidable and produce most general unifiers, respectively matchers. 

  1008   In this way, matching and unification can be implemented as functions that 

  1009   produce a type and term environment (unification actually returns a 

  1010   record of type @{ML_type Envir.env} containing a maxind, a type environment 

  1011   and a term environment). The corresponding functions are @{ML_ind match in Pattern},

  1012   and @{ML_ind unify in Pattern} both implemented in the structure

  1013   @{ML_struct Pattern}. An example for higher-order pattern unification is

  1014 

  1015   @{ML_response_fake [display, gray]

  1016   "let

  1017   val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}

  1018   val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"}

  1019   val init = Envir.empty 0

  1020   val env = Pattern.unify @{theory} (trm1, trm2) init

  1021 in

  1022   pretty_env @{context} (Envir.term_env env)

  1023 end"

  1024   "[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]"}

  1025 

  1026   The function @{ML_ind "Envir.empty"} generates a record with a specified

  1027   max-index for the schematic variables (in the example the index is @{text

  1028   0}) and empty type and term environments. The function @{ML_ind

  1029   "Envir.term_env"} pulls out the term environment from the result record. The

  1030   function for type environment is @{ML_ind "Envir.type_env"}. An assumption of

  1031   this function is that the terms to be unified have already the same type. In

  1032   case of failure, the exceptions that are raised are either @{text Pattern},

  1033   @{text MATCH} or @{text Unif}.

  1034 

  1035   As mentioned before, unrestricted higher-order unification, respectively

  1036   higher-order matching, is in general undecidable and might also not posses a

  1037   single most general solution. Therefore Isabelle implements the unification

  1038   function @{ML_ind unifiers in Unify} so that it returns a lazy list of

  1039   potentially infinite unifiers.  An example is as follows

  1040 *}

  1041 

  1042 ML{*val uni_seq =

  1043 let 

  1044   val trm1 = @{term_pat "?X ?Y"}

  1045   val trm2 = @{term "f a"}

  1046   val init = Envir.empty 0

  1047 in

  1048   Unify.unifiers (@{theory}, init, [(trm1, trm2)])

  1049 end *}

  1050 

  1051 text {*

  1052   The unifiers can be extracted from the lazy sequence using the 

  1053   function @{ML_ind "Seq.pull"}. In the example we obtain three 

  1054   unifiers @{text "un1\<dots>un3"}.

  1055 *}

  1056 

  1057 ML{*val SOME ((un1, _), next1) = Seq.pull uni_seq;

  1058 val SOME ((un2, _), next2) = Seq.pull next1;

  1059 val SOME ((un3, _), next3) = Seq.pull next2;

  1060 val NONE = Seq.pull next3 *}

  1061 

  1062 text {*

  1063   \footnote{\bf FIXME: what is the list of term pairs in the unifier: flex-flex pairs?}

  1064 

  1065   We can print them out as follows.

  1066 

  1067   @{ML_response_fake [display, gray]

  1068   "pretty_env @{context} (Envir.term_env un1);

  1069 pretty_env @{context} (Envir.term_env un2);

  1070 pretty_env @{context} (Envir.term_env un3)"

  1071   "[?X := \<lambda>a. a, ?Y := f a]

  1072 [?X := f, ?Y := a]

  1073 [?X := \<lambda>b. f a]"}

  1074 

  1075 

  1076   In case of failure the function @{ML_ind unifiers in Unify} does not raise

  1077   an exception, rather returns the empty sequence. For example

  1078 

  1079   @{ML_response [display, gray]

  1080 "let 

  1081   val trm1 = @{term \"a\"}

  1082   val trm2 = @{term \"b\"}

  1083   val init = Envir.empty 0

  1084 in

  1085   Unify.unifiers (@{theory}, init, [(trm1, trm2)])

  1086   |> Seq.pull

  1087 end"

  1088 "NONE"}

  1089 

  1090   In order to find a

  1091   reasonable solution for a unification problem, Isabelle also tries first to

  1092   solve the problem by higher-order pattern unification. 

  1093 

  1094   For higher-order

  1095   matching the function is called @{ML_ind matchers in Unify} implemented

  1096   in the structure @{ML_struct Unify}. Also this

  1097   function returns sequences with possibly more than one matcher.

  1098   Like @{ML unifiers in Unify}, this function does not raise an exception

  1099   in case of failure, but returns an empty sequence. It also first tries 

  1100   out whether the matching problem can be solved by first-order matching.

  1101 

  1102   \begin{readmore}

  1103   Unification and matching of higher-order patterns is implemented in 

  1104   @{ML_file "Pure/pattern.ML"}. This file also contains a first-order matcher

  1105   for terms. Full higher-order unification is implemented

  1106   in @{ML_file "Pure/unify.ML"}. It uses lazy sequences which are implemented

  1107   in @{ML_file "Pure/General/seq.ML"}.

  1108   \end{readmore}

  1109 *}

  1110 

  1111 section {* Sorts (TBD) *}

  1112 

  1113 

  1114 section {* Type-Checking\label{sec:typechecking} *}

  1115 

  1116 text {* 

  1117   Remember Isabelle follows the Church-style typing for terms, i.e., a term contains 

  1118   enough typing information (constants, free variables and abstractions all have typing 

  1119   information) so that it is always clear what the type of a term is. 

  1120   Given a well-typed term, the function @{ML_ind type_of in Term} returns the 

  1121   type of a term. Consider for example:

  1122 

  1123   @{ML_response [display,gray] 

  1124   "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}

  1125 

  1126   To calculate the type, this function traverses the whole term and will

  1127   detect any typing inconsistency. For example changing the type of the variable 

  1128   @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message: 

  1129 

  1130   @{ML_response_fake [display,gray] 

  1131   "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" 

  1132   "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}

  1133 

  1134   Since the complete traversal might sometimes be too costly and