384 *}

   384 

   385   There are a few subtle issues with constants. They usually crop up when

   386   pattern matching terms or constructing terms. While it is perfectly ok

   387   to write the function @{text is_true} as follows

   388 *}

   389 

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

   391   | is_true _ = false*}

   392 

   393 text {*

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

   395   the function 

   396 *}

   397 

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

   399   | is_all _ = false*}

   400 

   401 text {* 

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

   403 

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

   405 

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

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

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

   409   for this function is

   410 *}

   411 

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

   413   | is_all _ = false*}

   414 

   415 text {* 

   416   because now

   417 

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

   419 

   420   matches correctly (the wildcard in the pattern matches any type).

   421 

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

   423   attempts to pick out a @{text "Nil"}-term:

   424 *}

   425 

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

   427   | is_nil _ = false *}

   428 

   429 text {* 

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

   431 

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

   433 

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

   435   subtle as you might expect. The function @{ML is_all} worked correctly,

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

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

   438 

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

   440 

   441   the name of the constant depends on the theory in which the term constructor

   442   @{text "Nil"} is defined (@{text "List"}) and also in which datatype 

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

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

   445   and @{text "(op *)"}:

   446 

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

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

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

   450 

   451   While you could use the complete name, for example 

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

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

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

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

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

   457   variable parts of the constant's name. Therefore a functions for 

   458   matching against constants that have a polymorphic type should 

   459   be written as follows.

   460 *}

   461 

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

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

   464   | is_nil_or_all _ = false *}

   465 

   466 text {*

   467   Note that you occasional have to calculate what the ``base'' name of a given

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

   469   @{ML Sign.base_name}. For example:

   470 

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

   472 

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

   474   the smallest name which is still unique, while @{ML base_name in Sign} always

   475   strips off all qualifiers.

   476 

   477   (FIXME authentic syntax on the ML-level)

   478 

   479   \begin{readmore}

   480   FIXME

   481   \end{readmore}

   482 *}

   483 

   431   (FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT})

   530   Remember that in Isabelle a term contains enough typing information

   432 

   531   (constants, free variables and abstractions all have typing 

   433   (FIXME: say something about constants and variables having types as

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

   434   arguments and how they can be constructed with fast-type and dummT)

   533   Given a well-typed term, the function @{ML type_of} returns the 

   435 *}

   534   type of a term. Consider for example:

   436 

   535 

   437 section {* Constants *}

   536   @{ML_response [display,gray] 

   438 

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

   439 text {*

   538 

   440   There are a few subtle issues with constants. They usually crop up when

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

   441   pattern matching terms or constructing terms. While it is perfectly ok

   540   detect any inconsistency. For examle changing the type of the variable 

   442   to write the function @{text is_true} as follows

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

   443 *}

   542 

   444 

   543   @{ML_response_fake [display,gray] 

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

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

   446   | is_true _ = false*}

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

   447 

   546 

   448 text {*

   547   Since the complete traversal might sometimes be too costly and

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

   548   not necessary, there is also the function @{ML fastype_of} which 

   450   the function 

   549   returns a type.

   451 *}

   550 

   452 

   551   @{ML_response [display,gray] 

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

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

   454   | is_all _ = false*}

   553 

   455 

   554   However, efficiency is gained on the expense of skiping some tests. You 

   456 text {* 

   555   can see this in the following example

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

   556 

   458 

   557    @{ML_response [display,gray] 

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

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

   460 

   559 

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

   560   where no error is raised.

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

   561 

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

   562   Sometimes it is a bit inconvenient to construct a term with 

   464   for this function is

   563   complete typing annotations, especially in cases where the typing 

   465 *}

   564   information is redundant. A short-cut is to use the ``place-holder'' 

   466 

   565   type @{ML "dummyT"} and then let type-inference figure out the 

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

   566   complete type. An example is as follows:

   468   | is_all _ = false*}

   567 

   469 

   568   @{ML_response_fake [display,gray] 

   470 text {* 

   569 "let

   471   because now

   570   val term = 

   472 

   571    Const (@{const_name \"plus\"}, dummyT) $ @{term \"1::nat\"} $ Free (\"x\", dummyT)

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

   572 in   

   474 

   573   Syntax.check_term @{context} term

   475   matches correctly (the wildcard in the pattern matches any type).

   574 end"

   476 

   575   "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $

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

   576        Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}

   478   attempts to pick out a @{text "Nil"}-term:

   577 

   479 *}

   578   Instead of giving explicitly the type for the constant @{text "plus"} and the free 

   480 

   579   variable @{text "x"}, the type-inference will fill in the missing information.

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

   580 

   482   | is_nil _ = false *}

   483 

   484 text {* 

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

   486 

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

   488 

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

   490   subtle as you might expect. The function @{ML is_all} worked correctly,

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

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

   493 

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

   495 

   496   the name of the constant depends on the theory in which the term constructor

   497   @{text "Nil"} is defined (@{text "List"}) and also in which datatype 

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

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

   500   and @{term "(op *)"}:

   501 

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

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

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

   505 

   506   While you could use the complete name, for example 

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

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

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

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

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

   512   variable parts of the constant's name. Therefore a functions for 

   513   matching against constants that have a polymorphic type should 

   514   be written as follows.

   515 *}

   516 

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

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

   519   | is_nil_or_all _ = false *}

   520 

   521 text {*

   522   Note that you also frequently have to calculate what the

   523   ``base''  name of a given constant is. For this you can use 

   524   the function @{ML Sign.base_name}. For example:

   525   

   526   (FIXME is there an example for that statement?)

   527 

   528 

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

   530 

   531   (FIXME authentic syntax?)

   534   FIXME

   583   See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,

   584   checking and pretty-printing of terms are defined.

   544   in Isabelle is correct by construction. 

   594   in Isabelle is correct by construction. This follows the tradition of the LCF approach

   545 

   595   \cite{GordonMilnerWadsworth79}.

   546   (FIXME reference LCF-philosophy)

   596