--- a/CookBook/FirstSteps.thy Sun Feb 22 13:37:47 2009 +0000
+++ b/CookBook/FirstSteps.thy Mon Feb 23 00:27:27 2009 +0000
@@ -171,7 +171,7 @@
section {* Combinators\label{sec:combinators} *}
text {*
- For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
+ For beginners perhaps the most puzzling parts in the existing code of Isabelle are
the combinators. At first they seem to greatly obstruct the
comprehension of the code, but after getting familiar with them, they
actually ease the understanding and also the programming.
@@ -213,7 +213,7 @@
common when dealing with theories (for example by adding a definition, followed by
lemmas and so on). The reverse application allows you to read what happens in
a top-down manner. This kind of coding should also be familiar,
- if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using
+ if you used to Haskell's do-notation. Writing the function @{ML inc_by_five} using
the reverse application is much clearer than writing
*}
@@ -380,23 +380,28 @@
@{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
- and current simpsets:
+ and current simpsets. For this we use the function that extracts the
+ theorem names stored in the simpset.
+*}
- @{ML_response_fake [display,gray]
-"let
- val ({rules,...}, _) = MetaSimplifier.rep_ss @{simpset}
+ML{*fun get_thm_names simpset =
+let
+ val ({rules,...}, _) = MetaSimplifier.rep_ss simpset
in
map #name (Net.entries rules)
-end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
+end*}
- The code about simpsets extracts the theorem names stored in the
- simpset. You can get hold of the current simpset with the antiquotation
- @{text "@{simpset}"}. The function @{ML rep_ss in MetaSimplifier} returns a record
- containing all information about the simpset. The rules of a simpset are
- stored in a \emph{discrimination net} (a data structure for fast
- indexing). From this net you can extract the entries using the function @{ML
- Net.entries}.
+text {*
+ The function @{ML rep_ss in MetaSimplifier} returns a record containing all
+ information about the simpset. The rules of a simpset are stored in a
+ \emph{discrimination net} (a data structure for fast indexing). From this
+ net you can extract the entries using the function @{ML Net.entries}.
+ You can now use @{ML get_thm_names} to obtain all names of theorems of
+ the current simpset using the antiquotation @{text "@{simpset}"}.\footnote
+ {FIXME: you cannot cleanly match against lists with ommited parts}
+ @{ML_response_fake [display,gray]
+"get_thm_names @{simpset}" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
\begin{readmore}
The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
@@ -511,11 +516,11 @@
*}
ML{*fun make_imp P Q tau =
- let
- val x = Free ("x",tau)
- in
- Logic.all x (Logic.mk_implies (P $ x, Q $ x))
- end *}
+let
+ val x = Free ("x",tau)
+in
+ Logic.all x (Logic.mk_implies (P $ x, Q $ x))
+end *}
text {*
The reason is that you cannot pass the arguments @{term P}, @{term Q} and
@@ -603,7 +608,7 @@
There are a few subtle issues with constants. They usually crop up when
- pattern matching terms or constructing terms. While it is perfectly ok
+ pattern matching terms or types, or constructing them. While it is perfectly ok
to write the function @{text is_true} as follows
*}
@@ -637,10 +642,10 @@
@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
- matches correctly (the wildcard in the pattern matches any type).
+ matches correctly (the first wildcard in the pattern matches any type).
However there is still a problem: consider the similar function that
- attempts to pick out a @{text "Nil"}-term:
+ attempts to pick out @{text "Nil"}-terms:
*}
ML{*fun is_nil (Const ("Nil", _)) = true
@@ -658,11 +663,11 @@
@{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
- the name of the constant @{term "Nil"} depends on the theory in which the
+ 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
- @{text "(op *)"}:
+ \mbox{@{text "(op *)"}}:
@{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})"
"(Const (\"HOL.zero_class.zero\", \<dots>),
@@ -684,7 +689,7 @@
| is_nil_or_all _ = false *}
text {*
- Note that you occasional have to calculate what the ``base'' name of a given
+ Occasional you 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:
@@ -694,8 +699,6 @@
the smallest name that is still unique, whereas @{ML base_name in Sign} always
strips off all qualifiers.
- (FIXME authentic syntax on the ML-level)
-
\begin{readmore}
FIXME
\end{readmore}
@@ -706,15 +709,15 @@
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''.
+ You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
+ typ}es, 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.
@@ -765,7 +768,7 @@
"*** 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
+ not necessary, there is also the function @{ML fastype_of}, which
returns the type of a term.
@{ML_response [display,gray]
@@ -799,7 +802,6 @@
Instead of giving explicitly the type for the constant @{text "plus"} and the free
variable @{text "x"}, the type-inference filled 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.