--- a/CookBook/FirstSteps.thy Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/FirstSteps.thy Wed Feb 18 17:17:37 2009 +0000
@@ -381,62 +381,7 @@
"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
$ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
-*}
-section {* Type-Checking *}
-
-text {*
-
- You can freely construct and manipulate @{ML_type "term"}s, since they are just
- arbitrary unchecked trees. However, you eventually want to see if a
- term is well-formed, or type-checks, relative to a theory.
- Type-checking is done via the function @{ML cterm_of}, which converts
- a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
- Unlike @{ML_type term}s, which are just trees, @{ML_type
- "cterm"}s are abstract objects that are guaranteed to be
- type-correct, and they can only be constructed via ``official
- interfaces''.
-
- Type-checking is always relative to a theory context. For now we use
- the @{ML "@{theory}"} antiquotation to get hold of the current theory.
- For example you can write:
-
- @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
-
- This can also be written with an antiquotation:
-
- @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
-
- Attempting to obtain the certified term for
-
- @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
-
- yields an error (since the term is not typable). A slightly more elaborate
- example that type-checks is:
-
-@{ML_response_fake [display,gray]
-"let
- val natT = @{typ \"nat\"}
- val zero = @{term \"0::nat\"}
-in
- cterm_of @{theory}
- (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
-end" "0 + 0"}
-
- \begin{exercise}
- Check that the function defined in Exercise~\ref{fun:revsum} returns a
- result that type-checks.
- \end{exercise}
-
- (FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT})
-
- (FIXME: say something about constants and variables having types as
- arguments and how they can be constructed with fast-type and dummT)
-*}
-
-section {* Constants *}
-
-text {*
There are a few subtle issues with constants. They usually crop up when
pattern matching terms or constructing terms. While it is perfectly ok
to write the function @{text is_true} as follows
@@ -497,7 +442,7 @@
@{text "Nil"} 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 @{term "(op *)"}:
+ and @{text "(op *)"}:
@{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})"
"(Const (\"HOL.zero_class.zero\", \<dots>),
@@ -519,16 +464,17 @@
| is_nil_or_all _ = false *}
text {*
- Note that you also frequently have to calculate what the
- ``base'' name of a given constant is. For this you can use
- the function @{ML Sign.base_name}. For example:
-
- (FIXME is there an example for that statement?)
+ Note that you occasional have to calculate what the ``base'' name of a given
+ constant is. For this you can use the function @{ML Sign.extern_const} or
+ @{ML Sign.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 which is still unique, while @{ML base_name in Sign} always
+ strips off all qualifiers.
- @{ML_response [display,gray] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
-
- (FIXME authentic syntax?)
+ (FIXME authentic syntax on the ML-level)
\begin{readmore}
FIXME
@@ -536,14 +482,118 @@
*}
+section {* Type-Checking *}
+
+text {*
+
+ You can freely construct and manipulate @{ML_type "term"}s, since they are just
+ arbitrary unchecked trees. However, you eventually want to see if a
+ term is well-formed, or type-checks, relative to a theory.
+ Type-checking is done via the function @{ML cterm_of}, which converts
+ a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
+ Unlike @{ML_type term}s, which are just trees, @{ML_type
+ "cterm"}s are abstract objects that are guaranteed to be
+ type-correct, and they can only be constructed via ``official
+ interfaces''.
+
+ Type-checking is always relative to a theory context. For now we use
+ the @{ML "@{theory}"} antiquotation to get hold of the current theory.
+ For example you can write:
+
+ @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
+
+ This can also be written with an antiquotation:
+
+ @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
+
+ Attempting to obtain the certified term for
+
+ @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
+
+ yields an error (since the term is not typable). A slightly more elaborate
+ example that type-checks is:
+
+@{ML_response_fake [display,gray]
+"let
+ val natT = @{typ \"nat\"}
+ val zero = @{term \"0::nat\"}
+in
+ cterm_of @{theory}
+ (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
+end" "0 + 0"}
+
+ \begin{exercise}
+ Check that the function defined in Exercise~\ref{fun:revsum} returns a
+ result that type-checks.
+ \end{exercise}
+
+ Remember that in Isabelle a term contains enough typing information
+ (constants, free variables and abstractions all have typing
+ information) so that it is always clear what the type of a term is.
+ Given a well-typed term, the function @{ML type_of} returns the
+ type of a term. Consider for example:
+
+ @{ML_response [display,gray]
+ "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
+
+ To calculate the type, this function traverses the whole term and will
+ detect any inconsistency. For examle changing the type of the variable
+ from @{typ "nat"} to @{typ "int"} will result in the error message:
+
+ @{ML_response_fake [display,gray]
+ "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})"
+ "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
+
+ Since the complete traversal might sometimes be too costly and
+ not necessary, there is also the function @{ML fastype_of} which
+ returns a type.
+
+ @{ML_response [display,gray]
+ "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
+
+ However, efficiency is gained on the expense of skiping some tests. You
+ can see this in the following example
+
+ @{ML_response [display,gray]
+ "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}
+
+ where no error is raised.
+
+ Sometimes it is a bit inconvenient to construct a term with
+ complete typing annotations, especially in cases where the typing
+ information is redundant. A short-cut is to use the ``place-holder''
+ type @{ML "dummyT"} and then let type-inference figure out the
+ complete type. An example is as follows:
+
+ @{ML_response_fake [display,gray]
+"let
+ val term =
+ Const (@{const_name \"plus\"}, dummyT) $ @{term \"1::nat\"} $ Free (\"x\", dummyT)
+in
+ Syntax.check_term @{context} term
+end"
+ "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
+ Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
+
+ Instead of giving explicitly the type for the constant @{text "plus"} and the free
+ variable @{text "x"}, the type-inference will fill in the missing information.
+
+
+ \begin{readmore}
+ See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
+ checking and pretty-printing of terms are defined.
+ \end{readmore}
+*}
+
+
section {* Theorems *}
text {*
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
that can only be build by going through interfaces. As a consequence, every proof
- in Isabelle is correct by construction.
+ in Isabelle is correct by construction. This follows the tradition of the LCF approach
+ \cite{GordonMilnerWadsworth79}.
- (FIXME reference LCF-philosophy)
To see theorems in ``action'', let us give a proof on the ML-level for the following
statement: