--- a/CookBook/FirstSteps.thy Wed Feb 25 22:13:41 2009 +0000
+++ b/CookBook/FirstSteps.thy Thu Feb 26 12:16:24 2009 +0000
@@ -141,9 +141,9 @@
Syntax.string_of_term ctxt (term_of t)*}
text {*
- The function @{ML term_of} extracts the @{ML_type term} from a @{ML_type cterm}.
- If there are more than one @{ML_type cterm}s to be printed, you can use the
- function @{ML commas} to separate them.
+ In this example the function @{ML term_of} extracts the @{ML_type term} from
+ a @{ML_type cterm}. If there are more than one @{ML_type cterm}s to be
+ printed, you can use the function @{ML commas} to separate them.
*}
ML{*fun str_of_cterms ctxt ts =
@@ -214,7 +214,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 to Haskell's do-notation. Writing the function @{ML inc_by_five} using
+ if you have been exposed to Haskell's do-notation. Writing the function @{ML inc_by_five} using
the reverse application is much clearer than writing
*}
@@ -389,11 +389,11 @@
(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}
- You can also refer to the current simpset. To illustrate this we use the
+ You can also refer to the current simpset. To illustrate this we implement the
function that extracts the theorem names stored in a simpset.
*}
-ML{*fun get_thm_names simpset =
+ML{*fun get_thm_names_from_ss simpset =
let
val ({rules,...}, _) = MetaSimplifier.rep_ss simpset
in
@@ -405,13 +405,13 @@
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 stored
+ You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored
in the current simpset---this simpset can be referred to using the antiquotation
- @{text "@{simpset}"}.\footnote
- {FIXME: you cannot cleanly match against lists with ommited parts}
+ @{text "@{simpset}"}.
@{ML_response_fake [display,gray]
-"get_thm_names @{simpset}" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
+ "get_thm_names_from_ss @{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"}
@@ -431,7 +431,7 @@
packages. Antiquotations solve this problem, since they are ``linked''
statically at compile-time. However, this static linkage also limits their
usefulness in cases where data needs to be build up dynamically. In the
- course of this introduction, you will learn more about these antiquotations:
+ course of this chapter you will learn more about these antiquotations:
they can simplify Isabelle programming since one can directly access all
kinds of logical elements from th ML-level.
@@ -446,7 +446,7 @@
@{ML_response [display,gray]
"@{term \"(a::nat) + b = c\"}"
"Const (\"op =\", \<dots>) $
- (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
+ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
representation of this term. This internal representation corresponds to the
@@ -456,7 +456,7 @@
variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
binds the corresponding variable. However, in Isabelle the names of bound variables are
- kept at abstractions for printing purposes, and so should be treated only as comments.
+ kept at abstractions for printing purposes, and so should be treated only as ``comments''.
Application in Isabelle is realised with the term-constructor @{ML $}.
\begin{readmore}
@@ -492,7 +492,7 @@
@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})"
"(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
- Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
+ Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
where a coercion is inserted in the second component and
@@ -617,7 +617,7 @@
\end{exercise}
There are a few subtle issues with constants. They usually crop up when
- pattern matching terms or types, or constructing them. While it is perfectly ok
+ pattern matching terms or types, or when constructing them. While it is perfectly ok
to write the function @{text is_true} as follows
*}
@@ -651,7 +651,8 @@
@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
- matches correctly (the first wildcard in the pattern matches any type).
+ matches correctly (the first wildcard in the pattern matches any type and the
+ second any term).
However there is still a problem: consider the similar function that
attempts to pick out @{text "Nil"}-terms:
@@ -666,7 +667,7 @@
@{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
The problem is that on the ML-level the name of a constant is more
- subtle as you might expect. The function @{ML is_all} worked correctly,
+ subtle than you might expect. The function @{ML is_all} worked correctly,
because @{term "All"} is such a fundamental constant, which can be referenced
by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
@@ -732,7 +733,7 @@
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"}
+ @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" "a + b = c"}
This can also be written with an antiquotation:
@@ -770,15 +771,15 @@
To calculate the type, this function traverses the whole term and will
detect any typing inconsistency. For examle changing the type of the variable
- from @{typ "nat"} to @{typ "int"} will result in the error message:
+ @{term "x"} 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 the type of a term.
+ not necessary, there is the function @{ML fastype_of}, which
+ also returns the type of a term.
@{ML_response [display,gray]
"fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
@@ -789,7 +790,7 @@
@{ML_response [display,gray]
"fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}
- where no error is raised.
+ where no error is detected.
Sometimes it is a bit inconvenient to construct a term with
complete typing annotations, especially in cases where the typing
@@ -809,7 +810,7 @@
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 filled in the missing information.
+ variable @{text "x"}, the type-inference filles in the missing information.
\begin{readmore}
See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
@@ -842,7 +843,6 @@
@{ML_response_fake [display,gray]
"let
-
val assm1 = @{cprop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
val assm2 = @{cprop \"(P::nat\<Rightarrow>bool) t\"}
@@ -916,9 +916,9 @@
text {*
where the function @{ML "Thm.rule_attribute"} expects a function taking a
- context (we ignore it in the code above) and a theorem (@{text thm}) and
- returns another theorem (namely @{text thm} resolved with the rule
- @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns
+ context (which we ignore in the code above) and a theorem (@{text thm}), and
+ returns another theorem (namely @{text thm} resolved with the lemma
+ @{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns
an attribute (of type @{ML_type "attribute"}).
Before we can use the attribute, we need to set it up. This can be done
@@ -931,10 +931,11 @@
*}
text {*
- The attribute does not expect any further arguments (like @{text "[OF \<dots>]"} that
- can take a list of theorems as argument). Therefore we use the function
- @{ML Attrib.no_args}. Later on we will also consider attributes taking further
- arguments. An example for the attribute @{text "[my_sym]"} is the proof
+ The attribute does not expect any further arguments (unlike @{text "[OF
+ \<dots>]"}, for example, which can take a list of theorems as argument). Therefore
+ we use the function @{ML Attrib.no_args}. Later on we will also consider
+ attributes taking further arguments. An example for the attribute @{text
+ "[my_sym]"} is the proof
*}
lemma test[my_sym]: "2 = Suc (Suc 0)" by simp