isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:096776f180fc
+:d3cd633e8240
 (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling})
 *}
 (*
-ML {* set Toplevel.debug *}
+ML {* reset Toplevel.debug *}
-ML {*
+ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *}
-fun dodgy_fun () = (raise (ERROR "bar"); 1)
-*}
+ML {* fun innocent () = dodgy_fun () *}
+ML {* exception_trace (fn () => cterm_of @{theory} (Bound 0)) *}
-ML {* fun f1 () = dodgy_fun () *}
+ML {* exception_trace (fn () => innocent ()) *}
-ML {* f1 () *}
+ML {* Toplevel.program (fn () => cterm_of @{theory} (Bound 0)) *}
+ML {* Toplevel.program (fn () => innocent ()) *}
 *)
 text {*
 Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm}
 or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them,
 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} is now printed as follows:
 @{ML_response_fake [display, gray]
 "warning (str_of_thm_no_vars @{context} @{thm conjI})"
 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
 local_setup %gray {*
 snd o LocalTheory.define Thm.internalK
 ((@{binding "TrueConj"}, NoSyn),
 (Attrib.empty_binding, @{term "True \<and> True"})) *}
-<<<<<<< local
 text {*
 Now querying the definition you obtain:
 \begin{isabelle}
 \isacommand{thm}~@{text "TrueConj_def"}\\
 @{ML_response [display,gray]
 "@{term \"(a::nat) + b = c\"}"
 "Const (\"op =\", \<dots>) $
 (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
-will show the term @{term "(a::nat) + b = c"}, but printed using an internal
+will show the term @{term "(a::nat) + b = c"}, but printed using the internal
 representation corresponding to the data type @{ML_type "term"}.
 This internal representation 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
 you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on
 the ML-level as follows:
 @{ML_response_fake [display,gray]
 "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
+"nat \<Rightarrow> bool"}
+or with the antiquotation:
+@{ML_response_fake [display,gray]
+"@{ctyp \"nat \<Rightarrow> bool\"}"
 "nat \<Rightarrow> bool"}
 \begin{readmore}
 For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see
 the file @{ML_file "Pure/thm.ML"}.
 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: handy functions working on theorems; how to add case-names to goal
+(FIXME: handy functions working on theorems, like @{ML ObjectLogic.rulify} and so on)
-states - maybe in the next section)
+(FIXME how to add case-names to goal states - maybe in the
+next section)
 *}
 section {* Theorem Attributes *}
 text {*
 @{text "> HOL.elim:  declaration of Classical elimination rule"}\\
 @{text "> \<dots>"}
 \end{isabelle}
 The theorem attributes fall roughly into two categories: the first category manipulates
-the proved theorem (like @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
+the proved theorem (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
-stores the proved theorem somewhere as data (like @{text "[simp]"}, which adds
+stores the proved theorem somewhere as data (for example @{text "[simp]"}, which adds
 the theorem to the current simpset).
 To explain how to write your own attribute, let us start with an extremely simple
 version of the attribute @{text "[symmetric]"}. The purpose of this attribute is
 to produce the ``symmetric'' version of an equation. The main function behind
 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 (which we ignore in the code above) and a theorem (@{text thm}), and
-returns another theorem (namely @{text thm} resolved with the lemma
+returns another theorem (namely @{text thm} resolved with the theorem
-@{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns
+@{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML RS} is explained
+later on in Section~\ref{sec:simpletacs}.} 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 Isabelle command \isacommand{attribute\_setup} as follows:
 *}
 attribute_setup %gray my_sym = {* Scan.succeed my_symmetric *}
 "applying the sym rule"
 text {*
-The attribute does not expect any further arguments (unlike @{text "[THEN
+Inside the @{text "\<verbopen> \<dots> \<verbclose>"}, we have to specify a parser
-\<dots>]"}, for example). Therefore
+for the theorem attribute. Since the attribute does not expect any further
-we use the parser @{ML Scan.succeed}. Later on we will also consider
+arguments (unlike @{text "[THEN \<dots>]"}, for example), we use the parser @{ML
-attributes taking further arguments. An example for the attribute @{text
+Scan.succeed}. Later on we will also consider attributes taking further
-"[my_sym]"} is the proof
+arguments. An example for the attribute @{text "[my_sym]"} is the proof
 *}
 lemma test[my_sym]: "2 = Suc (Suc 0)" by simp
 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 will take a list of theorems
+our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
 as argument and resolve the proved theorem with this list (one theorem
 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 (@{ML RS} is explained
+where @{ML swap} swaps the components of a pair. The setup of this theorem
-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 *}
 *}
 ML{*val my_thms = ref ([] : thm list)*}
 text {*
-A word of warning: such references must not be used in any code that
+The purpose of this reference is that we are going to add and delete theorems
-is meant to be more than just for testing purposes! Here it is only used
+to the referenced list. However, a word of warning: such references must not
-to illustrate matters. We will show later how to store data properly without
+be used in any code that is meant to be more than just for testing purposes!
-using references.
+Here it is only used to illustrate matters. We will show later how to store
+data properly without using references.
-The function @{ML Thm.declaration_attribute} expects us to
+We need to provide two functions that add and delete theorems from this list.
-provide two functions that add and delete theorems from this list.
 For this we use the two functions:
 *}
-ML{*fun my_thms_add thm ctxt =
+ML{*fun my_thm_add thm ctxt =
 (my_thms := Thm.add_thm thm (!my_thms); ctxt)
-fun my_thms_del thm ctxt =
+fun my_thm_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 that they just return the context unchanged. They change
 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).
-You can turn functions @{ML my_thms_add} and @{ML my_thms_del} into
+You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into
 attributes with the code
 *}
-ML{*val my_add = Thm.declaration_attribute my_thms_add
+ML{*val my_add = Thm.declaration_attribute my_thm_add
-val my_del = Thm.declaration_attribute my_thms_del *}
+val my_del = Thm.declaration_attribute my_thm_del *}
 text {*
 and set up the attributes as follows
 *}
 attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *}
-"maintaining a list of my_thms"
+"maintaining a list of my_thms - rough test only!"
 text {*
-The parser @{ML Attrib.add_del} is a predefined parser for
+The parser @{ML Attrib.add_del} is a pre-defined parser for
 adding and deleting lemmas. Now if you prove the next lemma
-and attach the attribute
+and attach to it the attribute @{text "[my_thms]"}
-@{text "[my_thms]"}
 *}
 lemma trueI_2[my_thms]: "True" by simp
 text {*
 "!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
+With this attribute, the @{text "add"} operation is the default and does
-to be explicitly given. These two declarations will cause the
+not need to be explicitly given. These three declarations will cause the
 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'', below called @{text MyThmsData}, by using the functor
+start a ``data slot'', below called @{text MyThmsData}, generated by the functor
 @{text GenericDataFun}:
 *}
 ML {*structure MyThmsData = GenericDataFun
 (type T = thm list
 val empty = []
 val extend = I
 fun merge _ = Thm.merge_thms) *}
 text {*
-To use this data slot, you only have to change @{ML my_thms_add} and
+The type @{text "T"} of this data slot is @{ML_type "thm list"}.\footnote{FIXME: give a pointer
-@{ML my_thms_del} to:
+to where data slots are explained properly.}
-*}
+To use this data slot, you only have to change @{ML my_thm_add} and
+@{ML my_thm_del} to:
-ML{*val thm_add = MyThmsData.map o Thm.add_thm
+*}
-val thm_del = MyThmsData.map o Thm.del_thm*}
+ML{*val my_thm_add = MyThmsData.map o Thm.add_thm
+val my_thm_del = MyThmsData.map o Thm.del_thm*}
 text {*
 where @{ML MyThmsData.map} updates the data appropriately. The
 corresponding theorem addtributes are
 *}
-ML{*val add = Thm.declaration_attribute thm_add
+ML{*val my_add = Thm.declaration_attribute my_thm_add
-val del = Thm.declaration_attribute thm_del *}
+val my_del = Thm.declaration_attribute my_thm_del *}
 text {*
 and the setup is as follows
 *}
-attribute_setup %gray my_thms2 = {* Attrib.add_del add del *}
+attribute_setup %gray my_thms2 = {* Attrib.add_del my_add my_del *}
 "properly maintaining a list of my_thms"
 text {*
 Initially, the data slot is empty
 @{ML_response_fake [display,gray]
 "MyThmsData.get (Context.Proof @{context})"
 "[]"}
 *}
 lemma three[my_thms2]: "3 = Suc (Suc (Suc 0))" by simp
 text {*
-the lemma is now included
+then the lemma is recorded.
 @{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
+With theorem attribute @{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
+to the point just before the lemma @{thm [source] three} was proved and
-check the the content of @{ML_struct "MyThmsData"}: it is now again
+check the the content of @{ML_struct "MyThmsData"}: it should be empty.
-empty. The addition has been properly retracted. Now consider the proof:
+The addition has been properly retracted. Now consider the proof:
 *}
 lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp
 text {*
 @{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
+as expected, but if you 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!
+of Isabelle is completely oblivious about what to do with references, but
+properly treats ``data slots''!
-Since storing theorems in a special list is such a common task, there is the
+Since storing theorems in a list is such a common task, there is the special
 functor @{text NamedThmsFun}, which does most of the work for you. To obtain
-such a named theorem lists, you just declare
+a named theorem lists, you just declare
 *}
 ML{*structure FooRules = NamedThmsFun
 (val name = "foo"
 val description = "Rules for foo") *}
 (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)
 \begin{readmore}
-FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"}
+FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in
+@{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about
+parsing.
 \end{readmore}
 *}
 section {* Setups (TBD) *}

changeset 207	d3cd633e8240
parent 204	3857d987576a
child 210	db8e302f44c8