isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:bca83ed1d45a
+:ef778679d3e0
 \isacommand{ML}-commands can be evaluated by using the advance and undo buttons of
 your Isabelle environment. The code inside the \isacommand{ML}-command
 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
 theory by using \isacommand{uses} in the header of the theory, like
 converting values into strings, namely using the function @{ML makestring}:
 @{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
 raised. For printing anything more serious and elaborate, the
 function @{ML tracing} is more appropriate. This function writes all output into
 a separate tracing buffer. For example
 @{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
 *}
 ML{*val strip_specials =
 let
 val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset}
 in
 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.
+The code above extracts the theorem names that are stored in the current simpset.
-We refer to the current simpset with the antiquotation @{text "@{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"}
+The infrastructure for simpsets is contained in @{ML_file "Pure/meta_simplifier.ML"}
-and @{ML_file "Pure/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
 to avoid explicit bindings for theorems such as
 *}
 ML{*val allI = thm "allI" *}
 text {*
-These bindings were difficult to maintain and also could be accidentally
+These bindings are difficult to maintain and also can be accidentally
-overwritten by the user. This usually broke definitional
+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
 this introduction, we will learn more about
 these antiquotations: they greatly simplify Isabelle programming since one
 binds the corresponding variable. However, in Isabelle the names of bound variables are
 kept at abstractions for printing purposes, and so should be treated only as comments.
 \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
 from what you see at the user level, because the layers of
 parsing/type-checking/pretty printing can be quite elaborate.
 @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 \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}
 *}
 section {* Constructing Terms and Types Manually *}
 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
 @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term "\<tau>"}
 as arguments can only be written as
 "Const \<dots> $
 Abs (\"x\", Type (\"nat\",[]),
 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}"
 "Const \<dots> $
 Abs (\"x\", \<dots>,
 @{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"}
 (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
-Similarly, types can be constructed manually. For example a function type
+Similarly, one can construct types manually. For example the function returning
-can be constructed as follows:
+a function type is as follows:
 *}
 ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
 term is well-formed, or type-checks, relative to a theory.
 Type-checking is done via the function @{ML cterm_of}, which converts
 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
 the @{ML "@{theory}"} antiquotation to get hold of the current theory.
 For example we can write
 or use the antiquotation
 @{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
 val natT = @{typ \"nat\"}
 val zero = @{term \"0::nat\"}
 section {* Theorems *}
 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
+that can only be built by going through interfaces. As a consequence, every proof
-every proof is correct by construction (FIXME reference LCF-philosophy)
+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
 assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x"
 and     assm\<^isub>2: "P t"
 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]
 "let
 val thy = @{theory}
 section {* Theorem Attributes *}
 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.
 \begin{readmore}
 The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
 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*}
 text {* Another frequently used combinator is @{ML K} *}
 text {*
 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

changeset 78	ef778679d3e0
parent 75	f2dea0465bb4
child 81	8fda6b452f28