isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:4e2341f6599d
+:fb8f22dd8ad0
 text {*
 Another reason why the let-bindings in the code above are better to be
 avoided: it is more than easy to get the intermediate values wrong, not to
 mention the nightmares the maintenance of this code causes!
-A ``real world'' example for a function written in the waterfall fashion might
+In the context of Isabelle, a ``real world'' example for a function written in
-be the following:
+the waterfall fashion might be the following code:
 *}
 ML %linenosgray{*fun apply_fresh_args pred ctxt =
 pred |> fastype_of
 |> binder_types
 |> Variable.variant_frees ctxt [pred]
 |> map Free
 |> (curry list_comb) pred *}
 text {*
-The point of this function is to extract the argument types of the given
+The point of this code is to extract the argument types of the given
 predicate and then generate for each type a distinct variable; finally it
 applies the generated variables to the predicate. You can read this off from
 how the function is coded: in Line 2, the function @{ML fastype_of}
 calculates the type of the predicate; in Line 3, @{ML binder_types} produces
-the list of argument types; Line 4 pairs up each type with the string/name
+the list of argument types; Line 4 pairs up each type with the string (or name)
 @{text "z"}; the function @{ML variant_frees in Variable} generates for each
 @{text "z"} a unique name avoiding @{text pred}; the list of name-type pairs
 is turned into a list of variable terms in Line 6, which in the last line
 are applied by the function @{ML list_comb} to the predicate. We have to use
 the function @{ML curry}, because @{ML list_comb} expects the predicate and
 in
 cterm_of @{theory}
 (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
 end" "0 + 0"}
-In Isabelle also types need can be certified. For example, you obtain
+In Isabelle not just types need to be certified, but also types. For example,
-the certified type for the Isablle type @{typ "nat \<Rightarrow> bool"} on the ML-level
+you obtain the certified type for the Isablle type @{typ "nat \<Rightarrow> bool"} on
-as follows:
+the ML-level as follows:
 @{ML_response_fake [display,gray]
 "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
 "nat \<Rightarrow> bool"}
 \begin{exercise}
 Check that the function defined in Exercise~\ref{fun:revsum} returns a
 result that type-checks.
 \end{exercise}
-Remember that in Isabelle a term contains enough typing information
+Remember Isabelle foolows the Church-style typing for terms, i.e.~a term contains
-(constants, free variables and abstractions all have typing
+enough typing information (constants, free variables and abstractions all have typing
 information) so that it is always clear what the type of a term is.
 Given a well-typed term, the function @{ML type_of} returns the
 type of a term. Consider for example:
 @{ML_response [display,gray]
 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.
 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.
+using the function @{ML Attrib.setup} as follows.
 *}
-setup %gray {* Attrib.add_attributes
+setup %gray {* Attrib.setup @{binding "my_sym"}
-[("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *}
+(Scan.succeed my_symmetric) "applying the sym rule"*}
 text {*
 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
+we use the parser @{ML Scan.succeed}. 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
 text {*
 and set up the attributes as follows
 *}
-setup %gray {* Attrib.add_attributes
+setup %gray {* Attrib.setup @{binding "my_thms"}
-[("my_thms", Attrib.add_del_args my_add my_del,
+(Attrib.add_del my_add my_del) "maintaining a list of my_thms" *}
-"maintaining a list of my_thms")] *}
 text {*
 Now if you prove the lemma attaching the attribute @{text "[my_thms]"}
 *}
 FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"}
 \end{readmore}
 *}
+section {* Setups (TBD) *}
+text {*
+In the previous section we used \isacommand{setup} in order to make
+a theorem attribute known to Isabelle. What happens behind the scenes
+is that \isacommand{setup} expects a functions from @{ML_type theory}
+to @{ML_type theory}: the input theory is the current theory and the
+output the theory where the theory attribute has been stored.
+This is a fundamental principle in Isabelle. A similar situation occurs
+for example with declaring constants. The function that declares a
+constant on the ML-level is @{ML Sign.add_consts_i}. Recall that ML-code
+needs to be \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.
+If you write
+*}
+ML{*Sign.add_consts_i [(Binding.name "BAR", @{typ "nat"}, NoSyn)] @{theory} *}
+text {*
+for declaring the constant @{text "BAR"} with type @{typ nat} and
+run the code, then you indeed obtain a theory as result. But if you
+query the constant with \isacommand{term}
+\begin{isabelle}
+\isacommand{term}~@{text [quotes] "BAR"}\\
+@{text "> \"BAR\" :: \"'a\""}
+\end{isabelle}
+you do not obtain a constant of type @{typ nat}, but a free variable (printed in
+blue) of polymorphic type. The problem is that the ML-expression above did
+not register the declaration with the current theory. This is what the command
+\isacommand{setup} is for. The constant is properly declared with
+*}
+setup %gray {* Sign.add_consts_i [(Binding.name "BAR", @{typ "nat"}, NoSyn)] *}
+text {*
+Now
+\begin{isabelle}
+\isacommand{term}~@{text [quotes] "BAR"}\\
+@{text "> \"BAR\" :: \"nat\""}
+\end{isabelle}
+returns a (black) constant with the type @{typ nat}.
+A similar command is \isacommand{local\_setup}, which expects a function
+of type @{ML_type "local_theory -> local_theory"}. Later on we will also
+use the commands \isacommand{method\_setup} for installing methods in the
+current theory and \isacommand{simproc\_setup} for adding new simprocs to
+the current simpset.
+*}
 section {* Theories, Contexts and Local Theories (TBD) *}
 text {*
-(FIXME: expand)
-(FIXME: explain \isacommand{setup})
 There are theories, proof contexts and local theories (in this order, if you
 want to order them).
 In contrast to an ordinary theory, which simply consists of a type
 signature, as well as tables for constants, axioms and theorems, a local
 theory also contains additional context information, such as locally fixed
 variables and local assumptions that may be used by the package. The type
 @{ML_type local_theory} is identical to the type of \emph{proof contexts}
 @{ML_type "Proof.context"}, although not every proof context constitutes a
 valid local theory.
+*}
-*}
 section {* Storing Theorems\label{sec:storing} (TBD) *}
 text {* @{ML PureThy.add_thms_dynamic} *}

changeset 178	fb8f22dd8ad0
parent 177	4e2341f6599d
child 183	8bb4eaa2ec92