isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:123401a5c8e9
+:5e309df58557
 @{text "\<verbclose>"}\isanewline
 @{text "> 7"}\smallskip
 \end{graybox}
 \end{isabelle}
-Like normal Isabelle proof scripts,
+Like normal Isabelle proof scripts, \isacommand{ML}-commands can be
-\isacommand{ML}-commands can be evaluated by using the advance and undo buttons of
+evaluated by using the advance and undo buttons of your Isabelle
-your Isabelle environment. The code inside the \isacommand{ML}-command
+environment. The code inside the \isacommand{ML}-command can also contain
-can also contain value and function bindings, and even those can be
+value and function bindings, and even those can be undone when the proof
-undone when the proof script is retracted. As mentioned earlier, we will
+script is retracted. As mentioned earlier, we will drop the
-drop the \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}
+\isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
-scaffolding whenever we show code.
+show code. The lines prefixed with @{text ">"} are not part of the
+code, rather they indicate what the response is when the code is evaluated.
-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
+Once a portion of code is relatively stable, you usually want to export it
-theory by using the \isacommand{uses}-command in the header of the theory, like:
+to a separate ML-file. Such files can then be included in a theory by using
+the \isacommand{uses}-command in the header of the theory, like:
 \begin{center}
 \begin{tabular}{@ {}l}
 \isacommand{theory} FirstSteps\\
 \isacommand{imports} Main\\
 You can print out error messages with the function @{ML error}, as in:
 @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
+See leter on in Section~\ref{sec:printing} for information about printing
+out data of type @{ML_type term}, @{ML_type cterm} and @{ML_type thm}.
 *}
 section {* Constructing Terms and Types Manually *}
 text {*
 While antiquotations are very convenient for constructing terms, they can
-only construct fixed terms (remember they are ``linked'' at
+only construct fixed terms (remember they are ``linked'' at compile-time).
-compile-time). See Recipe~\ref{rec:external} on Page~\pageref{rec:external}
+However, you often need to construct terms dynamically. For example, a
-for a function that pattern-matches over terms and where the patterns are
+function that returns the implication @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking
-constructed using antiquotations.  However, one often needs to construct
+@{term P}, @{term Q} and the type @{term "\<tau>"} as arguments can only be
-terms dynamically. For example, a function that returns the implication
+written as:
-@{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:
 *}
 ML{*fun make_imp P Q tau =
 let
 val x = Free ("x",tau)
 in
 Logic.all x (Logic.mk_implies (P $ x, Q $ x))
 end *}
 text {*
-The reason is that one cannot pass the arguments @{term P}, @{term Q} and
+The reason is that you cannot pass the arguments @{term P}, @{term Q} and
 @{term "tau"} into an antiquotation. For example the following does \emph{not} work:
 *}
 ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}
 text {*
 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"}
 to both functions. With @{ML make_imp} we obtain the intended term involving
-@{term "S"}, @{text "T"} and  @{text "@{typ nat}"}
+the given arguments
 @{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}"
 "Const \<dots> $
 Abs (\"x\", Type (\"nat\",[]),
 Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $
 @{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"}
 (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
-Similarly, one can construct types manually. For example the function returning
+Similarly, you occasionally need to construct types manually. For example
-a function type is as follows:
+the function returning a function type is as follows:
 *}
 ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
 text {*
 \begin{readmore}
 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
-@{ML_file "HOL/hologic.ML"} that make such manual constructions of terms
+@{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms
 and types easier.\end{readmore}
 Have a look at these files and try to solve the following two exercises:
 *}
 section {* Type-Checking *}
 text {*
-We can freely construct and manipulate terms, since they are just
+You can freely construct and manipulate terms, since they are just
-arbitrary unchecked trees. However, we eventually want to see if a
+arbitrary unchecked trees. However, you eventually want to see if a
 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 they can only be constructed via ``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
+For example you can write:
 @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
-This can also be wirtten with an antiquotation
+This can also be wirtten with an antiquotation:
 @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
 Attempting to obtain the certified term for
 @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
 yields an error (since the term is not typable). A slightly more elaborate
-example that type-checks is
+example that type-checks is:
 @{ML_response_fake [display,gray]
 "let
 val natT = @{typ \"nat\"}
 val zero = @{term \"0::nat\"}
 }
 }
 }
 \]
+However, while we obtained a theorem as result, this theorem is not
+yet stored in Isabelle's theorem database. So it cannot be referenced later
+on. How to store theorems will be explained in the next section.
 \begin{readmore}
 For the functions @{text "assume"}, @{text "forall_elim"} etc
 see \isccite{sec:thms}. The basic functions for theorems are defined in
 @{ML_file "Pure/thm.ML"}.
 section {* Theorem Attributes *}
 section {* Printing Terms, CTerms and Theorems\label{sec:printing} *}
 text {*
-You will occationally feel the need to inspect terms, cterms or theorems during
+During development, you will occationally feel the need to inspect terms, cterms
-development. Isabelle contains elaborate pretty-printing functions for that, but
+or theorems. Isabelle contains elaborate pretty-printing functions for that, but
 for quick-and-dirty solutions they are way too unwieldy. A simple way to transform
 a term into a string is to use the function @{ML Syntax.string_of_term}.
 @{ML_response_fake [display,gray]
 "Syntax.string_of_term @{context} @{term \"1::nat\"}"
 ML{*fun str_of_cterm ctxt t =
 Syntax.string_of_term ctxt (term_of t)*}
 text {*
-If there are more than one @{ML_type cterm} to be printed, you can use the function
+If there are more than one @{ML_type cterm}s to be printed, you can use the
-@{ML commas} to conveniently separate them.
+function @{ML commas} to separate them.
 *}
 ML{*fun str_of_cterms ctxt ts =
 commas (map (str_of_cterm ctxt) ts)*}
 text {*
 The easiest way to get the string of a theorem is to transform it
 into a @{ML_type cterm} using the function @{ML crep_thm}.
 *}
 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 "|>>"} and @{ML "||>"} are defined for
 functions manipulating pairs. The first applies the function to
-the first component of the pair, defined as:
+the first component of the pair, defined as
 *}
 ML{*fun (x, y) |>> f = (f x, y)*}
 text {*

changeset 102	5e309df58557
parent 101	123401a5c8e9
child 104	5dcad9348e4d