isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:a21d7b300616
+:8db9195bb3e9
 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.
 The simplest combinator is @{ML I}, which is just the identity function defined as
 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 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
 *}
 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
 In a similar way you can use antiquotations to refer to proved theorems:
 @{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
+text {*
-simpset.  You can get hold of the current simpset with the antiquotation
+The function @{ML rep_ss in MetaSimplifier} returns a record containing all
-@{text "@{simpset}"}.  The function @{ML rep_ss in MetaSimplifier} returns a record
+information about the simpset. The rules of a simpset are stored in a
-containing all information about the simpset. The rules of a simpset are
+\emph{discrimination net} (a data structure for fast indexing). From this
-stored in a \emph{discrimination net} (a data structure for fast
+net you can extract the entries using the function @{ML Net.entries}.
-indexing). From this net you can extract the entries using the function @{ML
+You can now use @{ML get_thm_names} to obtain all names of theorems of
-Net.entries}.
+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"}
 and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented
 in @{ML_file "Pure/net.ML"}.
 written as:
 *}
 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 *}
 text {*
 The reason is that you cannot pass the arguments @{term P}, @{term Q} and
 @{term "tau"} into an antiquotation. For example the following does \emph{not} work.
 *}
 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
 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
 *}
 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 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
 | is_nil _ = false *}
 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>)"}
-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>),
 Const (\"HOL.times_class.times\", \<dots>))"}
 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
 | 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:
 @{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 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}
 *}
 section {* Type-Checking *}
 text {*
-You can freely construct and manipulate @{ML_type "term"}s, since they are just
+You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
-arbitrary unchecked trees. However, you eventually want to see if a
+typ}es, since they are just arbitrary unchecked trees. However, you
-term is well-formed, or type-checks, relative to a theory.
+eventually want to see if a term is well-formed, or type-checks, relative to
-Type-checking is done via the function @{ML cterm_of}, which converts
+a theory.  Type-checking is done via the function @{ML cterm_of}, which
-a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term.
+converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified}
-Unlike @{ML_type term}s, which are just trees, @{ML_type
+term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are
-"cterm"}s are abstract objects that are guaranteed to be
+abstract objects that are guaranteed to be type-correct, and they can only
-type-correct, and they can only be constructed via ``official
+be constructed via ``official interfaces''.
-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]
 "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 also the function @{ML fastype_of}, which
 returns the type of a term.
 @{ML_response [display,gray]
 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
 "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.
 \begin{readmore}
 See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
 checking and pretty-printing of terms are defined.
 \end{readmore}

changeset 131	8db9195bb3e9
parent 128	693711a0c702
child 132	2d9198bcb850