isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:42a1c230daff
+:43df2d59fb98
 @{ML_response_fake [display,gray]
 "let
 val natT = @{typ \"nat\"}
 val zero = @{term \"0::nat\"}
-in
+val plus = Const (@{const_name plus}, [natT, natT] ---> natT)
-cterm_of @{theory}
+in
-(Const (@{const_name plus}, [natT, natT] ---> natT) $ zero $ zero)
+cterm_of @{theory} (plus $ zero $ zero)
-end" "0 + 0"}
+end"
+"0 + 0"}
 In Isabelle not just terms need to be certified, but also types. For example,
 you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on
 the ML-level as follows:
 ML{*structure MyThmList = GenericDataFun
 (type T = thm list
 val empty = []
 val extend = I
-val merge = K (op @)
+val merge = K (op @))
-)
 fun update thm = Context.theory_map (MyThmList.map (fn thms => thm::thms))*}
 text {*
 The function @{ML update} allows us to update the theorem list, for example
 text {*
 We can now install a the modified theorem style as follows
 *}
-setup %gray {*
+setup %gray {* let
-let
 val parser = Scan.repeat Args.name
 fun action xs = K (rename_allq xs #> strip_allq)
 in
 Term_Style.setup "my_strip_allq2" (parser >> action)
 end *}
 section {* Theorem Attributes\label{sec:attributes} *}
 text {*
 Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text
 "[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
-annotated to theorems, but functions that do further processing once a
+annotated to theorems, but functions that do further processing of
-theorem is proved. In particular, it is not possible to find out
+theorems. In particular, it is not possible to find out
 what are all theorems that have a given attribute in common, unless of course
 the function behind the attribute stores the theorems in a retrievable
 data structure.
 If you want to print out all currently known attributes a theorem can have,
 @{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 (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
+theorems (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
-stores the proved theorem somewhere as data (for example @{text "[simp]"}, which adds
+stores theorems somewhere as data (for example @{text "[simp]"}, which adds
-the theorem to the current simpset).
+theorems 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
 this attribute is
 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 *}
+attribute_setup %gray my_sym =
-"applying the sym rule"
+{* Scan.succeed my_symmetric *} "applying the sym rule"
 text {*
 Inside the @{text "\<verbopen> \<dots> \<verbclose>"}, we have to specify a parser
 for the theorem attribute. Since the attribute does not expect any further
-arguments (unlike @{text "[THEN \<dots>]"}, for example), we use the parser @{ML
+arguments (unlike @{text "[THEN \<dots>]"}, for instance), we use the parser @{ML
-Scan.succeed}. Later on we will also consider attributes taking further
+Scan.succeed}. An example for the attribute @{text "[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 {*
 ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
 "applying the sym rule" *}
 text {*
-This gives a function from @{ML_type "Context.theory -> Context.theory"}, which
+This gives a function from @{ML_type "theory -> theory"}, which
 can be used for example with \isacommand{setup}.
 As an example of a slightly more complicated theorem attribute, we implement
 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
+as argument and resolve the 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)*}
+Thm.rule_attribute (fn _ => fn thm => List.foldl ((op RS) o swap) thm thms)*}
 text {*
 where @{ML swap} swaps the components of a pair. The setup of this theorem
 attribute uses the parser @{ML thms in Attrib}, which parses a list of
 theorems.
 *}
 attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *}
-"resolving the list of theorems with the proved theorem"
+"resolving the list of theorems with the theorem"
 text {*
 You can, for example, use this theorem attribute to turn an equation into a
 meta-equation:
 end"
 "ab
 a
 b"}
-\footnote{\bf What happens with printing big formulae?}
+\footnote{\bf FIXME: What happens with printing big formulae?}
 \begin{readmore}
 The general infrastructure for pretty-printing is implemented in the file

changeset 356	43df2d59fb98
parent 355	42a1c230daff
child 358	9cf3bc448210