867   skip until we hit the @{ML Abs} that binds the corresponding variable. Constructing 

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

   868   a term with dangling de Bruijn indices is possible, but will be flagged as

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

   869   ill-formed when you try to typecheck or certify it (see

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

   870   Section~\ref{sec:typechecking}). Note that the names of bound variables are kept at

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

   871   abstractions for printing purposes, and so should be treated only as

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

   872   ``comments''.  Application in Isabelle is realised with the term-constructor

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

   873   @{ML $}.

   873   term-constructor @{ML $}.

   874 

   877   @{ML Free} and written in blue colour) and \emph{schematic} variables

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

   878   (term-constructor @{ML Var} and written with a leading question mark). The

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

   879   latter correspond to the schematic variables that when printed show up with

   878   leading question mark). Consider the following two examples

   880   a question mark in front of them. Consider the following two examples

   879 

   894   When constructing terms, you are usually concerned with free variables (as mentioned earlier,

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

   895   you cannot construct schematic variables using the antiquotation @{text "@{term \<dots>}"}). 

   894   mentioned earlier, you cannot construct schematic variables using the

   896   If you deal with theorems, you have to, however, observe the distinction. A similar

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

   897   distinction holds for types (see below).

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

   897   varaibles can be instantiated with terms when a theorem is applied. A

   898   similar distinction between free and schematic variables holds for types

   899   (see below).

   947   The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 

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

   948   inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 

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

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

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

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

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

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

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

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

  1098   subst_free [s1, s2] trm

  1104   subst_free [sub1, sub2] trm

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

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

  1110   subst_free [s] trm

  1116   subst_free [sub] trm

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

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

  1159   tracing (string_of_term @{context} eq)

  1165   string_of_term @{context} eq

  1166   |> tracing

  1282   and types easier.\end{readmore}

  1264   and types easier.

  1283 

  1265   \end{readmore}

  1284   Have a look at these files and try to solve the following two exercises:

  1266 

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

  1268   For example

  1269 

  1270   @{ML_response [display,gray]

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

  1272 

  1273   (FIXME: Explain the following better.)

  1274 

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

  1276   constant is. For this you can use the function @{ML [index] "Sign.extern_const"} or

  1277   @{ML [index] Long_Name.base_name}. For example:

  1278 

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

  1280 

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

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

  1283   strips off all qualifiers.

  1284 

  1285   \begin{readmore}

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

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

  1288   \end{readmore}

  1289 

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

  1291   situations where you need to construct types manually, especially  

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

  1293   type is as follows:

  1294 

  1295 *} 

  1296 

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

  1298 

  1299 text {* This can be equally written with the combinator @{ML [index] "-->"} as: *}

  1300 

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

  1302 

  1303 text {*

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

  1305   type, then you can use @{ML [index] "--->"}.

  1306 *}

  1307 

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

  1309 

  1310 text {*

  1311   A handy function for manipulating terms is @{ML [index] map_types}: it takes a 

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

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

  1314 *}

  1315 

  1316 ML{*fun nat_to_int ty =

  1317   (case ty of

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

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

  1320    | _ => ty)*}

  1321 

  1322 text {*

  1323   Here is an example:

  1324 

  1325 @{ML_response_fake [display,gray] 

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

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

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

  1329 

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

  1331   can use the function @{ML [index] add_tfrees in Term} 

  1332   (similarly @{ML [index] add_tvars in Term} for the schematic type-variables). 

  1333   One would expect that such functions

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

  1335 

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

  1337 

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

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

  1340   call them as follows

  1341 

  1342   @{ML_response [gray,display]

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

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

  1345 

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

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

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

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

  1364   \begin{exercise}\footnote{Personal communication of

  1301   For example

  1365   de Bruijn to Dyckhoff.}\label{ex:debruijn}

  1302 

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

  1303   @{ML_response [display,gray]

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

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

  1368   

  1305 

  1369   \begin{center}

  1306   (FIXME: Explain the following better.)

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

  1307 

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

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

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

  1309   constant is. For this you can use the function @{ML [index] "Sign.extern_const"} or

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

  1310   @{ML [index] Long_Name.base_name}. For example:

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

  1311 

  1375   \end{tabular}

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

  1376   \end{center}

  1313 

  1377 

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

  1378   For n=3 this function returns the term

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

  1379 

  1316   strips off all qualifiers.

  1380   \begin{center}

  1317 

  1381   \begin{tabular}{l}

  1318   \begin{readmore}

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

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

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

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

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

  1321   \end{readmore}

  1385   \end{tabular}

  1322 

  1386   \end{center}

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

  1387 

  1324   situations where you need to construct types manually, especially  

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

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

  1389   for constructing the terms for the logical connectives. 

  1326   type is as follows:

  1390   \end{exercise}

  1327 

  1328 *} 

  1329 

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

  1331 

  1332 text {* This can be equally written with the combinator @{ML [index] "-->"} as: *}

  1333 

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

  1335 

  1336 text {*

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

  1338   type, then you can use @{ML [index] "--->"}.

  1339 *}

  1340 

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

  1342 

  1343 text {*

  1344   A handy function for manipulating terms is @{ML [index] map_types}: it takes a 

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

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

  1347 *}

  1348 

  1349 ML{*fun nat_to_int ty =

  1350   (case ty of

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

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

  1353    | _ => ty)*}

  1354 

  1355 text {*

  1356   Here is an example:

  1357 

  1358 @{ML_response_fake [display,gray] 

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

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

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

  1362 

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

  1364   can use the function @{ML [index] add_tfrees in Term} 

  1365   (similarly @{ML [index] add_tvars in Term} for the schematic type-variables). 

  1366   One would expect that such functions

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

  1368 

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

  1370 

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

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

  1373   call them as follows

  1374 

  1375   @{ML_response [gray,display]

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

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

  1378 

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

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

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

  1382