--- a/CookBook/FirstSteps.thy Mon Jan 26 01:10:21 2009 +0000
+++ b/CookBook/FirstSteps.thy Mon Jan 26 12:28:43 2009 +0000
@@ -44,7 +44,7 @@
can also contain value and function bindings, and even those can be
undone when the proof script is retracted. As mentioned earlier, we will
drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}
- whenever we show code and its response.
+ whenever we show code.
Once a portion of code is relatively stable, one usually wants to
export it to a separate ML-file. Such files can then be included in a
@@ -80,7 +80,7 @@
@{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""}
However @{ML makestring} only works if the type of what is converted is monomorphic
- and is not a function.
+ and not a function.
The function @{ML "warning"} should only be used for testing purposes, because any
output this function generates will be overwritten as soon as an error is
@@ -91,7 +91,7 @@
@{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
It is also possible to redirect the ``channel'' where the string @{text "foo"} is
- printed to a separate file, e.g. to prevent ProofGeneral from choking on massive
+ printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive
amounts of trace output. This redirection can be achieved using the code
*}
@@ -167,16 +167,17 @@
map #name (Net.entries rules)
end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
- The code above extracts the theorem names that are stored in a simpset.
- We refer to the current simpset with the antiquotation @{text "@{simpset}"}.
+ The code above extracts the theorem names that are stored in the current simpset.
+ We refer to the simpset with the antiquotation @{text "@{simpset}"}.
The function @{ML rep_ss in MetaSimplifier} returns a record
containing all information about the simpset. The rules of a simpset are stored
- in a discrimination net (a datastructure for fast indexing). From this net
+ in a \emph{discrimination net} (a datastructure for fast indexing). From this net
we can extract the entries using the function @{ML Net.entries}.
\begin{readmore}
- The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
- and @{ML_file "Pure/simplifier.ML"}.
+ The infrastructure for simpsets is contained in @{ML_file "Pure/meta_simplifier.ML"}
+ and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented
+ in @{ML_file "Pure/net.ML"}.
\end{readmore}
While antiquotations have many applications, they were originally introduced in order
@@ -186,8 +187,8 @@
ML{*val allI = thm "allI" *}
text {*
- These bindings were difficult to maintain and also could be accidentally
- overwritten by the user. This usually broke definitional
+ These bindings are difficult to maintain and also can be accidentally
+ overwritten by the user. This often breakes definitional
packages. Antiquotations solve this problem, since they are ``linked''
statically at compile-time. However, this static linkage also limits their
usefulness in cases where data needs to be build up dynamically. In the course of
@@ -220,7 +221,7 @@
\begin{readmore}
Terms are described in detail in \isccite{sec:terms}. Their
- definition and many useful operations can be found in @{ML_file "Pure/term.ML"}.
+ definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
\end{readmore}
Sometimes the internal representation of terms can be surprisingly different
@@ -265,7 +266,8 @@
\begin{readmore}
Types are described in detail in \isccite{sec:types}. Their
- definition and many useful operations can also be found in @{ML_file "Pure/type.ML"}.
+ definition and many useful operations are implemented
+ in @{ML_file "Pure/type.ML"}.
\end{readmore}
*}
@@ -274,7 +276,7 @@
text {*
- While antiquotations are very convenient for constructing terms and types,
+ While antiquotations are very convenient for constructing terms,
they can only construct fixed terms (remember they are ``linked'' at compile-time).
However, one often needs to construct terms
dynamically. For example, a function that returns the implication
@@ -308,7 +310,7 @@
Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $
(Free (\"T\",\<dots>) $ \<dots>))"}
- With @{ML make_wrong_imp} we obtain a term involving the @{term "P"}
+ Whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"}
and @{text "Q"} from the antiquotation.
@{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}"
@@ -337,8 +339,8 @@
(FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
- Similarly, types can be constructed manually. For example a function type
- can be constructed as follows:
+ Similarly, one can construct types manually. For example the function returning
+ a function type is as follows:
*}
@@ -388,7 +390,7 @@
a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
Unlike @{ML_type term}s, which are just trees, @{ML_type
"cterm"}s are abstract objects that are guaranteed to be
- type-correct, and that can only be constructed via the ``official
+ type-correct, and they can only be constructed via the ``official
interfaces''.
Type-checking is always relative to a theory context. For now we use
@@ -401,11 +403,13 @@
@{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
- Attempting
+ Attempting to obtain the certified term for
@{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
- yields an error. A slightly more elaborate example is
+ yields an error (since the term is not typable). A slightly more elaborate
+ example that type-checks is
+
@{ML_response_fake [display,gray]
"let
@@ -427,10 +431,11 @@
text {*
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
- that can only be built by going through interfaces. As a consequence of this is that
- every proof is correct by construction (FIXME reference LCF-philosophy)
+ that can only be built by going through interfaces. As a consequence, every proof
+ in Isabelle is correct by construction (FIXME reference LCF-philosophy)
- To see theorems in ``action'', let us give a proof for the following statement
+ To see theorems in ``action'', let us give a proof on the ML-level for the following
+ statement:
*}
lemma
@@ -439,7 +444,7 @@
shows "Q t" (*<*)oops(*>*)
text {*
- on the ML-level:\footnote{Note that @{text "|>"} is reverse
+ The corresponding ML-code is as follows:\footnote{Note that @{text "|>"} is reverse
application. See Section~\ref{sec:combinators}.}
@{ML_response_fake [display,gray]
@@ -492,13 +497,15 @@
section {* Operations on Constants (Names) *}
text {*
- (FIXME how can I extract the constant name without the theory name etc)
+
+@{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
+
*}
section {* Combinators\label{sec:combinators} *}
text {*
- Perhaps one of the most puzzling aspects for a beginner when reading at
+ Perhaps one of the most puzzling aspects for a beginner when reading
existing Isabelle code is the liberal use of combinators. At first they
seem to obstruct the comprehension of the code, but after getting familiar
with them they actually ease the reading and also the programming.
@@ -508,7 +515,7 @@
and @{ML_file "Pure/General/basics.ML"}.
\end{readmore}
- The simplest combinator is @{ML I} which is just the identidy function.
+ The simplest combinator is @{ML I} which is just the identity function.
*}
ML{*fun I x = x*}
@@ -521,9 +528,103 @@
which ``wraps'' a function around the argument @{text "x"}. This function
ignores its argument.
- @{ML "(op |>)"}
+ The next combinator is reverse application defined as
*}
ML{*fun x |> f = f x*}
+text {* The purpose of this combinator is to implement functions in a
+ ``waterfall fashion''. Consider for example the function *}
+
+ML %linenumbers{*fun inc_by_five x =
+ x |> (fn x => x + 1)
+ |> (fn x => (x, x))
+ |> fst
+ |> (fn x => x + 4)*}
+
+text {*
+ which increments the argument @{text x} by 5. It does this by first incrementing
+ the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking
+ the first component of the pair (Line 4) and finally incrementing the first
+ component by 4 (Line 5). This kind of cascading manipulations of values is quite
+ common when extending theories (for example by adding a definition, followed by
+ lemmas and so on). Writing the function @{ML inc_by_five} using the reverse
+ application is much clearer than writing
+*}
+
+ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
+
+text {* or *}
+
+ML{*fun inc_by_five x =
+ ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
+
+text {* and much more economical than *}
+
+ML{*fun inc_by_five x =
+ let val y1 = x + 1
+ val y2 = (y1, y1)
+ val y3 = fst y2
+ val y4 = y3 + 4
+ in y4 end*}
+
+text {*
+ Similarly, the combinator @{ML "(op #>)"} is the reverse function
+ composition. It allows us to define functions as follows
+*}
+
+ML{*val inc_by_six =
+ (fn x => x + 1)
+ #> (fn x => x + 2)
+ #> (fn x => x + 3)*}
+
+text {*
+ which is the function composed of first the increment-by-one function and then
+ increment-by-two, followed by increment-by-three. Applying 6 to this function
+ yields
+
+ @{ML_response [display,gray] "inc_by_six 6" "12"}
+
+ as expected.
+
+ The remaining combinators add convenience for the ``waterfall method''
+ of writing functions. The combinator @{ML tap} allows one to get
+ hold of a intermediate result for some side-calculations. For
+ example the function *}
+
+ML{*fun inc_by_three x =
+ x |> (fn x => x + 1)
+ |> tap (fn x => tracing (makestring x))
+ |> (fn x => x + 2)*}
+
+text {* increments the argument first by one and then by two. In the middle,
+ however, it prints the ``plus-one'' intermediate result inside the
+ tracing buffer.
+
+ The combinator @{ML "(op `)"} is similar, but applies a function to the value
+ and returns the result together with the original value as pair. For example
+ the following function takes @{text x} then increments @{text x} and returns
+ the pair @{ML "(x + 1,x)" for x}. It then increments the right-hand component
+ of the pair.
+*}
+
+ML{*fun inc_as_pair x =
+ x |> `(fn x => x + 1)
+ |> (fn (x, y) => (x, y + 1))*}
+
+text {*
+ The combinators @{ML "(op |>>)"} and @{ML "(op ||>)"} are defined for
+ functions manipulating pairs. The first applies the function to
+ the first component of the pair:
+*}
+
+ML{*fun (x, y) |>> f = (f x, y)*}
+
+text {*
+ and the second combinator to the second component:
+*}
+
+ML{*fun (x, y) ||> f = (x, f y)*}
+
+
end
\ No newline at end of file