isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:b6fca043a796
+:e8f11280c762
 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_from_ss} to obtain all names of theorems stored
-in the current simpset---this simpset can be referred to using the antiquotation
+in the current simpset. This simpset can be referred to using the antiquotation
 @{text "@{simpset}"}.
 @{ML_response_fake [display,gray]
 "get_thm_names_from_ss @{simpset}"
 "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
+Again, this way or referencing simpsets makes you independent from additions
+of lemmas to the simpset by the user that potentially cause loops.
 \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"}.
 ML{*val allI = thm "allI" *}
 text {*
 These bindings are difficult to maintain and also can be accidentally
-overwritten by the user. This often breakes Isabelle
+overwritten by the user. This often broke 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 chapter you will learn more about these antiquotations:
 they can simplify Isabelle programming since one can directly access all
 in @{ML_file "Pure/type.ML"}.
 \end{readmore}
 *}
-section {* Constructing Terms and Types Manually *}
+section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *}
 text {*
 While antiquotations are very convenient for constructing terms, they can
 only construct fixed terms (remember they are ``linked'' at compile-time).
 However, you often need to construct terms dynamically. For example, a
 *}
 ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
-text {* This can be equally written as: *}
+text {* This can be equally written with the combinator @{ML "-->"} as: *}
 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 text {*
 A handy function for manipulating terms is @{ML map_types}: it takes a
-function and applies it to every type in the term. You can, for example,
+function and applies it to every type in a term. You can, for example,
 change every @{typ nat} in a term into an @{typ int} using the function:
 *}
 ML{*fun nat_to_int t =
 (case t of
 text {*
 where the function @{ML "Thm.rule_attribute"} expects a function taking a
 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"}).
+an 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.
 *}
 fun my_thms_del thm ctxt =
 (my_thms := Thm.del_thm thm (!my_thms); ctxt)*}
 text {*
 These functions take a theorem and a context and, for what we are explaining
-here it is sufficient to just return the context unchanged. They change
+here it is sufficient that they just return the context unchanged. They change
 however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm}
 adds a theorem if it is not already included in the list, and @{ML
 Thm.del_thm} deletes one. Both functions use the predicate @{ML
 Thm.eq_thm_prop} which compares theorems according to their proved
 propositions (modulo alpha-equivalence).
-We can turn both functions into attributes using
+You can turn both functions into attributes using
 *}
 ML{*val my_add = Thm.declaration_attribute my_thms_add
 val my_del = Thm.declaration_attribute my_thms_del *}
 then you can see the lemma is added to the initially empty list.
 @{ML_response_fake [display,gray]
 "!my_thms" "[\"True\"]"}
-We can also add theorems using the command \isacommand{declare}
+You can also add theorems using the command \isacommand{declare}
 *}
 declare test[my_thms] trueI_2[my_thms add]
 text {*
 the list. Deletion from the list works as follows:
 *}
 declare test[my_thms del]
-text {* After this, the theorem list is:
+text {* After this, the theorem list is again:
 @{ML_response_fake [display,gray]
 "!my_thms"
 "[\"True\"]"}
 We used in this example two functions declared as @{ML Thm.declaration_attribute},
 but there can be any number of them. We just have to change the parser for reading
 the arguments accordingly.
-However, as said at the beginning using references for storing theorems is
+However, as said at the beginning of this example, using references for storing theorems is
 \emph{not} the received way of doing such things. The received way is to
 start a ``data slot'' in a context by using the functor @{text GenericDataFun}:
 *}
 ML {*structure Data = GenericDataFun
 val empty = []
 val extend = I
 fun merge _ = Thm.merge_thms) *}
 text {*
-To use this data slot, we only have to change the functions @{ML my_thms_add} and
+To use this data slot, you only have to change @{ML my_thms_add} and
 @{ML my_thms_del} to:
 *}
 ML{*val thm_add = Data.map o Thm.add_thm
 val thm_del = Data.map o Thm.del_thm*}
 an attribute @{text foo} (with the @{text add} and @{text del} options
 for adding and deleting theorems) and an internal ML interface to retrieve and
 modify the theorems.
 Furthermore, the facts are made available on the user level under the dynamic
-fact name @{text foo}. For example we can declare three lemmas to be of the kind
+fact name @{text foo}. For example you can declare three lemmas to be of the kind
 @{text foo} by:
 *}
 lemma rule1[foo]: "A" sorry
 lemma rule2[foo]: "B" sorry
 \isacommand{thm}~@{text "foo"}\\
 @{text "> ?C"}\\
 @{text "> ?B"}
 \end{isabelle}
-On the ML-level the rules marked with @{text "foo"} an be retrieved
+On the ML-level the rules marked with @{text "foo"} can be retrieved
 using the function @{ML FooRules.get}:
 @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
 \begin{readmore}
 For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also
 the recipe in Section~\ref{recipe:storingdata} about storing arbitrary
 data.
 \end{readmore}
-(FIXME What are:
+(FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)
-@{text "theory_attributes"}
-@{text "proof_attributes"})
 \begin{readmore}
 FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"}
 \end{readmore}

changeset 156	e8f11280c762
parent 153	c22b507e1407
child 157	76cdc8f562fc