--- a/ProgTutorial/FirstSteps.thy Sun Oct 11 22:45:29 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Sun Oct 11 23:16:34 2009 +0200
@@ -352,21 +352,24 @@
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*}
@@ -443,19 +446,20 @@
end"
"P z za zb"}
- You can read off this behaviour from how @{ML apply_fresh_args} is
- coded: in Line 2, the function @{ML_ind fastype_of} calculates the type of the
- term; @{ML_ind binder_types} in the next line produces the list of argument
- 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_ind 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_ind list_comb} to the term. In this last step we have to
- use the function @{ML_ind curry}, because @{ML_ind list_comb} expects the
- function and the variables list as a pair. This kind of functions is often needed when
- constructing terms with fresh variables. The infrastructure helps tremendously
- to avoid any name clashes. Consider for example:
+ You can read off this behaviour from how @{ML apply_fresh_args} is coded: in
+ Line 2, the function @{ML_ind fastype_of in Term} calculates the type of the
+ term; @{ML_ind binder_types in Term} in the next line produces the list of
+ argument 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_ind
+ 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_ind list_comb in Term} to the term. In this last step we have
+ to use the function @{ML_ind curry in Library}, because @{ML list_comb}
+ expects the function and the variables list as a pair. This kind of
+ functions is often needed when constructing terms with fresh variables. The
+ infrastructure helps tremendously to avoid any name clashes. Consider for
+ example:
@{ML_response_fake [display,gray]
"let
@@ -470,8 +474,8 @@
where the @{text "za"} is correctly avoided.
- The combinator @{ML_ind "#>"} is the reverse function composition. It can be
- used to define the following function
+ The combinator @{ML_ind "#>" in Basics} is the reverse function composition.
+ It can be used to define the following function
*}
ML{*val inc_by_six =
@@ -485,10 +489,9 @@
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
- you to get hold of an intermediate result (to do some side-calculations for
- instance). The function
-
+ ``waterfall method'' of writing functions. The combinator @{ML_ind tap in
+ Basics} allows you to get hold of an intermediate result (to do some
+ side-calculations for instance). The function
*}
ML %linenosgray{*fun inc_by_three x =
@@ -498,15 +501,15 @@
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''
- intermediate result inside the tracing buffer. The function @{ML_ind tap} can
+ middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
+ 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
- function to the value and returns the result together with the value (as a
- pair). For example the function
+ The combinator @{ML_ind "`" in Basics} (a backtick) is similar to @{ML tap},
+ but applies a function to the value and returns the result together with the
+ value (as a pair). For example the function
*}
ML{*fun inc_as_pair x =
@@ -519,8 +522,8 @@
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
- functions manipulating pairs. The first applies the function to
+ The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are
+ defined for functions manipulating pairs. The first applies the function to
the first component of the pair, defined as
*}
@@ -566,8 +569,8 @@
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.
- This combinator is defined as
+ With the combinator @{ML_ind "|->" in Basics} you can re-combine the
+ elements from a pair. This combinator is defined as
*}
ML{*fun (x, y) |-> f = f x y*}
@@ -582,11 +585,12 @@
|-> (fn x => fn y => x + y)*}
text {*
- The combinator @{ML_ind ||>>} plays a central rôle whenever your task is to update a
- theory and the update also produces a side-result (for example a theorem). Functions
- for such tasks return a pair whose second component is the theory and the fist
- component is the side-result. Using @{ML_ind ||>>}, you can do conveniently the update
- and also accumulate the side-results. Consider the following simple function.
+ The combinator @{ML_ind ||>> in Basics} plays a central rôle whenever your
+ task is to update a theory and the update also produces a side-result (for
+ example a theorem). Functions for such tasks return a pair whose second
+ component is the theory and the fist component is the side-result. Using
+ @{ML ||>>}, you can do conveniently the update and also
+ accumulate the side-results. Consider the following simple function.
*}
ML %linenosgray{*fun acc_incs x =
@@ -597,7 +601,7 @@
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]
@@ -614,14 +618,13 @@
*}
text {*
- Recall that @{ML_ind "|>"} is the reverse function application. Recall also that
- the related
- reverse function composition is @{ML_ind "#>"}. In fact all the combinators
- @{ML_ind "|->"}, @{ML_ind "|>>"} , @{ML_ind "||>"} and @{ML_ind
- "||>>"} described above have related combinators for
- function composition, namely @{ML_ind "#->"}, @{ML_ind "#>>"},
- @{ML_ind "##>"} and @{ML_ind "##>>"}.
- Using @{ML_ind "#->"}, for example, the function @{text double} can also be written as:
+ Recall that @{ML "|>"} is the reverse function application. Recall also that
+ the related reverse function composition is @{ML "#>"}. In fact all the
+ combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
+ described above have related combinators for function composition, namely
+ @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in
+ Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the
+ function @{text double} can also be written as:
*}
ML{*val double =
@@ -637,7 +640,7 @@
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]
@@ -708,7 +711,7 @@
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
@@ -779,7 +782,7 @@
"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"}.
*}
@@ -814,7 +817,7 @@
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.
*}