isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:8f73e80c8c6f
+:83d5bca38bec
 For beginners perhaps the most puzzling parts in the existing code of Isabelle are
 the combinators. At first they seem to greatly obstruct the
 comprehension of the code, but after getting familiar with them, they
 actually ease the understanding and also the programming.
-The simplest combinator is @{ML_ind  I}, which is just the identity function defined as
+The simplest combinator is @{ML_ind I in Basic_Library}, which is just the
+identity function defined as
 *}
 ML{*fun I x = x*}
-text {* Another simple combinator is @{ML_ind  K}, defined as *}
+text {*
+Another simple combinator is @{ML_ind K in Library}, defined as
+*}
 ML{*fun K x = fn _ => x*}
 text {*
-@{ML_ind  K} ``wraps'' a function around the argument @{text "x"}. However, this
+@{ML K} ``wraps'' a function around the argument @{text "x"}. However, this
 function ignores its argument. As a result, @{ML K} defines a constant function
 always returning @{text x}.
-The next combinator is reverse application, @{ML_ind  "|>"}, defined as:
+The next combinator is reverse application, @{ML_ind  "|>" in Basics}, defined as:
 *}
 ML{*fun x |> f = f x*}
 text {* While just syntactic sugar for the usual function application,
 |> string_of_term ctxt
 |> tracing
 end"
 "P z za zb"}
-You can read off this behaviour from how @{ML apply_fresh_args} is
+You can read off this behaviour from how @{ML apply_fresh_args} is coded: in
-coded: in Line 2, the function @{ML_ind  fastype_of} calculates the type of the
+Line 2, the function @{ML_ind fastype_of in Term} calculates the type of the
-term; @{ML_ind binder_types} in the next line produces the list of argument
+term; @{ML_ind binder_types in Term} in the next line produces the list of
-types (in the case above the list @{text "[nat, int, unit]"}); Line 4
+argument types (in the case above the list @{text "[nat, int, unit]"}); Line
-pairs up each type with the string  @{text "z"}; the
+4 pairs up each type with the string @{text "z"}; the function @{ML_ind
-function @{ML_ind  variant_frees in Variable} generates for each @{text "z"} a
+variant_frees in Variable} generates for each @{text "z"} a unique name
-unique name avoiding the given @{text f}; the list of name-type pairs is turned
+avoiding the given @{text f}; the list of name-type pairs is turned into a
-into a list of variable terms in Line 6, which in the last line is applied
+list of variable terms in Line 6, which in the last line is applied by the
-by the function @{ML_ind  list_comb} to the term. In this last step we have to
+function @{ML_ind list_comb in Term} to the term. In this last step we have
-use the function @{ML_ind  curry}, because @{ML_ind  list_comb} expects the
+to use the function @{ML_ind curry in Library}, because @{ML list_comb}
-function and the variables list as a pair. This kind of functions is often needed when
+expects the function and the variables list as a pair. This kind of
-constructing terms with fresh variables. The infrastructure helps tremendously
+functions is often needed when constructing terms with fresh variables. The
-to avoid any name clashes. Consider for example:
+infrastructure helps tremendously to avoid any name clashes. Consider for
+example:
 @{ML_response_fake [display,gray]
 "let
 val t = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
 val ctxt = @{context}
 end"
 "za z zb"}
 where the @{text "za"} is correctly avoided.
-The combinator @{ML_ind  "#>"} is the reverse function composition. It can be
+The combinator @{ML_ind "#>" in Basics} is the reverse function composition.
-used to define the following function
+It can be used to define the following function
 *}
 ML{*val inc_by_six =
 (fn x => x + 1)
 #> (fn x => x + 2)
 which is the function composed of first the increment-by-one function and then
 increment-by-two, followed by increment-by-three. Again, the reverse function
 composition allows you to read the code top-down.
 The remaining combinators described in this section add convenience for the
-``waterfall method'' of writing functions. The combinator @{ML_ind  tap} allows
+``waterfall method'' of writing functions. The combinator @{ML_ind tap in
-you to get hold of an intermediate result (to do some side-calculations for
+Basics} allows you to get hold of an intermediate result (to do some
-instance). The function
+side-calculations for instance). The function
 *}
 ML %linenosgray{*fun inc_by_three x =
 x |> (fn x => x + 1)
 |> tap (fn x => tracing (PolyML.makestring x))
 |> (fn x => x + 2)*}
 text {*
 increments the argument first by @{text "1"} and then by @{text "2"}. In the
-middle (Line 3), however, it uses @{ML_ind  tap} for printing the ``plus-one''
+middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
-intermediate result inside the tracing buffer. The function @{ML_ind  tap} can
+intermediate result inside the tracing buffer. The function @{ML tap} can
 only be used for side-calculations, because any value that is computed
 cannot be merged back into the ``main waterfall''. To do this, you can use
 the next combinator.
-The combinator @{ML_ind  "`"} (a backtick) is similar to @{ML tap}, but applies a
+The combinator @{ML_ind "`" in Basics} (a backtick) is similar to @{ML tap},
-function to the value and returns the result together with the value (as a
+but applies a function to the value and returns the result together with the
-pair). For example the function
+value (as a pair). For example the function
 *}
 ML{*fun inc_as_pair x =
 x |> `(fn x => x + 1)
 |> (fn (x, y) => (x, y + 1))*}
 takes @{text x} as argument, and then increments @{text x}, but also keeps
 @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
 for x}. After that, the function increments the right-hand component of the
 pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
-The combinators @{ML_ind  "|>>"} and @{ML_ind  "||>"} are defined for
+The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are
-functions manipulating pairs. The first applies the function to
+defined for functions manipulating pairs. The first applies the function to
 the first component of the pair, defined as
 *}
 ML{*fun (x, y) |>> f = (f x, y)*}
 text {*
 avoiding the explicit @{text "let"}. While in this example the gain in
 conciseness is only small, in more complicated situations the benefit of
 avoiding @{text "lets"} can be substantial.
-With the combinator @{ML_ind  "|->"} you can re-combine the elements from a pair.
+With the combinator @{ML_ind "|->" in Basics} you can re-combine the
-This combinator is defined as
+elements from a pair. This combinator is defined as
 *}
 ML{*fun (x, y) |-> f = f x y*}
 text {*
 ML{*fun double x =
 x |>  (fn x => (x, x))
 |-> (fn x => fn y => x + y)*}
 text {*
-The combinator @{ML_ind  ||>>} plays a central rôle whenever your task is to update a
+The combinator @{ML_ind ||>> in Basics} plays a central rôle whenever your
-theory and the update also produces a side-result (for example a theorem). Functions
+task is to update a theory and the update also produces a side-result (for
-for such tasks return a pair whose second component is the theory and the fist
+example a theorem). Functions for such tasks return a pair whose second
-component is the side-result. Using @{ML_ind  ||>>}, you can do conveniently the update
+component is the theory and the fist component is the side-result. Using
-and also accumulate the side-results. Consider the following simple function.
+@{ML ||>>}, you can do conveniently the update and also
+accumulate the side-results. Consider the following simple function.
 *}
 ML %linenosgray{*fun acc_incs x =
 x |> (fn x => ("", x))
 ||>> (fn x => (x, x + 1))
 ||>> (fn x => (x, x + 1))
 ||>> (fn x => (x, x + 1))*}
 text {*
 The purpose of Line 2 is to just pair up the argument with a dummy value (since
-@{ML_ind  "||>>"} operates on pairs). Each of the next three lines just increment
+@{ML ||>>} operates on pairs). Each of the next three lines just increment
 the value by one, but also nest the intermediate results to the left. For example
 @{ML_response [display,gray]
 "acc_incs 1"
 "((((\"\", 1), 2), 3), 4)"}
 \footnote{\bf FIXME: maybe give a ``real world'' example for this combinator.}
 *}
 text {*
-Recall that @{ML_ind  "|>"} is the reverse function application. Recall also that
+Recall that @{ML "|>"} is the reverse function application. Recall also that
-the related
+the related reverse function composition is @{ML "#>"}. In fact all the
-reverse function composition is @{ML_ind  "#>"}. In fact all the combinators
+combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
-@{ML_ind  "|->"}, @{ML_ind  "|>>"} , @{ML_ind  "||>"} and @{ML_ind
+described above have related combinators for function composition, namely
-"||>>"} described above have related combinators for
+@{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in
-function composition, namely @{ML_ind  "#->"}, @{ML_ind  "#>>"},
+Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the
-@{ML_ind  "##>"} and @{ML_ind  "##>>"}.
+function @{text double} can also be written as:
-Using @{ML_ind  "#->"}, for example, the function @{text double} can also be written as:
 *}
 ML{*val double =
 (fn x => (x, x))
 #-> (fn x => fn y => x + y)*}
 together. We have already seen such plumbing in the function @{ML
 apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
 list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such
 plumbing is also needed in situations where a function operate over lists,
 but one calculates only with a single element. An example is the function
-@{ML_ind  check_terms in Syntax}, whose purpose is to type-check a list
+@{ML_ind check_terms in Syntax}, whose purpose is to type-check a list
 of terms. Consider the code:
 @{ML_response_fake [display, gray]
 "let
 val ctxt = @{context}
 @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
 where @{text "@{theory}"} is an antiquotation that is substituted with the
 current theory (remember that we assumed we are inside the theory
 @{text FirstSteps}). The name of this theory can be extracted using
-the function @{ML_ind  theory_name in Context}.
+the function @{ML_ind theory_name in Context}.
 Note, however, that antiquotations are statically linked, that is their value is
 determined at ``compile-time'', not at ``run-time''. For example the function
 *}
 @{ML_response [display,gray]
 "@{binding \"name\"}"
 "name"}
 An example where a qualified name is needed is the function
-@{ML_ind  define in LocalTheory}.  This function is used below to define
+@{ML_ind define in LocalTheory}.  This function is used below to define
 the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
 *}
 local_setup %gray {*
 LocalTheory.define Thm.internalK
 also difficult to read. In the next chapter we will see how the (build in)
 antiquotation @{text "@{term \<dots>}"} can be used to construct terms.  A
 restriction of this antiquotation is that it does not allow you to use
 schematic variables. If you want to have an antiquotation that does not have
 this restriction, you can implement your own using the function @{ML_ind
-ML_Antiquote.inline}. The code for the antiquotation @{text "term_pat"} is
+inline in ML_Antiquote}. The code for the antiquotation @{text "term_pat"} is
 as follows.
 *}
 ML %linenosgray{*let
 val parser = Args.context -- Scan.lift Args.name_source

changeset 344	83d5bca38bec
parent 343	8f73e80c8c6f
child 346	0fea8b7a14a1