isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:0c3580c831a4
+:1783211b3494
 chapter {* First Steps *}
 text {*
-Isabelle programming is done in SML.  Just like lemmas and proofs, SML-code
+Isabelle programming is done in ML.  Just like lemmas and proofs, ML-code
 in Isabelle is part of a theory. If you want to follow the code written in
-this chapter, we assume you are working inside the theory defined by
+this chapter, we assume you are working inside the theory starting with
 \begin{center}
 \begin{tabular}{@ {}l}
 \isacommand{theory} FirstSteps\\
 \isacommand{imports} Main\\
 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
 \begin{center}
 \begin{tabular}{@ {}l}
-\isacommand{theory} CookBook\\
+\isacommand{theory} FirstSteps\\
 \isacommand{imports} Main\\
 \isacommand{uses} @{ML_text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
 \isacommand{begin}\\
 \ldots
 \end{tabular}
 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} should be used. This function writes all output into
+function @{ML tracing} is more appropriate. This function writes all output into
 a separate tracing buffer. For example
 @{ML [display] "tracing \"foo\""}
-It is also possible to redirect the ``channel'' where the @{ML_text "foo"} is
+It is also possible to redirect the ``channel'' where the string @{ML_text "foo"} is
 printed to a separate file, e.g. to prevent Proof General from choking on massive
 amounts of trace output. This redirection can be achieved using the code
 *}
 ML{*
 some data structure and return it. Instead, it is literally
 replaced with the value representing the theory name.
 In a similar way you can use antiquotations to refer to theorems or simpsets:
-@{ML [display] "@{thm allI}"}
+@{ML_response_fake [display] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
-@{ML [display] "@{simpset}"}
+@{ML_response_fake [display] "@{simpset}" "\<dots>"}
+(FIXME: what does a simpset look like? It seems to be the same problem
+like tokens.)
 While antiquotations have many applications, they were originally introduced to
 avoid explicit bindings for theorems such as
 *}
 @{ML_response_fake [display] "@{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 be found in @{ML_file "Pure/type.ML"}.
+definition and many useful operations can also be found in @{ML_file "Pure/type.ML"}.
 \end{readmore}
 *}
 section {* Constructing Terms and Types Manually *}
 text {*
 We can freely construct and manipulate terms, since they are just
 arbitrary unchecked trees. However, we eventually want to see if a
-term is well-formed, or type checks, relative to a theory.
+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
 interfaces''.
-Type checking is always relative to a theory context. For now we use
+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
 @{ML_response_fake [display] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
 or use the antiquotation
 @{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
-A slightly more elaborate example is
+Attempting
+@{ML_response_fake_both [display] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
+yields an error. A slightly more elaborate example is
 @{ML_response_fake [display]
 "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, which means that all your proofs
+that can only be built by going through interfaces. In effect all proofs
-will be checked.
+are checked.
 To see theorems in ``action'', let us give a proof for the following statement
 *}
 lemma
 @{text "#"} wrapped around it, which prevents that premises are
 misinterpreted as open subgoals. The wrapper @{text "# :: prop \<Rightarrow>
 prop"} is just the identity function and used as a syntactic marker.
 \begin{readmore}
-For more on goals see \isccite{sec:tactical-goals}.
+For more on goals see \isccite{sec:tactical-goals}. (FIXME: in which
+file is most code for dealing with goals?)
 \end{readmore}
 Tactics are functions that map a goal state to a (lazy)
 sequence of successor states, hence the type of a tactic is
 @{ML_type[display] "thm -> thm Seq.seq"}
 THEN resolve_tac [disjI1] 1
 THEN assume_tac 1)
 end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
 \begin{readmore}
-To learn more about the function @{ML Goal.prove} see \isccite{sec:results}.
+To learn more about the function @{ML Goal.prove} see \isccite{sec:results} and
+the file @{ML_file "Pure/goal.ML"}.
 \end{readmore}
 An alternative way to transcribe this proof is as follows

changeset 54	1783211b3494
parent 52	a04bdee4fb1e
child 58	f3794c231898