isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:ffd93dcc269d
+:8cd51a25a7ca
 text {*
 The easiest way to get the string of a theorem is to transform it
 into a @{ML_type cterm} using the function @{ML crep_thm}.
 *}
-ML{*fun str_of_thm_raw ctxt thm =
+ML{*fun str_of_thm ctxt thm =
 str_of_cterm ctxt (#prop (crep_thm thm))*}
 text {*
 Theorems also include schematic variables, such as @{text "?P"},
 @{text "?Q"} and so on.
 @{ML_response_fake [display, gray]
-"warning (str_of_thm_raw @{context} @{thm conjI})"
+"warning (str_of_thm @{context} @{thm conjI})"
 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 In order to improve the readability of theorems we convert
 these schematic variables into free variables using the
 function @{ML Variable.import_thms}.
 val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
 in
 thm'
 end
-fun str_of_thm ctxt thm =
+fun str_of_thm_no_vars ctxt thm =
 str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}
 text {*
-Theorem @{thm [source] conjI} looks now as follows
+Theorem @{thm [source] conjI} looks now as follows:
 @{ML_response_fake [display, gray]
-"warning (str_of_thm_raw @{context} @{thm conjI})"
+"warning (str_of_thm_no_vars @{context} @{thm conjI})"
-"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
+"\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
 Again the function @{ML commas} helps with printing more than one theorem.
 *}
 ML{*fun str_of_thms ctxt thms =
 commas (map (str_of_thm ctxt) thms)
-fun str_of_thms_raw ctxt thms =
+fun str_of_thms_no_vars ctxt thms =
-commas (map (str_of_thm_raw ctxt) thms)*}
+commas (map (str_of_thm_no_vars ctxt) thms) *}
 section {* Combinators\label{sec:combinators} *}
 text {*
 For beginners perhaps the most puzzling parts in the existing code of Isabelle are
 |> Variable.variant_frees ctxt [f]
 |> map Free
 |> (curry list_comb) f *}
 text {*
-This code extracts the argument types of a given function and then generates
+This code extracts the argument types of a given function @{text "f"} and then generates
 for each argument type a distinct variable; finally it applies the generated
-variables to the function. For example
+variables to the function. For example:
 @{ML_response_fake [display,gray]
 "apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context}
 |> Syntax.string_of_term @{context}
 |> warning"
 types (in the case above the list @{text "[nat, int, unit]"}); Line 4
 pairs up each type with the string  @{text "z"}; the
 function @{ML variant_frees in Variable} generates for each @{text "z"} a
 unique name avoiding the given @{text f}; the list of name-type pairs is turned
 into a list of variable terms in Line 6, which in the last line is applied
-by the function @{ML list_comb} to the function. We have to use the
+by the function @{ML list_comb} to the function. In this last step we have to
-function @{ML curry}, because @{ML list_comb} expects the function and the
+use the function @{ML curry}, because @{ML list_comb} expects the function and the
 variables list as a pair.
 The combinator @{ML "#>"} is the reverse function composition. It can be
 used to define the following function
 *}
 \begin{isabelle}
 \isacommand{thm}~@{text "TrueConj_def"}\\
 @{text "> "}@{thm TrueConj_def}
 \end{isabelle}
-(FIXME give a better example why bindings are important)
+(FIXME give a better example why bindings are important; maybe
+give a pointer to \isacommand{local\_setup})
 While antiquotations have many applications, they were originally introduced in order
 to avoid explicit bindings for theorems such as:
 *}
 @{ML_response_fake_both [display,gray]
 "@{term \"(x::nat) x\"}"
 "Type unification failed \<dots>"}
-raises a typing error, while it perfectly ok to construct
+raises a typing error, while it perfectly ok to construct the term
 @{ML [display,gray] "Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})"}
 with the raw ML-constructors.
 Sometimes the internal representation of terms can be surprisingly different
 *}
 ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
 text {*
-To see this apply @{text "@{term S}"} and @{text "@{term T}"}
+To see this, apply @{text "@{term S}"} and @{text "@{term T}"}
 to both functions. With @{ML make_imp} you obtain the intended term involving
 the given arguments
 @{ML_response [display,gray] "make_imp @{term S} @{term T}"
 "Const \<dots> $
 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 There are a number of handy functions that are frequently used for
 constructing terms. One is the function @{ML list_comb}, which takes
-a term and a list of terms as argument, and produces as output the term
+a term and a list of terms as arguments, and produces as output the term
 list applied to the term. For example
 @{ML_response_fake [display,gray]
 "list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])"
 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
 @{ML_response_fake [display,gray]
 "lambda @{term \"x::nat\"} @{term \"(P::nat\<Rightarrow>bool) x\"}"
 "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
-In the example @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound  0"}),
+In the example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound  0"}),
 and an abstraction. It also records the type of the abstracted
 variable and for printing purposes also its name.  Note that because of the
 typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
 is of the same type as the abstracted variable. If it is of different type,
 as in
 This is a fundamental principle
 of Church-style typing, where variables with the same name still differ, if they
 have different type.
 There is also the function @{ML subst_free} with which terms can
-be replaced by other terms. For example below we replace in  @{term "f 0 x"}
+be replaced by other terms. For example below, we will replace in
-the subterm @{term "f 0"} by @{term y} and @{term x} by @{term True}.
+@{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0 x"}
+the subterm @{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0"} by @{term y}, and @{term x} by @{term True}.
 @{ML_response_fake [display,gray]
 "subst_free [(@{term \"(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0\"}, @{term \"y::nat\<Rightarrow>nat\"}),
 (@{term \"x::nat\"}, @{term \"True\"})]
 @{term \"((f::nat\<Rightarrow>nat\<Rightarrow>nat) 0) x\"}"
 For the functions @{text "assume"}, @{text "forall_elim"} etc
 see \isccite{sec:thms}. The basic functions for theorems are defined in
 @{ML_file "Pure/thm.ML"}.
 \end{readmore}
-(FIXME: how to add case-names to goal states - maybe in the next section)
+(FIXME: handy functions working on theorems; how to add case-names to goal
+states - maybe in the next section)
 *}
 section {* Theorem Attributes *}
 text {*
 \isacommand{thm}~@{text "test[my_sym]"}\\
 @{text "> "}~@{thm test[my_sym]}
 \end{isabelle}
 As an example of a slightly more complicated theorem attribute, we implement
-our version of @{text "[THEN \<dots>]"}. This attribute takes a list of theorems
+our version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
-as argument and resolves the proved theorem with this list (one theorem
+as argument and resolve the proved theorem with this list (one theorem
-after another). The code for this attribute is:
+after another). The code for this attribute is
 *}
 ML{*fun MY_THEN thms =
 Thm.rule_attribute (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*}
 text {*
-where @{ML swap} swaps the components of a pair. The setup of this theorem
+where @{ML swap} swaps the components of a pair (@{ML RS} is explained
+later on in Section~\ref{sec:simpletacs}). The setup of this theorem
 attribute uses the parser @{ML Attrib.thms}, which parses a list of
 theorems.
 *}
 attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *}
 \begin{isabelle}
 \isacommand{thm}~@{text "test[MY_THEN sym eq_reflection]"}\\
 @{text "> "}~@{thm test[MY_THEN sym eq_reflection]}
 \end{isabelle}
-Of course, it is also possible to combine different theorem attributes, as in:
+It is also possible to combine different theorem attributes, as in:
 \begin{isabelle}
 \isacommand{thm}~@{text "test[my_sym, MY_THEN eq_reflection]"}\\
 @{text "> "}~@{thm test[my_sym, MY_THEN eq_reflection]}
 \end{isabelle}
 However, here also a weakness of the concept
-of theorem attributes show through: since theorem attributes can be an
+of theorem attributes shows through: since theorem attributes can be
 arbitrary functions, they do not in general commute. If you try
 \begin{isabelle}
 \isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\
 @{text "> "}~@{text "exception THM 1 raised: RSN: no unifiers"}
 you get an exception indicating that the theorem @{thm [source] sym}
 does not resolve with meta-equations.
 The purpose of @{ML Thm.rule_attribute} is to directly manipulate theorems.
-Another usage of attributes is to add and delete theorems from stored data.
+Another usage of theorem attributes is to add and delete theorems from stored data.
-For example the attribute @{text "[simp]"} adds or deletes a theorem from the
+For example the theorem attribute @{text "[simp]"} adds or deletes a theorem from the
 current simpset. For these applications, you can use @{ML Thm.declaration_attribute}.
 To illustrate this function, let us introduce a reference containing a list
 of theorems.
 *}
 text {*
 These functions take a theorem and a context and, for what we are explaining
 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.del_thm} deletes one (both functions use the predicate @{ML
-Thm.eq_thm_prop} which compares theorems according to their proved
+Thm.eq_thm_prop}, which compares theorems according to their proved
-propositions (modulo alpha-equivalence).
+propositions modulo alpha-equivalence).
-You can turn both functions into attributes using
+You can turn functions @{ML my_thms_add} and @{ML my_thms_del} into
+attributes with the code
 *}
 ML{*val my_add = Thm.declaration_attribute my_thms_add
 val my_del = Thm.declaration_attribute my_thms_del *}
 attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *}
 "maintaining a list of my_thms"
 text {*
-Now if you prove the lemma attaching the attribute @{text "[my_thms]"}
+The parser @{ML Attrib.add_del} is a predefined parser for
+adding and deleting lemmas. Now if you prove the next lemma
+and attach the attribute
+@{text "[my_thms]"}
 *}
 lemma trueI_2[my_thms]: "True" by simp
 text {*
-then you can see the lemma is added to the initially empty list.
+then you can see it is added to the initially empty list.
 @{ML_response_fake [display,gray]
 "!my_thms" "[\"True\"]"}
 You can also add theorems using the command \isacommand{declare}.
 declare test[my_thms] trueI_2[my_thms add]
 text {*
 The @{text "add"} is the default operation and does not need
-to be given. This declaration will cause the theorem list to be
+to be explicitly given. These two declarations will cause the
-updated as follows.
+theorem list to be updated as:
 @{ML_response_fake [display,gray]
 "!my_thms"
 "[\"True\", \"Suc (Suc 0) = 2\"]"}
 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 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}:
+start a ``data slot'', below called @{text MyThmsData}, by using the functor
+@{text GenericDataFun}:
 *}
 ML {*structure MyThmsData = GenericDataFun
 (type T = thm list
 val empty = []
 ML{*val thm_add = MyThmsData.map o Thm.add_thm
 val thm_del = MyThmsData.map o Thm.del_thm*}
 text {*
-where @{ML MyThmsData.map} updates the data appropriately in the context. The
+where @{ML MyThmsData.map} updates the data appropriately. The
-theorem addtributes are
+corresponding theorem addtributes are
 *}
 ML{*val add = Thm.declaration_attribute thm_add
 val del = Thm.declaration_attribute thm_del *}
 text {*
-ad the setup is as follows
+and the setup is as follows
 *}
 attribute_setup %gray my_thms2 = {* Attrib.add_del add del *}
 "properly maintaining a list of my_thms"
-ML {* MyThmsData.get (Context.Proof @{context}) *}
+text {*
+Initially, the data slot is empty
-lemma [my_thms2]: "2 = Suc (Suc 0)" by simp
+@{ML_response_fake [display,gray]
-ML {* MyThmsData.get (Context.Proof @{context}) *}
+"MyThmsData.get (Context.Proof @{context})"
+"[]"}
-ML {* !my_thms *}
+but if you prove
-text {*
+*}
-(FIXME: explain problem with backtracking)
+lemma three[my_thms2]: "3 = Suc (Suc (Suc 0))" by simp
-Since storing
-theorems in a special list is such a common task, there is the functor @{text NamedThmsFun},
+text {*
-which does most of the work for you. To obtain such a named theorem lists, you just
+the lemma is now included
-declare
+@{ML_response_fake [display,gray]
+"MyThmsData.get (Context.Proof @{context})"
+"[\"3 = Suc (Suc (Suc 0))\"]"}
+With @{text my_thms2} you can also nicely see why it is important to
+store data in a ``data slot'' and \emph{not} in a reference. Backtrack
+to the point just before the lemma @{thm [source] three} is proved and
+check the the content of @{ML_struct "MyThmsData"}: it is now again
+empty. The addition has been properly retracted. Now consider the proof:
+*}
+lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp
+text {*
+Checking the content of @{ML my_thms} gives
+@{ML_response_fake [display,gray]
+"!my_thms"
+"[\"4 = Suc (Suc (Suc (Suc 0)))\", \"True\"]"}
+as expected, but if we backtrack before the lemma @{thm [source] four}, the
+content of @{ML my_thms} is unchanged. The backtracking mechanism
+of Isabelle is completely oblivious about what to do with references!
+Since storing theorems in a special list is such a common task, there is the
+functor @{text NamedThmsFun}, which does most of the work for you. To obtain
+such a named theorem lists, you just declare
 *}
 ML{*structure FooRules = NamedThmsFun
 (val name = "foo"
-val description = "Rules for foo"); *}
+val description = "Rules for foo") *}
 text {*
 and set up the @{ML_struct FooRules} with the command
 *}

changeset 194	8cd51a25a7ca
parent 193	ffd93dcc269d
child 204	3857d987576a