isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:84d1392186d3
+:253ea99c1441
 ML{*fun str_of_cterm ctxt t =
 Syntax.string_of_term ctxt (term_of t)*}
 text {*
-The function @{ML term_of} extracts the @{ML_type term} from a @{ML_type cterm}.
+In this example the function @{ML term_of} extracts the @{ML_type term} from
-If there are more than one @{ML_type cterm}s to be printed, you can use the
+a @{ML_type cterm}.  If there are more than one @{ML_type cterm}s to be
-function @{ML commas} to separate them.
+printed, you can use the function @{ML commas} to separate them.
 *}
 ML{*fun str_of_cterms ctxt ts =
 commas (map (str_of_cterm ctxt) ts)*}
 the first component of the pair (Line 4) and finally incrementing the first
 component by 4 (Line 5). This kind of cascading manipulations of values is quite
 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
 *}
 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
 @{ML_response_fake [display,gray] "@{thms conj_ac}"
 "(?P \<and> ?Q) = (?Q \<and> ?P)
 (?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
 map #name (Net.entries rules)
 end*}
 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 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
+@{text "@{simpset}"}.
-{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>]"}
+"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"}
 and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented
 in @{ML_file "Pure/net.ML"}.
 These bindings are difficult to maintain and also can be accidentally
 overwritten by the user. This often breakes Isabelle
 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.
 *}
 \mbox{@{text "@{term \<dots>}"}}. For example:
 @{ML_response [display,gray]
 "@{term \"(a::nat) + b = c\"}"
 "Const (\"op =\", \<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
 datatype @{ML_type "term"}.
 The internal representation of terms uses the usual de Bruijn index mechanism where bound
 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}
 Terms are described in detail in \isccite{sec:terms}. Their
 definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
 inserting the invisible @{text "Trueprop"}-coercions whenever necessary.
 Consider for example the pairs
 @{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>)))"}
 where a coercion is inserted in the second component and
 @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
 "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the
 number representing their sum.
 \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
 *}
 ML{*fun is_true @{term True} = true
 | is_true _ = false*}
 text {*
 because now
 @{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:
 *}
 Unfortunately, also this function does \emph{not} work as expected, since
 @{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
 @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
 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"}
+@{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"(a::nat) + 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"}
 @{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 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
+not necessary, there is the function @{ML fastype_of}, which
-returns the type of a term.
+also returns the type of a term.
 @{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.
+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
 information is redundant. A short-cut is to use the ``place-holder''
 type @{ML "dummyT"} and then let type-inference figure out the
 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 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,
 checking and pretty-printing of terms are defined.
 \end{readmore}
 The corresponding ML-code is as follows:\footnote{Note that @{text "|>"} is reverse
 application. See Section~\ref{sec:combinators}.}
 @{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\"}
 val Pt_implies_Qt =
 assume assm1
 ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
 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
+context (which we ignore in the code above) and a theorem (@{text thm}), and
-returns another theorem (namely @{text thm} resolved with the rule
+returns another theorem (namely @{text thm} resolved with the lemma
-@{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns
+@{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
 using the function @{ML Attrib.add_attributes} as follows.
 *}
 Attrib.add_attributes
 [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")]
 *}
 text {*
-The attribute does not expect any further arguments (like @{text "[OF \<dots>]"} that
+The attribute does not expect any further arguments (unlike @{text "[OF
-can take a list of theorems as argument). Therefore we use the function
+\<dots>]"}, for example, which can take a list of theorems as argument). Therefore
-@{ML Attrib.no_args}. Later on we will also consider attributes taking further
+we use the function @{ML Attrib.no_args}. Later on we will also consider
-arguments. An example for the attribute @{text "[my_sym]"} is the proof
+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
 text {*

changeset 149	253ea99c1441
parent 138	e4d8dfb7e34a
child 151	7e0bf13bf743